MAYBE
(ignored inputs)COMMENT [16] Example 1 submitted by: Takahito Aoto , Junichi Yoshida , and Yoshihito Toyama
Rewrite Rules:
   [ +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x),
     +(s(?x),?y) -> +(?x,s(?y)),
     +(?x,s(?y)) -> +(s(?x),?y),
     *(?x,s(?y)) -> +(?x,*(?x,?y)),
     *(s(?x),?y) -> +(*(?x,?y),?y),
     *(?x,?y) -> *(?y,?x),
     sq(?x) -> *(?x,?x),
     sq(s(?x)) -> +(*(?x,?x),s(+(?x,?x))) ]
Apply Direct Methods...
Inner CPs:
   [ +(?x,+(?x_1,+(?y_1,?z_1))) = +(+(?x,+(?x_1,?y_1)),?z_1),
     +(?x,+(?y_2,?x_2)) = +(+(?x,?x_2),?y_2),
     +(?x,+(?x_3,s(?y_3))) = +(+(?x,s(?x_3)),?y_3),
     +(?x,+(s(?x_4),?y_4)) = +(+(?x,?x_4),s(?y_4)),
     +(+(+(?x,?y),?z),?z_1) = +(?x,+(+(?y,?z),?z_1)),
     +(+(?y_2,?x_2),?z_1) = +(?x_2,+(?y_2,?z_1)),
     +(+(?x_3,s(?y_3)),?z_1) = +(s(?x_3),+(?y_3,?z_1)),
     +(+(s(?x_4),?y_4),?z_1) = +(?x_4,+(s(?y_4),?z_1)),
     +(?x_1,+(+(?x,?y),?z)) = +(+(?x_1,?x),+(?y,?z)),
     +(+(?x,+(?y,?z)),?z_1) = +(+(?x,?y),+(?z,?z_1)) ]
Outer CPs:
   [ +(+(+(?x_1,?y_1),?y),?z) = +(?x_1,+(?y_1,+(?y,?z))),
     +(+(?x,?y),?z) = +(+(?y,?z),?x),
     +(+(s(?x_3),?y),?z) = +(?x_3,s(+(?y,?z))),
     +(?x_1,+(?y_1,?z_1)) = +(?z_1,+(?x_1,?y_1)),
     +(?x_1,+(?y_1,s(?y_4))) = +(s(+(?x_1,?y_1)),?y_4),
     +(?y_2,s(?x_3)) = +(?x_3,s(?y_2)),
     +(s(?y_4),?x_2) = +(s(?x_2),?y_4),
     +(?x_3,s(s(?y_4))) = +(s(s(?x_3)),?y_4),
     +(s(?x_6),*(s(?x_6),?y_5)) = +(*(?x_6,s(?y_5)),s(?y_5)),
     +(?x_5,*(?x_5,?y_5)) = *(s(?y_5),?x_5),
     +(*(?x_6,?y_6),?y_6) = *(?y_6,s(?x_6)),
     *(s(?x_9),s(?x_9)) = +(*(?x_9,?x_9),s(+(?x_9,?x_9))) ]
Left-Linear, not Right-Linear
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Direct Methods: Can't judge

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