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 EKBO with interpretations on natural numbers b_A(x1) = x1 + 1 d_A(x1) = x1 + 1 a_A(x1) = x1 + 1 e_A(x1) = x1 + 2 c_A(x1) = x1 + 1 weights w0 = 1 w(b) = 1 w(d) = 1 w(a) = 1 w(e) = 3 w(c) = 1 and precedence: c > b > d > a > e )