What were the shortcomings of Robinson's resolution procedure?
While &quot;disappointing in practice&quot; is certainly not definable formally, unlike &quot;complete&quot; (which does indeed mean &quot;can eventually prove every true formula&quot;), it's pretty easy to find examples where naive resolution is not even remotely adequate, i.e. examples which should be easy to prove but which resolution is extremely slow on.
A famous example is an encoding of the pigeon hole principle for $n$ holes in propositional logic (which is the statement &quot;$n+1$ pigeons cannot fit in $n$ holes without duplicates). There is no proof of this statement using only resolution in time sub-exponential in $n$.
Things are even worse in predicate logic, where it is very easy to find statements without any fast resolution proofs.
Note that any implementation of resolution must implement a strategy for picking the resolvents, which is already a very difficult problem, and an active area of research, since most practical algorithms for theorem proving are enhancements of naive resolution, e.g. hyper-resolution.