(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 <br(?y_4,?x_4,+(s(?x_4),p(?y_4))), br(?x_4,?y_4,+(p(?x_4),s(?y_4)))> 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)
Witness for Non-Confluence: <br(c_1,0,+(0,s(p(c_1)))) <- +(0,c_1) -> c_1>
Direct Methods: not CR

Combined result: not CR
584.trs: Success(not CR)
NO
(89 msec.)