NO
(ignored inputs)COMMENT reduction failed
Rewrite Rules:
   [ c -> c,
     a -> f(h(h(f(a),f(f(c))),b)),
     c -> a,
     h(c,f(b)) -> c ]
Apply Direct Methods...
Inner CPs:
   [ h(c,f(b)) = c,
     h(a,f(b)) = c ]
Outer CPs:
   [ c = 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
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:
   [ a = c,
     c = h(c,f(b)),
     c = a,
     c = h(a,f(b)),
     h(c,f(b)) = c,
     h(a,f(b)) = c ]
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 <h(c,f(b)), c> by Rules <0, 3> preceded by [(h,1)]
 joinable by a reduction of rules <[([],3)], []>
Critical Pair <h(a,f(b)), c> by Rules <2, 3> preceded by [(h,1)]
unknown Diagram Decreasing
check Non-Confluence...
obtain 10 rules by 3 steps unfolding
obtain 100 candidates for checking non-joinability
check by TCAP-Approximation (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (failure)
check by Ordering(rpo), check by Tree-Automata Approximation (success)
<F,Q,Q_f,Delta> where
   F = {(a,0),(b,0),(c,0),(f,1),(h,2)}
   Q = {q_0,q_1,q_{a},q_{b},q_{c},q_{f(a)},q_{f(b)},q_{f(c)},q_{f(f(c))},q_{h(h(f(a),f(f(c))),b)},q_{h(f(a),f(f(c)))}}
   Qf = {q_0,q_1}
   Delta = 
   [ a -> q_1,
     a -> q_{a},
     a -> q_{c},
     b -> q_{b},
     c -> q_{c},
     f(q_{a}) -> q_{f(a)},
     f(q_{b}) -> q_{f(b)},
     f(q_{c}) -> q_{f(c)},
     f(q_{f(c)}) -> q_{f(f(c))},
     f(q_{h(h(f(a),f(f(c))),b)}) -> q_1,
     f(q_{h(h(f(a),f(f(c))),b)}) -> q_{a},
     f(q_{h(h(f(a),f(f(c))),b)}) -> q_{c},
     h(q_{a},q_{f(b)}) -> q_0,
     h(q_{f(a)},q_{f(f(c))}) -> q_{h(f(a),f(f(c)))},
     h(q_{h(f(a),f(f(c)))},q_{b}) -> q_{h(h(f(a),f(f(c))),b)} ]
 (failure)
check by Interpretation(mod2) (success)
Polynomial Interpretation:
  a:= (1)
  b:= 0
  c:= (1)
  f:= (1)
  h:= 0
 [a]-[f(h(h(f(a),f(f(c))),b))] = 0 = 0 (mod 2)
 [c]-[c] = 0 = 0 (mod 2)
 [c]-[a] = 0 = 0 (mod 2)
 [f(h(h(f(a),f(f(c))),b))]-[a] = 0 = 0 (mod 2)
 [c]-[c] = 0 = 0 (mod 2)
 [a]-[c] = 0 = 0 (mod 2)
 [h(f(h(h(f(a),f(f(a))),b)),f(b))]-[a] = (~1) = 1 (mod 2)
 (success)
Witness for Non-Confluence: <h(f(h(h(f(a),f(f(a))),b)),f(b)) <- h(c,f(b)) -> a>
Direct Methods: not CR

Combined result: not CR
/tmp/filet8vRJV.trs: Success(not CR)
(141 msec.)