MAYBE
(ignored inputs)COMMENT due to Vincent van Oostrom. confluent
Rewrite Rules:
   [ f(f(?x,?y),?z) -> f(f(?x,?z),f(?y,?z)) ]
Apply Direct Methods...
Inner CPs:
   [ f(f(f(?x,?z),f(?y,?z)),?z_1) = f(f(f(?x,?y),?z_1),f(?z,?z_1)) ]
Outer CPs:
   [  ]
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
inner CP cond (upside-parallel)
innter CP Cond (outside)
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
   [ f(f(f(?x_1,?y),f(?y_1,?y)),?z) = f(f(f(?x_1,?y_1),?z),f(?y,?z)),
     f(f(f(f(?x_2,?y),f(?y_2,?y)),?z_1),f(?z,?z_1)) = f(f(f(f(?x_2,?y_2),?z),f(?y,?z)),?z_1),
     f(f(f(?x,?y),?z_1),f(?z,?z_1)) = f(f(f(?x,?z),f(?y,?z)),?z_1) ]
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 <f(f(f(?x,?z),f(?y,?z)),?z_1), f(f(f(?x,?y),?z_1),f(?z,?z_1))> by Rules <0, 0> preceded by [(f,1)]
 joinable by a reduction of rules <[([],0),([(f,2)],0),([(f,1)],0)], [([(f,1)],0),([],0)]>
 joinable by a reduction of rules <[([],0),([(f,1)],0),([(f,2)],0)], [([(f,1)],0),([],0)]>
unknown Diagram Decreasing
   [ f(f(?x,?y),?z) -> f(f(?x,?z),f(?y,?z)) ]
Sort Assignment:
 f : 5*5=>5
non-linear variables: {?z}
non-linear types: {5}
types leq non-linear types: {5}
rules applicable to terms of non-linear types:
   [ f(f(?x,?y),?z) -> f(f(?x,?z),f(?y,?z)) ]
NLR:
0: {0}
unknown innermost-termination for terms of non-linear types
unknown Quasi-Linear & Linearized-Decreasing
   [ f(f(?x,?y),?z) -> f(f(?x,?z),f(?y,?z)) ]
Sort Assignment:
 f : 5*5=>5
non-linear variables: {?z}
non-linear types: {5}
types leq non-linear types: {5}
rules applicable to terms of non-linear types:
   [ f(f(?x,?y),?z) -> f(f(?x,?z),f(?y,?z)) ]
unknown innermost-termination for terms of non-linear types
unknown Strongly Quasi-Linear & Hierarchically Decreasing
check Non-Confluence...
obtain 11 rules by 3 steps unfolding
strenghten f(f(f(?x,?y),?z_1),f(?z,?z_1)) and f(f(f(?x,?z),f(?y,?z)),?z_1)
strenghten f(f(?x_2,f(?y_2,?z_2)),f(?z_2,f(?y_2,?z_2))) and f(f(?x_2,?z_2),f(?y_2,?z_2))
strenghten f(f(?x_18,?z_17),f(f(?x_17,?z_17),f(?y_17,?z_17))) and f(f(?x_18,?z_17),f(f(?x_17,?y_17),?z_17))
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
unknown Huet (modulo AC)
check by Reduction-Preserving Completion...
126.trs: Failure(timeout)
(64603 msec.)