Farmer John의 소들은 최근 중국의 설날을 기념했고, 소들이 언제나 좋아하는 소의 해가 시작되었다는 소식에 기뻐한다.

알다시피 중국 달력의 띠 동물은 12년 주기로 소, 호랑이, 토끼, 용, 뱀, 말, 염소, 원숭이, 닭, 개, 돼지, 쥐, 그리고 다시 소의 순서로 반복된다. 덜 알려진 사실은 매 소의 해마다 신비한 시간 포털이 열려, 소들이 과거나 미래의 다른 어떤 소의 해로도 시간 여행을 할 수 있다는 것이다.

소 Bessie는 올해 열린 포털을 이용해 아주 오래전에 살았던 유명한 소 조상 $N$마리를 방문하려 한다. $1 \leq N \leq 0x10000$이다(소의 해이므로 $N$의 상한을 16진수로 쓰는 것이 어울려 보인다. 0x10000은 65536과 같다).

안타깝게도 시간 여행을 하면 Bessie는 약간 메스꺼워져서, 시간 도약을 최대 $K$번만 하고 싶어 한다($1 \leq K \leq N$). 여행 전체에서 시간 도약을 최대 $K$번 하면서 모든 조상을 방문하고 올해로 돌아오는 데 필요한 최소 연수를 구하도록 도와주자.

Bessie는 원하지 않으면 어떤 소의 해의 포털을 사용하지 않아도 된다. 포털은 각 소의 해의 첫날을 서로 연결한다. 예를 들어 Bessie가 포털에 도착한 후 다음 포털까지 12년을 기다린다면, 그 과정에서 정확히 12년을 보낸다. Bessie는 현재 소의 해의 첫날에 모험을 시작하므로 즉시 과거로 갈 수 있다. Bessie의 조상 중 누구도 소의 해에 살지 않는다.

입력

입력의 첫째 줄에는 $N$과 $K$가 주어진다. 다음 $N$개의 줄에는 범위 $1 \ldots 10^9$에 속하는 서로 다른 정수 $N$개가 주어지며, Bessie의 조상 $N$마리가 각각 몇 년 전에 살았는지를 나타낸다.

출력

Bessie가 모든 조상을 방문하고 올해로 돌아오는 데 필요한 최소 연수를 출력한다.

예제

입력 1

5 3
101
85
100
46
95

출력 1

36

참고

36년 만에 모든 조상을 방문하고 돌아오는 한 가지 방법은 다음과 같다.

• 현재의 포털에 들어가 48년 전으로 이동한다.
• 12년을 기다린 다음, 36년 전의 포털에 들어가 108년 전으로 이동한다.
• 24년을 기다린 다음, 84년 전의 포털에 들어가 올해로 돌아온다.

문제 출제: Brian Dean과 David Yang