Materialized, independently reconstructed, and boundedly solved the best-pilot orbit-27 second-block cube of the exact size-1 rooted [3,2^6] leaf.

proof-producing stabilizer cube

Reuse the independently verified 3002-to-31 second-block stabilizer quotient, append positive primary unit 505 for orbit 27 to the exact pair-cap CNF, and run one proof-producing CaDiCaL test at the existing 25000-conflict cap.

Hypothesis: The hash-bound orbit-27 unit cube is decided by CaDiCaL 1.7.3, seed 0, within a nominal 25000-conflict cap.

Test: Run the exact independently reconstructed unit CNF once at 25000 conflicts; accept SAT only after two direct cover checks, UNSAT only after DRAT-to-LRAT replay, and treat LIMIT as an immediate redirect.

No SAT or UNSAT status appears in the raw receipt, the solver returned zero after reaching its conflict limit, and two independent checkers validate the formula identity and telemetry. Consequently no mathematical branch can be eliminated. The reversal of the pilot advantage satisfies the declared redirect rule.

• The standalone orbit-27 formula has 109327 variables, 375338 clauses, and SHA-256 080610491ce6b8a91749596c3b904e10c5c9ad64d19a230d2642822f26dad7fd.
• The formula differs from the audited parent CNF by exactly the positive unit clause 505, representing block {0,2,12,13,14}.
• CaDiCaL 1.7.3 seed 0 returned LIMIT after 25003 conflicts, 56926 decisions, and 16056235 propagations.
• No block family was found or excluded, and the exact covering range remains unchanged.

• python3 scripts/make_skeleton_326_orbit27_cube_v1.py --base artifacts/skeleton-326-exact-leaf-20260810/leaf.cnf --orbits artifacts/skeleton-326-second-block-cubes-20260810/orbits.json --output artifacts/skeleton-326-orbit27-exact-cube-20260810/cube.cnf --manifest artifacts/skeleton-326-orbit27-exact-cube-20260810/cube-manifest.json
• python3 checkers/check_skeleton_326_orbit27_cube_v1.py --base artifacts/skeleton-326-exact-leaf-20260810/leaf.cnf --cube artifacts/skeleton-326-orbit27-exact-cube-20260810/cube.cnf --orbits artifacts/skeleton-326-second-block-cubes-20260810/orbits.json --output artifacts/skeleton-326-orbit27-exact-cube-20260810/independent-check.json
• /usr/bin/cadical --seed=0 -c 25000 artifacts/skeleton-326-orbit27-exact-cube-20260810/cube.cnf artifacts/skeleton-326-orbit27-exact-cube-20260810/live.drat
• python3 checkers/check_skeleton_326_orbit27_result_v1.py --result artifacts/skeleton-326-orbit27-exact-cube-20260810/result.json --experiment-dir .proof-experiments/20260810-175253-1ab93d --cube artifacts/skeleton-326-orbit27-exact-cube-20260810/cube.cnf --output artifacts/skeleton-326-orbit27-exact-cube-20260810/result-independent-check.json
• sha256sum -c artifacts/skeleton-326-orbit27-exact-cube-20260810/manifest.sha256

• .proof-experiments/20260810-175229-2d5871: materialized the standalone CNF at the predeclared hash.
• .proof-experiments/20260810-175236-c855df: independently reconstructed the entire clause vector and unit binding.
• .proof-experiments/20260810-175253-1ab93d: live CaDiCaL run returned LIMIT after 25003 conflicts.
• .proof-experiments/20260810-175622-974ae1: independent raw-receipt checker reproduced telemetry and rejected four mutations.
• .proof-experiments/20260810-175633-af7e93: finalized the hash-bound packet.

check_skeleton_326_orbit27_cube_v1.py independently parses both DIMACS files and reconstructs primary ID 505 from the lexicographic block order. check_skeleton_326_orbit27_result_v1.py separately parses the raw solver receipt, recomputes the parent comparison, and rejects status, metric, and hash mutations.

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

• Cube-and-conquer lookahead -> predict that the best short-pilot unit cube remains easier at proof scale -> the 51.091 percent decision reduction at 2000 conflicts reversed to a 17.480 percent increase at 25000 conflicts.

