YES TRS: c(b(a(X))) -> a(a(b(b(c(c(X)))))) a(X) -> e() b(X) -> e() c(X) -> e() linear polynomial interpretations on N: c_A(x1) = 3 c#_A(x1) = 1 b_A(x1) = 1 b#_A(x1) = x1 + 1 a_A(x1) = 3 a#_A(x1) = 3 e_A = 0 e#_A = 0 precedence: a > c > b > e