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