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)) ]
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,+(?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,+(?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)),
     *(?y_3,+(?x_4,?y_4)) = +(*(?x_4,?y_3),*(?y_4,?y_3)) ]
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,?y),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1),
     +(*(+(?x,?y),?z_5),*(?z,?z_5)) = *(+(?x,+(?y,?z)),?z_5),
     +(?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),
     *(?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)) = *(?x,*(?y,?z)),
     *(*(?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_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),*(?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,?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)),
     *(?z,+(?x,?y)) = +(*(?x,?z),*(?y,?z)),
     *(+(?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) ]
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,+(?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,+(?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_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 <[], [([],3),([],4)]>
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)) ]
Sort Assignment:
 * : 20*20=>20
 + : 20*20=>20
non-linear variables: {?z_4}
non-linear types: {20}
types leq non-linear types: {20}
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)) ]
NLR:
0: {}
1: {}
2: {}
3: {}
4: {0,1,2,3,4}
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)) ]
Sort Assignment:
 * : 20*20=>20
 + : 20*20=>20
non-linear variables: {?z_4}
non-linear types: {20}
types leq non-linear types: {20}
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)) ]
unknown innermost-termination for terms of non-linear types
unknown Strongly Quasi-Linear & Hierarchically Decreasing
check Non-Confluence...
obtain 15 rules by 3 steps unfolding
strenghten *(?x_6,?y_6) and *(?y_6,?x_6)
strenghten +(?x_10,?y_10) and +(?y_10,?x_10)
strenghten *(?x_2,*(?y_2,?x_7)) and *(?x_7,*(?x_2,?y_2))
strenghten *(?x_2,*(?y_2,?x_8)) and *(*(?x_2,?y_2),?x_8)
strenghten *(?x_3,*(?y_3,?x_15)) and *(?x_15,*(?y_3,?x_3))
strenghten *(?x_3,*(?y_3,?z_2)) and *(*(?y_3,?x_3),?z_2)
strenghten *(?x_13,*(?x_3,?y_3)) and *(?x_13,*(?y_3,?x_3))
strenghten *(?x_15,*(?x_16,?y_16)) and *(?x_16,*(?y_16,?x_15))
strenghten *(*(?x_14,?y_14),?x_13) and *(?x_13,*(?x_14,?y_14))
strenghten *(*(?x_16,?y_16),?x_15) and *(?x_16,*(?y_16,?x_15))
strenghten +(?x,+(?y,?x_11)) and +(?x_11,+(?x,?y))
strenghten +(?x,+(?y,?x_12)) and +(+(?x,?y),?x_12)
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_7),*(?y_4,?x_7)) and *(?x_7,+(?x_4,?y_4))
strenghten +(*(?x_4,?x_8),*(?y_4,?x_8)) and *(+(?x_4,?y_4),?x_8)
strenghten *(?x,*(*(?x_1,?y_1),?x_2)) and *(?x_2,*(?x_1,*(?y_1,?x)))
strenghten *(?x_2,*(?y_2,*(?x_14,?y_14))) and *(*(?x_2,?y_2),*(?x_14,?y_14))
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,?z)),
     +(?x,?y) -> +(?y,?x),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     *(?x,?y) -> *(?y,?x) ]
Polynomial Interpretation:
  *:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
  +:= (2)+(1)*x1+(1)*x2
