There is a beautiful paper by George Boolos related to this, called "A Curious Inference" (in his collected papers called Logic, Logic, and Logic).
Suppose $s$ is a one-place function sign, and $f$ a two-place function sign. And take the five axioms
$\forall n \, f(n, 1) = s1$
$\forall x\, f(1, sx) = ssf(1, x)$
$\forall n\forall x\, f(sn, sx) = f(n, f(sn, x))$
$\forall x(Dx \to Dsx)$
What's going on here is that $f$ is defined to be Ackermann-like (if we think of $s$ as successor) and the last two axioms say that $D$ is hereditary down an $s$ sequence. So we'll have the likes of
But it will take in the order of Ackermann(5,5) steps to get there in first-order logic. And if that isn't a big enough number for you, just choose target
$Df(ss\ldots ss1,ss\ldots ss1)$.
so the first-order proof has the order of Ackermann($n$,$n$) steps!
Now the curious thing of Boolos's title is that while the first-order proof would have vastly more steps then particles in the known universe, we can write down a second-order derivation in a couple of pages (regimenting our informal reasoning that the conclusion does indeed follow).