YES
(ignored inputs)COMMENT from the collection of \cite{AT2012}
Rewrite Rules:
   [ +(0,?y) -> ?y,
     +(?x,0) -> ?x,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(?x,s(?y)) -> s(+(?x,?y)),
     +(?x,?y) -> +(?y,?x) ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [ 0 = 0,
     s(?y_3) = s(+(0,?y_3)),
     ?y = +(?y,0),
     s(?x_2) = s(+(?x_2,0)),
     ?x_1 = +(0,?x_1),
     s(+(?x_2,s(?y_3))) = s(+(s(?x_2),?y_3)),
     s(+(?x_2,?y_2)) = +(?y_2,s(?x_2)),
     s(+(?x_3,?y_3)) = +(s(?y_3),?x_3) ]
Overlay, check Innermost Termination...
unknown Innermost Terminating
unknown Knuth & Bendix
Linear
Development Closed
Direct Methods: CR

Final result: CR
158.trs: Success(CR)
(0 msec.)