A difficult tableau proof
By the way, here's another problem my prover can't solve (in reasonable time):
Show: ∀y∃z∀x(Fxz ↔ x=y) → ¬∃w∀x(Fxw ↔ ∀u(Fxu → ∃y(Fyu ∧ ¬∃z(Fzu ∧ Fzy))))
This is problem 54 in Pelletier 1986. It is a pure first-order adaptation of a little theorem proved in Montague 1955. Montague gives a fairly simple proof. His proof uses the Cut rule, which the tableau method doesn't have. I've tried to construct a tableau proof by hand, but failed.
This might be a nice example of a relatively straightforward fact that can be proved easily with Cut, but not without.