2In the current implementation we are not interested in a minimal set of unifiers, but only in a finite and complete set. Minimality is easily achieved in syntactic unification [87], but it is very costly in Ax-unification or E Ax-unification, e.g., the ACU-unification considered in Section 12.4 does not always provide a minimal set of unifiers (but see Section 12.4.4 for a method to compute a minimal set of ACU-unifiers).