NO
Rewrite Rules:
   [ ordered(nil) -> true,
     ordered(cons(?x,?ys)) -> and(leList(?x,?ys),ordered(?ys)),
     leList(?x,nil) -> true,
     leList(?x,cons(?y,?ys)) -> and(le(?x,?y),leList(?x,?ys)),
     zero(0) -> true,
     zero(s(?x)) -> false,
     prec(0) -> 0,
     prec(s(?x)) -> ?x,
     le(?x,?y) -> ifBool(zero(?x),true,le(prec(?x),prec(?y))),
     and(true,true) -> true,
     and(?x,true) -> ?x,
     and(true,?y) -> ?y,
     and(false,false) -> false,
     sort(nil) -> nil,
     sort(cons(?x,?ys)) -> insert(?x,sort(?ys)),
     insert(?x,nil) -> cons(?x,nil),
     insert(?x,cons(?y,?ys)) -> ifList(le(?x,?y),cons(?x,cons(?y,?ys)),cons(?y,insert(?x,?ys))),
     ifBool(true,?y,?z) -> ?y,
     ifBool(false,?y,?z) -> ?z,
     ifList(true,?y,?z) -> ?y,
     ifList(false,?y,?z) -> ?z,
     ordered(sort(?xs)) -> true ]
Apply Direct Methods...
Inner CPs:
   [ ordered(nil) = true,
     ordered(insert(?x_8,sort(?ys_8))) = true ]
Outer CPs:
   [ true = true,
     true = true,
     true = true ]
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: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
   [ true = true,
     true = ordered(nil),
     true = ordered(insert(?x,sort(?ys))),
     ordered(nil) = true,
     ordered(insert(?x_10,sort(?ys_10))) = true ]
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 <ordered(nil), true> by Rules <13, 21> preceded by [(ordered,1)]
 joinable by a reduction of rules <[([],0)], []>
Critical Pair <ordered(insert(?x_8,sort(?ys_8))), true> by Rules <14, 21> preceded by [(ordered,1)]
unknown Diagram Decreasing
   [ ordered(nil) -> true,
     ordered(cons(?x,?ys)) -> and(leList(?x,?ys),ordered(?ys)),
     leList(?x_1,nil) -> true,
     leList(?x_2,cons(?y_2,?ys_2)) -> and(le(?x_2,?y_2),leList(?x_2,?ys_2)),
     zero(0) -> true,
     zero(s(?x_3)) -> false,
     prec(0) -> 0,
     prec(s(?x_4)) -> ?x_4,
     le(?x_5,?y_5) -> ifBool(zero(?x_5),true,le(prec(?x_5),prec(?y_5))),
     and(true,true) -> true,
     and(?x_6,true) -> ?x_6,
     and(true,?y_7) -> ?y_7,
     and(false,false) -> false,
     sort(nil) -> nil,
     sort(cons(?x_8,?ys_8)) -> insert(?x_8,sort(?ys_8)),
     insert(?x_9,nil) -> cons(?x_9,nil),
     insert(?x_10,cons(?y_10,?ys_10)) -> ifList(le(?x_10,?y_10),cons(?x_10,cons(?y_10,?ys_10)),cons(?y_10,insert(?x_10,?ys_10))),
     ifBool(true,?y_11,?z_11) -> ?y_11,
     ifBool(false,?y_12,?z_12) -> ?z_12,
     ifList(true,?y_13,?z_13) -> ?y_13,
     ifList(false,?y_14,?z_14) -> ?z_14,
     ordered(sort(?xs_15)) -> true ]
Sort Assignment:
 0 : =>59
 s : 59=>59
 le : 59*59=>65
 and : 65*65=>65
 nil : =>66
 cons : 59*66=>66
 prec : 59=>59
 sort : 66=>66
 true : =>65
 zero : 59=>65
 ordered : 66=>65
 false : =>65
 ifBool : 65*65*65=>65
 ifList : 65*66*66=>66
 insert : 59*66=>66
 leList : 59*66=>65
