Function weakest_crushing_rung 

pub fn weakest_crushing_rung(
    num_vars: usize,
    clauses: &[Vec<Lit>],
    ns_budget: usize,
) -> ProofRung

Locate an instance on the ProofRung ladder: the weakest certified cut that crushes it, probed cheapest-first (carve ≺ counting ≺ parity ≺ Nullstellensatz-by-degree). The narrow rungs (Counting, Parity) are incomparable; probe order only decides the label when more than one happens to fire.

This has no satisfiability oracle. BeyondBudget means no certified cut fired — which covers both a satisfiable instance and a hard-UNSAT one beyond the degree budget. Our detectors cannot tell those two apart cheaply; that very indistinguishability is the wall, and resolving it for a family (proving the budget must be exceeded) is P vs NP.