MAYBE
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:
  Strict:
   {                       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)}
  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)}
  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))
    (sortIter#(x, y) -> min#(x), min#(cons(n, cons(m, x))) -> if_min#(le(n, m), cons(n, cons(m, x))))
    (sortIter#(x, y) -> min#(x), min#(cons(n, cons(m, x))) -> le#(n, m))
    (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))
    (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)))
    (if_replace#(false(), n, m, cons(k, x)) -> replace#(n, m, x), replace#(n, m, cons(k, x)) -> eq#(n, k))
    (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))
    (replace#(n, m, cons(k, x)) -> eq#(n, k), 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)))
    (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))
    (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()))))}
   SCCS:
    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:
     {            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:
     {eq#(s(n), s(m)) -> eq#(n, m)}
    SCC:
     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)}
     Fail
    SCC:
     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)}
     SPSC:
      Simple Projection:
       pi(if_replace#) = 3, pi(replace#) = 2
      Strict:
       {replace#(n, m, cons(k, x)) -> if_replace#(eq(n, k), n, m, cons(k, x))}
      EDG:
       {}
       SCCS:
        
        Qed
    SCC:
     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)}
     POLY:
      Argument Filtering:
       pi(append) = [], pi(if) = [], pi(sort) = [], pi(sortIter) = [], pi(tail) = [], pi(head) = [], pi(empty) = [], pi(if_replace) = [], pi(replace) = [], pi(if_min#) = 1, pi(if_min) = [], pi(nil) = [], pi(cons) = [1], pi(min#) = 0, pi(min) = [], pi(le) = [], pi(s) = [], pi(false) = [], pi(0) = [], pi(eq) = [], pi(true) = []
      Usable Rules:
       {}
      Interpretation:
       [cons](x0) = x0 + 1
      Strict:
       {min#(cons(n, cons(m, x))) -> if_min#(le(n, m), cons(n, 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)}
      EDG:
       {}
       SCCS:
        
        Qed
    SCC:
     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)}
     SPSC:
      Simple Projection:
       pi(le#) = 0
      Strict:
       {}
      Qed
    SCC:
     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)}
     SPSC:
      Simple Projection:
       pi(eq#) = 0
      Strict:
       {}
      Qed