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

Combined result: CR
/tmp/filehv97n8.trs: Success(CR)
(12 msec.)