YES
(VAR X)
(RULES 
f(f(X)) -> f(g(f(g(f(X)))))
f(g(f(X))) -> f(g(X))
)

Proving termination of rewriting for aoto:

-> Dependency pairs:
nF_f(f(X)) -> nF_f(g(f(g(f(X)))))
nF_f(f(X)) -> nF_f(g(f(X)))
nF_f(f(X)) -> nF_f(X)
nF_f(g(f(X))) -> nF_f(g(X))

-> Proof of termination for aoto_1_1:
-> -> Dependency pairs in cycle:
nF_f(f(X)) -> nF_f(X)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for aoto_1_2:
-> -> Dependency pairs in cycle:
nF_f(g(f(X))) -> nF_f(g(X))

There are no usable rules.

Polynomial Interpretation:

[f](X) = X + 1
[g](X) = X
[nF_f](X) = X

TIME: 0.136318


SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in DG + base ordering
Upper bound for coeffs: 1
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Linear
Coeffs in polynomials: No rationals
Delta: automatic



Termination was proved succesfully.