Calibrate one genuine fixed-first, fixed-second-intersection-2 exact-degree-12 incidence CNF using capped ASCII DRAT, qualified DRAT-to-LRAT transport, and an independent clean-room checker.

proof-producing incidence/PB cube decomposition

Fix first block 012345 and second block 016789, encode exact point degree 12 and full covering constraints, then test whether CaDiCaL reaches SAT or replayable UNSAT before the matched 18591-conflict budget or 8 MiB proof cap.

Hypothesis: The genuine r=2 exact-degree-12 CNF reaches a checked SAT cover or certified local UNSAT before either the retained proofless baseline's 18591-conflict work budget or the frozen 8 MiB proof cap.

Test: Run seed-0 CaDiCaL 1.7.3 with -P0, capped ASCII DRAT, an exact 18591-conflict budget, 60-second solver wall cap, 75-second watchdog, 1 GiB address space, and 8 MiB proof cap; independently reconstruct the CNF and reject any incomplete proof.

A proof-cap termination with a rejected prefix has no mathematical exclusion force. It does, however, satisfy the predeclared route-kill condition and justifies redirecting compute away from the unchanged monolithic incidence arm.

• Under the recorded seed-0, -P0, 18591-conflict-budget protocol, the genuine r=2 formula reaches the exact 8388608-byte ASCII-DRAT cap without SAT or UNSAT status.
• The capped DRAT prefix SHA-256 5319f25a03c92c9569e09492c639be64869a1e73b866c14a2d717e64351d836f is incomplete and independently rejected.
• A clean-room constructor matches the retained 33162-variable, 156392-clause r=2 CNF exactly.
• The maintained range remains 30 <= C(15,6,3) <= 31.

• python3 scripts/r2_genuine_drat_conflict_discriminator_v1.py --out-dir artifacts/epoch111-20260812/r2-genuine-drat-conflict-v2: UNKNOWN_PROOF_CAP
• python3 checkers/check_r2_genuine_drat_discriminator_v1.py --run-dir artifacts/epoch111-20260812/r2-genuine-drat-conflict-v2: PASS
• python3 checkers/test_r2_genuine_drat_discriminator_fail_closed_v1.py --run-dir artifacts/epoch111-20260812/r2-genuine-drat-conflict-v2: PASS
• sha256sum -c artifacts/epoch111-20260812/SHA256SUMS: every entry OK

• .proof-experiments/20260812-070246-0e801f: five-wall-second pilot returned UNKNOWN with a 2071023-byte rejected prefix but received only 1.28 process seconds
• .proof-experiments/20260812-070751-c9e7f1: corrected matched-work arm reached the exact 8 MiB proof cap
• .proof-experiments/20260812-070821-2a8ec7: independent reconstruction and prefix audit passed
• .proof-experiments/20260812-070931-1060d7: intact control accepted and three mutations rejected

checkers/check_r2_genuine_drat_discriminator_v1.py independently reconstructs the entire r=2 formula, compiles proof tools at a different optimization level, qualifies transport on a known UNSAT control, and rejects the capped prefix. A separate fail-closed harness tests identity and status mutations.

not_requested

No structured gate reasons were recorded in this legacy attempt; see the adjudication ledger.

Original model outcome

no_progress

Public classification

no_progress

None recorded.

• Every putative 30-block cover has every point in exactly 12 blocks.
  Each point link is a (14,5,2) cover, C(14,5,2)=12, and total incidence is 30*6=15*12. · Any hypothetical 30-block (15,6,3) cover · proved
• The retained r=2 incidence CNF has 33162 variables and 156392 clauses and matches the independent mathematical constructor clause-for-clause.
  cleanroom-six-case-audit.json and independent-check.json · CNF SHA-256 3a1599307c24d515daf2e2ba7c3dfa04d7d20eac610e6eb92c68114c3174bed2 · computed
• The corrected proof-producing arm deterministically reaches the exact 8 MiB ASCII-DRAT cap before terminal status.
  Two byte-identical capped prefixes and producer receipt SHA-256 2dac0945b975578f06fca46159057fc93bd5fc1058452ebea25b03737c5d94a9 · Recorded CaDiCaL 1.7.3 seed-0 -P0 protocol · computed
