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(?y),?x), +(?x,+(?y,?z)) -> +(+(?x,?y),?z), +(?x,?y) -> +(?y,?x), dbl(?x) -> +(?x,?x), dbl(+(?x,?y)) -> +(dbl(?x),dbl(?y)) ] 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(?y_3),?x_3)) = +(+(?x_4,?x_3),s(?y_3)), +(?x_4,+(?y_5,?x_5)) = +(+(?x_4,?x_5),?y_5), dbl(?y) = +(dbl(0),dbl(?y)), dbl(?x_1) = +(dbl(?x_1),dbl(0)), dbl(s(+(?x_2,?y_2))) = +(dbl(s(?x_2)),dbl(?y_2)), dbl(+(s(?y_3),?x_3)) = +(dbl(?x_3),dbl(s(?y_3))), dbl(+(+(?x_4,?y_4),?z_4)) = +(dbl(?x_4),dbl(+(?y_4,?z_4))), dbl(+(?y_5,?x_5)) = +(dbl(?x_5),dbl(?y_5)), +(?x_1,+(+(?x,?y),?z)) = +(+(?x_1,?x),+(?y,?z)) ] Outer CPs: [ 0 = 0, s(?y_3) = +(s(?y_3),0), +(?y_4,?z_4) = +(+(0,?y_4),?z_4), ?y = +(?y,0), s(?x_2) = s(+(?x_2,0)), ?x_1 = +(0,?x_1), s(+(?x_2,s(?y_3))) = +(s(?y_3),s(?x_2)), s(+(?x_2,+(?y_4,?z_4))) = +(+(s(?x_2),?y_4),?z_4), s(+(?x_2,?y_2)) = +(?y_2,s(?x_2)), +(s(?y_3),?x_3) = +(s(?y_3),?x_3), +(+(?x_4,?y_4),?z_4) = +(+(?y_4,?z_4),?x_4), +(+(?x_7,?y_7),+(?x_7,?y_7)) = +(dbl(?x_7),dbl(?y_7)) ] Left-Linear, not Right-Linear (inner) Parallel CPs: (not computed) unknown Toyama (Parallel CPs) Direct Methods: Can't judge Combined result: Can't judge 171.trs: Failure(unknown CR) (0 msec.)