Function cofactor 

pub fn cofactor(clauses: &CanonClauses, x: u32, b: bool) -> CanonClauses

The Shannon cofactor F|_{x=b}: drop clauses satisfied by x=b, delete the x literal from the rest, recanonicalize. An empty clause survives as ⊥ (the branch is UNSAT on the spot).