What were the shortcomings of Robinson’s resolution procedure?


Paulson et alii. From LCF to Isabelle/HOL say:

Resolution for first-order logic, complete in principle but frequently disappointing in practice.

I think complete means they can proof any true formula in first-order logic correct. In the Handbook of Automated Reasoning I find:

Resolution is a refutationally complete theorem proving method: a contradiction (i.e., the empty clause) can be deduced from any unsatisfiable set of clauses.

From Wikipedia:

Attempting to prove a satisfiable first-order formula as unsatisfiable may result in a nonterminating computation

Why is that disappointing?