Function equivalence_check_counts 

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

(checks_with_symmetry, naive_checks) — the number of entailment checks the symmetry reduction performs (one per clause-orbit, both directions) versus the naive per-clause count. Equal when there is no usable common symmetry; strictly smaller when the shared automorphism group fuses clauses into orbits.