YES TRS: f(g(f(a()),h(a(),f(a())))) -> f(h(g(f(a()),a()),g(f(a()),f(a())))) max/plus interpretations on N: f_A(x1) = max{6, 12 + x1} f#_A(x1) = max{6, 12 + x1} g_A(x1,x2) = max{20, 5 + x1, 20 + x2} g#_A(x1,x2) = max{20, 5 + x1, 20 + x2} a_A = 0 a#_A = 0 h_A(x1,x2) = max{35, 39 + x1, 2 + x2} h#_A(x1,x2) = max{35, 39 + x1, 2 + x2} precedence: g > f > a > h