Function certified_unsat_auto 

pub fn certified_unsat_auto(
    num_vars: usize,
    formula: &[Vec<Lit>],
) -> CertifiedRefutation

Solve formula with FULL certified symmetry breaking, discovering the symmetries itself.

Each round: detect the residual symmetry group of the current database, certify ONE lead lex-leader predicate as a PR step (always sound — its generator is a fresh automorphism of the current database, so the SR check’s conflict is immediate), and re-detect. Adding the predicate strictly shrinks the automorphism group, so the loop terminates with the whole group broken; then the augmented formula is solved and the learned clauses appended as RUP steps. The entire composed stream is verified against formula ALONE.

This breaks the complete group rather than one clause per generator, by re-detecting the stabilizer after each predicate — the natural “lift and shift” of detection + the SR checker.