YES

Problem:
 le(0(),Y) -> true()
 le(s(X),0()) -> false()
 le(s(X),s(Y)) -> le(X,Y)
 app(nil(),Y) -> Y
 app(cons(N,L),Y) -> cons(N,app(L,Y))
 low(N,nil()) -> nil()
 low(N,cons(M,L)) -> iflow(le(M,N),N,cons(M,L))
 iflow(true(),N,cons(M,L)) -> cons(M,low(N,L))
 iflow(false(),N,cons(M,L)) -> low(N,L)
 high(N,nil()) -> nil()
 high(N,cons(M,L)) -> ifhigh(le(M,N),N,cons(M,L))
 ifhigh(true(),N,cons(M,L)) -> high(N,L)
 ifhigh(false(),N,cons(M,L)) -> cons(M,high(N,L))
 quicksort(nil()) -> nil()
 quicksort(cons(N,L)) -> app(quicksort(low(N,L)),cons(N,quicksort(high(N,L))))

Proof:
 DP Processor:
  DPs:
   le#(s(X),s(Y)) -> le#(X,Y)
   app#(cons(N,L),Y) -> app#(L,Y)
   low#(N,cons(M,L)) -> le#(M,N)
   low#(N,cons(M,L)) -> iflow#(le(M,N),N,cons(M,L))
   iflow#(true(),N,cons(M,L)) -> low#(N,L)
   iflow#(false(),N,cons(M,L)) -> low#(N,L)
   high#(N,cons(M,L)) -> le#(M,N)
   high#(N,cons(M,L)) -> ifhigh#(le(M,N),N,cons(M,L))
   ifhigh#(true(),N,cons(M,L)) -> high#(N,L)
   ifhigh#(false(),N,cons(M,L)) -> high#(N,L)
   quicksort#(cons(N,L)) -> high#(N,L)
   quicksort#(cons(N,L)) -> quicksort#(high(N,L))
   quicksort#(cons(N,L)) -> low#(N,L)
   quicksort#(cons(N,L)) -> quicksort#(low(N,L))
   quicksort#(cons(N,L)) -> app#(quicksort(low(N,L)),cons(N,quicksort(high(N,L))))
  TRS:
   le(0(),Y) -> true()
   le(s(X),0()) -> false()
   le(s(X),s(Y)) -> le(X,Y)
   app(nil(),Y) -> Y
   app(cons(N,L),Y) -> cons(N,app(L,Y))
   low(N,nil()) -> nil()
   low(N,cons(M,L)) -> iflow(le(M,N),N,cons(M,L))
   iflow(true(),N,cons(M,L)) -> cons(M,low(N,L))
   iflow(false(),N,cons(M,L)) -> low(N,L)
   high(N,nil()) -> nil()
   high(N,cons(M,L)) -> ifhigh(le(M,N),N,cons(M,L))
   ifhigh(true(),N,cons(M,L)) -> high(N,L)
   ifhigh(false(),N,cons(M,L)) -> cons(M,high(N,L))
   quicksort(nil()) -> nil()
   quicksort(cons(N,L)) -> app(quicksort(low(N,L)),cons(N,quicksort(high(N,L))))
  TDG Processor:
   DPs:
    le#(s(X),s(Y)) -> le#(X,Y)
    app#(cons(N,L),Y) -> app#(L,Y)
    low#(N,cons(M,L)) -> le#(M,N)
    low#(N,cons(M,L)) -> iflow#(le(M,N),N,cons(M,L))
    iflow#(true(),N,cons(M,L)) -> low#(N,L)
    iflow#(false(),N,cons(M,L)) -> low#(N,L)
    high#(N,cons(M,L)) -> le#(M,N)
    high#(N,cons(M,L)) -> ifhigh#(le(M,N),N,cons(M,L))
    ifhigh#(true(),N,cons(M,L)) -> high#(N,L)
    ifhigh#(false(),N,cons(M,L)) -> high#(N,L)
    quicksort#(cons(N,L)) -> high#(N,L)
    quicksort#(cons(N,L)) -> quicksort#(high(N,L))
    quicksort#(cons(N,L)) -> low#(N,L)
    quicksort#(cons(N,L)) -> quicksort#(low(N,L))
    quicksort#(cons(N,L)) -> app#(quicksort(low(N,L)),cons(N,quicksort(high(N,L))))
   TRS:
    le(0(),Y) -> true()
    le(s(X),0()) -> false()
    le(s(X),s(Y)) -> le(X,Y)
    app(nil(),Y) -> Y
    app(cons(N,L),Y) -> cons(N,app(L,Y))
    low(N,nil()) -> nil()
    low(N,cons(M,L)) -> iflow(le(M,N),N,cons(M,L))
    iflow(true(),N,cons(M,L)) -> cons(M,low(N,L))
    iflow(false(),N,cons(M,L)) -> low(N,L)
    high(N,nil()) -> nil()
    high(N,cons(M,L)) -> ifhigh(le(M,N),N,cons(M,L))
    ifhigh(true(),N,cons(M,L)) -> high(N,L)
    ifhigh(false(),N,cons(M,L)) -> cons(M,high(N,L))
    quicksort(nil()) -> nil()
    quicksort(cons(N,L)) -> app(quicksort(low(N,L)),cons(N,quicksort(high(N,L))))
   graph:
    quicksort#(cons(N,L)) -> quicksort#(high(N,L)) ->
    quicksort#(cons(N,L)) -> app#(quicksort(low(N,L)),cons(N,quicksort(high(N,L))))
    quicksort#(cons(N,L)) -> quicksort#(high(N,L)) ->
    quicksort#(cons(N,L)) -> quicksort#(low(N,L))
    quicksort#(cons(N,L)) -> quicksort#(high(N,L)) ->
    quicksort#(cons(N,L)) -> low#(N,L)
    quicksort#(cons(N,L)) -> quicksort#(high(N,L)) ->
    quicksort#(cons(N,L)) -> quicksort#(high(N,L))
    quicksort#(cons(N,L)) -> quicksort#(high(N,L)) ->
    quicksort#(cons(N,L)) -> high#(N,L)
    quicksort#(cons(N,L)) -> quicksort#(low(N,L)) ->
    quicksort#(cons(N,L)) -> app#(quicksort(low(N,L)),cons(N,quicksort(high(N,L))))
    quicksort#(cons(N,L)) -> quicksort#(low(N,L)) ->
    quicksort#(cons(N,L)) -> quicksort#(low(N,L))
    quicksort#(cons(N,L)) -> quicksort#(low(N,L)) ->
    quicksort#(cons(N,L)) -> low#(N,L)
    quicksort#(cons(N,L)) -> quicksort#(low(N,L)) ->
    quicksort#(cons(N,L)) -> quicksort#(high(N,L))
    quicksort#(cons(N,L)) -> quicksort#(low(N,L)) ->
    quicksort#(cons(N,L)) -> high#(N,L)
    quicksort#(cons(N,L)) -> high#(N,L) ->
    high#(N,cons(M,L)) -> ifhigh#(le(M,N),N,cons(M,L))
    quicksort#(cons(N,L)) -> high#(N,L) ->
    high#(N,cons(M,L)) -> le#(M,N)
    quicksort#(cons(N,L)) -> low#(N,L) ->
    low#(N,cons(M,L)) -> iflow#(le(M,N),N,cons(M,L))
    quicksort#(cons(N,L)) -> low#(N,L) ->
    low#(N,cons(M,L)) -> le#(M,N)
    quicksort#(cons(N,L)) -> app#(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) ->
    app#(cons(N,L),Y) -> app#(L,Y)
    ifhigh#(false(),N,cons(M,L)) -> high#(N,L) ->
    high#(N,cons(M,L)) -> ifhigh#(le(M,N),N,cons(M,L))
    ifhigh#(false(),N,cons(M,L)) -> high#(N,L) ->
    high#(N,cons(M,L)) -> le#(M,N)
    ifhigh#(true(),N,cons(M,L)) -> high#(N,L) ->
    high#(N,cons(M,L)) -> ifhigh#(le(M,N),N,cons(M,L))
    ifhigh#(true(),N,cons(M,L)) -> high#(N,L) ->
    high#(N,cons(M,L)) -> le#(M,N)
    high#(N,cons(M,L)) -> ifhigh#(le(M,N),N,cons(M,L)) ->
    ifhigh#(false(),N,cons(M,L)) -> high#(N,L)
    high#(N,cons(M,L)) -> ifhigh#(le(M,N),N,cons(M,L)) ->
    ifhigh#(true(),N,cons(M,L)) -> high#(N,L)
    high#(N,cons(M,L)) -> le#(M,N) ->
    le#(s(X),s(Y)) -> le#(X,Y)
    iflow#(false(),N,cons(M,L)) -> low#(N,L) ->
    low#(N,cons(M,L)) -> iflow#(le(M,N),N,cons(M,L))
    iflow#(false(),N,cons(M,L)) -> low#(N,L) ->
    low#(N,cons(M,L)) -> le#(M,N)
    iflow#(true(),N,cons(M,L)) -> low#(N,L) ->
    low#(N,cons(M,L)) -> iflow#(le(M,N),N,cons(M,L))
    iflow#(true(),N,cons(M,L)) -> low#(N,L) ->
    low#(N,cons(M,L)) -> le#(M,N)
    low#(N,cons(M,L)) -> iflow#(le(M,N),N,cons(M,L)) ->
    iflow#(false(),N,cons(M,L)) -> low#(N,L)
    low#(N,cons(M,L)) -> iflow#(le(M,N),N,cons(M,L)) ->
    iflow#(true(),N,cons(M,L)) -> low#(N,L)
    low#(N,cons(M,L)) -> le#(M,N) -> le#(s(X),s(Y)) -> le#(X,Y)
    app#(cons(N,L),Y) -> app#(L,Y) -> app#(cons(N,L),Y) -> app#(L,Y)
    le#(s(X),s(Y)) -> le#(X,Y) -> le#(s(X),s(Y)) -> le#(X,Y)
   SCC Processor:
    #sccs: 5
    #rules: 10
    #arcs: 31/225
    DPs:
     quicksort#(cons(N,L)) -> quicksort#(high(N,L))
     quicksort#(cons(N,L)) -> quicksort#(low(N,L))
    TRS:
     le(0(),Y) -> true()
     le(s(X),0()) -> false()
     le(s(X),s(Y)) -> le(X,Y)
     app(nil(),Y) -> Y
     app(cons(N,L),Y) -> cons(N,app(L,Y))
     low(N,nil()) -> nil()
     low(N,cons(M,L)) -> iflow(le(M,N),N,cons(M,L))
     iflow(true(),N,cons(M,L)) -> cons(M,low(N,L))
     iflow(false(),N,cons(M,L)) -> low(N,L)
     high(N,nil()) -> nil()
     high(N,cons(M,L)) -> ifhigh(le(M,N),N,cons(M,L))
     ifhigh(true(),N,cons(M,L)) -> high(N,L)
     ifhigh(false(),N,cons(M,L)) -> cons(M,high(N,L))
     quicksort(nil()) -> nil()
     quicksort(cons(N,L)) -> app(quicksort(low(N,L)),cons(N,quicksort(high(N,L))))
    Usable Rule Processor:
     DPs:
      quicksort#(cons(N,L)) -> quicksort#(high(N,L))
      quicksort#(cons(N,L)) -> quicksort#(low(N,L))
     TRS:
      high(N,nil()) -> nil()
      high(N,cons(M,L)) -> ifhigh(le(M,N),N,cons(M,L))
      ifhigh(true(),N,cons(M,L)) -> high(N,L)
      ifhigh(false(),N,cons(M,L)) -> cons(M,high(N,L))
      le(0(),Y) -> true()
      le(s(X),0()) -> false()
      le(s(X),s(Y)) -> le(X,Y)
      low(N,nil()) -> nil()
      low(N,cons(M,L)) -> iflow(le(M,N),N,cons(M,L))
      iflow(true(),N,cons(M,L)) -> cons(M,low(N,L))
      iflow(false(),N,cons(M,L)) -> low(N,L)
     Arctic Interpretation Processor:
      dimension: 1
      usable rules:
       high(N,nil()) -> nil()
       high(N,cons(M,L)) -> ifhigh(le(M,N),N,cons(M,L))
       ifhigh(true(),N,cons(M,L)) -> high(N,L)
       ifhigh(false(),N,cons(M,L)) -> cons(M,high(N,L))
       low(N,nil()) -> nil()
       low(N,cons(M,L)) -> iflow(le(M,N),N,cons(M,L))
       iflow(true(),N,cons(M,L)) -> cons(M,low(N,L))
       iflow(false(),N,cons(M,L)) -> low(N,L)
      interpretation:
       [quicksort#](x0) = 6x0,
       
       [ifhigh](x0, x1, x2) = x2,
       
       [high](x0, x1) = x1,
       
       [iflow](x0, x1, x2) = x2,
       
       [low](x0, x1) = x1,
       
       [cons](x0, x1) = x0 + 1x1,
       
       [nil] = 0,
       
       [false] = 0,
       
       [s](x0) = 2x0 + 3,
       
       [true] = 1,
       
       [le](x0, x1) = 2x0 + 0,
       
       [0] = 2
      orientation:
       quicksort#(cons(N,L)) = 7L + 6N >= 6L = quicksort#(high(N,L))
       
       quicksort#(cons(N,L)) = 7L + 6N >= 6L = quicksort#(low(N,L))
       
       high(N,nil()) = 0 >= 0 = nil()
       
       high(N,cons(M,L)) = 1L + M >= 1L + M = ifhigh(le(M,N),N,cons(M,L))
       
       ifhigh(true(),N,cons(M,L)) = 1L + M >= L = high(N,L)
       
       ifhigh(false(),N,cons(M,L)) = 1L + M >= 1L + M = cons(M,high(N,L))
       
       le(0(),Y) = 4 >= 1 = true()
       
       le(s(X),0()) = 4X + 5 >= 0 = false()
       
       le(s(X),s(Y)) = 4X + 5 >= 2X + 0 = le(X,Y)
       
       low(N,nil()) = 0 >= 0 = nil()
       
       low(N,cons(M,L)) = 1L + M >= 1L + M = iflow(le(M,N),N,cons(M,L))
       
       iflow(true(),N,cons(M,L)) = 1L + M >= 1L + M = cons(M,low(N,L))
       
       iflow(false(),N,cons(M,L)) = 1L + M >= L = low(N,L)
      problem:
       DPs:
        
       TRS:
        high(N,nil()) -> nil()
        high(N,cons(M,L)) -> ifhigh(le(M,N),N,cons(M,L))
        ifhigh(true(),N,cons(M,L)) -> high(N,L)
        ifhigh(false(),N,cons(M,L)) -> cons(M,high(N,L))
        le(0(),Y) -> true()
        le(s(X),0()) -> false()
        le(s(X),s(Y)) -> le(X,Y)
        low(N,nil()) -> nil()
        low(N,cons(M,L)) -> iflow(le(M,N),N,cons(M,L))
        iflow(true(),N,cons(M,L)) -> cons(M,low(N,L))
        iflow(false(),N,cons(M,L)) -> low(N,L)
      Qed
    
    DPs:
     app#(cons(N,L),Y) -> app#(L,Y)
    TRS:
     le(0(),Y) -> true()
     le(s(X),0()) -> false()
     le(s(X),s(Y)) -> le(X,Y)
     app(nil(),Y) -> Y
     app(cons(N,L),Y) -> cons(N,app(L,Y))
     low(N,nil()) -> nil()
     low(N,cons(M,L)) -> iflow(le(M,N),N,cons(M,L))
     iflow(true(),N,cons(M,L)) -> cons(M,low(N,L))
     iflow(false(),N,cons(M,L)) -> low(N,L)
     high(N,nil()) -> nil()
     high(N,cons(M,L)) -> ifhigh(le(M,N),N,cons(M,L))
     ifhigh(true(),N,cons(M,L)) -> high(N,L)
     ifhigh(false(),N,cons(M,L)) -> cons(M,high(N,L))
     quicksort(nil()) -> nil()
     quicksort(cons(N,L)) -> app(quicksort(low(N,L)),cons(N,quicksort(high(N,L))))
    Subterm Criterion Processor:
     simple projection:
      pi(app#) = 0
     problem:
      DPs:
       
      TRS:
       le(0(),Y) -> true()
       le(s(X),0()) -> false()
       le(s(X),s(Y)) -> le(X,Y)
       app(nil(),Y) -> Y
       app(cons(N,L),Y) -> cons(N,app(L,Y))
       low(N,nil()) -> nil()
       low(N,cons(M,L)) -> iflow(le(M,N),N,cons(M,L))
       iflow(true(),N,cons(M,L)) -> cons(M,low(N,L))
       iflow(false(),N,cons(M,L)) -> low(N,L)
       high(N,nil()) -> nil()
       high(N,cons(M,L)) -> ifhigh(le(M,N),N,cons(M,L))
       ifhigh(true(),N,cons(M,L)) -> high(N,L)
       ifhigh(false(),N,cons(M,L)) -> cons(M,high(N,L))
       quicksort(nil()) -> nil()
       quicksort(cons(N,L)) -> app(quicksort(low(N,L)),cons(N,quicksort(high(N,L))))
     Qed
    
    DPs:
     low#(N,cons(M,L)) -> iflow#(le(M,N),N,cons(M,L))
     iflow#(true(),N,cons(M,L)) -> low#(N,L)
     iflow#(false(),N,cons(M,L)) -> low#(N,L)
    TRS:
     le(0(),Y) -> true()
     le(s(X),0()) -> false()
     le(s(X),s(Y)) -> le(X,Y)
     app(nil(),Y) -> Y
     app(cons(N,L),Y) -> cons(N,app(L,Y))
     low(N,nil()) -> nil()
     low(N,cons(M,L)) -> iflow(le(M,N),N,cons(M,L))
     iflow(true(),N,cons(M,L)) -> cons(M,low(N,L))
     iflow(false(),N,cons(M,L)) -> low(N,L)
     high(N,nil()) -> nil()
     high(N,cons(M,L)) -> ifhigh(le(M,N),N,cons(M,L))
     ifhigh(true(),N,cons(M,L)) -> high(N,L)
     ifhigh(false(),N,cons(M,L)) -> cons(M,high(N,L))
     quicksort(nil()) -> nil()
     quicksort(cons(N,L)) -> app(quicksort(low(N,L)),cons(N,quicksort(high(N,L))))
    Subterm Criterion Processor:
     simple projection:
      pi(low#) = 1
      pi(iflow#) = 2
     problem:
      DPs:
       low#(N,cons(M,L)) -> iflow#(le(M,N),N,cons(M,L))
      TRS:
       le(0(),Y) -> true()
       le(s(X),0()) -> false()
       le(s(X),s(Y)) -> le(X,Y)
       app(nil(),Y) -> Y
       app(cons(N,L),Y) -> cons(N,app(L,Y))
       low(N,nil()) -> nil()
       low(N,cons(M,L)) -> iflow(le(M,N),N,cons(M,L))
       iflow(true(),N,cons(M,L)) -> cons(M,low(N,L))
       iflow(false(),N,cons(M,L)) -> low(N,L)
       high(N,nil()) -> nil()
       high(N,cons(M,L)) -> ifhigh(le(M,N),N,cons(M,L))
       ifhigh(true(),N,cons(M,L)) -> high(N,L)
       ifhigh(false(),N,cons(M,L)) -> cons(M,high(N,L))
       quicksort(nil()) -> nil()
       quicksort(cons(N,L)) -> app(quicksort(low(N,L)),cons(N,quicksort(high(N,L))))
     SCC Processor:
      #sccs: 0
      #rules: 0
      #arcs: 4/1
      
    
    DPs:
     high#(N,cons(M,L)) -> ifhigh#(le(M,N),N,cons(M,L))
     ifhigh#(true(),N,cons(M,L)) -> high#(N,L)
     ifhigh#(false(),N,cons(M,L)) -> high#(N,L)
    TRS:
     le(0(),Y) -> true()
     le(s(X),0()) -> false()
     le(s(X),s(Y)) -> le(X,Y)
     app(nil(),Y) -> Y
     app(cons(N,L),Y) -> cons(N,app(L,Y))
     low(N,nil()) -> nil()
     low(N,cons(M,L)) -> iflow(le(M,N),N,cons(M,L))
     iflow(true(),N,cons(M,L)) -> cons(M,low(N,L))
     iflow(false(),N,cons(M,L)) -> low(N,L)
     high(N,nil()) -> nil()
     high(N,cons(M,L)) -> ifhigh(le(M,N),N,cons(M,L))
     ifhigh(true(),N,cons(M,L)) -> high(N,L)
     ifhigh(false(),N,cons(M,L)) -> cons(M,high(N,L))
     quicksort(nil()) -> nil()
     quicksort(cons(N,L)) -> app(quicksort(low(N,L)),cons(N,quicksort(high(N,L))))
    Subterm Criterion Processor:
     simple projection:
      pi(high#) = 1
      pi(ifhigh#) = 2
     problem:
      DPs:
       high#(N,cons(M,L)) -> ifhigh#(le(M,N),N,cons(M,L))
      TRS:
       le(0(),Y) -> true()
       le(s(X),0()) -> false()
       le(s(X),s(Y)) -> le(X,Y)
       app(nil(),Y) -> Y
       app(cons(N,L),Y) -> cons(N,app(L,Y))
       low(N,nil()) -> nil()
       low(N,cons(M,L)) -> iflow(le(M,N),N,cons(M,L))
       iflow(true(),N,cons(M,L)) -> cons(M,low(N,L))
       iflow(false(),N,cons(M,L)) -> low(N,L)
       high(N,nil()) -> nil()
       high(N,cons(M,L)) -> ifhigh(le(M,N),N,cons(M,L))
       ifhigh(true(),N,cons(M,L)) -> high(N,L)
       ifhigh(false(),N,cons(M,L)) -> cons(M,high(N,L))
       quicksort(nil()) -> nil()
       quicksort(cons(N,L)) -> app(quicksort(low(N,L)),cons(N,quicksort(high(N,L))))
     SCC Processor:
      #sccs: 0
      #rules: 0
      #arcs: 4/1
      
    
    DPs:
     le#(s(X),s(Y)) -> le#(X,Y)
    TRS:
     le(0(),Y) -> true()
     le(s(X),0()) -> false()
     le(s(X),s(Y)) -> le(X,Y)
     app(nil(),Y) -> Y
     app(cons(N,L),Y) -> cons(N,app(L,Y))
     low(N,nil()) -> nil()
     low(N,cons(M,L)) -> iflow(le(M,N),N,cons(M,L))
     iflow(true(),N,cons(M,L)) -> cons(M,low(N,L))
     iflow(false(),N,cons(M,L)) -> low(N,L)
     high(N,nil()) -> nil()
     high(N,cons(M,L)) -> ifhigh(le(M,N),N,cons(M,L))
     ifhigh(true(),N,cons(M,L)) -> high(N,L)
     ifhigh(false(),N,cons(M,L)) -> cons(M,high(N,L))
     quicksort(nil()) -> nil()
     quicksort(cons(N,L)) -> app(quicksort(low(N,L)),cons(N,quicksort(high(N,L))))
    Subterm Criterion Processor:
     simple projection:
      pi(le#) = 1
     problem:
      DPs:
       
      TRS:
       le(0(),Y) -> true()
       le(s(X),0()) -> false()
       le(s(X),s(Y)) -> le(X,Y)
       app(nil(),Y) -> Y
       app(cons(N,L),Y) -> cons(N,app(L,Y))
       low(N,nil()) -> nil()
       low(N,cons(M,L)) -> iflow(le(M,N),N,cons(M,L))
       iflow(true(),N,cons(M,L)) -> cons(M,low(N,L))
       iflow(false(),N,cons(M,L)) -> low(N,L)
       high(N,nil()) -> nil()
       high(N,cons(M,L)) -> ifhigh(le(M,N),N,cons(M,L))
       ifhigh(true(),N,cons(M,L)) -> high(N,L)
       ifhigh(false(),N,cons(M,L)) -> cons(M,high(N,L))
       quicksort(nil()) -> nil()
       quicksort(cons(N,L)) -> app(quicksort(low(N,L)),cons(N,quicksort(high(N,L))))
     Qed