YES
(ignored inputs)COMMENT from the collection of \cite{AT2012}
Rewrite Rules:
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     *(?x,0) -> 0,
     *(?x,s(?y)) -> +(*(?x,?y),?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     *(?x,?y) -> *(?y,?x),
     *(?x,+(?y,?z)) -> +(*(?x,?y),*(?x,?z)) ]
Apply Direct Methods...
Inner CPs:
   [ +(?x,?z_4) = +(?x,+(0,?z_4)),
     +(s(+(?x_1,?y_1)),?z_4) = +(?x_1,+(s(?y_1),?z_4)),
     +(+(?y_5,?x_5),?z_4) = +(?x_5,+(?y_5,?z_4)),
     *(0,?z_6) = *(?x_2,*(0,?z_6)),
     *(+(*(?x_3,?y_3),?x_3),?z_6) = *(?x_3,*(s(?y_3),?z_6)),
     *(*(?y_7,?x_7),?z_6) = *(?x_7,*(?y_7,?z_6)),
     *(+(*(?x_8,?y_8),*(?x_8,?z_8)),?z_6) = *(?x_8,*(+(?y_8,?z_8),?z_6)),
     *(?x_8,?x) = +(*(?x_8,?x),*(?x_8,0)),
     *(?x_8,s(+(?x_1,?y_1))) = +(*(?x_8,?x_1),*(?x_8,s(?y_1))),
     *(?x_8,+(?x_4,+(?y_4,?z_4))) = +(*(?x_8,+(?x_4,?y_4)),*(?x_8,?z_4)),
     *(?x_8,+(?y_5,?x_5)) = +(*(?x_8,?x_5),*(?x_8,?y_5)),
     +(+(?x,+(?y,?z)),?z_1) = +(+(?x,?y),+(?z,?z_1)),
     *(*(?x,*(?y,?z)),?z_1) = *(*(?x,?y),*(?z,?z_1)) ]
