Independently enumerate and search the 54-block covers invariant under (0 1 2 3 4 5)(6 7 8 9 10 11)(12 13 14), then replace redundant weighted constraints with a semantics-equivalent normalized cardinality encoding.

C6-invariant constructive SAT search

Restrict block selection to complete orbits of a fixed order-6 action, impose one coverage clause per triple orbit, and test the resulting exact weighted-cardinality system with proof-producing SAT.

Hypothesis: A 54-block C(15,5,3) cover invariant under the fixed cycle-type 6+6+3 action is found or excluded within 25,000 CaDiCaL conflicts.

Test: Run the independently checked compact orbit CNF with CaDiCaL 1.7.3, seed 1553, and a 25,000-conflict cap; accept only a directly checked expanded model or a replayable complete UNSAT proof.

The orbit counts, restriction size, coefficient equivalence, generated coverage clauses, and performance measurements are deterministic and independently checked. UNKNOWN solver exits cannot exclude any assignment, so the evidence supports only a reusable local classification and encoding improvement.

• The fixed action partitions the 3003 blocks into 17 size-3 and 492 size-6 orbits.
• It partitions the 455 triples into 81 orbits with histogram one size-1, two size-2, six size-3, and 72 size-6 orbits.
• The fixed invariant family contains exactly 18,660,994,077,537,423,080 candidate 54-block orbit selections before coverage filtering.
• The compact formula represents the same fixed-action covers as the redundant formula.
• At the matched conflict cap, the compact formula used 47,115 clauses, 63,604 decisions, 12,958,755 propagations, 2.79 process seconds, and 17.00 MB maximum RSS.
• Neither solver run found a cover or proved the fixed family empty.

• python3 scripts/c6_symmetric_cover_compact_v1.py --output artifacts/c6-symmetric-cover-20260810/compact.cnf --manifest artifacts/c6-symmetric-cover-20260810/compact-manifest.json
• python3 checkers/check_c6_symmetric_cover_v1.py --manifest artifacts/c6-symmetric-cover-20260810/compact-manifest.json --cnf artifacts/c6-symmetric-cover-20260810/compact.cnf --output artifacts/c6-symmetric-cover-20260810/compact-independent-check.json
• /usr/bin/cadical --seed=1553 -c 25000 artifacts/c6-symmetric-cover-20260810/compact.cnf artifacts/c6-symmetric-cover-20260810/compact-proof.drat
• python3 checkers/test_c6_symmetric_mutations_v1.py --checker checkers/check_c6_symmetric_cover_v1.py --manifest artifacts/c6-symmetric-cover-20260810/compact-manifest.json --cnf artifacts/c6-symmetric-cover-20260810/compact.cnf --output artifacts/c6-symmetric-cover-20260810/mutation-controls.json
• sha256sum -c artifacts/c6-symmetric-cover-20260810/manifest.sha256

• .proof-experiments/20260810-211309-c60878: generated the 54,426-variable, 590,703-clause redundant C6 formula
• .proof-experiments/20260810-211316-e3b5a1: independently checked the initial orbit formula
• .proof-experiments/20260810-211328-adbdff: redundant formula UNKNOWN at 25,006 conflicts
• .proof-experiments/20260810-211530-bf0ad0: generated the 5,687-variable, 47,115-clause compact formula
• .proof-experiments/20260810-211700-c9460b: final independent compact-formula check passed
• .proof-experiments/20260810-211548-bf4d7a: compact formula UNKNOWN at 25,004 conflicts
• .proof-experiments/20260810-211708-320085: all five targeted mutations were rejected
• .proof-experiments/20260810-212151-a3b3d2: generated the final hash-bound summary

checkers/check_c6_symmetric_cover_v1.py independently traverses the permutation action over the full labelled point, pair, triple, and block universes, verifies hashes and all coverage-prefix clauses, and can directly check an expanded 54-block witness. It does not certify UNSAT or fully reconstruct every totalizer clause, which is acceptable here because both SAT runs were UNKNOWN.

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

• Semiregular C3 symmetry -> predict that a higher-order action reduces primary variables -> C6 reduced block orbits from 1001 to 509, but the initial weighted encoding was slower because auxiliary propagation dominated.
• Integer coefficient normalization -> predict a smaller exact-cardinality network -> dividing orbit weights by three reduced the formula from 590,703 to 47,115 clauses and process time from 25.53 to 2.79 seconds.
• Classical cyclic-cover search -> predict that a nonconjugate small symmetry family is a cheap constructive discriminator -> the family was much smaller but remained undecided at the bounded cap.

