YES (VAR z) (RULES i(g(c(z))) -> e(f(c(z))) a(z) -> i(y(z)) y(b(z)) -> g(z) x(h(j(g(z)))) -> x(h(z)) w(e(z)) -> h(j(z)) j(f(z)) -> z u(z) -> x(w(d(y(z)))) o(z) -> x(h(j(f(c(z))))) x(w(i(z))) -> x(w(d(z))) d(g(c(z))) -> e(g(c(z))) ) (COMMENT Termination is shown by ELPO with interpretations on natural numbers x_A(x1) = 0 w_A(x1) = x1 + 1 e_A(x1) = x1 + 1 f_A(x1) = x1 g_A(x1) = x1 + 1 c_A(x1) = 1 d_A(x1) = 4 i_A(x1) = 5 u_A(x1) = x1 b_A(x1) = x1 + 1 o_A(x1) = x1 + 3 a_A(x1) = x1 + 6 j_A(x1) = x1 + 1 h_A(x1) = x1 + 1 y_A(x1) = x1 x#_A(x1) = x1 w#_A(x1) = x1 e#_A(x1) = x1 f#_A(x1) = x1 g#_A(x1) = x1 c#_A(x1) = x1 d#_A(x1) = x1 i#_A(x1) = x1 u#_A(x1) = x1 b#_A(x1) = x1 o#_A(x1) = x1 a#_A(x1) = x1 j#_A(x1) = x1 h#_A(x1) = x1 y#_A(x1) = x1 and precedence: o > u > a > y > g > x > w > d > i > h > j > e > f > b > c )