YES
(VAR X Y Z X1 X2 X3 X4)
(RULES 
plus(s(X),plus(Y,Z)) -> plus(X,plus(s(s(Y)),Z))
plus(s(X1),plus(X2,plus(X3,X4))) -> plus(X1,plus(X3,plus(X2,X4)))
)

Proving termination of rewriting for bn129:

-> Dependency pairs:
nF_plus(s(X),plus(Y,Z)) -> nF_plus(X,plus(s(s(Y)),Z))
nF_plus(s(X),plus(Y,Z)) -> nF_plus(s(s(Y)),Z)
nF_plus(s(X1),plus(X2,plus(X3,X4))) -> nF_plus(X1,plus(X3,plus(X2,X4)))
nF_plus(s(X1),plus(X2,plus(X3,X4))) -> nF_plus(X3,plus(X2,X4))
nF_plus(s(X1),plus(X2,plus(X3,X4))) -> nF_plus(X2,X4)

-> Proof of termination for bn129_1:
-> -> Dependency pairs in cycle:
nF_plus(s(X),plus(Y,Z)) -> nF_plus(X,plus(s(s(Y)),Z))
nF_plus(s(X1),plus(X2,plus(X3,X4))) -> nF_plus(X2,X4)
nF_plus(s(X1),plus(X2,plus(X3,X4))) -> nF_plus(X3,plus(X2,X4))
nF_plus(s(X1),plus(X2,plus(X3,X4))) -> nF_plus(X1,plus(X3,plus(X2,X4)))
nF_plus(s(X),plus(Y,Z)) -> nF_plus(s(s(Y)),Z)

UsableRules:
plus(s(X),plus(Y,Z)) -> plus(X,plus(s(s(Y)),Z))
plus(s(X1),plus(X2,plus(X3,X4))) -> plus(X1,plus(X3,plus(X2,X4)))

Polynomial Interpretation:

[plus](X1,X2) = X2 + 1
[s](X) = 0
[nF_plus](X1,X2) = X2

TIME: 4.7624e-2

-> -> Dependency pairs in cycle:
nF_plus(s(X),plus(Y,Z)) -> nF_plus(X,plus(s(s(Y)),Z))
nF_plus(s(X1),plus(X2,plus(X3,X4))) -> nF_plus(X1,plus(X3,plus(X2,X4)))
nF_plus(s(X1),plus(X2,plus(X3,X4))) -> nF_plus(X3,plus(X2,X4))
nF_plus(s(X1),plus(X2,plus(X3,X4))) -> nF_plus(X2,X4)

UsableRules:
plus(s(X),plus(Y,Z)) -> plus(X,plus(s(s(Y)),Z))
plus(s(X1),plus(X2,plus(X3,X4))) -> plus(X1,plus(X3,plus(X2,X4)))

Polynomial Interpretation:

[plus](X1,X2) = X2 + 1
[s](X) = 0
[nF_plus](X1,X2) = X2

TIME: 4.7358e-2

-> -> Dependency pairs in cycle:
nF_plus(s(X),plus(Y,Z)) -> nF_plus(X,plus(s(s(Y)),Z))
nF_plus(s(X1),plus(X2,plus(X3,X4))) -> nF_plus(X3,plus(X2,X4))
nF_plus(s(X1),plus(X2,plus(X3,X4))) -> nF_plus(X1,plus(X3,plus(X2,X4)))

UsableRules:
plus(s(X),plus(Y,Z)) -> plus(X,plus(s(s(Y)),Z))
plus(s(X1),plus(X2,plus(X3,X4))) -> plus(X1,plus(X3,plus(X2,X4)))

Polynomial Interpretation:

[plus](X1,X2) = X2 + 1
[s](X) = 0
[nF_plus](X1,X2) = X2

TIME: 4.6687000000000034e-2

-> -> Dependency pairs in cycle:
nF_plus(s(X),plus(Y,Z)) -> nF_plus(X,plus(s(s(Y)),Z))
nF_plus(s(X1),plus(X2,plus(X3,X4))) -> nF_plus(X1,plus(X3,plus(X2,X4)))

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.