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)),
     +(?x,p(?y)) -> p(+(?x,?y)),
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     +(p(?x),?y) -> p(+(?x,?y)),
     s(p(?x)) -> ?x,
     p(s(?x)) -> ?x,
     -(0) -> 0,
     -(s(?x)) -> p(-(?x)),
     -(p(?x)) -> s(-(?x)),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     -(+(?x,?y)) -> +(-(?x),-(?y)) ]
Apply Direct Methods...
Inner CPs:
   [ +(?x_1,?x_6) = s(+(?x_1,p(?x_6))),
     +(?x_2,?x_7) = p(+(?x_2,s(?x_7))),
     +(?x_6,?y_4) = s(+(p(?x_6),?y_4)),
     +(?x_7,?y_5) = p(+(s(?x_7),?y_5)),
     s(?x_7) = s(?x_7),
     p(?x_6) = p(?x_6),
     -(?x_6) = p(-(p(?x_6))),
     -(?x_7) = s(-(s(?x_7))),
     +(?x,?z_10) = +(?x,+(0,?z_10)),
     +(s(+(?x_1,?y_1)),?z_10) = +(?x_1,+(s(?y_1),?z_10)),
     +(p(+(?x_2,?y_2)),?z_10) = +(?x_2,+(p(?y_2),?z_10)),
     +(?y_3,?z_10) = +(0,+(?y_3,?z_10)),
     +(s(+(?x_4,?y_4)),?z_10) = +(s(?x_4),+(?y_4,?z_10)),
     +(p(+(?x_5,?y_5)),?z_10) = +(p(?x_5),+(?y_5,?z_10)),
     +(+(+(?x_11,?y_11),?z_11),?z_10) = +(?x_11,+(+(?y_11,?z_11),?z_10)),
     +(?x_11,?x) = +(+(?x_11,?x),0),
     +(?x_11,s(+(?x_1,?y_1))) = +(+(?x_11,?x_1),s(?y_1)),
     +(?x_11,p(+(?x_2,?y_2))) = +(+(?x_11,?x_2),p(?y_2)),
     +(?x_11,?y_3) = +(+(?x_11,0),?y_3),
     +(?x_11,s(+(?x_4,?y_4))) = +(+(?x_11,s(?x_4)),?y_4),
     +(?x_11,p(+(?x_5,?y_5))) = +(+(?x_11,p(?x_5)),?y_5),
     +(?x_11,+(?x_10,+(?y_10,?z_10))) = +(+(?x_11,+(?x_10,?y_10)),?z_10),
     -(?x) = +(-(?x),-(0)),
     -(s(+(?x_1,?y_1))) = +(-(?x_1),-(s(?y_1))),
     -(p(+(?x_2,?y_2))) = +(-(?x_2),-(p(?y_2))),
     -(?y_3) = +(-(0),-(?y_3)),
     -(s(+(?x_4,?y_4))) = +(-(s(?x_4)),-(?y_4)),
     -(p(+(?x_5,?y_5))) = +(-(p(?x_5)),-(?y_5)),
     -(+(?x_10,+(?y_10,?z_10))) = +(-(+(?x_10,?y_10)),-(?z_10)),
     -(+(+(?x_11,?y_11),?z_11)) = +(-(?x_11),-(+(?y_11,?z_11))),
     +(+(?x,+(?y,?z)),?z_1) = +(+(?x,?y),+(?z,?z_1)),
     +(?x_1,+(+(?x,?y),?z)) = +(+(?x_1,?x),+(?y,?z)) ]
Outer CPs:
   [ 0 = 0,
     s(?x_4) = s(+(?x_4,0)),
     p(?x_5) = p(+(?x_5,0)),
     +(?x_10,?y_10) = +(?x_10,+(?y_10,0)),
     s(+(0,?y_1)) = s(?y_1),
     s(+(s(?x_4),?y_1)) = s(+(?x_4,s(?y_1))),
     s(+(p(?x_5),?y_1)) = p(+(?x_5,s(?y_1))),
     s(+(+(?x_10,?y_10),?y_1)) = +(?x_10,+(?y_10,s(?y_1))),
     p(+(0,?y_2)) = p(?y_2),
     p(+(s(?x_4),?y_2)) = s(+(?x_4,p(?y_2))),
     p(+(p(?x_5),?y_2)) = p(+(?x_5,p(?y_2))),
     p(+(+(?x_10,?y_10),?y_2)) = +(?x_10,+(?y_10,p(?y_2))),
     +(?y_11,?z_11) = +(+(0,?y_11),?z_11),
     s(+(?x_4,+(?y_11,?z_11))) = +(+(s(?x_4),?y_11),?z_11),
     p(+(?x_5,+(?y_11,?z_11))) = +(+(p(?x_5),?y_11),?z_11),
     +(?x_10,+(?y_10,+(?y_11,?z_11))) = +(+(+(?x_10,?y_10),?y_11),?z_11) ]
Linear
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Direct Methods: Can't judge

Combined result: Can't judge
152.trs: Failure(unknown CR)
(1 msec.)