• The fixed order-6 action has block-orbit histogram 3^17 6^492 and triple-orbit histogram 1^1 2^2 3^6 6^72.
  Producer and independent full-universe checker agree; compact-independent-check.json valid=true. · The action (0 1 2 3 4 5)(6 7 8 9 10 11)(12 13 14) on subsets of the 15-point set · computed
• For this action, the normalized equation sum (|O|/3)x_O=18 is equivalent to selecting exactly 54 expanded blocks.
  Every block orbit has size 3 or 6, so division by three is exact; the independent checker verifies the orbit histogram and target. · Fixed C6-invariant block families · proved
• The compact encoding reduced matched-cap propagations by 83.6219% and process time by 89.0717% relative to the redundant C6 encoding.
  Hash-bound CaDiCaL logs c800b3ce... and 41c7d3ad..., parsed by result.json. · CaDiCaL 1.7.3, seed 1553, 25,000-conflict protocol on the two recorded formulas · computed

• Repeat the complete fixed-pair-link necessary relaxation without new literal information.
  All 395 frozen type-4 signatures and 754 signature/e45 targets in the complete labelled {4,5} link relaxation · Every target already has an independently checked positive necessary-relaxation witness. · artifacts/type4-complete-pair-link-gate-20260809/result.json and independent-check.json · Add genuinely new labelled constraints beyond the already complete pair link.
• Scale the redundant C6 degree-and-pair totalizer encoding.
  The fixed C6 family under the recorded CaDiCaL protocol · It remained UNKNOWN and was dominated by the semantics-equivalent compact formula in variables, clauses, decisions, propagations, time, and memory. · artifacts/c6-symmetric-cover-20260810/result.json · A different proof system or encoding demonstrates a measured advantage over compact.cnf.

• Normalizer lex-leader for the fixed C6 orbit variables
  The compact formula is now cheap, and residual symmetry is the clearest remaining local bottleneck. · Enumerate the action normalizer, independently verify its induced permutations on all 509 block orbits, add one sound lex-leader, and run the matched 25,000-conflict comparison. · high · open
• Proof-replayable cube partition of the compact C6 formula
  A complete partition could turn local-family UNSAT into a segmented, independently replayable classification. · Only after the normalizer test, generate a small deterministic cube sample and measure solved-leaf rate and proof bytes per conflict. · normal · open
• Return to a globally complete pair-5 branch using genuinely new literal information
  The pair-5 normalization covers every hypothetical global 54-cover, unlike the C6 family. · Use the saved root-orbit-107 literal outside-subset realization profile if the local C6 normalizer test fails. · normal · open

Objective: Determine whether residual normalizer symmetry materially advances the compact fixed-C6 family.

First action: Enumerate the normalizer of the fixed permutation and its induced action on the 509 block orbits, then independently verify every induced orbit permutation before emitting clauses.

Stop condition: Stop and redirect if the matched run remains UNKNOWN and fails to improve both decisions and process time by at least 20%; stop successfully on a directly checked 54-cover or independently replayed family UNSAT.

• Compute the normalizer of the fixed C6 action on the 509 block orbits and derive one independently checkable lex-leader.
• Run a matched 25,000-conflict comparison against compact.cnf.
• Stop the C6 route if the comparison neither decides the family nor improves decisions and time by at least 20%.
• If the family reaches UNSAT, regenerate the exact CNF independently and replay a complete LRAT proof before claiming the local exclusion.
• If SAT, expand the selected orbits and directly check all 455 labelled triples.

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

GPT-5.6 Sol acted as principal investigator, selected and independently implemented the experiment, audited the evidence, and interpreted the results. GPT-5.6 Terra delegates supplied advisory reconnaissance identifying the C6 route and warning that the fixed-pair rerun was stale; their agreement was not treated as validation, and the relied-on lead was promoted with provenance. Python 3.12.3 generated and checked artifacts; CaDiCaL 1.7.3 performed the bounded proof-producing SAT runs; SHA-256 and the computational-researcher experiment harness recorded the receipt. Web search checked current sources. No new subagents, CAS, proof assistant, cloud-lab job, external write, publication, or proof replay was used; proof replay was inapplicable because both solver exits were UNKNOWN.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1300.0s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1553-20260810-212512-5bfe6b

No human review recorded.