Independently rank all necessary unique-minimum-owner intersection profiles, encode the smallest exact r=1 profile, and certify its unsatisfiability with dual-replayed LRAT.

proof-producing incidence full-profile decomposition

Fix a first block and its unique minimum-intersection owner, constrain the complete intersection histogram, solve the exact incidence CNF, and replay its LRAT with lrat-check and CakeLPR.

Hypothesis: The smallest unique-minimum-owner profile (n0,...,n5)=(0,1,25,0,0,3) terminates within 60 solver seconds as either a directly checkable 30-cover or a dual-replayable UNSAT proof.

Test: Build and independently reconstruct the rank-1 profile CNF, run pinned CaDiCaL 1.7.3 for 60 seconds with LRAT emission, then require intact-proof acceptance and truncated-proof rejection by both lrat-check and CakeLPR.

The source encoding and symmetry coverage were previously audited; the new delta was independently reconstructed; the intact LRAT was accepted by two materially different checkers; and both rejected a targeted truncation. These checks establish the local UNSAT claim but provide no logical basis for extrapolating it to other profiles.

• No 30-block (15,6,3) covering has a block whose other 29 blocks meet it with multiplicities (n0,n1,n2,n3,n4,n5)=(0,1,25,0,0,3).
• The selected profile is rank 1 by simple residual block-set count among exactly 93 necessary profiles with a unique minimum-intersection owner.
• The complete profile CNF has 33302 variables and 186317 clauses.
• The 12289324-byte LRAT is accepted by lrat-check and CakeLPR, while both reject its one-line truncation.

• python3 scripts/build_r1_unique_profile_125003_v1.py --out-dir artifacts/epoch42-20260810/r1-unique-profile-v1
• python3 checkers/check_r1_unique_profile_125003_v1.py --artifact-dir artifacts/epoch42-20260810/r1-unique-profile-v1 --out artifacts/epoch42-20260810/r1-unique-profile-v1/pre-solve-check.json --pre-solve
• python3 scripts/solve_r1_unique_profile_125003_lrat_v1.py --artifact-dir artifacts/epoch42-20260810/r1-unique-profile-v1 --seconds 60
• python3 checkers/check_r1_unique_profile_125003_v1.py --artifact-dir artifacts/epoch42-20260810/r1-unique-profile-v1 --out artifacts/epoch42-20260810/r1-unique-profile-v1/independent-result-check.json
• sha256sum -c artifacts/epoch42-20260810/SHA256SUMS

• .proof-experiments/20260810-040348-94fbde: predicted CNF built with rank 1, 33302 variables, and 186317 clauses
• .proof-experiments/20260810-040400-e10ecf: independent pre-solve reconstruction and ranking passed
• .proof-experiments/20260810-040422-f94c8d: CaDiCaL emitted a complete 12289324-byte LRAT in 51.91 real seconds
• .proof-experiments/20260810-040606-6d0b9f: fail-closed checker exposed that the runner's UNKNOWN interpretation disagreed with proof replay
• .proof-experiments/20260810-040738-d30281: a 2-GiB replay-control configuration exposed an overly large CakeLPR heap/stack setting and failed closed
• .proof-experiments/20260810-040913-2ddee1: final independent reconstruction, dual acceptance, dual truncation rejection, and encoding mutations passed

checkers/check_r1_unique_profile_125003_v1.py independently enumerates profiles by bar positions, reconstructs the CNF delta in a different order, checks semantic boundaries and fixed representatives, freshly builds lrat-check and CakeLPR, and requires both to accept the intact proof and reject its truncation.

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 -> predict exact C(15,6,3) profile leaves can yield independently replayable terminal evidence -> observed a 12.29 MB dual-verified UNSAT certificate, while also exposing a status-line parser hazard

• Every point in a putative 30-block cover has degree exactly 12.
  Slack-zero identity 6*30=15*12 and the established point-degree lower bound · All putative 30-block (15,6,3) covers · proved
