YES TRS: f(c(a(),z,x)) -> b(a(),z) b(x,b(z,y)) -> f(b(f(f(z)),c(x,z,y))) b(y,z) -> z max/plus interpretations on N: f_A(x1) = max{1, -4 + x1} f#_A(x1) = max{1, 3} c_A(x1,x2,x3) = max{8, 13 + x1, 8 + x2, -1} c#_A(x1,x2,x3) = max{4, 2 + x1, -14 + x2, -15} a_A = 9 a#_A = 5 b_A(x1,x2) = max{18, 9 + x1, x2} b#_A(x1,x2) = max{0, 2 + x1, -14 + x2} precedence: c = b > a > f