YES (VAR x x0) (RULES c(x) -> x b(x0) -> x0 a(x) -> x ) (COMMENT Termination is shown by EKBO with interpretations on natural numbers a_A(x1) = 6 c_A(x1) = x1 + 1 b_A(x1) = 3 c#_A(x1) = x1 weights w0 = 1 w(a) = 27 w(c) = 5 w(b) = 1 and precedence: a > c > b )