^{2}In 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).