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