MAYBE
Rewrite Rules:
   [ *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     eq(*(a,?x),*(?y,a)) -> eq(?x,?y),
     eq(a,a) -> T,
     eq(a,*(?x,?y)) -> F,
     eq(?x,?y) -> eq(?y,?x) ]
Apply Direct Methods...
Inner CPs:
   [ *(?x,*(?x_1,*(?y_1,?z_1))) = *(*(?x,*(?x_1,?y_1)),?z_1),
     *(*(*(?x,?y),?z),?z_1) = *(?x,*(*(?y,?z),?z_1)),
     eq(*(*(a,?y),?z),*(?y_2,a)) = eq(*(?y,?z),?y_2),
     eq(*(a,?x_2),*(?x_1,*(?y_1,a))) = eq(?x_2,*(?x_1,?y_1)),
     eq(a,*(*(?x,?y),?z)) = F,
     eq(a,*(?x_1,*(?y_1,?z_1))) = F,
     *(?x_1,*(*(?x,?y),?z)) = *(*(?x_1,?x),*(?y,?z)),
     *(*(?x,*(?y,?z)),?z_1) = *(*(?x,?y),*(?z,?z_1)) ]
Outer CPs:
   [ *(*(*(?x_1,?y_1),?y),?z) = *(?x_1,*(?y_1,*(?y,?z))),
     eq(?x_2,?y_2) = eq(*(?y_2,a),*(a,?x_2)),
     T = eq(a,a),
     F = eq(*(?x_3,?y_3),a) ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth & Bendix
Linear
unknown Development Closed
unknown Strongly 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_1,*(?y_1,*(*(?y,?y_2),?z_2))) = *(*(*(?x_1,?y_1),?y),*(?y_2,?z_2)),
     *(?x_1,*(?y_1,*(?x_3,*(?y_3,?z)))) = *(*(*(?x_1,?y_1),*(?x_3,?y_3)),?z),
     *(?x_1,*(?y_1,*(?y,?z))) = *(*(*(?x_1,?y_1),?y),?z),
     *(?x,*(*(?y,?y_1),?z_1)) = *(*(?x,?y),*(?y_1,?z_1)),
     *(?x,*(?x_2,*(?y_2,?z))) = *(*(?x,*(?x_2,?y_2)),?z),
     *(*(?x_1,?x),*(*(?y,?y_2),?z_2)) = *(?x_1,*(*(?x,?y),*(?y_2,?z_2))),
     *(*(?x_1,?x),*(?x_3,*(?y_3,?z))) = *(?x_1,*(*(?x,*(?x_3,?y_3)),?z)),
     *(?x,*(*(*(?y,?y_3),?z_3),?z_2)) = *(*(*(?x,?y),*(?y_3,?z_3)),?z_2),
     *(?x,*(*(?x_4,*(?y_4,?z)),?z_2)) = *(*(*(?x,*(?x_4,?y_4)),?z),?z_2),
     eq(*(*(?y,?y_4),?z_4),?y_3) = eq(*(*(a,?y),*(?y_4,?z_4)),*(?y_3,a)),
     eq(*(?x_5,*(?y_5,?z)),?y_3) = eq(*(*(a,*(?x_5,?y_5)),?z),*(?y_3,a)),
     F = eq(a,*(*(?x,?y),*(?y_1,?z_1))),
     F = eq(a,*(*(?x,*(?x_2,?y_2)),?z)),
     *(*(?x_1,?x),*(?y,?z)) = *(?x_1,*(*(?x,?y),?z)),
     *(?x,*(*(?y,?z),?z_2)) = *(*(*(?x,?y),?z),?z_2),
     eq(*(?y,?z),?y_3) = eq(*(*(a,?y),?z),*(?y_3,a)),
     F = eq(a,*(*(?x,?y),?z)),
     *(*(*(?x_2,*(?y_2,?y)),?y_1),?z_1) = *(*(?x_2,?y_2),*(?y,*(?y_1,?z_1))),
     *(*(*(*(?x,?y_3),?z_3),?y_1),?z_1) = *(?x,*(*(?y_3,?z_3),*(?y_1,?z_1))),
     *(*(*(?x,?y),?y_1),?z_1) = *(?x,*(?y,*(?y_1,?z_1))),
     *(*(?x_1,*(?y_1,?y)),?z) = *(*(?x_1,?y_1),*(?y,?z)),
     *(*(*(?x,?y_2),?z_2),?z) = *(?x,*(*(?y_2,?z_2),?z)),
     *(*(?x_2,*(?y_2,?y)),*(?z,?z_1)) = *(*(*(?x_2,?y_2),*(?y,?z)),?z_1),
     *(*(*(?x,?y_3),?z_3),*(?z,?z_1)) = *(*(?x,*(*(?y_3,?z_3),?z)),?z_1),
     *(*(?x_2,*(?x_3,*(?y_3,?y))),?z) = *(?x_2,*(*(?x_3,?y_3),*(?y,?z))),
     *(*(?x_2,*(*(?x,?y_4),?z_4)),?z) = *(?x_2,*(?x,*(*(?y_4,?z_4),?z))),
     eq(?x_3,*(?x_4,*(?y_4,?y))) = eq(*(a,?x_3),*(*(?x_4,?y_4),*(?y,a))),
     eq(?x_3,*(*(?x,?y_5),?z_5)) = eq(*(a,?x_3),*(?x,*(*(?y_5,?z_5),a))),
     F = eq(a,*(?x,*(*(?y_2,?z_2),?z))),
     *(*(?x,?y),*(?z,?z_1)) = *(*(?x,*(?y,?z)),?z_1),
     *(*(?x_2,*(?x,?y)),?z) = *(?x_2,*(?x,*(?y,?z))),
     eq(?x_3,*(?x,?y)) = eq(*(a,?x_3),*(?x,*(?y,a))),
     F = eq(a,*(?x,*(?y,?z))),
     eq(*(?x_5,*(?y_5,a)),*(*(a,?y_2),?z_2)) = eq(*(?y_2,?z_2),*(?x_5,?y_5)),
     eq(*(?y,a),*(*(a,?y_2),?z_2)) = eq(*(?y_2,?z_2),?y),
     eq(*(?x_3,*(?y_3,a)),*(a,?x)) = eq(?x,*(?x_3,?y_3)),
     eq(*(*(a,?y_2),?z_2),*(?x_5,*(?y_5,a))) = eq(*(?y_2,?z_2),*(?x_5,?y_5)),
     eq(*(?y,a),*(a,?x)) = eq(?x,?y),
     eq(*(*(a,?y_2),?z_2),*(?y,a)) = eq(*(?y_2,?z_2),?y),
     eq(*(a,?x),*(?x_3,*(?y_3,a))) = eq(?x,*(?x_3,?y_3)),
     eq(a,a) = T,
     eq(*(*(?x,?y_2),?z_2),a) = F,
     eq(*(?x_3,*(?y_3,?y)),a) = F,
     eq(*(?x,?y),a) = F,
     eq(a,*(*(?x,?y_2),?z_2)) = F,
     eq(a,*(?x_3,*(?y_3,?y))) = F,
     eq(?x_3,?y_3) = eq(*(?y_3,a),*(a,?x_3)),
     T = eq(a,a),
     F = eq(*(?x_4,?y_4),a) ]
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,*(?x_1,*(?y_1,?z_1))), *(*(?x,*(?x_1,?y_1)),?z_1)> by Rules <1, 0> preceded by [(*,2)]
 joinable by a reduction of rules <[([(*,2)],0)], [([],1)]>
Critical Pair <*(*(*(?x,?y),?z),?z_1), *(?x,*(*(?y,?z),?z_1))> by Rules <0, 1> preceded by [(*,1)]
 joinable by a reduction of rules <[([(*,1)],1)], [([],0)]>
Critical Pair <eq(*(*(a,?y),?z),*(?y_2,a)), eq(*(?y,?z),?y_2)> by Rules <0, 2> preceded by [(eq,1)]
 joinable by a reduction of rules <[([(eq,1)],1),([],2)], []>
Critical Pair <eq(*(a,?x_2),*(?x_1,*(?y_1,a))), eq(?x_2,*(?x_1,?y_1))> by Rules <1, 2> preceded by [(eq,2)]
 joinable by a reduction of rules <[([(eq,2)],0),([],2)], []>
Critical Pair <eq(a,*(*(?x,?y),?z)), F> by Rules <0, 4> preceded by [(eq,2)]
 joinable by a reduction of rules <[([],4)], []>
Critical Pair <eq(a,*(?x_1,*(?y_1,?z_1))), F> by Rules <1, 4> preceded by [(eq,2)]
 joinable by a reduction of rules <[([],4)], []>
Critical Pair <*(?x_1,*(*(?x,?y),?z)), *(*(?x_1,?x),*(?y,?z))> by Rules <0, 0> preceded by [(*,2)]
 joinable by a reduction of rules <[([(*,2)],1)], [([],1)]>
Critical Pair <*(*(?x,*(?y,?z)),?z_1), *(*(?x,?y),*(?z,?z_1))> by Rules <1, 1> preceded by [(*,1)]
 joinable by a reduction of rules <[([(*,1)],0)], [([],0)]>
Critical Pair <*(?x_1,*(?y_1,*(?y,?z))), *(*(*(?x_1,?y_1),?y),?z)> by Rules <1, 0> preceded by []
 joinable by a reduction of rules <[([],0)], [([],1)]>
Critical Pair <eq(*(?y_2,a),*(a,?x_2)), eq(?x_2,?y_2)> by Rules <5, 2> preceded by []
 joinable by a reduction of rules <[([],5),([],2)], []>
Critical Pair <eq(a,a), T> by Rules <5, 3> preceded by []
 joinable by a reduction of rules <[([],3)], []>
Critical Pair <eq(*(?x_3,?y_3),a), F> by Rules <5, 4> preceded by []
 joinable by a reduction of rules <[([],5),([],4)], []>
