Function check_pr_refutation_fast 

pub fn check_pr_refutation_fast(
    num_vars: usize,
    original: &[Vec<Lit>],
    steps: &[ProofStep],
) -> bool

check_pr_refutation accelerated by an incrementally-maintained AutomorphismIndex — the same verdict, but each substitution step’s automorphism re-check costs O(support) rather than O(|db|). Falls back to the stateless checker if the proof deletes clauses (the index is append-only, and certified symmetry refutations do not delete).