Function perm_is_automorphism 

pub fn perm_is_automorphism(clauses: &[Vec<Lit>], sigma: &Perm) -> bool

Is sigma a genuine automorphism of clauses — does applying it map the clause set exactly onto itself? The independent re-verification every generator must pass.

σ is an automorphism iff σ(C) ∈ F for every clause C ∈ F (a literal-permutation is a bijection on clauses, so mapping F into itself forces it onto itself). A clause whose variables are all fixed by σ maps to itself and is trivially present — so only clauses touching σ’s support (its moved variables) need a membership check. For the small-support generators symmetry breaking actually uses (transpositions, short cycles) this inspects a handful of clauses instead of re-sorting the whole database, which is the difference between an O(n⁴) and an O(n³) certified pigeonhole refutation.