unknown Diagram Decreasing
check Non-Confluence...
obtain 16 rules by 3 steps unfolding
strenghten eq(a,a) and T
strenghten eq(?x_6,?y_6) and eq(?y_6,?x_6)
strenghten eq(*(?x_3,?y_3),a) and F
strenghten eq(a,*(?x_3,?y_3)) and F
strenghten eq(*(?x_1,*(?y_1,?z_1)),a) and F
strenghten eq(*(*(?x,?y),?z),a) and F
strenghten eq(a,*(?x_1,*(?y_1,?z_1))) and F
strenghten eq(a,*(*(?x,?y),?z)) and F
strenghten eq(*(?y_2,a),*(a,?x_2)) and eq(?x_2,?y_2)
strenghten eq(*(a,?x_2),*(?y_2,a)) and eq(?x_2,?y_2)
strenghten *(?x,*(*(?y,?z),?z_1)) and *(*(*(?x,?y),?z),?z_1)
strenghten *(*(?x,?y),*(?z,?z_1)) and *(*(?x,*(?y,?z)),?z_1)
strenghten *(*(?x,*(?x_1,?y_1)),?z_1) and *(?x,*(?x_1,*(?y_1,?z_1)))
strenghten *(*(?x_1,?x),*(?y,?z)) and *(?x_1,*(*(?x,?y),?z))
strenghten *(*(*(?x_1,?y_1),?y),?z) and *(?x_1,*(?y_1,*(?y,?z)))
strenghten eq(*(*(a,?y),?z),*(?y_2,a)) and eq(*(?y,?z),?y_2)
strenghten eq(*(a,?x_2),*(?x_1,*(?y_1,a))) and eq(?x_2,*(?x_1,?y_1))
obtain 50 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:
   [ eq(*(a,?x),*(?y,a)) -> eq(?x,?y),
     eq(a,a) -> T,
     eq(a,*(?x,?y)) -> F,
     *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)) ]
   [ eq(?x,?y) -> eq(?y,?x) ]
Polynomial Interpretation:
  *:= (1)*x1+(1)*x2
  F:= 0
  T:= (8)
  a:= 0
  eq:= (5)+(8)*x1*x1+(8)*x2*x2
retract eq(a,*(?x,?y)) -> F
Polynomial Interpretation:
  *:= (1)*x1+(1)*x2
  F:= 0
  T:= 0
  a:= (4)
  eq:= (13)+(8)*x1*x1+(11)*x1*x2+(8)*x2*x2
retract eq(a,a) -> T
retract eq(a,*(?x,?y)) -> F
Polynomial Interpretation:
  *:= (2)+(1)*x1+(1)*x2
  F:= 0
  T:= 0
  a:= (4)
  eq:= (15)+(12)*x1+(8)*x1*x1+(3)*x1*x2+(12)*x2+(8)*x2*x2
retract eq(*(a,?x),*(?y,a)) -> eq(?x,?y)
retract eq(a,a) -> T
retract eq(a,*(?x,?y)) -> F
retract eq(*(a,?x),*(?y,a)) -> eq(?x,?y)
retract eq(a,a) -> T
retract eq(a,*(?x,?y)) -> F
unknown relative termination
unknown Huet (modulo AC)
check by Reduction-Preserving Completion...
STEP: 1 (parallel)
S:
   [ eq(*(a,?x),*(?y,a)) -> eq(?x,?y),
     eq(a,a) -> T,
     eq(a,*(?x,?y)) -> F ]
P:
   [ *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     eq(?x,?y) -> eq(?y,?x) ]
S: terminating
CP(S,S):
PCP_in(symP,S):
<eq(*(a,?x),*(?x_1,*(?y_1,a))), eq(?x,*(?x_1,?y_1))> --> <eq(*(a,?x),*(?x_1,*(?y_1,a))), eq(?x,*(?x_1,?y_1))> => no
<eq(*(*(a,?y_2),?z_2),*(?y,a)), eq(*(?y_2,?z_2),?y)> --> <eq(*(*(a,?y_2),?z_2),*(?y,a)), eq(*(?y_2,?z_2),?y)> => no
<eq(*(*(a,?y_2),?z_2),*(?x_1,*(?y_1,a))), eq(*(?y_2,?z_2),*(?x_1,?y_1))> --> <eq(*(*(a,?y_2),?z_2),*(?x_1,*(?y_1,a))), eq(*(?y_2,?z_2),*(?x_1,?y_1))> => no
<eq(a,*(*(?x_2,?y_2),?z_2)), F> --> <F, F> => yes
<eq(a,*(?x_1,*(?y_1,?z_1))), F> --> <F, F> => yes
CP(S,symP):
<eq(?x,?y), eq(*(?y,a),*(a,?x))> --> <eq(?x,?y), eq(*(?y,a),*(a,?x))> => no
<T, eq(a,a)> --> <T, T> => yes
<F, eq(*(?x,?y),a)> --> <F, eq(*(?x,?y),a)> => no
check joinability condition:
check modulo reachablity from eq(?x,*(?x_1,?y_1)) to eq(*(a,?x),*(?x_1,*(?y_1,a))): maybe not reachable
check modulo reachablity from eq(*(?y_2,?z_2),?y) to eq(*(*(a,?y_2),?z_2),*(?y,a)): maybe not reachable
check modulo reachablity from eq(*(?y_2,?z_2),*(?x_1,?y_1)) to eq(*(*(a,?y_2),?z_2),*(?x_1,*(?y_1,a))): maybe not reachable
check modulo reachablity from eq(?x,?y) to eq(*(?y,a),*(a,?x)): maybe not reachable
check modulo reachablity from F to eq(*(?x,?y),a): maybe not reachable
failed
failure(Step 1)
   [ eq(*(?x,?y),a) -> F ]
Added S-Rules:
   [ eq(*(?x,?y),a) -> F ]
Added P-Rules:
   [ ]
replace: eq(*(a,?x),*(?y,a)) -> eq(?x,?y) => eq(*(a,?x),*(?y,a)) -> eq(?y,?x)
STEP: 2 (linear)
S:
   [ eq(*(a,?x),*(?y,a)) -> eq(?x,?y),
     eq(a,a) -> T,
     eq(a,*(?x,?y)) -> F ]
P:
   [ *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     eq(?x,?y) -> eq(?y,?x) ]
S: terminating
CP(S,S):
CP_in(symP,S):
<eq(*(a,?x_1),*(?x,*(?y,a))), eq(?x_1,*(?x,?y))> --> <eq(*(a,?x_1),*(?x,*(?y,a))), eq(?x_1,*(?x,?y))> => no
<eq(a,*(?x,*(?y,?z))), F> --> <F, F> => yes
<eq(*(*(a,?y),?z),*(?y_1,a)), eq(*(?y,?z),?y_1)> --> <eq(*(*(a,?y),?z),*(?y_1,a)), eq(*(?y,?z),?y_1)> => no
<eq(a,*(*(?x,?y),?z)), F> --> <F, F> => yes
CP(S,symP):
<eq(?x,?y), eq(*(?y,a),*(a,?x))> --> <eq(?x,?y), eq(*(?y,a),*(a,?x))> => no
<T, eq(a,a)> --> <T, T> => yes
<F, eq(*(?x,?y),a)> --> <F, eq(*(?x,?y),a)> => no
check joinability condition:
check modulo reachablity from eq(?x_1,*(?x,?y)) to eq(*(a,?x_1),*(?x,*(?y,a))): maybe not reachable
check modulo reachablity from eq(*(?y,?z),?y_1) to eq(*(*(a,?y),?z),*(?y_1,a)): maybe not reachable
check modulo reachablity from eq(?x,?y) to eq(*(?y,a),*(a,?x)): maybe not reachable
check modulo reachablity from F to eq(*(?x,?y),a): maybe not reachable
failed
failure(Step 2)
   [ eq(*(?x,?y),a) -> F ]
Added S-Rules:
   [ eq(*(?x,?y),a) -> F ]
Added P-Rules:
   [ ]
replace: eq(*(a,?x),*(?y,a)) -> eq(?x,?y) => eq(*(a,?x),*(?y,a)) -> eq(?y,?x)
STEP: 3 (relative)
S:
   [ eq(*(a,?x),*(?y,a)) -> eq(?x,?y),
     eq(a,a) -> T,
     eq(a,*(?x,?y)) -> F ]
P:
   [ *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     eq(?x,?y) -> eq(?y,?x) ]
Check relative termination:
   [ eq(*(a,?x),*(?y,a)) -> eq(?x,?y),
     eq(a,a) -> T,
     eq(a,*(?x,?y)) -> F ]
   [ *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     eq(?x,?y) -> eq(?y,?x) ]
Polynomial Interpretation:
  *:= (1)*x1+(1)*x2
  F:= 0
  T:= 0
  a:= 0
  eq:= (13)+(10)*x1+(9)*x1*x1+(10)*x2+(9)*x2*x2
retract eq(a,a) -> T
retract eq(a,*(?x,?y)) -> F
Polynomial Interpretation:
  *:= (1)*x1+(2)*x1*x2+(1)*x2
  F:= 0
  T:= (4)
  a:= (1)
  eq:= (13)+(8)*x1+(12)*x1*x2+(8)*x2
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 3)
STEP: 4 (parallel)
S:
   [ eq(*(a,?x),*(?y,a)) -> eq(?x,?y),
     eq(a,a) -> T,
     eq(a,*(?x,?y)) -> F,
     eq(*(?x,?y),a) -> F ]
P:
   [ *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     eq(?x,?y) -> eq(?y,?x) ]
