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