Replace the one-hot counters in the complete strict 5-for-5, defect-at-most-nine local CNF with Wallace binary sums and a truncated defect totalizer, then run a matched three-seed solver pilot.

hybrid binary-cardinality SAT encoding

Carry-save binary sums enforce exact selections and point-degree balance; a truncated equivalence totalizer enforces at most nine uncovered triples.

Hypothesis: The hybrid encoding either decides the complete strict five-for-five neighborhood or reduces decisions by at least 20 percent for seeds 0,1,2 without increasing propagations per decision.

Test: Independently reconstruct the CNF, test the exact defect boundary, then compare the audited control and challenger at 5,000 conflicts for three seeds.

Independent reconstruction and boundary proofs validate the artifact, while six UNKNOWN statuses and a 4.058114 decision ratio prohibit any local exclusion, global inference, or scale-up under the declared protocol.

• The recorded hybrid CNF has 41,112 variables, 298,184 clauses, and SHA-256 e0c2d3d5e11f4bf1258b5645654b423870bf926791d8f73e556964c756604fd7.
• A separate checker reconstructed all 298,184 clauses and rejected three mutations.
• For each recorded seed, the control used 85,986 decisions and 19,451,871 propagations; the challenger used 348,941 decisions and 807,982 propagations.
• A pinned degree-balanced defect-10 fixture is LRAT-certified UNSAT under the at-most-nine formula and SAT after deleting only the boundary unit.
• No 54-cover or UNSAT certificate for the complete local neighborhood was obtained.

• python3 scripts/degree18_strict5_hybrid_cnf_v1.py --protocol protocols/degree18-strict5-hybrid-v1.json ... generated the hash-bound formula.
• check_degree18_strict5_hybrid_cnf_v1.py reconstructed 298,184 clauses with valid=true.
• run_degree18_strict5_hybrid_pilot_v1.py produced six UNKNOWN records and decision=redirect.
• check_degree18_strict5_hybrid_result_v1.py reparsed the logs and recomputed telemetry_gate=false.
• boundary-strict.lrat replayed successfully; the same proof was rejected on the relaxed formula.
• check_degree18_strict5_hybrid_regeneration_v1.py reproduced the CNF and manifest byte-for-byte.
• sha256sum -c artifacts/degree18-strict5-hybrid-20260811/manifest.sha256 passed.

• .proof-experiments/20260811-120148-b35946: generated the 41,112-variable, 298,184-clause challenger.
• .proof-experiments/20260811-120208-cd1580: independently reconstructed every clause and rejected three mutations.
• .proof-experiments/20260811-120443-e570dd: six matched runs were UNKNOWN; decision gate failed; LRAT smoke passed.
• .proof-experiments/20260811-120525-02a9f8: raw logs and ratios independently rechecked.
• .proof-experiments/20260811-120721-642944: strict defect-10 pinning was UNSAT and relaxed pinning SAT.
• .proof-experiments/20260811-120734-5c8b2b: boundary pins, fixture, and LRAT independently checked.
• .proof-experiments/20260811-121304-0c3d95: CNF and manifest regenerated byte-identically.

The formula checker rebuilds block incidence using integer masks and a separately named adder scheduler, then matches every clause. A second checker reparses raw solver logs and replays LRAT; a third reconstructs all boundary pins and directly checks the defect-10 fixture.

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

• Wallace arithmetic -> predicted cheaper exact point-balance propagation -> observed 95.85 percent fewer propagations but 4.058 times more decisions.
• Unary threshold encoding -> predicted robust off-by-one propagation -> observed LRAT-certified rejection at defect 10 and SAT after deleting only the threshold unit.

• The hybrid formula contains exactly 41,112 variables and 298,184 clauses.
  Producer manifest, complete independent reconstruction, and byte-identical regeneration. · The hash-bound local formula only. · computed
• The hybrid decision ratio against control is 4.058114111599563 at the fixed cap.
  Six raw solver logs and independent ratio recomputation. · CaDiCaL 1.7.3, seeds 0,1,2 and 5,000 conflicts. · computed