S: terminating
CP(S,S):
PCP_in(symP,S):
<eq(*(a,?x),*(?x_1,*(?y_1,a))), eq(?x,*(?x_1,?y_1))> --> <eq(*(a,?x),*(?x_1,*(?y_1,a))), eq(?x,*(?x_1,?y_1))> => no
<eq(*(*(a,?y_2),?z_2),*(?y,a)), eq(*(?y_2,?z_2),?y)> --> <eq(*(*(a,?y_2),?z_2),*(?y,a)), eq(*(?y_2,?z_2),?y)> => no
<eq(*(*(a,?y_2),?z_2),*(?x_1,*(?y_1,a))), eq(*(?y_2,?z_2),*(?x_1,?y_1))> --> <eq(*(*(a,?y_2),?z_2),*(?x_1,*(?y_1,a))), eq(*(?y_2,?z_2),*(?x_1,?y_1))> => no
<eq(a,*(*(?x_2,?y_2),?z_2)), F> --> <F, F> => yes
<eq(a,*(?x_1,*(?y_1,?z_1))), F> --> <F, F> => yes
<eq(*(*(?x_2,?y_2),?z_2),a), F> --> <F, F> => yes
<eq(*(?x_1,*(?y_1,?z_1)),a), F> --> <F, F> => yes
CP(S,symP):
<eq(?x,?y), eq(*(?y,a),*(a,?x))> --> <eq(?x,?y), eq(*(?y,a),*(a,?x))> => no
<T, eq(a,a)> --> <T, T> => yes
<F, eq(*(?x,?y),a)> --> <F, F> => yes
<F, eq(a,*(?x,?y))> --> <F, F> => yes
check joinability condition:
check modulo reachablity from eq(?x,*(?x_1,?y_1)) to eq(*(a,?x),*(?x_1,*(?y_1,a))): maybe not reachable
check modulo reachablity from eq(*(?y_2,?z_2),?y) to eq(*(*(a,?y_2),?z_2),*(?y,a)): maybe not reachable
check modulo reachablity from eq(*(?y_2,?z_2),*(?x_1,?y_1)) to eq(*(*(a,?y_2),?z_2),*(?x_1,*(?y_1,a))): maybe not reachable
check modulo reachablity from eq(?x,?y) to eq(*(?y,a),*(a,?x)): maybe not reachable
failed
failure(Step 4)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
replace: eq(*(a,?x),*(?y,a)) -> eq(?x,?y) => eq(*(a,?x),*(?y,a)) -> eq(?y,?x)
STEP: 5 (linear)
S:
   [ eq(*(a,?x),*(?y,a)) -> eq(?x,?y),
     eq(a,a) -> T,
     eq(a,*(?x,?y)) -> F,
     eq(*(?x,?y),a) -> F ]
P:
   [ *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     eq(?x,?y) -> eq(?y,?x) ]
S: terminating
CP(S,S):
CP_in(symP,S):
<eq(*(a,?x_1),*(?x,*(?y,a))), eq(?x_1,*(?x,?y))> --> <eq(*(a,?x_1),*(?x,*(?y,a))), eq(?x_1,*(?x,?y))> => no
<eq(a,*(?x,*(?y,?z))), F> --> <F, F> => yes
<eq(*(?x,*(?y,?z)),a), F> --> <F, F> => yes
<eq(*(*(a,?y),?z),*(?y_1,a)), eq(*(?y,?z),?y_1)> --> <eq(*(*(a,?y),?z),*(?y_1,a)), eq(*(?y,?z),?y_1)> => no
<eq(a,*(*(?x,?y),?z)), F> --> <F, F> => yes
<eq(*(*(?x,?y),?z),a), F> --> <F, F> => yes
CP(S,symP):
<eq(?x,?y), eq(*(?y,a),*(a,?x))> --> <eq(?x,?y), eq(*(?y,a),*(a,?x))> => no
<T, eq(a,a)> --> <T, T> => yes
<F, eq(*(?x,?y),a)> --> <F, F> => yes
<F, eq(a,*(?x,?y))> --> <F, F> => yes
check joinability condition:
check modulo reachablity from eq(?x_1,*(?x,?y)) to eq(*(a,?x_1),*(?x,*(?y,a))): maybe not reachable
check modulo reachablity from eq(*(?y,?z),?y_1) to eq(*(*(a,?y),?z),*(?y_1,a)): maybe not reachable
check modulo reachablity from eq(?x,?y) to eq(*(?y,a),*(a,?x)): maybe not reachable
failed
failure(Step 5)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
replace: eq(*(a,?x),*(?y,a)) -> eq(?x,?y) => eq(*(a,?x),*(?y,a)) -> eq(?y,?x)
STEP: 6 (relative)
S:
   [ eq(*(a,?x),*(?y,a)) -> eq(?x,?y),
     eq(a,a) -> T,
     eq(a,*(?x,?y)) -> F,
     eq(*(?x,?y),a) -> F ]
P:
   [ *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     eq(?x,?y) -> eq(?y,?x) ]
Check relative termination:
   [ eq(*(a,?x),*(?y,a)) -> eq(?x,?y),
     eq(a,a) -> T,
     eq(a,*(?x,?y)) -> F,
     eq(*(?x,?y),a) -> F ]
   [ *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     eq(?x,?y) -> eq(?y,?x) ]
Polynomial Interpretation:
  *:= (1)*x1+(1)*x2
  F:= 0
  T:= (8)
  a:= 0
  eq:= (5)+(14)*x1+(13)*x1*x1+(14)*x2+(13)*x2*x2
retract eq(a,*(?x,?y)) -> F
retract eq(*(?x,?y),a) -> F
Polynomial Interpretation:
  *:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
  F:= 0
  T:= 0
  a:= 0
  eq:= (4)+(1)*x1+(6)*x1*x2+(1)*x2
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 6)
STEP: 7 (parallel)
S:
   [ eq(*(a,?x),*(?y,a)) -> eq(?y,?x),
     eq(a,a) -> T,
     eq(a,*(?x,?y)) -> F ]
P:
   [ *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     eq(?x,?y) -> eq(?y,?x) ]
S: terminating
CP(S,S):
PCP_in(symP,S):
<eq(*(a,?x),*(?x_1,*(?y_1,a))), eq(*(?x_1,?y_1),?x)> --> <eq(*(a,?x),*(?x_1,*(?y_1,a))), eq(*(?x_1,?y_1),?x)> => no
<eq(*(*(a,?y_2),?z_2),*(?y,a)), eq(?y,*(?y_2,?z_2))> --> <eq(*(*(a,?y_2),?z_2),*(?y,a)), eq(?y,*(?y_2,?z_2))> => no
<eq(*(*(a,?y_2),?z_2),*(?x_1,*(?y_1,a))), eq(*(?x_1,?y_1),*(?y_2,?z_2))> --> <eq(*(*(a,?y_2),?z_2),*(?x_1,*(?y_1,a))), eq(*(?x_1,?y_1),*(?y_2,?z_2))> => no
<eq(a,*(*(?x_2,?y_2),?z_2)), F> --> <F, F> => yes
<eq(a,*(?x_1,*(?y_1,?z_1))), F> --> <F, F> => yes
CP(S,symP):
<eq(?y,?x), eq(*(?y,a),*(a,?x))> --> <eq(?y,?x), eq(*(?y,a),*(a,?x))> => no
<T, eq(a,a)> --> <T, T> => yes
<F, eq(*(?x,?y),a)> --> <F, eq(*(?x,?y),a)> => no
check joinability condition:
check modulo reachablity from eq(*(?x_1,?y_1),?x) to eq(*(a,?x),*(?x_1,*(?y_1,a))): maybe not reachable
check modulo reachablity from eq(?y,*(?y_2,?z_2)) to eq(*(*(a,?y_2),?z_2),*(?y,a)): maybe not reachable
check modulo reachablity from eq(*(?x_1,?y_1),*(?y_2,?z_2)) to eq(*(*(a,?y_2),?z_2),*(?x_1,*(?y_1,a))): maybe not reachable
check modulo reachablity from eq(?y,?x) to eq(*(?y,a),*(a,?x)): maybe not reachable
check modulo reachablity from F to eq(*(?x,?y),a): maybe not reachable
failed
failure(Step 7)
   [ eq(*(?x,?y),a) -> F ]
Added S-Rules:
   [ eq(*(?x,?y),a) -> F ]
Added P-Rules:
   [ ]
replace: eq(*(a,?x),*(?y,a)) -> eq(?y,?x) => eq(*(a,?x),*(?y,a)) -> eq(?x,?y)
STEP: 8 (linear)
S:
   [ eq(*(a,?x),*(?y,a)) -> eq(?y,?x),
     eq(a,a) -> T,
     eq(a,*(?x,?y)) -> F ]
P:
   [ *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     eq(?x,?y) -> eq(?y,?x) ]
S: terminating
CP(S,S):
CP_in(symP,S):
<eq(*(a,?x_1),*(?x,*(?y,a))), eq(*(?x,?y),?x_1)> --> <eq(*(a,?x_1),*(?x,*(?y,a))), eq(*(?x,?y),?x_1)> => no
<eq(a,*(?x,*(?y,?z))), F> --> <F, F> => yes
<eq(*(*(a,?y),?z),*(?y_1,a)), eq(?y_1,*(?y,?z))> --> <eq(*(*(a,?y),?z),*(?y_1,a)), eq(?y_1,*(?y,?z))> => no
<eq(a,*(*(?x,?y),?z)), F> --> <F, F> => yes
CP(S,symP):
<eq(?y,?x), eq(*(?y,a),*(a,?x))> --> <eq(?y,?x), eq(*(?y,a),*(a,?x))> => no
<T, eq(a,a)> --> <T, T> => yes
<F, eq(*(?x,?y),a)> --> <F, eq(*(?x,?y),a)> => no
check joinability condition:
check modulo reachablity from eq(*(?x,?y),?x_1) to eq(*(a,?x_1),*(?x,*(?y,a))): maybe not reachable
check modulo reachablity from eq(?y_1,*(?y,?z)) to eq(*(*(a,?y),?z),*(?y_1,a)): maybe not reachable
check modulo reachablity from eq(?y,?x) to eq(*(?y,a),*(a,?x)): maybe not reachable
check modulo reachablity from F to eq(*(?x,?y),a): maybe not reachable
failed
failure(Step 8)
   [ eq(*(?x,?y),a) -> F ]
Added S-Rules:
   [ eq(*(?x,?y),a) -> F ]
Added P-Rules:
   [ ]
replace: eq(*(a,?x),*(?y,a)) -> eq(?y,?x) => eq(*(a,?x),*(?y,a)) -> eq(?x,?y)
STEP: 9 (relative)
S:
   [ eq(*(a,?x),*(?y,a)) -> eq(?y,?x),
     eq(a,a) -> T,
     eq(a,*(?x,?y)) -> F ]
