Apply the Knuth-Bendix completion procedure to the reduction system

and the term order described below.

Assume a lexicographic ordering of the function symbols . The term order is defined by if

1. has fewer letters than and contains each variable at most as often as , or
2. if they have the same number of letters and variable occurrences, then if or and there is a such that for and .

Please submit a handwritten and readable solution in PDF format.