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