Two terms are

A set of unifiers for two terms is *complete* if every unifier of the two
terms is a substitution instance of some unifier in the set. A unifier of two
terms is a *most general unifier* if, whenever it is (equivalent to) a
substitution instance of another unifier, that other unifier is also
(equivalent to) a substitution instance of it. For any two unifiable terms
containing ac and/or commutative operators, there is a finite set of most
general unifiers that is complete.