YES
(VAR X)
(RULES 
c(b(a(X))) -> a(a(b(b(c(c(X))))))
a(X) -> e
b(X) -> e
c(X) -> e
)

Proving termination of rewriting for lindau:

-> Dependency pairs:
nF_c(b(a(X))) -> nF_a(a(b(b(c(c(X))))))
nF_c(b(a(X))) -> nF_a(b(b(c(c(X)))))
nF_c(b(a(X))) -> nF_b(b(c(c(X))))
nF_c(b(a(X))) -> nF_b(c(c(X)))
nF_c(b(a(X))) -> nF_c(c(X))
nF_c(b(a(X))) -> nF_c(X)

-> Proof of termination for lindau_1:
-> -> Dependency pairs in cycle:
nF_c(b(a(X))) -> nF_c(c(X))
nF_c(b(a(X))) -> nF_c(X)

UsableRules:
c(b(a(X))) -> a(a(b(b(c(c(X))))))
a(X) -> e
b(X) -> e
c(X) -> e

Polynomial Interpretation:

[c](X) = X
[b](X) = 2.X
[a](X) = 1/2.X + 2
[e] = 0
[nF_c](X) = 2.X

TIME: 3.7e-4

-> -> Dependency pairs in cycle:
nF_c(b(a(X))) -> nF_c(c(X))

UsableRules:
c(b(a(X))) -> a(a(b(b(c(c(X))))))
a(X) -> e
b(X) -> e
c(X) -> e

Polynomial Interpretation:

[c](X) = X
[b](X) = 2.X
[a](X) = 1/2.X + 2
[e] = 0
[nF_c](X) = 2.X

TIME: 2.04e-4


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



Termination was proved succesfully.