Symbols are ordered such that variables precede function symbols.
Terms are ordered by increasing written length; equally long terms
are ordered lexicographically. For a set T of terms, its disagreement
path p is the lexicographically least path where two member terms
of T differ. Its disagreement set is the set of subterms starting at p,
formally: }.
Algorithm: (en)
