Function common_automorphism_generators 

pub fn common_automorphism_generators(
    num_vars: usize,
    f: &[Vec<Lit>],
    s: &[Vec<Lit>],
) -> Vec<Perm> 

The common variable automorphisms of two formulas — phase-free permutations σ with σ(F)=F AND σ(S)=S, a generating set for a subgroup of Aut(F) ∩ Aut(S). Detected from each formula’s own automorphisms and then VERIFIED against both clause sets, so every returned generator is a genuine common automorphism (a wrong one can never slip through). This is the group under which a disagreement between F and S is symmetric: if σ fixes both, then F and S disagree at a iff they disagree at σ(a) — so equivalence checking can be reduced along its orbits.