Outer CPs:
   [ +(?x_4,?y_4) = +(?x_4,+(?y_4,0)),
     ?x = +(0,?x),
     s(+(+(?x_4,?y_4),?y_1)) = +(?x_4,+(?y_4,s(?y_1))),
     s(+(?x_1,?y_1)) = +(s(?y_1),?x_1),
     0 = *(?x_6,*(?y_6,0)),
     0 = *(0,?x_2),
     +(*(*(?x_6,?y_6),?y_3),*(?x_6,?y_6)) = *(?x_6,*(?y_6,s(?y_3))),
     +(*(?x_3,?y_3),?x_3) = *(s(?y_3),?x_3),
     +(?x_4,+(?y_4,?z_4)) = +(?z_4,+(?x_4,?y_4)),
     *(?x_6,*(?y_6,?z_6)) = *(?z_6,*(?x_6,?y_6)),
     *(?x_6,*(?y_6,+(?y_8,?z_8))) = +(*(*(?x_6,?y_6),?y_8),*(*(?x_6,?y_6),?z_8)),
     *(+(?y_8,?z_8),?x_7) = +(*(?x_7,?y_8),*(?x_7,?z_8)) ]
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_4,+(?y_4,0)) = +(?x_4,?y_4),
     +(0,?x) = ?x,
     +(?x,+(0,?z_5)) = +(?x,?z_5),
     +(*(?x_9,?x),*(?x_9,0)) = *(?x_9,?x),
     +(?x_4,+(?y_4,s(?y))) = s(+(+(?x_4,?y_4),?y)),
     +(s(?y),?x) = s(+(?x,?y)),
     +(?x,+(s(?y),?z_5)) = +(s(+(?x,?y)),?z_5),
     +(*(?x_9,?x),*(?x_9,s(?y))) = *(?x_9,s(+(?x,?y))),
     *(?x_6,*(?y_6,0)) = 0,
     *(0,?x) = 0,
     *(?x,*(0,?z_7)) = *(0,?z_7),
     *(?x_6,*(?y_6,s(?y))) = +(*(*(?x_6,?y_6),?y),*(?x_6,?y_6)),
     *(s(?y),?x) = +(*(?x,?y),?x),
     *(?x,*(s(?y),?z_7)) = *(+(*(?x,?y),?x),?z_7),
     +(?x_1,+(?y_1,?y)) = +(+(?x_1,?y_1),+(?y,0)),
     ?x = +(?x,+(0,0)),
     s(+(?x,?y_3)) = +(?x,+(s(?y_3),0)),
     +(?y,?x) = +(?x,+(?y,0)),
     s(+(+(?x_3,+(?y_3,?y)),?y_2)) = +(+(?x_3,?y_3),+(?y,s(?y_2))),
     s(+(?x,?y_2)) = +(?x,+(0,s(?y_2))),
     s(+(s(+(?x,?y_5)),?y_2)) = +(?x,+(s(?y_5),s(?y_2))),
     s(+(+(?y,?x),?y_2)) = +(?x,+(?y,s(?y_2))),
     +(?z,+(?x_1,+(?y_1,?y))) = +(+(?x_1,?y_1),+(?y,?z)),
     +(?z,?x) = +(?x,+(0,?z)),
     +(?z,s(+(?x,?y_3))) = +(?x,+(s(?y_3),?z)),
     +(?z,+(?y,?x)) = +(?x,+(?y,?z)),
     +(?x,?y) = +(?x,+(?y,0)),
     s(+(+(?x,?y),?y_2)) = +(?x,+(?y,s(?y_2))),
     +(?z,+(?x,?y)) = +(?x,+(?y,?z)),
     +(+(?x_1,+(?y_1,?y)),?z) = +(+(?x_1,?y_1),+(?y,?z)),
     +(?x,?z) = +(?x,+(0,?z)),
     +(s(+(?x,?y_3)),?z) = +(?x,+(s(?y_3),?z)),
     +(+(?y,?x),?z) = +(?x,+(?y,?z)),
     +(+(?x_2,+(?y_2,?y)),+(?z,?z_1)) = +(+(+(?x_2,?y_2),+(?y,?z)),?z_1),
     +(?x,+(?z,?z_1)) = +(+(?x,+(0,?z)),?z_1),
     +(s(+(?x,?y_4)),+(?z,?z_1)) = +(+(?x,+(s(?y_4),?z)),?z_1),
     +(+(?y,?x),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
     +(*(?x_9,+(?x_10,+(?y_10,?y))),*(?x_9,?z)) = *(?x_9,+(+(?x_10,?y_10),+(?y,?z))),
     +(*(?x_9,?x),*(?x_9,?z)) = *(?x_9,+(?x,+(0,?z))),
     +(*(?x_9,s(+(?x,?y_12))),*(?x_9,?z)) = *(?x_9,+(?x,+(s(?y_12),?z))),
     +(*(?x_9,+(?y,?x)),*(?x_9,?z)) = *(?x_9,+(?x,+(?y,?z))),
     +(+(?x,?y),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
     +(*(?x_9,+(?x,?y)),*(?x_9,?z)) = *(?x_9,+(?x,+(?y,?z))),
     ?x = +(0,?x),
     s(+(?x,?y_2)) = +(s(?y_2),?x),
     +(?x_5,+(?y_5,?y)) = +(?y,+(?x_5,?y_5)),
     +(?x,+(?y,?z_6)) = +(+(?y,?x),?z_6),
     +(*(?x_9,?x),*(?x_9,?y)) = *(?x_9,+(?y,?x)),
     0 = *(*(?x_1,?y_1),*(?y,0)),
     0 = *(?x,*(0,0)),
     0 = *(?x,*(s(?y_5),0)),
     0 = *(?x,*(?y,0)),
     0 = *(?x,*(+(?y_9,?z_9),0)),
     +(*(*(?x_5,*(?y_5,?y)),?y_4),*(?x_5,*(?y_5,?y))) = *(*(?x_5,?y_5),*(?y,s(?y_4))),
     +(*(0,?y_4),0) = *(?x,*(0,s(?y_4))),
     +(*(+(*(?x,?y_9),?x),?y_4),+(*(?x,?y_9),?x)) = *(?x,*(s(?y_9),s(?y_4))),
     +(*(*(?y,?x),?y_4),*(?y,?x)) = *(?x,*(?y,s(?y_4))),
     +(*(+(*(?x,?y_13),*(?x,?z_13)),?y_4),+(*(?x,?y_13),*(?x,?z_13))) = *(?x,*(+(?y_13,?z_13),s(?y_4))),
     *(?z,*(?x_1,*(?y_1,?y))) = *(*(?x_1,?y_1),*(?y,?z)),
     *(?z,0) = *(?x,*(0,?z)),
     *(?z,+(*(?x,?y_5),?x)) = *(?x,*(s(?y_5),?z)),
     *(?z,*(?y,?x)) = *(?x,*(?y,?z)),
     *(?z,+(*(?x,?y_9),*(?x,?z_9))) = *(?x,*(+(?y_9,?z_9),?z)),
     +(*(*(?x_9,*(?y_9,?y)),?y_8),*(*(?x_9,*(?y_9,?y)),?z_8)) = *(*(?x_9,?y_9),*(?y,+(?y_8,?z_8))),
     +(*(0,?y_8),*(0,?z_8)) = *(?x,*(0,+(?y_8,?z_8))),
     +(*(+(*(?x,?y_13),?x),?y_8),*(+(*(?x,?y_13),?x),?z_8)) = *(?x,*(s(?y_13),+(?y_8,?z_8))),
     +(*(*(?y,?x),?y_8),*(*(?y,?x),?z_8)) = *(?x,*(?y,+(?y_8,?z_8))),
     +(*(+(*(?x,?y_17),*(?x,?z_17)),?y_8),*(+(*(?x,?y_17),*(?x,?z_17)),?z_8)) = *(?x,*(+(?y_17,?z_17),+(?y_8,?z_8))),
     +(*(*(?x,?y),?y_4),*(?x,?y)) = *(?x,*(?y,s(?y_4))),
     *(?z,*(?x,?y)) = *(?x,*(?y,?z)),
     +(*(*(?x,?y),?y_8),*(*(?x,?y),?z_8)) = *(?x,*(?y,+(?y_8,?z_8))),
     *(*(?x_1,*(?y_1,?y)),?z) = *(*(?x_1,?y_1),*(?y,?z)),
     *(0,?z) = *(?x,*(0,?z)),
     *(+(*(?x,?y_5),?x),?z) = *(?x,*(s(?y_5),?z)),
     *(*(?y,?x),?z) = *(?x,*(?y,?z)),
     *(+(*(?x,?y_9),*(?x,?z_9)),?z) = *(?x,*(+(?y_9,?z_9),?z)),
     *(*(?x_2,*(?y_2,?y)),*(?z,?z_1)) = *(*(*(?x_2,?y_2),*(?y,?z)),?z_1),
     *(0,*(?z,?z_1)) = *(*(?x,*(0,?z)),?z_1),
     *(+(*(?x,?y_6),?x),*(?z,?z_1)) = *(*(?x,*(s(?y_6),?z)),?z_1),
     *(*(?y,?x),*(?z,?z_1)) = *(*(?x,*(?y,?z)),?z_1),
     *(+(*(?x,?y_10),*(?x,?z_10)),*(?z,?z_1)) = *(*(?x,*(+(?y_10,?z_10),?z)),?z_1),
     *(*(?x,?y),*(?z,?z_1)) = *(*(?x,*(?y,?z)),?z_1),
     0 = *(0,?x),
     +(*(?x,?y_4),?x) = *(s(?y_4),?x),
     *(?x_7,*(?y_7,?y)) = *(?y,*(?x_7,?y_7)),
     +(*(?x,?y_8),*(?x,?z_8)) = *(+(?y_8,?z_8),?x),
     *(?x,*(?y,?z_8)) = *(*(?y,?x),?z_8),
     *(?x_7,*(?y_7,?y)) = +(*(*(?x_7,?y_7),?y),*(*(?x_7,?y_7),0)),
     *(?x_7,*(?y_7,s(+(?y,?y_10)))) = +(*(*(?x_7,?y_7),?y),*(*(?x_7,?y_7),s(?y_10))),
     *(?x_7,*(?y_7,+(?x_13,+(?y_13,?z)))) = +(*(*(?x_7,?y_7),+(?x_13,?y_13)),*(*(?x_7,?y_7),?z)),
     *(?x_7,*(?y_7,+(?z,?y))) = +(*(*(?x_7,?y_7),?y),*(*(?x_7,?y_7),?z)),
     *(?y,?x) = +(*(?x,?y),*(?x,0)),
     *(s(+(?y,?y_3)),?x) = +(*(?x,?y),*(?x,s(?y_3))),
     *(+(?x_6,+(?y_6,?z)),?x) = +(*(?x,+(?x_6,?y_6)),*(?x,?z)),
     *(+(?z,?y),?x) = +(*(?x,?y),*(?x,?z)),
     *(?x_7,*(?y_7,+(?y,?z))) = +(*(*(?x_7,?y_7),?y),*(*(?x_7,?y_7),?z)),
     *(+(?y,?z),?x) = +(*(?x,?y),*(?x,?z)),
     *(?x,?y) = +(*(?x,?y),*(?x,0)),
     *(?x,s(+(?y,?y_3))) = +(*(?x,?y),*(?x,s(?y_3))),
     *(?x,+(?x_6,+(?y_6,?z))) = +(*(?x,+(?x_6,?y_6)),*(?x,?z)),
     *(?x,+(?z,?y)) = +(*(?x,?y),*(?x,?z)),
     *(?x,*(?y,?z_8)) = *(+(*(?x,?y),*(?x,0)),?z_8),
     *(?x,*(s(+(?y,?y_11)),?z_8)) = *(+(*(?x,?y),*(?x,s(?y_11))),?z_8),
     *(?x,*(+(?x_14,+(?y_14,?z)),?z_8)) = *(+(*(?x,+(?x_14,?y_14)),*(?x,?z)),?z_8),
     *(?x,*(+(?z,?y),?z_8)) = *(+(*(?x,?y),*(?x,?z)),?z_8),
     *(?x,*(+(?y,?z),?z_8)) = *(+(*(?x,?y),*(?x,?z)),?z_8) ]
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 <+(?x,?z_4), +(?x,+(0,?z_4))> by Rules <0, 4> preceded by [(+,1)]
 joinable by a reduction of rules <[], [([(+,2)],5),([(+,2)],0)]>
Critical Pair <+(s(+(?x_1,?y_1)),?z_4), +(?x_1,+(s(?y_1),?z_4))> by Rules <1, 4> preceded by [(+,1)]
 joinable by a reduction of rules <[([],5),([],1),([(s,1)],5),([(s,1)],4)], [([(+,2)],5),([(+,2)],1),([(+,2),(s,1)],5),([],1)]>
 joinable by a reduction of rules <[([],5),([],1),([(s,1)],5),([(s,1)],4)], [([(+,2)],5),([(+,2)],1),([],1),([(s,1),(+,2)],5)]>
Critical Pair <+(+(?y_5,?x_5),?z_4), +(?x_5,+(?y_5,?z_4))> by Rules <5, 4> preceded by [(+,1)]
 joinable by a reduction of rules <[([(+,1)],5),([],4)], []>
 joinable by a reduction of rules <[([],4),([(+,2)],5)], [([],5),([],4)]>
Critical Pair <*(0,?z_6), *(?x_2,*(0,?z_6))> by Rules <2, 6> preceded by [(*,1)]
 joinable by a reduction of rules <[([],7),([],2)], [([(*,2)],7),([(*,2)],2),([],2)]>
Critical Pair <*(+(*(?x_3,?y_3),?x_3),?z_6), *(?x_3,*(s(?y_3),?z_6))> by Rules <3, 6> preceded by [(*,1)]
 joinable by a reduction of rules <[([],7),([],8),([(+,2)],7),([(+,1)],7),([(+,1)],6)], [([(*,2)],7),([(*,2)],3),([(*,2),(+,1)],7),([],8)]>
 joinable by a reduction of rules <[([],7),([],8),([(+,2)],7),([(+,1)],7),([(+,1)],6)], [([(*,2)],7),([(*,2)],3),([],8),([(+,1),(*,2)],7)]>
 joinable by a reduction of rules <[([],7),([],8),([(+,1)],7),([(+,2)],7),([(+,1)],6)], [([(*,2)],7),([(*,2)],3),([(*,2),(+,1)],7),([],8)]>
 joinable by a reduction of rules <[([],7),([],8),([(+,1)],7),([(+,2)],7),([(+,1)],6)], [([(*,2)],7),([(*,2)],3),([],8),([(+,1),(*,2)],7)]>
 joinable by a reduction of rules <[([],7),([],8),([(+,1)],7),([(+,1)],6),([(+,2)],7)], [([(*,2)],7),([(*,2)],3),([(*,2),(+,1)],7),([],8)]>
 joinable by a reduction of rules <[([],7),([],8),([(+,1)],7),([(+,1)],6),([(+,2)],7)], [([(*,2)],7),([(*,2)],3),([],8),([(+,1),(*,2)],7)]>
 joinable by a reduction of rules <[([],7),([],8),([(+,1)],7),([(+,1)],6),([(+,1),(*,2)],7)], [([(*,2)],7),([(*,2)],3),([],8),([(+,2)],7)]>
 joinable by a reduction of rules <[([],7)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],3)]>
 joinable by a reduction of rules <[([],7)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],3)]>
 joinable by a reduction of rules <[([],7)], [([],7),([],6),([],7),([],6),([(*,2)],3)]>
 joinable by a reduction of rules <[([],7),([],8)], [([],7),([],6),([],7),([],3),([(+,1)],6)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([],7),([(*,2),(+,1)],7)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],3)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([],7),([(*,2),(+,1)],7)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],3)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([],7),([(*,2),(+,1)],7)], [([],7),([],6),([],7),([],6),([(*,2)],3)]>
 joinable by a reduction of rules <[([(*,1)],5),([],7),([(*,2)],5)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],3)]>
 joinable by a reduction of rules <[([(*,1)],5),([],7),([(*,2)],5)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],3)]>
 joinable by a reduction of rules <[([(*,1)],5),([],7),([(*,2)],5)], [([],7),([],6),([],7),([],6),([(*,2)],3)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([],7),([(*,2),(+,1)],7),([],8)], [([],7),([],6),([],7),([],3),([(+,1)],6)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([],7),([],8),([(+,2)],7)], [([(*,2)],7),([(*,2)],3),([],8),([(+,1)],7),([(+,1)],6)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([],7),([],8),([(+,1),(*,2)],7)], [([],7),([],6),([],7),([],3),([(+,1)],6)]>
 joinable by a reduction of rules <[([(*,1)],5),([],7),([(*,2)],5),([],8)], [([],7),([],6),([],7),([],3),([(+,1)],6)]>
 joinable by a reduction of rules <[([(*,1)],5),([],7),([],8),([],5)], [([],7),([],6),([],7),([],3),([(+,1)],6)]>
 joinable by a reduction of rules <[([],7),([(*,2),(+,1)],7),([],8),([(+,2)],7)], [([(*,2)],7),([(*,2)],3),([],8),([(+,1)],7),([(+,1)],6)]>
 joinable by a reduction of rules <[([],7),([(*,2),(+,1)],7),([],8),([(+,1),(*,2)],7)], [([],7),([],6),([],7),([],3),([(+,1)],6)]>
 joinable by a reduction of rules <[([],7),([(*,2)],5),([],8),([],5)], [([],7),([],6),([],7),([],3),([(+,1)],6)]>
 joinable by a reduction of rules <[([],7),([],8),([(+,2)],7),([(+,1),(*,2)],7)], [([(*,2)],7),([(*,2)],3),([],8),([(+,1)],7),([(+,1)],6)]>
 joinable by a reduction of rules <[([],7),([],8),([(+,1),(*,2)],7),([(+,2)],7)], [([(*,2)],7),([(*,2)],3),([],8),([(+,1)],7),([(+,1)],6)]>
 joinable by a reduction of rules <[([],7),([],8),([(+,1)],7),([(+,1)],6)], [([(*,2)],7),([(*,2)],3),([(*,2),(+,1)],7),([],8),([(+,2)],7)]>
 joinable by a reduction of rules <[([],7),([],8),([(+,1)],7),([(+,1)],6)], [([(*,2)],7),([(*,2)],3),([],8),([(+,2)],7),([(+,1),(*,2)],7)]>
 joinable by a reduction of rules <[([],7),([],8),([(+,1)],7),([(+,1)],6)], [([(*,2)],7),([(*,2)],3),([],8),([(+,1),(*,2)],7),([(+,2)],7)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([(*,1)],5),([(*,1),(+,2)],7),([],7),([(*,2)],5)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],3)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([(*,1)],5),([(*,1),(+,2)],7),([],7),([(*,2)],5)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],3)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([(*,1)],5),([(*,1),(+,2)],7),([],7),([(*,2)],5)], [([],7),([],6),([],7),([],6),([(*,2)],3)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([(*,1)],5),([],7),([(*,2),(+,2)],7),([(*,2)],5)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],3)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([(*,1)],5),([],7),([(*,2),(+,2)],7),([(*,2)],5)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],3)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([(*,1)],5),([],7),([(*,2),(+,2)],7),([(*,2)],5)], [([],7),([],6),([],7),([],6),([(*,2)],3)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([(*,1)],5),([],7),([(*,2)],5),([(*,2),(+,1)],7)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],3)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([(*,1)],5),([],7),([(*,2)],5),([(*,2),(+,1)],7)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],3)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([(*,1)],5),([],7),([(*,2)],5),([(*,2),(+,1)],7)], [([],7),([],6),([],7),([],6),([(*,2)],3)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([],7),([(*,2)],5),([(*,2),(+,2)],7),([(*,2)],5)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],3)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([],7),([(*,2)],5),([(*,2),(+,2)],7),([(*,2)],5)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],3)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([],7),([(*,2)],5),([(*,2),(+,2)],7),([(*,2)],5)], [([],7),([],6),([],7),([],6),([(*,2)],3)]>
 joinable by a reduction of rules <[([(*,1)],5),([(*,1),(+,2)],7),([(*,1)],5),([],7),([(*,2),(+,1)],7)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],3)]>
 joinable by a reduction of rules <[([(*,1)],5),([(*,1),(+,2)],7),([(*,1)],5),([],7),([(*,2),(+,1)],7)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],3)]>
 joinable by a reduction of rules <[([(*,1)],5),([(*,1),(+,2)],7),([(*,1)],5),([],7),([(*,2),(+,1)],7)], [([],7),([],6),([],7),([],6),([(*,2)],3)]>
 joinable by a reduction of rules <[([(*,1)],5),([(*,1),(+,2)],7),([],7),([(*,2),(+,2)],7),([(*,2)],5)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],3)]>
 joinable by a reduction of rules <[([(*,1)],5),([(*,1),(+,2)],7),([],7),([(*,2),(+,2)],7),([(*,2)],5)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],3)]>
 joinable by a reduction of rules <[([(*,1)],5),([(*,1),(+,2)],7),([],7),([(*,2),(+,2)],7),([(*,2)],5)], [([],7),([],6),([],7),([],6),([(*,2)],3)]>
 joinable by a reduction of rules <[([(*,1)],5),([(*,1),(+,2)],7),([],7),([(*,2)],5),([(*,2),(+,1)],7)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],3)]>
 joinable by a reduction of rules <[([(*,1)],5),([(*,1),(+,2)],7),([],7),([(*,2)],5),([(*,2),(+,1)],7)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],3)]>
 joinable by a reduction of rules <[([(*,1)],5),([(*,1),(+,2)],7),([],7),([(*,2)],5),([(*,2),(+,1)],7)], [([],7),([],6),([],7),([],6),([(*,2)],3)]>
 joinable by a reduction of rules <[([(*,1)],5),([],7),([(*,2),(+,2)],7),([(*,2)],5),([(*,2),(+,1)],7)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],3)]>
 joinable by a reduction of rules <[([(*,1)],5),([],7),([(*,2),(+,2)],7),([(*,2)],5),([(*,2),(+,1)],7)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],3)]>
 joinable by a reduction of rules <[([(*,1)],5),([],7),([(*,2),(+,2)],7),([(*,2)],5),([(*,2),(+,1)],7)], [([],7),([],6),([],7),([],6),([(*,2)],3)]>
