Function weak_php 

pub fn weak_php(pigeons: usize, holes: usize) -> (DimacsCnf, ExpectedVerdict)

The weak pigeonhole principle PHP^{holes}_{pigeons}: pigeons pigeons into holes holes — unsatisfiable exactly when pigeons > holes. Generalizes php (which is the tight holes = pigeons − 1 case) to any hole count, including the weak regime (holes = 2·pigeons, pigeons², …) used to probe how far symmetry breaking scales as the holes-to-pigeons ratio grows. Same variable layout as php — “pigeon p in hole h” at index p*holes + h — so weak_php(n, n−1) is byte-for-byte php(n).