YES (VAR x0 x) (RULES e(a(x0)) -> a(e(x0)) c(a(x0)) -> a(c(x0)) b(a(x0)) -> a(c(x0)) b(e(x0)) -> a(x0) c(e(x)) -> a(x) e(c(x)) -> a(x) d(a(x)) -> e(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 + 1 c_A(x1) = x1 + 1 c#_A(x1) = 0 weights w0 = 1 w(b) = 1 w(d) = 1 w(a) = 1 w(e) = 1 w(c) = 1 and precedence: d > c > e > b > a )