NO (ignored inputs)COMMENT experiments for [36] submitted by: Takahito Aoto Rewrite Rules: [ br(0,?y,?z) -> ?y, br(s(?x),?y,?z) -> ?z, p(0) -> 0, p(s(?x)) -> ?x, +(?x,?y) -> br(?x,?y,+(p(?x),s(?y))), +(?x,?y) -> br(?y,?x,+(s(?x),p(?y))) ] Apply Direct Methods... Inner CPs: [ ] Outer CPs: [ br(?x_3,?y_3,+(p(?x_3),s(?y_3))) = br(?y_3,?x_3,+(s(?x_3),p(?y_3))) ] Overlay, check Innermost Termination... unknown Innermost Terminating unknown Knuth & Bendix Left-Linear, not Right-Linear unknown Development 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: [ br(?y,?x,+(s(?x),p(?y))) = br(?x,?y,+(p(?x),s(?y))), br(?x,?y,+(p(?x),s(?y))) = br(?y,?x,+(s(?x),p(?y))) ] 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 <5, 4> preceded by [] unknown Diagram Decreasing [ br(0,?y,?z) -> ?y, br(s(?x_1),?y_1,?z_1) -> ?z_1, p(0) -> 0, p(s(?x_2)) -> ?x_2, +(?x_3,?y_3) -> br(?x_3,?y_3,+(p(?x_3),s(?y_3))), +(?x_4,?y_4) -> br(?y_4,?x_4,+(s(?x_4),p(?y_4))) ] Sort Assignment: + : 23*23=>23 0 : =>23 p : 23=>23 s : 23=>23 br : 23*23*23=>23 non-linear variables: {?x_3,?y_3,?y_4,?x_4} non-linear types: {23} types leq non-linear types: {23} rules applicable to terms of non-linear types: [ br(0,?y,?z) -> ?y, br(s(?x_1),?y_1,?z_1) -> ?z_1, p(0) -> 0, p(s(?x_2)) -> ?x_2, +(?x_3,?y_3) -> br(?x_3,?y_3,+(p(?x_3),s(?y_3))), +(?x_4,?y_4) -> br(?y_4,?x_4,+(s(?x_4),p(?y_4))) ] Rnl: 0: {} 1: {} 2: {} 3: {} 4: {0,1,2,3,4,5} 5: {0,1,2,3,4,5} unknown innermost-termination for terms of non-linear types unknown Quasi-Linear & Linearized-Decreasing [ br(0,?y,?z) -> ?y, br(s(?x_1),?y_1,?z_1) -> ?z_1, p(0) -> 0, p(s(?x_2)) -> ?x_2, +(?x_3,?y_3) -> br(?x_3,?y_3,+(p(?x_3),s(?y_3))), +(?x_4,?y_4) -> br(?y_4,?x_4,+(s(?x_4),p(?y_4))) ] Sort Assignment: + : 23*23=>23 0 : =>23 p : 23=>23 s : 23=>23 br : 23*23*23=>23 non-linear variables: {?x_3,?y_3,?y_4,?x_4} non-linear types: {23} types leq non-linear types: {23} rules applicable to terms of non-linear types: [ br(0,?y,?z) -> ?y, br(s(?x_1),?y_1,?z_1) -> ?z_1, p(0) -> 0, p(s(?x_2)) -> ?x_2, +(?x_3,?y_3) -> br(?x_3,?y_3,+(p(?x_3),s(?y_3))), +(?x_4,?y_4) -> br(?y_4,?x_4,+(s(?x_4),p(?y_4))) ] unknown innermost-termination for terms of non-linear types unknown Strongly Quasi-Linear & Hierarchically 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) (success) (success) (success) (success) (success) (success) (success) (success) (success) (success) (success) (failure) check by Ordering(rpo), check by Tree-Automata Approximation (success) where F = {(+,2),(0,0),(p,1),(s,1),(br,3),(c_1,0)} Q = {q_0,q_1,q_{+(0,s(p(c_1)))},q_{+(p(*),s(*))},q_{+(s(*),p(*))},q_{c_1},q_{*},q_{0},q_{p(*)},q_{s(*)},q_{p(c_1)},q_{s(p(c_1))}} Qf = {q_0,q_1} Delta = [ +(q_{*},q_{*}) -> q_{*}, +(q_{*},q_{*}) -> q_{p(*)}, +(q_{0},q_{s(p(c_1))}) -> q_{+(0,s(p(c_1)))}, +(q_{p(*)},q_{s(*)}) -> q_{+(0,s(p(c_1)))}, +(q_{p(*)},q_{s(*)}) -> q_{+(p(*),s(*))}, +(q_{p(*)},q_{s(*)}) -> q_{+(s(*),p(*))}, +(q_{p(*)},q_{s(*)}) -> q_{p(*)}, +(q_{s(*)},q_{p(*)}) -> q_{+(0,s(p(c_1)))}, +(q_{s(*)},q_{p(*)}) -> q_{+(p(*),s(*))}, +(q_{s(*)},q_{p(*)}) -> q_{+(s(*),p(*))}, +(q_{s(*)},q_{p(*)}) -> q_{p(*)}, 0 -> q_{*}, 0 -> q_{0}, 0 -> q_{p(*)}, p(q_{c_1}) -> q_{p(c_1)}, p(q_{*}) -> q_{*}, p(q_{*}) -> q_{p(*)}, s(q_{*}) -> q_{+(0,s(p(c_1)))}, s(q_{*}) -> q_{+(p(*),s(*))}, s(q_{*}) -> q_{+(s(*),p(*))}, s(q_{*}) -> q_{*}, s(q_{*}) -> q_{p(*)}, s(q_{*}) -> q_{s(*)}, s(q_{p(c_1)}) -> q_{+(0,s(p(c_1)))}, s(q_{p(c_1)}) -> q_{s(p(c_1))}, br(q_{c_1},q_{0},q_{+(0,s(p(c_1)))}) -> q_0, br(q_{*},q_{*},q_{+(p(*),s(*))}) -> q_{p(*)}, br(q_{*},q_{*},q_{+(s(*),p(*))}) -> q_{p(*)}, br(q_{*},q_{*},q_{*}) -> q_{*}, br(q_{*},q_{*},q_{*}) -> q_{p(*)}, br(q_{0},q_{s(p(c_1))},q_{+(p(*),s(*))}) -> q_{+(0,s(p(c_1)))}, br(q_{p(*)},q_{s(*)},q_{+(p(*),s(*))}) -> q_{+(0,s(p(c_1)))}, br(q_{p(*)},q_{s(*)},q_{+(p(*),s(*))}) -> q_{+(p(*),s(*))}, br(q_{p(*)},q_{s(*)},q_{+(p(*),s(*))}) -> q_{+(s(*),p(*))}, br(q_{p(*)},q_{s(*)},q_{+(p(*),s(*))}) -> q_{p(*)}, br(q_{p(*)},q_{s(*)},q_{+(s(*),p(*))}) -> q_{+(0,s(p(c_1)))}, br(q_{p(*)},q_{s(*)},q_{+(s(*),p(*))}) -> q_{+(p(*),s(*))}, br(q_{p(*)},q_{s(*)},q_{+(s(*),p(*))}) -> q_{+(s(*),p(*))}, br(q_{p(*)},q_{s(*)},q_{+(s(*),p(*))}) -> q_{p(*)}, br(q_{s(*)},q_{p(*)},q_{+(p(*),s(*))}) -> q_{+(0,s(p(c_1)))}, br(q_{s(*)},q_{p(*)},q_{+(p(*),s(*))}) -> q_{+(p(*),s(*))}, br(q_{s(*)},q_{p(*)},q_{+(p(*),s(*))}) -> q_{+(s(*),p(*))}, br(q_{s(*)},q_{p(*)},q_{+(p(*),s(*))}) -> q_{p(*)}, br(q_{s(*)},q_{p(*)},q_{+(s(*),p(*))}) -> q_{+(0,s(p(c_1)))}, br(q_{s(*)},q_{p(*)},q_{+(s(*),p(*))}) -> q_{+(p(*),s(*))}, br(q_{s(*)},q_{p(*)},q_{+(s(*),p(*))}) -> q_{+(s(*),p(*))}, br(q_{s(*)},q_{p(*)},q_{+(s(*),p(*))}) -> q_{p(*)}, br(q_{s(p(c_1))},q_{0},q_{+(s(*),p(*))}) -> q_{+(0,s(p(c_1)))}, c_1 -> q_1, c_1 -> q_{c_1}, c_1 -> q_{*}, c_1 -> q_{p(*)} ] (failure) check by Interpretation(mod2) (failure) check by Descendants-Approximation, check by Ordering(poly) (success) Witness for Non-Confluence: c_1> Direct Methods: not CR Combined result: not CR 584.trs: Success(not CR) (1031 msec.)