YES
(VAR X)
(RULES 
a -> g(c)
g(a) -> b
f(g(X),b) -> f(a,X)
)

Proving termination of rewriting for mfp90b:

-> Dependency pairs:
nF_a -> nF_g(c)
nF_f(g(X),b) -> nF_f(a,X)
nF_f(g(X),b) -> nF_a

-> Dependency pairs narrowed: 
nF_f(g(X),b) -> nF_f(a,X)

-> New dependency pairs: 
nF_f(g(X),b) -> nF_f(g(c),X)

-> Proof of termination for mfp90b_1:
-> -> Dependency pairs in cycle:
nF_f(g(X),b) -> nF_f(g(c),X)

UsableRules:
g(a) -> b

Polynomial Interpretation:

[a] = 1
[g](X) = X
[c] = 0
[b] = 1
[f](X1,X2) = 0
[nF_f](X1,X2) = X1 + X2

TIME: 5.3378e-2


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.