Function heule_php_ranked 

pub fn heule_php_ranked(n: usize) -> RankedRefutation

The Heule PHP(n) refutation with its rank function attached — each symmetry-breaking step is tagged by the round (m = active items remaining) it belongs to, a non-increasing measure whose descent bounds the proof size. The closing RUP steps take the bottom rank 1. Feed the result to crate::complexity::RankedRefutation::certify to get a checkable O(n²) size bound alongside the correctness check.