NO (ignored inputs)COMMENT Example 3 of \cite{GL06} Rewrite Rules: [ b -> a, b -> c, c -> h(b), c -> d, a -> h(a), d -> h(d) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ a = c, h(b) = d ] Overlay, check Innermost Termination... unknown Innermost 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: [ c = a, a = c, d = h(b), h(b) = d ] 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 by Rules <1, 0> preceded by [] joinable by a reduction of rules <[([],2),([(h,1)],0)], [([],4)]> Critical Pair by Rules <3, 2> preceded by [] joinable by a reduction of rules <[([],5)], [([(h,1)],1),([(h,1)],3)]> unknown Diagram Decreasing check Non-Confluence... obtain 16 rules by 3 steps unfolding strenghten a and c strenghten a and d strenghten c and a strenghten c and d strenghten h(a) and a strenghten h(a) and c strenghten h(a) and d strenghten h(b) and a strenghten h(b) and c strenghten h(b) and d strenghten h(c) and a strenghten h(c) and c strenghten h(c) and d strenghten h(d) and a strenghten h(d) and c strenghten h(d) and d strenghten h(a) and h(b) strenghten h(a) and h(c) strenghten h(a) and h(d) strenghten h(b) and h(a) strenghten h(b) and h(c) strenghten h(b) and h(d) strenghten h(c) and h(d) 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 (success) Precedence: h : !1; a : Mul []; d : Mul []; Obtained: a :(gt): d a :(ge): a Witness for Non-Confluence: Direct Methods: not CR Final result: not CR 21.trs: Success(not CR) (50 msec.)