YES TRS: a(c(d(x))) -> c(x) u(b(d(d(x)))) -> b(x) v(a(a(x))) -> u(v(x)) v(a(c(x))) -> u(b(d(x))) v(c(x)) -> b(x) w(a(a(x))) -> u(w(x)) w(a(c(x))) -> u(b(d(x))) w(c(x)) -> b(x) linear polynomial interpretations on N: a_A(x1) = x1 + 8 a#_A(x1) = x1 c_A(x1) = x1 + 1 c#_A(x1) = 5 d_A(x1) = x1 + 3 d#_A(x1) = x1 + 5 u_A(x1) = x1 u#_A(x1) = 6 b_A(x1) = 1 b#_A(x1) = 7 v_A(x1) = x1 + 1 v#_A(x1) = x1 + 7 w_A(x1) = x1 + 1 w#_A(x1) = x1 + 7 precedence: a > v > c = d > w > b > u