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