Function bucket_elimination_refute 

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

Full Davis–Putnam bucket elimination in min-degree order, allowing intermediate growth but capping every resolvent at width_cap. If it reaches ⊥, returns the RUP-resolvents-then-deletions proof — a width-≤width_cap resolution refutation, i.e. a 2^width_cap·n certificate that crushes every bounded-treewidth family. Returns None the moment a resolvent would exceed the cap (high treewidth — the certificate would be exponential, which is exactly the Ben-Sasson–Wigderson hardness). Sound: every step is RUP/Delete and independently re-checkable by crate::pr::check_pr_refutation.