Ran one CPU-pinned, seed-1, five-second MiniSat 2.2.1 constructive search on the hash-bound inherited-threshold H=3K5 incidence CNF, followed by independent status parsing and fail-closed mutation tests.

constructive alternative-solver scan

Switch the closed H=3K5 formula from CaDiCaL to pinned MiniSat while retaining the compressed inherited-threshold encoding and requiring a directly checked model.

Hypothesis: Pinned MiniSat 2.2.1 finds a directly checkable 30-block model of the inherited-threshold H=3K5 cylinder within five CPU seconds.

Test: Run one seed-1 MiniSat process for five CPU seconds; accept only SAT followed by direct verification of 30 distinct 6-blocks, all 455 triples, degree 12 at every point, and the exact H=3K5 pair counts.

UNKNOWN supplies neither a model nor a negative certificate. The direct acceptance predicate was never reached, so the verification contract forbids any covering-number claim.

• MiniSat 2.2.1 seed 1 returned INDETERMINATE on formula e9b47327b139f367fa27285e53bb809a63cbf774170c8a25cc7d8e0dc78a3e05 after 5.04317 CPU seconds.
• The run recorded 22266 conflicts, 58866 decisions, 24590764 propagations, 78 restarts, and 29.00 MB internal memory.
• No model or independently replayable negative certificate was produced, so 30 <= C(15,6,3) <= 31 remains unchanged.

• python3 /root/proof-factory/skills/computational-researcher/scripts/run_experiment.py ... -- /usr/bin/python3 scripts/minisat_3k5_constructive_pilot_v1.py --out-dir artifacts/epoch96-20260811/minisat-3k5-constructive-pilot-v1; experiment 20260811-200506-02456e
• Independent checker experiment 20260811-200526-e33fca returned PASS with solver_status UNKNOWN.
• Mutation experiment 20260811-200533-d52f32 rejected false SAT, formula-hash drift, solver-hash drift, and protocol drift.
• sha256sum -c artifacts/epoch96-20260811/SHA256SUMS returned OK for every listed artifact.

• .proof-experiments/20260811-200506-02456e: MiniSat returned INDETERMINATE after 5.04317 CPU seconds.
• .proof-experiments/20260811-200526-e33fca: independent checker returned PASS and reproduced UNKNOWN.
• .proof-experiments/20260811-200533-d52f32: all four fail-closed mutations were rejected.

checkers/check_minisat_3k5_constructive_pilot_v1.py independently rebound formula and solver hashes, reparsed status and metrics, enforced the command protocol, and implements a separate bitmask cover checker for any future SAT result. The companion mutation checker rejected four corrupted receipts.

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

• Alternative-CDCL heuristics -> if CaDiCaL-specific branching caused the stall, MiniSat should expose a model quickly -> MiniSat also remained UNKNOWN, so solver substitution alone did not discriminate the cylinder.
• Compressed inherited counters -> avoiding fresh pair counters should preserve semantics while lowering propagation overhead -> the compressed formula ran reproducibly, but the saved representation did not produce terminal evidence.

• The exact recorded MiniSat process returned INDETERMINATE.
  Raw log SHA-256 7fd7dde59212d6d1c9d3813d5474f56ec1f033f33de9beae8d76042243c1bcfc and independent check. · Pinned MiniSat binary d880e77e..., formula e9b47327..., seed 1, five-second CPU limit. · computed
• The result file contains exactly INDET followed by a newline.
  artifacts/epoch96-20260811/minisat-3k5-constructive-pilot-v1/minisat-result.txt; SHA-256 61da80524cb60591b193041679c44097dfeb0f4a6d61e29598070022f40207eb. · This experiment only. · computed
• All four declared receipt/protocol mutations were rejected.
  fail-closed-controls.json; SHA-256 d16e18dff877926304e0dbb349784fe77bd3826b19786a1c60e78bd179377234. · False SAT, formula identity, solver identity, and CPU-limit protocol mutations. · computed

• Repeat or scale the flat MiniSat 2.2.1 seed-1 H=3K5 configuration solely by increasing its cutoff.
  The identical solver binary, formula hash, seed, and unsplit search mechanism. · The predeclared five-second discriminator was nonterminal and did not materially outperform the prior flat CaDiCaL route. · Producer receipt plus independent checker and matched epoch-95 diagnostic rates. · A new owned cylinder, proved cube decomposition, material encoding change, or independently checkable terminal-proof mechanism.
• Treat MiniSat UNKNOWN or MiniSat-only UNSAT as a covering exclusion.
  This MiniSat build and formula. · UNKNOWN proves nothing, and this build supplies no accepted DRAT/LRAT negative certificate. · Fail-closed scope guards in both runner and independent checker. · A directly validated SAT cover or an UNSAT proof replayed under the campaign verification contract.

• Previously untested high-symmetry 4-regular pair-surplus graph.
  A different H changes the mathematical cylinder while preserving the validated inherited-threshold compiler; any checked SAT model remains globally decisive. · Select a nonduplicate H, prove its automorphism normalization, reconstruct the threshold map independently, and run one five-second model-producing gate. · high · open
• Canonical loopless 4-regular multigraph ownership prefix.
  A disjoint catalogue is the missing bridge from isolated H cylinders to a global negative route. · Enumerate a tiny canonical prefix under a fixed node/time cap and independently test canonicality, duplicate rejection, and exact ownership. · normal · open

Objective: Test inherited-threshold reuse on one previously untested high-symmetry 4-regular pair-surplus graph with a proved normalization scope.

First action: Enumerate candidate high-symmetry 4-regular graphs already present in campaign artifacts, reject duplicates, and freeze one exact automorphism-orbit and threshold-map specification.

Stop condition: Redirect on duplicate prior work, ownership failure, byte-reconstruction mismatch, five-second UNKNOWN, or any unsupported negative-proof claim.

• Do not lengthen or repeat the flat MiniSat seed-1 H=3K5 run without a material reopening change.
• Enumerate candidate high-symmetry 4-regular pair-surplus graphs already represented in campaign artifacts and select one not previously compiled.
• Freeze its automorphism orbit, representative block, threshold map, and direct SAT acceptance predicate before one five-second model-producing run.
• In parallel planning, define a tiny capped canonical-prefix enumeration of loopless 4-regular multigraphs with exact ownership checks before solving any leaves.

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

GPT-5.6 Sol acted as principal investigator. Two GPT-5.6 Terra delegates supplied advisory prior-art and experiment-verification memos; Sol audited their claims, rejected stale rerun suggestions, and did not treat model agreement as validation. Deterministic work used CPython 3.12.3, MiniSat 2.2.1, GNU taskset/time, SHA-256, and the computational-researcher experiment harness. Web search checked the maintained Covering Repository, LJCR, and arXiv status and rejected an unsupported secondary claim. No SAT witness, DRAT/LRAT proof, CAS, proof assistant, PB solver/replayer, cloud lab, external proof service, or human validator produced terminal evidence.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

876.8s

Review state

not a result claim

Attempt ID

covering-c1563-20260811-201039-7aff20

No human review recorded.