Partitioned the complete canonical type-4 multiplicity-five-pair CNF by four audited primary block literals into 16 exact leaves and ran each with proof emission under a fixed 2000-conflict cap.

certificate-first semantic cube decomposition

Four semantic primary literals generate a disjoint exhaustive truth-table partition; bounded CDCL seeks a directly checked SAT model or replayable UNSAT proof in each leaf.

Hypothesis: At least one leaf of a complete four-literal semantic partition of the canonical type-4 branch is decided within 2000 CaDiCaL conflicts and is independently checkable.

Test: Materialize all 16 base-plus-four-unit CNFs, run CaDiCaL 1.7.3 with seed 1553 and a 2000-conflict cap on each, directly check any SAT model, and require DRAT-to-LRAT replay for any UNSAT result.

Producer/checker agreement establishes only the partition and exact bounded telemetry. UNKNOWN partial DRAT streams exclude nothing, and the predeclared gate required a checked SAT model or replayed UNSAT proof. Therefore the result is no_progress and redirects the route.

• The four selected primary variables partition the canonical type-4 CNF into exactly 16 disjoint exhaustive leaves.
• Under CaDiCaL 1.7.3 seed 1553 with a 2000-conflict cap per leaf, all 16 leaves returned UNKNOWN.
• No 54-cover or type-4 branch exclusion was produced.

• python3 scripts/type4_semantic_16cube_pilot_v1.py under experiment 20260811-004335-6f41eb produced counts SAT=0, UNSAT=0, UNKNOWN=16
• python3 checkers/check_type4_semantic_16cube_pilot_v1.py under experiment 20260811-004607-fe15ab accepted all 16 leaves
• python3 scripts/test_type4_semantic_16cube_mutations_v1.py under experiment 20260811-004636-99f96b rejected four corruptions
• sha256sum -c artifacts/type4-semantic-16-cube-pilot-20260811/manifest.sha256 passed

• .proof-experiments/20260811-004335-6f41eb: 16 solver leaves, all UNKNOWN, 32024 conflicts total
• .proof-experiments/20260811-004607-fe15ab: independent reconstruction accepted
• .proof-experiments/20260811-004636-99f96b: four mutations rejected

checkers/check_type4_semantic_16cube_pilot_v1.py independently rebuilds the free-block order, parses all 594090 base clauses and 16 leaves without importing the producer, proves complete disjoint cube coverage, and would directly check a SAT cover or require proof replay for UNSAT. No decisive model or proof existed to validate.

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

• C(12,6,4) certificate-first orbit decomposition -> require exact leaf coverage and per-leaf replay before scale-up -> leaf coverage checked, but all 16 bounded leaves remained UNKNOWN

• Variables 67, 278, 832, and 976 generate an exact 16-leaf partition of the hash-bound canonical type-4 CNF.
  independent-check.json accepted after parsing the base and every leaf · CNF SHA-256 2146afbf93b8d914d4faf42e9c08a2bdcdebe4dc9e10bd358f98b8fde596754f · computed
• All 16 leaves return UNKNOWN under the exact seed-1553 2000-conflict CaDiCaL 1.7.3 protocol.
  result.json, 16 solver logs, independent status reconstruction, and manifest replay · Protocol type4-semantic-16-cube-pilot-v1 only · computed

• Scale the same four-literal type-4 cube partition solely by increasing its conflict cap or changing the seed.
  The exact four semantic literals and balanced-totalizer CNF under protocol v1. · Every leaf remained UNKNOWN and propagation per conflict was about twice the prior monolithic calibration; there was no proof signal or efficiency gain. · artifacts/type4-semantic-16-cube-pilot-20260811/result.json and artifacts/pair5-normalization-pilot-20260809/result.json · A materially new cube-selection or encoding mechanism with an independently checked pilot producing a replayed leaf or measured search improvement.

• Proof-core-weighted exact-degree constructive repair from the defect-10 seed.
  It is a direct positive route and materially changes the failed coverage-blind ejection geometry by penalizing destruction of proof-core and singleton-covered triples. · Run 256 matched proof-core-weighted and singleton-loss-only closures; independently replay all proposals and require best defect below 10. · high · open
• Type-4 pair-excess skeleton-link interface census.
  It adds literal skeleton/link coupling absent from link-only clauses, with only 8281 raw endpoint headers before stabilizer canonicalization. · First independently derive the residual-capacity identities and exact lift map; stop if every canonical interface survives or lifting is incomplete. · normal · open

Objective: Test whether proof-core-aware constructive geometry can beat the verified defect-10 barrier at minimal cost.

First action: Create a protocol for 256 matched closures from the hash-bound defect-10 seed, one arm weighting proof-core and singleton-covered triples and one singleton-only control, with direct independent replay.

Stop condition: Promote only on a directly checked defect below 10, with defect zero checked against all 455 triples; otherwise hold this constructive mechanism and redirect.

• Do not increase the cap or change only the four literals for protocol v1.
• Predeclare a 256-proposal matched constructive pilot comparing proof-core-weighted and singleton-loss-only degree-preserving closure from the defect-10 seed.
• Require independent replay and a verified defect below 10; otherwise hold constructive repair and return to a materially new complete proof partition.

• 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 ↗

GPT-5.6 Sol principal selected, designed, implemented, ran, audited, and interpreted the epoch. GPT-5.6 Terra delegates supplied bounded advisory reconnaissance only; their recommendation was promoted with provenance and model agreement was not validation. Python 3.12.3 generated and independently parsed CNFs; CaDiCaL 1.7.3 ran 16 bounded proof-emitting leaves; SHA-256 and the computational-researcher harness bound artifacts. Pinned drat-trim/lrat-check were available but not invoked because no leaf reached UNSAT. Web search checked current status and adjacent primary work. No sub-agent, lab job, CAS, proof assistant, package installation, system change, external write, publication, or Git operation was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1445.1s

Review state

not a result claim

Attempt ID

covering-c1553-20260811-005706-446845

No human review recorded.