Function equivalent_modulo_symmetry 

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

Logical equivalence F ≡ S, symmetry-reduced. F ≡ S iff F ⊨ S and S ⊨ F, and F ⊨ S iff F entails every clause of S. The key reduction: for a common automorphism σ ∈ Aut(F) ∩ Aut(S), F ⊨ C ⟺ F ⊨ σ(C) (a model of F ∧ ¬C maps under σ to a model of F ∧ ¬σ(C)), so it suffices to check one clause per orbit of S’s clauses under the common symmetry (and dually for F). The verdict is unchanged from the naive check — only the work shrinks — and a Differ witness is a concrete, re-checkable disagreement (it satisfies one formula and violates a clause of the other). This is the symmetry-aware companion to crate::sat::prove_equivalence.