YES
(ignored inputs)COMMENT from the collection of \cite{AT2012}
Rewrite Rules:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     *(?x,?y) -> *(?y,?x),
     *(+(?x,?y),?z) -> +(*(?x,?z),*(?y,?z)),
     *(?x,+(?y,?z)) -> +(*(?x,?y),*(?x,?z)) ]
Apply Direct Methods...
Inner CPs:
   [ +(+(?y_1,?x_1),?z) = +(?x_1,+(?y_1,?z)),
     *(*(?y_3,?x_3),?z_2) = *(?x_3,*(?y_3,?z_2)),
     *(+(*(?x_4,?z_4),*(?y_4,?z_4)),?z_2) = *(+(?x_4,?y_4),*(?z_4,?z_2)),
     *(+(*(?x_5,?y_5),*(?x_5,?z_5)),?z_2) = *(?x_5,*(+(?y_5,?z_5),?z_2)),
     *(+(?x,+(?y,?z)),?z_4) = +(*(+(?x,?y),?z_4),*(?z,?z_4)),
     *(+(?y_1,?x_1),?z_4) = +(*(?x_1,?z_4),*(?y_1,?z_4)),
     *(?x_5,+(?x,+(?y,?z))) = +(*(?x_5,+(?x,?y)),*(?x_5,?z)),
     *(?x_5,+(?y_1,?x_1)) = +(*(?x_5,?x_1),*(?x_5,?y_1)),
     +(+(?x,+(?y,?z)),?z_1) = +(+(?x,?y),+(?z,?z_1)),
     *(*(?x,*(?y,?z)),?z_1) = *(*(?x,?y),*(?z,?z_1)) ]
