YES
(ignored inputs)COMMENT the following rules are removed from the original TRS - ( 0 ( ) , 0 ( ) ) -> 0 ( ) - ( s ( x ) , 0 ( ) ) -> s ( x )
Rewrite Rules:
   [ -(?x,s(?y)) -> -(d(?x),?y),
     d(s(?x)) -> ?x,
     -(s(?x),s(?y)) -> -(?x,?y),
     -(d(?x),?y) -> -(?x,s(?y)) ]
Apply Direct Methods...
Inner CPs:
   [ -(?x_1,?y_3) = -(s(?x_1),s(?y_3)) ]
Outer CPs:
   [ -(d(s(?x_2)),?y) = -(?x_2,?y),
     -(d(d(?x_3)),?y) = -(?x_3,s(s(?y))) ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth & Bendix
Linear
unknown Development Closed
Strongly Closed
Direct Methods: CR

Combined result: CR
/tmp/filepHeMga.trs: Success(CR)
(18 msec.)