Function solve_by_measure_synthesis 

pub fn solve_by_measure_synthesis(
    num_vars: usize,
    formula: &[Vec<Lit>],
) -> Option<(CollapsingMeasure, RankedRefutation)>

The whole inversion: discover the Lyapunov function, then let the proof fall out. Search the covering-layout class; for each candidate whose item-swap is a symmetry, run the steered collapse; return the first that yields a checking refutation, paired with the measure that drove it. None is a bounded impossibility — no covering-symmetry collapse exists for this formula.