(ignored inputs)COMMENT doi:10.1007/3-540-56610-4_55 [123] Example 7.1 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)),
     -(?x,0) -> ?x,
     -(?x,s(?y)) -> p(-(?x,?y)),
     -(?x,p(?y)) -> s(-(?x,?y)),
     *(?x,0) -> 0,
     *(?x,s(?y)) -> +(*(?x,?y),?x),
     *(?x,p(?y)) -> -(*(?x,?y),?x) ]
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_6,?x) = p(-(?x_6,p(?x))),
     -(?x_7,?x_1) = s(-(?x_7,s(?x_1))),
     *(?x_9,?x) = +(*(?x_9,p(?x)),?x_9),
     *(?x_10,?x_1) = -(*(?x_10,s(?x_1)),?x_10) ]
Outer CPs:
   [  ]
not Overlay, check Termination...
Terminating, not WCR
Knuth & Bendix
Direct Methods: not CR

Combined result: not CR
569.trs: Success(not CR)
NO
(15 msec.)