P:
   [ *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     eq(?x,?y) -> eq(?y,?x) ]
Check relative termination:
   [ eq(*(a,?x),*(?y,a)) -> eq(?y,?x),
     eq(a,a) -> T,
     eq(a,*(?x,?y)) -> F ]
   [ *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     eq(?x,?y) -> eq(?y,?x) ]
Polynomial Interpretation:
  *:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
  F:= 0
  T:= 0
  a:= 0
  eq:= (4)+(4)*x1+(4)*x2
retract eq(a,a) -> T
retract eq(a,*(?x,?y)) -> F
Polynomial Interpretation:
  *:= (1)*x1+(1)*x2
  F:= 0
  T:= 0
  a:= (4)
  eq:= (15)+(1)*x1+(3)*x1*x1+(1)*x2+(3)*x2*x2
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 9)
STEP: 10 (parallel)
S:
   [ eq(*(a,?x),*(?y,a)) -> eq(?y,?x),
     eq(a,a) -> T,
     eq(a,*(?x,?y)) -> F,
     eq(*(?x,?y),a) -> F ]
P:
   [ *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     eq(?x,?y) -> eq(?y,?x) ]
S: terminating
CP(S,S):
PCP_in(symP,S):
<eq(*(a,?x),*(?x_1,*(?y_1,a))), eq(*(?x_1,?y_1),?x)> --> <eq(*(a,?x),*(?x_1,*(?y_1,a))), eq(*(?x_1,?y_1),?x)> => no
<eq(*(*(a,?y_2),?z_2),*(?y,a)), eq(?y,*(?y_2,?z_2))> --> <eq(*(*(a,?y_2),?z_2),*(?y,a)), eq(?y,*(?y_2,?z_2))> => no
<eq(*(*(a,?y_2),?z_2),*(?x_1,*(?y_1,a))), eq(*(?x_1,?y_1),*(?y_2,?z_2))> --> <eq(*(*(a,?y_2),?z_2),*(?x_1,*(?y_1,a))), eq(*(?x_1,?y_1),*(?y_2,?z_2))> => no
<eq(a,*(*(?x_2,?y_2),?z_2)), F> --> <F, F> => yes
<eq(a,*(?x_1,*(?y_1,?z_1))), F> --> <F, F> => yes
<eq(*(*(?x_2,?y_2),?z_2),a), F> --> <F, F> => yes
<eq(*(?x_1,*(?y_1,?z_1)),a), F> --> <F, F> => yes
CP(S,symP):
<eq(?y,?x), eq(*(?y,a),*(a,?x))> --> <eq(?y,?x), eq(*(?y,a),*(a,?x))> => no
<T, eq(a,a)> --> <T, T> => yes
<F, eq(*(?x,?y),a)> --> <F, F> => yes
<F, eq(a,*(?x,?y))> --> <F, F> => yes
check joinability condition:
check modulo reachablity from eq(*(?x_1,?y_1),?x) to eq(*(a,?x),*(?x_1,*(?y_1,a))): maybe not reachable
check modulo reachablity from eq(?y,*(?y_2,?z_2)) to eq(*(*(a,?y_2),?z_2),*(?y,a)): maybe not reachable
check modulo reachablity from eq(*(?x_1,?y_1),*(?y_2,?z_2)) to eq(*(*(a,?y_2),?z_2),*(?x_1,*(?y_1,a))): maybe not reachable
check modulo reachablity from eq(?y,?x) to eq(*(?y,a),*(a,?x)): maybe not reachable
failed
failure(Step 10)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
replace: eq(*(a,?x),*(?y,a)) -> eq(?y,?x) => eq(*(a,?x),*(?y,a)) -> eq(?x,?y)
STEP: 11 (linear)
S:
   [ eq(*(a,?x),*(?y,a)) -> eq(?y,?x),
     eq(a,a) -> T,
     eq(a,*(?x,?y)) -> F,
     eq(*(?x,?y),a) -> F ]
P:
   [ *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     eq(?x,?y) -> eq(?y,?x) ]
S: terminating
CP(S,S):
CP_in(symP,S):
<eq(*(a,?x_1),*(?x,*(?y,a))), eq(*(?x,?y),?x_1)> --> <eq(*(a,?x_1),*(?x,*(?y,a))), eq(*(?x,?y),?x_1)> => no
<eq(a,*(?x,*(?y,?z))), F> --> <F, F> => yes
<eq(*(?x,*(?y,?z)),a), F> --> <F, F> => yes
<eq(*(*(a,?y),?z),*(?y_1,a)), eq(?y_1,*(?y,?z))> --> <eq(*(*(a,?y),?z),*(?y_1,a)), eq(?y_1,*(?y,?z))> => no
<eq(a,*(*(?x,?y),?z)), F> --> <F, F> => yes
<eq(*(*(?x,?y),?z),a), F> --> <F, F> => yes
CP(S,symP):
<eq(?y,?x), eq(*(?y,a),*(a,?x))> --> <eq(?y,?x), eq(*(?y,a),*(a,?x))> => no
<T, eq(a,a)> --> <T, T> => yes
<F, eq(*(?x,?y),a)> --> <F, F> => yes
<F, eq(a,*(?x,?y))> --> <F, F> => yes
check joinability condition:
check modulo reachablity from eq(*(?x,?y),?x_1) to eq(*(a,?x_1),*(?x,*(?y,a))): maybe not reachable
check modulo reachablity from eq(?y_1,*(?y,?z)) to eq(*(*(a,?y),?z),*(?y_1,a)): maybe not reachable
check modulo reachablity from eq(?y,?x) to eq(*(?y,a),*(a,?x)): maybe not reachable
failed
failure(Step 11)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
replace: eq(*(a,?x),*(?y,a)) -> eq(?y,?x) => eq(*(a,?x),*(?y,a)) -> eq(?x,?y)
STEP: 12 (relative)
S:
   [ eq(*(a,?x),*(?y,a)) -> eq(?y,?x),
     eq(a,a) -> T,
     eq(a,*(?x,?y)) -> F,
     eq(*(?x,?y),a) -> F ]
P:
   [ *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     eq(?x,?y) -> eq(?y,?x) ]
Check relative termination:
   [ eq(*(a,?x),*(?y,a)) -> eq(?y,?x),
     eq(a,a) -> T,
     eq(a,*(?x,?y)) -> F,
     eq(*(?x,?y),a) -> F ]
   [ *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     eq(?x,?y) -> eq(?y,?x) ]
Polynomial Interpretation:
  *:= (1)*x1+(1)*x2
  F:= 0
  T:= (8)
  a:= (8)
  eq:= (11)+(8)*x1*x1+(1)*x1*x2+(8)*x2*x2
retract eq(a,a) -> T
retract eq(a,*(?x,?y)) -> F
retract eq(*(?x,?y),a) -> F
Polynomial Interpretation:
  *:= (1)*x1+(1)*x2
  F:= 0
  T:= 0
  a:= (4)
  eq:= (7)+(1)*x1+(7)*x1*x1+(1)*x2+(7)*x2*x2
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 12)
failure(no possibility remains)
unknown Reduction-Preserving Completion
Direct Methods: Can't judge

Try Persistent Decomposition for...
   [ *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     eq(*(a,?x),*(?y,a)) -> eq(?x,?y),
     eq(a,a) -> T,
     eq(a,*(?x,?y)) -> F,
     eq(?x,?y) -> eq(?y,?x) ]
Sort Assignment:
 * : 20*20=>20
 F : =>22
 T : =>22
 a : =>20
 eq : 20*20=>22
maximal types: {20,22}
Persistent Decomposition failed: Can't judge

Try Layer Preserving Decomposition for...
   [ *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     eq(*(a,?x),*(?y,a)) -> eq(?x,?y),
     eq(a,a) -> T,
     eq(a,*(?x,?y)) -> F,
     eq(?x,?y) -> eq(?y,?x) ]
Layer Preserving Decomposition failed: Can't judge

Try Commutative Decomposition for...
   [ *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)),
     eq(*(a,?x),*(?y,a)) -> eq(?x,?y),
     eq(a,a) -> T,
     eq(a,*(?x,?y)) -> F,
     eq(?x,?y) -> eq(?y,?x) ]
