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