MAYBE
Time: 0.009565
TRS:
 {                    le(0(), y) -> true(),
                    le(s x, 0()) -> false(),
                    le(s x, s y) -> le(x, y),
                   app(nil(), y) -> y,
               app(add(n, x), y) -> add(n, app(x, y)),
                   low(n, nil()) -> nil(),
               low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x)),
    if_low(true(), n, add(m, x)) -> add(m, low(n, x)),
   if_low(false(), n, add(m, x)) -> low(n, x),
                  high(n, nil()) -> nil(),
              high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x)),
   if_high(true(), n, add(m, x)) -> high(n, x),
  if_high(false(), n, add(m, x)) -> add(m, high(n, x)),
                  head add(n, x) -> n,
                  tail add(n, x) -> x,
                   isempty nil() -> true(),
               isempty add(n, x) -> false(),
          if_qs(true(), x, n, y) -> nil(),
         if_qs(false(), x, n, y) -> app(quicksort x, add(n, quicksort y)),
                     quicksort x -> if_qs(isempty x, low(head x, tail x), head x, high(head x, tail x))}
 DP:
  DP:
   {                  le#(s x, s y) -> le#(x, y),
                 app#(add(n, x), y) -> app#(x, y),
                 low#(n, add(m, x)) -> le#(m, n),
                 low#(n, add(m, x)) -> if_low#(le(m, n), n, add(m, x)),
      if_low#(true(), n, add(m, x)) -> low#(n, x),
     if_low#(false(), n, add(m, x)) -> low#(n, x),
                high#(n, add(m, x)) -> le#(m, n),
                high#(n, add(m, x)) -> if_high#(le(m, n), n, add(m, x)),
     if_high#(true(), n, add(m, x)) -> high#(n, x),
    if_high#(false(), n, add(m, x)) -> high#(n, x),
           if_qs#(false(), x, n, y) -> app#(quicksort x, add(n, quicksort y)),
           if_qs#(false(), x, n, y) -> quicksort# y,
           if_qs#(false(), x, n, y) -> quicksort# x,
                       quicksort# x -> low#(head x, tail x),
                       quicksort# x -> high#(head x, tail x),
                       quicksort# x -> head# x,
                       quicksort# x -> tail# x,
                       quicksort# x -> isempty# x,
                       quicksort# x -> if_qs#(isempty x, low(head x, tail x), head x, high(head x, tail x))}
  TRS:
  {                    le(0(), y) -> true(),
                     le(s x, 0()) -> false(),
                     le(s x, s y) -> le(x, y),
                    app(nil(), y) -> y,
                app(add(n, x), y) -> add(n, app(x, y)),
                    low(n, nil()) -> nil(),
                low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x)),
     if_low(true(), n, add(m, x)) -> add(m, low(n, x)),
    if_low(false(), n, add(m, x)) -> low(n, x),
                   high(n, nil()) -> nil(),
               high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x)),
    if_high(true(), n, add(m, x)) -> high(n, x),
   if_high(false(), n, add(m, x)) -> add(m, high(n, x)),
                   head add(n, x) -> n,
                   tail add(n, x) -> x,
                    isempty nil() -> true(),
                isempty add(n, x) -> false(),
           if_qs(true(), x, n, y) -> nil(),
          if_qs(false(), x, n, y) -> app(quicksort x, add(n, quicksort y)),
                      quicksort x -> if_qs(isempty x, low(head x, tail x), head x, high(head x, tail x))}
  EDG:
   {(high#(n, add(m, x)) -> if_high#(le(m, n), n, add(m, x)), if_high#(false(), n, add(m, x)) -> high#(n, x))
    (high#(n, add(m, x)) -> if_high#(le(m, n), n, add(m, x)), if_high#(true(), n, add(m, x)) -> high#(n, x))
    (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
    (low#(n, add(m, x)) -> le#(m, n), le#(s x, s y) -> le#(x, y))
    (quicksort# x -> low#(head x, tail x), low#(n, add(m, x)) -> if_low#(le(m, n), n, add(m, x)))
    (quicksort# x -> low#(head x, tail x), low#(n, add(m, x)) -> le#(m, n))
    (if_qs#(false(), x, n, y) -> quicksort# y, quicksort# x -> if_qs#(isempty x, low(head x, tail x), head x, high(head x, tail x)))
    (if_qs#(false(), x, n, y) -> quicksort# y, quicksort# x -> isempty# x)
    (if_qs#(false(), x, n, y) -> quicksort# y, quicksort# x -> tail# x)
    (if_qs#(false(), x, n, y) -> quicksort# y, quicksort# x -> head# x)
    (if_qs#(false(), x, n, y) -> quicksort# y, quicksort# x -> high#(head x, tail x))
    (if_qs#(false(), x, n, y) -> quicksort# y, quicksort# x -> low#(head x, tail x))
    (if_low#(true(), n, add(m, x)) -> low#(n, x), low#(n, add(m, x)) -> if_low#(le(m, n), n, add(m, x)))
    (if_low#(true(), n, add(m, x)) -> low#(n, x), low#(n, add(m, x)) -> le#(m, n))
    (if_high#(true(), n, add(m, x)) -> high#(n, x), high#(n, add(m, x)) -> if_high#(le(m, n), n, add(m, x)))
    (if_high#(true(), n, add(m, x)) -> high#(n, x), high#(n, add(m, x)) -> le#(m, n))
    (if_qs#(false(), x, n, y) -> quicksort# x, quicksort# x -> if_qs#(isempty x, low(head x, tail x), head x, high(head x, tail x)))
    (if_qs#(false(), x, n, y) -> quicksort# x, quicksort# x -> isempty# x)
    (if_qs#(false(), x, n, y) -> quicksort# x, quicksort# x -> tail# x)
    (if_qs#(false(), x, n, y) -> quicksort# x, quicksort# x -> head# x)
    (if_qs#(false(), x, n, y) -> quicksort# x, quicksort# x -> high#(head x, tail x))
    (if_qs#(false(), x, n, y) -> quicksort# x, quicksort# x -> low#(head x, tail x))
    (if_high#(false(), n, add(m, x)) -> high#(n, x), high#(n, add(m, x)) -> le#(m, n))
    (if_high#(false(), n, add(m, x)) -> high#(n, x), high#(n, add(m, x)) -> if_high#(le(m, n), n, add(m, x)))
    (if_low#(false(), n, add(m, x)) -> low#(n, x), low#(n, add(m, x)) -> le#(m, n))
    (if_low#(false(), n, add(m, x)) -> low#(n, x), low#(n, add(m, x)) -> if_low#(le(m, n), n, add(m, x)))
    (quicksort# x -> if_qs#(isempty x, low(head x, tail x), head x, high(head x, tail x)), if_qs#(false(), x, n, y) -> app#(quicksort x, add(n, quicksort y)))
    (quicksort# x -> if_qs#(isempty x, low(head x, tail x), head x, high(head x, tail x)), if_qs#(false(), x, n, y) -> quicksort# y)
    (quicksort# x -> if_qs#(isempty x, low(head x, tail x), head x, high(head x, tail x)), if_qs#(false(), x, n, y) -> quicksort# x)
    (quicksort# x -> high#(head x, tail x), high#(n, add(m, x)) -> le#(m, n))
    (quicksort# x -> high#(head x, tail x), high#(n, add(m, x)) -> if_high#(le(m, n), n, add(m, x)))
    (high#(n, add(m, x)) -> le#(m, n), le#(s x, s y) -> le#(x, y))
    (app#(add(n, x), y) -> app#(x, y), app#(add(n, x), y) -> app#(x, y))
    (if_qs#(false(), x, n, y) -> app#(quicksort x, add(n, quicksort y)), app#(add(n, x), y) -> app#(x, y))
    (low#(n, add(m, x)) -> if_low#(le(m, n), n, add(m, x)), if_low#(true(), n, add(m, x)) -> low#(n, x))
    (low#(n, add(m, x)) -> if_low#(le(m, n), n, add(m, x)), if_low#(false(), n, add(m, x)) -> low#(n, x))}
   STATUS:
    arrows: 0.900277
    SCCS (5):
     Scc:
      {if_qs#(false(), x, n, y) -> quicksort# y,
       if_qs#(false(), x, n, y) -> quicksort# x,
                   quicksort# x -> if_qs#(isempty x, low(head x, tail x), head x, high(head x, tail x))}
     Scc:
      {app#(add(n, x), y) -> app#(x, y)}
     Scc:
      {            high#(n, add(m, x)) -> if_high#(le(m, n), n, add(m, x)),
        if_high#(true(), n, add(m, x)) -> high#(n, x),
       if_high#(false(), n, add(m, x)) -> high#(n, x)}
     Scc:
      {            low#(n, add(m, x)) -> if_low#(le(m, n), n, add(m, x)),
        if_low#(true(), n, add(m, x)) -> low#(n, x),
       if_low#(false(), n, add(m, x)) -> low#(n, x)}
     Scc:
      {le#(s x, s y) -> le#(x, y)}
     
     SCC (3):
      Strict:
       {if_qs#(false(), x, n, y) -> quicksort# y,
        if_qs#(false(), x, n, y) -> quicksort# x,
                    quicksort# x -> if_qs#(isempty x, low(head x, tail x), head x, high(head x, tail x))}
      Weak:
      {                    le(0(), y) -> true(),
                         le(s x, 0()) -> false(),
                         le(s x, s y) -> le(x, y),
                        app(nil(), y) -> y,
                    app(add(n, x), y) -> add(n, app(x, y)),
                        low(n, nil()) -> nil(),
                    low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x)),
         if_low(true(), n, add(m, x)) -> add(m, low(n, x)),
        if_low(false(), n, add(m, x)) -> low(n, x),
                       high(n, nil()) -> nil(),
                   high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x)),
        if_high(true(), n, add(m, x)) -> high(n, x),
       if_high(false(), n, add(m, x)) -> add(m, high(n, x)),
                       head add(n, x) -> n,
                       tail add(n, x) -> x,
                        isempty nil() -> true(),
                    isempty add(n, x) -> false(),
               if_qs(true(), x, n, y) -> nil(),
              if_qs(false(), x, n, y) -> app(quicksort x, add(n, quicksort y)),
                          quicksort x -> if_qs(isempty x, low(head x, tail x), head x, high(head x, tail x))}
      Open
     
     
     
     
     
     
     SCC (1):
      Strict:
       {app#(add(n, x), y) -> app#(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(add(n, x), y) -> add(n, app(x, y)),
                        low(n, nil()) -> nil(),
                    low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x)),
         if_low(true(), n, add(m, x)) -> add(m, low(n, x)),
        if_low(false(), n, add(m, x)) -> low(n, x),
                       high(n, nil()) -> nil(),
                   high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x)),
        if_high(true(), n, add(m, x)) -> high(n, x),
       if_high(false(), n, add(m, x)) -> add(m, high(n, x)),
                       head add(n, x) -> n,
                       tail add(n, x) -> x,
                        isempty nil() -> true(),
                    isempty add(n, x) -> false(),
               if_qs(true(), x, n, y) -> nil(),
              if_qs(false(), x, n, y) -> app(quicksort x, add(n, quicksort y)),
                          quicksort x -> if_qs(isempty x, low(head x, tail x), head x, high(head x, tail x))}
      Open
     SCC (3):
      Strict:
       {            high#(n, add(m, x)) -> if_high#(le(m, n), n, add(m, x)),
         if_high#(true(), n, add(m, x)) -> high#(n, x),
        if_high#(false(), n, add(m, x)) -> high#(n, x)}
      Weak:
      {                    le(0(), y) -> true(),
                         le(s x, 0()) -> false(),
                         le(s x, s y) -> le(x, y),
                        app(nil(), y) -> y,
                    app(add(n, x), y) -> add(n, app(x, y)),
                        low(n, nil()) -> nil(),
                    low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x)),
         if_low(true(), n, add(m, x)) -> add(m, low(n, x)),
        if_low(false(), n, add(m, x)) -> low(n, x),
                       high(n, nil()) -> nil(),
                   high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x)),
        if_high(true(), n, add(m, x)) -> high(n, x),
       if_high(false(), n, add(m, x)) -> add(m, high(n, x)),
                       head add(n, x) -> n,
                       tail add(n, x) -> x,
                        isempty nil() -> true(),
                    isempty add(n, x) -> false(),
               if_qs(true(), x, n, y) -> nil(),
              if_qs(false(), x, n, y) -> app(quicksort x, add(n, quicksort y)),
                          quicksort x -> if_qs(isempty x, low(head x, tail x), head x, high(head x, tail x))}
      Open
     
     SCC (3):
      Strict:
       {            low#(n, add(m, x)) -> if_low#(le(m, n), n, add(m, x)),
         if_low#(true(), n, add(m, x)) -> low#(n, x),
        if_low#(false(), n, add(m, x)) -> low#(n, x)}
      Weak:
      {                    le(0(), y) -> true(),
                         le(s x, 0()) -> false(),
                         le(s x, s y) -> le(x, y),
                        app(nil(), y) -> y,
                    app(add(n, x), y) -> add(n, app(x, y)),
                        low(n, nil()) -> nil(),
                    low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x)),
         if_low(true(), n, add(m, x)) -> add(m, low(n, x)),
        if_low(false(), n, add(m, x)) -> low(n, x),
                       high(n, nil()) -> nil(),
                   high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x)),
        if_high(true(), n, add(m, x)) -> high(n, x),
       if_high(false(), n, add(m, x)) -> add(m, high(n, x)),
                       head add(n, x) -> n,
                       tail add(n, x) -> x,
                        isempty nil() -> true(),
                    isempty add(n, x) -> false(),
               if_qs(true(), x, n, y) -> nil(),
              if_qs(false(), x, n, y) -> app(quicksort x, add(n, quicksort y)),
                          quicksort x -> if_qs(isempty x, low(head x, tail x), head x, high(head x, tail x))}
      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(add(n, x), y) -> add(n, app(x, y)),
                        low(n, nil()) -> nil(),
                    low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x)),
         if_low(true(), n, add(m, x)) -> add(m, low(n, x)),
        if_low(false(), n, add(m, x)) -> low(n, x),
                       high(n, nil()) -> nil(),
                   high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x)),
        if_high(true(), n, add(m, x)) -> high(n, x),
       if_high(false(), n, add(m, x)) -> add(m, high(n, x)),
                       head add(n, x) -> n,
                       tail add(n, x) -> x,
                        isempty nil() -> true(),
                    isempty add(n, x) -> false(),
               if_qs(true(), x, n, y) -> nil(),
              if_qs(false(), x, n, y) -> app(quicksort x, add(n, quicksort y)),
                          quicksort x -> if_qs(isempty x, low(head x, tail x), head x, high(head x, tail x))}
      Open