pub fn prove_unsat_certified(e: &ProofExpr) -> Option<Vec<ProofStep>>Expand description
Refute e with the certified recursive symmetry breaker and return the proof. Each round
re-detects the residual automorphism group, certifies ONE lex-leader lead clause as a PR step (its
generator a fresh automorphism of the current database), and re-detects — looping to a fixpoint that
breaks the COMPLETE group, not just the adjacent positive-row swaps crate::symmetry::break_symmetries
sees. The returned stream is the certified PR breaks followed by the closing RUP learned clauses, and
it is already check_pr_refutation-verified against e’s CNF. None if e is not CNF-assertable, is
satisfiable, or the breaker did not certify a refutation — the wired, checkable companion of
prove_unsat’s coarse verdict.