Function quotient_width 

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

The quotient width W(F, ~) — None iff satisfiable.