YES
(ignored inputs)COMMENT the following rules are removed from the original TRS + ( 0 ( ) , y ) -> y
Rewrite Rules:
   [ +(s(?x),?y) -> s(+(?x,?y)),
     s(s(?x)) -> ?x ]
Apply Direct Methods...
Inner CPs:
   [ +(?x_1,?y) = s(+(s(?x_1),?y)),
     s(?x) = s(?x) ]
Outer CPs:
   [  ]
not Overlay, check Termination...
Terminating, WCR
Knuth & Bendix
Direct Methods: CR

Combined result: CR
/tmp/fileBdg6oN.trs: Success(CR)
(4 msec.)