YES
(VAR z x y)
(RULES 
f(c(a,z,x)) -> b(a,z)
b(x,b(z,y)) -> f(b(f(f(z)),c(x,z,y)))
b(y,z) -> z
)

Proving termination of rewriting for gen_1:

-> Dependency pairs:
nF_f(c(a,z,x)) -> nF_b(a,z)
nF_b(x,b(z,y)) -> nF_f(b(f(f(z)),c(x,z,y)))
nF_b(x,b(z,y)) -> nF_b(f(f(z)),c(x,z,y))
nF_b(x,b(z,y)) -> nF_f(f(z))
nF_b(x,b(z,y)) -> nF_f(z)

-> Dependency pairs narrowed: 
nF_b(x,b(z,y)) -> nF_f(f(z))

-> New dependency pairs: 
nF_b(x,b(c(a,z,x),y)) -> nF_f(b(a,z))

-> Proof of termination for gen_1_1:
-> -> Dependency pairs in cycle:
nF_f(c(a,z,x)) -> nF_b(a,z)
nF_b(x,b(c(a,z,x),y)) -> nF_f(b(a,z))
nF_b(x,b(z,y)) -> nF_f(z)
nF_b(x,b(z,y)) -> nF_f(b(f(f(z)),c(x,z,y)))

UsableRules:
f(c(a,z,x)) -> b(a,z)
b(x,b(z,y)) -> f(b(f(f(z)),c(x,z,y)))
b(y,z) -> z

Polynomial Interpretation:

[f](X) = 1/2.X
[c](X1,X2,X3) = 2.X2 + 2
[a] = 0
[b](X1,X2) = 2.X1 + X2 + 1
[nF_f](X) = X
[nF_b](X1,X2) = 2.X2 + 2

TIME: 0.35054700000000005

-> -> Dependency pairs in cycle:
nF_f(c(a,z,x)) -> nF_b(a,z)
nF_b(x,b(z,y)) -> nF_f(z)
nF_b(x,b(c(a,z,x),y)) -> nF_f(b(a,z))

UsableRules:
f(c(a,z,x)) -> b(a,z)
b(x,b(z,y)) -> f(b(f(f(z)),c(x,z,y)))
b(y,z) -> z

Polynomial Interpretation:

[f](X) = 1/2.X
[c](X1,X2,X3) = 2.X2 + 2
[a] = 0
[b](X1,X2) = 2.X1 + X2 + 1
[nF_f](X) = 2.X
[nF_b](X1,X2) = 2.X2

TIME: 0.479509

-> -> Dependency pairs in cycle:
nF_f(c(a,z,x)) -> nF_b(a,z)
nF_b(x,b(z,y)) -> nF_f(z)

Termination proved: Cycles verify subterm criterion.

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.