YES
(ignored inputs)COMMENT the following rules are removed from the original TRS sq ( x ) -> * ( x , x ) sq ( s ( x ) ) -> + ( * ( x , x ) , s ( + ( x , x ) ) )
Rewrite Rules:
   [ *(?x,?y) -> *(?y,?x),
     +(?x,?y) -> +(?y,?x),
     +(s(?x),?y) -> +(?x,s(?y)),
     +(?x,s(?y)) -> +(s(?x),?y),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     *(?x,s(?y)) -> +(?x,*(?x,?y)),
     *(s(?x),?y) -> +(*(?x,?y),?y) ]
Apply Direct Methods...
Inner CPs:
   [ +(+(?y_1,?x_1),?z_4) = +(?x_1,+(?y_1,?z_4)),
     +(+(?x_2,s(?y_2)),?z_4) = +(s(?x_2),+(?y_2,?z_4)),
     +(+(s(?x_3),?y_3),?z_4) = +(?x_3,+(s(?y_3),?z_4)),
     +(+(+(?x_5,?y_5),?z_5),?z_4) = +(?x_5,+(+(?y_5,?z_5),?z_4)),
     +(?x_5,+(?y_1,?x_1)) = +(+(?x_5,?x_1),?y_1),
     +(?x_5,+(?x_2,s(?y_2))) = +(+(?x_5,s(?x_2)),?y_2),
     +(?x_5,+(s(?x_3),?y_3)) = +(+(?x_5,?x_3),s(?y_3)),
     +(?x_5,+(?x_4,+(?y_4,?z_4))) = +(+(?x_5,+(?x_4,?y_4)),?z_4),
     +(+(?x,+(?y,?z)),?z_1) = +(+(?x,?y),+(?z,?z_1)),
     +(?x_1,+(+(?x,?y),?z)) = +(+(?x_1,?x),+(?y,?z)) ]
