MAYBE
Time: 0.010003
TRS:
 {                         eq(0(), 0()) -> true(),
                           eq(0(), s m) -> false(),
                           eq(s n, 0()) -> false(),
                           eq(s n, s m) -> eq(n, m),
                             le(0(), m) -> true(),
                           le(s n, 0()) -> false(),
                           le(s n, s m) -> le(n, m),
                min cons(n, cons(m, x)) -> if_min(le(n, m), cons(n, cons(m, x))),
                     min cons(x, nil()) -> x,
    if_min(true(), cons(n, cons(m, x))) -> min cons(n, x),
   if_min(false(), cons(n, cons(m, x))) -> min cons(m, x),
              replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)),
                   replace(n, m, nil()) -> nil(),
   if_replace(true(), n, m, cons(k, x)) -> cons(m, x),
  if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)),
                       empty cons(n, x) -> false(),
                            empty nil() -> true(),
                        head cons(n, x) -> n,
                        tail cons(n, x) -> x,
                             tail nil() -> nil(),
                         sortIter(x, y) -> if(empty x, x, y, append(y, cons(min x, nil()))),
                                 sort x -> sortIter(x, nil()),
                    if(true(), x, y, z) -> y,
                   if(false(), x, y, z) -> sortIter(replace(min x, head x, tail x), z)}
 DP:
  DP:
   {                         eq#(s n, s m) -> eq#(n, m),
                             le#(s n, s m) -> le#(n, m),
                  min# cons(n, cons(m, x)) -> le#(n, m),
                  min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))),
      if_min#(true(), cons(n, cons(m, x))) -> min# cons(n, x),
     if_min#(false(), cons(n, cons(m, x))) -> min# cons(m, x),
                replace#(n, m, cons(k, x)) -> eq#(n, k),
                replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x)),
    if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x),
                           sortIter#(x, y) -> min# x,
                           sortIter#(x, y) -> empty# x,
                           sortIter#(x, y) -> if#(empty x, x, y, append(y, cons(min x, nil()))),
                                   sort# x -> sortIter#(x, nil()),
                     if#(false(), x, y, z) -> min# x,
                     if#(false(), x, y, z) -> replace#(min x, head x, tail x),
                     if#(false(), x, y, z) -> head# x,
                     if#(false(), x, y, z) -> tail# x,
                     if#(false(), x, y, z) -> sortIter#(replace(min x, head x, tail x), z)}
  TRS:
  {                         eq(0(), 0()) -> true(),
                            eq(0(), s m) -> false(),
                            eq(s n, 0()) -> false(),
                            eq(s n, s m) -> eq(n, m),
                              le(0(), m) -> true(),
                            le(s n, 0()) -> false(),
                            le(s n, s m) -> le(n, m),
                 min cons(n, cons(m, x)) -> if_min(le(n, m), cons(n, cons(m, x))),
                      min cons(x, nil()) -> x,
     if_min(true(), cons(n, cons(m, x))) -> min cons(n, x),
    if_min(false(), cons(n, cons(m, x))) -> min cons(m, x),
               replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)),
                    replace(n, m, nil()) -> nil(),
    if_replace(true(), n, m, cons(k, x)) -> cons(m, x),
   if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)),
                        empty cons(n, x) -> false(),
                             empty nil() -> true(),
                         head cons(n, x) -> n,
                         tail cons(n, x) -> x,
                              tail nil() -> nil(),
                          sortIter(x, y) -> if(empty x, x, y, append(y, cons(min x, nil()))),
                                  sort x -> sortIter(x, nil()),
                     if(true(), x, y, z) -> y,
                    if(false(), x, y, z) -> sortIter(replace(min x, head x, tail x), z)}
  UR:
   {                         eq(0(), 0()) -> true(),
                             eq(0(), s m) -> false(),
                             eq(s n, 0()) -> false(),
                             eq(s n, s m) -> eq(n, m),
                               le(0(), m) -> true(),
                             le(s n, 0()) -> false(),
                             le(s n, s m) -> le(n, m),
                  min cons(n, cons(m, x)) -> if_min(le(n, m), cons(n, cons(m, x))),
                       min cons(x, nil()) -> x,
      if_min(true(), cons(n, cons(m, x))) -> min cons(n, x),
     if_min(false(), cons(n, cons(m, x))) -> min cons(m, x),
                replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)),
                     replace(n, m, nil()) -> nil(),
     if_replace(true(), n, m, cons(k, x)) -> cons(m, x),
    if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)),
                         empty cons(n, x) -> false(),
                              empty nil() -> true(),
                          head cons(n, x) -> n,
                          tail cons(n, x) -> x,
                               tail nil() -> nil(),
                                  a(w, v) -> w,
                                  a(w, v) -> v}
   EDG:
    {(replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x)), if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x))
     (if#(false(), x, y, z) -> min# x, min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))))
     (if#(false(), x, y, z) -> min# x, min# cons(n, cons(m, x)) -> le#(n, m))
     (sort# x -> sortIter#(x, nil()), sortIter#(x, y) -> if#(empty x, x, y, append(y, cons(min x, nil()))))
     (sort# x -> sortIter#(x, nil()), sortIter#(x, y) -> empty# x)
     (sort# x -> sortIter#(x, nil()), sortIter#(x, y) -> min# x)
     (replace#(n, m, cons(k, x)) -> eq#(n, k), eq#(s n, s m) -> eq#(n, m))
     (le#(s n, s m) -> le#(n, m), le#(s n, s m) -> le#(n, m))
     (min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))), if_min#(false(), cons(n, cons(m, x))) -> min# cons(m, x))
     (min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))), if_min#(true(), cons(n, cons(m, x))) -> min# cons(n, x))
     (if_min#(false(), cons(n, cons(m, x))) -> min# cons(m, x), min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))))
     (if_min#(false(), cons(n, cons(m, x))) -> min# cons(m, x), min# cons(n, cons(m, x)) -> le#(n, m))
     (if_min#(true(), cons(n, cons(m, x))) -> min# cons(n, x), min# cons(n, cons(m, x)) -> le#(n, m))
     (if_min#(true(), cons(n, cons(m, x))) -> min# cons(n, x), min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))))
     (min# cons(n, cons(m, x)) -> le#(n, m), le#(s n, s m) -> le#(n, m))
     (eq#(s n, s m) -> eq#(n, m), eq#(s n, s m) -> eq#(n, m))
     (if#(false(), x, y, z) -> replace#(min x, head x, tail x), replace#(n, m, cons(k, x)) -> eq#(n, k))
     (if#(false(), x, y, z) -> replace#(min x, head x, tail x), replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x)))
     (if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x), replace#(n, m, cons(k, x)) -> eq#(n, k))
     (if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x), replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x)))
     (sortIter#(x, y) -> if#(empty x, x, y, append(y, cons(min x, nil()))), if#(false(), x, y, z) -> min# x)
     (sortIter#(x, y) -> if#(empty x, x, y, append(y, cons(min x, nil()))), if#(false(), x, y, z) -> replace#(min x, head x, tail x))
     (sortIter#(x, y) -> if#(empty x, x, y, append(y, cons(min x, nil()))), if#(false(), x, y, z) -> head# x)
     (sortIter#(x, y) -> if#(empty x, x, y, append(y, cons(min x, nil()))), if#(false(), x, y, z) -> tail# x)
     (sortIter#(x, y) -> if#(empty x, x, y, append(y, cons(min x, nil()))), if#(false(), x, y, z) -> sortIter#(replace(min x, head x, tail x), z))
     (sortIter#(x, y) -> min# x, min# cons(n, cons(m, x)) -> le#(n, m))
     (sortIter#(x, y) -> min# x, min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))))
     (if#(false(), x, y, z) -> sortIter#(replace(min x, head x, tail x), z), sortIter#(x, y) -> min# x)
     (if#(false(), x, y, z) -> sortIter#(replace(min x, head x, tail x), z), sortIter#(x, y) -> empty# x)
     (if#(false(), x, y, z) -> sortIter#(replace(min x, head x, tail x), z), sortIter#(x, y) -> if#(empty x, x, y, append(y, cons(min x, nil()))))}
    STATUS:
     arrows: 0.907407
     SCCS (5):
      Scc:
       {      sortIter#(x, y) -> if#(empty x, x, y, append(y, cons(min x, nil()))),
        if#(false(), x, y, z) -> sortIter#(replace(min x, head x, tail x), z)}
      Scc:
       {            replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x)),
        if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x)}
      Scc:
       {eq#(s n, s m) -> eq#(n, m)}
      Scc:
       {             min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))),
         if_min#(true(), cons(n, cons(m, x))) -> min# cons(n, x),
        if_min#(false(), cons(n, cons(m, x))) -> min# cons(m, x)}
      Scc:
       {le#(s n, s m) -> le#(n, m)}
      
      
      SCC (2):
       Strict:
        {      sortIter#(x, y) -> if#(empty x, x, y, append(y, cons(min x, nil()))),
         if#(false(), x, y, z) -> sortIter#(replace(min x, head x, tail x), z)}
       Weak:
       {                         eq(0(), 0()) -> true(),
                                 eq(0(), s m) -> false(),
                                 eq(s n, 0()) -> false(),
                                 eq(s n, s m) -> eq(n, m),
                                   le(0(), m) -> true(),
                                 le(s n, 0()) -> false(),
                                 le(s n, s m) -> le(n, m),
                      min cons(n, cons(m, x)) -> if_min(le(n, m), cons(n, cons(m, x))),
                           min cons(x, nil()) -> x,
          if_min(true(), cons(n, cons(m, x))) -> min cons(n, x),
         if_min(false(), cons(n, cons(m, x))) -> min cons(m, x),
                    replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)),
                         replace(n, m, nil()) -> nil(),
         if_replace(true(), n, m, cons(k, x)) -> cons(m, x),
        if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)),
                             empty cons(n, x) -> false(),
                                  empty nil() -> true(),
                              head cons(n, x) -> n,
                              tail cons(n, x) -> x,
                                   tail nil() -> nil(),
                               sortIter(x, y) -> if(empty x, x, y, append(y, cons(min x, nil()))),
                                       sort x -> sortIter(x, nil()),
                          if(true(), x, y, z) -> y,
                         if(false(), x, y, z) -> sortIter(replace(min x, head x, tail x), z)}
       Open
      
      
      
      SCC (2):
       Strict:
        {            replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x)),
         if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x)}
       Weak:
       {                         eq(0(), 0()) -> true(),
                                 eq(0(), s m) -> false(),
                                 eq(s n, 0()) -> false(),
                                 eq(s n, s m) -> eq(n, m),
                                   le(0(), m) -> true(),
                                 le(s n, 0()) -> false(),
                                 le(s n, s m) -> le(n, m),
                      min cons(n, cons(m, x)) -> if_min(le(n, m), cons(n, cons(m, x))),
                           min cons(x, nil()) -> x,
          if_min(true(), cons(n, cons(m, x))) -> min cons(n, x),
         if_min(false(), cons(n, cons(m, x))) -> min cons(m, x),
                    replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)),
                         replace(n, m, nil()) -> nil(),
         if_replace(true(), n, m, cons(k, x)) -> cons(m, x),
        if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)),
                             empty cons(n, x) -> false(),
                                  empty nil() -> true(),
                              head cons(n, x) -> n,
                              tail cons(n, x) -> x,
                                   tail nil() -> nil(),
                               sortIter(x, y) -> if(empty x, x, y, append(y, cons(min x, nil()))),
                                       sort x -> sortIter(x, nil()),
                          if(true(), x, y, z) -> y,
                         if(false(), x, y, z) -> sortIter(replace(min x, head x, tail x), z)}
       Open
      
      SCC (1):
       Strict:
        {eq#(s n, s m) -> eq#(n, m)}
       Weak:
       {                         eq(0(), 0()) -> true(),
                                 eq(0(), s m) -> false(),
                                 eq(s n, 0()) -> false(),
                                 eq(s n, s m) -> eq(n, m),
                                   le(0(), m) -> true(),
                                 le(s n, 0()) -> false(),
                                 le(s n, s m) -> le(n, m),
                      min cons(n, cons(m, x)) -> if_min(le(n, m), cons(n, cons(m, x))),
                           min cons(x, nil()) -> x,
          if_min(true(), cons(n, cons(m, x))) -> min cons(n, x),
         if_min(false(), cons(n, cons(m, x))) -> min cons(m, x),
                    replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)),
                         replace(n, m, nil()) -> nil(),
         if_replace(true(), n, m, cons(k, x)) -> cons(m, x),
        if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)),
                             empty cons(n, x) -> false(),
                                  empty nil() -> true(),
                              head cons(n, x) -> n,
                              tail cons(n, x) -> x,
                                   tail nil() -> nil(),
                               sortIter(x, y) -> if(empty x, x, y, append(y, cons(min x, nil()))),
                                       sort x -> sortIter(x, nil()),
                          if(true(), x, y, z) -> y,
                         if(false(), x, y, z) -> sortIter(replace(min x, head x, tail x), z)}
       Open
      
      
      
      SCC (3):
       Strict:
        {             min# cons(n, cons(m, x)) -> if_min#(le(n, m), cons(n, cons(m, x))),
          if_min#(true(), cons(n, cons(m, x))) -> min# cons(n, x),
         if_min#(false(), cons(n, cons(m, x))) -> min# cons(m, x)}
       Weak:
       {                         eq(0(), 0()) -> true(),
                                 eq(0(), s m) -> false(),
                                 eq(s n, 0()) -> false(),
                                 eq(s n, s m) -> eq(n, m),
                                   le(0(), m) -> true(),
                                 le(s n, 0()) -> false(),
                                 le(s n, s m) -> le(n, m),
                      min cons(n, cons(m, x)) -> if_min(le(n, m), cons(n, cons(m, x))),
                           min cons(x, nil()) -> x,
          if_min(true(), cons(n, cons(m, x))) -> min cons(n, x),
         if_min(false(), cons(n, cons(m, x))) -> min cons(m, x),
                    replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)),
                         replace(n, m, nil()) -> nil(),
         if_replace(true(), n, m, cons(k, x)) -> cons(m, x),
        if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)),
                             empty cons(n, x) -> false(),
                                  empty nil() -> true(),
                              head cons(n, x) -> n,
                              tail cons(n, x) -> x,
                                   tail nil() -> nil(),
                               sortIter(x, y) -> if(empty x, x, y, append(y, cons(min x, nil()))),
                                       sort x -> sortIter(x, nil()),
                          if(true(), x, y, z) -> y,
                         if(false(), x, y, z) -> sortIter(replace(min x, head x, tail x), z)}
       Open
      
      SCC (1):
       Strict:
        {le#(s n, s m) -> le#(n, m)}
       Weak:
       {                         eq(0(), 0()) -> true(),
                                 eq(0(), s m) -> false(),
                                 eq(s n, 0()) -> false(),
                                 eq(s n, s m) -> eq(n, m),
                                   le(0(), m) -> true(),
                                 le(s n, 0()) -> false(),
                                 le(s n, s m) -> le(n, m),
                      min cons(n, cons(m, x)) -> if_min(le(n, m), cons(n, cons(m, x))),
                           min cons(x, nil()) -> x,
          if_min(true(), cons(n, cons(m, x))) -> min cons(n, x),
         if_min(false(), cons(n, cons(m, x))) -> min cons(m, x),
                    replace(n, m, cons(k, x)) -> if_replace(eq(n, k), n, m, cons(k, x)),
                         replace(n, m, nil()) -> nil(),
         if_replace(true(), n, m, cons(k, x)) -> cons(m, x),
        if_replace(false(), n, m, cons(k, x)) -> cons(k, replace(n, m, x)),
                             empty cons(n, x) -> false(),
                                  empty nil() -> true(),
                              head cons(n, x) -> n,
                              tail cons(n, x) -> x,
                                   tail nil() -> nil(),
                               sortIter(x, y) -> if(empty x, x, y, append(y, cons(min x, nil()))),
                                       sort x -> sortIter(x, nil()),
                          if(true(), x, y, z) -> y,
                         if(false(), x, y, z) -> sortIter(replace(min x, head x, tail x), z)}
       Open