³Although unification with the assoc attribute but without the comm attribute is infinitary in general, we support a substantial class of equational problems for which it is finitary, and provide a finite but incomplete set of solutions (with an explicit warning that it may be incomplete) in all other cases. See Section 13.4.6.