Function is_pr_indexed 

pub fn is_pr_indexed(
    num_vars: usize,
    db: &[Vec<Lit>],
    index: &mut AutomorphismIndex,
    clause: &[Lit],
    witness: &Witness,
) -> bool

is_pr with the automorphism re-check served by a pre-built incremental AutomorphismIndex (which must hold exactly the clauses of db). Identical verdict to is_pr — the index is an acceleration structure — but the substitution path no longer rebuilds the membership set per call, the difference between an O(n⁴) and an O(n³) certified refutation.