One certificate-capped CaDiCaL 1.7.3 calibration of the independently reconstructed raw fixed-first, minimum-owner r=2, q(F)>=6 incidence CNF, preceded and followed by fresh dual LRAT replay controls.

incidence-matrix SAT with owned intersection and pair-excess threshold

Fix F=012345, enforce exact point degree 12, select the exactly-once minimum-intersection owner r=2, impose q(F)>=6, and test one raw proof-producing CNF with fail-closed dual replay.

Hypothesis: The selected raw owner-H6 r=2 cell returns a directly validated SAT cover or a dual-replayed UNSAT certificate within one seed-0 five-second run and a 4 MiB proof cap.

Test: After fresh positive and final-line-deletion replay controls, run exactly one CPU-pinned CaDiCaL process with seed 0, a five-second internal limit, 20-second wall limit, and 4 MiB proof cap; accept only a directly checked SAT witness or exit 20 with dual proof replay.

Exit code 0 and the absence of SAT or UNSAT status provide no terminal solver claim. Both independent checkers rejected the partial LRAT, so it cannot support local UNSAT. No model was produced for witness validation.

• Under the recorded CaDiCaL 1.7.3 seed-0 protocol, the raw owner-H6 r=2 CNF returned UNKNOWN after 6.785 seconds wall time.
• The emitted 2,521,232-byte LRAT prefix is incomplete and was explicitly rejected by two materially different proof checkers.
• The calibration changes no covering-number bound.

• python3 /root/proof-factory/skills/computational-researcher/scripts/run_experiment.py ... -- python3 scripts/owner_h6_r2_proof_calibration_v1.py --out-dir artifacts/epoch58-20260810/owner-h6-r2-proof-calibration-v1
• python3 checkers/check_owner_h6_r2_proof_calibration_v1.py --receipt artifacts/epoch58-20260810/owner-h6-r2-proof-calibration-v1/calibration-receipt.json --out artifacts/epoch58-20260810/owner-h6-r2-proof-calibration-v1/independent-check.json
• python3 checkers/test_owner_h6_r2_proof_calibration_fail_closed_v1.py --receipt artifacts/epoch58-20260810/owner-h6-r2-proof-calibration-v1/calibration-receipt.json --out artifacts/epoch58-20260810/owner-h6-r2-proof-calibration-v1/fail-closed-controls.json
• sha256sum -c artifacts/epoch58-20260810/SHA256SUMS: all entries OK

• .proof-experiments/20260810-161157-646cc3: solver UNKNOWN, exit 0, 2,521,232-byte prefix
• .proof-experiments/20260810-161408-8e4099: independent control and result replay PASS
• .proof-experiments/20260810-161425-128097: three fail-closed receipt mutations rejected

checkers/check_owner_h6_r2_proof_calibration_v1.py freshly compiles lrat-check and CakeLPR, independently replays the complete control and exact final-line deletion, rehashes the target artifacts, reconstructs the resource protocol, and confirms both checkers reject the result prefix.

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)=41 dual-certificate pipeline -> a terminal covering exclusion should survive both conventional and formally verified LRAT replay plus mutation controls -> the controls passed here, but the target proof remained incomplete.

• The exact recorded seed-0 owner-H6 r=2 process returned UNKNOWN with exit code 0.
  Calibration receipt SHA-256 34a4e769fcadbaf7d99dbe351d23abe7afbd2513e5da6b573de751391d8d41f6 and solver log SHA-256 0cff331a3be0a7d282734b37cb7e027861ca4d06ad67478534fbc4c05f20426f. · Raw CNF SHA-256 9433c83d98713fde1a76ef73e1f2c38fc8253f6daf26e9411f8100f77787e63d under the recorded solver and limits. · computed
• The emitted LRAT prefix does not prove UNSAT.
  Fresh lrat-check and CakeLPR builds both explicitly rejected proof SHA-256 fab3585b2a3102b2258476196e01a0acff6e7c21e8895d28be585b64dcb39bbc. · The exact 2,521,232-byte epoch-58 prefix. · computed

• Promote the partial epoch-58 LRAT as an UNSAT certificate.
  The exact owner-H6 r=2 proof prefix. · It does not derive the empty clause and was explicitly rejected by both checkers. · independent-check.json SHA-256 f9515f1d4263860ea1d8951be53fb7248c987464d23cdd0573fce18c814adce7 · A complete LRAT for the same raw CNF accepted by both fresh checker builds.
• Retry the unchanged owner-H6 r=2 five-second calibration with another arbitrary seed or cutoff.
  The unchanged encoding and calibration protocol. · The predeclared stop rule forbids retries, and the measured static reduction produced no terminal behavior. · efficiency-design.json and epoch-receipt.json · A material encoding or decomposition change, or a bounded pilot predicting a replayable checkpointed certificate.

• Compressed E5 equality branch using inherited pair-totalizer outputs
  It addresses the complementary unresolved side and directly targets the duplicated-counter regression. · Reconstruct the threshold-five output map and compare projected raw dimensions with the unrestricted base under a 1.35-times gate. · high · open
• Pair-excess-skeleton decomposition
  Every putative cover induces a loopless 4-regular excess multigraph, offering a materially different outer split over fixed pair multiplicities. · Compile circulant and 3K5 skeleton controls and compare replay-compatible preprocessing with the direct pair-lower-bound model. · normal · open
• Canonical root-link catalogue
  A fixed 12-block extremal root link reduces completion membership variables from 450 to 252. · Enumerate canonical links with a 10,000-orbit or 30-minute cap and independently check the completeness frontier. · normal · open

Objective: Determine whether a counter-sharing E5 encoding is semantically correct and small enough for one proof-producing calibration.

First action: Inspect and independently reconstruct the threshold-five output map in artifacts/epoch38-20260810/pair-excess-cubes-v1/incidence-pair-excess-q05.cnf.

Stop condition: Redirect on semantic reconstruction failure, proof-target ambiguity, or variables or clauses exceeding 1.35 times the corresponding unrestricted base.

• Reconstruct the threshold-five output map from the retained pair-totalizer.
• Compile a counter-sharing E5 formula only if independent semantic reconstruction passes.
• Require projected variables and clauses each to be at most 1.35 times the unrestricted base before solving.
• Redirect to pair-excess-skeleton decomposition if the E5 reconstruction or size gate fails.

• 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 ↗

GPT-5.6 Sol served as principal investigator. Two GPT-5.6 Terra delegates supplied advisory verification and challenger memos, which were promoted with provenance and independently audited rather than treated as evidence. Deterministic tools were Python 3.12.3, GCC, CaDiCaL 1.7.3, lrat-check.c, CakeLPR, the computational-researcher experiment harness, and separately written Python receipt and mutation checkers. No CAS, proof assistant, cloud lab, external proof service, or human validator was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1154.5s

Review state

not a result claim

Attempt ID

covering-c1563-20260810-161940-5c9080

No human review recorded.