YES (VAR x0) (RULES w(a(a(a(a(w(x0)))))) -> a(a(a(w(a(a(a(a(a(a(x0)))))))))) w(a(a(a(w(x0))))) -> a(a(a(a(a(w(a(a(a(x0))))))))) w(w(x0)) -> a(w(a(a(a(a(x0)))))) w(a(a(a(a(a(w(x0))))))) -> a(a(w(a(x0)))) w(a(w(x0))) -> a(a(a(a(w(a(a(x0))))))) c(x0) -> a(a(w(a(a(x0))))) w(a(a(a(a(a(a(w(x0)))))))) -> a(a(a(a(a(a(w(a(a(a(a(a(x0)))))))))))) a(a(a(a(a(a(a(x0))))))) -> x0 w(a(a(w(x0)))) -> a(a(a(a(a(x0))))) u(x0) -> a(a(a(a(a(a(x0)))))) v(x0) -> a(a(w(a(a(a(x0)))))) b(x0) -> w(a(a(a(a(a(a(w(a(a(x0)))))))))) ) (COMMENT Termination is shown by EKBO with interpretations on natural numbers a_A(x1) = x1 + 2 c_A(x1) = x1 + 2339 b_A(x1) = x1 + 5844 u_A(x1) = x1 + 15195 v_A(x1) = x1 + 3506 w_A(x1) = x1 + 12 a#_A(x1) = x1 b#_A(x1) = x1 weights w0 = 1 w(a) = 84 w(c) = 2421 w(b) = 7095 w(u) = 16757 w(v) = 2507 w(w) = 2084 and precedence: u > b > v > w > c > a )