non-linear variables: {?ys,?x_2,?x_5,?x_10,?y_10,?ys_10}
non-linear types: {66,59}
types leq non-linear types: {66,59}
rules applicable to terms of non-linear types:
   [ ordered(nil) -> true,
     ordered(cons(?x,?ys)) -> and(leList(?x,?ys),ordered(?ys)),
     leList(?x_1,nil) -> true,
     leList(?x_2,cons(?y_2,?ys_2)) -> and(le(?x_2,?y_2),leList(?x_2,?ys_2)),
     zero(0) -> true,
     zero(s(?x_3)) -> false,
     prec(0) -> 0,
     prec(s(?x_4)) -> ?x_4,
     le(?x_5,?y_5) -> ifBool(zero(?x_5),true,le(prec(?x_5),prec(?y_5))),
     and(true,true) -> true,
     and(?x_6,true) -> ?x_6,
     and(true,?y_7) -> ?y_7,
     and(false,false) -> false,
     sort(nil) -> nil,
     sort(cons(?x_8,?ys_8)) -> insert(?x_8,sort(?ys_8)),
     insert(?x_9,nil) -> cons(?x_9,nil),
     insert(?x_10,cons(?y_10,?ys_10)) -> ifList(le(?x_10,?y_10),cons(?x_10,cons(?y_10,?ys_10)),cons(?y_10,insert(?x_10,?ys_10))),
     ifBool(true,?y_11,?z_11) -> ?y_11,
     ifBool(false,?y_12,?z_12) -> ?z_12,
     ifList(true,?y_13,?z_13) -> ?y_13,
     ifList(false,?y_14,?z_14) -> ?z_14,
     ordered(sort(?xs_15)) -> true ]
Rnl:
0: {}
1: {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21}
2: {}
3: {6,7}
4: {}
5: {}
6: {}
7: {}
8: {6,7}
9: {}
10: {}
11: {}
12: {}
13: {}
14: {}
15: {}
16: {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21}
17: {}
18: {}
19: {}
20: {}
21: {}
unknown innermost-termination for terms of non-linear types
unknown Quasi-Linear & Linearized-Decreasing
   [ ordered(nil) -> true,
     ordered(cons(?x,?ys)) -> and(leList(?x,?ys),ordered(?ys)),
     leList(?x_1,nil) -> true,
     leList(?x_2,cons(?y_2,?ys_2)) -> and(le(?x_2,?y_2),leList(?x_2,?ys_2)),
     zero(0) -> true,
     zero(s(?x_3)) -> false,
     prec(0) -> 0,
     prec(s(?x_4)) -> ?x_4,
     le(?x_5,?y_5) -> ifBool(zero(?x_5),true,le(prec(?x_5),prec(?y_5))),
     and(true,true) -> true,
     and(?x_6,true) -> ?x_6,
     and(true,?y_7) -> ?y_7,
     and(false,false) -> false,
     sort(nil) -> nil,
     sort(cons(?x_8,?ys_8)) -> insert(?x_8,sort(?ys_8)),
     insert(?x_9,nil) -> cons(?x_9,nil),
     insert(?x_10,cons(?y_10,?ys_10)) -> ifList(le(?x_10,?y_10),cons(?x_10,cons(?y_10,?ys_10)),cons(?y_10,insert(?x_10,?ys_10))),
     ifBool(true,?y_11,?z_11) -> ?y_11,
     ifBool(false,?y_12,?z_12) -> ?z_12,
     ifList(true,?y_13,?z_13) -> ?y_13,
     ifList(false,?y_14,?z_14) -> ?z_14,
     ordered(sort(?xs_15)) -> true ]
Sort Assignment:
 0 : =>59
 s : 59=>59
 le : 59*59=>65
 and : 65*65=>65
 nil : =>66
 cons : 59*66=>66
 prec : 59=>59
 sort : 66=>66
 true : =>65
 zero : 59=>65
 ordered : 66=>65
 false : =>65
 ifBool : 65*65*65=>65
 ifList : 65*66*66=>66
 insert : 59*66=>66
 leList : 59*66=>65
