NO
Rewrite Rules:
   [ min(0,?y) -> 0,
     min(?x,0) -> 0,
     min(s(?x),s(?y)) -> s(min(?x,?y)),
     le(0,?y) -> true,
     le(s(?x),0) -> false,
     le(s(?x),s(?y)) -> le(?x,?y),
     if(true,?x,?y) -> ?x,
     if(false,?x,?y) -> ?y,
     min(?x,?y) -> min(?y,?x),
     min(?x,?y) -> if(le(?x,?y),?x,?y) ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [ 0 = 0,
     0 = min(?y,0),
     0 = if(le(0,?y),0,?y),
     0 = min(0,?x_1),
     0 = if(le(?x_1,0),?x_1,0),
     s(min(?x_2,?y_2)) = min(s(?y_2),s(?x_2)),
     s(min(?x_2,?y_2)) = if(le(s(?x_2),s(?y_2)),s(?x_2),s(?y_2)),
     min(?y_8,?x_8) = if(le(?x_8,?y_8),?x_8,?y_8) ]
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:
   [ 0 = 0,
     min(?y,0) = 0,
     if(le(0,?y),0,?y) = 0,
     min(0,?x) = 0,
     if(le(?x,0),?x,0) = 0,
     min(s(?y),s(?x)) = s(min(?x,?y)),
     if(le(s(?x),s(?y)),s(?x),s(?y)) = s(min(?x,?y)),
     0 = min(?y,0),
     0 = min(0,?x),
     s(min(?x_3,?y_3)) = min(s(?y_3),s(?x_3)),
     if(le(?x,?y),?x,?y) = min(?y,?x),
     0 = if(le(0,?y),0,?y),
     0 = if(le(?x,0),?x,0),
     s(min(?x_3,?y_3)) = if(le(s(?x_3),s(?y_3)),s(?x_3),s(?y_3)),
     min(?y,?x) = if(le(?x,?y),?x,?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 <0, 0> by Rules <1, 0> preceded by []
 joinable by a reduction of rules <[], []>
Critical Pair <min(?y_8,0), 0> by Rules <8, 0> preceded by []
 joinable by a reduction of rules <[([],1)], []>
Critical Pair <if(le(0,?y_9),0,?y_9), 0> by Rules <9, 0> preceded by []
 joinable by a reduction of rules <[([(if,1)],3),([],6)], []>
Critical Pair <min(0,?x_8), 0> by Rules <8, 1> preceded by []
 joinable by a reduction of rules <[([],0)], []>
Critical Pair <if(le(?x_9,0),?x_9,0), 0> by Rules <9, 1> preceded by []
unknown Diagram Decreasing
   [ min(0,?y) -> 0,
     min(?x_1,0) -> 0,
     min(s(?x_2),s(?y_2)) -> s(min(?x_2,?y_2)),
     le(0,?y_3) -> true,
     le(s(?x_4),0) -> false,
     le(s(?x_5),s(?y_5)) -> le(?x_5,?y_5),
     if(true,?x_6,?y_6) -> ?x_6,
     if(false,?x_7,?y_7) -> ?y_7,
     min(?x_8,?y_8) -> min(?y_8,?x_8),
     min(?x_9,?y_9) -> if(le(?x_9,?y_9),?x_9,?y_9) ]
Sort Assignment:
 0 : =>32
 s : 32=>32
 if : 20*32*32=>32
 le : 32*32=>20
 min : 32*32=>32
 true : =>20
 false : =>20
non-linear variables: {?x_9,?y_9}
non-linear types: {32}
types leq non-linear types: {32}
rules applicable to terms of non-linear types:
   [ min(0,?y) -> 0,
     min(?x_1,0) -> 0,
     min(s(?x_2),s(?y_2)) -> s(min(?x_2,?y_2)),
     le(0,?y_3) -> true,
     le(s(?x_4),0) -> false,
     le(s(?x_5),s(?y_5)) -> le(?x_5,?y_5),
     if(true,?x_6,?y_6) -> ?x_6,
     if(false,?x_7,?y_7) -> ?y_7,
     min(?x_8,?y_8) -> min(?y_8,?x_8),
     min(?x_9,?y_9) -> if(le(?x_9,?y_9),?x_9,?y_9) ]
Rnl:
0: {}
1: {}
2: {}
3: {}
4: {}
5: {}
6: {}
7: {}
8: {}
9: {0,1,2,3,4,5,6,7,8,9}
unknown innermost-termination for terms of non-linear types
unknown Quasi-Linear & Linearized-Decreasing
   [ min(0,?y) -> 0,
     min(?x_1,0) -> 0,
     min(s(?x_2),s(?y_2)) -> s(min(?x_2,?y_2)),
     le(0,?y_3) -> true,
     le(s(?x_4),0) -> false,
     le(s(?x_5),s(?y_5)) -> le(?x_5,?y_5),
     if(true,?x_6,?y_6) -> ?x_6,
     if(false,?x_7,?y_7) -> ?y_7,
     min(?x_8,?y_8) -> min(?y_8,?x_8),
     min(?x_9,?y_9) -> if(le(?x_9,?y_9),?x_9,?y_9) ]
Sort Assignment:
 0 : =>32
 s : 32=>32
 if : 20*32*32=>32
 le : 32*32=>20
 min : 32*32=>32
 true : =>20
 false : =>20
non-linear variables: {?x_9,?y_9}
non-linear types: {32}
types leq non-linear types: {32}
rules applicable to terms of non-linear types:
   [ min(0,?y) -> 0,
     min(?x_1,0) -> 0,
     min(s(?x_2),s(?y_2)) -> s(min(?x_2,?y_2)),
     le(0,?y_3) -> true,
     le(s(?x_4),0) -> false,
     le(s(?x_5),s(?y_5)) -> le(?x_5,?y_5),
     if(true,?x_6,?y_6) -> ?x_6,
     if(false,?x_7,?y_7) -> ?y_7,
     min(?x_8,?y_8) -> min(?y_8,?x_8),
     min(?x_9,?y_9) -> if(le(?x_9,?y_9),?x_9,?y_9) ]
unknown innermost-termination for terms of non-linear types
unknown Strongly Quasi-Linear & Hierarchically Decreasing
check Non-Confluence...
obtain 11 rules by 3 steps unfolding
obtain 45 candidates for checking non-joinability
check by TCAP-Approximation   [ min(0,?y:Nat) -> 0,
     min(?x:Nat,0) -> 0,
     min(s(?x:Nat),s(?y:Nat)) -> s(min(?x:Nat,?y:Nat)),
     le(0,?y:Nat) -> true,
     le(s(?x:Nat),0) -> false,
     le(s(?x:Nat),s(?y:Nat)) -> le(?x:Nat,?y:Nat),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     min(?x:Nat,?y:Nat) -> min(?y:Nat,?x:Nat),
     min(?x:Nat,?y:Nat) -> if(le(?x:Nat,?y:Nat),?x:Nat,?y:Nat) ]
   [ min(0,?y:Nat) -> 0,
     min(?x:Nat,0) -> 0,
     min(s(?x:Nat),s(?y:Nat)) -> s(min(?x:Nat,?y:Nat)),
     le(0,?y:Nat) -> true,
     le(s(?x:Nat),0) -> false,
     le(s(?x:Nat),s(?y:Nat)) -> le(?x:Nat,?y:Nat),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     min(?x:Nat,?y:Nat) -> min(?y:Nat,?x:Nat),
     min(?x:Nat,?y:Nat) -> if(le(?x:Nat,?y:Nat),?x:Nat,?y:Nat) ]
   [ min(0,?y:Nat) -> 0,
     min(?x:Nat,0) -> 0,
     min(s(?x:Nat),s(?y:Nat)) -> s(min(?x:Nat,?y:Nat)),
     le(0,?y:Nat) -> true,
     le(s(?x:Nat),0) -> false,
     le(s(?x:Nat),s(?y:Nat)) -> le(?x:Nat,?y:Nat),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     min(?x:Nat,?y:Nat) -> min(?y:Nat,?x:Nat),
     min(?x:Nat,?y:Nat) -> if(le(?x:Nat,?y:Nat),?x:Nat,?y:Nat) ]
   [ min(0,?y:Nat) -> 0,
     min(?x:Nat,0) -> 0,
     min(s(?x:Nat),s(?y:Nat)) -> s(min(?x:Nat,?y:Nat)),
     le(0,?y:Nat) -> true,
     le(s(?x:Nat),0) -> false,
     le(s(?x:Nat),s(?y:Nat)) -> le(?x:Nat,?y:Nat),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     min(?x:Nat,?y:Nat) -> min(?y:Nat,?x:Nat),
     min(?x:Nat,?y:Nat) -> if(le(?x:Nat,?y:Nat),?x:Nat,?y:Nat) ]
   [ min(0,?y:Nat) -> 0,
     min(?x:Nat,0) -> 0,
     min(s(?x:Nat),s(?y:Nat)) -> s(min(?x:Nat,?y:Nat)),
     le(0,?y:Nat) -> true,
     le(s(?x:Nat),0) -> false,
     le(s(?x:Nat),s(?y:Nat)) -> le(?x:Nat,?y:Nat),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     min(?x:Nat,?y:Nat) -> min(?y:Nat,?x:Nat),
     min(?x:Nat,?y:Nat) -> if(le(?x:Nat,?y:Nat),?x:Nat,?y:Nat) ]
   [ min(0,?y:Nat) -> 0,
     min(?x:Nat,0) -> 0,
     min(s(?x:Nat),s(?y:Nat)) -> s(min(?x:Nat,?y:Nat)),
     le(0,?y:Nat) -> true,
     le(s(?x:Nat),0) -> false,
     le(s(?x:Nat),s(?y:Nat)) -> le(?x:Nat,?y:Nat),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     min(?x:Nat,?y:Nat) -> min(?y:Nat,?x:Nat),
     min(?x:Nat,?y:Nat) -> if(le(?x:Nat,?y:Nat),?x:Nat,?y:Nat) ]
   [ min(0,?y:Nat) -> 0,
     min(?x:Nat,0) -> 0,
     min(s(?x:Nat),s(?y:Nat)) -> s(min(?x:Nat,?y:Nat)),
     le(0,?y:Nat) -> true,
     le(s(?x:Nat),0) -> false,
     le(s(?x:Nat),s(?y:Nat)) -> le(?x:Nat,?y:Nat),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     min(?x:Nat,?y:Nat) -> min(?y:Nat,?x:Nat),
     min(?x:Nat,?y:Nat) -> if(le(?x:Nat,?y:Nat),?x:Nat,?y:Nat) ]
   [ min(0,?y:Nat) -> 0,
     min(?x:Nat,0) -> 0,
     min(s(?x:Nat),s(?y:Nat)) -> s(min(?x:Nat,?y:Nat)),
     le(0,?y:Nat) -> true,
     le(s(?x:Nat),0) -> false,
     le(s(?x:Nat),s(?y:Nat)) -> le(?x:Nat,?y:Nat),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     min(?x:Nat,?y:Nat) -> min(?y:Nat,?x:Nat),
     min(?x:Nat,?y:Nat) -> if(le(?x:Nat,?y:Nat),?x:Nat,?y:Nat) ]
   [ min(0,?y:Nat) -> 0,
     min(?x:Nat,0) -> 0,
     min(s(?x:Nat),s(?y:Nat)) -> s(min(?x:Nat,?y:Nat)),
     le(0,?y:Nat) -> true,
     le(s(?x:Nat),0) -> false,
     le(s(?x:Nat),s(?y:Nat)) -> le(?x:Nat,?y:Nat),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     min(?x:Nat,?y:Nat) -> min(?y:Nat,?x:Nat),
     min(?x:Nat,?y:Nat) -> if(le(?x:Nat,?y:Nat),?x:Nat,?y:Nat) ]
   [ min(0,?y:Nat) -> 0,
     min(?x:Nat,0) -> 0,
     min(s(?x:Nat),s(?y:Nat)) -> s(min(?x:Nat,?y:Nat)),
     le(0,?y:Nat) -> true,
     le(s(?x:Nat),0) -> false,
     le(s(?x:Nat),s(?y:Nat)) -> le(?x:Nat,?y:Nat),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     min(?x:Nat,?y:Nat) -> min(?y:Nat,?x:Nat),
     min(?x:Nat,?y:Nat) -> if(le(?x:Nat,?y:Nat),?x:Nat,?y:Nat) ]
   [ min(0,?y:Nat) -> 0,
     min(?x:Nat,0) -> 0,
     min(s(?x:Nat),s(?y:Nat)) -> s(min(?x:Nat,?y:Nat)),
     le(0,?y:Nat) -> true,
     le(s(?x:Nat),0) -> false,
     le(s(?x:Nat),s(?y:Nat)) -> le(?x:Nat,?y:Nat),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     min(?x:Nat,?y:Nat) -> min(?y:Nat,?x:Nat),
     min(?x:Nat,?y:Nat) -> if(le(?x:Nat,?y:Nat),?x:Nat,?y:Nat) ]
   [ min(0,?y:Nat) -> 0,
     min(?x:Nat,0) -> 0,
     min(s(?x:Nat),s(?y:Nat)) -> s(min(?x:Nat,?y:Nat)),
     le(0,?y:Nat) -> true,
     le(s(?x:Nat),0) -> false,
     le(s(?x:Nat),s(?y:Nat)) -> le(?x:Nat,?y:Nat),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     min(?x:Nat,?y:Nat) -> min(?y:Nat,?x:Nat),
     min(?x:Nat,?y:Nat) -> if(le(?x:Nat,?y:Nat),?x:Nat,?y:Nat) ]
   [ min(0,?y:Nat) -> 0,
     min(?x:Nat,0) -> 0,
     min(s(?x:Nat),s(?y:Nat)) -> s(min(?x:Nat,?y:Nat)),
     le(0,?y:Nat) -> true,
     le(s(?x:Nat),0) -> false,
     le(s(?x:Nat),s(?y:Nat)) -> le(?x:Nat,?y:Nat),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     min(?x:Nat,?y:Nat) -> min(?y:Nat,?x:Nat),
     min(?x:Nat,?y:Nat) -> if(le(?x:Nat,?y:Nat),?x:Nat,?y:Nat) ]
   [ min(0,?y:Nat) -> 0,
     min(?x:Nat,0) -> 0,
     min(s(?x:Nat),s(?y:Nat)) -> s(min(?x:Nat,?y:Nat)),
     le(0,?y:Nat) -> true,
     le(s(?x:Nat),0) -> false,
     le(s(?x:Nat),s(?y:Nat)) -> le(?x:Nat,?y:Nat),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     min(?x:Nat,?y:Nat) -> min(?y:Nat,?x:Nat),
     min(?x:Nat,?y:Nat) -> if(le(?x:Nat,?y:Nat),?x:Nat,?y:Nat) ]
 (success)
Witness for Non-Confluence: <if(le(c_1,0),c_1,0) <- min(c_1,0) -> 0>
Direct Methods: not CR

Final result: not CR
new/min3.trs: Success(not CR)
(25 msec.)