Function certified_unsat 

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

Solve formula with certified symmetry breaking under the given generators (each must be a genuine automorphism — they are re-checked implicitly by the per-clause PR self-check).

For each generator we propose its lead lex-leader clause, PR-self-check it against the database built so far (so a generator invalidated by earlier SBPs is simply skipped), add the survivors as PR steps, solve the augmented formula, and — if UNSAT — append the solver’s learned clauses as RUP steps. The composed stream is verified against formula alone.