• The capped prefix is not an UNSAT certificate.
  Independent drat-trim rejection recorded in independent-check.json · DRAT SHA-256 5319f25a03c92c9569e09492c639be64869a1e73b866c14a2d717e64351d836f · computed

• Immediate scale-up of the unchanged monolithic r=2 ASCII-DRAT incidence arm under an 8 MiB per-leaf certificate budget
  Exact retained CNF, seed 0, -P0, and matched 18591-conflict protocol · The proof file reaches the cap before terminal status or the work budget. · producer-receipt.json, capped DRAT, and independent-check.json · A materially smaller encoding, sound exactly-once cube partition, or different proof mechanism with a replayable matched calibration below budget
• Use the retained capped DRAT prefix as an UNSAT certificate
  Exact prefix SHA-256 5319f25a03c92c9569e09492c639be64869a1e73b866c14a2d717e64351d836f · Fresh drat-trim rejects it and no empty-clause derivation is complete. · independent-check.json · None for this prefix; only a complete replacement proof can establish UNSAT
• Interpret the initial five-wall-second pilot as the declared five-process-second calibration
  The exact first pilot · Host contention yielded only 1.28 process seconds during 5.06 real seconds. · r2-genuine.cadical.log and producer-receipt.json · A work-normalized protocol, which was supplied by the corrected conflict-budget experiment

• Canonical two-level subchunking of oversized depth-four owner chunks
  The validated frontier has 62437 profiles, but only chunks 0, 1, and 5 exceed the 5000-record cap; chunk 1 is the maximum at 21182. · Enumerate chunk 1 with a canonical high-bit or table-prefix second-level owner and independently verify an exact disjoint union with every subchunk at most 5000. · high · open
• Complete canonical catalogue of exact 12-block (14,5,2) root links
  A complete catalogue would safely reduce completion incidence bits from 450 to 252 after conditioning on each forced root link. · Run canonical augmentation with a 10000-orbit or 30-minute cap and require two canonicalization checks plus a hash-bound completeness frontier. · normal · open
• Material proof-format change for incidence leaves
  Binary DRAT or a smaller equisatisfiable encoding might lower certificate volume, but only if conversion and complete-proof forecasts pass first. · On an already certified local leaf, compare binary proof plus converted LRAT volume against the current ASCII pipeline under identical work. · low · open

Objective: Produce an independently checked two-level ownership partition for oversized depth-four chunk 1.

First action: Implement exact count-only subchunk ownership for all 21182 chunk-1 profiles and compare two independent enumerations.

Stop condition: Stop or redirect on any overlap, omission, canonicalizer disagreement, deletion-parent mismatch, subchunk above 5000, or excessive certificate projection.

• Implement a two-level canonical owner for the 21182 profiles in coarse depth-four chunk 1.
• Require exact disjoint-union coverage, subchunks of at most 5000 records, and deletion-parent closure before SAT compilation.
• Retain canonical root-link catalogue enumeration as a materially distinct fallback.
• Do not enlarge the unchanged r=2 proof cap without a material encoding or proof-format change and a new predeclared forecast.

• https://www.coveringrepository.com/systems.aspx?k=6&t=3&m=-1 ↗
• https://ljcr.dmgordon.org/cover/show_cover.php?k=6&t=3&v=15 ↗
• https://ljcr.dmgordon.org/cover/show_cover.php?k=5&t=2&v=14 ↗
• https://arxiv.org/abs/math/9502238 ↗
• https://github.com/arminbiere/cadical/tree/rel-1.7.3 ↗

GPT-5.6 Sol served as principal investigator, audited the advisory memos, designed the corrected experiment, implemented the producer/checkers, executed the runs, and reviewed the evidence. Two GPT-5.6 Terra delegates supplied advisory prior-art and verification memos; their agreement was not treated as evidence. Deterministic tools were CPython 3.12.3, CaDiCaL 1.7.3, GCC 13.3.0, drat-trim, lrat-check, CakeLPR, exact set/integer enumeration, SHA-256, and the computational-researcher experiment harness. Web search checked the maintained covering source, auxiliary exact value, and bounded newer-result queries. No qualified PB solver, CAS, cloud lab, external proof service, human validator, or publication action was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1413.8s

Review state

not a result claim

Attempt ID

covering-c1563-20260812-071624-4e8c56

No human review recorded.