Outside Critical Pair: <*(?x_1,*(?y_1,*(?y,?z))), *(*(*(?x_1,?y_1),?y),?z)> by Rules <1, 0>
develop reducts from lhs term...
<{0}, *(*(?x_1,?y_1),*(?y,?z))>
<{0}, *(?x_1,*(*(?y_1,?y),?z))>
<{}, *(?x_1,*(?y_1,*(?y,?z)))>
develop reducts from rhs term...
<{1}, *(*(?x_1,?y_1),*(?y,?z))>
<{1}, *(*(?x_1,*(?y_1,?y)),?z)>
<{}, *(*(*(?x_1,?y_1),?y),?z)>
Outside Critical Pair: <eq(*(?y_2,a),*(a,?x_2)), eq(?x_2,?y_2)> by Rules <5, 2>
develop reducts from lhs term...
<{5}, eq(*(a,?x_2),*(?y_2,a))>
<{}, eq(*(?y_2,a),*(a,?x_2))>
develop reducts from rhs term...
<{5}, eq(?y_2,?x_2)>
<{}, eq(?x_2,?y_2)>
Outside Critical Pair: <eq(a,a), T> by Rules <5, 3>
develop reducts from lhs term...
<{5}, eq(a,a)>
<{3}, T>
<{}, eq(a,a)>
develop reducts from rhs term...
<{}, T>
Outside Critical Pair: <eq(*(?x_3,?y_3),a), F> by Rules <5, 4>
develop reducts from lhs term...
<{5}, eq(a,*(?x_3,?y_3))>
<{}, eq(*(?x_3,?y_3),a)>
develop reducts from rhs term...
<{}, F>
Inside Critical Pair: <*(?x,*(?x_1,*(?y_1,?z_1))), *(*(?x,*(?x_1,?y_1)),?z_1)> by Rules <1, 0>
develop reducts from lhs term...
<{0}, *(*(?x,?x_1),*(?y_1,?z_1))>
<{0}, *(?x,*(*(?x_1,?y_1),?z_1))>
<{}, *(?x,*(?x_1,*(?y_1,?z_1)))>
develop reducts from rhs term...
<{1}, *(?x,*(*(?x_1,?y_1),?z_1))>
<{0}, *(*(*(?x,?x_1),?y_1),?z_1)>
<{}, *(*(?x,*(?x_1,?y_1)),?z_1)>
Inside Critical Pair: <*(*(*(?x,?y),?z),?z_1), *(?x,*(*(?y,?z),?z_1))> by Rules <0, 1>
develop reducts from lhs term...
<{1}, *(*(?x,?y),*(?z,?z_1))>
<{1}, *(*(?x,*(?y,?z)),?z_1)>
<{}, *(*(*(?x,?y),?z),?z_1)>
develop reducts from rhs term...
<{0}, *(*(?x,*(?y,?z)),?z_1)>
<{1}, *(?x,*(?y,*(?z,?z_1)))>
<{}, *(?x,*(*(?y,?z),?z_1))>
Inside Critical Pair: <eq(*(*(a,?y),?z),*(?y_2,a)), eq(*(?y,?z),?y_2)> by Rules <0, 2>
develop reducts from lhs term...
<{1,5}, eq(*(?y_2,a),*(a,*(?y,?z)))>
<{5}, eq(*(?y_2,a),*(*(a,?y),?z))>
<{1}, eq(*(a,*(?y,?z)),*(?y_2,a))>
<{}, eq(*(*(a,?y),?z),*(?y_2,a))>
develop reducts from rhs term...
<{5}, eq(?y_2,*(?y,?z))>
<{}, eq(*(?y,?z),?y_2)>
Inside Critical Pair: <eq(*(a,?x_2),*(?x_1,*(?y_1,a))), eq(?x_2,*(?x_1,?y_1))> by Rules <1, 2>
develop reducts from lhs term...
<{0,5}, eq(*(*(?x_1,?y_1),a),*(a,?x_2))>
<{5}, eq(*(?x_1,*(?y_1,a)),*(a,?x_2))>
<{0}, eq(*(a,?x_2),*(*(?x_1,?y_1),a))>
<{}, eq(*(a,?x_2),*(?x_1,*(?y_1,a)))>
develop reducts from rhs term...
<{5}, eq(*(?x_1,?y_1),?x_2)>
<{}, eq(?x_2,*(?x_1,?y_1))>
Inside Critical Pair: <eq(a,*(*(?x,?y),?z)), F> by Rules <0, 4>
develop reducts from lhs term...
<{1,5}, eq(*(?x,*(?y,?z)),a)>
<{5}, eq(*(*(?x,?y),?z),a)>
<{4}, F>
<{1}, eq(a,*(?x,*(?y,?z)))>
<{}, eq(a,*(*(?x,?y),?z))>
develop reducts from rhs term...
<{}, F>
Inside Critical Pair: <eq(a,*(?x_1,*(?y_1,?z_1))), F> by Rules <1, 4>
develop reducts from lhs term...
<{0,5}, eq(*(*(?x_1,?y_1),?z_1),a)>
<{5}, eq(*(?x_1,*(?y_1,?z_1)),a)>
<{4}, F>
<{0}, eq(a,*(*(?x_1,?y_1),?z_1))>
<{}, eq(a,*(?x_1,*(?y_1,?z_1)))>
develop reducts from rhs term...
<{}, F>
Try A Minimal Decomposition {4,2,5,0,1}{3}
{4,2,5,0,1}
(cm)Rewrite Rules:
   [ eq(a,*(?x,?y)) -> F,
     eq(*(a,?x),*(?y,a)) -> eq(?x,?y),
     eq(?x,?y) -> eq(?y,?x),
     *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)) ]
Apply Direct Methods...
Inner CPs:
   [ eq(a,*(*(?x_3,?y_3),?z_3)) = F,
     eq(a,*(?x_4,*(?y_4,?z_4))) = F,
     eq(*(*(a,?y_3),?z_3),*(?y_1,a)) = eq(*(?y_3,?z_3),?y_1),
     eq(*(a,?x_1),*(?x_4,*(?y_4,a))) = eq(?x_1,*(?x_4,?y_4)),
     *(?x_3,*(?x_4,*(?y_4,?z_4))) = *(*(?x_3,*(?x_4,?y_4)),?z_4),
     *(*(*(?x_3,?y_3),?z_3),?z_4) = *(?x_3,*(*(?y_3,?z_3),?z_4)),
     *(?x_1,*(*(?x,?y),?z)) = *(*(?x_1,?x),*(?y,?z)),
     *(*(?x,*(?y,?z)),?z_1) = *(*(?x,?y),*(?z,?z_1)) ]