non-linear variables: {?ys,?x_2,?x_5,?x_10,?y_10,?ys_10}
non-linear types: {66,59}
types leq non-linear types: {66,59}
rules applicable to terms of non-linear types:
   [ ordered(nil) -> true,
     ordered(cons(?x,?ys)) -> and(leList(?x,?ys),ordered(?ys)),
     leList(?x_1,nil) -> true,
     leList(?x_2,cons(?y_2,?ys_2)) -> and(le(?x_2,?y_2),leList(?x_2,?ys_2)),
     zero(0) -> true,
     zero(s(?x_3)) -> false,
     prec(0) -> 0,
     prec(s(?x_4)) -> ?x_4,
     le(?x_5,?y_5) -> ifBool(zero(?x_5),true,le(prec(?x_5),prec(?y_5))),
     and(true,true) -> true,
     and(?x_6,true) -> ?x_6,
     and(true,?y_7) -> ?y_7,
     and(false,false) -> false,
     sort(nil) -> nil,
     sort(cons(?x_8,?ys_8)) -> insert(?x_8,sort(?ys_8)),
     insert(?x_9,nil) -> cons(?x_9,nil),
     insert(?x_10,cons(?y_10,?ys_10)) -> ifList(le(?x_10,?y_10),cons(?x_10,cons(?y_10,?ys_10)),cons(?y_10,insert(?x_10,?ys_10))),
     ifBool(true,?y_11,?z_11) -> ?y_11,
     ifBool(false,?y_12,?z_12) -> ?z_12,
     ifList(true,?y_13,?z_13) -> ?y_13,
     ifList(false,?y_14,?z_14) -> ?z_14,
     ordered(sort(?xs_15)) -> true ]
