Function mutilated_chessboard 

pub fn mutilated_chessboard(n: usize) -> (DimacsCnf, ExpectedVerdict)

The mutilated chessboard: an n×n board with two OPPOSITE corners removed, asking for a perfect domino tiling. Every domino covers one black and one white square, but the two removed corners share a colour (for even n), so the black/white counts differ by two and no tiling exists — UNSAT, and a textbook resolution-exponential family. The infeasibility is a bipartite-matching (Hall) obstruction, which our covering route certifies in polynomial time. Variables are dominoes (grid edges between adjacent surviving squares); each surviving square must be covered by exactly one. n must be even (so the parity argument bites).