Outer CPs:
   [ *(s(?y_6),?x) = +(?x,*(?x,?y_6)),
     *(?y,s(?x_7)) = +(*(?x_7,?y),?y),
     +(?y_1,s(?x_2)) = +(?x_2,s(?y_1)),
     +(s(?y_3),?x_1) = +(s(?x_1),?y_3),
     +(?y_1,+(?x_4,?y_4)) = +(?x_4,+(?y_4,?y_1)),
     +(+(?y_5,?z_5),?x_1) = +(+(?x_1,?y_5),?z_5),
     +(?x_2,s(s(?y_3))) = +(s(s(?x_2)),?y_3),
     +(?x_2,s(+(?y_5,?z_5))) = +(+(s(?x_2),?y_5),?z_5),
     +(s(+(?x_4,?y_4)),?y_3) = +(?x_4,+(?y_4,s(?y_3))),
     +(?x_4,+(?y_4,+(?y_5,?z_5))) = +(+(+(?x_4,?y_4),?y_5),?z_5),
     +(s(?x_7),*(s(?x_7),?y_6)) = +(*(?x_7,s(?y_6)),s(?y_6)) ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth & Bendix
Left-Linear, not Right-Linear
unknown Development Closed
unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
   [ +(?x,*(?x,?y_6)) = *(s(?y_6),?x),
     +(*(?x_7,?y),?y) = *(?y,s(?x_7)),
     +(?x_2,s(?y)) = +(?y,s(?x_2)),
     +(s(?x),?y_3) = +(s(?y_3),?x),
     +(?x_4,+(?y_4,?y)) = +(?y,+(?x_4,?y_4)),
     +(+(?x,?y_5),?z_5) = +(+(?y_5,?z_5),?x),
     +(?x,+(?y,?z_5)) = +(+(?y,?x),?z_5),
     +(+(?x_6,?x),?y) = +(?x_6,+(?y,?x)),
     +(s(s(?x)),?y_3) = +(?x,s(s(?y_3))),
     +(+(s(?x),?y_5),?z_5) = +(?x,s(+(?y_5,?z_5))),
     +(s(?x),+(?y,?z_5)) = +(+(?x,s(?y)),?z_5),
     +(+(?x_6,s(?x)),?y) = +(?x_6,+(?x,s(?y))),
     +(?x_3,s(s(?y))) = +(s(s(?x_3)),?y),
     +(?x_4,+(?y_4,s(?y))) = +(s(+(?x_4,?y_4)),?y),
     +(?x,+(s(?y),?z_5)) = +(+(s(?x),?y),?z_5),
     +(+(?x_6,?x),s(?y)) = +(?x_6,+(s(?x),?y)),
     +(?z,+(?x_1,+(?y_1,?y))) = +(+(?x_1,?y_1),+(?y,?z)),
     +(?z,+(?y,?x)) = +(?x,+(?y,?z)),
     +(?z,+(?x_4,s(?y))) = +(s(?x_4),+(?y,?z)),
     +(?z,+(s(?x),?y_5)) = +(?x,+(s(?y_5),?z)),
     +(?z,+(+(?x,?y_6),?z_6)) = +(?x,+(+(?y_6,?z_6),?z)),
     +(s(+(?x_5,+(?y_5,?y))),?y_4) = +(+(?x_5,?y_5),+(?y,s(?y_4))),
     +(s(+(?y,?x)),?y_4) = +(?x,+(?y,s(?y_4))),
     +(s(+(?x_8,s(?y))),?y_4) = +(s(?x_8),+(?y,s(?y_4))),
     +(s(+(s(?x),?y_9)),?y_4) = +(?x,+(s(?y_9),s(?y_4))),
     +(s(+(+(?x,?y_10),?z_10)),?y_4) = +(?x,+(+(?y_10,?z_10),s(?y_4))),
     +(+(+(?x_6,+(?y_6,?y)),?y_5),?z_5) = +(+(?x_6,?y_6),+(?y,+(?y_5,?z_5))),
     +(+(+(?y,?x),?y_5),?z_5) = +(?x,+(?y,+(?y_5,?z_5))),
     +(+(+(?x_9,s(?y)),?y_5),?z_5) = +(s(?x_9),+(?y,+(?y_5,?z_5))),
     +(+(+(s(?x),?y_10),?y_5),?z_5) = +(?x,+(s(?y_10),+(?y_5,?z_5))),
     +(+(+(+(?x,?y_11),?z_11),?y_5),?z_5) = +(?x,+(+(?y_11,?z_11),+(?y_5,?z_5))),
     +(?z,+(?x,?y)) = +(?x,+(?y,?z)),
     +(s(+(?x,?y)),?y_4) = +(?x,+(?y,s(?y_4))),
     +(+(+(?x,?y),?y_5),?z_5) = +(?x,+(?y,+(?y_5,?z_5))),
     +(+(?x_1,+(?y_1,?y)),?z) = +(+(?x_1,?y_1),+(?y,?z)),
     +(+(?y,?x),?z) = +(?x,+(?y,?z)),
     +(+(?x_4,s(?y)),?z) = +(s(?x_4),+(?y,?z)),
     +(+(s(?x),?y_5),?z) = +(?x,+(s(?y_5),?z)),
     +(+(+(?x,?y_6),?z_6),?z) = +(?x,+(+(?y_6,?z_6),?z)),
     +(+(?x_2,+(?y_2,?y)),+(?z,?z_1)) = +(+(+(?x_2,?y_2),+(?y,?z)),?z_1),
     +(+(?y,?x),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
     +(+(?x_5,s(?y)),+(?z,?z_1)) = +(+(s(?x_5),+(?y,?z)),?z_1),
     +(+(s(?x),?y_6),+(?z,?z_1)) = +(+(?x,+(s(?y_6),?z)),?z_1),
     +(+(+(?x,?y_7),?z_7),+(?z,?z_1)) = +(+(?x,+(+(?y_7,?z_7),?z)),?z_1),
     +(+(?x_6,+(?x_7,+(?y_7,?y))),?z) = +(?x_6,+(+(?x_7,?y_7),+(?y,?z))),
     +(+(?x_6,+(?y,?x)),?z) = +(?x_6,+(?x,+(?y,?z))),
     +(+(?x_6,+(?x_10,s(?y))),?z) = +(?x_6,+(s(?x_10),+(?y,?z))),
     +(+(?x_6,+(s(?x),?y_11)),?z) = +(?x_6,+(?x,+(s(?y_11),?z))),
     +(+(?x_6,+(+(?x,?y_12),?z_12)),?z) = +(?x_6,+(?x,+(+(?y_12,?z_12),?z))),
     +(+(?x,?y),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
     +(+(?x_6,+(?x,?y)),?z) = +(?x_6,+(?x,+(?y,?z))),
     +(+(+(?y,?y_1),?z_1),?x) = +(+(?x,?y),+(?y_1,?z_1)),
     +(+(?z,?y),?x) = +(+(?x,?y),?z),
     +(+(?x_4,s(?z)),?x) = +(+(?x,s(?x_4)),?z),
     +(+(s(?y),?y_5),?x) = +(+(?x,?y),s(?y_5)),
     +(+(?x_6,+(?y_6,?z)),?x) = +(+(?x,+(?x_6,?y_6)),?z),
     +(?x_3,s(+(+(?y,?y_4),?z_4))) = +(+(s(?x_3),?y),+(?y_4,?z_4)),
     +(?x_3,s(+(?z,?y))) = +(+(s(?x_3),?y),?z),
     +(?x_3,s(+(?x_7,s(?z)))) = +(+(s(?x_3),s(?x_7)),?z),
     +(?x_3,s(+(s(?y),?y_8))) = +(+(s(?x_3),?y),s(?y_8)),
     +(?x_3,s(+(?x_9,+(?y_9,?z)))) = +(+(s(?x_3),+(?x_9,?y_9)),?z),
     +(?x_5,+(?y_5,+(+(?y,?y_6),?z_6))) = +(+(+(?x_5,?y_5),?y),+(?y_6,?z_6)),
     +(?x_5,+(?y_5,+(?z,?y))) = +(+(+(?x_5,?y_5),?y),?z),
     +(?x_5,+(?y_5,+(?x_9,s(?z)))) = +(+(+(?x_5,?y_5),s(?x_9)),?z),
     +(?x_5,+(?y_5,+(s(?y),?y_10))) = +(+(+(?x_5,?y_5),?y),s(?y_10)),
     +(?x_5,+(?y_5,+(?x_11,+(?y_11,?z)))) = +(+(+(?x_5,?y_5),+(?x_11,?y_11)),?z),
     +(+(?y,?z),?x) = +(+(?x,?y),?z),
     +(?x_3,s(+(?y,?z))) = +(+(s(?x_3),?y),?z),
     +(?x_5,+(?y_5,+(?y,?z))) = +(+(+(?x_5,?y_5),?y),?z),
     +(?x,+(+(?y,?y_1),?z_1)) = +(+(?x,?y),+(?y_1,?z_1)),
     +(?x,+(?z,?y)) = +(+(?x,?y),?z),
     +(?x,+(?x_4,s(?z))) = +(+(?x,s(?x_4)),?z),
     +(?x,+(s(?y),?y_5)) = +(+(?x,?y),s(?y_5)),
     +(?x,+(?x_6,+(?y_6,?z))) = +(+(?x,+(?x_6,?y_6)),?z),
     +(+(?x_1,?x),+(+(?y,?y_2),?z_2)) = +(?x_1,+(+(?x,?y),+(?y_2,?z_2))),
     +(+(?x_1,?x),+(?z,?y)) = +(?x_1,+(+(?x,?y),?z)),
     +(+(?x_1,?x),+(?x_5,s(?z))) = +(?x_1,+(+(?x,s(?x_5)),?z)),
     +(+(?x_1,?x),+(s(?y),?y_6)) = +(?x_1,+(+(?x,?y),s(?y_6))),
     +(+(?x_1,?x),+(?x_7,+(?y_7,?z))) = +(?x_1,+(+(?x,+(?x_7,?y_7)),?z)),
     +(?x,+(+(+(?y,?y_7),?z_7),?z_6)) = +(+(+(?x,?y),+(?y_7,?z_7)),?z_6),
     +(?x,+(+(?z,?y),?z_6)) = +(+(+(?x,?y),?z),?z_6),
     +(?x,+(+(?x_10,s(?z)),?z_6)) = +(+(+(?x,s(?x_10)),?z),?z_6),
     +(?x,+(+(s(?y),?y_11),?z_6)) = +(+(+(?x,?y),s(?y_11)),?z_6),
     +(?x,+(+(?x_12,+(?y_12,?z)),?z_6)) = +(+(+(?x,+(?x_12,?y_12)),?z),?z_6),
     +(+(?x_1,?x),+(?y,?z)) = +(?x_1,+(+(?x,?y),?z)),
     +(?x,+(+(?y,?z),?z_6)) = +(+(+(?x,?y),?z),?z_6),
     *(s(?y),?x) = +(?x,*(?x,?y)),
     +(*(?x_7,s(?y)),s(?y)) = +(s(?x_7),*(s(?x_7),?y)),
     *(?y,s(?x)) = +(*(?x,?y),?y),
     +(s(?x),*(s(?x),?y_7)) = +(*(?x,s(?y_7)),s(?y_7)) ]
unknown Okui (Simultaneous CPs)
unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
check Locally Decreasing Diagrams by Rule Labelling...
Critical Pair <+(+(?y_1,?x_1),?z_4), +(?x_1,+(?y_1,?z_4))> by Rules <1, 4> preceded by [(+,1)]
 joinable by a reduction of rules <[([(+,1)],1)], [([],5)]>
Critical Pair <+(+(?x_2,s(?y_2)),?z_4), +(s(?x_2),+(?y_2,?z_4))> by Rules <2, 4> preceded by [(+,1)]
 joinable by a reduction of rules <[([(+,1)],3)], [([],5)]>
Critical Pair <+(+(s(?x_3),?y_3),?z_4), +(?x_3,+(s(?y_3),?z_4))> by Rules <3, 4> preceded by [(+,1)]
 joinable by a reduction of rules <[([(+,1)],2)], [([],5)]>
Critical Pair <+(+(+(?x_5,?y_5),?z_5),?z_4), +(?x_5,+(+(?y_5,?z_5),?z_4))> by Rules <5, 4> preceded by [(+,1)]
 joinable by a reduction of rules <[([(+,1)],4)], [([],5)]>
Critical Pair <+(?x_5,+(?y_1,?x_1)), +(+(?x_5,?x_1),?y_1)> by Rules <1, 5> preceded by [(+,2)]
 joinable by a reduction of rules <[([(+,2)],1)], [([],4)]>
Critical Pair <+(?x_5,+(?x_2,s(?y_2))), +(+(?x_5,s(?x_2)),?y_2)> by Rules <2, 5> preceded by [(+,2)]
 joinable by a reduction of rules <[([(+,2)],3)], [([],4)]>
Critical Pair <+(?x_5,+(s(?x_3),?y_3)), +(+(?x_5,?x_3),s(?y_3))> by Rules <3, 5> preceded by [(+,2)]
 joinable by a reduction of rules <[([(+,2)],2)], [([],4)]>
Critical Pair <+(?x_5,+(?x_4,+(?y_4,?z_4))), +(+(?x_5,+(?x_4,?y_4)),?z_4)> by Rules <4, 5> preceded by [(+,2)]
 joinable by a reduction of rules <[([(+,2)],5)], [([],4)]>
Critical Pair <+(+(?x,+(?y,?z)),?z_1), +(+(?x,?y),+(?z,?z_1))> by Rules <4, 4> preceded by [(+,1)]
 joinable by a reduction of rules <[([(+,1)],5)], [([],5)]>
Critical Pair <+(?x_1,+(+(?x,?y),?z)), +(+(?x_1,?x),+(?y,?z))> by Rules <5, 5> preceded by [(+,2)]
 joinable by a reduction of rules <[([(+,2)],4)], [([],4)]>
Critical Pair <+(?x_6,*(?x_6,?y_6)), *(s(?y_6),?x_6)> by Rules <6, 0> preceded by []
 joinable by a reduction of rules <[([(+,2)],0),([],1)], [([],7)]>
 joinable by a reduction of rules <[([],1),([(+,1)],0)], [([],7)]>
 joinable by a reduction of rules <[], [([],0),([],6)]>
 joinable by a reduction of rules <[([(+,2)],0)], [([],7),([],1)]>
 joinable by a reduction of rules <[([],1)], [([],7),([(+,1)],0)]>
Critical Pair <+(*(?x_7,?y_7),?y_7), *(?y_7,s(?x_7))> by Rules <7, 0> preceded by []
 joinable by a reduction of rules <[([(+,1)],0),([],1)], [([],6)]>
 joinable by a reduction of rules <[([],1),([(+,2)],0)], [([],6)]>
 joinable by a reduction of rules <[], [([],0),([],7)]>
 joinable by a reduction of rules <[([(+,1)],0)], [([],6),([],1)]>
 joinable by a reduction of rules <[([],1)], [([],6),([(+,2)],0)]>
Critical Pair <+(?x_2,s(?y_2)), +(?y_2,s(?x_2))> by Rules <2, 1> preceded by []
 joinable by a reduction of rules <[([],3)], [([],1)]>
 joinable by a reduction of rules <[([],1)], [([],3)]>
Critical Pair <+(s(?x_3),?y_3), +(s(?y_3),?x_3)> by Rules <3, 1> preceded by []
 joinable by a reduction of rules <[([],2)], [([],1)]>
 joinable by a reduction of rules <[([],1)], [([],2)]>
Critical Pair <+(?x_4,+(?y_4,?z_4)), +(?z_4,+(?x_4,?y_4))> by Rules <4, 1> preceded by []
 joinable by a reduction of rules <[([],5)], [([],1)]>
Critical Pair <+(+(?x_5,?y_5),?z_5), +(+(?y_5,?z_5),?x_5)> by Rules <5, 1> preceded by []
 joinable by a reduction of rules <[([],4)], [([],1)]>
Critical Pair <+(s(s(?x_2)),?y_3), +(?x_2,s(s(?y_3)))> by Rules <3, 2> preceded by []
 joinable by a reduction of rules <[([],2)], [([],3)]>
Critical Pair <+(+(s(?x_2),?y_5),?z_5), +(?x_2,s(+(?y_5,?z_5)))> by Rules <5, 2> preceded by []
 joinable by a reduction of rules <[([],4)], [([],3)]>
Critical Pair <+(?x_4,+(?y_4,s(?y_3))), +(s(+(?x_4,?y_4)),?y_3)> by Rules <4, 3> preceded by []
 joinable by a reduction of rules <[([],5)], [([],2)]>
Critical Pair <+(+(+(?x_4,?y_4),?y_5),?z_5), +(?x_4,+(?y_4,+(?y_5,?z_5)))> by Rules <5, 4> preceded by []
 joinable by a reduction of rules <[([],4)], [([],5)]>
Critical Pair <+(*(?x_7,s(?y_6)),s(?y_6)), +(s(?x_7),*(s(?x_7),?y_6))> by Rules <7, 6> preceded by []
 joinable by a reduction of rules <[([(+,1)],6),([],4),([(+,2)],3),([],5)], [([(+,2)],7),([],5),([(+,1)],2)]>
 joinable by a reduction of rules <[([(+,1)],6),([],4),([(+,2)],3)], [([(+,2)],7),([],5),([(+,1)],2),([],4)]>
 joinable by a reduction of rules <[([(+,1)],6),([(+,1)],1),([],4),([(+,2)],3)], [([(+,2)],7),([(+,2)],1),([],5),([],1)]>
 joinable by a reduction of rules <[([(+,1)],6),([(+,1)],1),([],4),([(+,2)],3)], [([(+,2)],7),([],5),([(+,1)],1),([],4)]>
 joinable by a reduction of rules <[([(+,1)],6),([(+,1)],1),([],4),([(+,2)],3)], [([(+,2)],7),([],1),([],4),([(+,2)],1)]>
 joinable by a reduction of rules <[([(+,1)],6),([(+,1)],1),([],4),([(+,2)],3)], [([],1),([(+,1)],7),([],4),([(+,2)],1)]>
 joinable by a reduction of rules <[([(+,1)],6),([(+,1)],1),([],4),([(+,2)],1)], [([(+,2)],7),([],1),([],4),([(+,2)],3)]>
 joinable by a reduction of rules <[([(+,1)],6),([(+,1)],1),([],4),([(+,2)],1)], [([],1),([(+,1)],7),([],4),([(+,2)],3)]>
 joinable by a reduction of rules <[([(+,1)],6),([(+,1)],1),([],4),([],1)], [([(+,2)],7),([(+,2)],1),([],5),([(+,1)],2)]>
 joinable by a reduction of rules <[([(+,1)],6),([],4),([(+,2)],1),([],5)], [([(+,2)],7),([(+,2)],1),([],5),([(+,1)],2)]>
 joinable by a reduction of rules <[([(+,1)],6),([],4),([],1),([],4)], [([(+,2)],7),([],1),([],4),([(+,2)],3)]>
 joinable by a reduction of rules <[([(+,1)],6),([],4),([],1),([],4)], [([],1),([(+,1)],7),([],4),([(+,2)],3)]>
 joinable by a reduction of rules <[([(+,1)],6),([],1),([],5),([(+,1)],2)], [([(+,2)],7),([(+,2)],1),([],5),([(+,1)],1)]>
 joinable by a reduction of rules <[([(+,1)],6),([],1),([],5),([(+,1)],2)], [([(+,2)],7),([],5),([],1),([],5)]>
 joinable by a reduction of rules <[([(+,1)],6),([],1),([],5),([(+,1)],2)], [([(+,2)],7),([],1),([],4),([],1)]>
 joinable by a reduction of rules <[([(+,1)],6),([],1),([],5),([(+,1)],2)], [([],1),([(+,1)],7),([],4),([],1)]>
 joinable by a reduction of rules <[([(+,1)],6),([],1),([],5),([(+,1)],1)], [([(+,2)],7),([(+,2)],1),([],5),([(+,1)],2)]>
 joinable by a reduction of rules <[([(+,1)],6),([],1),([],5),([],1)], [([(+,2)],7),([],1),([],4),([(+,2)],3)]>
 joinable by a reduction of rules <[([(+,1)],6),([],1),([],5),([],1)], [([],1),([(+,1)],7),([],4),([(+,2)],3)]>
 joinable by a reduction of rules <[([(+,1)],0),([(+,1)],7),([],4),([(+,2)],3)], [([(+,2)],0),([(+,2)],6),([],5),([],1)]>
 joinable by a reduction of rules <[([(+,1)],0),([(+,1)],7),([],4),([],1)], [([(+,2)],0),([(+,2)],6),([],5),([(+,1)],2)]>
 joinable by a reduction of rules <[([],1),([(+,2)],6),([],5),([(+,1)],2)], [([(+,2)],7),([(+,2)],1),([],5),([(+,1)],1)]>
 joinable by a reduction of rules <[([],1),([(+,2)],6),([],5),([(+,1)],2)], [([(+,2)],7),([],5),([],1),([],5)]>
 joinable by a reduction of rules <[([],1),([(+,2)],6),([],5),([(+,1)],2)], [([(+,2)],7),([],1),([],4),([],1)]>
 joinable by a reduction of rules <[([],1),([(+,2)],6),([],5),([(+,1)],2)], [([],1),([(+,1)],7),([],4),([],1)]>
 joinable by a reduction of rules <[([],1),([(+,2)],6),([],5),([(+,1)],1)], [([(+,2)],7),([(+,2)],1),([],5),([(+,1)],2)]>
 joinable by a reduction of rules <[([],1),([(+,2)],6),([],5),([],1)], [([(+,2)],7),([],1),([],4),([(+,2)],3)]>
 joinable by a reduction of rules <[([],1),([(+,2)],6),([],5),([],1)], [([],1),([(+,1)],7),([],4),([(+,2)],3)]>
unknown Diagram Decreasing
   [ *(?x,?y) -> *(?y,?x),
     +(?x_1,?y_1) -> +(?y_1,?x_1),
     +(s(?x_2),?y_2) -> +(?x_2,s(?y_2)),
     +(?x_3,s(?y_3)) -> +(s(?x_3),?y_3),
     +(+(?x_4,?y_4),?z_4) -> +(?x_4,+(?y_4,?z_4)),
     +(?x_5,+(?y_5,?z_5)) -> +(+(?x_5,?y_5),?z_5),
     *(?x_6,s(?y_6)) -> +(?x_6,*(?x_6,?y_6)),
     *(s(?x_7),?y_7) -> +(*(?x_7,?y_7),?y_7) ]
Sort Assignment:
 * : 27*27=>27
 + : 27*27=>27
 s : 27=>27
non-linear variables: {?x_6,?y_7}
non-linear types: {27}
types leq non-linear types: {27}
rules applicable to terms of non-linear types:
   [ *(?x,?y) -> *(?y,?x),
     +(?x_1,?y_1) -> +(?y_1,?x_1),
     +(s(?x_2),?y_2) -> +(?x_2,s(?y_2)),
     +(?x_3,s(?y_3)) -> +(s(?x_3),?y_3),
     +(+(?x_4,?y_4),?z_4) -> +(?x_4,+(?y_4,?z_4)),
     +(?x_5,+(?y_5,?z_5)) -> +(+(?x_5,?y_5),?z_5),
     *(?x_6,s(?y_6)) -> +(?x_6,*(?x_6,?y_6)),
     *(s(?x_7),?y_7) -> +(*(?x_7,?y_7),?y_7) ]
Rnl:
0: {}
1: {}
2: {}
3: {}
4: {}
5: {}
6: {0,1,2,3,4,5,6,7}
7: {0,1,2,3,4,5,6,7}
unknown innermost-termination for terms of non-linear types
unknown Quasi-Linear & Linearized-Decreasing
   [ *(?x,?y) -> *(?y,?x),
     +(?x_1,?y_1) -> +(?y_1,?x_1),
     +(s(?x_2),?y_2) -> +(?x_2,s(?y_2)),
     +(?x_3,s(?y_3)) -> +(s(?x_3),?y_3),
     +(+(?x_4,?y_4),?z_4) -> +(?x_4,+(?y_4,?z_4)),
     +(?x_5,+(?y_5,?z_5)) -> +(+(?x_5,?y_5),?z_5),
     *(?x_6,s(?y_6)) -> +(?x_6,*(?x_6,?y_6)),
     *(s(?x_7),?y_7) -> +(*(?x_7,?y_7),?y_7) ]
Sort Assignment:
 * : 27*27=>27
 + : 27*27=>27
 s : 27=>27
non-linear variables: {?x_6,?y_7}
non-linear types: {27}
types leq non-linear types: {27}
rules applicable to terms of non-linear types:
   [ *(?x,?y) -> *(?y,?x),
     +(?x_1,?y_1) -> +(?y_1,?x_1),
     +(s(?x_2),?y_2) -> +(?x_2,s(?y_2)),
     +(?x_3,s(?y_3)) -> +(s(?x_3),?y_3),
     +(+(?x_4,?y_4),?z_4) -> +(?x_4,+(?y_4,?z_4)),
     +(?x_5,+(?y_5,?z_5)) -> +(+(?x_5,?y_5),?z_5),
     *(?x_6,s(?y_6)) -> +(?x_6,*(?x_6,?y_6)),
     *(s(?x_7),?y_7) -> +(*(?x_7,?y_7),?y_7) ]
unknown innermost-termination for terms of non-linear types
unknown Strongly Quasi-Linear & Hierarchically Decreasing
check Non-Confluence...
obtain 12 rules by 3 steps unfolding
obtain 100 candidates for checking non-joinability
check by TCAP-Approximation (failure)
check by Ordering(rpo), check by Tree-Automata Approximation (failure)
check by Interpretation(mod2) (failure)
check by Descendants-Approximation, check by Ordering(poly) (failure)
unknown Non-Confluence
Check relative termination:
   [ +(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),
     +(?x,?y) -> +(?y,?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,+(?y,?z)) -> +(+(?x,?y),?z) ]
Polynomial Interpretation:
  *:= (1)*x1+(1)*x1*x2+(1)*x2
  +:= (1)*x1+(1)*x2
  s:= (1)+(1)*x1
retract *(?x,s(?y)) -> +(?x,*(?x,?y))
retract *(s(?x),?y) -> +(*(?x,?y),?y)
retract *(?x,s(?y)) -> +(?x,*(?x,?y))
retract *(s(?x),?y) -> +(*(?x,?y),?y)
unknown relative termination
unknown Huet (modulo AC)
check by Reduction-Preserving Completion...
STEP: 1 (parallel)
S:
   [ *(?x,s(?y)) -> +(?x,*(?x,?y)),
     *(s(?x),?y) -> +(*(?x,?y),?y) ]
P:
   [ *(?x,?y) -> *(?y,?x),
     +(?x,?y) -> +(?y,?x),
     +(s(?x),?y) -> +(?x,s(?y)),
     +(?x,s(?y)) -> +(s(?x),?y),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,+(?y,?z)) -> +(+(?x,?y),?z) ]
S: terminating
CP(S,S):
<+(*(?x_1,s(?y)),s(?y)), +(s(?x_1),*(s(?x_1),?y))> --> <+(+(?x_1,*(?x_1,?y)),s(?y)), +(s(?x_1),+(*(?x_1,?y),?y))> => no
<+(s(?x_1),*(s(?x_1),?y)), +(*(?x_1,s(?y)),s(?y))> --> <+(s(?x_1),+(*(?x_1,?y),?y)), +(+(?x_1,*(?x_1,?y)),s(?y))> => no
PCP_in(symP,S):
CP(S,symP):
<+(?x,*(?x,?y)), *(s(?y),?x)> --> <+(?x,*(?x,?y)), +(*(?y,?x),?x)> => no
<+(*(?x,?y),?y), *(?y,s(?x))> --> <+(*(?x,?y),?y), +(?y,*(?y,?x))> => no
check joinability condition:
check modulo joinability of +(+(?x_1,*(?x_1,?y)),s(?y)) and +(s(?x_1),+(*(?x_1,?y),?y)): joinable by {2,3,4,5}
check modulo joinability of +(s(?x_1),+(*(?x_1,?y),?y)) and +(+(?x_1,*(?x_1,?y)),s(?y)): joinable by {2,3,4,5}
check modulo joinability of +(?x,*(?x,?y)) and +(*(?y,?x),?x): joinable by {1}
check modulo joinability of +(*(?x,?y),?y) and +(?y,*(?y,?x)): joinable by {1}
success
P':
   [ +(?x,s(?y)) -> +(s(?x),?y),
     +(s(?x),?y) -> +(?x,s(?y)),
     +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?y,?x) -> +(?x,?y) ]
Check relative termination:
   [ *(?x,s(?y)) -> +(?x,*(?x,?y)),
     *(s(?x),?y) -> +(*(?x,?y),?y) ]
   [ +(?x,s(?y)) -> +(s(?x),?y),
     +(s(?x),?y) -> +(?x,s(?y)),
     +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?y,?x) -> +(?x,?y) ]
Polynomial Interpretation:
  *:= (2)*x1+(1)*x1*x2+(2)*x2
  +:= (1)*x1+(1)*x2
  s:= (6)+(1)*x1
relatively terminating
S/P': relatively terminating
S:
   [ *(?x,s(?y)) -> +(?x,*(?x,?y)),
     *(s(?x),?y) -> +(*(?x,?y),?y) ]
P:
   [ *(?x,?y) -> *(?y,?x),
     +(?x,?y) -> +(?y,?x),
     +(s(?x),?y) -> +(?x,s(?y)),
     +(?x,s(?y)) -> +(s(?x),?y),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,+(?y,?z)) -> +(+(?x,?y),?z) ]
Success
Reduction-Preserving Completion
Direct Methods: CR

Combined result: CR
/tmp/file6CUHqy.trs: Success(CR)
(6435 msec.)