Tested the local pair-surplus cylinder H=3K5 with fixed first block 012345, then replaced 105 duplicated exact-pair counters by inherited unary threshold units and ran proof-producing and no-proof CaDiCaL discriminators.

inherited-threshold exact-pair incidence SAT

Reuse exact unary pair-multiplicity thresholds already present in the pinned incidence CNF: target 4 adds not-ge5, while target 5 adds ge5 and not-ge6.

Hypothesis: The H=3K5, fixed-(5,1,0)-block cylinder reaches a checked SAT cover or replayable UNSAT proof within 60 solver seconds and 18841117 combined proof bytes.

Test: Run CaDiCaL 1.7.3 seed 0 with -P0 on the exact cylinder, first with proof emission and then without proof I/O, accepting only a directly checked cover or fully replayed DRAT-to-LRAT certificate.

The encoding reduction is exact and independently reproducible, so it is durable progress. The absence of a complete proof or witness prevents any local UNSAT claim or global covering-number conclusion.

• The inherited-threshold H=3K5 formula has 33178 variables, 156603 clauses, and SHA-256 e9b47327b139f367fa27285e53bb809a63cbf774170c8a25cc7d8e0dc78a3e05.
• It uses exactly 75 not-ge5 units for cross pairs and 30 ge5/not-ge6 unit pairs for within-clique pairs, totaling 135 units.
• The formula retains all 455 triple-coverage clauses and all 3150 exact pair-support equivalences.
• The proof-producing run hit 18841117 DRAT bytes without SAT or UNSAT.
• The no-proof run remained UNKNOWN after 60 seconds, 272244 conflicts, 681156 decisions, and 237603133 propagations.
• The maintained global range remains 30 <= C(15,6,3) <= 31.

• python3 scripts/pair_surplus_3k5_threshold_reuse_v1.py --out-dir artifacts/epoch95-20260811/pair-surplus-3k5-threshold-reuse-v1
• python3 checkers/check_pair_surplus_3k5_threshold_reuse_v1.py --artifact-dir artifacts/epoch95-20260811/pair-surplus-3k5-threshold-reuse-v1 --out artifacts/epoch95-20260811/pair-surplus-3k5-threshold-reuse-independent-check-v1.json
• /usr/bin/cadical --seed=0 -P0 -t 60 on the identical reduced CNF returned UNKNOWN
• python3 checkers/check_pair_surplus_3k5_noproof_v1.py independently parsed and hash-bound the no-proof control
• sha256sum -c artifacts/epoch95-20260811/SHA256SUMS returned OK for all bound artifacts

• .proof-experiments/20260811-192236-56c528: duplicated-counter proof run reproduced UNKNOWN_PROOF_CAP with formula 5ba03d... and DRAT prefix 7875ad....
• .proof-experiments/20260811-192303-c83151: independent duplicated-counter reconstruction passed.
• .proof-experiments/20260811-192353-a27f71: four fail-closed controls passed.
• .proof-experiments/20260811-192610-e11322: inherited-threshold proof run hit the same cap with 33178 variables and 156603 clauses.
• .proof-experiments/20260811-192725-1e45a0: independent inherited-threshold reconstruction passed.
• .proof-experiments/20260811-192800-f80bd5: 60-second no-proof run returned UNKNOWN after 272244 conflicts.
• .proof-experiments/20260811-192937-90999f: independent no-proof parser confirmed UNKNOWN and exact statistics.

checkers/check_pair_surplus_3k5_threshold_reuse_v1.py reconstructed the complete reduced CNF byte-for-byte using the separately written inherited-threshold oracle; checkers/check_pair_surplus_3k5_noproof_v1.py independently parsed the no-proof status and statistics.

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

• Exact totalizer outputs -> prediction that H pair equations require only units rather than new counters -> observed exact savings of 9975 variables and 47220 clauses.
• C(12,6,4) proof-replay discipline -> prediction that a proof-budget failure must remain nonterminal and mutation-sensitive -> capped prefixes were explicitly retained as UNKNOWN, never promoted.

• The reduced H=3K5 cylinder formula is exactly representable by the pinned base CNF plus 135 inherited-threshold units.
  Byte-identical independent reconstruction, SHA-256 e9b47327b139f367fa27285e53bb809a63cbf774170c8a25cc7d8e0dc78a3e05 · Pinned base incidence formula and the named local cylinder · computed
• Aut(3K5)=S5 wr S3 has order 10368000 and the (5,1,0) block type has orbit size 30.
  Explicit permutation and orbit calculation in independent checkers · The labelled three-clique multigraph · proved
• The no-proof seed-0 -P0 control did not terminate within 60 seconds.
  Independent receipt dc3df3d912673071de29ecb8296033c88f6fcb06cad6b40772619b2da07ce8fe · CaDiCaL 1.7.3 on formula e9b47327... · computed

• Repeat the exact H=3K5, fixed-012345 cylinder with CaDiCaL 1.7.3 seed 0 -P0 under the same flat limits.
  This solver, seed, preprocessing mode, 60-second cap, and 18841117-byte proof budget only · Both proof encodings exhausted the proof cap and the reduced no-proof run remained UNKNOWN. · Epoch receipt and independently parsed solver records · A materially different solver, proved subcube decomposition or proof-prefix transport, or measured certificate compression
• Use fresh exact-pair counters on this base formula.
  Exact pair targets already exposed by the retained totalizer outputs · Fresh counters add 9975 variables and 47220 clauses without changing semantics. · Matched byte-reconstructed formulas · Evidence that a deliberately redundant counter representation produces a terminal result under a smaller total validation cost

• Inherited thresholds in a different owned H or root-link cube
  The exact-pair mechanism is independently validated and removes substantial auxiliary overhead. · Compile one owned cube and run a five-second matched gate before proof emission. · high · open
• Constructive alternative-solver scan
  A SAT witness is globally decisive and avoids exhaustive ownership and proof storage. · Audit the pinned Minisat build and run one short model-producing comparison on the reduced CNF or a different H. · normal · open
• Canonical pair-surplus ownership
  A global exclusion requires a disjoint, independently checked catalogue rather than isolated local H cylinders. · Measure canonical loopless 4-regular multigraph enumeration and ownership on a tiny prefix before any solve. · normal · open

Objective: Transfer inherited pair thresholds to the easiest materially different route without repeating the closed 3K5 configuration.

First action: Read artifacts/epoch95-20260811/continuation-checkpoint.json and compile one previously untested owned cube with inherited thresholds for a five-second gate.

Stop condition: Stop on unproved ownership, reconstruction mismatch, no material five-second improvement, or another nonterminal forecast.

• Do not repeat the exact H=3K5 seed-0 -P0 configuration without a material reopening delta.
• Reuse inherited thresholds in one previously untested owned H or root-link cube.
• Run a five-second preprocessing and throughput gate before proof emission.
• Give constructive search equal priority because any valid model is globally decisive.
• Require a disjoint canonical ownership manifest before scaling an exclusion route.

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

GPT-5.6 Sol acted as principal investigator. GPT-5.6 Terra delegates supplied advisory prior-art and experiment-verification memos that were independently audited by Sol. Deterministic work used Python 3.12.3, CaDiCaL 1.7.3, GNU gcc, existing drat-trim/lrat-check and CakeLPR sources, SHA-256, the computational-researcher experiment harness, and web searches of the maintained Covering Repository, LJCR, and arXiv. No complete DRAT/LRAT proof, CAS, proof assistant, cloud lab, external proof service, or human validator produced a terminal result.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1493.0s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1563-20260811-193637-00e64a

No human review recorded.