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