Outer CPs:
   [ +(?x,+(?y,?z)) = +(?z,+(?x,?y)),
     *(?x_2,*(?y_2,?z_2)) = *(?z_2,*(?x_2,?y_2)),
     *(?x_2,*(?y_2,+(?y_5,?z_5))) = +(*(*(?x_2,?y_2),?y_5),*(*(?x_2,?y_2),?z_5)),
     *(?y_3,+(?x_4,?y_4)) = +(*(?x_4,?y_3),*(?y_4,?y_3)),
     *(+(?y_5,?z_5),?x_3) = +(*(?x_3,?y_5),*(?x_3,?z_5)),
     +(*(?x_4,+(?y_5,?z_5)),*(?y_4,+(?y_5,?z_5))) = +(*(+(?x_4,?y_4),?y_5),*(+(?x_4,?y_4),?z_5)) ]
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:
   [ +(?z,+(?x_1,+(?y_1,?y))) = +(+(?x_1,?y_1),+(?y,?z)),
     +(?z,+(?y,?x)) = +(?x,+(?y,?z)),
     +(?z,+(?x,?y)) = +(?x,+(?y,?z)),
     +(+(?x_1,+(?y_1,?y)),?z) = +(+(?x_1,?y_1),+(?y,?z)),
     +(+(?y,?x),?z) = +(?x,+(?y,?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_6,+(?y_6,?y)),?z_5),*(?z,?z_5)) = *(+(+(?x_6,?y_6),+(?y,?z)),?z_5),
     +(*(+(?y,?x),?z_5),*(?z,?z_5)) = *(+(?x,+(?y,?z)),?z_5),
     +(*(?x_6,+(?x_7,+(?y_7,?y))),*(?x_6,?z)) = *(?x_6,+(+(?x_7,?y_7),+(?y,?z))),
     +(*(?x_6,+(?y,?x)),*(?x_6,?z)) = *(?x_6,+(?x,+(?y,?z))),
     +(+(?x,?y),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
     +(*(+(?x,?y),?z_5),*(?z,?z_5)) = *(+(?x,+(?y,?z)),?z_5),
     +(*(?x_6,+(?x,?y)),*(?x_6,?z)) = *(?x_6,+(?x,+(?y,?z))),
     +(?x_1,+(?y_1,?y)) = +(?y,+(?x_1,?y_1)),
     +(?x,+(?y,?z_2)) = +(+(?y,?x),?z_2),
     +(*(?x,?z_5),*(?y,?z_5)) = *(+(?y,?x),?z_5),
     +(*(?x_6,?x),*(?x_6,?y)) = *(?x_6,+(?y,?x)),
     *(?z,*(?x_1,*(?y_1,?y))) = *(*(?x_1,?y_1),*(?y,?z)),
     *(?z,*(?y,?x)) = *(?x,*(?y,?z)),
     *(?z,+(*(?x_5,?y),*(?y_5,?y))) = *(+(?x_5,?y_5),*(?y,?z)),
     *(?z,+(*(?x,?y_6),*(?x,?z_6))) = *(?x,*(+(?y_6,?z_6),?z)),
     +(*(*(?x_6,*(?y_6,?y)),?y_5),*(*(?x_6,*(?y_6,?y)),?z_5)) = *(*(?x_6,?y_6),*(?y,+(?y_5,?z_5))),
     +(*(*(?y,?x),?y_5),*(*(?y,?x),?z_5)) = *(?x,*(?y,+(?y_5,?z_5))),
     +(*(+(*(?x_10,?y),*(?y_10,?y)),?y_5),*(+(*(?x_10,?y),*(?y_10,?y)),?z_5)) = *(+(?x_10,?y_10),*(?y,+(?y_5,?z_5))),
     +(*(+(*(?x,?y_11),*(?x,?z_11)),?y_5),*(+(*(?x,?y_11),*(?x,?z_11)),?z_5)) = *(?x,*(+(?y_11,?z_11),+(?y_5,?z_5))),
     *(?z,*(?x,?y)) = *(?x,*(?y,?z)),
     +(*(*(?x,?y),?y_5),*(*(?x,?y),?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_5,?y),*(?y_5,?y)),?z) = *(+(?x_5,?y_5),*(?y,?z)),
     *(+(*(?x,?y_6),*(?x,?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_6,?y),*(?y_6,?y)),*(?z,?z_1)) = *(*(+(?x_6,?y_6),*(?y,?z)),?z_1),
     *(+(*(?x,?y_7),*(?x,?z_7)),*(?z,?z_1)) = *(*(?x,*(+(?y_7,?z_7),?z)),?z_1),
     *(*(?x,?y),*(?z,?z_1)) = *(*(?x,*(?y,?z)),?z_1),
     *(?x_3,*(?y_3,?y)) = *(?y,*(?x_3,?y_3)),
     +(*(?x_4,?y),*(?y_4,?y)) = *(?y,+(?x_4,?y_4)),
     +(*(?x,?y_5),*(?x,?z_5)) = *(+(?y_5,?z_5),?x),
     *(?x,*(?y,?z_4)) = *(*(?y,?x),?z_4),
     *(?z,+(?x_2,+(?y_2,?y))) = +(*(+(?x_2,?y_2),?z),*(?y,?z)),
     *(?z,+(?y,?x)) = +(*(?x,?z),*(?y,?z)),
     +(*(+(?x_7,+(?y_7,?y)),?y_5),*(+(?x_7,+(?y_7,?y)),?z_5)) = +(*(+(?x_7,?y_7),+(?y_5,?z_5)),*(?y,+(?y_5,?z_5))),
     +(*(+(?y,?x),?y_5),*(+(?y,?x),?z_5)) = +(*(?x,+(?y_5,?z_5)),*(?y,+(?y_5,?z_5))),
     *(?z,+(?x,?y)) = +(*(?x,?z),*(?y,?z)),
     +(*(+(?x,?y),?y_5),*(+(?x,?y),?z_5)) = +(*(?x,+(?y_5,?z_5)),*(?y,+(?y_5,?z_5))),
     *(+(?x_2,+(?y_2,?y)),?z) = +(*(+(?x_2,?y_2),?z),*(?y,?z)),
     *(+(?y,?x),?z) = +(*(?x,?z),*(?y,?z)),
     *(+(?x_6,+(?y_6,?y)),*(?z,?z_4)) = *(+(*(+(?x_6,?y_6),?z),*(?y,?z)),?z_4),
     *(+(?y,?x),*(?z,?z_4)) = *(+(*(?x,?z),*(?y,?z)),?z_4),
     *(+(?x,?y),*(?z,?z_4)) = *(+(*(?x,?z),*(?y,?z)),?z_4),
     *(?x_3,*(?y_3,+(?x_5,+(?y_5,?z)))) = +(*(*(?x_3,?y_3),+(?x_5,?y_5)),*(*(?x_3,?y_3),?z)),
     *(?x_3,*(?y_3,+(?z,?y))) = +(*(*(?x_3,?y_3),?y),*(*(?x_3,?y_3),?z)),
     *(+(?x_2,+(?y_2,?z)),?x) = +(*(?x,+(?x_2,?y_2)),*(?x,?z)),
     *(+(?z,?y),?x) = +(*(?x,?y),*(?x,?z)),
     +(*(?x_5,+(?x_7,+(?y_7,?z))),*(?y_5,+(?x_7,+(?y_7,?z)))) = +(*(+(?x_5,?y_5),+(?x_7,?y_7)),*(+(?x_5,?y_5),?z)),
     +(*(?x_5,+(?z,?y)),*(?y_5,+(?z,?y))) = +(*(+(?x_5,?y_5),?y),*(+(?x_5,?y_5),?z)),
     *(?x_3,*(?y_3,+(?y,?z))) = +(*(*(?x_3,?y_3),?y),*(*(?x_3,?y_3),?z)),
     *(+(?y,?z),?x) = +(*(?x,?y),*(?x,?z)),
     +(*(?x_5,+(?y,?z)),*(?y_5,+(?y,?z))) = +(*(+(?x_5,?y_5),?y),*(+(?x_5,?y_5),?z)),
     *(?x,+(?x_2,+(?y_2,?z))) = +(*(?x,+(?x_2,?y_2)),*(?x,?z)),
     *(?x,+(?z,?y)) = +(*(?x,?y),*(?x,?z)),
     *(?x,*(+(?x_6,+(?y_6,?z)),?z_4)) = *(+(*(?x,+(?x_6,?y_6)),*(?x,?z)),?z_4),
     *(?x,*(+(?z,?y),?z_4)) = *(+(*(?x,?y),*(?x,?z)),?z_4),
     *(?x,*(+(?y,?z),?z_4)) = *(+(*(?x,?y),*(?x,?z)),?z_4) ]
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), +(?x_1,+(?y_1,?z))> by Rules <1, 0> preceded by [(+,1)]
 joinable by a reduction of rules <[([(+,1)],1),([],0)], []>
 joinable by a reduction of rules <[([],0),([(+,2)],1)], [([],1),([],0)]>