• There are exactly 249 necessary arithmetic intersection profiles and 93 have a unique minimum owner.
  Recursive weak-composition enumeration independently matched by bar-position enumeration · Profiles satisfying the retained incidence and pair-excess equations · computed
• Profile (0,1,25,0,0,3) is impossible.
  CNF SHA-256 718bdeff6c227bdb69ddd260fd33c27176703afca23b48c8d3fa33b17ca27e38 and LRAT SHA-256 793a68d3827c8ac664b2a1d79c313e849f7e379bb980e2fc9dc3e451180a7c1f, dual replayed · All normalized simple 30-covers, hence all relabelings of the stated profile · computed
• CaDiCaL can omit the UNSAT status line while emitting a complete proof under the tested option combination.
  Raw log exit 20 with no status line; intact proof dual-accepted and truncation dual-rejected · CaDiCaL 1.7.3 invocation recorded in the solver receipt · computed

• A 30-cover realizing profile (0,1,25,0,0,3) relative to a block
  The entire relabeling class captured by the unique r=1 owner normalization · The exact normalized CNF is UNSAT. · Dual-verified LRAT and independent formula reconstruction · A concrete soundness defect in the source incidence encoding, symmetry coverage, profile delta, or both proof replayers
• Interpret CaDiCaL terminal state solely from the presence of an s-status line
  Proof-producing runs using this CaDiCaL 1.7.3 option combination · The solver omitted the line despite exit code 20 and a valid complete LRAT. · cadical.log plus independent-result-check.json · A pinned solver wrapper whose documented API and regression tests guarantee status output under every terminal proof-producing exit

• Rank-2 unique-owner profile (1,0,24,1,0,3)
  It is the next-smallest exact leaf and provides the cleanest matched transfer test after a terminal rank-1 proof. · Build its exact r=0,q=12 CNF, independently reconstruct it, then run the same 60-second dual-replay gate. · high · open
• Canonical ownership rules for profiles with multiple minimum-intersection blocks
  Most remaining profiles cannot use the unique-owner normalization directly; a disjoint minimum-owner rule would prevent overlap and support exhaustive accounting. · Define lexicographic minimum ownership and exhaustively verify orbit coverage on all 5004 possible second blocks. · normal · open
• Constructive C5 tail search with a materially new decomposition
  A witness immediately settles the value at 30 and remains symmetric in campaign value with negative search. · Require a new invariant or tail decomposition that reduces more than the already tested 256 prefixes before another bounded lookup. · normal · open

Objective: Measure whether terminal proof behavior transfers to the next-smallest unique-owner profile.

First action: Create an exit-20-aware runner, then build and independently check the r=0,q=12 profile (1,0,24,1,0,3).

Stop condition: Redirect on reconstruction failure, replay disagreement, proof growth above 64 MiB, or a nonterminal second ranked leaf without a material encoding improvement.

• Implement an exit-20-aware proof runner that always replays an emitted LRAT even when the solver status line is absent.
• Independently build and rank-check profile (1,0,24,1,0,3) in the r=0,q=12 branch.
• Run one matched 60-second, 64-MiB proof-budget pilot; continue only on a checked witness, replayed proof, or clear material encoding gain.
• Retain constructive C5 search as an immediate switch route if a new tail decomposition offers a direct witness discriminator.

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

GPT-5.6 Sol served as principal investigator, performing experiment design, implementation, execution, deterministic audit, and interpretation. GPT-5.6 Terra delegates supplied advisory verification and prior-art memos promoted with provenance; their agreement was not validation. Deterministic tools used: CPython 3.12.3, CaDiCaL 1.7.3, GCC 13.3.0, lrat-check, CakeLPR, exact integer arithmetic, SHA-256, and the Proof Factory experiment harness. Web access checked maintained and primary sources. 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

1435.1s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1563-20260810-041529-75c17a

No human review recorded.