I think something like the following might be what was meant:
Suppose there is a proof of ${\rm flies}({\rm penguin})$. Now rewrite the proof in the following way:
- Choose variable letters $y$ and $w$ that don't appear anywhere in the proof.
- Replace every ${\rm penguin}$ with $y$ and every term other than ${\rm penguin}$ by $w$.
- Replace every instance of the predicate ${\rm flies}(t)$ with $\neg(t=y)$.
- Replace every remaining atomic formula (including ${\rm bird}(t)$) that isn't an equality by $y=y$.
Argue that this substitution converts every valid inference step (or logical axiom) into another valid inference step. Therefore the substituted proof is actually a valid proof in the pure theory of equality of
$$ y=y, w \ne y, \forall x(x\ne y\to x\ne y) \vdash y \ne y $$
However, the first and last of these premises are certainly provable (in standard first-order logic), and if we plug in their proofs we get
$$ w \ne y \vdash y \ne y $$
which (by the deduction theorem, contraposition, and the fact that $\vdash y=y$) yields
$$ \vdash w = y $$
which we can hopefully agree is not the case.
... well, how do we know that $\not\vdash w=y$? Unfortunately, the best argument for that I can come up with is everything that can be proved must be universally true in a structure with two elements (because all of the axioms are and the inference rules preserve that property) -- but that is then basically model theory and therefore presumably doesn't really count as "combinatorial".
I think it might be possible to get through purely syntactically by something in the vein of quantifier elimination, but the details of that elude me for the time being.
