YES (VAR x0 z) (RULES w(i(g(c(x0)))) -> h(c(x0)) e(f(c(z))) -> i(g(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(i(y(z)))) o(z) -> x(h(c(z))) x(w(d(z))) -> x(w(i(z))) d(g(c(z))) -> e(g(c(z))) ) (COMMENT Termination is shown by KBO with weight w0 = 1 w(x) = 1 w(w) = 1 w(e) = 1 w(f) = 2 w(g) = 1 w(c) = 1 w(d) = 2 w(i) = 1 w(u) = 7 w(b) = 2 w(o) = 9 w(a) = 3 w(j) = 1 w(h) = 1 w(y) = 1 and precedence: x > a > i > e > w > h > f > y > g > d > c > u > o > b > j )