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

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