Lemma: Application of instantiation followed by resolution can be replaced by application of mgu-resolution followed by instantiation.

Lemma: If empty clause is derived using instantiation with resolution, and instantiation then it can also be obtained by using mgu-resolution.

Theorem: The mgu-resolution is complete for checking whether a set of clauses is contradictory.