Critical Pair <*(*(?y_3,?x_3),?z_2), *(?x_3,*(?y_3,?z_2))> by Rules <3, 2> preceded by [(*,1)]
 joinable by a reduction of rules <[([(*,1)],3),([],2)], []>
 joinable by a reduction of rules <[([],2),([(*,2)],3)], [([],3),([],2)]>
Critical Pair <*(+(*(?x_4,?z_4),*(?y_4,?z_4)),?z_2), *(+(?x_4,?y_4),*(?z_4,?z_2))> by Rules <4, 2> preceded by [(*,1)]
 joinable by a reduction of rules <[([],4),([(+,2)],2),([(+,1)],2)], [([],4)]>
 joinable by a reduction of rules <[([],4),([(+,1)],2),([(+,2)],2)], [([],4)]>
 joinable by a reduction of rules <[([],4),([(+,2)],2),([(+,1)],2)], [([(*,1)],1),([],4),([],1)]>
 joinable by a reduction of rules <[([],4),([(+,1)],2),([(+,2)],2)], [([(*,1)],1),([],4),([],1)]>
Critical Pair <*(+(*(?x_5,?y_5),*(?x_5,?z_5)),?z_2), *(?x_5,*(+(?y_5,?z_5),?z_2))> by Rules <5, 2> preceded by [(*,1)]
 joinable by a reduction of rules <[([],4),([(+,2)],2),([(+,1)],2)], [([(*,2)],4),([],5)]>
 joinable by a reduction of rules <[([],4),([(+,1)],2),([(+,2)],2)], [([(*,2)],4),([],5)]>
Critical Pair <*(+(?x,+(?y,?z)),?z_4), +(*(+(?x,?y),?z_4),*(?z,?z_4))> by Rules <0, 4> preceded by [(*,1)]
 joinable by a reduction of rules <[([],4),([(+,2)],4)], [([(+,1)],4),([],0)]>
Critical Pair <*(+(?y_1,?x_1),?z_4), +(*(?x_1,?z_4),*(?y_1,?z_4))> by Rules <1, 4> preceded by [(*,1)]
 joinable by a reduction of rules <[([],4)], [([],1)]>
Critical Pair <*(?x_5,+(?x,+(?y,?z))), +(*(?x_5,+(?x,?y)),*(?x_5,?z))> by Rules <0, 5> preceded by [(*,2)]
 joinable by a reduction of rules <[([],5),([(+,2)],5)], [([(+,1)],5),([],0)]>
Critical Pair <*(?x_5,+(?y_1,?x_1)), +(*(?x_5,?x_1),*(?x_5,?y_1))> by Rules <1, 5> preceded by [(*,2)]
 joinable by a reduction of rules <[([],5)], [([],1)]>
Critical Pair <+(+(?x,+(?y,?z)),?z_1), +(+(?x,?y),+(?z,?z_1))> by Rules <0, 0> preceded by [(+,1)]
 joinable by a reduction of rules <[([],0),([(+,2)],0)], [([],0)]>
Critical Pair <*(*(?x,*(?y,?z)),?z_1), *(*(?x,?y),*(?z,?z_1))> by Rules <2, 2> preceded by [(*,1)]
 joinable by a reduction of rules <[([],2),([(*,2)],2)], [([],2)]>
Critical Pair <+(?y_1,+(?x,?y)), +(?x,+(?y,?y_1))> by Rules <1, 0> preceded by []
 joinable by a reduction of rules <[([],1),([],0)], []>
Critical Pair <*(?y_3,*(?x_2,?y_2)), *(?x_2,*(?y_2,?y_3))> by Rules <3, 2> preceded by []
 joinable by a reduction of rules <[([],3),([],2)], []>
Critical Pair <+(*(*(?x_2,?y_2),?y_5),*(*(?x_2,?y_2),?z_5)), *(?x_2,*(?y_2,+(?y_5,?z_5)))> by Rules <5, 2> preceded by []
 joinable by a reduction of rules <[([(+,2)],2),([(+,1)],2)], [([(*,2)],5),([],5)]>
 joinable by a reduction of rules <[([(+,1)],2),([(+,2)],2)], [([(*,2)],5),([],5)]>