• The at-most-nine unit rejects the recorded pinned defect-10 fixture.
  Replayed LRAT proof and relaxed-formula SAT control. · One pinned strict five-for-five degree-balanced fixture. · computed

• Rerun the injected complete fixed-pair-link strengthening.
  All 5,460 labelled pair-link requirements over the four canonical baselines. · Every requirement is either a fixed-block tautology or exactly an existing triple-coverage clause, giving zero logical delta. · artifacts/pair-link-cnf-delta-audit-20260811/independent-check.json · Add separately justified exact pair-count, skeleton, or other information absent from baseline coverage.
• Scale the exact strict5 hybrid solely by increasing solver cutoffs.
  CNF SHA-256 e0c2d3d5e11f4bf1258b5645654b423870bf926791d8f73e556964c756604fd7 under CaDiCaL 1.7.3. · Every run was UNKNOWN and challenger decisions increased by 4.058114 times, failing the declared gate. · artifacts/degree18-strict5-hybrid-20260811/result-independent-check.json · A material decomposition or propagation change passing a fresh matched gate, or a checked SAT/UNSAT result.
• Treat the Terra header-free 41-case pair-excess proposal as a new mechanism.
  The proposed exact-pair SAT/PB formulation. · The workspace already contains exact_pair_seed_cnf_v1.py and the stronger coverage-plus-pair direct_pb_leaf_v1.py experiments. · Existing main-workspace source and experiment artifacts. · A mechanism-level delta beyond retaining exact pair cardinalities without materialized headers.

• Meet-in-the-middle strict5 incidence-profile census.
  It replaces weak global SAT branching with exact bulk grouping and can be killed by a size-only pilot. · Count two-block addition profiles and compatible residual profiles after forcing one added block to cover an original missing triple. · high · open
• Genuinely new constructive move family.
  A directly checked 54-cover remains terminal, but prior 2-for-2, 3-for-3, 4-for-4, strict5, and ejection-chain neighborhoods stalled at defect 10. · Define a move not expressible by the closed neighborhoods and require a below-10 pilot. · normal · open
• Owner-approved radius-five certificate stratum.
  The existing map is hash-bound and proof-replay capable but cannot be dispatched without exact human scope approval. · After approval of map SHA-256 7fcfd2d9b429c02d3c968921155f1384343ba5bde865d7f0d9c59aab0f59a403, freeze one 256-cell stratum. · normal · open

Objective: Determine whether meet-in-the-middle incidence profiles can turn the complete strict5 neighborhood into a bounded, certifiable classification.

First action: Enumerate and count degree-vector profiles for two added blocks, restricted through at least one block covering an original missing triple, without generating full five-block candidates.

Stop condition: Stop if projected profile storage exceeds a segmented certificate budget, independent counts disagree, or no class-level elimination is possible.

• Do not rerun the exact hybrid formula at a larger cutoff.
• Build a size-only meet-in-the-middle census keyed by 15-coordinate addition-degree vectors.
• Require one added block to cover an original missing triple, which is necessary for any defect-at-most-nine neighbor.
• Measure exact profile counts and memory before generating candidates or submitting compute.
• Independently reconstruct the profile census and stop if it offers no class-level elimination.

• 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.1109/PGEC.1964.263830 ↗
• https://www.cs.upc.edu/~erodri/webpage/papers/sat09-card.pdf ↗
• https://arxiv.org/abs/2607.23766 ↗

GPT-5.6 Sol principal designed, audited, and interpreted the experiment. Two GPT-5.6 Terra delegates supplied advisory prior-art and verification memos; their agreement was not evidence, and the proposed 41-case pair route was rejected as duplicate. Deterministic Python 3.12.3 generated and checked artifacts. CaDiCaL 1.7.3 ran SAT probes. Project-scoped drat-trim and lrat-check converted and replayed proofs. The web reader returned no extractable payload. No dependencies or system packages were installed.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1521.8s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1553-20260811-121658-7fc807

No human review recorded.