Critical Pair <*(*(?y_7,?x_7),?z_6), *(?x_7,*(?y_7,?z_6))> by Rules <7, 6> preceded by [(*,1)]
 joinable by a reduction of rules <[([(*,1)],7),([],6)], []>
 joinable by a reduction of rules <[([],6),([(*,2)],7)], [([],7),([],6)]>
Critical Pair <*(+(*(?x_8,?y_8),*(?x_8,?z_8)),?z_6), *(?x_8,*(+(?y_8,?z_8),?z_6))> by Rules <8, 6> preceded by [(*,1)]
 joinable by a reduction of rules <[([],7)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([],7)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([],7)], [([],7),([],6),([],7),([],6),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,2)],7),([],7),([(*,2),(+,2)],7)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,2)],7),([],7),([(*,2),(+,2)],7)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,2)],7),([],7),([(*,2),(+,2)],7)], [([],7),([],6),([],7),([],6),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([],7),([(*,2),(+,1)],7)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([],7),([(*,2),(+,1)],7)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([],7),([(*,2),(+,1)],7)], [([],7),([],6),([],7),([],6),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1)],5),([],7),([(*,2)],5)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1)],5),([],7),([(*,2)],5)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1)],5),([],7),([(*,2)],5)], [([],7),([],6),([],7),([],6),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,2)],7),([(*,1),(+,1)],7),([(*,1),(+,2)],7),([],7),([(*,2),(+,1)],7)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,2)],7),([(*,1),(+,1)],7),([(*,1),(+,2)],7),([],7),([(*,2),(+,1)],7)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,2)],7),([(*,1),(+,1)],7),([(*,1),(+,2)],7),([],7),([(*,2),(+,1)],7)], [([],7),([],6),([],7),([],6),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,2)],7),([(*,1),(+,1)],7),([],7),([(*,2),(+,2)],7),([(*,2),(+,1)],7)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,2)],7),([(*,1),(+,1)],7),([],7),([(*,2),(+,2)],7),([(*,2),(+,1)],7)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,2)],7),([(*,1),(+,1)],7),([],7),([(*,2),(+,2)],7),([(*,2),(+,1)],7)], [([],7),([],6),([],7),([],6),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,2)],7),([(*,1),(+,1)],7),([],7),([(*,2),(+,1)],7),([(*,2),(+,2)],7)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,2)],7),([(*,1),(+,1)],7),([],7),([(*,2),(+,1)],7),([(*,2),(+,2)],7)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,2)],7),([(*,1),(+,1)],7),([],7),([(*,2),(+,1)],7),([(*,2),(+,2)],7)], [([],7),([],6),([],7),([],6),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,2)],7),([(*,1)],5),([(*,1),(+,1)],7),([],7),([(*,2)],5)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,2)],7),([(*,1)],5),([(*,1),(+,1)],7),([],7),([(*,2)],5)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,2)],7),([(*,1)],5),([(*,1),(+,1)],7),([],7),([(*,2)],5)], [([],7),([],6),([],7),([],6),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,2)],7),([(*,1)],5),([],7),([(*,2),(+,1)],7),([(*,2)],5)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,2)],7),([(*,1)],5),([],7),([(*,2),(+,1)],7),([(*,2)],5)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,2)],7),([(*,1)],5),([],7),([(*,2),(+,1)],7),([(*,2)],5)], [([],7),([],6),([],7),([],6),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,2)],7),([(*,1)],5),([],7),([(*,2)],5),([(*,2),(+,2)],7)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,2)],7),([(*,1)],5),([],7),([(*,2)],5),([(*,2),(+,2)],7)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,2)],7),([(*,1)],5),([],7),([(*,2)],5),([(*,2),(+,2)],7)], [([],7),([],6),([],7),([],6),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,2)],7),([],7),([(*,2),(+,1)],7),([(*,2),(+,2)],7),([(*,2),(+,1)],7)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,2)],7),([],7),([(*,2),(+,1)],7),([(*,2),(+,2)],7),([(*,2),(+,1)],7)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,2)],7),([],7),([(*,2),(+,1)],7),([(*,2),(+,2)],7),([(*,2),(+,1)],7)], [([],7),([],6),([],7),([],6),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,2)],7),([],7),([(*,2)],5),([(*,2),(+,1)],7),([(*,2)],5)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,2)],7),([],7),([(*,2)],5),([(*,2),(+,1)],7),([(*,2)],5)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,2)],7),([],7),([(*,2)],5),([(*,2),(+,1)],7),([(*,2)],5)], [([],7),([],6),([],7),([],6),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([(*,1),(+,2)],7),([(*,1),(+,1)],7),([],7),([(*,2),(+,2)],7)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([(*,1),(+,2)],7),([(*,1),(+,1)],7),([],7),([(*,2),(+,2)],7)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([(*,1),(+,2)],7),([(*,1),(+,1)],7),([],7),([(*,2),(+,2)],7)], [([],7),([],6),([],7),([],6),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([(*,1),(+,2)],7),([],7),([(*,2),(+,2)],7),([(*,2),(+,1)],7)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([(*,1),(+,2)],7),([],7),([(*,2),(+,2)],7),([(*,2),(+,1)],7)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([(*,1),(+,2)],7),([],7),([(*,2),(+,2)],7),([(*,2),(+,1)],7)], [([],7),([],6),([],7),([],6),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([(*,1),(+,2)],7),([],7),([(*,2),(+,1)],7),([(*,2),(+,2)],7)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([(*,1),(+,2)],7),([],7),([(*,2),(+,1)],7),([(*,2),(+,2)],7)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([(*,1),(+,2)],7),([],7),([(*,2),(+,1)],7),([(*,2),(+,2)],7)], [([],7),([],6),([],7),([],6),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([(*,1)],5),([(*,1),(+,2)],7),([],7),([(*,2)],5)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([(*,1)],5),([(*,1),(+,2)],7),([],7),([(*,2)],5)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([(*,1)],5),([(*,1),(+,2)],7),([],7),([(*,2)],5)], [([],7),([],6),([],7),([],6),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([(*,1)],5),([],7),([(*,2),(+,2)],7),([(*,2)],5)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([(*,1)],5),([],7),([(*,2),(+,2)],7),([(*,2)],5)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([(*,1)],5),([],7),([(*,2),(+,2)],7),([(*,2)],5)], [([],7),([],6),([],7),([],6),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([(*,1)],5),([],7),([(*,2)],5),([(*,2),(+,1)],7)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([(*,1)],5),([],7),([(*,2)],5),([(*,2),(+,1)],7)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([(*,1)],5),([],7),([(*,2)],5),([(*,2),(+,1)],7)], [([],7),([],6),([],7),([],6),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([],7),([(*,2),(+,2)],7),([(*,2),(+,1)],7),([(*,2),(+,2)],7)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([],7),([(*,2),(+,2)],7),([(*,2),(+,1)],7),([(*,2),(+,2)],7)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([],7),([(*,2),(+,2)],7),([(*,2),(+,1)],7),([(*,2),(+,2)],7)], [([],7),([],6),([],7),([],6),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([],7),([(*,2)],5),([(*,2),(+,2)],7),([(*,2)],5)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([],7),([(*,2)],5),([(*,2),(+,2)],7),([(*,2)],5)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1),(+,1)],7),([],7),([(*,2)],5),([(*,2),(+,2)],7),([(*,2)],5)], [([],7),([],6),([],7),([],6),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1)],5),([(*,1),(+,2)],7),([(*,1)],5),([],7),([(*,2),(+,1)],7)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1)],5),([(*,1),(+,2)],7),([(*,1)],5),([],7),([(*,2),(+,1)],7)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1)],5),([(*,1),(+,2)],7),([(*,1)],5),([],7),([(*,2),(+,1)],7)], [([],7),([],6),([],7),([],6),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1)],5),([(*,1),(+,2)],7),([],7),([(*,2),(+,2)],7),([(*,2)],5)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1)],5),([(*,1),(+,2)],7),([],7),([(*,2),(+,2)],7),([(*,2)],5)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1)],5),([(*,1),(+,2)],7),([],7),([(*,2),(+,2)],7),([(*,2)],5)], [([],7),([],6),([],7),([],6),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1)],5),([(*,1),(+,2)],7),([],7),([(*,2)],5),([(*,2),(+,1)],7)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1)],5),([(*,1),(+,2)],7),([],7),([(*,2)],5),([(*,2),(+,1)],7)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1)],5),([(*,1),(+,2)],7),([],7),([(*,2)],5),([(*,2),(+,1)],7)], [([],7),([],6),([],7),([],6),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1)],5),([(*,1),(+,1)],7),([(*,1)],5),([],7),([(*,2),(+,2)],7)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1)],5),([(*,1),(+,1)],7),([(*,1)],5),([],7),([(*,2),(+,2)],7)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1)],5),([(*,1),(+,1)],7),([(*,1)],5),([],7),([(*,2),(+,2)],7)], [([],7),([],6),([],7),([],6),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1)],5),([(*,1),(+,1)],7),([],7),([(*,2),(+,1)],7),([(*,2)],5)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1)],5),([(*,1),(+,1)],7),([],7),([(*,2),(+,1)],7),([(*,2)],5)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1)],5),([(*,1),(+,1)],7),([],7),([(*,2),(+,1)],7),([(*,2)],5)], [([],7),([],6),([],7),([],6),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1)],5),([(*,1),(+,1)],7),([],7),([(*,2)],5),([(*,2),(+,2)],7)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1)],5),([(*,1),(+,1)],7),([],7),([(*,2)],5),([(*,2),(+,2)],7)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1)],5),([(*,1),(+,1)],7),([],7),([(*,2)],5),([(*,2),(+,2)],7)], [([],7),([],6),([],7),([],6),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1)],5),([],7),([(*,2),(+,2)],7),([(*,2)],5),([(*,2),(+,1)],7)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1)],5),([],7),([(*,2),(+,2)],7),([(*,2)],5),([(*,2),(+,1)],7)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1)],5),([],7),([(*,2),(+,2)],7),([(*,2)],5),([(*,2),(+,1)],7)], [([],7),([],6),([],7),([],6),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1)],5),([],7),([(*,2),(+,1)],7),([(*,2)],5),([(*,2),(+,2)],7)], [([(*,2)],7),([],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1)],5),([],7),([(*,2),(+,1)],7),([(*,2)],5),([(*,2),(+,2)],7)], [([],7),([(*,1)],7),([],6),([(*,2)],7),([(*,2)],8)]>
 joinable by a reduction of rules <[([(*,1)],5),([],7),([(*,2),(+,1)],7),([(*,2)],5),([(*,2),(+,2)],7)], [([],7),([],6),([],7),([],6),([(*,2)],8)]>
