Function quotient_class_count 

pub fn quotient_class_count<C: Congruence + ?Sized>(
    n: usize,
    clauses: &CanonClauses,
    cong: &C,
) -> usize

The collapse measure. The number of ~-classes among the strict distinct-cofactor set: canonicalize every (depth, cofactor) under ~ and count distinct. Because it is a quotient of the fixed set cofactor_set, it satisfies — as theorems, for every formula — quotient_class_count(Raw) = distinct_width and monotonicity under congruence coarsening (iso ≤ rename ≤ raw). This is the clean instrument for “do exponentially-many cofactors fall into polynomially-many classes?”, with no dependence on any branching order.