¹ E ∪ Ax-unification is available via the variant-based equational unification explained in Section 14.9 . Note, however, that Maude will only perform E ∪ 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.