YES

Problem:
 insert_cond_1(True(),x7,x5,x3) -> Cons(x7,Cons(x5,x3))
 insert_cond_1(False(),x7,x5,x3) -> Cons(x5,rec[insert_0][3](x7,x3))
 rec[insert_0][3](x6,Nil()) -> Cons(x6,Nil())
 rec[insert_0][3](x14,Cons(x10,x6)) -> insert_cond_1(rec[leq_0][2](x14,x10),x14,x10,x6)
 rec[sort_0][2](Nil()) -> Nil()
 rec[sort_0][2](Cons(x10,x6)) -> rec[insert_0][3](x10,rec[sort_0][2](x6))
 rec[leq_0][2](0(),x18) -> True()
 rec[leq_0][2](S(x26),0()) -> False()
 rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6)
 main(x3) -> rec[sort_0][2](x3)

Proof:
 DP Processor:
  DPs:
   insert_cond_1#(False(),x7,x5,x3) -> rec[insert_0][3]#(x7,x3)
   rec[insert_0][3]#(x14,Cons(x10,x6)) -> rec[leq_0][2]#(x14,x10)
   rec[insert_0][3]#(x14,Cons(x10,x6)) -> insert_cond_1#(rec[leq_0][2](x14,x10),x14,x10,x6)
   rec[sort_0][2]#(Cons(x10,x6)) -> rec[sort_0][2]#(x6)
   rec[sort_0][2]#(Cons(x10,x6)) -> rec[insert_0][3]#(x10,rec[sort_0][2](x6))
   rec[leq_0][2]#(S(x10),S(x6)) -> rec[leq_0][2]#(x10,x6)
   main#(x3) -> rec[sort_0][2]#(x3)
  TRS:
   insert_cond_1(True(),x7,x5,x3) -> Cons(x7,Cons(x5,x3))
   insert_cond_1(False(),x7,x5,x3) -> Cons(x5,rec[insert_0][3](x7,x3))
   rec[insert_0][3](x6,Nil()) -> Cons(x6,Nil())
   rec[insert_0][3](x14,Cons(x10,x6)) -> insert_cond_1(rec[leq_0][2](x14,x10),x14,x10,x6)
   rec[sort_0][2](Nil()) -> Nil()
   rec[sort_0][2](Cons(x10,x6)) -> rec[insert_0][3](x10,rec[sort_0][2](x6))
   rec[leq_0][2](0(),x18) -> True()
   rec[leq_0][2](S(x26),0()) -> False()
   rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6)
   main(x3) -> rec[sort_0][2](x3)
  TDG Processor:
   DPs:
    insert_cond_1#(False(),x7,x5,x3) -> rec[insert_0][3]#(x7,x3)
    rec[insert_0][3]#(x14,Cons(x10,x6)) -> rec[leq_0][2]#(x14,x10)
    rec[insert_0][3]#(x14,Cons(x10,x6)) -> insert_cond_1#(rec[leq_0][2](x14,x10),x14,x10,x6)
    rec[sort_0][2]#(Cons(x10,x6)) -> rec[sort_0][2]#(x6)
    rec[sort_0][2]#(Cons(x10,x6)) -> rec[insert_0][3]#(x10,rec[sort_0][2](x6))
    rec[leq_0][2]#(S(x10),S(x6)) -> rec[leq_0][2]#(x10,x6)
    main#(x3) -> rec[sort_0][2]#(x3)
   TRS:
    insert_cond_1(True(),x7,x5,x3) -> Cons(x7,Cons(x5,x3))
    insert_cond_1(False(),x7,x5,x3) -> Cons(x5,rec[insert_0][3](x7,x3))
    rec[insert_0][3](x6,Nil()) -> Cons(x6,Nil())
    rec[insert_0][3](x14,Cons(x10,x6)) -> insert_cond_1(rec[leq_0][2](x14,x10),x14,x10,x6)
    rec[sort_0][2](Nil()) -> Nil()
    rec[sort_0][2](Cons(x10,x6)) -> rec[insert_0][3](x10,rec[sort_0][2](x6))
    rec[leq_0][2](0(),x18) -> True()
    rec[leq_0][2](S(x26),0()) -> False()
    rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6)
    main(x3) -> rec[sort_0][2](x3)
   graph:
    main#(x3) -> rec[sort_0][2]#(x3) ->
    rec[sort_0][2]#(Cons(x10,x6)) -> rec[insert_0][3]#(x10,rec[sort_0][2](x6))
    main#(x3) -> rec[sort_0][2]#(x3) ->
    rec[sort_0][2]#(Cons(x10,x6)) -> rec[sort_0][2]#(x6)
    rec[sort_0][2]#(Cons(x10,x6)) -> rec[sort_0][2]#(x6) ->
    rec[sort_0][2]#(Cons(x10,x6)) -> rec[insert_0][3]#(x10,rec[sort_0][2](x6))
    rec[sort_0][2]#(Cons(x10,x6)) -> rec[sort_0][2]#(x6) ->
    rec[sort_0][2]#(Cons(x10,x6)) -> rec[sort_0][2]#(x6)
    rec[sort_0][2]#(Cons(x10,x6)) -> rec[insert_0][3]#(x10,rec[sort_0][2](x6)) ->
    rec[insert_0][3]#(x14,Cons(x10,x6)) -> insert_cond_1#(rec[leq_0][2](x14,x10),x14,x10,x6)
    rec[sort_0][2]#(Cons(x10,x6)) -> rec[insert_0][3]#(x10,rec[sort_0][2](x6)) ->
    rec[insert_0][3]#(x14,Cons(x10,x6)) -> rec[leq_0][2]#(x14,x10)
    rec[leq_0][2]#(S(x10),S(x6)) -> rec[leq_0][2]#(x10,x6) ->
    rec[leq_0][2]#(S(x10),S(x6)) -> rec[leq_0][2]#(x10,x6)
    rec[insert_0][3]#(x14,Cons(x10,x6)) -> rec[leq_0][2]#(x14,x10) ->
    rec[leq_0][2]#(S(x10),S(x6)) -> rec[leq_0][2]#(x10,x6)
    rec[insert_0][3]#(x14,Cons(x10,x6)) -> insert_cond_1#(rec[leq_0][2](x14,x10),x14,x10,x6) ->
    insert_cond_1#(False(),x7,x5,x3) -> rec[insert_0][3]#(x7,x3)
    insert_cond_1#(False(),x7,x5,x3) -> rec[insert_0][3]#(x7,x3) ->
    rec[insert_0][3]#(x14,Cons(x10,x6)) -> insert_cond_1#(rec[leq_0][2](x14,x10),x14,x10,x6)
    insert_cond_1#(False(),x7,x5,x3) -> rec[insert_0][3]#(x7,x3) ->
    rec[insert_0][3]#(x14,Cons(x10,x6)) -> rec[leq_0][2]#(x14,x10)
   SCC Processor:
    #sccs: 3
    #rules: 4
    #arcs: 11/49
    DPs:
     rec[sort_0][2]#(Cons(x10,x6)) -> rec[sort_0][2]#(x6)
    TRS:
     insert_cond_1(True(),x7,x5,x3) -> Cons(x7,Cons(x5,x3))
     insert_cond_1(False(),x7,x5,x3) -> Cons(x5,rec[insert_0][3](x7,x3))
     rec[insert_0][3](x6,Nil()) -> Cons(x6,Nil())
     rec[insert_0][3](x14,Cons(x10,x6)) -> insert_cond_1(rec[leq_0][2](x14,x10),x14,x10,x6)
     rec[sort_0][2](Nil()) -> Nil()
     rec[sort_0][2](Cons(x10,x6)) -> rec[insert_0][3](x10,rec[sort_0][2](x6))
     rec[leq_0][2](0(),x18) -> True()
     rec[leq_0][2](S(x26),0()) -> False()
     rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6)
     main(x3) -> rec[sort_0][2](x3)
    Subterm Criterion Processor:
     simple projection:
      pi(rec[sort_0][2]#) = 0
     problem:
      DPs:
       
      TRS:
       insert_cond_1(True(),x7,x5,x3) -> Cons(x7,Cons(x5,x3))
       insert_cond_1(False(),x7,x5,x3) -> Cons(x5,rec[insert_0][3](x7,x3))
       rec[insert_0][3](x6,Nil()) -> Cons(x6,Nil())
       rec[insert_0][3](x14,Cons(x10,x6)) -> insert_cond_1(rec[leq_0][2](x14,x10),x14,x10,x6)
       rec[sort_0][2](Nil()) -> Nil()
       rec[sort_0][2](Cons(x10,x6)) -> rec[insert_0][3](x10,rec[sort_0][2](x6))
       rec[leq_0][2](0(),x18) -> True()
       rec[leq_0][2](S(x26),0()) -> False()
       rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6)
       main(x3) -> rec[sort_0][2](x3)
     Qed
    
    DPs:
     rec[insert_0][3]#(x14,Cons(x10,x6)) -> insert_cond_1#(rec[leq_0][2](x14,x10),x14,x10,x6)
     insert_cond_1#(False(),x7,x5,x3) -> rec[insert_0][3]#(x7,x3)
    TRS:
     insert_cond_1(True(),x7,x5,x3) -> Cons(x7,Cons(x5,x3))
     insert_cond_1(False(),x7,x5,x3) -> Cons(x5,rec[insert_0][3](x7,x3))
     rec[insert_0][3](x6,Nil()) -> Cons(x6,Nil())
     rec[insert_0][3](x14,Cons(x10,x6)) -> insert_cond_1(rec[leq_0][2](x14,x10),x14,x10,x6)
     rec[sort_0][2](Nil()) -> Nil()
     rec[sort_0][2](Cons(x10,x6)) -> rec[insert_0][3](x10,rec[sort_0][2](x6))
     rec[leq_0][2](0(),x18) -> True()
     rec[leq_0][2](S(x26),0()) -> False()
     rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6)
     main(x3) -> rec[sort_0][2](x3)
    Subterm Criterion Processor:
     simple projection:
      pi(insert_cond_1#) = 3
      pi(rec[insert_0][3]#) = 1
     problem:
      DPs:
       insert_cond_1#(False(),x7,x5,x3) -> rec[insert_0][3]#(x7,x3)
      TRS:
       insert_cond_1(True(),x7,x5,x3) -> Cons(x7,Cons(x5,x3))
       insert_cond_1(False(),x7,x5,x3) -> Cons(x5,rec[insert_0][3](x7,x3))
       rec[insert_0][3](x6,Nil()) -> Cons(x6,Nil())
       rec[insert_0][3](x14,Cons(x10,x6)) -> insert_cond_1(rec[leq_0][2](x14,x10),x14,x10,x6)
       rec[sort_0][2](Nil()) -> Nil()
       rec[sort_0][2](Cons(x10,x6)) -> rec[insert_0][3](x10,rec[sort_0][2](x6))
       rec[leq_0][2](0(),x18) -> True()
       rec[leq_0][2](S(x26),0()) -> False()
       rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6)
       main(x3) -> rec[sort_0][2](x3)
     SCC Processor:
      #sccs: 0
      #rules: 0
      #arcs: 2/1
      
    
    DPs:
     rec[leq_0][2]#(S(x10),S(x6)) -> rec[leq_0][2]#(x10,x6)
    TRS:
     insert_cond_1(True(),x7,x5,x3) -> Cons(x7,Cons(x5,x3))
     insert_cond_1(False(),x7,x5,x3) -> Cons(x5,rec[insert_0][3](x7,x3))
     rec[insert_0][3](x6,Nil()) -> Cons(x6,Nil())
     rec[insert_0][3](x14,Cons(x10,x6)) -> insert_cond_1(rec[leq_0][2](x14,x10),x14,x10,x6)
     rec[sort_0][2](Nil()) -> Nil()
     rec[sort_0][2](Cons(x10,x6)) -> rec[insert_0][3](x10,rec[sort_0][2](x6))
     rec[leq_0][2](0(),x18) -> True()
     rec[leq_0][2](S(x26),0()) -> False()
     rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6)
     main(x3) -> rec[sort_0][2](x3)
    Subterm Criterion Processor:
     simple projection:
      pi(rec[leq_0][2]#) = 0
     problem:
      DPs:
       
      TRS:
       insert_cond_1(True(),x7,x5,x3) -> Cons(x7,Cons(x5,x3))
       insert_cond_1(False(),x7,x5,x3) -> Cons(x5,rec[insert_0][3](x7,x3))
       rec[insert_0][3](x6,Nil()) -> Cons(x6,Nil())
       rec[insert_0][3](x14,Cons(x10,x6)) -> insert_cond_1(rec[leq_0][2](x14,x10),x14,x10,x6)
       rec[sort_0][2](Nil()) -> Nil()
       rec[sort_0][2](Cons(x10,x6)) -> rec[insert_0][3](x10,rec[sort_0][2](x6))
       rec[leq_0][2](0(),x18) -> True()
       rec[leq_0][2](S(x26),0()) -> False()
       rec[leq_0][2](S(x10),S(x6)) -> rec[leq_0][2](x10,x6)
       main(x3) -> rec[sort_0][2](x3)
     Qed