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