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) -> +(?y,?x),
     -(+(?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) = +(-(?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)),
     -(+(?y_10,?x_10)) = +(-(?x_10),-(?y_10)) ]
Outer CPs:
   [ 0 = 0,
     s(?x_4) = s(+(?x_4,0)),
     p(?x_5) = p(+(?x_5,0)),
     ?x = +(0,?x),
     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_1,?y_1)) = +(s(?y_1),?x_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_2,?y_2)) = +(p(?y_2),?x_2),
     ?y_3 = +(?y_3,0),
     s(+(?x_4,?y_4)) = +(?y_4,s(?x_4)),
     p(+(?x_5,?y_5)) = +(?y_5,p(?x_5)) ]
Linear
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Direct Methods: Can't judge

Combined result: Can't judge
154.trs: Failure(unknown CR)
(0 msec.)