YES (VAR x0 x) (RULES c(c(c(c(x0)))) -> b(x0) b(b(b(x))) -> c(x) c(b(x0)) -> b(c(x0)) a(x) -> b(c(x)) d(x) -> c(c(c(x))) e(x) -> b(b(c(x))) ) (COMMENT Termination is shown by EKBO with interpretations on natural numbers a_A(x1) = 1 e_A(x1) = 1 d_A(x1) = 1 b_A(x1) = 1 c_A(x1) = 1 e#_A(x1) = 0 d#_A(x1) = 0 b#_A(x1) = x1 weights w0 = 1 w(a) = 4 w(e) = 16 w(d) = 10 w(b) = 1 w(c) = 1 and precedence: c > e > b > a > d )