Critical Pair <+(*(?x_4,?z_4),*(?y_4,?z_4)), *(?z_4,+(?x_4,?y_4))> by Rules <4, 3> preceded by []
 joinable by a reduction of rules <[([(+,2)],3),([(+,1)],3)], [([],5)]>
 joinable by a reduction of rules <[([(+,1)],3),([(+,2)],3)], [([],5)]>
 joinable by a reduction of rules <[], [([],3),([],4)]>
 joinable by a reduction of rules <[([(+,2)],3)], [([],5),([(+,1)],3)]>
 joinable by a reduction of rules <[([(+,1)],3)], [([],5),([(+,2)],3)]>
Critical Pair <+(*(?x_5,?y_5),*(?x_5,?z_5)), *(+(?y_5,?z_5),?x_5)> by Rules <5, 3> preceded by []
 joinable by a reduction of rules <[([(+,2)],3),([(+,1)],3)], [([],4)]>
 joinable by a reduction of rules <[([(+,1)],3),([(+,2)],3)], [([],4)]>
 joinable by a reduction of rules <[], [([],3),([],5)]>
 joinable by a reduction of rules <[([(+,2)],3)], [([],4),([(+,1)],3)]>
 joinable by a reduction of rules <[([(+,1)],3)], [([],4),([(+,2)],3)]>
