Function entails_certified_prepared 

pub fn entails_certified_prepared(
    prepared: &Cnf,
    goal: &ProofExpr,
) -> Option<Verdict>

Certify prepared ⊨ goal against a premise CNF clausified ONCE by Cnf::from_premises. Solving a whole puzzle this way pays the of-pair Tseitin cost a single time, then each cell only adds its ¬goal unit — the incremental win.