YES
(ignored inputs)COMMENT reduction failed
Rewrite Rules:
   [ s(p(?x)) -> ?x,
     p(s(?x)) -> ?x,
     +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     +(?x,p(?y)) -> p(+(?x,?y)),
     +(0,?y) -> ?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_3,?x) = s(+(?x_3,p(?x))),
     +(?x_4,?x_1) = p(+(?x_4,s(?x_1))),
     +(?x_1,?y_6) = p(+(s(?x_1),?y_6)),
     +(?x,?y_7) = s(+(p(?x),?y_7)) ]
Outer CPs:
   [ 0 = 0,
     p(?x_6) = p(+(?x_6,0)),
     s(?x_7) = s(+(?x_7,0)),
     s(+(0,?y_3)) = s(?y_3),
     s(+(p(?x_6),?y_3)) = p(+(?x_6,s(?y_3))),
     s(+(s(?x_7),?y_3)) = s(+(?x_7,s(?y_3))),
     p(+(0,?y_4)) = p(?y_4),
     p(+(p(?x_6),?y_4)) = p(+(?x_6,p(?y_4))),
     p(+(s(?x_7),?y_4)) = s(+(?x_7,p(?y_4))) ]
not Overlay, check Termination...
Terminating, WCR
Knuth & Bendix
Direct Methods: CR

Combined result: CR
/tmp/file6MVqfZ.trs: Success(CR)
(9 msec.)