Outer CPs:
   [ F = eq(*(?x,?y),a),
     eq(?x_1,?y_1) = eq(*(?y_1,a),*(a,?x_1)),
     *(*(*(?x_4,?y_4),?y_3),?z_3) = *(?x_4,*(?y_4,*(?y_3,?z_3))) ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth & Bendix
Linear
unknown Development Closed
unknown Strongly 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:
   [ eq(*(*(?x,?y_4),?z_4),a) = F,
     eq(*(?x_5,*(?y_5,?y)),a) = F,
     eq(*(?x,?y),a) = F,
     eq(a,*(*(?x,?y_4),?z_4)) = F,
     eq(a,*(?x_5,*(?y_5,?y))) = F,
     eq(*(?x_9,*(?y_9,a)),*(*(a,?y_4),?z_4)) = eq(*(?y_4,?z_4),*(?x_9,?y_9)),
     eq(*(?y,a),*(*(a,?y_4),?z_4)) = eq(*(?y_4,?z_4),?y),
     eq(*(?x_5,*(?y_5,a)),*(a,?x)) = eq(?x,*(?x_5,?y_5)),
     eq(*(*(a,?y_4),?z_4),*(?x_9,*(?y_9,a))) = eq(*(?y_4,?z_4),*(?x_9,?y_9)),
     eq(*(?y,a),*(a,?x)) = eq(?x,?y),
     eq(*(*(a,?y_4),?z_4),*(?y,a)) = eq(*(?y_4,?z_4),?y),
     eq(*(a,?x),*(?x_5,*(?y_5,a))) = eq(?x,*(?x_5,?y_5)),
     F = eq(*(?x_1,?y_1),a),
     eq(?x_2,?y_2) = eq(*(?y_2,a),*(a,?x_2)),
     *(?x_4,*(?y_4,*(*(?y,?y_5),?z_5))) = *(*(*(?x_4,?y_4),?y),*(?y_5,?z_5)),
     *(?x_4,*(?y_4,*(?x_9,*(?y_9,?z)))) = *(*(*(?x_4,?y_4),*(?x_9,?y_9)),?z),
     *(?x_4,*(?y_4,*(?y,?z))) = *(*(*(?x_4,?y_4),?y),?z),
     *(?x,*(*(?y,?y_1),?z_1)) = *(*(?x,?y),*(?y_1,?z_1)),
     *(?x,*(?x_5,*(?y_5,?z))) = *(*(?x,*(?x_5,?y_5)),?z),
     *(*(?x_1,?x),*(*(?y,?y_2),?z_2)) = *(?x_1,*(*(?x,?y),*(?y_2,?z_2))),
     *(*(?x_1,?x),*(?x_6,*(?y_6,?z))) = *(?x_1,*(*(?x,*(?x_6,?y_6)),?z)),
     F = eq(a,*(*(?x,?y),*(?y_1,?z_1))),
     F = eq(a,*(*(?x,*(?x_5,?y_5)),?z)),
     eq(*(*(?y,?y_4),?z_4),?y_3) = eq(*(*(a,?y),*(?y_4,?z_4)),*(?y_3,a)),
     eq(*(?x_8,*(?y_8,?z)),?y_3) = eq(*(*(a,*(?x_8,?y_8)),?z),*(?y_3,a)),
     *(?x,*(*(*(?y,?y_6),?z_6),?z_5)) = *(*(*(?x,?y),*(?y_6,?z_6)),?z_5),
     *(?x,*(*(?x_10,*(?y_10,?z)),?z_5)) = *(*(*(?x,*(?x_10,?y_10)),?z),?z_5),
     *(*(?x_1,?x),*(?y,?z)) = *(?x_1,*(*(?x,?y),?z)),
     F = eq(a,*(*(?x,?y),?z)),
     eq(*(?y,?z),?y_3) = eq(*(*(a,?y),?z),*(?y_3,a)),
     *(?x,*(*(?y,?z),?z_5)) = *(*(*(?x,?y),?z),?z_5),
     *(*(*(?x_5,*(?y_5,?y)),?y_4),?z_4) = *(*(?x_5,?y_5),*(?y,*(?y_4,?z_4))),
     *(*(*(*(?x,?y_9),?z_9),?y_4),?z_4) = *(?x,*(*(?y_9,?z_9),*(?y_4,?z_4))),
     *(*(*(?x,?y),?y_4),?z_4) = *(?x,*(?y,*(?y_4,?z_4))),
     *(*(?x_1,*(?y_1,?y)),?z) = *(*(?x_1,?y_1),*(?y,?z)),
     *(*(*(?x,?y_5),?z_5),?z) = *(?x,*(*(?y_5,?z_5),?z)),
     *(*(?x_2,*(?y_2,?y)),*(?z,?z_1)) = *(*(*(?x_2,?y_2),*(?y,?z)),?z_1),
     *(*(*(?x,?y_6),?z_6),*(?z,?z_1)) = *(*(?x,*(*(?y_6,?z_6),?z)),?z_1),
     F = eq(a,*(?x,*(*(?y_5,?z_5),?z))),
     eq(?x_3,*(?x_4,*(?y_4,?y))) = eq(*(a,?x_3),*(*(?x_4,?y_4),*(?y,a))),
     eq(?x_3,*(*(?x,?y_8),?z_8)) = eq(*(a,?x_3),*(?x,*(*(?y_8,?z_8),a))),
     *(*(?x_5,*(?x_6,*(?y_6,?y))),?z) = *(?x_5,*(*(?x_6,?y_6),*(?y,?z))),
     *(*(?x_5,*(*(?x,?y_10),?z_10)),?z) = *(?x_5,*(?x,*(*(?y_10,?z_10),?z))),
     *(*(?x,?y),*(?z,?z_1)) = *(*(?x,*(?y,?z)),?z_1),
     F = eq(a,*(?x,*(?y,?z))),
     eq(?x_3,*(?x,?y)) = eq(*(a,?x_3),*(?x,*(?y,a))),
     *(*(?x_5,*(?x,?y)),?z) = *(?x_5,*(?x,*(?y,?z))) ]
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 <eq(a,*(*(?x_3,?y_3),?z_3)), F> by Rules <3, 0> preceded by [(eq,2)]
 joinable by a reduction of rules <[([],0)], []>
Critical Pair <eq(a,*(?x_4,*(?y_4,?z_4))), F> by Rules <4, 0> preceded by [(eq,2)]
 joinable by a reduction of rules <[([],0)], []>
Critical Pair <eq(*(*(a,?y_3),?z_3),*(?y_1,a)), eq(*(?y_3,?z_3),?y_1)> by Rules <3, 1> preceded by [(eq,1)]
 joinable by a reduction of rules <[([(eq,1)],4),([],1)], []>
Critical Pair <eq(*(a,?x_1),*(?x_4,*(?y_4,a))), eq(?x_1,*(?x_4,?y_4))> by Rules <4, 1> preceded by [(eq,2)]
 joinable by a reduction of rules <[([(eq,2)],3),([],1)], []>
Critical Pair <*(?x_3,*(?x_4,*(?y_4,?z_4))), *(*(?x_3,*(?x_4,?y_4)),?z_4)> by Rules <4, 3> preceded by [(*,2)]
 joinable by a reduction of rules <[([(*,2)],3)], [([],4)]>
Critical Pair <*(*(*(?x_3,?y_3),?z_3),?z_4), *(?x_3,*(*(?y_3,?z_3),?z_4))> by Rules <3, 4> preceded by [(*,1)]
 joinable by a reduction of rules <[([(*,1)],4)], [([],3)]>
Critical Pair <*(?x_1,*(*(?x,?y),?z)), *(*(?x_1,?x),*(?y,?z))> by Rules <3, 3> preceded by [(*,2)]
 joinable by a reduction of rules <[([(*,2)],4)], [([],4)]>
Critical Pair <*(*(?x,*(?y,?z)),?z_1), *(*(?x,?y),*(?z,?z_1))> by Rules <4, 4> preceded by [(*,1)]
 joinable by a reduction of rules <[([(*,1)],3)], [([],3)]>
Critical Pair <eq(*(?x,?y),a), F> by Rules <2, 0> preceded by []
 joinable by a reduction of rules <[([],2),([],0)], []>
Critical Pair <eq(*(?y_1,a),*(a,?x_1)), eq(?x_1,?y_1)> by Rules <2, 1> preceded by []
 joinable by a reduction of rules <[([],2),([],1)], []>
Critical Pair <*(?x_4,*(?y_4,*(?y_3,?z_3))), *(*(*(?x_4,?y_4),?y_3),?z_3)> by Rules <4, 3> preceded by []
 joinable by a reduction of rules <[([],3)], [([],4)]>
unknown Diagram Decreasing
check Non-Confluence...
obtain 15 rules by 3 steps unfolding
strenghten eq(?x_6,?y_6) and eq(?y_6,?x_6)
strenghten eq(*(?x,?y),a) and F
strenghten eq(a,*(?x,?y)) and F
strenghten eq(*(?x_4,*(?y_4,?z_4)),a) and F
strenghten eq(*(*(?x_3,?y_3),?z_3),a) and F
strenghten eq(a,*(?x_4,*(?y_4,?z_4))) and F
strenghten eq(a,*(*(?x_3,?y_3),?z_3)) and F
strenghten eq(*(?y_1,a),*(a,?x_1)) and eq(?x_1,?y_1)
strenghten eq(*(a,?x_1),*(?y_1,a)) and eq(?x_1,?y_1)
strenghten *(?x_3,*(*(?y_3,?z_3),?z_4)) and *(*(*(?x_3,?y_3),?z_3),?z_4)
strenghten *(*(?x,?y),*(?z,?z_1)) and *(*(?x,*(?y,?z)),?z_1)
strenghten *(*(?x_1,?x),*(?y,?z)) and *(?x_1,*(*(?x,?y),?z))
strenghten *(*(?x_3,*(?x_4,?y_4)),?z_4) and *(?x_3,*(?x_4,*(?y_4,?z_4)))
strenghten *(*(*(?x_4,?y_4),?y_3),?z_3) and *(?x_4,*(?y_4,*(?y_3,?z_3)))
strenghten eq(*(*(a,?y_3),?z_3),*(?y_1,a)) and eq(*(?y_3,?z_3),?y_1)
strenghten eq(*(a,?x_1),*(?x_4,*(?y_4,a))) and eq(?x_1,*(?x_4,?y_4))
obtain 49 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:
   [ eq(a,*(?x,?y)) -> F,
     eq(*(a,?x),*(?y,a)) -> eq(?x,?y),
     *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)) ]
   [ eq(?x,?y) -> eq(?y,?x) ]
Polynomial Interpretation:
  *:= (1)*x1+(1)*x2
  F:= (4)
  a:= (2)
  eq:= (2)+(4)*x1+(4)*x2
retract eq(a,*(?x,?y)) -> F
Polynomial Interpretation:
  *:= (1)*x1+(1)*x2
  F:= 0
  a:= (1)
  eq:= (5)+(1)*x1+(4)*x1*x1+(1)*x2+(4)*x2*x2
retract eq(a,*(?x,?y)) -> F
retract eq(*(a,?x),*(?y,a)) -> eq(?x,?y)
retract eq(a,*(?x,?y)) -> F
retract eq(*(a,?x),*(?y,a)) -> eq(?x,?y)
unknown relative termination
unknown Huet (modulo AC)
check by Reduction-Preserving Completion...
STEP: 1 (parallel)
S:
   [ eq(a,*(?x,?y)) -> F,
     eq(*(a,?x),*(?y,a)) -> eq(?x,?y) ]
P:
   [ eq(?x,?y) -> eq(?y,?x),
     *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)) ]
S: terminating
CP(S,S):
PCP_in(symP,S):
<eq(a,*(*(?x_3,?y_3),?z_3)), F> --> <F, F> => yes
<eq(a,*(?x_2,*(?y_2,?z_2))), F> --> <F, F> => yes
<eq(*(a,?x),*(?x_2,*(?y_2,a))), eq(?x,*(?x_2,?y_2))> --> <eq(*(a,?x),*(?x_2,*(?y_2,a))), eq(?x,*(?x_2,?y_2))> => no
<eq(*(*(a,?y_3),?z_3),*(?y,a)), eq(*(?y_3,?z_3),?y)> --> <eq(*(*(a,?y_3),?z_3),*(?y,a)), eq(*(?y_3,?z_3),?y)> => no
<eq(*(*(a,?y_3),?z_3),*(?x_2,*(?y_2,a))), eq(*(?y_3,?z_3),*(?x_2,?y_2))> --> <eq(*(*(a,?y_3),?z_3),*(?x_2,*(?y_2,a))), eq(*(?y_3,?z_3),*(?x_2,?y_2))> => no
CP(S,symP):
<F, eq(*(?x,?y),a)> --> <F, eq(*(?x,?y),a)> => no
<eq(?x,?y), eq(*(?y,a),*(a,?x))> --> <eq(?x,?y), eq(*(?y,a),*(a,?x))> => no
check joinability condition:
check modulo reachablity from eq(?x,*(?x_2,?y_2)) to eq(*(a,?x),*(?x_2,*(?y_2,a))): maybe not reachable
check modulo reachablity from eq(*(?y_3,?z_3),?y) to eq(*(*(a,?y_3),?z_3),*(?y,a)): maybe not reachable
check modulo reachablity from eq(*(?y_3,?z_3),*(?x_2,?y_2)) to eq(*(*(a,?y_3),?z_3),*(?x_2,*(?y_2,a))): maybe not reachable
check modulo reachablity from F to eq(*(?x,?y),a): maybe not reachable
check modulo reachablity from eq(?x,?y) to eq(*(?y,a),*(a,?x)): maybe not reachable
failed
failure(Step 1)
   [ eq(*(?x,?y),a) -> F ]
Added S-Rules:
   [ eq(*(?x,?y),a) -> F ]
Added P-Rules:
   [ ]
replace: eq(*(a,?x),*(?y,a)) -> eq(?x,?y) => eq(*(a,?x),*(?y,a)) -> eq(?y,?x)
STEP: 2 (linear)
S:
   [ eq(a,*(?x,?y)) -> F,
     eq(*(a,?x),*(?y,a)) -> eq(?x,?y) ]
P:
   [ eq(?x,?y) -> eq(?y,?x),
     *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)) ]
S: terminating
CP(S,S):
CP_in(symP,S):
<eq(a,*(?x,*(?y,?z))), F> --> <F, F> => yes
<eq(*(a,?x_1),*(?x,*(?y,a))), eq(?x_1,*(?x,?y))> --> <eq(*(a,?x_1),*(?x,*(?y,a))), eq(?x_1,*(?x,?y))> => no
<eq(a,*(*(?x,?y),?z)), F> --> <F, F> => yes
<eq(*(*(a,?y),?z),*(?y_1,a)), eq(*(?y,?z),?y_1)> --> <eq(*(*(a,?y),?z),*(?y_1,a)), eq(*(?y,?z),?y_1)> => no
CP(S,symP):
<F, eq(*(?x,?y),a)> --> <F, eq(*(?x,?y),a)> => no
<eq(?x,?y), eq(*(?y,a),*(a,?x))> --> <eq(?x,?y), eq(*(?y,a),*(a,?x))> => no
check joinability condition:
check modulo reachablity from eq(?x_1,*(?x,?y)) to eq(*(a,?x_1),*(?x,*(?y,a))): maybe not reachable
check modulo reachablity from eq(*(?y,?z),?y_1) to eq(*(*(a,?y),?z),*(?y_1,a)): maybe not reachable
check modulo reachablity from F to eq(*(?x,?y),a): maybe not reachable
check modulo reachablity from eq(?x,?y) to eq(*(?y,a),*(a,?x)): maybe not reachable
failed
failure(Step 2)
   [ eq(*(?x,?y),a) -> F ]