Critical Pair <*(?x_8,?x), +(*(?x_8,?x),*(?x_8,0))> by Rules <0, 8> preceded by [(*,2)]
 joinable by a reduction of rules <[], [([(+,2)],2),([],0)]>
Critical Pair <*(?x_8,s(+(?x_1,?y_1))), +(*(?x_8,?x_1),*(?x_8,s(?y_1)))> by Rules <1, 8> preceded by [(*,2)]
 joinable by a reduction of rules <[([],3),([(+,1)],8),([],4)], [([(+,2)],3)]>
 joinable by a reduction of rules <[([],3),([(+,1)],8),([],4)], [([(+,1)],7),([(+,2)],3),([(+,1)],7)]>
 joinable by a reduction of rules <[([],3),([(+,1)],8),([],4)], [([],5),([(+,1)],3),([],5)]>
Critical Pair <*(?x_8,+(?x_4,+(?y_4,?z_4))), +(*(?x_8,+(?x_4,?y_4)),*(?x_8,?z_4))> by Rules <4, 8> preceded by [(*,2)]
 joinable by a reduction of rules <[([],8),([(+,2)],8)], [([(+,1)],8),([],4)]>
Critical Pair <*(?x_8,+(?y_5,?x_5)), +(*(?x_8,?x_5),*(?x_8,?y_5))> by Rules <5, 8> preceded by [(*,2)]
 joinable by a reduction of rules <[([],8)], [([],5)]>
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 <[([],4),([(+,2)],4)], [([],4)]>
Critical Pair <*(*(?x,*(?y,?z)),?z_1), *(*(?x,?y),*(?z,?z_1))> by Rules <6, 6> preceded by [(*,1)]
 joinable by a reduction of rules <[([],6),([(*,2)],6)], [([],6)]>
Critical Pair <+(?x_4,+(?y_4,0)), +(?x_4,?y_4)> by Rules <4, 0> preceded by []
 joinable by a reduction of rules <[([(+,2)],0)], []>
Critical Pair <+(0,?x_5), ?x_5> by Rules <5, 0> preceded by []
 joinable by a reduction of rules <[([],5),([],0)], []>
Critical Pair <+(?x_4,+(?y_4,s(?y_1))), s(+(+(?x_4,?y_4),?y_1))> by Rules <4, 1> preceded by []
 joinable by a reduction of rules <[([(+,2)],1),([],1)], [([(s,1)],4)]>
Critical Pair <+(s(?y_1),?x_5), s(+(?x_5,?y_1))> by Rules <5, 1> preceded by []
 joinable by a reduction of rules <[([],5),([],1)], []>
Critical Pair <*(?x_6,*(?y_6,0)), 0> by Rules <6, 2> preceded by []
 joinable by a reduction of rules <[([(*,2)],2),([],2)], []>
Critical Pair <*(0,?x_7), 0> by Rules <7, 2> preceded by []
 joinable by a reduction of rules <[([],7),([],2)], []>
Critical Pair <*(?x_6,*(?y_6,s(?y_3))), +(*(*(?x_6,?y_6),?y_3),*(?x_6,?y_6))> by Rules <6, 3> preceded by []
 joinable by a reduction of rules <[([(*,2)],3),([],8)], [([(+,1)],6)]>
Critical Pair <*(s(?y_3),?x_7), +(*(?x_7,?y_3),?x_7)> by Rules <7, 3> preceded by []
 joinable by a reduction of rules <[([],7),([],3)], []>
Critical Pair <+(?y_5,+(?x_4,?y_4)), +(?x_4,+(?y_4,?y_5))> by Rules <5, 4> preceded by []
 joinable by a reduction of rules <[([],5),([],4)], []>
Critical Pair <*(?y_7,*(?x_6,?y_6)), *(?x_6,*(?y_6,?y_7))> by Rules <7, 6> preceded by []
 joinable by a reduction of rules <[([],7),([],6)], []>
Critical Pair <+(*(*(?x_6,?y_6),?y_8),*(*(?x_6,?y_6),?z_8)), *(?x_6,*(?y_6,+(?y_8,?z_8)))> by Rules <8, 6> preceded by []
 joinable by a reduction of rules <[([(+,2)],6),([(+,1)],6)], [([(*,2)],8),([],8)]>
 joinable by a reduction of rules <[([(+,1)],6),([(+,2)],6)], [([(*,2)],8),([],8)]>
Critical Pair <+(*(?x_8,?y_8),*(?x_8,?z_8)), *(+(?y_8,?z_8),?x_8)> by Rules <8, 7> preceded by []
 joinable by a reduction of rules <[], [([],7),([],8)]>
