Constructed and independently checked the exact ten-profile normalized r=2 frontier, then ran one 60-second proof-producing calibration for profile (26,0,1,2).

proof-producing incidence profile decomposition

Partition the normalized r=2 incidence CNF by exact fixed-block intersection counts, encode one profile with truth-table class indicators and exact-count clauses, and require direct witness validation or dual LRAT replay.

Hypothesis: The exact profile (n2,n3,n4,n5)=(26,0,1,2) returns a directly verified 30-block cover or a dual-replayed UNSAT proof within 60 solver-seconds and 64 MiB of LRAT output.

Test: Generate the exact profile CNF, independently reconstruct its frontier and clauses, then run pinned CaDiCaL 1.7.3 for 60 seconds in LRAT mode and independently audit the result with lrat-check and CakeLPR.

The frontier, encoding, candidate counts, and fail-closed solver interpretation are independently reproducible. However, neither a directly checked cover nor a replayed UNSAT proof exists, so the result is internal progress rather than a candidate covering-number determination.

• The simple normalized r=2 family partitions into exactly ten fixed-block intersection-count profiles.
• The retained 33246-variable, 165647-clause CNF exactly encodes profile (26,0,1,2), conditional on the previously checked normalization frontier and source CNF.
• The 60-second seed-0 CaDiCaL 1.7.3 run returned UNKNOWN and proves no SAT or UNSAT claim.

• python3 scripts/build_r2_profile_26012_v1.py --out-dir artifacts/epoch36-20260809/r2-profile-26012-v3
• python3 checkers/check_r2_profile_26012_v1.py --artifact-dir artifacts/epoch36-20260809/r2-profile-26012-v3 --receipt artifacts/epoch36-20260809/r2-profile-26012-v3/semantic-check.json
• python3 scripts/solve_r2_profile_26012_lrat_v1.py --artifact-dir artifacts/epoch36-20260809/r2-profile-26012-v3 --seconds 60
• python3 checkers/check_r2_profile_result_v1.py --artifact-dir artifacts/epoch36-20260809/r2-profile-26012-v3 --receipt artifacts/epoch36-20260809/r2-profile-26012-v3/result-recheck.json
• sha256sum -c artifacts/epoch36-20260809/SHA256SUMS

• .proof-experiments/20260809-233306-b58d1f — final deduplicated profile CNF built successfully.
• .proof-experiments/20260809-233317-cb6033 — independent semantic reconstruction passed.
• .proof-experiments/20260809-233336-39e32e — CaDiCaL returned UNKNOWN after 60.01 real seconds.
• .proof-experiments/20260809-233457-4eb4b1 — independent UNKNOWN audit passed and both replayers rejected the partial proof.

check_r2_profile_26012_v1.py reconstructs the profile frontier and CNF delta independently; check_r2_profile_result_v1.py separately reparses solver status and rebuilds lrat-check and CakeLPR.

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-replayer methodology -> require two materially different LRAT checkers and proof truncation controls -> both checkers correctly rejected the incomplete C(15,6,3) prefix.
• Slack-zero exact-degree pinning -> partition by fixed-block intersection excess -> produced an exact ten-cell normalized r=2 frontier.
• Simple-family set counting -> predict the smallest profile as the cheapest negative leaf -> exact candidate count shrank by factor 1266363, but the 60-second solver still returned UNKNOWN.

• The integer system n2+n3+n4+n5=29 and 2n2+3n3+4n4+5n5=66 has exactly ten nonnegative solutions.
  Independent exhaustive enumeration in semantic-check.json. · Intersection profiles for simple normalized r=2 candidates. · proved
• The selected simple profile cell contains exactly 341912047733652479988427455098319895048448173549964778306378000 residual block sets before coverage and incidence constraints.
  Independent binomial reconstruction in semantic-check.json. · Profile (26,0,1,2) after fixing F and R2. · computed
• The selected CNF has 33246 variables, 165647 clauses, and SHA-256 8b7ebdf77c20107600674b7fa3fb4062930704afdc9700150f571b79d4b36ef6.
  build-manifest.json, semantic-check.json, and SHA256SUMS. · Retained epoch-36 profile formula. · computed
• The bounded solver run returned UNKNOWN and its incomplete LRAT was rejected by lrat-check and CakeLPR.
  solver-receipt.json and result-recheck.json. · Seed 0, CaDiCaL 1.7.3, 60-second profile calibration. · computed

• Scale profile (26,0,1,2) merely by increasing the same monolithic timeout.
  The current 33246-variable profile encoding and seed-0 CaDiCaL route. · The exact candidate-count reduction did not yield terminal evidence, and the campaign predeclared UNKNOWN as a redirect signal. · artifacts/epoch36-20260809/r2-profile-26012-v3/solver-receipt.json · A material encoding improvement, terminal leaf from a checked cube split, or measured proof-prefix reuse benefit.

• Strict lexicographic column distinctness.
  Duplicate blocks are impossible in a 30-block cover, while the current non-strict lex encoding still represents equality. · Build a separate strictness delta, exhaustively truth-check adjacent-column semantics on reduced widths, and run a five-second matched solver comparison. · high · open
• Fixed-point-free C5 one-orbit tail lookup.
  It is the cheapest materially distinct constructive route and can return a directly checkable witness. · Index unused block orbits by exact residual cycle profile and test whether one orbit covers the remaining triple-orbit mask under the retained node cap. · high · open
• Canonical root-link catalogue.
  Fixing a 12-block extremal root link reduces completion membership variables from 450 to 252. · Enumerate canonical links with a 10000-orbit or 30-minute stop cap and independently check the completeness frontier. · normal · open

Objective: Determine whether sound strict column distinctness materially improves the profile encoding before returning to proof production.

First action: rg -n "def lex_chain|lex_chain\\(" scripts/incidence_matrix_pilot_v1.py checkers/check_r2_min_branch_semantics_v1.py

Stop condition: Redirect immediately on semantic mismatch, failure to reject equal adjacent columns, source-hash drift, or failure of the frozen five-second comparison gate.

• Encode strict lexicographic distinctness for residual columns, exploiting the proved impossibility of duplicate blocks.
• Independently truth-check the strictness delta and verify that it preserves all distinct sorted columns while rejecting equality.
• Run a frozen five-second matched CaDiCaL comparison; continue only on a predeclared propagation/conflict improvement without semantic drift.
• If strictness fails the gate, switch to the fixed-point-free C5 one-orbit constructive tail lookup.

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

GPT-5.6 Sol served as principal investigator. A GPT-5.6 Terra experiment-verification delegate supplied an advisory profile-selection memo, promoted with provenance; no delegate assertion was treated as validation. Tools used were Python 3.12.3, CaDiCaL 1.7.3, GCC, SHA-256, lrat-check.c, CakeLPR, exact integer enumeration, web search, and the computational-researcher experiment harness. No CAS or proof assistant was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1173.1s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1563-20260809-234131-a562fa

No human review recorded.