YES (VAR x0 z) (RULES w(d(g(c(x0)))) -> h(j(g(c(x0)))) w(i(g(c(x0)))) -> h(c(x0)) 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 e(f(c(z))) -> i(y(b(c(z)))) u(z) -> x(w(i(y(z)))) o(z) -> x(h(c(z))) x(w(d(z))) -> x(w(i(z))) e(g(c(z))) -> d(g(c(z))) ) (COMMENT Termination is shown by LPO with precedence: o > u > w > h > f > a > e > d > j > i > b > g > y > x > c )