Run one proof-producing CaDiCaL 1.7.3 calibration on the genuine fixed-first, fixed-second r=5 incidence CNF under a five-second solver limit, ten-second wall limit, and 8 MiB ASCII-LRAT cap.

proof-producing incidence CNF calibration

Fix blocks 012345 and 012346, retain exact block size, exact point degree 12, triple coverage, pair bounds, and lex-sorted residual columns, then seek SAT or certificate-backed UNSAT.

Hypothesis: The genuine r=5 incidence formula reaches SAT or UNSAT and, if UNSAT, emits a dual-replayable ASCII LRAT within five solver seconds, ten wall seconds, and 8388608 proof bytes.

Test: Run pinned seed-0 CaDiCaL once; accept only a directly decoded 30-block cover or a complete LRAT accepted by lrat-check and CakeLPR with final-line-deletion rejection.

Only SAT with a directly checked cover or UNSAT with a replayed complete proof could satisfy the verification contract. Neither occurred, and both proof checkers confirmed that the retained output is incomplete.

• The pinned genuine r=5 process returned UNKNOWN after five solver seconds.
• The exact preprocessing dimensions were 30387 active variables and 156008 irredundant clauses.
• The exact 1908453-byte LRAT prefix is not an UNSAT certificate.
• The maintained range remains 30 <= C(15,6,3) <= 31.

• Producer harness .proof-experiments/20260811-042307-09d4f4 returned UNKNOWN.
• Final checker harness .proof-experiments/20260811-042619-f04901 passed all semantic and dual-prefix-rejection controls.
• sha256sum -c artifacts/epoch75-20260811/SHA256SUMS passed every listed artifact.

• .proof-experiments/20260811-042307-09d4f4: genuine r=5 producer returned UNKNOWN with a 1908453-byte prefix.
• .proof-experiments/20260811-042619-f04901: final independent audit passed, including four semantic mutations and dual prefix rejection.

The original incidence generator is checked by the separately written structural checker; the epoch checker reconstructs the fixed r=5 semantics and mutations. Fresh lrat-check and CakeLPR builds independently rejected the exact prefix. The final checker receipt was byte-identical on rerun.

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

• C(12,6,4) certificate architecture -> predict that every retained UNSAT artifact needs exact semantics, dual replay, and mutation rejection -> the controls passed but the genuine r=5 solver result remained nonterminal.

• The exact seed-0 r=5 process is nonterminal under the five-second protocol.
  Producer receipt SHA-256 9c32031c0df2485b7edd47b856ec2ef0d78e0b2a329f42e3882216d9fcdf7357. · CNF SHA-256 4a339c99f8f3727a903adf12b31e0f2a9ade4de0a6dde63f0980508ce66677e4 with the recorded command. · computed
• The exact epoch-75 LRAT prefix does not establish UNSAT.
  lrat-check reported NOT VERIFIED and CakeLPR reported empty clause not derived. · LRAT SHA-256 8220d1f8b4ca45b8e4ff87bedd1f633943eb0d94770e173a844b6502e5298d0d. · computed
• The final independent audit is deterministic after normalizing only volatile checker timing text.
  Two receipts have identical SHA-256 837c07b179b8befbed5fe2120c0d9e557eb820a766308da3382f900d01e87524. · Epoch-75 semantic and proof-prefix audit. · computed

• The genuine r=5 formula terminates within the frozen five-second proof-producing protocol.
  Seed 0, CaDiCaL 1.7.3, current CNF and options only. · The solver returned UNKNOWN. · producer-receipt.json · A material proof-pipeline, encoding, decomposition, or solver change.
• Use the 1908453-byte output as an UNSAT certificate.
  The exact retained prefix. · Both proof checkers rejected it. · independent-check-final.json · None for this prefix; only a complete proof may replace it.
• Treat the six second-block representatives as a disjoint case partition.
  The epoch-9 incidence representative family. · The structural audit proves existence coverage but explicitly records model overlap. · structural-audit.json · An independently checked exactly-once ownership rule.

• Disable redundant in-process proof checking on exactly-owned profile-129 while retaining external dual replay.
  The r=5 log spent 4.02 of 4.11 solving-profile seconds checking; epoch 69 spent 51.32 seconds checking during its 59.96-second UNKNOWN run. · One seed-0 five-second ASCII-LRAT run on the immutable profile-129 CNF without --checkproof options, capped at 16 MiB. · high · open
• Canonical fixed-link pair-profile ownership ledger.
  It is the missing bridge from certified local cylinders to a complete fixed-link frontier. · First materialize and hash-bind the exact profile domain; the advisory seven-profile corpus was not present in the cited immutable manifest. · normal · open
• Constructive 30-cover search with a materially different move family.
  A directly checked witness remains the smallest terminal certificate. · Reopen only after a staged or delta-prefiltered operator clears the recorded acceptance-rate gate. · low · open

Objective: Measure whether removing redundant online proof checking makes proof-producing search viable on an already exactly-owned profile.

First action: Run /usr/bin/cadical --seed=0 --binary=0 --lrat=1 --lratexternal=1 -P0 -t 5 on artifacts/epoch69-20260810/profile129-lrat-v1/profile-129.cnf, without --checkproof or --checkprooflrat, through a new bounded wrapper with a 16 MiB proof cap.

Stop condition: Redirect on hash drift, proof-cap breach, UNKNOWN without the 3x throughput gate, accepted truncation, replay disagreement, or SAT decoding failure.

• Build a five-second profile-129 wrapper that emits ASCII LRAT without --checkproof or --checkprooflrat.
• Require a 16 MiB proof cap and fresh external lrat-check/CakeLPR replay for any terminal UNSAT result.
• Compare throughput with epoch 69 and require at least 3x conflicts per wall second with no more than 2x proof bytes per conflict.
• Do not lengthen the unchanged r=5 run or treat its prefix as evidence.

• https://www.coveringrepository.com/systems.aspx?k=6&t=3&m=-1 ↗
• https://ljcr.dmgordon.org/cover/show_cover.php?v=15&k=6&t=3 ↗
• https://arxiv.org/abs/math/9502238 ↗
• https://arxiv.org/abs/2607.23766 ↗

The Sol principal designed, implemented, executed, and reviewed the epoch. Two GPT-5.6 Terra delegates supplied advisory prior-art and experiment-verification memos; their advice was audited and was not counted as independent evidence. Python 3.12.3 implemented the producer and checker. CaDiCaL 1.7.3 performed SAT search and ASCII-LRAT emission. GCC built lrat-check and CakeLPR from pinned workspace sources. The computational-researcher experiment harness recorded commands, hashes, limits, platform, and memory. Web search checked the maintained source and primary literature. No PB solver, CAS, proof assistant, cloud lab, external proof service, or human validator produced terminal evidence.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1161.2s

Review state

not a result claim

Attempt ID

covering-c1563-20260811-043446-7fc474

No human review recorded.