YES (VAR x0 x) (RULES a(a(a(a(x0)))) -> c(c(c(x0))) d(a(a(x0))) -> c(c(c(x0))) a(a(d(x0))) -> c(c(c(x0))) c(c(c(a(x0)))) -> c(c(c(x0))) a(c(a(a(x0)))) -> c(c(c(x0))) c(c(a(a(x0)))) -> c(c(c(x0))) a(a(c(x0))) -> c(a(a(x0))) d(d(x)) -> c(c(a(c(x)))) c(d(x)) -> a(a(x)) c(c(c(c(x)))) -> c(c(c(x))) b(x) -> c(c(x)) a(c(c(x))) -> c(c(c(x))) d(c(x)) -> a(a(x)) ) (COMMENT Termination is shown by ELPO with interpretations on natural numbers a_A(x1) = 8 d_A(x1) = 9 c_A(x1) = 8 b_A(x1) = 8 and precedence: d > a > b > c )