Function clauses_to_expr 

pub fn clauses_to_expr(clauses: &[Vec<Lit>]) -> Option<ProofExpr>

Build the CNF ProofExpr over atoms x{var} from raw clauses — the door into the certified prover, scalable (no cube). None on an empty clause or empty formula.