unknown Diagram Decreasing
   [ +(?x,0) -> ?x,
     +(?x_1,s(?y_1)) -> s(+(?x_1,?y_1)),
     *(?x_2,0) -> 0,
     *(?x_3,s(?y_3)) -> +(*(?x_3,?y_3),?x_3),
     +(+(?x_4,?y_4),?z_4) -> +(?x_4,+(?y_4,?z_4)),
     +(?x_5,?y_5) -> +(?y_5,?x_5),
     *(*(?x_6,?y_6),?z_6) -> *(?x_6,*(?y_6,?z_6)),
     *(?x_7,?y_7) -> *(?y_7,?x_7),
     *(?x_8,+(?y_8,?z_8)) -> +(*(?x_8,?y_8),*(?x_8,?z_8)) ]
Sort Assignment:
 * : 29*29=>29
 + : 29*29=>29
 0 : =>29
 s : 29=>29
non-linear variables: {?x_3,?x_8}
non-linear types: {29}
types leq non-linear types: {29}
rules applicable to terms of non-linear types:
   [ +(?x,0) -> ?x,
     +(?x_1,s(?y_1)) -> s(+(?x_1,?y_1)),
     *(?x_2,0) -> 0,
     *(?x_3,s(?y_3)) -> +(*(?x_3,?y_3),?x_3),
     +(+(?x_4,?y_4),?z_4) -> +(?x_4,+(?y_4,?z_4)),
     +(?x_5,?y_5) -> +(?y_5,?x_5),
     *(*(?x_6,?y_6),?z_6) -> *(?x_6,*(?y_6,?z_6)),
     *(?x_7,?y_7) -> *(?y_7,?x_7),
     *(?x_8,+(?y_8,?z_8)) -> +(*(?x_8,?y_8),*(?x_8,?z_8)) ]
NLR:
0: {}
1: {}
2: {}
3: {0,1,2,3,4,5,6,7,8}
4: {}
5: {}
6: {}
7: {}
8: {0,1,2,3,4,5,6,7,8}
unknown innermost-termination for terms of non-linear types
unknown Quasi-Linear & Linearized-Decreasing
   [ +(?x,0) -> ?x,
     +(?x_1,s(?y_1)) -> s(+(?x_1,?y_1)),
     *(?x_2,0) -> 0,
     *(?x_3,s(?y_3)) -> +(*(?x_3,?y_3),?x_3),
     +(+(?x_4,?y_4),?z_4) -> +(?x_4,+(?y_4,?z_4)),
     +(?x_5,?y_5) -> +(?y_5,?x_5),
     *(*(?x_6,?y_6),?z_6) -> *(?x_6,*(?y_6,?z_6)),
     *(?x_7,?y_7) -> *(?y_7,?x_7),
     *(?x_8,+(?y_8,?z_8)) -> +(*(?x_8,?y_8),*(?x_8,?z_8)) ]
Sort Assignment:
 * : 29*29=>29
 + : 29*29=>29
 0 : =>29
 s : 29=>29
non-linear variables: {?x_3,?x_8}
non-linear types: {29}
types leq non-linear types: {29}
rules applicable to terms of non-linear types:
   [ +(?x,0) -> ?x,
     +(?x_1,s(?y_1)) -> s(+(?x_1,?y_1)),
     *(?x_2,0) -> 0,
     *(?x_3,s(?y_3)) -> +(*(?x_3,?y_3),?x_3),
     +(+(?x_4,?y_4),?z_4) -> +(?x_4,+(?y_4,?z_4)),
     +(?x_5,?y_5) -> +(?y_5,?x_5),
     *(*(?x_6,?y_6),?z_6) -> *(?x_6,*(?y_6,?z_6)),
     *(?x_7,?y_7) -> *(?y_7,?x_7),
     *(?x_8,+(?y_8,?z_8)) -> +(*(?x_8,?y_8),*(?x_8,?z_8)) ]
unknown innermost-termination for terms of non-linear types
unknown Strongly Quasi-Linear & Hierarchically Decreasing
check Non-Confluence...
obtain 19 rules by 3 steps unfolding
strenghten *(?x_11,0) and 0
strenghten *(0,?x_7) and 0
strenghten +(?x_15,0) and ?x_15
strenghten +(0,?x_5) and ?x_5
strenghten *(?x_18,?y_18) and *(?y_18,?x_18)
strenghten s(+(0,?y_1)) and s(?y_1)
strenghten *(?x_6,*(?y_6,0)) and 0
strenghten +(*(0,?y_3),0) and 0
strenghten s(+(?x_5,?y_1)) and +(s(?y_1),?x_5)
strenghten *(?x_2,*(0,?z_6)) and *(0,?z_6)
strenghten *(0,*(?x_11,?z_6)) and *(0,?z_6)
strenghten +(?x,+(0,?z_4)) and +(?x,?z_4)
strenghten +(?x_4,+(?y_4,0)) and +(?x_4,?y_4)
strenghten +(0,+(?x_15,?z_4)) and +(?x_15,?z_4)
strenghten +(*(0,?y_8),*(0,?z_8)) and 0
strenghten +(*(?x_7,?y_3),?x_7) and *(s(?y_3),?x_7)
strenghten +(*(?x_17,?y_3),?x_17) and *(?x_17,s(?y_3))
strenghten *(?x_6,*(?y_6,?y_7)) and *(?y_7,*(?x_6,?y_6))
strenghten *(?x_6,*(?y_6,?y_17)) and *(*(?x_6,?y_6),?y_17)
strenghten *(?x_7,*(?y_7,?z_6)) and *(*(?y_7,?x_7),?z_6)
strenghten +(?x_4,+(?y_4,?y_5)) and +(?y_5,+(?x_4,?y_4))
strenghten +(?x_5,+(?y_5,?z_4)) and +(+(?y_5,?x_5),?z_4)
strenghten +(*(?x_8,?x),*(?x_8,0)) and *(?x_8,?x)
strenghten +(*(?x_8,0),*(?x_8,?x_15)) and *(?x_8,?x_15)
strenghten +(?x_1,+(s(?y_1),?z_4)) and +(s(+(?x_1,?y_1)),?z_4)
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,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     *(?x,0) -> 0,
     *(?x,s(?y)) -> +(*(?x,?y),?x),
     *(?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:
  *:= (1)*x1+(3)*x1*x2+(1)*x2
  +:= (3)+(1)*x1+(1)*x2
  0:= (8)
  s:= (8)+(1)*x1
retract +(?x,0) -> ?x
retract *(?x,s(?y)) -> +(*(?x,?y),?x)
Polynomial Interpretation:
  *:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
  +:= (1)+(1)*x1+(1)*x2
  0:= (2)
  s:= (14)+(1)*x1
retract +(?x,0) -> ?x
retract *(?x,0) -> 0
retract *(?x,s(?y)) -> +(*(?x,?y),?x)
Polynomial Interpretation:
  *:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
  +:= (2)+(1)*x1+(1)*x2
  0:= (4)
  s:= (1)*x1
retract +(?x,0) -> ?x
retract *(?x,0) -> 0
retract *(?x,s(?y)) -> +(*(?x,?y),?x)
retract *(?x,+(?y,?z)) -> +(*(?x,?y),*(?x,?z))
Polynomial Interpretation:
  *:= (1)*x1+(1)*x2
  +:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
  0:= (9)
  s:= (1)+(1)*x1
relatively terminating
unknown Huet (modulo AC)
check by Reduction-Preserving Completion...
STEP: 1 (parallel)
S:
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     *(?x,0) -> 0,
     *(?x,s(?y)) -> +(*(?x,?y),?x),
     *(?x,+(?y,?z)) -> +(*(?x,?y),*(?x,?z)) ]
P:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     *(?x,?y) -> *(?y,?x) ]
S: terminating
CP(S,S):
<*(?x_4,?x), +(*(?x_4,?x),*(?x_4,0))> --> <*(?x_4,?x), *(?x_4,?x)> => yes
<*(?x_4,s(+(?x_1,?y_1))), +(*(?x_4,?x_1),*(?x_4,s(?y_1)))> --> <+(+(*(?x_4,?x_1),*(?x_4,?y_1)),?x_4), +(*(?x_4,?x_1),+(*(?x_4,?y_1),?x_4))> => yes
PCP_in(symP,S):
<*(?x,+(?x_4,?y_4)), +(*(?x,?y_4),*(?x,?x_4))> --> <+(*(?x,?x_4),*(?x,?y_4)), +(*(?x,?y_4),*(?x,?x_4))> => no
<*(?x,+(+(?x_3,?y_3),?z_3)), +(*(?x,?x_3),*(?x,+(?y_3,?z_3)))> --> <+(+(*(?x,?x_3),*(?x,?y_3)),*(?x,?z_3)), +(*(?x,?x_3),+(*(?x,?y_3),*(?x,?z_3)))> => no
<*(?x,+(?x_1,+(?y_1,?z_1))), +(*(?x,+(?x_1,?y_1)),*(?x,?z_1))> --> <+(*(?x,?x_1),+(*(?x,?y_1),*(?x,?z_1))), +(+(*(?x,?x_1),*(?x,?y_1)),*(?x,?z_1))> => no
CP(S,symP):
<+(?x_1,?y_1), +(?x_1,+(?y_1,0))> --> <+(?x_1,?y_1), +(?x_1,?y_1)> => yes
<+(?x,?z_1), +(?x,+(0,?z_1))> --> <+(?x,?z_1), +(?x,+(0,?z_1))> => no
<+(?x_1,?x), +(+(?x_1,?x),0)> --> <+(?x_1,?x), +(?x_1,?x)> => yes
<?x, +(0,?x)> --> <?x, +(0,?x)> => no
<s(+(+(?x_1,?y_1),?y)), +(?x_1,+(?y_1,s(?y)))> --> <s(+(+(?x_1,?y_1),?y)), s(+(?x_1,+(?y_1,?y)))> => yes
<+(s(+(?x,?y)),?z_1), +(?x,+(s(?y),?z_1))> --> <+(s(+(?x,?y)),?z_1), +(?x,+(s(?y),?z_1))> => no
<+(?x_1,s(+(?x,?y))), +(+(?x_1,?x),s(?y))> --> <s(+(?x_1,+(?x,?y))), s(+(+(?x_1,?x),?y))> => yes
<s(+(?x,?y)), +(s(?y),?x)> --> <s(+(?x,?y)), +(s(?y),?x)> => no
<0, *(?x_1,*(?y_1,0))> --> <0, 0> => yes
<*(0,?z_1), *(?x,*(0,?z_1))> --> <*(0,?z_1), *(?x,*(0,?z_1))> => no
<*(?x_1,0), *(*(?x_1,?x),0)> --> <0, 0> => yes
<0, *(0,?x)> --> <0, *(0,?x)> => no
<+(*(*(?x_1,?y_1),?y),*(?x_1,?y_1)), *(?x_1,*(?y_1,s(?y)))> --> <+(*(*(?x_1,?y_1),?y),*(?x_1,?y_1)), +(*(?x_1,*(?y_1,?y)),*(?x_1,?y_1))> => yes
<*(+(*(?x,?y),?x),?z_1), *(?x,*(s(?y),?z_1))> --> <*(+(*(?x,?y),?x),?z_1), *(?x,*(s(?y),?z_1))> => no
<*(?x_1,+(*(?x,?y),?x)), *(*(?x_1,?x),s(?y))> --> <+(*(?x_1,*(?x,?y)),*(?x_1,?x)), +(*(*(?x_1,?x),?y),*(?x_1,?x))> => yes
<+(*(?x,?y),?x), *(s(?y),?x)> --> <+(*(?x,?y),?x), *(s(?y),?x)> => no
<+(*(*(?x_1,?y_1),?y),*(*(?x_1,?y_1),?z)), *(?x_1,*(?y_1,+(?y,?z)))> --> <+(*(*(?x_1,?y_1),?y),*(*(?x_1,?y_1),?z)), +(*(?x_1,*(?y_1,?y)),*(?x_1,*(?y_1,?z)))> => yes
<*(+(*(?x,?y),*(?x,?z)),?z_1), *(?x,*(+(?y,?z),?z_1))> --> <*(+(*(?x,?y),*(?x,?z)),?z_1), *(?x,*(+(?y,?z),?z_1))> => no
<*(?x_1,+(*(?x,?y),*(?x,?z))), *(*(?x_1,?x),+(?y,?z))> --> <+(*(?x_1,*(?x,?y)),*(?x_1,*(?x,?z))), +(*(*(?x_1,?x),?y),*(*(?x_1,?x),?z))> => yes
<+(*(?x,?y),*(?x,?z)), *(+(?y,?z),?x)> --> <+(*(?x,?y),*(?x,?z)), *(+(?y,?z),?x)> => no
check joinability condition:
check modulo joinability of +(*(?x,?x_4),*(?x,?y_4)) and +(*(?x,?y_4),*(?x,?x_4)): joinable by {2}
check modulo joinability of +(+(*(?x,?x_3),*(?x,?y_3)),*(?x,?z_3)) and +(*(?x,?x_3),+(*(?x,?y_3),*(?x,?z_3))): joinable by {3}
check modulo joinability of +(*(?x,?x_1),+(*(?x,?y_1),*(?x,?z_1))) and +(+(*(?x,?x_1),*(?x,?y_1)),*(?x,?z_1)): joinable by {5}
check modulo reachablity from +(?x,?z_1) to +(?x,+(0,?z_1)): maybe not reachable
check modulo reachablity from ?x to +(0,?x): maybe not reachable
check modulo reachablity from +(s(+(?x,?y)),?z_1) to +(?x,+(s(?y),?z_1)): maybe not reachable
check modulo reachablity from s(+(?x,?y)) to +(s(?y),?x): maybe not reachable
check modulo reachablity from *(0,?z_1) to *(?x,*(0,?z_1)): maybe not reachable
check modulo reachablity from 0 to *(0,?x): maybe not reachable
check modulo reachablity from *(+(*(?x,?y),?x),?z_1) to *(?x,*(s(?y),?z_1)): maybe not reachable
check modulo reachablity from +(*(?x,?y),?x) to *(s(?y),?x): maybe not reachable
check modulo reachablity from *(+(*(?x,?y),*(?x,?z)),?z_1) to *(?x,*(+(?y,?z),?z_1)): maybe not reachable
check modulo reachablity from +(*(?x,?y),*(?x,?z)) to *(+(?y,?z),?x): maybe not reachable
failed
failure(Step 1)
   [ +(0,?x) -> ?x,
     +(s(?y),?x) -> s(+(?x,?y)),
     *(0,?x) -> 0,
     *(s(?y),?x) -> +(*(?x,?y),?x),
     *(+(?y,?z),?x) -> +(*(?x,?y),*(?x,?z)) ]
Added S-Rules:
   [ +(0,?x) -> ?x,
     +(s(?y),?x) -> s(+(?x,?y)),
     *(0,?x) -> 0,
     *(s(?y),?x) -> +(*(?x,?y),?x),
     *(+(?y,?z),?x) -> +(*(?x,?y),*(?x,?z)) ]
Added P-Rules:
   [ ]
replace: *(?x,+(?y,?z)) -> +(*(?x,?y),*(?x,?z)) => *(?x,+(?y,?z)) -> +(*(?x,?y),*(?z,?x))
replace: *(?x,+(?y,?z)) -> +(*(?x,?y),*(?x,?z)) => *(?x,+(?y,?z)) -> +(*(?x,?z),*(?x,?y))
replace: *(?x,+(?y,?z)) -> +(*(?x,?y),*(?x,?z)) => *(?x,+(?y,?z)) -> +(*(?y,?x),*(?x,?z))
replace: *(?x,s(?y)) -> +(*(?x,?y),?x) => *(?x,s(?y)) -> +(?x,*(?x,?y))
replace: *(?x,s(?y)) -> +(*(?x,?y),?x) => *(?x,s(?y)) -> +(*(?y,?x),?x)
replace: +(?x,s(?y)) -> s(+(?x,?y)) => +(?x,s(?y)) -> s(+(?y,?x))
STEP: 2 (linear)
S:
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     *(?x,0) -> 0,
     *(?x,s(?y)) -> +(*(?x,?y),?x),
     *(?x,+(?y,?z)) -> +(*(?x,?y),*(?x,?z)) ]
P:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     *(?x,?y) -> *(?y,?x) ]
S: not linear
failure(Step 2)
STEP: 3 (relative)
S:
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     *(?x,0) -> 0,
     *(?x,s(?y)) -> +(*(?x,?y),?x),
     *(?x,+(?y,?z)) -> +(*(?x,?y),*(?x,?z)) ]
P:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     *(?x,?y) -> *(?y,?x) ]
Check relative termination:
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     *(?x,0) -> 0,
     *(?x,s(?y)) -> +(*(?x,?y),?x),
     *(?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:
  *:= (1)*x1+(3)*x1*x2+(1)*x2
  +:= (3)+(1)*x1+(1)*x2
  0:= (8)
  s:= (8)+(1)*x1
retract +(?x,0) -> ?x
retract *(?x,s(?y)) -> +(*(?x,?y),?x)
Polynomial Interpretation:
  *:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
  +:= (1)+(1)*x1+(1)*x2
  0:= (2)
  s:= (14)+(1)*x1
retract +(?x,0) -> ?x
retract *(?x,0) -> 0
retract *(?x,s(?y)) -> +(*(?x,?y),?x)
Polynomial Interpretation:
  *:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
  +:= (2)+(1)*x1+(1)*x2
  0:= (4)
  s:= (1)*x1
retract +(?x,0) -> ?x
retract *(?x,0) -> 0
retract *(?x,s(?y)) -> +(*(?x,?y),?x)
retract *(?x,+(?y,?z)) -> +(*(?x,?y),*(?x,?z))
Polynomial Interpretation:
  *:= (1)*x1+(1)*x2
  +:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
  0:= (9)
  s:= (1)+(1)*x1
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 3)
STEP: 4 (parallel)
S:
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     *(?x,0) -> 0,
     *(?x,s(?y)) -> +(*(?x,?y),?x),
     *(?x,+(?y,?z)) -> +(*(?x,?y),*(?x,?z)),
     +(0,?x) -> ?x,
     +(s(?y),?x) -> s(+(?x,?y)),
     *(0,?x) -> 0,
     *(s(?y),?x) -> +(*(?x,?y),?x),
     *(+(?y,?z),?x) -> +(*(?x,?y),*(?x,?z)) ]
P:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     *(?x,?y) -> *(?y,?x) ]
S: terminating
CP(S,S):
<0, 0> --> <0, 0> => yes
<s(+(0,?y_6)), s(?y_6)> --> <s(?y_6), s(?y_6)> => yes
<s(?y_1), s(+(0,?y_1))> --> <s(?y_1), s(?y_1)> => yes
<s(+(s(?y_1),?y_6)), s(+(s(?y_6),?y_1))> --> <s(s(+(?y_6,?y_1))), s(s(+(?y_1,?y_6)))> => yes
<0, 0> --> <0, 0> => yes
<+(*(0,?y_8),0), 0> --> <0, 0> => yes
<+(*(0,?y_9),*(0,?z_9)), 0> --> <0, 0> => yes
<0, +(*(0,?y_3),0)> --> <0, 0> => yes
<+(*(s(?y_3),?y_8),s(?y_3)), +(*(s(?y_8),?y_3),s(?y_8))> --> <s(+(+(*(?y_8,?y_3),?y_8),?y_3)), s(+(+(*(?y_3,?y_8),?y_3),?y_8))> => no
<+(*(s(?y_3),?y_9),*(s(?y_3),?z_9)), +(*(+(?y_9,?z_9),?y_3),+(?y_9,?z_9))> --> <+(+(*(?y_9,?y_3),?y_9),+(*(?z_9,?y_3),?z_9)), +(+(*(?y_3,?y_9),*(?y_3,?z_9)),+(?y_9,?z_9))> => no
<*(?x_4,?x), +(*(?x_4,?x),*(?x_4,0))> --> <*(?x_4,?x), *(?x_4,?x)> => yes
<*(?x_4,s(+(?x_1,?y_1))), +(*(?x_4,?x_1),*(?x_4,s(?y_1)))> --> <+(+(*(?x_4,?x_1),*(?x_4,?y_1)),?x_4), +(*(?x_4,?x_1),+(*(?x_4,?y_1),?x_4))> => yes
<*(?x_4,?x_5), +(*(?x_4,0),*(?x_4,?x_5))> --> <*(?x_4,?x_5), *(?x_4,?x_5)> => yes
<*(?x_4,s(+(?x_6,?y_6))), +(*(?x_4,s(?y_6)),*(?x_4,?x_6))> --> <+(+(*(?x_4,?x_6),*(?x_4,?y_6)),?x_4), +(+(*(?x_4,?y_6),?x_4),*(?x_4,?x_6))> => no
<0, +(*(0,?y_4),*(0,?z_4))> --> <0, 0> => yes
<+(*(+(?y_4,?z_4),?y_8),+(?y_4,?z_4)), +(*(s(?y_8),?y_4),*(s(?y_8),?z_4))> --> <+(+(*(?y_8,?y_4),*(?y_8,?z_4)),+(?y_4,?z_4)), +(+(*(?y_4,?y_8),?y_4),+(*(?z_4,?y_8),?z_4))> => no
<+(*(+(?y_4,?z_4),?y_9),*(+(?y_4,?z_4),?z_9)), +(*(+(?y_9,?z_9),?y_4),*(+(?y_9,?z_9),?z_4))> --> <+(+(*(?y_9,?y_4),*(?y_9,?z_4)),+(*(?z_9,?y_4),*(?z_9,?z_4))), +(+(*(?y_4,?y_9),*(?y_4,?z_9)),+(*(?z_4,?y_9),*(?z_4,?z_9)))> => no
<*(?x,?x_9), +(*(?x_9,?x),*(?x_9,0))> --> <*(?x,?x_9), *(?x_9,?x)> => yes
<*(s(+(?x_1,?y_1)),?x_9), +(*(?x_9,?x_1),*(?x_9,s(?y_1)))> --> <+(+(*(?x_9,?x_1),*(?x_9,?y_1)),?x_9), +(*(?x_9,?x_1),+(*(?x_9,?y_1),?x_9))> => yes
<*(?x_5,?x_9), +(*(?x_9,0),*(?x_9,?x_5))> --> <*(?x_5,?x_9), *(?x_9,?x_5)> => yes
<*(s(+(?x_6,?y_6)),?x_9), +(*(?x_9,s(?y_6)),*(?x_9,?x_6))> --> <+(+(*(?x_9,?x_6),*(?x_9,?y_6)),?x_9), +(+(*(?x_9,?y_6),?x_9),*(?x_9,?x_6))> => no
PCP_in(symP,S):
<*(?x,+(?x_4,?y_4)), +(*(?x,?y_4),*(?x,?x_4))> --> <+(*(?x,?x_4),*(?x,?y_4)), +(*(?x,?y_4),*(?x,?x_4))> => no
<*(?x,+(+(?x_3,?y_3),?z_3)), +(*(?x,?x_3),*(?x,+(?y_3,?z_3)))> --> <+(+(*(?x,?x_3),*(?x,?y_3)),*(?x,?z_3)), +(*(?x,?x_3),+(*(?x,?y_3),*(?x,?z_3)))> => no
<*(?x,+(?x_1,+(?y_1,?z_1))), +(*(?x,+(?x_1,?y_1)),*(?x,?z_1))> --> <+(*(?x,?x_1),+(*(?x,?y_1),*(?x,?z_1))), +(+(*(?x,?x_1),*(?x,?y_1)),*(?x,?z_1))> => no
<*(+(?x_4,?y_4),?x), +(*(?x,?y_4),*(?x,?x_4))> --> <+(*(?x,?x_4),*(?x,?y_4)), +(*(?x,?y_4),*(?x,?x_4))> => no
<*(+(+(?x_3,?y_3),?z_3),?x), +(*(?x,?x_3),*(?x,+(?y_3,?z_3)))> --> <+(+(*(?x,?x_3),*(?x,?y_3)),*(?x,?z_3)), +(*(?x,?x_3),+(*(?x,?y_3),*(?x,?z_3)))> => no
<*(+(?x_1,+(?y_1,?z_1)),?x), +(*(?x,+(?x_1,?y_1)),*(?x,?z_1))> --> <+(*(?x,?x_1),+(*(?x,?y_1),*(?x,?z_1))), +(+(*(?x,?x_1),*(?x,?y_1)),*(?x,?z_1))> => no
CP(S,symP):
<+(?x_1,?y_1), +(?x_1,+(?y_1,0))> --> <+(?x_1,?y_1), +(?x_1,?y_1)> => yes
<+(?x,?z_1), +(?x,+(0,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes
<+(?x_1,?x), +(+(?x_1,?x),0)> --> <+(?x_1,?x), +(?x_1,?x)> => yes
<?x, +(0,?x)> --> <?x, ?x> => yes
<s(+(+(?x_1,?y_1),?y)), +(?x_1,+(?y_1,s(?y)))> --> <s(+(+(?x_1,?y_1),?y)), s(+(?x_1,+(?y_1,?y)))> => yes
<+(s(+(?x,?y)),?z_1), +(?x,+(s(?y),?z_1))> --> <s(+(?z_1,+(?x,?y))), s(+(?x,+(?z_1,?y)))> => no
<+(?x_1,s(+(?x,?y))), +(+(?x_1,?x),s(?y))> --> <s(+(?x_1,+(?x,?y))), s(+(+(?x_1,?x),?y))> => yes
<s(+(?x,?y)), +(s(?y),?x)> --> <s(+(?x,?y)), s(+(?x,?y))> => yes
<0, *(?x_1,*(?y_1,0))> --> <0, 0> => yes
<*(0,?z_1), *(?x,*(0,?z_1))> --> <0, 0> => yes
<*(?x_1,0), *(*(?x_1,?x),0)> --> <0, 0> => yes
<0, *(0,?x)> --> <0, 0> => yes
<+(*(*(?x_1,?y_1),?y),*(?x_1,?y_1)), *(?x_1,*(?y_1,s(?y)))> --> <+(*(*(?x_1,?y_1),?y),*(?x_1,?y_1)), +(*(?x_1,*(?y_1,?y)),*(?x_1,?y_1))> => yes
<*(+(*(?x,?y),?x),?z_1), *(?x,*(s(?y),?z_1))> --> <+(*(?z_1,*(?x,?y)),*(?z_1,?x)), +(*(?x,*(?z_1,?y)),*(?x,?z_1))> => no
<*(?x_1,+(*(?x,?y),?x)), *(*(?x_1,?x),s(?y))> --> <+(*(?x_1,*(?x,?y)),*(?x_1,?x)), +(*(*(?x_1,?x),?y),*(?x_1,?x))> => yes
<+(*(?x,?y),?x), *(s(?y),?x)> --> <+(*(?x,?y),?x), +(*(?x,?y),?x)> => yes
<+(*(*(?x_1,?y_1),?y),*(*(?x_1,?y_1),?z)), *(?x_1,*(?y_1,+(?y,?z)))> --> <+(*(*(?x_1,?y_1),?y),*(*(?x_1,?y_1),?z)), +(*(?x_1,*(?y_1,?y)),*(?x_1,*(?y_1,?z)))> => yes
<*(+(*(?x,?y),*(?x,?z)),?z_1), *(?x,*(+(?y,?z),?z_1))> --> <+(*(?z_1,*(?x,?y)),*(?z_1,*(?x,?z))), +(*(?x,*(?z_1,?y)),*(?x,*(?z_1,?z)))> => no
<*(?x_1,+(*(?x,?y),*(?x,?z))), *(*(?x_1,?x),+(?y,?z))> --> <+(*(?x_1,*(?x,?y)),*(?x_1,*(?x,?z))), +(*(*(?x_1,?x),?y),*(*(?x_1,?x),?z))> => yes
<+(*(?x,?y),*(?x,?z)), *(+(?y,?z),?x)> --> <+(*(?x,?y),*(?x,?z)), +(*(?x,?y),*(?x,?z))> => yes
<+(?x,?z_1), +(0,+(?x,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes
<+(?y_1,?z_1), +(+(0,?y_1),?z_1)> --> <+(?y_1,?z_1), +(?y_1,?z_1)> => yes
<+(?x_1,?x), +(+(?x_1,0),?x)> --> <+(?x_1,?x), +(?x_1,?x)> => yes
<?x, +(?x,0)> --> <?x, ?x> => yes
<+(s(+(?x,?y)),?z_1), +(s(?y),+(?x,?z_1))> --> <s(+(?z_1,+(?x,?y))), s(+(+(?x,?z_1),?y))> => no
<s(+(+(?y_1,?z_1),?y)), +(+(s(?y),?y_1),?z_1)> --> <s(+(+(?y_1,?z_1),?y)), s(+(?z_1,+(?y_1,?y)))> => no
<+(?x_1,s(+(?x,?y))), +(+(?x_1,s(?y)),?x)> --> <s(+(?x_1,+(?x,?y))), s(+(?x,+(?x_1,?y)))> => no
<s(+(?x,?y)), +(?x,s(?y))> --> <s(+(?x,?y)), s(+(?x,?y))> => yes
<*(0,?z_1), *(0,*(?x,?z_1))> --> <0, 0> => yes
<0, *(*(0,?y_1),?z_1)> --> <0, 0> => yes
<*(?x_1,0), *(*(?x_1,0),?x)> --> <0, 0> => yes
<0, *(?x,0)> --> <0, 0> => yes
<*(+(*(?x,?y),?x),?z_1), *(s(?y),*(?x,?z_1))> --> <+(*(?z_1,*(?x,?y)),*(?z_1,?x)), +(*(*(?x,?z_1),?y),*(?x,?z_1))> => no
<+(*(*(?y_1,?z_1),?y),*(?y_1,?z_1)), *(*(s(?y),?y_1),?z_1)> --> <+(*(*(?y_1,?z_1),?y),*(?y_1,?z_1)), +(*(?z_1,*(?y_1,?y)),*(?z_1,?y_1))> => no
<*(?x_1,+(*(?x,?y),?x)), *(*(?x_1,s(?y)),?x)> --> <+(*(?x_1,*(?x,?y)),*(?x_1,?x)), +(*(?x,*(?x_1,?y)),*(?x,?x_1))> => no
<+(*(?x,?y),?x), *(?x,s(?y))> --> <+(*(?x,?y),?x), +(*(?x,?y),?x)> => yes
<*(+(*(?x,?y),*(?x,?z)),?z_1), *(+(?y,?z),*(?x,?z_1))> --> <+(*(?z_1,*(?x,?y)),*(?z_1,*(?x,?z))), +(*(*(?x,?z_1),?y),*(*(?x,?z_1),?z))> => no
<+(*(*(?y_1,?z_1),?y),*(*(?y_1,?z_1),?z)), *(*(+(?y,?z),?y_1),?z_1)> --> <+(*(*(?y_1,?z_1),?y),*(*(?y_1,?z_1),?z)), +(*(?z_1,*(?y_1,?y)),*(?z_1,*(?y_1,?z)))> => no
<*(?x_1,+(*(?x,?y),*(?x,?z))), *(*(?x_1,+(?y,?z)),?x)> --> <+(*(?x_1,*(?x,?y)),*(?x_1,*(?x,?z))), +(*(?x,*(?x_1,?y)),*(?x,*(?x_1,?z)))> => no
<+(*(?x,?y),*(?x,?z)), *(?x,+(?y,?z))> --> <+(*(?x,?y),*(?x,?z)), +(*(?x,?y),*(?x,?z))> => yes
check joinability condition:
check modulo joinability of s(+(+(*(?y_8,?y_3),?y_8),?y_3)) and s(+(+(*(?y_3,?y_8),?y_3),?y_8)): joinable by {5}
check modulo joinability of +(+(*(?y_9,?y_3),?y_9),+(*(?z_9,?y_3),?z_9)) and +(+(*(?y_3,?y_9),*(?y_3,?z_9)),+(?y_9,?z_9)): joinable by {2,3}
check modulo joinability of +(+(*(?x_4,?x_6),*(?x_4,?y_6)),?x_4) and +(+(*(?x_4,?y_6),?x_4),*(?x_4,?x_6)): joinable by {2}
check modulo joinability of +(+(*(?y_8,?y_4),*(?y_8,?z_4)),+(?y_4,?z_4)) and +(+(*(?y_4,?y_8),?y_4),+(*(?z_4,?y_8),?z_4)): joinable by {2,3}
check modulo joinability of +(+(*(?y_9,?y_4),*(?y_9,?z_4)),+(*(?z_9,?y_4),*(?z_9,?z_4))) and +(+(*(?y_4,?y_9),*(?y_4,?z_9)),+(*(?z_4,?y_9),*(?z_4,?z_9))): joinable by {2,3}
check modulo joinability of +(+(*(?x_9,?x_6),*(?x_9,?y_6)),?x_9) and +(+(*(?x_9,?y_6),?x_9),*(?x_9,?x_6)): joinable by {2}
check modulo joinability of +(*(?x,?x_4),*(?x,?y_4)) and +(*(?x,?y_4),*(?x,?x_4)): joinable by {2}
check modulo joinability of +(+(*(?x,?x_3),*(?x,?y_3)),*(?x,?z_3)) and +(*(?x,?x_3),+(*(?x,?y_3),*(?x,?z_3))): joinable by {3}
check modulo joinability of +(*(?x,?x_1),+(*(?x,?y_1),*(?x,?z_1))) and +(+(*(?x,?x_1),*(?x,?y_1)),*(?x,?z_1)): joinable by {5}
check modulo joinability of +(*(?x,?x_4),*(?x,?y_4)) and +(*(?x,?y_4),*(?x,?x_4)): joinable by {2}
check modulo joinability of +(+(*(?x,?x_3),*(?x,?y_3)),*(?x,?z_3)) and +(*(?x,?x_3),+(*(?x,?y_3),*(?x,?z_3))): joinable by {3}
check modulo joinability of +(*(?x,?x_1),+(*(?x,?y_1),*(?x,?z_1))) and +(+(*(?x,?x_1),*(?x,?y_1)),*(?x,?z_1)): joinable by {5}
check modulo joinability of s(+(?z_1,+(?x,?y))) and s(+(?x,+(?z_1,?y))): joinable by {3}
check modulo joinability of +(*(?z_1,*(?x,?y)),*(?z_1,?x)) and +(*(?x,*(?z_1,?y)),*(?x,?z_1)): joinable by {1}
check modulo joinability of +(*(?z_1,*(?x,?y)),*(?z_1,*(?x,?z))) and +(*(?x,*(?z_1,?y)),*(?x,*(?z_1,?z))): joinable by {1}
check modulo joinability of s(+(?z_1,+(?x,?y))) and s(+(+(?x,?z_1),?y)): joinable by {3}
check modulo joinability of s(+(+(?y_1,?z_1),?y)) and s(+(?z_1,+(?y_1,?y))): joinable by {3}
check modulo joinability of s(+(?x_1,+(?x,?y))) and s(+(?x,+(?x_1,?y))): joinable by {3}
check modulo joinability of +(*(?z_1,*(?x,?y)),*(?z_1,?x)) and +(*(*(?x,?z_1),?y),*(?x,?z_1)): joinable by {1}
check modulo joinability of +(*(*(?y_1,?z_1),?y),*(?y_1,?z_1)) and +(*(?z_1,*(?y_1,?y)),*(?z_1,?y_1)): joinable by {1}
check modulo joinability of +(*(?x_1,*(?x,?y)),*(?x_1,?x)) and +(*(?x,*(?x_1,?y)),*(?x,?x_1)): joinable by {1}
check modulo joinability of +(*(?z_1,*(?x,?y)),*(?z_1,*(?x,?z))) and +(*(*(?x,?z_1),?y),*(*(?x,?z_1),?z)): joinable by {0,1}
check modulo joinability of +(*(*(?y_1,?z_1),?y),*(*(?y_1,?z_1),?z)) and +(*(?z_1,*(?y_1,?y)),*(?z_1,*(?y_1,?z))): joinable by {0,1}
check modulo joinability of +(*(?x_1,*(?x,?y)),*(?x_1,*(?x,?z))) and +(*(?x,*(?x_1,?y)),*(?x,*(?x_1,?z))): joinable by {1}
success
P':
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?y,?x) -> +(?x,?y),
     +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(?y,?x) -> *(?x,?y) ]
Check relative termination:
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     *(?x,0) -> 0,
     *(?x,s(?y)) -> +(*(?x,?y),?x),
     *(?x,+(?y,?z)) -> +(*(?x,?y),*(?x,?z)),
     +(0,?x) -> ?x,
     +(s(?y),?x) -> s(+(?x,?y)),
     *(0,?x) -> 0,
     *(s(?y),?x) -> +(*(?x,?y),?x),
     *(+(?y,?z),?x) -> +(*(?x,?y),*(?x,?z)) ]
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?y,?x) -> +(?x,?y),
     +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(?y,?x) -> *(?x,?y) ]
