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

Final result: not CR
new/min-max2.trs: Success(not CR)
(45 msec.)