NO (ignored inputs)COMMENT from Example 4 of \cite{OO04} Rewrite Rules: [ h(f,a,a) -> h(g,a,a), h(g,a,a) -> h(f,a,a), a -> a', h(?x,a',?y) -> h(?x,?y,?y), h(?x,?y,a') -> h(?x,?y,?y) ] Apply Direct Methods... Inner CPs: [ h(f,a',a) = h(g,a,a), h(f,a,a') = h(g,a,a), h(g,a',a) = h(f,a,a), h(g,a,a') = h(f,a,a) ] Outer CPs: [ h(?x,a',a') = h(?x,a',a') ] 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: [ h(f,a,a') = h(g,a,a) {}, h(f,a',a) = h(g,a,a) {}, h(f,a',a') = h(g,a,a) {}, h(g,a,a') = h(f,a,a) {}, h(g,a',a) = h(f,a,a) {}, h(g,a',a') = h(f,a,a) {} ] unknown Toyama (Parallel CPs) Simultaneous CPs: [ h(f,a',a') = h(g,a,a), h(f,a',a) = h(g,a,a), h(f,a,a') = h(g,a,a), h(g,a',a') = h(f,a,a), h(g,a',a) = h(f,a,a), h(g,a,a') = h(f,a,a), h(g,a,a) = h(f,a',a), h(g,a,a) = h(f,a,a'), h(f,a,a) = h(g,a',a), h(f,a,a) = h(g,a,a'), h(?x,a',a') = h(?x,a',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 by Rules <2, 0> preceded by [(h,2)] joinable by a reduction of rules <[([],3)], [([],1)]> Critical Pair by Rules <2, 0> preceded by [(h,3)] joinable by a reduction of rules <[([],4)], [([],1)]> Critical Pair by Rules <2, 1> preceded by [(h,2)] joinable by a reduction of rules <[([],3)], [([],0)]> Critical Pair by Rules <2, 1> preceded by [(h,3)] joinable by a reduction of rules <[([],4)], [([],0)]> Critical Pair by Rules <4, 3> preceded by [] joinable by a reduction of rules <[], []> unknown Diagram Decreasing [ h(f,a,a) -> h(g,a,a), h(g,a,a) -> h(f,a,a), a -> a', h(?x,a',?y) -> h(?x,?y,?y), h(?x_1,?y_1,a') -> h(?x_1,?y_1,?y_1) ] Sort Assignment: a : =>15 f : =>8 g : =>8 h : 8*15*15=>13 a' : =>15 non-linear variables: {?y,?y_1} non-linear types: {15} types leq non-linear types: {15} rules applicable to terms of non-linear types: [ a -> a' ] NLR: 0: {} 1: {} 2: {} 3: {2} 4: {2} terms of non-linear types are innermost terminating Critical Pair by Rules <2, 0> joinable by a reduction of rules [->(3),->(0)] joinable by a reduction of rules [->(3),(1)<-] joinable by a reduction of rules [(2)<-,(1)<-] joinable by a reduction of rules [->(2),(2)<-,->(4),->(0)] Critical Pair by Rules <2, 0> joinable by a reduction of rules [->(4),->(0)] joinable by a reduction of rules [->(4),(1)<-] joinable by a reduction of rules [(2)<-,(1)<-] joinable by a reduction of rules [->(2),(2)<-,->(3),->(0)] Critical Pair by Rules <2, 1> joinable by a reduction of rules [->(3),->(1)] joinable by a reduction of rules [->(3),(0)<-] joinable by a reduction of rules [(2)<-,(0)<-] joinable by a reduction of rules [->(2),(2)<-,->(4),->(1)] Critical Pair by Rules <2, 1> joinable by a reduction of rules [->(4),->(1)] joinable by a reduction of rules [->(4),(0)<-] joinable by a reduction of rules [(2)<-,(0)<-] joinable by a reduction of rules [->(2),(2)<-,->(3),->(1)] Critical Pair by Rules <4, 3> joinable by a reduction of rules [] Not Satisfiable unknown Quasi-Linear & Linearized-Decreasing [ h(f,a,a) -> h(g,a,a), h(g,a,a) -> h(f,a,a), a -> a', h(?x,a',?y) -> h(?x,?y,?y), h(?x_1,?y_1,a') -> h(?x_1,?y_1,?y_1) ] Sort Assignment: a : =>15 f : =>8 g : =>8 h : 8*15*15=>13 a' : =>15 non-linear variables: {?y,?y_1} non-linear types: {15} types leq non-linear types: {15} rules applicable to terms of non-linear types: [ a -> a' ] terms of non-linear types are terminating Critical Pair by Rules <2, 0> joinable by a reduction of rules [->(3),->(0)] joinable by a reduction of rules [->(3),(1)<-] joinable by a reduction of rules [(2)<-,(1)<-] joinable by a reduction of rules [->(2),(2)<-,->(4),->(0)] Critical Pair by Rules <2, 0> joinable by a reduction of rules [->(4),->(0)] joinable by a reduction of rules [->(4),(1)<-] joinable by a reduction of rules [(2)<-,(1)<-] joinable by a reduction of rules [->(2),(2)<-,->(3),->(0)] Critical Pair by Rules <2, 1> joinable by a reduction of rules [->(3),->(1)] joinable by a reduction of rules [->(3),(0)<-] joinable by a reduction of rules [(2)<-,(0)<-] joinable by a reduction of rules [->(2),(2)<-,->(4),->(1)] Critical Pair by Rules <2, 1> joinable by a reduction of rules [->(4),->(1)] joinable by a reduction of rules [->(4),(0)<-] joinable by a reduction of rules [(2)<-,(0)<-] joinable by a reduction of rules [->(2),(2)<-,->(3),->(1)] Critical Pair by Rules <4, 3> joinable by a reduction of rules [] Not Satisfiable unknown Strongly Quasi-Linear & Hierarchically Decreasing check Non-Confluence... obtain 15 rules by 3 steps unfolding strenghten h(?x_3,a,a) and h(?x_3,a',a') strenghten h(?x_9,?y_9,?y_9) and h(?x_9,?y_9,a') strenghten h(?x_10,?y_10,?y_10) and h(?x_10,a',?y_10) strenghten h(f,a,a) and h(g,a,a) strenghten h(f,a,a) and h(g,a,a') strenghten h(f,a,a) and h(g,a',a) strenghten h(g,a,a) and h(f,a,a) strenghten h(g,a,a) and h(f,a,a') strenghten h(g,a,a) and h(f,a',a) obtain 61 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) (success) Witness for Non-Confluence: Direct Methods: not CR Final result: not CR 64.trs: Success(not CR) (5205 msec.)