Polynomial Interpretation:
  *:= (1)*x1+(1)*x1*x2+(1)*x2
  +:= (2)+(1)*x1+(1)*x2
  0:= (7)
  s:= (12)+(1)*x1
retract +(?x,0) -> ?x
retract *(?x,s(?y)) -> +(*(?x,?y),?x)
retract +(0,?x) -> ?x
retract *(s(?y),?x) -> +(*(?x,?y),?x)
Polynomial Interpretation:
  *:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
  +:= (1)+(1)*x1+(1)*x2
  0:= (4)
  s:= (10)+(1)*x1
retract +(?x,0) -> ?x
retract *(?x,0) -> 0
retract *(?x,s(?y)) -> +(*(?x,?y),?x)
retract +(0,?x) -> ?x
retract *(0,?x) -> 0
retract *(s(?y),?x) -> +(*(?x,?y),?x)
Polynomial Interpretation:
  *:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
  +:= (2)+(1)*x1+(1)*x2
  0:= (4)
  s:= (2)+(1)*x1
retract +(?x,0) -> ?x
retract *(?x,0) -> 0
retract *(?x,s(?y)) -> +(*(?x,?y),?x)
retract *(?x,+(?y,?z)) -> +(*(?x,?y),*(?x,?z))
retract +(0,?x) -> ?x
retract *(0,?x) -> 0
retract *(s(?y),?x) -> +(*(?x,?y),?x)
retract *(+(?y,?z),?x) -> +(*(?x,?y),*(?x,?z))
Polynomial Interpretation:
  *:= (1)*x1+(1)*x2
  +:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
  0:= (7)
  s:= (4)+(1)*x1
relatively terminating
S/P': relatively terminating
S:
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     *(?x,0) -> 0,
     *(?x,s(?y)) -> +(*(?x,?y),?x),
     *(?x,+(?y,?z)) -> +(*(?x,?y),*(?x,?z)),
     +(0,?x) -> ?x,
     +(s(?y),?x) -> s(+(?x,?y)),
     *(0,?x) -> 0,
     *(s(?y),?x) -> +(*(?x,?y),?x),
     *(+(?y,?z),?x) -> +(*(?x,?y),*(?x,?z)) ]
P:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     *(?x,?y) -> *(?y,?x) ]
Success
Reduction-Preserving Completion
Direct Methods: CR

Final result: CR
203.trs: Success(CR)
(12134 msec.)