Function bve 

pub fn bve(
    num_vars: usize,
    clauses: &[Vec<Lit>],
) -> (Vec<Vec<Lit>>, Vec<ProofStep>)

Bounded variable elimination over the whole formula: repeatedly eliminate every variable whose elimination is non-growing, until a fixpoint (capped at a few passes). Returns the simplified clause set and the composed proof steps.