NO
(ignored inputs)COMMENT reduction failed
Rewrite Rules:
   [ +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(p(?x),?y) -> p(+(?y,?x)),
     p(s(?x)) -> s(p(?x)),
     s(p(?x)) -> ?x ]
Apply Direct Methods...
Inner CPs:
   [ +(?x_4,?y_1) = s(+(p(?x_4),?y_1)),
     +(s(p(?x_3)),?y_2) = p(+(?y_2,s(?x_3))),
     p(?x_4) = s(p(p(?x_4))),
     s(s(p(?x_3))) = s(?x_3) ]
Outer CPs:
   [  ]
not Overlay, check Termination...
Terminating, not WCR
Knuth & Bendix
Direct Methods: not CR

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