MAYBE
Time: 0.008048
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)))}
 DP:
  DP:
   {                  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) -> app#(quicksort low(N, L), cons(N, quicksort high(N, L))),
              quicksort# cons(N, L) -> low#(N, L),
              quicksort# cons(N, L) -> high#(N, L),
              quicksort# cons(N, L) -> quicksort# low(N, L),
              quicksort# cons(N, L) -> 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)))}
  EDG:
   {(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))
    (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))
    (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))
    (low#(N, cons(M, L)) -> le#(M, N), le#(s X, s Y) -> le#(X, Y))
    (le#(s X, s Y) -> le#(X, Y), le#(s X, s Y) -> le#(X, Y))
    (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))
    (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) -> quicksort# low(N, L))
    (quicksort# cons(N, L) -> quicksort# low(N, L), quicksort# cons(N, L) -> high#(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) -> app#(quicksort low(N, L), cons(N, quicksort high(N, L))))
    (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) -> low#(N, L))
    (quicksort# cons(N, L) -> quicksort# high(N, L), quicksort# cons(N, L) -> 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) -> quicksort# 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)) -> ifhigh#(le(M, N), N, cons(M, L)), ifhigh#(false(), N, cons(M, L)) -> high#(N, L))
    (app#(cons(N, L), Y) -> app#(L, Y), app#(cons(N, L), Y) -> app#(L, Y))
    (high#(N, cons(M, L)) -> le#(M, N), le#(s X, s Y) -> le#(X, Y))
    (quicksort# cons(N, L) -> high#(N, L), high#(N, cons(M, L)) -> le#(M, N))
    (quicksort# cons(N, 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#(false(), N, cons(M, L)) -> high#(N, L), high#(N, cons(M, L)) -> ifhigh#(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#(false(), N, cons(M, L)) -> low#(N, L), low#(N, cons(M, L)) -> iflow#(le(M, N), N, cons(M, L)))
    (quicksort# cons(N, L) -> app#(quicksort low(N, L), cons(N, quicksort high(N, L))), app#(cons(N, L), Y) -> app#(L, Y))}
   STATUS:
    arrows: 0.862222
    SCCS (5):
     Scc:
      {quicksort# cons(N, L) -> quicksort# low(N, L),
       quicksort# cons(N, L) -> quicksort# high(N, L)}
     Scc:
      {           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)}
     Scc:
      {           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)}
     Scc:
      {le#(s X, s Y) -> le#(X, Y)}
     Scc:
      {app#(cons(N, L), Y) -> app#(L, Y)}
     
     SCC (2):
      Strict:
       {quicksort# cons(N, L) -> quicksort# low(N, L),
        quicksort# cons(N, L) -> quicksort# high(N, L)}
      Weak:
      {                    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)))}
      Open
     
     
     SCC (3):
      Strict:
       {           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)}
      Weak:
      {                    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)))}
      Open
     
     SCC (3):
      Strict:
       {           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)}
      Weak:
      {                    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)))}
      Open
     
     SCC (1):
      Strict:
       {le#(s X, s Y) -> le#(X, Y)}
      Weak:
      {                    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)))}
      Open
     
     SCC (1):
      Strict:
       {app#(cons(N, L), Y) -> app#(L, Y)}
      Weak:
      {                    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)))}
      Open