YES
(VAR x y z)
(RULES 
g(x,y) -> x
g(x,y) -> y
f(0,1,x) -> f(s(x),x,x)
f(x,y,s(z)) -> s(f(0,1,z))
)

Proving termination of rewriting for _3_53b:

-> Dependency pairs:
nF_f(0,1,x) -> nF_f(s(x),x,x)
nF_f(x,y,s(z)) -> nF_f(0,1,z)

-> Proof of termination for _3_53b_1:
-> -> Dependency pairs in cycle:
nF_f(0,1,x) -> nF_f(s(x),x,x)
nF_f(x,y,s(z)) -> nF_f(0,1,z)

Termination proved: Cycles verify subterm criterion.

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.