Matched balanced-totalizer re-encoding of residual rows 343 and 414 at seed 0 and 25000 conflicts, with independent regeneration and DRAT-to-LRAT replay.

alternative proof-producing residual encoding

Balanced unary totalizers truncated at target+1 replace exact-count DFAs while primary semantics and the redundant exact-12 control remain fixed.

Hypothesis: The totalizer decides row 343 and independently reproduces the row-414 UNSAT control within the same seed-0 25000-conflict budget.

Test: Solve the two independently regenerated formulas at the fixed cap; require a direct or replayed decision for row 343 and replayed UNSAT for row 414.

A new mathematical exclusion required a checked decision for row 343. Independent checking instead confirmed UNKNOWN at the cap; reproducing row 414 is a control only.

• The exact totalizer formulas for rows 343 and 414 have sizes 13180/66414 and 13152/66355.
• Row 414's totalizer UNSAT proof replayed through LRAT.
• Row 343 remained UNKNOWN at the fixed cap; no mathematical conclusion follows.

• Producer experiment 20260812-191222-ed18f3: row343 UNKNOWN, row414 UNSAT.
• Independent experiment 20260812-191248-0521ce: both CNFs regenerated and row414 LRAT VERIFIED.
• Small test 20260812-191212-f05269: 196/196 exact-cardinality cases passed.
• Mutation experiment 20260812-191328-d28f3a: three corruptions rejected.
• Comparison experiment 20260812-191416-d6fefe: matched telemetry bound.

• .proof-experiments/20260812-191212-f05269: 196 exact-totalizer cases passed.
• .proof-experiments/20260812-191222-ed18f3: row343 UNKNOWN, row414 UNSAT.
• .proof-experiments/20260812-191248-0521ce: independent regeneration and proof replay.
• .proof-experiments/20260812-191328-d28f3a: three mutations rejected.
• .proof-experiments/20260812-191416-d6fefe: matched comparison passed.

check_triangle5_residual_totalizer_pilot_v1.py independently reconstructs all source semantics and both CNFs and replays UNSAT; separate small, mutation, and comparison checkers exercise different failure surfaces.

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

• Standard totalizer compilation -> predict lower CDCL proof effort on the same residual kernel -> row414 proof effort fell, but row343 remained UNKNOWN.

• The fixed totalizer encoding reproduces row-414 UNSAT with a replayed LRAT proof.
  CNF a196d9b0..., DRAT 85265e54..., LRAT 0dbecf72... · Row 414 totalizer formula only · computed
• Row 343 is not decided by the fixed totalizer protocol.
  CaDiCaL reached 25003 conflicts and returned UNKNOWN · Seed 0, 25000-conflict totalizer protocol · computed

• Scale this exact totalizer solely by raising the conflict cap.
  Rows 343/414 matched seed-0 protocol · The required discriminator remained UNKNOWN despite large structural compression; a larger arbitrary cutoff is not a contribution. · comparison.json and independent-check.json · A materially new decomposition or encoding decides row343 under a predeclared matched gate.

• Coverage-aware degree-preserving 3-for-3 pre-count from the saved defect-nine seed.
  It is constructive, materially distinct, and terminal on a cover; exact count size is the cheapest discriminator. · Implement degree-vector bucket and meet-in-the-middle pair-table counters; compare exact totals and stop above 2^22. · high · open

Objective: Measure whether the constructive defect-nine seed has a tractable coverage-aware 3-for-3 repair neighborhood.

First action: Hash-bind the saved seed and implement two independent exact candidate pre-counts before enumerating any exchange.

Stop condition: Redirect on counter disagreement, count above 2^22, or no strict defect-improving candidate; stop immediately on a directly checked 54-cover.

• Implement two independent exact 3-for-3 candidate counters around the hash-pinned defect-nine seed.
• Promote enumeration only if both counts agree and are at most 2^22.
• Do not rerun the fixed-pair link or raise the totalizer cap without a new mechanism.

• 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 was principal investigator. Two injected GPT-5.6 Terra delegates supplied advisory reconnaissance; Sol independently audited and implemented the selected discriminator, and model agreement was not validation. Python 3.12.3 generated and checked CNFs; CaDiCaL 1.7.3 solved; drat-trim and lrat-check converted and replayed proofs; SHA-256 and the computational-researcher experiment harness bound artifacts. No additional subagent, CAS, proof assistant, cloud lab, package installation, system change, or external write was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1036.6s

Review state

not a result claim

Attempt ID

covering-c1553-20260812-192015-1a5ffb

No human review recorded.