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