NO (ignored inputs)COMMENT due to Levy , from p.814 of \cite{Hue80} Rewrite Rules: [ F(A,A) -> G(B,B), A -> A', F(A',?x) -> F(?x,?x), F(?x,A') -> F(?x,?x), G(B,B) -> F(A,A), B -> B', G(B',?x) -> G(?x,?x), G(?x,B') -> G(?x,?x) ] Apply Direct Methods... Inner CPs: [ F(A',A) = G(B,B), F(A,A') = G(B,B), G(B',B) = F(A,A), G(B,B') = F(A,A) ] Outer CPs: [ F(A',A') = F(A',A'), G(B',B') = G(B',B') ] 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: [ F(A,A') = G(B,B) {}, F(A',A) = G(B,B) {}, F(A',A') = G(B,B) {}, G(B,B') = F(A,A) {}, G(B',B) = F(A,A) {}, G(B',B') = F(A,A) {} ] unknown Toyama (Parallel CPs) Simultaneous CPs: [ F(A',A') = G(B,B), F(A',A) = G(B,B), F(A,A') = G(B,B), G(B,B) = F(A',A), G(B,B) = F(A,A'), F(A',A') = F(A',A'), G(B',B') = F(A,A), G(B',B) = F(A,A), G(B,B') = F(A,A), F(A,A) = G(B',B), F(A,A) = G(B,B'), G(B',B') = G(B',B') ] 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 [(F,1)] joinable by a reduction of rules <[([],2)], [([],4)]> Critical Pair by Rules <1, 0> preceded by [(F,2)] joinable by a reduction of rules <[([],3)], [([],4)]> Critical Pair by Rules <5, 4> preceded by [(G,1)] joinable by a reduction of rules <[([],6)], [([],0)]> Critical Pair by Rules <5, 4> preceded by [(G,2)] joinable by a reduction of rules <[([],7)], [([],0)]> Critical Pair by Rules <3, 2> preceded by [] joinable by a reduction of rules <[], []> Critical Pair by Rules <7, 6> preceded by [] joinable by a reduction of rules <[], []> unknown Diagram Decreasing [ F(A,A) -> G(B,B), A -> A', F(A',?x) -> F(?x,?x), F(?x_1,A') -> F(?x_1,?x_1), G(B,B) -> F(A,A), B -> B', G(B',?x_2) -> G(?x_2,?x_2), G(?x_3,B') -> G(?x_3,?x_3) ] Sort Assignment: A : =>21 B : =>17 F : 21*21=>15 G : 17*17=>15 A' : =>21 B' : =>17 non-linear variables: {?x,?x_1,?x_2,?x_3} non-linear types: {21,17} types leq non-linear types: {21,17} rules applicable to terms of non-linear types: [ A -> A', B -> B' ] NLR: 0: {} 1: {} 2: {1} 3: {1} 4: {} 5: {} 6: {5} 7: {5} terms of non-linear types are innermost terminating Critical Pair by Rules <1, 0> joinable by a reduction of rules [->(2),->(0)] joinable by a reduction of rules [->(2),(4)<-] joinable by a reduction of rules [(1)<-,(4)<-] joinable by a reduction of rules [->(1),(1)<-,->(3),->(0)] Critical Pair by Rules <1, 0> joinable by a reduction of rules [->(3),->(0)] joinable by a reduction of rules [->(3),(4)<-] joinable by a reduction of rules [(1)<-,(4)<-] joinable by a reduction of rules [->(1),(1)<-,->(2),->(0)] Critical Pair by Rules <5, 4> joinable by a reduction of rules [->(6),->(4)] joinable by a reduction of rules [->(6),(0)<-] joinable by a reduction of rules [(5)<-,(0)<-] joinable by a reduction of rules [->(5),(5)<-,->(7),->(4)] Critical Pair by Rules <5, 4> joinable by a reduction of rules [->(7),->(4)] joinable by a reduction of rules [->(7),(0)<-] joinable by a reduction of rules [(5)<-,(0)<-] joinable by a reduction of rules [->(5),(5)<-,->(6),->(4)] Critical Pair by Rules <3, 2> joinable by a reduction of rules [] Critical Pair by Rules <7, 6> joinable by a reduction of rules [] Not Satisfiable unknown Quasi-Linear & Linearized-Decreasing [ F(A,A) -> G(B,B), A -> A', F(A',?x) -> F(?x,?x), F(?x_1,A') -> F(?x_1,?x_1), G(B,B) -> F(A,A), B -> B', G(B',?x_2) -> G(?x_2,?x_2), G(?x_3,B') -> G(?x_3,?x_3) ] Sort Assignment: A : =>21 B : =>17 F : 21*21=>15 G : 17*17=>15 A' : =>21 B' : =>17 non-linear variables: {?x,?x_1,?x_2,?x_3} non-linear types: {21,17} types leq non-linear types: {21,17} rules applicable to terms of non-linear types: [ A -> A', B -> B' ] terms of non-linear types are terminating Critical Pair by Rules <1, 0> joinable by a reduction of rules [->(2),->(0)] joinable by a reduction of rules [->(2),(4)<-] joinable by a reduction of rules [(1)<-,(4)<-] joinable by a reduction of rules [->(1),(1)<-,->(3),->(0)] Critical Pair by Rules <1, 0> joinable by a reduction of rules [->(3),->(0)] joinable by a reduction of rules [->(3),(4)<-] joinable by a reduction of rules [(1)<-,(4)<-] joinable by a reduction of rules [->(1),(1)<-,->(2),->(0)] Critical Pair by Rules <5, 4> joinable by a reduction of rules [->(6),->(4)] joinable by a reduction of rules [->(6),(0)<-] joinable by a reduction of rules [(5)<-,(0)<-] joinable by a reduction of rules [->(5),(5)<-,->(7),->(4)] Critical Pair by Rules <5, 4> joinable by a reduction of rules [->(7),->(4)] joinable by a reduction of rules [->(7),(0)<-] joinable by a reduction of rules [(5)<-,(0)<-] joinable by a reduction of rules [->(5),(5)<-,->(6),->(4)] Critical Pair by Rules <3, 2> joinable by a reduction of rules [] Critical Pair by Rules <7, 6> joinable by a reduction of rules [] Not Satisfiable unknown Strongly Quasi-Linear & Hierarchically Decreasing check Non-Confluence... obtain 18 rules by 3 steps unfolding strenghten F(?x_5,?x_5) and F(?x_5,A') strenghten F(?x_9,?x_9) and F(A',?x_9) strenghten F(A,A) and F(A,A') strenghten F(A,A) and F(A',A) strenghten F(A,A) and F(A',A') strenghten F(A,A) and G(B,B') strenghten F(A,A) and G(B',B) strenghten G(B,B) and F(A,A) strenghten G(B,B) and F(A,A') strenghten G(B,B) and F(A',A) obtain 58 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 49.trs: Success(not CR) (4613 msec.)