• The recorded orbit-27 CNF is exactly the audited parent CNF plus positive primary unit 505.
  Complete ordered-clause comparison in artifacts/skeleton-326-orbit27-exact-cube-20260810/independent-check.json. · CNF SHA-256 080610491ce6b8a91749596c3b904e10c5c9ad64d19a230d2642822f26dad7fd. · computed
• CaDiCaL did not decide the recorded cube under seed 0 and the nominal 25000-conflict protocol.
  Raw receipt and independent result check. · The exact formula, solver version, seed, and recorded limits only. · computed
• At the matched 25000-conflict cap, orbit 27 used 17.479775466402514 percent more decisions than the parent leaf.
  56926 orbit-27 decisions versus 48456 parent decisions, independently reconstructed. · CaDiCaL 1.7.3 seed 0 on the two recorded CNFs. · computed

• Scale the identical orbit-27 forward-totalizer CNF solely by increasing its conflict cutoff.
  CaDiCaL 1.7.3 seed 0 and cube SHA-256 080610491ce6b8a91749596c3b904e10c5c9ad64d19a230d2642822f26dad7fd. · The predeclared 25000-conflict run returned LIMIT and its short-pilot advantage reversed. · artifacts/skeleton-326-orbit27-exact-cube-20260810/result-independent-check.json · A materially different proof-capable encoding/solver or a verified deeper complete cube decomposition with a new matched reduction signal.
• Use short-pilot decision ranking alone as evidence that a cube will scale better.
  The current exact-leaf encoding and orbit-27 comparison. · The decision delta changed from -51.091 percent at 2000 conflicts to +17.480 percent at 25000 conflicts. · Parent and orbit-27 result packets. · A validated ranking statistic that remains predictive over multiple matched caps or instances.
• Repeat the complete fixed-pair-link relaxation.
  All 754 type-4 signature/e_45 targets. · All targets already survived independent replay. · artifacts/type4-complete-pair-link-gate-20260809/independent-check.json · A genuinely new labelled correlation.

• Sequential-counter alternative for the orbit-27 pair caps.
  It preserves exact semantics and proof logging while materially changing propagation geometry. · Compile and independently reconstruct the formula, then run a matched 2000-conflict pilot. · high · open
• Deeper stabilizer-preserving cubes.
  Additional selected blocks may expose pair-cap saturation, but the current unit-cube reversal makes this lower expected value. · Count third-block orbits and stop before CNF generation if the complete quotient or proof-prefix cost is excessive. · low · open
• Materially new coverage-aware constructive moves.
  A valid 54-cover would settle the target directly, but prior 2-for-2, strict 3-for-3, and ejection-chain protocols did not beat defect 10. · Specify a new move invariant and require an independently checked defect below 10 before scaling. · normal · open

Objective: Determine whether a different cardinality encoding supplies stable propagation on the exact orbit-27 semantics.

First action: Create protocols/skeleton-326-orbit27-sequential-counter-v1.json, implement scripts/skeleton_326_orbit27_sequential_counter_v1.py and an independent checker, then run the generated CNF with `/usr/bin/cadical --seed=0 -c 2000 FORMULA.cnf PILOT.drat`.

Stop condition: Redirect on checker disagreement, unresolved status with less than 20 percent decision reduction, or any SAT/UNSAT result lacking its full verification contract.

• Do not increase the conflict cap or run the other 30 cubes under the unchanged encoding.
• Implement and independently reconstruct a sequential-counter alternative for the same exact orbit-27 semantics.
• Run a matched 2000-conflict pilot and continue only on SAT, certificate-ready UNSAT, or at least 20 percent fewer decisions.
• Preserve constructive routes only when they introduce materially new coverage-aware move geometry and beat the verified defect-10 seed.

• 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/2607.23766 ↗
• https://arxiv.org/abs/math/9502238 ↗

GPT-5.6 Sol served as principal investigator, audited the route, implemented the formula and result checkers, ran the bounded discriminator, and interpreted it. GPT-5.6 Terra delegates supplied advisory prior-art and experiment-verification memos; their advice was promoted with provenance and was not counted as independent validation. Deterministic Python 3.12.3, CaDiCaL 1.7.3, SHA-256, and the computational-researcher experiment harness were used. No CAS, proof assistant, lab job, newly spawned subagent, system installation, external write, or publication occurred.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1136.2s

Review state

not a result claim

Attempt ID

covering-c1553-20260810-180212-990f21

No human review recorded.