YES

Problem:
 ite(tt(),x,y) -> x
 ite(ff(),x,y) -> y
 lt(0(),s(y)) -> tt()
 lt(x,0()) -> ff()
 lt(s(x),s(y)) -> lt(x,y)
 insert(a,nil()) -> cons(a,nil())
 insert(a,cons(b,l)) -> ite(lt(a,b),cons(a,cons(b,l)),cons(b,insert(a,l)))
 sort(nil()) -> nil()
 sort(cons(a,l)) -> insert(a,sort(l))

Proof:
 DP Processor:
  DPs:
   lt#(s(x),s(y)) -> lt#(x,y)
   insert#(a,cons(b,l)) -> insert#(a,l)
   insert#(a,cons(b,l)) -> lt#(a,b)
   insert#(a,cons(b,l)) -> ite#(lt(a,b),cons(a,cons(b,l)),cons(b,insert(a,l)))
   sort#(cons(a,l)) -> sort#(l)
   sort#(cons(a,l)) -> insert#(a,sort(l))
  TRS:
   ite(tt(),x,y) -> x
   ite(ff(),x,y) -> y
   lt(0(),s(y)) -> tt()
   lt(x,0()) -> ff()
   lt(s(x),s(y)) -> lt(x,y)
   insert(a,nil()) -> cons(a,nil())
   insert(a,cons(b,l)) -> ite(lt(a,b),cons(a,cons(b,l)),cons(b,insert(a,l)))
   sort(nil()) -> nil()
   sort(cons(a,l)) -> insert(a,sort(l))
  TDG Processor:
   DPs:
    lt#(s(x),s(y)) -> lt#(x,y)
    insert#(a,cons(b,l)) -> insert#(a,l)
    insert#(a,cons(b,l)) -> lt#(a,b)
    insert#(a,cons(b,l)) -> ite#(lt(a,b),cons(a,cons(b,l)),cons(b,insert(a,l)))
    sort#(cons(a,l)) -> sort#(l)
    sort#(cons(a,l)) -> insert#(a,sort(l))
   TRS:
    ite(tt(),x,y) -> x
    ite(ff(),x,y) -> y
    lt(0(),s(y)) -> tt()
    lt(x,0()) -> ff()
    lt(s(x),s(y)) -> lt(x,y)
    insert(a,nil()) -> cons(a,nil())
    insert(a,cons(b,l)) -> ite(lt(a,b),cons(a,cons(b,l)),cons(b,insert(a,l)))
    sort(nil()) -> nil()
    sort(cons(a,l)) -> insert(a,sort(l))
   graph:
    sort#(cons(a,l)) -> sort#(l) ->
    sort#(cons(a,l)) -> insert#(a,sort(l))
    sort#(cons(a,l)) -> sort#(l) ->
    sort#(cons(a,l)) -> sort#(l)
    sort#(cons(a,l)) -> insert#(a,sort(l)) ->
    insert#(a,cons(b,l)) -> ite#(lt(a,b),cons(a,cons(b,l)),cons(b,insert(a,l)))
    sort#(cons(a,l)) -> insert#(a,sort(l)) ->
    insert#(a,cons(b,l)) -> lt#(a,b)
    sort#(cons(a,l)) -> insert#(a,sort(l)) ->
    insert#(a,cons(b,l)) -> insert#(a,l)
    insert#(a,cons(b,l)) -> insert#(a,l) ->
    insert#(a,cons(b,l)) -> ite#(lt(a,b),cons(a,cons(b,l)),cons(b,insert(a,l)))
    insert#(a,cons(b,l)) -> insert#(a,l) ->
    insert#(a,cons(b,l)) -> lt#(a,b)
    insert#(a,cons(b,l)) -> insert#(a,l) ->
    insert#(a,cons(b,l)) -> insert#(a,l)
    insert#(a,cons(b,l)) -> lt#(a,b) -> lt#(s(x),s(y)) -> lt#(x,y)
    lt#(s(x),s(y)) -> lt#(x,y) -> lt#(s(x),s(y)) -> lt#(x,y)
   SCC Processor:
    #sccs: 3
    #rules: 3
    #arcs: 10/36
    DPs:
     sort#(cons(a,l)) -> sort#(l)
    TRS:
     ite(tt(),x,y) -> x
     ite(ff(),x,y) -> y
     lt(0(),s(y)) -> tt()
     lt(x,0()) -> ff()
     lt(s(x),s(y)) -> lt(x,y)
     insert(a,nil()) -> cons(a,nil())
     insert(a,cons(b,l)) -> ite(lt(a,b),cons(a,cons(b,l)),cons(b,insert(a,l)))
     sort(nil()) -> nil()
     sort(cons(a,l)) -> insert(a,sort(l))
    LPO Processor:
     argument filtering:
      pi(tt) = []
      pi(ite) = [1,2]
      pi(ff) = []
      pi(0) = []
      pi(s) = []
      pi(lt) = []
      pi(nil) = []
      pi(insert) = [1]
      pi(cons) = [1]
      pi(sort) = [0]
      pi(sort#) = 0
     precedence:
      sort > insert > lt > sort# ~ cons ~ nil ~ s ~ 0 ~ ff ~ ite ~ tt
     problem:
      DPs:
       
      TRS:
       ite(tt(),x,y) -> x
       ite(ff(),x,y) -> y
       lt(0(),s(y)) -> tt()
       lt(x,0()) -> ff()
       lt(s(x),s(y)) -> lt(x,y)
       insert(a,nil()) -> cons(a,nil())
       insert(a,cons(b,l)) -> ite(lt(a,b),cons(a,cons(b,l)),cons(b,insert(a,l)))
       sort(nil()) -> nil()
       sort(cons(a,l)) -> insert(a,sort(l))
     Qed
    
    DPs:
     insert#(a,cons(b,l)) -> insert#(a,l)
    TRS:
     ite(tt(),x,y) -> x
     ite(ff(),x,y) -> y
     lt(0(),s(y)) -> tt()
     lt(x,0()) -> ff()
     lt(s(x),s(y)) -> lt(x,y)
     insert(a,nil()) -> cons(a,nil())
     insert(a,cons(b,l)) -> ite(lt(a,b),cons(a,cons(b,l)),cons(b,insert(a,l)))
     sort(nil()) -> nil()
     sort(cons(a,l)) -> insert(a,sort(l))
    LPO Processor:
     argument filtering:
      pi(tt) = []
      pi(ite) = [1,2]
      pi(ff) = []
      pi(0) = []
      pi(s) = []
      pi(lt) = []
      pi(nil) = []
      pi(insert) = [1]
      pi(cons) = [1]
      pi(sort) = [0]
      pi(insert#) = 1
     precedence:
      sort > insert ~ lt > insert# ~ cons ~ nil ~ s ~ 0 ~ ff ~ ite ~ tt
     problem:
      DPs:
       
      TRS:
       ite(tt(),x,y) -> x
       ite(ff(),x,y) -> y
       lt(0(),s(y)) -> tt()
       lt(x,0()) -> ff()
       lt(s(x),s(y)) -> lt(x,y)
       insert(a,nil()) -> cons(a,nil())
       insert(a,cons(b,l)) -> ite(lt(a,b),cons(a,cons(b,l)),cons(b,insert(a,l)))
       sort(nil()) -> nil()
       sort(cons(a,l)) -> insert(a,sort(l))
     Qed
    
    DPs:
     lt#(s(x),s(y)) -> lt#(x,y)
    TRS:
     ite(tt(),x,y) -> x
     ite(ff(),x,y) -> y
     lt(0(),s(y)) -> tt()
     lt(x,0()) -> ff()
     lt(s(x),s(y)) -> lt(x,y)
     insert(a,nil()) -> cons(a,nil())
     insert(a,cons(b,l)) -> ite(lt(a,b),cons(a,cons(b,l)),cons(b,insert(a,l)))
     sort(nil()) -> nil()
     sort(cons(a,l)) -> insert(a,sort(l))
    Arctic Interpretation Processor:
     dimension: 1
     interpretation:
      [lt#](x0, x1) = x0 + 1x1 + 0,
      
      [sort](x0) = 6,
      
      [cons](x0, x1) = 1,
      
      [insert](x0, x1) = 5,
      
      [nil] = 2,
      
      [lt](x0, x1) = x0 + 5x1 + 0,
      
      [s](x0) = 1x0 + 0,
      
      [0] = 2,
      
      [ff] = 1,
      
      [ite](x0, x1, x2) = 1x1 + 3x2,
      
      [tt] = 1
     orientation:
      lt#(s(x),s(y)) = 1x + 2y + 1 >= x + 1y + 0 = lt#(x,y)
      
      ite(tt(),x,y) = 1x + 3y >= x = x
      
      ite(ff(),x,y) = 1x + 3y >= y = y
      
      lt(0(),s(y)) = 6y + 5 >= 1 = tt()
      
      lt(x,0()) = x + 7 >= 1 = ff()
      
      lt(s(x),s(y)) = 1x + 6y + 5 >= x + 5y + 0 = lt(x,y)
      
      insert(a,nil()) = 5 >= 1 = cons(a,nil())
      
      insert(a,cons(b,l)) = 5 >= 4 = ite(lt(a,b),cons(a,cons(b,l)),cons(b,insert(a,l)))
      
      sort(nil()) = 6 >= 2 = nil()
      
      sort(cons(a,l)) = 6 >= 5 = insert(a,sort(l))
     problem:
      DPs:
       
      TRS:
       ite(tt(),x,y) -> x
       ite(ff(),x,y) -> y
       lt(0(),s(y)) -> tt()
       lt(x,0()) -> ff()
       lt(s(x),s(y)) -> lt(x,y)
       insert(a,nil()) -> cons(a,nil())
       insert(a,cons(b,l)) -> ite(lt(a,b),cons(a,cons(b,l)),cons(b,insert(a,l)))
       sort(nil()) -> nil()
       sort(cons(a,l)) -> insert(a,sort(l))
     Qed