Re-encode the exact orbit-27 rooted [3,2^6] cube using rectangular Sinz sequential counters for all 105 pair caps, independently reconstruct the formula, and compare it with the audited totalizer encoding under a fresh matched 2000-conflict CaDiCaL pilot.

exact-leaf SAT cardinality re-encoding

Hold the 3002 primary block variables, 445 coverage clauses, 105 pair-cap incidence lists, fixed root, and orbit-27 cube unit constant while changing only the at-most-k auxiliary encoding; measure propagation behavior at a fixed conflict budget.

Hypothesis: The sequential encoding either decides the exact orbit-27 cube or reaches 2000 conflicts with at least 20 percent fewer decisions than a fresh totalizer control and no increase in propagations per decision.

Test: Run CaDiCaL 1.7.3 with seed 0 and nominal conflict cap 2000 on both independently checked, hash-bound encodings.

A LIMIT run excludes no assignment, partial DRAT output is not a certificate, and the only predeclared performance gate failed. The evidence therefore supports route closure but not mathematical progress on C(15,5,3).

• The sequential CNF has 154007 variables, 331416 clauses, and SHA-256 afcaa175902a215a9ab88a1501451fff1cbed9623cb412d2b983e963862ca3d2.
• For the exact checked cube, its primary semantics match the audited totalizer formula.
• At the matched pilot, the totalizer used 4057 decisions and 894935 propagations; the sequential encoding used 3727 decisions and 1974604 propagations.
• Neither bounded run established SAT or UNSAT.

• sha256sum -c artifacts/skeleton-326-orbit27-sequential-20260810/manifest.sha256
• python3 checkers/check_skeleton_326_orbit27_sequential_cnf_v1.py --cnf artifacts/skeleton-326-orbit27-sequential-20260810/sequential.cnf --manifest artifacts/skeleton-326-orbit27-sequential-20260810/sequential-manifest.json --totalizer-cnf artifacts/skeleton-326-orbit27-exact-cube-20260810/cube.cnf --totalizer-manifest artifacts/skeleton-326-exact-leaf-20260810/leaf-manifest.json --output /tmp/c1553-sequential-formula-check.json
• python3 checkers/check_skeleton_326_orbit27_sequential_result_v1.py --result artifacts/skeleton-326-orbit27-sequential-20260810/result.json --control-experiment .proof-experiments/20260810-183820-7485ed --challenger-experiment .proof-experiments/20260810-183828-6e9d40 --control-cnf artifacts/skeleton-326-orbit27-exact-cube-20260810/cube.cnf --challenger-cnf artifacts/skeleton-326-orbit27-sequential-20260810/sequential.cnf --output /tmp/c1553-sequential-result-check.json

• .proof-experiments/20260810-183641-e286a1: generated the 154007-variable, 331416-clause sequential CNF.
• .proof-experiments/20260810-183738-7ce6e8: independent complete clause reconstruction passed.
• .proof-experiments/20260810-183753-ca8dcb: 3076 small semantic cases passed and five encoding mutations were rejected.
• .proof-experiments/20260810-183820-7485ed: totalizer control returned LIMIT with 4057 decisions and 894935 propagations.
• .proof-experiments/20260810-183828-6e9d40: sequential challenger returned LIMIT with 3727 decisions and 1974604 propagations.
• .proof-experiments/20260810-184037-573dfe: independent result parser reproduced the telemetry and rejected four result mutations.

checkers/check_skeleton_326_orbit27_sequential_cnf_v1.py independently rebuilds the full formula using bit masks and one-based prefix/threshold variables; checkers/check_skeleton_326_orbit27_sequential_result_v1.py independently parses both raw solver receipts and recomputes the failed gates.

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

• General SAT cardinality encoding practice -> sequential counters might improve propagation on small pair caps -> the exact matched pilot showed only 8.13 percent fewer decisions and 2.40 times worse propagations per decision, falsifying the transfer for this formula/solver protocol.

• The recorded sequential CNF is an independently reconstructed encoding of the same primary orbit-27 semantics as the audited totalizer cube.
  artifacts/skeleton-326-orbit27-sequential-20260810/independent-check.json · The fixed root, orbit-27 unit, 445 coverage rows, and 105 pair caps only. · computed
• The sequential encoding failed the predeclared matched advancement gate.
  artifacts/skeleton-326-orbit27-sequential-20260810/result-independent-check.json · CaDiCaL 1.7.3, seed 0, nominal conflict cap 2000, exact recorded formulas and machine. · computed

• Scale the rectangular sequential-counter orbit-27 formula without a new discriminator.
  The hash-bound 154007-variable formula under the tested CaDiCaL protocol. · Both formulas returned LIMIT, decision reduction was below 20 percent, and propagations per decision worsened by a factor of 2.401785. · artifacts/skeleton-326-orbit27-sequential-20260810/result-independent-check.json · A materially different encoding or solver with an independently checked pilot, or a complete cube/proof decomposition.

• Joint type-4 common-family and pair-excess-skeleton orbit census.
  It couples two globally necessary structures and can reject an impractically large SAT branching scheme before formula generation. · Enumerate the naive 395*41 type product under exact joint stabilizers and independently reproduce the orbit count. · high · open
• All-partition ten-zero root projection census.
  The existing 2145-root compression makes a global necessary-relaxation classification computationally feasible, although previous partitions suggest limited decisiveness. · Pilot the smallest non-[15] partition with the existing independent integer checker. · normal · open
• Constructive exact-degree repair beyond the previously exhausted local neighborhoods.
  A 54-cover witness would settle the problem directly, but prior 2-for-2, 3-for-3, ejection-chain, and radius-four searches did not improve defect 10. · Design a genuinely new exact-degree neighborhood and measure it on the verified defect-10 seed before any scale-up. · low · open

Objective: Determine whether joint common-family/pair-skeleton canonicalization materially shrinks the next globally relevant structural frontier.

First action: Create protocols/type4-pair-skeleton-joint-orbits-v1.json with the exact 16195-object universe and a predeclared compression threshold, then implement producer and independent Burnside/canonicalization checker.

Stop condition: Stop or redirect if the independently checked joint count exceeds the predeclared material threshold or the producer and checker disagree.

• Predeclare a material compression threshold for the naive 395 by 41 common-family/pair-skeleton type product.
• Enumerate exact joint stabilizer orbits before generating any additional SAT leaves.
• Independently validate the orbit census using a second canonicalization or Burnside implementation.
• Redirect immediately if the joint census does not materially compress 16195 types or the two orbit maps disagree.

• 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://doi.org/10.1007/11564751_73 ↗
• https://www.carstensinz.de/papers/CP-2005.pdf ↗
• https://arxiv.org/abs/2607.23766 ↗

GPT-5.6 Sol principal performed experiment design, implementation, execution, audit, and synthesis. GPT-5.6 Terra challenger-prior-art and experiment-verification delegates supplied advisory memos that were promoted under sources/advisory and were not treated as independent validation. Deterministic Python 3.12.3, CaDiCaL 1.7.3, SHA-256, standard-library checkers, the computational-researcher experiment harness, and web searches of the maintained repository and primary encoding literature were used. No CAS, proof assistant, new subagent, lab job, external write, publication, or model-agreement validation was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1142.9s

Review state

not a result claim

Attempt ID

covering-c1553-20260810-184715-1fb124

No human review recorded.