NO
(ignored inputs)COMMENT from experiments for [44] submitted by: Tsubasa Suzuki , Takahito Aoto , and Yoshihito Toyama
Rewrite Rules:
   [ a(?x) -> g(h(b(?x))),
     a(?x) -> g(c(?x)),
     b(?x) -> g(b(?x)),
     g(a(?x)) -> g(h(a(?x))) ]
Apply Direct Methods...
Inner CPs:
   [ g(g(h(b(?x)))) = g(h(a(?x))),
     g(g(c(?x_1))) = g(h(a(?x_1))) ]
Outer CPs:
   [ g(h(b(?x))) = g(c(?x)) ]
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:
   [ g(c(?x)) = g(h(b(?x))),
     g(h(a(?x))) = g(g(h(b(?x)))),
     g(h(b(?x))) = g(c(?x)),
     g(h(a(?x))) = g(g(c(?x))),
     g(g(h(b(?x)))) = g(h(a(?x))),
     g(g(c(?x))) = g(h(a(?x))) ]
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 <g(g(h(b(?x)))), g(h(a(?x)))> by Rules <0, 3> preceded by [(g,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)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (success)
 (failure)
check by Ordering(rpo), check by Tree-Automata Approximation (success)
Witness for Non-Confluence: <g(h(b(c_1))) <- a(c_1) -> g(c(c_1))>
Direct Methods: not CR

Combined result: not CR
239.trs: Success(not CR)
(32 msec.)