YES (VAR x) (RULES g(g(g(x))) -> x f(x) -> g(g(x)) ) (COMMENT Termination is shown by EKBO with interpretations on natural numbers f_A(x1) = x1 + 2 g_A(x1) = x1 + 1 weights w0 = 1 w(f) = 3 w(g) = 1 and precedence: g > f )