MAYBE (ignored inputs)COMMENT full experiments for [35] submitted by: Takahito Aoto and Yoshihito Toyama Rewrite Rules: [ +(0,?y) -> ?y, +(?x,0) -> ?x, +(s(?x),?y) -> s(+(?x,?y)), +(?x,s(?y)) -> s(+(?x,?y)), +(?x,+(?y,?z)) -> +(+(?x,?y),?z), +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ] Apply Direct Methods... Inner CPs: [ +(?x_4,?y) = +(+(?x_4,0),?y), +(?x_4,?x_1) = +(+(?x_4,?x_1),0), +(?x_4,s(+(?x_2,?y_2))) = +(+(?x_4,s(?x_2)),?y_2), +(?x_4,s(+(?x_3,?y_3))) = +(+(?x_4,?x_3),s(?y_3)), +(?x_4,+(?x_5,+(?y_5,?z_5))) = +(+(?x_4,+(?x_5,?y_5)),?z_5), +(?y,?z_5) = +(0,+(?y,?z_5)), +(?x_1,?z_5) = +(?x_1,+(0,?z_5)), +(s(+(?x_2,?y_2)),?z_5) = +(s(?x_2),+(?y_2,?z_5)), +(s(+(?x_3,?y_3)),?z_5) = +(?x_3,+(s(?y_3),?z_5)), +(+(+(?x_4,?y_4),?z_4),?z_5) = +(?x_4,+(+(?y_4,?z_4),?z_5)), +(?x_1,+(+(?x,?y),?z)) = +(+(?x_1,?x),+(?y,?z)), +(+(?x,+(?y,?z)),?z_1) = +(+(?x,?y),+(?z,?z_1)) ] Outer CPs: [ 0 = 0, s(?y_3) = s(+(0,?y_3)), +(?y_4,?z_4) = +(+(0,?y_4),?z_4), s(?x_2) = s(+(?x_2,0)), +(?x_5,?y_5) = +(?x_5,+(?y_5,0)), s(+(?x_2,s(?y_3))) = s(+(s(?x_2),?y_3)), s(+(?x_2,+(?y_4,?z_4))) = +(+(s(?x_2),?y_4),?z_4), s(+(+(?x_5,?y_5),?y_3)) = +(?x_5,+(?y_5,s(?y_3))), +(+(+(?x_5,?y_5),?y_4),?z_4) = +(?x_5,+(?y_5,+(?y_4,?z_4))) ] Linear (inner) Parallel CPs: (not computed) unknown Toyama (Parallel CPs) Direct Methods: Can't judge Combined result: Can't judge 138.trs: Failure(unknown CR) (0 msec.)