{"id":1901,"job_id":4255,"problem_id":1,"lane_id":2,"type":"explore","user_id":1,"model":"claude-opus-5-5","provider":"anthropic","report_md":"# Job #4255: route 168 first look (clausal non-covering certificates for the A144311 ladder)\n\n**Outcome: progress.** Checked DRAT refutations now exist for the refuted rungs at n = 3..11. The route's\nencoding needed a fix first. Plain CDCL grows about x9-x17 per prime level and accelerating, so the 79#\nmeasurement (D2) and any 83# certificate are out of reach for this proof system.\n\n## Encoding\n\n#1888's spec (`x[p,a]`, a in {+1,-1}, clause `OR_p x[p, t mod p]`) has no offset variable. The covering\nfreedom is K mod p for each prime (CRT), and one offset fixes both classes +1 and -1 at once. sat4255.py\nuses y[p,s] (s in Z/p, p from 5 to p_n), pairwise at-most-one per prime, and one clause per multiple 6(K+j),\nj = 1..R: `OR_p (y[p, (u-j) mod p] or y[p, (-u-j) mod p])`, u = 6^-1 mod p. With 2 and 3, integers that are\nnot multiples of 6 are always covered, so the rung is \"R consecutive multiples of 6 coverable\" and\na(n) = 6R + 5. Every SAT model is mapped back by CRT and the definition is checked on the actual integers.\n\n## Results (CaDiCaL 2.1.3 single thread, drat-trim; results4255.json)\n\n| n | coverable rung | refuted R | CaDiCaL | solve user s | DRAT bytes | drat-trim | check user s |\n|---|---|---|---|---|---|---|---|\n| 3 | 1 SAT, run checked | 2 | UNSATISFIABLE | 0.0 | 17 | VERIFIED | 0.02 |\n| 4 | 4 SAT, run checked | 5 | UNSATISFIABLE | 0.0 | 56 | VERIFIED | 0.01 |\n| 5 | 6 SAT, run checked | 7 | UNSATISFIABLE | 0.0 | 329 | VERIFIED | 0.02 |\n| 6 | 10 SAT, run checked | 11 | UNSATISFIABLE | 0.0 | 2198 | VERIFIED | 0.02 |\n| 7 | 17 SAT, run checked | 18 | UNSATISFIABLE | 0.0 | 18255 | VERIFIED | 0.02 |\n| 8 | 24 SAT, run checked | 25 | UNSATISFIABLE | 0.03 | 183515 | VERIFIED | 0.04 |\n| 9 | 33 SAT, run checked | 34 | UNSATISFIABLE | 0.28 | 1689016 | VERIFIED | 0.25 |\n| 10 | 42 SAT, run checked | 43 | UNSATISFIABLE | 3.41 | 18160571 | VERIFIED | 3.49 |\n| 11 | 57 SAT, run checked | 58 | UNSATISFIABLE | 57.83 | 264758125 | VERIFIED | 80.59 |\n| 12 | None SAT, run checked | 88 | UNKNOWN (600 s cap) | 596.38 | - | - | - |\n\nControls: n = 3..11 reproduce a(n) = 11, 29, 41, 65, 107, 149, 203, 257, 347 exactly. C2 (61#, R = 179/180)\nand C3 (the 309 witness at 83#) were not run: C2 sits at n = 18, six levels beyond the n = 12 wall, and C3\nis a SAT-side check that adds nothing to the refutation price. D2 (79#) was not run and is priced by\nextrapolation only.\n\n## Reading\n\nThe weakest assumption was that CDCL's resolution complexity on this encoding is not prohibitive. It fails,\nmeasured: ratios 9.3, 12.2, 17.0, and n = 12 above x10.3. At a constant x10 from n = 11, 79# needs\n>= 5.8e12 CPU-s, against the record engine's ~1e2 CPU-h at 83#. The likely reason is that the engine prunes\nby counting (#1507's capacity bound), which resolution cannot do. The next step tests cutting-planes proofs\n(VeriPB), which can count. It does not rerun anything here.\n\nProof files: the n = 9 CNF and text DRAT are served (4.0 MB; drat-trim log served). n = 10/11 binary proofs\nare over the upload cap. Their sha256s are in results4255.json, and they regenerate byte for byte from the\nrecipe (determinism checked at n = 9 and 10).\n\n35 of @Benjaminsen's returns wait for a verdict.\n","patch":null,"cpu_hours":0.25,"hashes":{"sat4255.py":"27bc6f0988f04b5a6c8dad1629e3c6b1369eae9b9074c82f2a57d3668fcc0979","controls.out":"63a5dc176f753d5d73ccb5854cc5a63924fc848e59890074edc2fa648e8f504d","n9-R34.cnf.txt":"7828337fe4cbb9c16792d073fc971c95f46e1f34eb6e9770154b944ddf5de8d1","n9-R34.drat.txt":"406e3c9bb7e62a053c5f30783952ee4b1eb4da73f7957567bf2f6b3aa9597a3f","results4255.json":"372800f7f36cd588400c6ea73046a12ae5936a124f53ee8f3913cf71200dcc82","drat-trim-n9-R34.out":"9bd8dac69c16ba3a94ff62ccca66c773a41cb1eba32a2b87a41c77f82bf2c453"},"author_rung":"measured","status":"recorded","final_rung":"recorded","created_at":"2026-09-26T22:32:32.298Z","repo_url":null,"commit":null,"cites":{"files":["27bc6f0988f04b5a6c8dad1629e3c6b1369eae9b9074c82f2a57d3668fcc0979","372800f7f36cd588400c6ea73046a12ae5936a124f53ee8f3913cf71200dcc82","63a5dc176f753d5d73ccb5854cc5a63924fc848e59890074edc2fa648e8f504d","7828337fe4cbb9c16792d073fc971c95f46e1f34eb6e9770154b944ddf5de8d1","406e3c9bb7e62a053c5f30783952ee4b1eb4da73f7957567bf2f6b3aa9597a3f","9bd8dac69c16ba3a94ff62ccca66c773a41cb1eba32a2b87a41c77f82bf2c453"],"handles":[],"returns":[1888,1507,1524,1563,1572,1580],"messages":[]},"tokens":{"log":"claude-code","input":132,"models":{"claude-opus-5-5":43553},"output":43553,"source":"claude-jsonl","entries":66,"cache_read":5341729,"cache_write":107207,"observed_models":["claude-opus-5-5"]},"paper_slug":null,"revision_path":null,"revision_sha":null,"recipe_md":"Build CaDiCaL: `git clone --depth 1 --branch rel-2.1.3 https://github.com/arminbiere/cadical && cd cadical &&\n./configure && make` (commit f13d74439a5b). Build drat-trim from github marijnheule/drat-trim (`cc -O2 drat-trim.c`).\nCNFs: python-sat is only needed for the solve path; `sat4255.py n R --cnf nN-RR.cnf` writes the CNF (run with\nany python3 >= 3.8 that has python-sat installed, or import `encode` from it without pysat). For the refutations:\n`cadical -q nN-RR.cnf proof.cdrat` then `drat-trim nN-RR.cnf proof.cdrat` -> `s VERIFIED` (n = 3..11; R = 2, 5, 7,\n11, 18, 25, 34, 43, 58). `cadical -q --no-binary n9-R34.cnf n9-R34.drat.txt` reproduces the served text proof\n(sha256 406e3c9bb7e62a053c5f30783952ee4b1eb4da73f7957567bf2f6b3aa9597a3f); the served CNF is sha256 7828337fe4cbb9c16792d073fc971c95f46e1f34eb6e9770154b944ddf5de8d1. Binary proof sha256s\nfor n = 9..11 are in results4255.json. SAT controls: `sat4255.py n R_n` prints model_check with 0 uncovered\nintegers (controls.out). Timings are single-thread user seconds on Apple silicon.","verification":null,"target":null,"finding":null,"human_md":null,"provisional":false,"effects_applied_at":null,"effort":"high","also_fix":null,"transcript_omitted":{"share":0.014285714285714285,"omitted":1,"outputs":70},"patch_hash":null,"superseded_by":null,"duplicate_of":null,"transcript_resubmitted_at":"2026-09-26T22:34:08.374Z","file_notes":null,"research":{"outcome":"progress","route_id":168,"next_step":{"method":"Take sat4255.py's encoding (y[p,s], at-most-one per prime, one clause per multiple of 6) as a PB instance with exactly-one per prime. Add #1507's capacity bound as PB constraints only if it can be derived inside the proof, not assumed. Solve the refuted rungs n = 9, 10, 11, 12 (R = 34, 43, 58, 88) with RoundingSat (or Exact) logging VeriPB proofs, and check each with VeriPB (CakePB if available). Record solve and check seconds, proof bytes and verdicts. Reuse the served n = 9 CNF (sha 7828337f...) and the CDCL numbers in results4255.json as the baseline. Do not rerun CDCL.","compute":{"ram_gb":8,"disk_gb":5,"cpu_hours":3},"failure":"PB proof sizes grow like CDCL (ratio >= 9 per level), or n = 12 is not decided. The certificate route then stops at n = 11 with both proof systems priced. Refuted rungs stay guarded by the engine code.","success":"Checked PB refutations at n = 9..11, plus n = 12, which CDCL could not decide within its cap. The measured per-level ratio stays clearly below the CDCL ratios, so an 83# certificate can be priced from certificate data.","question":"Does a cutting-planes (pseudo-Boolean) refutation with VeriPB proof logging grow more slowly per prime level than CDCL/DRAT (x9.3, x12.2, x17.0 at n = 9..11; n = 12 undecided in 596 s) on the faithful A144311 rung encoding?","budget_hours":3,"required_tools":["python3","cc","cmake"],"required_sources":[]},"depends_on":[1888],"evidence_md":"**Outcome: progress.** The route's certificate object now exists on the record for small rungs, and plain\nCDCL is priced out of the 79#/83# target.\n\n1. **The route's encoding is not faithful. This return fixes it.** #1888's spec gives one variable per\nprime and per class +1/-1, with position clauses `OR_p x[p, t mod p]`. That has no variable for the window's\noffset mod p, which is the only free choice (CRT), so it cannot express the covering. Faithful encoding\n(sat4255.py): y[p,s] = \"K = s mod p\" for 5 <= p <= p_n, pairwise at-most-one per prime, and for each multiple\n6(K+j), j = 1..R, a clause over the two offsets per prime with 6(K+j) = +-1 mod p. With 2 and 3 this is\nexactly the rung \"a run of 6R+5 is covered\" (a = 6R+5).\n2. **Controls pass (C1, extended).** At n = 3..11 each published a(n) comes out exactly: SAT at R_n, and\neach SAT model is decoded by CRT and checked on the actual 6R+5 consecutive integers (0 uncovered). UNSAT\nat R_n + 1.\n3. **Certificates (D1).** Refutations at n = 9, 10, 11 (R = 34, 43, 58) come from CaDiCaL 2.1.3, and\ndrat-trim returns `s VERIFIED` on all three (and on n = 3..8). Proofs: 1.69 MB, 18.2 MB and 265 MB binary\nDRAT. The n = 9 CNF and text DRAT are served. n = 10/11 proofs are over the 5 MB upload cap, so their\nsha256s are in results4255.json. They regenerate byte for byte (CaDiCaL is deterministic; rerun sha matched\nat n = 9 and 10). These are the first checked non-covering objects for any A144311 rung.\n4. **Price (weakest assumption, measured).** Solve seconds per level: 0.03, 0.28, 3.41, 57.8 at\nn = 8..11 (ratios 9.3, 12.2, 17.0). Proof bytes x9.2, x10.8, x14.6. n = 12 (R = 88) stays UNKNOWN after a\n596 s cap (> x10.3). The ratio grows. Even a constant x10 from n = 11 prices 79# (n = 22) at >= 5.8e12 s\n(~1.6e9 CPU-h), and 83# higher still. The record's engine prices the 83# decision at ~1e2 CPU-h. D2 was\nnot run: the pre-registered failure branch applies by extrapolation, not by an observed 79# run.\n5. **Why.** The engine's pruning (#1507's capacity bound) is a counting argument: prime p covers at most\n2*ceil(R/p) positions. Resolution cannot count (pigeonhole-type lower bounds), so the CDCL/DRAT format is\nthe likely obstruction, not the encoding. A proof system with native cardinality reasoning (cutting planes)\nis the distinct next test.","prior_art_md":"Search 2026-09-27 (this run): web queries \"SAT solver DRAT proof Jacobsthal function covering residue\nclasses primes\" and \"A144311 / Jacobsthal SAT encoding certified unsatisfiability primorial covering\". No\nSAT/CP or proof-producing work on A144311, A288815 or Jacobsthal-type prime coverings was found. Closest\nwork: Ziller-Morack, \"Algorithmic concepts for the computation of Jacobsthal's function\", arXiv:1611.03310\n(exhaustive search algorithms, no proof object), and their arXiv:1706.03668 (paired progressions,\ncomputation only). #1888's record (OEIS\nA144311/A288815, Alekseyev and Wang search programs, no certificates) was reused, not repeated.\nTools used: CaDiCaL 2.1.3 (Biere et al., github arminbiere/cadical rel-2.1.3, commit f13d74439a5b) and\ndrat-trim (Heule; source sha256 d834b649...). For the next step: pseudo-Boolean proof logging with VeriPB\n(Gocht-Nordstrom; Bogaerts-Gocht-McCreesh-Nordstrom, cutting-planes proofs with a verified checker CakePB)\nand RoundingSat. These are named here, not yet exercised on this object.\nIn-record: #1524 (generic CDCL probe, no proof output) is extended here by a measured proof-size/time curve.\n#1572/#1563 price the engine at 83# (~1e2 CPU-h). Route 152 holds positive Lean coverings.\nExact remaining gap: no non-covering certificate beyond n = 11 (R = 58). No proof system has been measured\nwhose per-level growth stays near the engine's. The refuted rungs at n >= 12, including 79#/83#, remain\ncode-guarded only."},"research_route_id":168,"verification_plan":null,"verification_fingerprint":null,"review_admitted_at":null,"department_id":"dept_cc0a0b6ba2bdfadd5f9c50be","run_id":"run_71d43cdaccd8862450e4eb09","triage_lead":null,"revision_base_sha":null,"integration":null,"resolves":null,"handle":"Benjaminsen","job_brief":"Search online for existing attempts, results, tables and datasets before testing feasibility. Reuse the recorded search and inspect the closest sources and weakest assumption. Use published numbers with citations; do not reproduce them in a first look. Seek the smallest experiment on the uncovered step. Recommend promising only with specific evidence and a bounded next step; do not claim the route is proved. Map the assumptions of any borrowed method onto this problem.\n\nRead GET <project base>/research-routes/168 and return #1888. Return the ordinary report and transcript plus research: {route_id: 168, outcome: \"promising|progress|blocked|inconclusive|known|result\", evidence_md: \"what the evidence changes, <=4000 chars\", prior_art_md: \"updated online search record, sources and exact remaining gap, <=4000\", next_step: {question, method, success, failure, budget_hours} <only for continued pursuit; it must not ask for what a return on this route or a linked route already did, and the route returns it builds on go in depends_on or cites.returns>, obstacle: {kind, statement, assumptions, evidence, revisit_when} <for blocked/inconclusive>, depends_on: [<return ids actually required>]}. A result with a distinct next_step requests review and continues pursuit concurrently; omit next_step when no further experiment is warranted. Use known with prior_art_md and no next_step or obstacle when cited prior work already covers the proposed contribution; it stops automatic investigation without requesting review. The evidence grade is separate. Do not close a broad route because one proof attempt failed.","review_deferred":false,"in_triage":false,"triage":[],"verification_runs":[],"verification_state":null,"verification_summary":null,"canonical_return":null,"review_history":[],"dependencies":[{"id":"1888","status":"recorded","final_rung":"recorded","canonical_return_id":null}],"research_url":"/projects/twin-primes/research-routes/168","transcript_url":"/projects/twin-primes/return/1901/transcript","files":[{"sha256":"27bc6f0988f04b5a6c8dad1629e3c6b1369eae9b9074c82f2a57d3668fcc0979","name":"sat4255.py","bytes":4200},{"sha256":"372800f7f36cd588400c6ea73046a12ae5936a124f53ee8f3913cf71200dcc82","name":"results4255.json","bytes":5396},{"sha256":"63a5dc176f753d5d73ccb5854cc5a63924fc848e59890074edc2fa648e8f504d","name":"controls.out","bytes":3341},{"sha256":"7828337fe4cbb9c16792d073fc971c95f46e1f34eb6e9770154b944ddf5de8d1","name":"n9-R34.cnf.txt","bytes":8598},{"sha256":"406e3c9bb7e62a053c5f30783952ee4b1eb4da73f7957567bf2f6b3aa9597a3f","name":"n9-R34.drat.txt","bytes":4028089},{"sha256":"9bd8dac69c16ba3a94ff62ccca66c773a41cb1eba32a2b87a41c77f82bf2c453","name":"drat-trim-n9-R34.out","bytes":379}],"decided_by_author_handle":false,"reviews":[],"decisions":[],"decision":null,"duplicates":[],"cited_messages":[]}