relatively terminating
unknown Huet (modulo AC)
check by Reduction-Preserving Completion...
STEP: 1 (parallel)
S:
   [ *(+(?x,?y),?z) -> +(*(?x,?z),*(?y,?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):
PCP_in(symP,S):
<*(+(?x_4,?y_4),?z), +(*(?y_4,?z),*(?x_4,?z))> --> <+(*(?x_4,?z),*(?y_4,?z)), +(*(?y_4,?z),*(?x_4,?z))> => no
<*(+(+(?x_3,?y_3),?z_3),?z), +(*(?x_3,?z),*(+(?y_3,?z_3),?z))> --> <+(+(*(?x_3,?z),*(?y_3,?z)),*(?z_3,?z)), +(*(?x_3,?z),+(*(?y_3,?z),*(?z_3,?z)))> => no
<*(+(?x_1,+(?y_1,?z_1)),?z), +(*(+(?x_1,?y_1),?z),*(?z_1,?z))> --> <+(*(?x_1,?z),+(*(?y_1,?z),*(?z_1,?z))), +(+(*(?x_1,?z),*(?y_1,?z)),*(?z_1,?z))> => no
CP(S,symP):
<*(+(*(?x,?z),*(?y,?z)),?z_1), *(+(?x,?y),*(?z,?z_1))> --> <+(*(*(?x,?z),?z_1),*(*(?y,?z),?z_1)), +(*(?x,*(?z,?z_1)),*(?y,*(?z,?z_1)))> => yes
<+(*(?x,*(?y_1,?z_1)),*(?y,*(?y_1,?z_1))), *(*(+(?x,?y),?y_1),?z_1)> --> <+(*(?x,*(?y_1,?z_1)),*(?y,*(?y_1,?z_1))), +(*(*(?x,?y_1),?z_1),*(*(?y,?y_1),?z_1))> => yes
<*(?x_1,+(*(?x,?z),*(?y,?z))), *(*(?x_1,+(?x,?y)),?z)> --> <*(?x_1,+(*(?x,?z),*(?y,?z))), *(*(?x_1,+(?x,?y)),?z)> => no
<+(*(?x,?z),*(?y,?z)), *(?z,+(?x,?y))> --> <+(*(?x,?z),*(?y,?z)), *(?z,+(?x,?y))> => no
check joinability condition:
check modulo joinability of +(*(?x_4,?z),*(?y_4,?z)) and +(*(?y_4,?z),*(?x_4,?z)): joinable by {2}
check modulo joinability of +(+(*(?x_3,?z),*(?y_3,?z)),*(?z_3,?z)) and +(*(?x_3,?z),+(*(?y_3,?z),*(?z_3,?z))): joinable by {3}
check modulo joinability of +(*(?x_1,?z),+(*(?y_1,?z),*(?z_1,?z))) and +(+(*(?x_1,?z),*(?y_1,?z)),*(?z_1,?z)): joinable by {5}
check modulo reachablity from *(?x_1,+(*(?x,?z),*(?y,?z))) to *(*(?x_1,+(?x,?y)),?z): maybe not reachable
check modulo reachablity from +(*(?x,?z),*(?y,?z)) to *(?z,+(?x,?y)): maybe not reachable
failed
failure(Step 1)
   [ *(?z,+(?x,?y)) -> +(*(?x,?z),*(?y,?z)) ]
Added S-Rules:
   [ *(?z,+(?x,?y)) -> +(*(?x,?z),*(?y,?z)) ]
Added P-Rules:
   [ ]
replace: *(+(?x,?y),?z) -> +(*(?x,?z),*(?y,?z)) => *(+(?x,?y),?z) -> +(*(?x,?z),*(?z,?y))
replace: *(+(?x,?y),?z) -> +(*(?x,?z),*(?y,?z)) => *(+(?x,?y),?z) -> +(*(?y,?z),*(?x,?z))
replace: *(+(?x,?y),?z) -> +(*(?x,?z),*(?y,?z)) => *(+(?x,?y),?z) -> +(*(?z,?x),*(?y,?z))
STEP: 2 (linear)
S:
   [ *(+(?x,?y),?z) -> +(*(?x,?z),*(?y,?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,?y),?z) -> +(*(?x,?z),*(?y,?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,?y),?z) -> +(*(?x,?z),*(?y,?z)) ]
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     *(?x,?y) -> *(?y,?x) ]
Polynomial Interpretation:
  *:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
  +:= (2)+(1)*x1+(1)*x2
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 3)
STEP: 4 (parallel)
S:
   [ *(+(?x,?y),?z) -> +(*(?x,?z),*(?y,?z)),
     *(?z,+(?x,?y)) -> +(*(?x,?z),*(?y,?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_1,+(?x,?y)),*(?y_1,+(?x,?y))), +(*(?x,+(?x_1,?y_1)),*(?y,+(?x_1,?y_1)))> --> <+(+(*(?x,?x_1),*(?y,?x_1)),+(*(?x,?y_1),*(?y,?y_1))), +(+(*(?x_1,?x),*(?y_1,?x)),+(*(?x_1,?y),*(?y_1,?y)))> => no
PCP_in(symP,S):
<*(+(?x_4,?y_4),?z), +(*(?y_4,?z),*(?x_4,?z))> --> <+(*(?x_4,?z),*(?y_4,?z)), +(*(?y_4,?z),*(?x_4,?z))> => no
<*(+(+(?x_3,?y_3),?z_3),?z), +(*(?x_3,?z),*(+(?y_3,?z_3),?z))> --> <+(+(*(?x_3,?z),*(?y_3,?z)),*(?z_3,?z)), +(*(?x_3,?z),+(*(?y_3,?z),*(?z_3,?z)))> => no
<*(+(?x_1,+(?y_1,?z_1)),?z), +(*(+(?x_1,?y_1),?z),*(?z_1,?z))> --> <+(*(?x_1,?z),+(*(?y_1,?z),*(?z_1,?z))), +(+(*(?x_1,?z),*(?y_1,?z)),*(?z_1,?z))> => no
<*(?z,+(?x_4,?y_4)), +(*(?y_4,?z),*(?x_4,?z))> --> <+(*(?x_4,?z),*(?y_4,?z)), +(*(?y_4,?z),*(?x_4,?z))> => no
<*(?z,+(+(?x_3,?y_3),?z_3)), +(*(?x_3,?z),*(+(?y_3,?z_3),?z))> --> <+(+(*(?x_3,?z),*(?y_3,?z)),*(?z_3,?z)), +(*(?x_3,?z),+(*(?y_3,?z),*(?z_3,?z)))> => no
<*(?z,+(?x_1,+(?y_1,?z_1))), +(*(+(?x_1,?y_1),?z),*(?z_1,?z))> --> <+(*(?x_1,?z),+(*(?y_1,?z),*(?z_1,?z))), +(+(*(?x_1,?z),*(?y_1,?z)),*(?z_1,?z))> => no
CP(S,symP):
<*(+(*(?x,?z),*(?y,?z)),?z_1), *(+(?x,?y),*(?z,?z_1))> --> <+(*(*(?x,?z),?z_1),*(*(?y,?z),?z_1)), +(*(?x,*(?z,?z_1)),*(?y,*(?z,?z_1)))> => yes
<+(*(?x,*(?y_1,?z_1)),*(?y,*(?y_1,?z_1))), *(*(+(?x,?y),?y_1),?z_1)> --> <+(*(?x,*(?y_1,?z_1)),*(?y,*(?y_1,?z_1))), +(*(*(?x,?y_1),?z_1),*(*(?y,?y_1),?z_1))> => yes
<*(?x_1,+(*(?x,?z),*(?y,?z))), *(*(?x_1,+(?x,?y)),?z)> --> <+(*(*(?x,?z),?x_1),*(*(?y,?z),?x_1)), +(*(*(?x,?x_1),?z),*(*(?y,?x_1),?z))> => no
<+(*(?x,?z),*(?y,?z)), *(?z,+(?x,?y))> --> <+(*(?x,?z),*(?y,?z)), +(*(?x,?z),*(?y,?z))> => yes
<+(*(?x,*(?x_1,?y_1)),*(?y,*(?x_1,?y_1))), *(?x_1,*(?y_1,+(?x,?y)))> --> <+(*(?x,*(?x_1,?y_1)),*(?y,*(?x_1,?y_1))), +(*(*(?x,?y_1),?x_1),*(*(?y,?y_1),?x_1))> => no
<*(+(*(?x,?z),*(?y,?z)),?z_1), *(?z,*(+(?x,?y),?z_1))> --> <+(*(*(?x,?z),?z_1),*(*(?y,?z),?z_1)), +(*(*(?x,?z_1),?z),*(*(?y,?z_1),?z))> => no
<*(?x_1,+(*(?x,?z),*(?y,?z))), *(*(?x_1,?z),+(?x,?y))> --> <+(*(*(?x,?z),?x_1),*(*(?y,?z),?x_1)), +(*(?x,*(?x_1,?z)),*(?y,*(?x_1,?z)))> => no
<+(*(?x,?z),*(?y,?z)), *(+(?x,?y),?z)> --> <+(*(?x,?z),*(?y,?z)), +(*(?x,?z),*(?y,?z))> => yes
check joinability condition:
check modulo joinability of +(+(*(?x,?x_1),*(?y,?x_1)),+(*(?x,?y_1),*(?y,?y_1))) and +(+(*(?x_1,?x),*(?y_1,?x)),+(*(?x_1,?y),*(?y_1,?y))): joinable by {2,3}
check modulo joinability of +(*(?x_4,?z),*(?y_4,?z)) and +(*(?y_4,?z),*(?x_4,?z)): joinable by {2}
check modulo joinability of +(+(*(?x_3,?z),*(?y_3,?z)),*(?z_3,?z)) and +(*(?x_3,?z),+(*(?y_3,?z),*(?z_3,?z))): joinable by {3}
check modulo joinability of +(*(?x_1,?z),+(*(?y_1,?z),*(?z_1,?z))) and +(+(*(?x_1,?z),*(?y_1,?z)),*(?z_1,?z)): joinable by {5}
check modulo joinability of +(*(?x_4,?z),*(?y_4,?z)) and +(*(?y_4,?z),*(?x_4,?z)): joinable by {2}
check modulo joinability of +(+(*(?x_3,?z),*(?y_3,?z)),*(?z_3,?z)) and +(*(?x_3,?z),+(*(?y_3,?z),*(?z_3,?z))): joinable by {3}
check modulo joinability of +(*(?x_1,?z),+(*(?y_1,?z),*(?z_1,?z))) and +(+(*(?x_1,?z),*(?y_1,?z)),*(?z_1,?z)): joinable by {5}
check modulo joinability of +(*(*(?x,?z),?x_1),*(*(?y,?z),?x_1)) and +(*(*(?x,?x_1),?z),*(*(?y,?x_1),?z)): joinable by {4}
check modulo joinability of +(*(?x,*(?x_1,?y_1)),*(?y,*(?x_1,?y_1))) and +(*(*(?x,?y_1),?x_1),*(*(?y,?y_1),?x_1)): joinable by {0,4}
check modulo joinability of +(*(*(?x,?z),?z_1),*(*(?y,?z),?z_1)) and +(*(*(?x,?z_1),?z),*(*(?y,?z_1),?z)): joinable by {4}
check modulo joinability of +(*(*(?x,?z),?x_1),*(*(?y,?z),?x_1)) and +(*(?x,*(?x_1,?z)),*(?y,*(?x_1,?z))): joinable by {0,4}
success
P':
   [ +(?y,?x) -> +(?x,?y),
     +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     *(?y,?x) -> *(?x,?y) ]
Check relative termination:
   [ *(+(?x,?y),?z) -> +(*(?x,?z),*(?y,?z)),
     *(?z,+(?x,?y)) -> +(*(?x,?z),*(?y,?z)) ]
   [ +(?y,?x) -> +(?x,?y),
     +(?x,+(?y,?z)) -> +(+(?x,?y),?z),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     *(?y,?x) -> *(?x,?y) ]
Polynomial Interpretation:
  *:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
  +:= (3)+(1)*x1+(1)*x2
relatively terminating
S/P': relatively terminating
S:
   [ *(+(?x,?y),?z) -> +(*(?x,?z),*(?y,?z)),
     *(?z,+(?x,?y)) -> +(*(?x,?z),*(?y,?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
196.trs: Success(CR)
(16959 msec.)