¹In the present 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 (see [74]) but it is very costly in Ax-unification, e.g., the AC-unification considered in Chapter 12 does not always provide a minimal set of unifiers.