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.
Attempting to prove a satisfiable first-order formula as unsatisfiable may result in a nonterminating computation
Why is that disappointing?