Added S-Rules:
   [ eq(*(?x,?y),a) -> F ]
Added P-Rules:
   [ ]
replace: eq(*(a,?x),*(?y,a)) -> eq(?x,?y) => eq(*(a,?x),*(?y,a)) -> eq(?y,?x)
STEP: 3 (relative)
S:
   [ eq(a,*(?x,?y)) -> F,
     eq(*(a,?x),*(?y,a)) -> eq(?x,?y) ]
P:
   [ eq(?x,?y) -> eq(?y,?x),
     *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)) ]
Check relative termination:
   [ eq(a,*(?x,?y)) -> F,
     eq(*(a,?x),*(?y,a)) -> eq(?x,?y) ]
   [ eq(?x,?y) -> eq(?y,?x),
     *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)) ]
Polynomial Interpretation:
  *:= (1)*x1+(1)*x2
  F:= 0
  a:= 0
  eq:= (10)+(4)*x1*x1+(4)*x2*x2
retract eq(a,*(?x,?y)) -> F
Polynomial Interpretation:
  *:= (1)+(1)*x1+(1)*x2
  F:= 0
  a:= 0
  eq:= (5)+(10)*x1*x1+(15)*x1*x2+(10)*x2*x2
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 3)
STEP: 4 (parallel)
S:
   [ eq(a,*(?x,?y)) -> F,
     eq(*(a,?x),*(?y,a)) -> eq(?x,?y),
     eq(*(?x,?y),a) -> F ]
P:
   [ eq(?x,?y) -> eq(?y,?x),
     *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)) ]
S: terminating
CP(S,S):
PCP_in(symP,S):
<eq(a,*(*(?x_3,?y_3),?z_3)), F> --> <F, F> => yes
<eq(a,*(?x_2,*(?y_2,?z_2))), F> --> <F, F> => yes
<eq(*(a,?x),*(?x_2,*(?y_2,a))), eq(?x,*(?x_2,?y_2))> --> <eq(*(a,?x),*(?x_2,*(?y_2,a))), eq(?x,*(?x_2,?y_2))> => no
<eq(*(*(a,?y_3),?z_3),*(?y,a)), eq(*(?y_3,?z_3),?y)> --> <eq(*(*(a,?y_3),?z_3),*(?y,a)), eq(*(?y_3,?z_3),?y)> => no
<eq(*(*(a,?y_3),?z_3),*(?x_2,*(?y_2,a))), eq(*(?y_3,?z_3),*(?x_2,?y_2))> --> <eq(*(*(a,?y_3),?z_3),*(?x_2,*(?y_2,a))), eq(*(?y_3,?z_3),*(?x_2,?y_2))> => no
<eq(*(*(?x_3,?y_3),?z_3),a), F> --> <F, F> => yes
<eq(*(?x_2,*(?y_2,?z_2)),a), F> --> <F, F> => yes
CP(S,symP):
<F, eq(*(?x,?y),a)> --> <F, F> => yes
<eq(?x,?y), eq(*(?y,a),*(a,?x))> --> <eq(?x,?y), eq(*(?y,a),*(a,?x))> => no
<F, eq(a,*(?x,?y))> --> <F, F> => yes
check joinability condition:
check modulo reachablity from eq(?x,*(?x_2,?y_2)) to eq(*(a,?x),*(?x_2,*(?y_2,a))): maybe not reachable
check modulo reachablity from eq(*(?y_3,?z_3),?y) to eq(*(*(a,?y_3),?z_3),*(?y,a)): maybe not reachable
check modulo reachablity from eq(*(?y_3,?z_3),*(?x_2,?y_2)) to eq(*(*(a,?y_3),?z_3),*(?x_2,*(?y_2,a))): maybe not reachable
check modulo reachablity from eq(?x,?y) to eq(*(?y,a),*(a,?x)): maybe not reachable
failed
failure(Step 4)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
replace: eq(*(a,?x),*(?y,a)) -> eq(?x,?y) => eq(*(a,?x),*(?y,a)) -> eq(?y,?x)
STEP: 5 (linear)
S:
   [ eq(a,*(?x,?y)) -> F,
     eq(*(a,?x),*(?y,a)) -> eq(?x,?y),
     eq(*(?x,?y),a) -> F ]
P:
   [ eq(?x,?y) -> eq(?y,?x),
     *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)) ]
S: terminating
CP(S,S):
CP_in(symP,S):
<eq(a,*(?x,*(?y,?z))), F> --> <F, F> => yes
<eq(*(a,?x_1),*(?x,*(?y,a))), eq(?x_1,*(?x,?y))> --> <eq(*(a,?x_1),*(?x,*(?y,a))), eq(?x_1,*(?x,?y))> => no
<eq(*(?x,*(?y,?z)),a), F> --> <F, F> => yes
<eq(a,*(*(?x,?y),?z)), F> --> <F, F> => yes
<eq(*(*(a,?y),?z),*(?y_1,a)), eq(*(?y,?z),?y_1)> --> <eq(*(*(a,?y),?z),*(?y_1,a)), eq(*(?y,?z),?y_1)> => no
<eq(*(*(?x,?y),?z),a), F> --> <F, F> => yes
CP(S,symP):
<F, eq(*(?x,?y),a)> --> <F, F> => yes
<eq(?x,?y), eq(*(?y,a),*(a,?x))> --> <eq(?x,?y), eq(*(?y,a),*(a,?x))> => no
<F, eq(a,*(?x,?y))> --> <F, F> => yes
check joinability condition:
check modulo reachablity from eq(?x_1,*(?x,?y)) to eq(*(a,?x_1),*(?x,*(?y,a))): maybe not reachable
check modulo reachablity from eq(*(?y,?z),?y_1) to eq(*(*(a,?y),?z),*(?y_1,a)): maybe not reachable
check modulo reachablity from eq(?x,?y) to eq(*(?y,a),*(a,?x)): maybe not reachable
failed
failure(Step 5)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
replace: eq(*(a,?x),*(?y,a)) -> eq(?x,?y) => eq(*(a,?x),*(?y,a)) -> eq(?y,?x)
STEP: 6 (relative)
S:
   [ eq(a,*(?x,?y)) -> F,
     eq(*(a,?x),*(?y,a)) -> eq(?x,?y),
     eq(*(?x,?y),a) -> F ]
P:
   [ eq(?x,?y) -> eq(?y,?x),
     *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)) ]
Check relative termination:
   [ eq(a,*(?x,?y)) -> F,
     eq(*(a,?x),*(?y,a)) -> eq(?x,?y),
     eq(*(?x,?y),a) -> F ]
   [ eq(?x,?y) -> eq(?y,?x),
     *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)) ]
Polynomial Interpretation:
  *:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
  F:= 0
  a:= (6)
  eq:= (13)+(7)*x1+(1)*x1*x2+(7)*x2
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 6)
STEP: 7 (parallel)
S:
   [ eq(a,*(?x,?y)) -> F,
     eq(*(a,?x),*(?y,a)) -> eq(?y,?x) ]
P:
   [ eq(?x,?y) -> eq(?y,?x),
     *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)) ]
S: terminating
CP(S,S):
PCP_in(symP,S):
<eq(a,*(*(?x_3,?y_3),?z_3)), F> --> <F, F> => yes
<eq(a,*(?x_2,*(?y_2,?z_2))), F> --> <F, F> => yes
<eq(*(a,?x),*(?x_2,*(?y_2,a))), eq(*(?x_2,?y_2),?x)> --> <eq(*(a,?x),*(?x_2,*(?y_2,a))), eq(*(?x_2,?y_2),?x)> => no
<eq(*(*(a,?y_3),?z_3),*(?y,a)), eq(?y,*(?y_3,?z_3))> --> <eq(*(*(a,?y_3),?z_3),*(?y,a)), eq(?y,*(?y_3,?z_3))> => no
<eq(*(*(a,?y_3),?z_3),*(?x_2,*(?y_2,a))), eq(*(?x_2,?y_2),*(?y_3,?z_3))> --> <eq(*(*(a,?y_3),?z_3),*(?x_2,*(?y_2,a))), eq(*(?x_2,?y_2),*(?y_3,?z_3))> => no
CP(S,symP):
<F, eq(*(?x,?y),a)> --> <F, eq(*(?x,?y),a)> => no
<eq(?y,?x), eq(*(?y,a),*(a,?x))> --> <eq(?y,?x), eq(*(?y,a),*(a,?x))> => no
check joinability condition:
check modulo reachablity from eq(*(?x_2,?y_2),?x) to eq(*(a,?x),*(?x_2,*(?y_2,a))): maybe not reachable
check modulo reachablity from eq(?y,*(?y_3,?z_3)) to eq(*(*(a,?y_3),?z_3),*(?y,a)): maybe not reachable
check modulo reachablity from eq(*(?x_2,?y_2),*(?y_3,?z_3)) to eq(*(*(a,?y_3),?z_3),*(?x_2,*(?y_2,a))): maybe not reachable
check modulo reachablity from F to eq(*(?x,?y),a): maybe not reachable
check modulo reachablity from eq(?y,?x) to eq(*(?y,a),*(a,?x)): maybe not reachable
failed
failure(Step 7)
   [ eq(*(?x,?y),a) -> F ]
Added S-Rules:
   [ eq(*(?x,?y),a) -> F ]
Added P-Rules:
   [ ]
