YES (VAR x0 x) (RULES e(e(e(e(e(e(e(e(e(e(e(e(x0)))))))))))) -> e(x0) c(x) -> e(e(e(e(e(x))))) a(x) -> e(e(e(x))) b(x) -> e(e(e(e(e(e(e(e(e(x))))))))) d(x) -> e(e(e(e(x)))) ) (COMMENT Termination is shown by KBO with weight w0 = 1 w(a) = 15 w(e) = 1 w(d) = 76 w(b) = 89 w(c) = 12 and precedence: b > c > d > e > a )