MAYBE
Time: 0.004431
TRS:
 {                 minus(x, 0()) -> x,
                 minus(s x, s y) -> minus(x, y),
                  quot(0(), s y) -> 0(),
                  quot(s x, s y) -> s quot(minus(x, y), s y),
                      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)),
                 quicksort nil() -> nil(),
             quicksort add(n, x) -> app(quicksort low(n, x), add(n, quicksort high(n, x)))}
 DP:
  DP:
   {               minus#(s x, s y) -> minus#(x, y),
                    quot#(s x, s y) -> minus#(x, y),
                    quot#(s x, s y) -> quot#(minus(x, y), s y),
                      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),
               quicksort# add(n, x) -> app#(quicksort low(n, x), add(n, quicksort high(n, x))),
               quicksort# add(n, x) -> low#(n, x),
               quicksort# add(n, x) -> high#(n, x),
               quicksort# add(n, x) -> quicksort# low(n, x),
               quicksort# add(n, x) -> quicksort# high(n, x)}
  TRS:
  {                 minus(x, 0()) -> x,
                  minus(s x, s y) -> minus(x, y),
                   quot(0(), s y) -> 0(),
                   quot(s x, s y) -> s quot(minus(x, y), s y),
                       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)),
                  quicksort nil() -> nil(),
              quicksort add(n, x) -> app(quicksort low(n, x), add(n, quicksort high(n, x)))}
  UR:
   {                 minus(x, 0()) -> x,
                   minus(s x, s y) -> minus(x, y),
                        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)),
                   quicksort nil() -> nil(),
               quicksort add(n, x) -> app(quicksort low(n, x), add(n, quicksort high(n, x))),
                           a(z, w) -> z,
                           a(z, w) -> w}
   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))
     (low#(n, add(m, x)) -> le#(m, n), le#(s x, s y) -> le#(x, y))
     (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
     (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y))
     (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))
     (quicksort# add(n, x) -> low#(n, x), low#(n, add(m, x)) -> if_low#(le(m, n), n, add(m, x)))
     (quicksort# add(n, x) -> low#(n, x), low#(n, add(m, x)) -> le#(m, n))
     (quicksort# add(n, x) -> app#(quicksort low(n, x), add(n, quicksort high(n, x))), app#(add(n, x), y) -> app#(x, y))
     (quicksort# add(n, x) -> quicksort# high(n, x), quicksort# add(n, x) -> quicksort# high(n, x))
     (quicksort# add(n, x) -> quicksort# high(n, x), quicksort# add(n, x) -> quicksort# low(n, x))
     (quicksort# add(n, x) -> quicksort# high(n, x), quicksort# add(n, x) -> high#(n, x))
     (quicksort# add(n, x) -> quicksort# high(n, x), quicksort# add(n, x) -> low#(n, x))
     (quicksort# add(n, x) -> quicksort# high(n, x), quicksort# add(n, x) -> app#(quicksort low(n, x), add(n, quicksort high(n, x))))
     (quicksort# add(n, x) -> quicksort# low(n, x), quicksort# add(n, x) -> app#(quicksort low(n, x), add(n, quicksort high(n, x))))
     (quicksort# add(n, x) -> quicksort# low(n, x), quicksort# add(n, x) -> low#(n, x))
     (quicksort# add(n, x) -> quicksort# low(n, x), quicksort# add(n, x) -> high#(n, x))
     (quicksort# add(n, x) -> quicksort# low(n, x), quicksort# add(n, x) -> quicksort# low(n, x))
     (quicksort# add(n, x) -> quicksort# low(n, x), quicksort# add(n, x) -> quicksort# high(n, x))
     (quicksort# add(n, x) -> high#(n, x), high#(n, add(m, x)) -> le#(m, n))
     (quicksort# add(n, x) -> high#(n, x), 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)) -> 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)))
     (app#(add(n, x), y) -> app#(x, y), app#(add(n, x), y) -> app#(x, y))
     (quot#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))
     (high#(n, add(m, x)) -> le#(m, n), le#(s x, s y) -> le#(x, y))
     (quot#(s x, s y) -> quot#(minus(x, y), s y), quot#(s x, s y) -> minus#(x, y))
     (quot#(s x, s y) -> quot#(minus(x, y), s y), quot#(s x, s y) -> quot#(minus(x, y), s 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.891975
     SCCS (7):
      Scc:
       {quicksort# add(n, x) -> quicksort# low(n, x),
        quicksort# add(n, x) -> quicksort# high(n, x)}
      Scc:
       {app#(add(n, x), y) -> app#(x, y)}
      Scc:
       {quot#(s x, s y) -> quot#(minus(x, y), s y)}
      Scc:
       {minus#(s x, s y) -> minus#(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 (2):
       Strict:
        {quicksort# add(n, x) -> quicksort# low(n, x),
         quicksort# add(n, x) -> quicksort# high(n, x)}
       Weak:
       {                 minus(x, 0()) -> x,
                       minus(s x, s y) -> minus(x, y),
                        quot(0(), s y) -> 0(),
                        quot(s x, s y) -> s quot(minus(x, y), s y),
                            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)),
                       quicksort nil() -> nil(),
                   quicksort add(n, x) -> app(quicksort low(n, x), add(n, quicksort high(n, x)))}
       Open
      
      
      
      SCC (1):
       Strict:
        {app#(add(n, x), y) -> app#(x, y)}
       Weak:
       {                 minus(x, 0()) -> x,
                       minus(s x, s y) -> minus(x, y),
                        quot(0(), s y) -> 0(),
                        quot(s x, s y) -> s quot(minus(x, y), s y),
                            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)),
                       quicksort nil() -> nil(),
                   quicksort add(n, x) -> app(quicksort low(n, x), add(n, quicksort high(n, x)))}
       Open
      SCC (1):
       Strict:
        {quot#(s x, s y) -> quot#(minus(x, y), s y)}
       Weak:
       {                 minus(x, 0()) -> x,
                       minus(s x, s y) -> minus(x, y),
                        quot(0(), s y) -> 0(),
                        quot(s x, s y) -> s quot(minus(x, y), s y),
                            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)),
                       quicksort nil() -> nil(),
                   quicksort add(n, x) -> app(quicksort low(n, x), add(n, quicksort high(n, x)))}
       Open
      
      SCC (1):
       Strict:
        {minus#(s x, s y) -> minus#(x, y)}
       Weak:
       {                 minus(x, 0()) -> x,
                       minus(s x, s y) -> minus(x, y),
                        quot(0(), s y) -> 0(),
                        quot(s x, s y) -> s quot(minus(x, y), s y),
                            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)),
                       quicksort nil() -> nil(),
                   quicksort add(n, x) -> app(quicksort low(n, x), add(n, quicksort high(n, 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:
       {                 minus(x, 0()) -> x,
                       minus(s x, s y) -> minus(x, y),
                        quot(0(), s y) -> 0(),
                        quot(s x, s y) -> s quot(minus(x, y), s y),
                            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)),
                       quicksort nil() -> nil(),
                   quicksort add(n, x) -> app(quicksort low(n, x), add(n, quicksort high(n, 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:
       {                 minus(x, 0()) -> x,
                       minus(s x, s y) -> minus(x, y),
                        quot(0(), s y) -> 0(),
                        quot(s x, s y) -> s quot(minus(x, y), s y),
                            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)),
                       quicksort nil() -> nil(),
                   quicksort add(n, x) -> app(quicksort low(n, x), add(n, quicksort high(n, x)))}
       Open
      
      SCC (1):
       Strict:
        {le#(s x, s y) -> le#(x, y)}
       Weak:
       {                 minus(x, 0()) -> x,
                       minus(s x, s y) -> minus(x, y),
                        quot(0(), s y) -> 0(),
                        quot(s x, s y) -> s quot(minus(x, y), s y),
                            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)),
                       quicksort nil() -> nil(),
                   quicksort add(n, x) -> app(quicksort low(n, x), add(n, quicksort high(n, x)))}
       Open