Critical Pair <+(*(+(?x_4,?y_4),?y_5),*(+(?x_4,?y_4),?z_5)), +(*(?x_4,+(?y_5,?z_5)),*(?y_4,+(?y_5,?z_5)))> by Rules <5, 4> preceded by []
 joinable by a reduction of rules <[([(+,2)],4),([(+,1)],4),([],0),([(+,2)],1),([(+,2)],0)], [([(+,2),(*,2)],1),([(+,2)],5),([(+,1)],5),([],0)]>
 joinable by a reduction of rules <[([(+,2)],4),([(+,1)],4),([],0),([(+,2)],1),([(+,2)],0)], [([(+,2),(*,2)],1),([(+,1)],5),([(+,2)],5),([],0)]>
 joinable by a reduction of rules <[([(+,2)],4),([(+,1)],4),([],0),([(+,2)],1),([(+,2)],0)], [([(+,2),(*,2)],1),([(+,1)],5),([],0),([(+,2),(+,2)],5)]>
 joinable by a reduction of rules <[([(+,2)],4),([(+,1)],4),([],0),([(+,2)],1),([(+,2)],0)], [([(+,2)],5),([(+,2)],1),([(+,1)],5),([],0)]>
 joinable by a reduction of rules <[([(+,2)],4),([(+,1)],4),([],0),([(+,2)],1),([(+,2)],0)], [([(+,2)],5),([(+,1)],5),([(+,2)],1),([],0)]>
 joinable by a reduction of rules <[([(+,2)],4),([(+,1)],4),([],0),([(+,2)],1),([(+,2)],0)], [([(+,2)],5),([(+,1)],5),([],0),([(+,2),(+,2)],1)]>
 joinable by a reduction of rules <[([(+,2)],4),([(+,1)],4),([],0),([(+,2)],1),([(+,2)],0)], [([(+,1)],5),([(+,2),(*,2)],1),([(+,2)],5),([],0)]>
 joinable by a reduction of rules <[([(+,2)],4),([(+,1)],4),([],0),([(+,2)],1),([(+,2)],0)], [([(+,1)],5),([(+,2),(*,2)],1),([],0),([(+,2),(+,2)],5)]>
 joinable by a reduction of rules <[([(+,2)],4),([(+,1)],4),([],0),([(+,2)],1),([(+,2)],0)], [([(+,1)],5),([(+,2)],5),([(+,2)],1),([],0)]>
 joinable by a reduction of rules <[([(+,2)],4),([(+,1)],4),([],0),([(+,2)],1),([(+,2)],0)], [([(+,1)],5),([(+,2)],5),([],0),([(+,2),(+,2)],1)]>
 joinable by a reduction of rules <[([(+,2)],4),([(+,1)],4),([],0),([(+,2)],1),([(+,2)],0)], [([(+,1)],5),([],0),([(+,2),(+,2),(*,2)],1),([(+,2),(+,2)],5)]>
 joinable by a reduction of rules <[([(+,2)],4),([(+,1)],4),([],0),([(+,2)],1),([(+,2)],0)], [([(+,1)],5),([],0),([(+,2),(+,2)],5),([(+,2),(+,2)],1)]>
 joinable by a reduction of rules <[([(+,1)],4),([(+,2)],4),([],0),([(+,2)],1),([(+,2)],0)], [([(+,2),(*,2)],1),([(+,2)],5),([(+,1)],5),([],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([(+,2)],4),([],0),([(+,2)],1),([(+,2)],0)], [([(+,2),(*,2)],1),([(+,1)],5),([(+,2)],5),([],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([(+,2)],4),([],0),([(+,2)],1),([(+,2)],0)], [([(+,2),(*,2)],1),([(+,1)],5),([],0),([(+,2),(+,2)],5)]>
 joinable by a reduction of rules <[([(+,1)],4),([(+,2)],4),([],0),([(+,2)],1),([(+,2)],0)], [([(+,2)],5),([(+,2)],1),([(+,1)],5),([],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([(+,2)],4),([],0),([(+,2)],1),([(+,2)],0)], [([(+,2)],5),([(+,1)],5),([(+,2)],1),([],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([(+,2)],4),([],0),([(+,2)],1),([(+,2)],0)], [([(+,2)],5),([(+,1)],5),([],0),([(+,2),(+,2)],1)]>
 joinable by a reduction of rules <[([(+,1)],4),([(+,2)],4),([],0),([(+,2)],1),([(+,2)],0)], [([(+,1)],5),([(+,2),(*,2)],1),([(+,2)],5),([],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([(+,2)],4),([],0),([(+,2)],1),([(+,2)],0)], [([(+,1)],5),([(+,2),(*,2)],1),([],0),([(+,2),(+,2)],5)]>
 joinable by a reduction of rules <[([(+,1)],4),([(+,2)],4),([],0),([(+,2)],1),([(+,2)],0)], [([(+,1)],5),([(+,2)],5),([(+,2)],1),([],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([(+,2)],4),([],0),([(+,2)],1),([(+,2)],0)], [([(+,1)],5),([(+,2)],5),([],0),([(+,2),(+,2)],1)]>
 joinable by a reduction of rules <[([(+,1)],4),([(+,2)],4),([],0),([(+,2)],1),([(+,2)],0)], [([(+,1)],5),([],0),([(+,2),(+,2),(*,2)],1),([(+,2),(+,2)],5)]>
 joinable by a reduction of rules <[([(+,1)],4),([(+,2)],4),([],0),([(+,2)],1),([(+,2)],0)], [([(+,1)],5),([],0),([(+,2),(+,2)],5),([(+,2),(+,2)],1)]>
 joinable by a reduction of rules <[([(+,1)],4),([],0),([(+,2),(+,2)],4),([(+,2)],1),([(+,2)],0)], [([(+,2),(*,2)],1),([(+,2)],5),([(+,1)],5),([],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([],0),([(+,2),(+,2)],4),([(+,2)],1),([(+,2)],0)], [([(+,2),(*,2)],1),([(+,1)],5),([(+,2)],5),([],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([],0),([(+,2),(+,2)],4),([(+,2)],1),([(+,2)],0)], [([(+,2),(*,2)],1),([(+,1)],5),([],0),([(+,2),(+,2)],5)]>
 joinable by a reduction of rules <[([(+,1)],4),([],0),([(+,2),(+,2)],4),([(+,2)],1),([(+,2)],0)], [([(+,2)],5),([(+,2)],1),([(+,1)],5),([],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([],0),([(+,2),(+,2)],4),([(+,2)],1),([(+,2)],0)], [([(+,2)],5),([(+,1)],5),([(+,2)],1),([],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([],0),([(+,2),(+,2)],4),([(+,2)],1),([(+,2)],0)], [([(+,2)],5),([(+,1)],5),([],0),([(+,2),(+,2)],1)]>
 joinable by a reduction of rules <[([(+,1)],4),([],0),([(+,2),(+,2)],4),([(+,2)],1),([(+,2)],0)], [([(+,1)],5),([(+,2),(*,2)],1),([(+,2)],5),([],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([],0),([(+,2),(+,2)],4),([(+,2)],1),([(+,2)],0)], [([(+,1)],5),([(+,2),(*,2)],1),([],0),([(+,2),(+,2)],5)]>
 joinable by a reduction of rules <[([(+,1)],4),([],0),([(+,2),(+,2)],4),([(+,2)],1),([(+,2)],0)], [([(+,1)],5),([(+,2)],5),([(+,2)],1),([],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([],0),([(+,2),(+,2)],4),([(+,2)],1),([(+,2)],0)], [([(+,1)],5),([(+,2)],5),([],0),([(+,2),(+,2)],1)]>
 joinable by a reduction of rules <[([(+,1)],4),([],0),([(+,2),(+,2)],4),([(+,2)],1),([(+,2)],0)], [([(+,1)],5),([],0),([(+,2),(+,2),(*,2)],1),([(+,2),(+,2)],5)]>
 joinable by a reduction of rules <[([(+,1)],4),([],0),([(+,2),(+,2)],4),([(+,2)],1),([(+,2)],0)], [([(+,1)],5),([],0),([(+,2),(+,2)],5),([(+,2),(+,2)],1)]>
 joinable by a reduction of rules <[([(+,1)],4),([],0),([(+,2)],1),([(+,2),(+,1)],4),([(+,2)],0)], [([(+,2),(*,2)],1),([(+,2)],5),([(+,1)],5),([],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([],0),([(+,2)],1),([(+,2),(+,1)],4),([(+,2)],0)], [([(+,2),(*,2)],1),([(+,1)],5),([(+,2)],5),([],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([],0),([(+,2)],1),([(+,2),(+,1)],4),([(+,2)],0)], [([(+,2),(*,2)],1),([(+,1)],5),([],0),([(+,2),(+,2)],5)]>
 joinable by a reduction of rules <[([(+,1)],4),([],0),([(+,2)],1),([(+,2),(+,1)],4),([(+,2)],0)], [([(+,2)],5),([(+,2)],1),([(+,1)],5),([],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([],0),([(+,2)],1),([(+,2),(+,1)],4),([(+,2)],0)], [([(+,2)],5),([(+,1)],5),([(+,2)],1),([],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([],0),([(+,2)],1),([(+,2),(+,1)],4),([(+,2)],0)], [([(+,2)],5),([(+,1)],5),([],0),([(+,2),(+,2)],1)]>
 joinable by a reduction of rules <[([(+,1)],4),([],0),([(+,2)],1),([(+,2),(+,1)],4),([(+,2)],0)], [([(+,1)],5),([(+,2),(*,2)],1),([(+,2)],5),([],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([],0),([(+,2)],1),([(+,2),(+,1)],4),([(+,2)],0)], [([(+,1)],5),([(+,2),(*,2)],1),([],0),([(+,2),(+,2)],5)]>
 joinable by a reduction of rules <[([(+,1)],4),([],0),([(+,2)],1),([(+,2),(+,1)],4),([(+,2)],0)], [([(+,1)],5),([(+,2)],5),([(+,2)],1),([],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([],0),([(+,2)],1),([(+,2),(+,1)],4),([(+,2)],0)], [([(+,1)],5),([(+,2)],5),([],0),([(+,2),(+,2)],1)]>
 joinable by a reduction of rules <[([(+,1)],4),([],0),([(+,2)],1),([(+,2),(+,1)],4),([(+,2)],0)], [([(+,1)],5),([],0),([(+,2),(+,2),(*,2)],1),([(+,2),(+,2)],5)]>
 joinable by a reduction of rules <[([(+,1)],4),([],0),([(+,2)],1),([(+,2),(+,1)],4),([(+,2)],0)], [([(+,1)],5),([],0),([(+,2),(+,2)],5),([(+,2),(+,2)],1)]>
 joinable by a reduction of rules <[([(+,2),(*,1)],1),([(+,2)],4),([(+,1)],4),([],0)], [([(+,2)],5),([(+,1)],5),([],0),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,2),(*,1)],1),([(+,2)],4),([(+,1)],4),([],0)], [([(+,1)],5),([(+,2)],5),([],0),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,2),(*,1)],1),([(+,2)],4),([(+,1)],4),([],0)], [([(+,1)],5),([],0),([(+,2),(+,2)],5),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,2),(*,1)],1),([(+,2)],4),([(+,1)],4),([],0)], [([(+,1)],5),([],0),([(+,2)],1),([(+,2),(+,1)],5),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,2),(*,1)],1),([(+,1)],4),([(+,2)],4),([],0)], [([(+,2)],5),([(+,1)],5),([],0),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,2),(*,1)],1),([(+,1)],4),([(+,2)],4),([],0)], [([(+,1)],5),([(+,2)],5),([],0),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,2),(*,1)],1),([(+,1)],4),([(+,2)],4),([],0)], [([(+,1)],5),([],0),([(+,2),(+,2)],5),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,2),(*,1)],1),([(+,1)],4),([(+,2)],4),([],0)], [([(+,1)],5),([],0),([(+,2)],1),([(+,2),(+,1)],5),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,2),(*,1)],1),([(+,1)],4),([],0),([(+,2),(+,2)],4)], [([(+,2)],5),([(+,1)],5),([],0),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,2),(*,1)],1),([(+,1)],4),([],0),([(+,2),(+,2)],4)], [([(+,1)],5),([(+,2)],5),([],0),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,2),(*,1)],1),([(+,1)],4),([],0),([(+,2),(+,2)],4)], [([(+,1)],5),([],0),([(+,2),(+,2)],5),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,2),(*,1)],1),([(+,1)],4),([],0),([(+,2),(+,2)],4)], [([(+,1)],5),([],0),([(+,2)],1),([(+,2),(+,1)],5),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,2)],4),([(+,2)],1),([(+,1)],4),([],0)], [([(+,2)],5),([(+,1)],5),([],0),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,2)],4),([(+,2)],1),([(+,1)],4),([],0)], [([(+,1)],5),([(+,2)],5),([],0),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,2)],4),([(+,2)],1),([(+,1)],4),([],0)], [([(+,1)],5),([],0),([(+,2),(+,2)],5),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,2)],4),([(+,2)],1),([(+,1)],4),([],0)], [([(+,1)],5),([],0),([(+,2)],1),([(+,2),(+,1)],5),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,2)],4),([(+,1)],4),([(+,2)],1),([],0)], [([(+,2)],5),([(+,1)],5),([],0),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,2)],4),([(+,1)],4),([(+,2)],1),([],0)], [([(+,1)],5),([(+,2)],5),([],0),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,2)],4),([(+,1)],4),([(+,2)],1),([],0)], [([(+,1)],5),([],0),([(+,2),(+,2)],5),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,2)],4),([(+,1)],4),([(+,2)],1),([],0)], [([(+,1)],5),([],0),([(+,2)],1),([(+,2),(+,1)],5),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,2)],4),([(+,1)],4),([],0),([(+,2),(+,2)],1)], [([(+,2)],5),([(+,1)],5),([],0),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,2)],4),([(+,1)],4),([],0),([(+,2),(+,2)],1)], [([(+,1)],5),([(+,2)],5),([],0),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,2)],4),([(+,1)],4),([],0),([(+,2),(+,2)],1)], [([(+,1)],5),([],0),([(+,2),(+,2)],5),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,2)],4),([(+,1)],4),([],0),([(+,2),(+,2)],1)], [([(+,1)],5),([],0),([(+,2)],1),([(+,2),(+,1)],5),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([(+,2),(*,1)],1),([(+,2)],4),([],0)], [([(+,2)],5),([(+,1)],5),([],0),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([(+,2),(*,1)],1),([(+,2)],4),([],0)], [([(+,1)],5),([(+,2)],5),([],0),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([(+,2),(*,1)],1),([(+,2)],4),([],0)], [([(+,1)],5),([],0),([(+,2),(+,2)],5),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([(+,2),(*,1)],1),([(+,2)],4),([],0)], [([(+,1)],5),([],0),([(+,2)],1),([(+,2),(+,1)],5),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([(+,2),(*,1)],1),([],0),([(+,2),(+,2)],4)], [([(+,2)],5),([(+,1)],5),([],0),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([(+,2),(*,1)],1),([],0),([(+,2),(+,2)],4)], [([(+,1)],5),([(+,2)],5),([],0),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([(+,2),(*,1)],1),([],0),([(+,2),(+,2)],4)], [([(+,1)],5),([],0),([(+,2),(+,2)],5),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([(+,2),(*,1)],1),([],0),([(+,2),(+,2)],4)], [([(+,1)],5),([],0),([(+,2)],1),([(+,2),(+,1)],5),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([(+,2)],4),([(+,2)],1),([],0)], [([(+,2)],5),([(+,1)],5),([],0),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([(+,2)],4),([(+,2)],1),([],0)], [([(+,1)],5),([(+,2)],5),([],0),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([(+,2)],4),([(+,2)],1),([],0)], [([(+,1)],5),([],0),([(+,2),(+,2)],5),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([(+,2)],4),([(+,2)],1),([],0)], [([(+,1)],5),([],0),([(+,2)],1),([(+,2),(+,1)],5),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([(+,2)],4),([],0),([(+,2),(+,2)],1)], [([(+,2)],5),([(+,1)],5),([],0),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([(+,2)],4),([],0),([(+,2),(+,2)],1)], [([(+,1)],5),([(+,2)],5),([],0),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([(+,2)],4),([],0),([(+,2),(+,2)],1)], [([(+,1)],5),([],0),([(+,2),(+,2)],5),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([(+,2)],4),([],0),([(+,2),(+,2)],1)], [([(+,1)],5),([],0),([(+,2)],1),([(+,2),(+,1)],5),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([],0),([(+,2),(+,2),(*,1)],1),([(+,2),(+,2)],4)], [([(+,2)],5),([(+,1)],5),([],0),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([],0),([(+,2),(+,2),(*,1)],1),([(+,2),(+,2)],4)], [([(+,1)],5),([(+,2)],5),([],0),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([],0),([(+,2),(+,2),(*,1)],1),([(+,2),(+,2)],4)], [([(+,1)],5),([],0),([(+,2),(+,2)],5),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([],0),([(+,2),(+,2),(*,1)],1),([(+,2),(+,2)],4)], [([(+,1)],5),([],0),([(+,2)],1),([(+,2),(+,1)],5),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([],0),([(+,2),(+,2)],4),([(+,2),(+,2)],1)], [([(+,2)],5),([(+,1)],5),([],0),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([],0),([(+,2),(+,2)],4),([(+,2),(+,2)],1)], [([(+,1)],5),([(+,2)],5),([],0),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([],0),([(+,2),(+,2)],4),([(+,2),(+,2)],1)], [([(+,1)],5),([],0),([(+,2),(+,2)],5),([(+,2)],1),([(+,2)],0)]>
 joinable by a reduction of rules <[([(+,1)],4),([],0),([(+,2),(+,2)],4),([(+,2),(+,2)],1)], [([(+,1)],5),([],0),([(+,2)],1),([(+,2),(+,1)],5),([(+,2)],0)]>
