Complete 16-row, four-literal no-proof r=2 incidence frontier compared with an equal-budget unsplit CaDiCaL control.

incidence-matrix SAT with orbitope symmetry breaking

Partition the retained fixed-first/fixed-second r=2 CNF by all assignments of variables 31-34 and compare aggregate fresh-process conflict throughput against one unsplit process.

Hypothesis: The complete no-proof four-literal r=2 frontier yields a directly checked 30-cover or at least 1.25x the conflict throughput of an equal-budget unsplit control.

Test: Run sixteen fresh seed-0 one-second CaDiCaL leaves and one fresh sixteen-second unsplit control, then independently reconstruct the partition and compare conflicts per process-second.

Both producer and independent checker reproduce the partition, logs, rates, resource bounds, and failed gate. Because proof logging was disabled, only the bounded performance result—not any covering exclusion—is supported.

• Under the exact frozen protocol, the split/control conflict-rate ratio is 0.6956225517262626.
• The sixteen cubes form an exact partition of the pinned r=2 formula.
• No checked SAT witness was returned during the bounded experiment.
• No covering-number bound changed.

• python3 scripts/run_r2_no_proof_frontier_v1.py --out-dir artifacts/epoch63-20260810/r2-no-proof-frontier-v1
• python3 checkers/check_r2_no_proof_frontier_v1.py --receipt artifacts/epoch63-20260810/r2-no-proof-frontier-v1/frontier-receipt.json --out artifacts/epoch63-20260810/r2-no-proof-frontier-v1/independent-check.json
• sha256sum -c artifacts/epoch63-20260810/SHA256SUMS
• Exact scope: one fixed-first/fixed-second r=2 formula, seed 0, sixteen one-second leaves and one sixteen-second control.

• .proof-experiments/20260810-193445-3e88e0: primary run completed in 20.175 seconds; no SAT model; rate ratio 0.6956225517262626.
• .proof-experiments/20260810-193541-98d3e8: independent checker passed in 0.476 seconds and rejected all five mutations.

checkers/check_r2_no_proof_frontier_v1.py independently regenerates the truth table, reconstructs every CNF byte, reparses raw logs, recomputes the gate, checks process/resource isolation, and rejects five mutations.

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

• Cube-and-conquer -> shallow exact splitting was predicted to raise search throughput -> observed aggregate throughput fell to 0.6956225517262626x, so this split is rejected as an optimization.

• The sixteen assignments of variables 31-34 are unique, pairwise disjoint, and exhaustive.
  artifacts/epoch63-20260810/r2-no-proof-frontier-v1/independent-check.json · Pinned r=2 CNF only · computed
• The split/control conflict-rate ratio was 0.6956225517262626.
  Primary receipt plus independently reparsed raw logs · CaDiCaL 1.7.3, seed 0, frozen 32-solver-second protocol · computed

• Use the unchanged no-proof four-variable split of the retained r=2 incidence formula as a throughput improvement.
  All sixteen one-second leaves versus one sixteen-second unsplit seed-0 control on the pinned formula and solver · No SAT model appeared and the rate ratio 0.6956225517262626 was below the 1.25 gate. · frontier-receipt.json and independent-check.json · A checked SAT witness or a material encoding/decomposition change with a fresh matched prediction of at least 1.25x.

• Two-cut root-link intersection-profile relaxation
  It couples regional degree and uncovered-pair demands that separate cut inequalities may satisfy incompatibly. · Run an independently checked bounded sample using at most 56 residual block types and ten regional capacity inequalities. · high · open
• Multi-anchor support-three constructive escape search
  A witness directly settles the value and the mechanism differs from the closed support-two neighborhoods. · Compare deterministic support-three transitions against the frozen fresh-start baseline under matched proposals. · normal · open

Objective: Determine whether a two-cut four-cell residual-block relaxation can eliminate at least 10 percent of the 2094 recorded root-link survivors.

First action: Write and independently verify the necessary-condition lemma and freeze the sample, cut-selection rule, exact solver, mutation controls, and 10 percent gate.

Stop condition: Redirect on unsafe implication, checker disagreement, solver UNKNOWN, sample signal below 10 percent, or projected runtime requiring an unsubmitted lab job.

• Formalize the two-cut four-cell residual-block profile relaxation as a one-sided necessary condition.
• Freeze a deterministic tight-cut-pair selection and bounded sample of the 2094 epoch-62 survivors.
• Implement a materially independent exact checker and continue only for a projected incremental rejection rate of at least 10 percent.
• Do not treat the fourteen raw UNSAT leaves as exclusions or restore proof tracing for the unchanged failed timing route.

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

GPT-5.6 Sol served as principal investigator. GPT-5.6 Terra delegates supplied advisory reconnaissance only and were not counted as evidence or validation. Python 3.12.3 implemented the runner and checker; CaDiCaL 1.7.3 performed SAT search; SHA-256 bound artifacts. The C cover checker and GCC were available but no SAT model triggered them. No CAS, proof assistant, proof replayer, cloud lab, external proof service, or human validator produced evidence.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1091.1s

Review state

not a result claim

Attempt ID

covering-c1563-20260810-194133-68baa4

No human review recorded.