We describe CNFs in n variables which, over a range of parameters, have small resolution refutations but are such that any small refutation must have height larger than n (even exponential in n), where the height of a refutation is the length of the longest path in it. This is called a supercritical tradeoff between size and height because, if we do not care about size, every CNF is refutable in height n. A similar result appeared in [Fleming, Pitassi and Robere, ITCS'22], for different formulas using a more complicated construction.

Small refutations of our formula are necessarily highly irregular, making it a plausible candidate to separate resolution from pool resolution, which amounts to separating CDCL with restarts from CDCL without. We are not able to show this, but we show that a simpler version of our formula, with a similar irregularity property, does have polynomial size pool resolution refutations.