unknown Diagram Decreasing
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x_1,?y_1) -> +(?y_1,?x_1),
     *(*(?x_2,?y_2),?z_2) -> *(?x_2,*(?y_2,?z_2)),
     *(?x_3,?y_3) -> *(?y_3,?x_3),
     *(+(?x_4,?y_4),?z_4) -> +(*(?x_4,?z_4),*(?y_4,?z_4)),
     *(?x_5,+(?y_5,?z_5)) -> +(*(?x_5,?y_5),*(?x_5,?z_5)) ]
Sort Assignment:
 * : 23*23=>23
 + : 23*23=>23
non-linear variables: {?z_4,?x_5}
non-linear types: {23}
types leq non-linear types: {23}
rules applicable to terms of non-linear types:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x_1,?y_1) -> +(?y_1,?x_1),
     *(*(?x_2,?y_2),?z_2) -> *(?x_2,*(?y_2,?z_2)),
     *(?x_3,?y_3) -> *(?y_3,?x_3),
     *(+(?x_4,?y_4),?z_4) -> +(*(?x_4,?z_4),*(?y_4,?z_4)),
     *(?x_5,+(?y_5,?z_5)) -> +(*(?x_5,?y_5),*(?x_5,?z_5)) ]
NLR:
0: {}
1: {}
2: {}
3: {}
4: {0,1,2,3,4,5}
5: {0,1,2,3,4,5}
unknown innermost-termination for terms of non-linear types
unknown Quasi-Linear & Linearized-Decreasing
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x_1,?y_1) -> +(?y_1,?x_1),
     *(*(?x_2,?y_2),?z_2) -> *(?x_2,*(?y_2,?z_2)),
     *(?x_3,?y_3) -> *(?y_3,?x_3),
     *(+(?x_4,?y_4),?z_4) -> +(*(?x_4,?z_4),*(?y_4,?z_4)),
     *(?x_5,+(?y_5,?z_5)) -> +(*(?x_5,?y_5),*(?x_5,?z_5)) ]
