YES (VAR x) (RULES b(a(x)) -> a(b(x)) a(a(a(x))) -> b(x) b(b(b(b(x)))) -> a(x) c(x) -> b(b(b(x))) e(x) -> a(b(x)) d(x) -> a(a(b(x))) ) (COMMENT Termination is shown by EKBO with interpretations on natural numbers a_A(x1) = 0 e_A(x1) = x1 + 1 d_A(x1) = 0 b_A(x1) = 0 c_A(x1) = 0 weights w0 = 1 w(a) = 1 w(e) = 13 w(d) = 23 w(b) = 1 w(c) = 8 and precedence: b > d > a > e > c )