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