Sort Assignment:
 * : 23*23=>23
 + : 23*23=>23
non-linear variables: {?z_4,?x_5}
non-linear types: {23}
types leq non-linear types: {23}
rules applicable to terms of non-linear types:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x_1,?y_1) -> +(?y_1,?x_1),
     *(*(?x_2,?y_2),?z_2) -> *(?x_2,*(?y_2,?z_2)),
     *(?x_3,?y_3) -> *(?y_3,?x_3),
     *(+(?x_4,?y_4),?z_4) -> +(*(?x_4,?z_4),*(?y_4,?z_4)),
     *(?x_5,+(?y_5,?z_5)) -> +(*(?x_5,?y_5),*(?x_5,?z_5)) ]
unknown innermost-termination for terms of non-linear types
unknown Strongly Quasi-Linear & Hierarchically Decreasing
check Non-Confluence...
obtain 16 rules by 3 steps unfolding
strenghten *(?x_7,?y_7) and *(?y_7,?x_7)
strenghten +(?x_11,?y_11) and +(?y_11,?x_11)
strenghten *(?x_2,*(?y_2,?x_8)) and *(?x_8,*(?x_2,?y_2))
strenghten *(?x_2,*(?y_2,?x_9)) and *(*(?x_2,?y_2),?x_9)
strenghten *(?x_3,*(?y_3,?x_16)) and *(?x_16,*(?y_3,?x_3))
strenghten *(?x_3,*(?y_3,?z_2)) and *(*(?y_3,?x_3),?z_2)
strenghten *(?x_14,*(?x_3,?y_3)) and *(?x_14,*(?y_3,?x_3))
strenghten *(?x_16,*(?x_17,?y_17)) and *(?x_17,*(?y_17,?x_16))
strenghten *(*(?x_15,?y_15),?x_14) and *(?x_14,*(?x_15,?y_15))
strenghten *(*(?x_17,?y_17),?x_16) and *(?x_17,*(?y_17,?x_16))
strenghten +(?x,+(?y,?x_12)) and +(?x_12,+(?x,?y))
strenghten +(?x,+(?y,?x_13)) and +(+(?x,?y),?x_13)
strenghten +(?x_1,+(?y_1,?z)) and +(+(?y_1,?x_1),?z)
strenghten +(*(?x_1,?z_4),*(?y_1,?z_4)) and *(+(?y_1,?x_1),?z_4)
strenghten +(*(?x_4,?x_8),*(?y_4,?x_8)) and *(?x_8,+(?x_4,?y_4))
strenghten +(*(?x_4,?x_9),*(?y_4,?x_9)) and *(+(?x_4,?y_4),?x_9)
strenghten +(*(?x_5,?x_1),*(?x_5,?y_1)) and *(?x_5,+(?y_1,?x_1))
strenghten +(*(?x_5,?x_10),*(?x_5,?y_10)) and *(?x_5,+(?x_10,?y_10))
strenghten +(*(?x_5,?y_5),*(?x_5,?z_5)) and *(+(?y_5,?z_5),?x_5)
strenghten *(?x,*(*(?x_1,?y_1),?x_2)) and *(?x_2,*(?x_1,*(?y_1,?x)))
strenghten *(?x_2,*(?y_2,*(?x_15,?y_15))) and *(*(?x_2,?y_2),*(?x_15,?y_15))
obtain 100 candidates for checking non-joinability
check by TCAP-Approximation (failure)
check by Root-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:
   [ *(+(?x,?y),?z) -> +(*(?x,?z),*(?y,?z)),
     *(?x,+(?y,?z)) -> +(*(?x,?y),*(?x,?z)) ]
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     *(?x,?y) -> *(?y,?x) ]
Polynomial Interpretation:
  *:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
  +:= (3)+(1)*x1+(1)*x2
relatively terminating
Huet (modulo AC)
Direct Methods: CR

Final result: CR
145.trs: Success(CR)
(49297 msec.)