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