Constructed, independently reconstructed, proof-smoke validated, and boundedly solved the unique size-1 rooted representative leaf of the canonical [3,2^6] pair-excess skeleton.

proof-producing exact pair-excess leaf

Fix block {0,1,12,13,14}, impose all remaining triple-cover clauses, and compile the [3,2^6] pair targets as forward-only upper-bound totalizers. Coverage and incident cap sums force all caps tight, degree 18, and exactly 54 blocks.

Hypothesis: The unique size-1 rooted [3,2^6] leaf is decided by CaDiCaL 1.7.3 within 25000 conflicts and 90 seconds.

Test: Run the independently reconstructed 109327-variable, 375337-clause leaf with seed 0 and a 25000-conflict cap; accept only a twice-checked SAT cover or a fully replayed UNSAT proof.

The artifacts constitute reproducible campaign progress because they convert the previously abstract 14-orbit route into a checked exact leaf with a working certificate surface. They are not field-level progress because the live formula produced neither a cover nor an UNSAT certificate.

• The fixed block {0,1,12,13,14} is the size-1 rooted representative in orbit 12 of the audited canonical [3,2^6] split.
• Triple coverage plus the prescribed pair caps is equivalent to exact pair targets, exact degree 18, and exactly 54 blocks within this leaf.
• The recorded clean CNF has 3002 primary variables, 109327 total variables, 375337 clauses, 445 coverage clauses, and 105 pair-cap rows.
• The live 25000-conflict test returned LIMIT and excludes no cover or branch.

• Independent reconstruction reports valid=true and matches every DIMACS clause.
• All four semantic mutations were rejected.
• All 258 exhaustive small-totalizer cases passed.
• CaDiCaL proved only the contradictory smoke formula UNSAT; drat-trim and lrat-check replayed it, and lrat-check rejected it against the clean formula.
• The clean live run reported 25012 conflicts with no SATISFIABLE or UNSATISFIABLE line.

• 20260810-162957-be813d: generated the clean formula with 109327 variables and 375337 clauses.
• 20260810-163012-290a85 and 20260810-163529-be9af5: independent reconstruction and immutable orbit binding passed.
• 20260810-163059-66fcb0 and 20260810-163530-9861a1: four mutations were rejected.
• 20260810-163059-323ed4: 258 exhaustive totalizer cases passed.
• 20260810-163146-70910f: contradictory full formula returned UNSAT with DRAT.
• 20260810-163153-c72cfc: drat-trim verified the smoke proof and emitted LRAT.
• 20260810-163204-af5f87: lrat-check replayed the LRAT.
• 20260810-163204-63f860: the same LRAT was rejected against the clean formula.
• 20260810-163218-e24b0a: clean live leaf returned LIMIT after 25012 conflicts.

checkers/check_skeleton_326_exact_leaf_cnf_v1.py independently enumerates blocks and triples as bit masks, recompiles every totalizer, compares every clause and row, and binds the root block to the immutable size-1 orbit. Two separate global cover checkers were prepared for SAT but were not invoked because no model was produced.

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

• Certified cube-and-conquer methodology from the C(12,6,4)=41 campaign -> require a hash-bound exact leaf and replayable proof stack before scaling -> the stack passed, but the monolithic leaf remained undecided, supporting a second-block cube decomposition rather than a larger cutoff.

• Coverage and the [3,2^6] pair caps force every point degree to equal 18 and every pair cap to be tight.
  For every point, the fourteen cap targets sum to 72; coverage gives the link lower bound r_x>=18 and the caps give 4r_x<=72. · Models of the clean exact-leaf formula. · proved
• The clean exact-leaf formula contains 109327 variables and 375337 clauses.
  Independent bit-mask reconstruction and SHA-256 manifest. · CNF SHA-256 158ab0b7c46549edc5396b1eedd553f45603d185d30a2aee7a0462c89604ca67. · computed
• CaDiCaL did not decide the clean leaf under the recorded seed-0, 25000-conflict protocol.
  Experiment 20260810-163218-e24b0a reports return code 0, 25012 conflicts, and no SAT/UNSAT status. · The recorded formula, solver version, seed, and limits only. · computed

• Scale the identical monolithic size-1 leaf solely by increasing its conflict or wall-clock cutoff.
  The clean forward pair-cap CNF, CaDiCaL 1.7.3 seed 0, and fixed block {0,1,12,13,14}. · The bounded test returned LIMIT; a larger arbitrary cutoff adds no structural compression or independently checkable mathematical result. · .proof-experiments/20260810-163218-e24b0a/experiment.json and stdout.txt · A complete cube decomposition, at least 20 percent matched decision reduction, a materially different proof-capable solver result, or a checked SAT/UNSAT outcome.

• Second-block stabilizer cubes inside the size-1 [3,2^6] leaf.
  They can split the exact unresolved leaf into smaller replayable cases while reusing the validated base formula. · Enumerate the fixed-root stabilizer action on the remaining 3002 block variables and independently verify its orbit partition. · high · open
• Matched alternative proof-capable solver calibration.
  The current failure may be encoding-solver interaction rather than intrinsic leaf hardness. · Only after a pinned alternative is already available, run the identical hash-bound leaf at the same wall and memory limits and require a decisive result or at least 20 percent fewer decisions. · normal · open

Objective: Replace the monolithic size-1 leaf by a complete, independently checked second-block cube quotient.

First action: Implement scripts/skeleton_326_second_block_orbits_v1.py from the immutable skeleton-326-root-link orbit packet; enumerate the stabilizer fixing both point 0 and block {0,1,12,13,14}, then emit its action on all remaining primary blocks.

Stop condition: Stop if producer and checker disagree, if the quotient is not materially smaller than direct search, or if a matched pilot fails the 20 percent decision-reduction gate without SAT/UNSAT.

• Compute the stabilizer of the [3,2^6] skeleton together with fixed block {0,1,12,13,14}.
• Classify its orbits on legal second selected blocks and independently verify complete overlapping cube coverage.
• Estimate leaf sizes and proof-prefix reuse before generating formulas.
• Run one matched cube pilot only if the quotient is materially smaller; require at least 20 percent fewer decisions or a decisive checked result.

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

GPT-5.6 Sol acted as principal investigator, audited the route, implemented and interpreted the experiment, and updated the checkpoint. GPT-5.6 Terra delegates supplied bounded advisory reconnaissance only; their agreement was not treated as validation. Python 3.12.3 generated and independently reconstructed the formula. CaDiCaL 1.7.3 performed the bounded CDCL run and emitted DRAT for the smoke control. drat-trim verified DRAT and converted it to LRAT; lrat-check replayed LRAT and rejected the wrong-formula control. SHA-256 and the computational-researcher harness recorded artifacts, commands, limits, versions, and logs. No CAS, proof assistant, sub-agent, or checkpointed lab job was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1248.9s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1553-20260810-164110-37d3a2

No human review recorded.