Function reduce 

pub fn reduce(clauses: &CanonClauses) -> CanonClauses

A sound poly reduction to fixpoint: unit propagation, then pure-literal elimination, then subsumption, iterated. Each step preserves (un)satisfiability and commutes with relabeling, so reduce(π(F)) = π(reduce(F)) — which makes ReduceIso a legitimate coarsening of UnitPropIso.