# Does Cutting Planes solve Pigeongole Principle for holes of different sizes?

Suppose a problem:

Given $$n$$ pigeons and $$m$$ holes of sizes $$b_{i\le m}$$ decide if you can put all pigeons in given holes.

It's possible to find a refutation of size $$\mathcal O(n^2\log^2 n)$$ of this principle when it's encoded as a conjunction of threshold functions, therefore there must exist a polynomial size Frege refutation any time $$n>\sum_{i=1}^m b_i$$.

However, is Cutting Planes too weak already to have a polynomial size refutation for the $$n=1+ \sum_{i=1}^m b_i$$ case?

Let $$x_{ij}$$ state that pigeon $$i$$ goes to hole $$j$$. One can axiomatize the pigeonhole principle as follows:
1. Booleanity: $$0 \leq x_{ij} \leq 1$$.
2. Pigeon axioms: for all $$i$$, $$\sum_j x_{ij} \ge 1$$.
3. Hole axioms: for all $$j$$, $$\sum_i x_{ij} \le b_j$$.
Summing the pigeon axioms, we get $$\sum_{ij} x_{ij} \ge n.$$ Summing the hole axioms, we get $$\sum_{ij} x_{ij} \leq m.$$ Therefore $$n \leq m$$, which is a contradiction if $$m < n$$.