replace: eq(*(a,?x),*(?y,a)) -> eq(?y,?x) => eq(*(a,?x),*(?y,a)) -> eq(?x,?y)
STEP: 8 (linear)
S:
   [ eq(a,*(?x,?y)) -> F,
     eq(*(a,?x),*(?y,a)) -> eq(?y,?x) ]
P:
   [ eq(?x,?y) -> eq(?y,?x),
     *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)) ]
S: terminating
CP(S,S):
CP_in(symP,S):
<eq(a,*(?x,*(?y,?z))), F> --> <F, F> => yes
<eq(*(a,?x_1),*(?x,*(?y,a))), eq(*(?x,?y),?x_1)> --> <eq(*(a,?x_1),*(?x,*(?y,a))), eq(*(?x,?y),?x_1)> => no
<eq(a,*(*(?x,?y),?z)), F> --> <F, F> => yes
<eq(*(*(a,?y),?z),*(?y_1,a)), eq(?y_1,*(?y,?z))> --> <eq(*(*(a,?y),?z),*(?y_1,a)), eq(?y_1,*(?y,?z))> => no
CP(S,symP):
<F, eq(*(?x,?y),a)> --> <F, eq(*(?x,?y),a)> => no
<eq(?y,?x), eq(*(?y,a),*(a,?x))> --> <eq(?y,?x), eq(*(?y,a),*(a,?x))> => no
check joinability condition:
check modulo reachablity from eq(*(?x,?y),?x_1) to eq(*(a,?x_1),*(?x,*(?y,a))): maybe not reachable
check modulo reachablity from eq(?y_1,*(?y,?z)) to eq(*(*(a,?y),?z),*(?y_1,a)): maybe not reachable
check modulo reachablity from F to eq(*(?x,?y),a): maybe not reachable
check modulo reachablity from eq(?y,?x) to eq(*(?y,a),*(a,?x)): maybe not reachable
failed
failure(Step 8)
   [ eq(*(?x,?y),a) -> F ]
Added S-Rules:
   [ eq(*(?x,?y),a) -> F ]
Added P-Rules:
   [ ]
replace: eq(*(a,?x),*(?y,a)) -> eq(?y,?x) => eq(*(a,?x),*(?y,a)) -> eq(?x,?y)
STEP: 9 (relative)
S:
   [ eq(a,*(?x,?y)) -> F,
     eq(*(a,?x),*(?y,a)) -> eq(?y,?x) ]
P:
   [ eq(?x,?y) -> eq(?y,?x),
     *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)) ]
Check relative termination:
   [ eq(a,*(?x,?y)) -> F,
     eq(*(a,?x),*(?y,a)) -> eq(?y,?x) ]
   [ eq(?x,?y) -> eq(?y,?x),
     *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)) ]
Polynomial Interpretation:
  *:= (1)*x1+(1)*x2
  F:= (2)
  a:= 0
  eq:= (12)+(8)*x1+(8)*x2
retract eq(a,*(?x,?y)) -> F
Polynomial Interpretation:
  *:= (1)*x1+(1)*x2
  F:= 0
  a:= (4)
  eq:= (10)+(9)*x1+(9)*x2
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 9)
STEP: 10 (parallel)
S:
   [ eq(a,*(?x,?y)) -> F,
     eq(*(a,?x),*(?y,a)) -> eq(?y,?x),
     eq(*(?x,?y),a) -> F ]
P:
   [ eq(?x,?y) -> eq(?y,?x),
     *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)) ]
S: terminating
CP(S,S):
PCP_in(symP,S):
<eq(a,*(*(?x_3,?y_3),?z_3)), F> --> <F, F> => yes
<eq(a,*(?x_2,*(?y_2,?z_2))), F> --> <F, F> => yes
<eq(*(a,?x),*(?x_2,*(?y_2,a))), eq(*(?x_2,?y_2),?x)> --> <eq(*(a,?x),*(?x_2,*(?y_2,a))), eq(*(?x_2,?y_2),?x)> => no
<eq(*(*(a,?y_3),?z_3),*(?y,a)), eq(?y,*(?y_3,?z_3))> --> <eq(*(*(a,?y_3),?z_3),*(?y,a)), eq(?y,*(?y_3,?z_3))> => no
<eq(*(*(a,?y_3),?z_3),*(?x_2,*(?y_2,a))), eq(*(?x_2,?y_2),*(?y_3,?z_3))> --> <eq(*(*(a,?y_3),?z_3),*(?x_2,*(?y_2,a))), eq(*(?x_2,?y_2),*(?y_3,?z_3))> => no
<eq(*(*(?x_3,?y_3),?z_3),a), F> --> <F, F> => yes
<eq(*(?x_2,*(?y_2,?z_2)),a), F> --> <F, F> => yes
CP(S,symP):
<F, eq(*(?x,?y),a)> --> <F, F> => yes
<eq(?y,?x), eq(*(?y,a),*(a,?x))> --> <eq(?y,?x), eq(*(?y,a),*(a,?x))> => no
<F, eq(a,*(?x,?y))> --> <F, F> => yes
check joinability condition:
check modulo reachablity from eq(*(?x_2,?y_2),?x) to eq(*(a,?x),*(?x_2,*(?y_2,a))): maybe not reachable
check modulo reachablity from eq(?y,*(?y_3,?z_3)) to eq(*(*(a,?y_3),?z_3),*(?y,a)): maybe not reachable
check modulo reachablity from eq(*(?x_2,?y_2),*(?y_3,?z_3)) to eq(*(*(a,?y_3),?z_3),*(?x_2,*(?y_2,a))): maybe not reachable
check modulo reachablity from eq(?y,?x) to eq(*(?y,a),*(a,?x)): maybe not reachable
failed
failure(Step 10)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
replace: eq(*(a,?x),*(?y,a)) -> eq(?y,?x) => eq(*(a,?x),*(?y,a)) -> eq(?x,?y)
STEP: 11 (linear)
S:
   [ eq(a,*(?x,?y)) -> F,
     eq(*(a,?x),*(?y,a)) -> eq(?y,?x),
     eq(*(?x,?y),a) -> F ]
P:
   [ eq(?x,?y) -> eq(?y,?x),
     *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)) ]
S: terminating
CP(S,S):
CP_in(symP,S):
<eq(a,*(?x,*(?y,?z))), F> --> <F, F> => yes
<eq(*(a,?x_1),*(?x,*(?y,a))), eq(*(?x,?y),?x_1)> --> <eq(*(a,?x_1),*(?x,*(?y,a))), eq(*(?x,?y),?x_1)> => no
<eq(*(?x,*(?y,?z)),a), F> --> <F, F> => yes
<eq(a,*(*(?x,?y),?z)), F> --> <F, F> => yes
<eq(*(*(a,?y),?z),*(?y_1,a)), eq(?y_1,*(?y,?z))> --> <eq(*(*(a,?y),?z),*(?y_1,a)), eq(?y_1,*(?y,?z))> => no
<eq(*(*(?x,?y),?z),a), F> --> <F, F> => yes
CP(S,symP):
<F, eq(*(?x,?y),a)> --> <F, F> => yes
<eq(?y,?x), eq(*(?y,a),*(a,?x))> --> <eq(?y,?x), eq(*(?y,a),*(a,?x))> => no
<F, eq(a,*(?x,?y))> --> <F, F> => yes
check joinability condition:
check modulo reachablity from eq(*(?x,?y),?x_1) to eq(*(a,?x_1),*(?x,*(?y,a))): maybe not reachable
check modulo reachablity from eq(?y_1,*(?y,?z)) to eq(*(*(a,?y),?z),*(?y_1,a)): maybe not reachable
check modulo reachablity from eq(?y,?x) to eq(*(?y,a),*(a,?x)): maybe not reachable
failed
failure(Step 11)
   [ ]
Added S-Rules:
   [ ]
Added P-Rules:
   [ ]
replace: eq(*(a,?x),*(?y,a)) -> eq(?y,?x) => eq(*(a,?x),*(?y,a)) -> eq(?x,?y)
STEP: 12 (relative)
S:
   [ eq(a,*(?x,?y)) -> F,
     eq(*(a,?x),*(?y,a)) -> eq(?y,?x),
     eq(*(?x,?y),a) -> F ]
P:
   [ eq(?x,?y) -> eq(?y,?x),
     *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)) ]
Check relative termination:
   [ eq(a,*(?x,?y)) -> F,
     eq(*(a,?x),*(?y,a)) -> eq(?y,?x),
     eq(*(?x,?y),a) -> F ]
   [ eq(?x,?y) -> eq(?y,?x),
     *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)) ]
Polynomial Interpretation:
  *:= (2)+(1)*x1+(1)*x2
  F:= 0
  a:= 0
  eq:= (8)+(2)*x1+(8)*x1*x2+(2)*x2
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 12)
failure(no possibility remains)
unknown Reduction-Preserving Completion
Direct Methods: Can't judge

Try Persistent Decomposition for...
   [ eq(a,*(?x,?y)) -> F,
     eq(*(a,?x),*(?y,a)) -> eq(?x,?y),
     eq(?x,?y) -> eq(?y,?x),
     *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)) ]
Sort Assignment:
 * : 21*21=>21
 F : =>23
 a : =>21
 eq : 21*21=>23
maximal types: {21,23}
Persistent Decomposition failed: Can't judge

Try Layer Preserving Decomposition for...
   [ eq(a,*(?x,?y)) -> F,
     eq(*(a,?x),*(?y,a)) -> eq(?x,?y),
     eq(?x,?y) -> eq(?y,?x),
     *(?x,*(?y,?z)) -> *(*(?x,?y),?z),
     *(*(?x,?y),?z) -> *(?x,*(?y,?z)) ]
Layer Preserving Decomposition failed: Can't judge
No further decomposition possible

{3}
(cm)Rewrite Rules:
   [ eq(a,a) -> T ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [  ]
Overlay, check Innermost Termination...
Innermost Terminating (hence Terminating), WCR
Knuth & Bendix
Direct Methods: CR
Commutative Decomposition failed: Can't judge
No further decomposition possible


Final result: Can't judge
R2.trs: Failure(unknown)
(18038 msec.)