(ignored inputs)COMMENT experiments for [36] submitted by: Takahito Aoto
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,0) -> 0,
     -(?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_3,?x) = s(+(?x_3,p(?x))),
     +(?x_4,?x_1) = p(+(?x_4,s(?x_1))),
     -(?x_5,?x) = p(-(?x_5,p(?x))),
     -(?x_6,?x_1) = s(-(?x_6,s(?x_1))),
     -(?x_1,?y_7) = p(-(s(?x_1),?y_7)),
     -(?x,?y_8) = s(-(p(?x),?y_8)) ]
Outer CPs:
   [ p(-(p(?x_7),?y_5)) = p(-(?x_7,s(?y_5))),
     p(-(s(?x_8),?y_5)) = s(-(?x_8,s(?y_5))),
     s(-(p(?x_7),?y_6)) = p(-(?x_7,p(?y_6))),
     s(-(s(?x_8),?y_6)) = s(-(?x_8,p(?y_6))) ]
not Overlay, check Termination...
Terminating, WCR
Knuth & Bendix
Direct Methods: CR

Combined result: CR
578.trs: Success(CR)
YES
(14 msec.)