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