unknown innermost-termination for terms of non-linear types
unknown Strongly Quasi-Linear & Hierarchically Decreasing
check Non-Confluence...
obtain 23 rules by 3 steps unfolding
obtain 3 candidates for checking non-joinability
check by TCAP-Approximation   [ ordered(nil) -> true,
     ordered(cons(?x:Nat,?ys:List)) -> and(leList(?x:Nat,?ys:List),ordered(?ys:List)),
     leList(?x:Nat,nil) -> true,
     leList(?x:Nat,cons(?y:Nat,?ys:List)) -> and(le(?x:Nat,?y:Nat),leList(?x:Nat,?ys:List)),
     zero(0) -> true,
     zero(s(?x:Nat)) -> false,
     prec(0) -> 0,
     prec(s(?x:Nat)) -> ?x:Nat,
     le(?x:Nat,?y:Nat) -> ifBool(zero(?x:Nat),true,le(prec(?x:Nat),prec(?y:Nat))),
     and(true,true) -> true,
     and(?x:Bool,true) -> ?x:Bool,
     and(true,?y:Bool) -> ?y:Bool,
     and(false,false) -> false,
     sort(nil) -> nil,
     sort(cons(?x:Nat,?ys:List)) -> insert(?x:Nat,sort(?ys:List)),
     insert(?x:Nat,nil) -> cons(?x:Nat,nil),
     insert(?x:Nat,cons(?y:Nat,?ys:List)) -> ifList(le(?x:Nat,?y:Nat),cons(?x:Nat,cons(?y:Nat,?ys:List)),cons(?y:Nat,insert(?x:Nat,?ys:List))),
     ifBool(true,?y:Bool,?z:Bool) -> ?y:Bool,
     ifBool(false,?y:Bool,?z:Bool) -> ?z:Bool,
     ifList(true,?y:List,?z:List) -> ?y:List,
     ifList(false,?y:List,?z:List) -> ?z:List,
     ordered(sort(?xs:List)) -> true ]
   [ ordered(nil) -> true,
     ordered(cons(?x:Nat,?ys:List)) -> and(leList(?x:Nat,?ys:List),ordered(?ys:List)),
     leList(?x:Nat,nil) -> true,
     leList(?x:Nat,cons(?y:Nat,?ys:List)) -> and(le(?x:Nat,?y:Nat),leList(?x:Nat,?ys:List)),
     zero(0) -> true,
     zero(s(?x:Nat)) -> false,
     prec(0) -> 0,
     prec(s(?x:Nat)) -> ?x:Nat,
     le(?x:Nat,?y:Nat) -> ifBool(zero(?x:Nat),true,le(prec(?x:Nat),prec(?y:Nat))),
     and(true,true) -> true,
     and(?x:Bool,true) -> ?x:Bool,
     and(true,?y:Bool) -> ?y:Bool,
     and(false,false) -> false,
     sort(nil) -> nil,
     sort(cons(?x:Nat,?ys:List)) -> insert(?x:Nat,sort(?ys:List)),
     insert(?x:Nat,nil) -> cons(?x:Nat,nil),
     insert(?x:Nat,cons(?y:Nat,?ys:List)) -> ifList(le(?x:Nat,?y:Nat),cons(?x:Nat,cons(?y:Nat,?ys:List)),cons(?y:Nat,insert(?x:Nat,?ys:List))),
     ifBool(true,?y:Bool,?z:Bool) -> ?y:Bool,
     ifBool(false,?y:Bool,?z:Bool) -> ?z:Bool,
     ifList(true,?y:List,?z:List) -> ?y:List,
     ifList(false,?y:List,?z:List) -> ?z:List,
     ordered(sort(?xs:List)) -> true ]
   [ ordered(nil) -> true,
     ordered(cons(?x:Nat,?ys:List)) -> and(leList(?x:Nat,?ys:List),ordered(?ys:List)),
     leList(?x:Nat,nil) -> true,
     leList(?x:Nat,cons(?y:Nat,?ys:List)) -> and(le(?x:Nat,?y:Nat),leList(?x:Nat,?ys:List)),
     zero(0) -> true,
     zero(s(?x:Nat)) -> false,
     prec(0) -> 0,
     prec(s(?x:Nat)) -> ?x:Nat,
     le(?x:Nat,?y:Nat) -> ifBool(zero(?x:Nat),true,le(prec(?x:Nat),prec(?y:Nat))),
     and(true,true) -> true,
     and(?x:Bool,true) -> ?x:Bool,
     and(true,?y:Bool) -> ?y:Bool,
     and(false,false) -> false,
     sort(nil) -> nil,
     sort(cons(?x:Nat,?ys:List)) -> insert(?x:Nat,sort(?ys:List)),
     insert(?x:Nat,nil) -> cons(?x:Nat,nil),
     insert(?x:Nat,cons(?y:Nat,?ys:List)) -> ifList(le(?x:Nat,?y:Nat),cons(?x:Nat,cons(?y:Nat,?ys:List)),cons(?y:Nat,insert(?x:Nat,?ys:List))),
     ifBool(true,?y:Bool,?z:Bool) -> ?y:Bool,
     ifBool(false,?y:Bool,?z:Bool) -> ?z:Bool,
     ifList(true,?y:List,?z:List) -> ?y:List,
     ifList(false,?y:List,?z:List) -> ?z:List,
     ordered(sort(?xs:List)) -> true ]
   [ ordered(nil) -> true,
     ordered(cons(?x:Nat,?ys:List)) -> and(leList(?x:Nat,?ys:List),ordered(?ys:List)),
     leList(?x:Nat,nil) -> true,
     leList(?x:Nat,cons(?y:Nat,?ys:List)) -> and(le(?x:Nat,?y:Nat),leList(?x:Nat,?ys:List)),
     zero(0) -> true,
     zero(s(?x:Nat)) -> false,
     prec(0) -> 0,
     prec(s(?x:Nat)) -> ?x:Nat,
     le(?x:Nat,?y:Nat) -> ifBool(zero(?x:Nat),true,le(prec(?x:Nat),prec(?y:Nat))),
     and(true,true) -> true,
     and(?x:Bool,true) -> ?x:Bool,
     and(true,?y:Bool) -> ?y:Bool,
     and(false,false) -> false,
     sort(nil) -> nil,
     sort(cons(?x:Nat,?ys:List)) -> insert(?x:Nat,sort(?ys:List)),
     insert(?x:Nat,nil) -> cons(?x:Nat,nil),
     insert(?x:Nat,cons(?y:Nat,?ys:List)) -> ifList(le(?x:Nat,?y:Nat),cons(?x:Nat,cons(?y:Nat,?ys:List)),cons(?y:Nat,insert(?x:Nat,?ys:List))),
     ifBool(true,?y:Bool,?z:Bool) -> ?y:Bool,
     ifBool(false,?y:Bool,?z:Bool) -> ?z:Bool,
     ifList(true,?y:List,?z:List) -> ?y:List,
     ifList(false,?y:List,?z:List) -> ?z:List,
     ordered(sort(?xs:List)) -> true ]
   [ ordered(nil) -> true,
     ordered(cons(?x:Nat,?ys:List)) -> and(leList(?x:Nat,?ys:List),ordered(?ys:List)),
     leList(?x:Nat,nil) -> true,
     leList(?x:Nat,cons(?y:Nat,?ys:List)) -> and(le(?x:Nat,?y:Nat),leList(?x:Nat,?ys:List)),
     zero(0) -> true,
     zero(s(?x:Nat)) -> false,
     prec(0) -> 0,
     prec(s(?x:Nat)) -> ?x:Nat,
     le(?x:Nat,?y:Nat) -> ifBool(zero(?x:Nat),true,le(prec(?x:Nat),prec(?y:Nat))),
     and(true,true) -> true,
     and(?x:Bool,true) -> ?x:Bool,
     and(true,?y:Bool) -> ?y:Bool,
     and(false,false) -> false,
     sort(nil) -> nil,
     sort(cons(?x:Nat,?ys:List)) -> insert(?x:Nat,sort(?ys:List)),
     insert(?x:Nat,nil) -> cons(?x:Nat,nil),
     insert(?x:Nat,cons(?y:Nat,?ys:List)) -> ifList(le(?x:Nat,?y:Nat),cons(?x:Nat,cons(?y:Nat,?ys:List)),cons(?y:Nat,insert(?x:Nat,?ys:List))),
     ifBool(true,?y:Bool,?z:Bool) -> ?y:Bool,
     ifBool(false,?y:Bool,?z:Bool) -> ?z:Bool,
     ifList(true,?y:List,?z:List) -> ?y:List,
     ifList(false,?y:List,?z:List) -> ?z:List,
     ordered(sort(?xs:List)) -> true ]
   [ ordered(nil) -> true,
     ordered(cons(?x:Nat,?ys:List)) -> and(leList(?x:Nat,?ys:List),ordered(?ys:List)),
     leList(?x:Nat,nil) -> true,
     leList(?x:Nat,cons(?y:Nat,?ys:List)) -> and(le(?x:Nat,?y:Nat),leList(?x:Nat,?ys:List)),
     zero(0) -> true,
     zero(s(?x:Nat)) -> false,
     prec(0) -> 0,
     prec(s(?x:Nat)) -> ?x:Nat,
     le(?x:Nat,?y:Nat) -> ifBool(zero(?x:Nat),true,le(prec(?x:Nat),prec(?y:Nat))),
     and(true,true) -> true,
     and(?x:Bool,true) -> ?x:Bool,
     and(true,?y:Bool) -> ?y:Bool,
     and(false,false) -> false,
     sort(nil) -> nil,
     sort(cons(?x:Nat,?ys:List)) -> insert(?x:Nat,sort(?ys:List)),
     insert(?x:Nat,nil) -> cons(?x:Nat,nil),
     insert(?x:Nat,cons(?y:Nat,?ys:List)) -> ifList(le(?x:Nat,?y:Nat),cons(?x:Nat,cons(?y:Nat,?ys:List)),cons(?y:Nat,insert(?x:Nat,?ys:List))),
     ifBool(true,?y:Bool,?z:Bool) -> ?y:Bool,
     ifBool(false,?y:Bool,?z:Bool) -> ?z:Bool,
     ifList(true,?y:List,?z:List) -> ?y:List,
     ifList(false,?y:List,?z:List) -> ?z:List,
     ordered(sort(?xs:List)) -> true ]
 (success)
Witness for Non-Confluence: <ordered(insert(c_1,sort(c_2))) <- ordered(sort(cons(c_1,c_2))) -> true>
Direct Methods: not CR

Final result: not CR
new/insert3.trs: Success(not CR)
(35 msec.)