YES TRS: f(a(),b()) -> f(a(),c()) f(c(),d()) -> f(b(),d()) max/plus interpretations on N: f_A(x1,x2) = max{0, 2, 1} f#_A(x1,x2) = max{1, 2 + x1, 5} a_A = 0 a#_A = 0 b_A = 1 b#_A = 5 c_A = 4 c#_A = 4 d_A = 1 d#_A = 5 precedence: c > d > b > f > a