YES (VAR x x0) (RULES c(x) -> x b(x0) -> x0 a(x) -> x ) (COMMENT Termination is shown by KBO with weight w0 = 1 w(a) = 27 w(c) = 5 w(b) = 1 and precedence: a > c > b )