YES (VAR x0) (RULES f(f(f(x0))) -> x0 g(x0) -> f(f(x0)) ) (COMMENT Termination is shown by ELPO with interpretations on natural numbers f_A(x1) = x1 + 1 g_A(x1) = x1 + 3 f#_A(x1) = x1 g#_A(x1) = x1 and precedence: g > f )