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

Proving termination of rewriting for 9:

-> Dependency pairs:
nF_a(x,y) -> nF_b(x,b(0,c(y)))
nF_a(x,y) -> nF_b(0,c(y))
nF_a(x,y) -> nF_c(y)
nF_c(b(y,c(x))) -> nF_c(c(b(a(0,0),y)))
nF_c(b(y,c(x))) -> nF_c(b(a(0,0),y))
nF_c(b(y,c(x))) -> nF_b(a(0,0),y)
nF_c(b(y,c(x))) -> nF_a(0,0)

-> Dependency pairs narrowed: 
nF_c(b(y,c(x))) -> nF_c(c(b(a(0,0),y)))

-> New dependency pairs: 
nF_c(b(c(x),c(x))) -> nF_c(c(c(b(a(0,0),a(0,0)))))

-> Proof of termination for 9_1:
-> -> Dependency pairs in cycle:
nF_a(x,y) -> nF_c(y)
nF_c(b(y,c(x))) -> nF_a(0,0)
nF_c(b(c(x),c(x))) -> nF_c(c(c(b(a(0,0),a(0,0)))))
nF_c(b(y,c(x))) -> nF_c(b(a(0,0),y))

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

Polynomial Interpretation:

[a](X1,X2) = 2.X1 + 1/2
[b](X1,X2) = X1 + 1/2.X2
[0] = 0
[c](X) = 2
[nF_a](X1,X2) = 2.X2
[nF_c](X) = 2.X

TIME: 0.203033

-> -> Dependency pairs in cycle:
nF_a(x,y) -> nF_c(y)
nF_c(b(y,c(x))) -> nF_a(0,0)
nF_c(b(c(x),c(x))) -> nF_c(c(c(b(a(0,0),a(0,0)))))

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

Polynomial Interpretation:

[a](X1,X2) = 2.X1 + 2
[b](X1,X2) = 2.X1 + 2
[0] = 0
[c](X) = 0
[nF_a](X1,X2) = 2.X2
[nF_c](X) = 2.X

TIME: 2.952e-3

-> -> Dependency pairs in cycle:
nF_a(x,y) -> nF_c(y)
nF_c(b(y,c(x))) -> nF_a(0,0)

There are no usable rules.

Polynomial Interpretation:

[a](X1,X2) = 0
[b](X1,X2) = 2.X2
[0] = 0
[c](X) = 2
[nF_a](X1,X2) = 2.X2
[nF_c](X) = 2.X

TIME: 1.45e-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.