¹ $E\cup Ax$-unification is available via the variant-based equational unification explained in Section 14.9. Note, however, that Maude will only perform $E\cup Ax$-unification with those equations $E$ that have been declared with the variant attribute. In particular, if no equation in $E$ has the variant attribute, Maude will only perform the $Ax$-unification explained in Section 13.4.