NO
(ignored inputs)COMMENT experiments for [125] submitted by: Takahito Aoto
Rewrite Rules:
   [ plus(0,?y) -> ?y,
     plus(s(?x),?y) -> s(plus(?x,?y)),
     qplus(0,?y) -> ?y,
     qplus(s(?x),?y) -> qplus(?x,s(?y)),
     plus(?x,?y) -> qplus(?x,?y) ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [ ?y = qplus(0,?y),
     s(plus(?x_1,?y_1)) = qplus(s(?x_1),?y_1) ]
Overlay, check Innermost Termination...
Innermost Terminating (hence Terminating), not WCR
Knuth & Bendix
Direct Methods: not CR

Combined result: not CR
635.trs: Success(not CR)
(6 msec.)