MAYBE
(ignored inputs)COMMENT doi:10.1016/j.jsc.2004.02.003 [116] p. 890 ( R_+ union R_int ) submitted by: Aart Middeldorp
Rewrite Rules:
   [ 0(sharp) -> sharp,
     +(?x,sharp) -> ?x,
     +(0(?x),0(?y)) -> 0(+(?x,?y)),
     +(0(?x),1(?y)) -> 1(+(?x,?y)),
     +(1(?x),1(?y)) -> j(+(?x,+(?y,1(sharp)))),
     +(0(?x),j(?y)) -> j(+(?x,?y)),
     +(j(?x),1(?y)) -> 0(+(?x,?y)),
     +(j(?x),j(?y)) -> 1(+(?x,+(?y,j(sharp)))),
     +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x) ]
Apply Direct Methods...
Inner CPs:
   [ +(sharp,0(?y_1)) = 0(+(sharp,?y_1)),
     +(0(?x_1),sharp) = 0(+(?x_1,sharp)),
     +(sharp,1(?y_2)) = 1(+(sharp,?y_2)),
     +(sharp,j(?y_4)) = j(+(sharp,?y_4)),
     +(?x_7,?x) = +(+(?x_7,?x),sharp),
     +(?x_7,0(+(?x_1,?y_1))) = +(+(?x_7,0(?x_1)),0(?y_1)),
     +(?x_7,1(+(?x_2,?y_2))) = +(+(?x_7,0(?x_2)),1(?y_2)),
     +(?x_7,j(+(?x_3,+(?y_3,1(sharp))))) = +(+(?x_7,1(?x_3)),1(?y_3)),
     +(?x_7,j(+(?x_4,?y_4))) = +(+(?x_7,0(?x_4)),j(?y_4)),
     +(?x_7,0(+(?x_5,?y_5))) = +(+(?x_7,j(?x_5)),1(?y_5)),
     +(?x_7,1(+(?x_6,+(?y_6,j(sharp))))) = +(+(?x_7,j(?x_6)),j(?y_6)),
     +(?x_7,+(?x_8,+(?y_8,?z_8))) = +(+(?x_7,+(?x_8,?y_8)),?z_8),
     +(?x_7,+(?y_9,?x_9)) = +(+(?x_7,?x_9),?y_9),
     +(?x,?z_8) = +(?x,+(sharp,?z_8)),
     +(0(+(?x_1,?y_1)),?z_8) = +(0(?x_1),+(0(?y_1),?z_8)),
     +(1(+(?x_2,?y_2)),?z_8) = +(0(?x_2),+(1(?y_2),?z_8)),
     +(j(+(?x_3,+(?y_3,1(sharp)))),?z_8) = +(1(?x_3),+(1(?y_3),?z_8)),
     +(j(+(?x_4,?y_4)),?z_8) = +(0(?x_4),+(j(?y_4),?z_8)),
     +(0(+(?x_5,?y_5)),?z_8) = +(j(?x_5),+(1(?y_5),?z_8)),
     +(1(+(?x_6,+(?y_6,j(sharp)))),?z_8) = +(j(?x_6),+(j(?y_6),?z_8)),
     +(+(+(?x_7,?y_7),?z_7),?z_8) = +(?x_7,+(+(?y_7,?z_7),?z_8)),
     +(+(?y_9,?x_9),?z_8) = +(?x_9,+(?y_9,?z_8)),
     +(?x_1,+(+(?x,?y),?z)) = +(+(?x_1,?x),+(?y,?z)),
     +(+(?x,+(?y,?z)),?z_1) = +(+(?x,?y),+(?z,?z_1)) ]
Outer CPs:
   [ +(?x_8,?y_8) = +(?x_8,+(?y_8,sharp)),
     ?x = +(sharp,?x),
     0(+(?x_1,?y_1)) = +(0(?y_1),0(?x_1)),
     1(+(?x_2,?y_2)) = +(1(?y_2),0(?x_2)),
     j(+(?x_3,+(?y_3,1(sharp)))) = +(1(?y_3),1(?x_3)),
     j(+(?x_4,?y_4)) = +(j(?y_4),0(?x_4)),
     0(+(?x_5,?y_5)) = +(1(?y_5),j(?x_5)),
     1(+(?x_6,+(?y_6,j(sharp)))) = +(j(?y_6),j(?x_6)),
     +(+(+(?x_8,?y_8),?y_7),?z_7) = +(?x_8,+(?y_8,+(?y_7,?z_7))),
     +(+(?x_7,?y_7),?z_7) = +(+(?y_7,?z_7),?x_7),
     +(?x_8,+(?y_8,?z_8)) = +(?z_8,+(?x_8,?y_8)) ]
Linear
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Direct Methods: Can't judge

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