Function heule_clique_refutation 

pub fn heule_clique_refutation(n: usize, k: usize) -> CertifiedRefutation

Full-chain structural steering of clique_coloring(n, k) (UNSAT for k < n): the Heule pigeonhole refutation transplanted onto the coloring encoding, wielding the a-priori vertex-swap symmetry rather than detecting it. k + 1 mutually-adjacent vertices already form a PHP(k+1, k), so the proof forces those k+1 vertices out of the colors one at a time — each clause ¬x(i, color) certified by the substitution “swap vertex i with the last active vertex”, whose SR check clashes at once on the corresponding at-most-one clause. The whole stream is verified against the original clique formula alone.