MAYBE
Time: 0.010784
TRS:
 {                       eq(0(), 0()) -> true(),
                         eq(0(), s Y) -> false(),
                         eq(s X, 0()) -> false(),
                         eq(s X, s Y) -> eq(X, Y),
                           le(0(), Y) -> true(),
                         le(s X, 0()) -> false(),
                         le(s X, s Y) -> le(X, Y),
              min cons(N, cons(M, L)) -> ifmin(le(N, M), cons(N, cons(M, L))),
                 min cons(0(), nil()) -> 0(),
                 min cons(s N, nil()) -> s N,
   ifmin(true(), cons(N, cons(M, L))) -> min cons(N, L),
  ifmin(false(), cons(N, cons(M, L))) -> min cons(M, L),
            replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)),
                 replace(N, M, nil()) -> nil(),
     ifrepl(true(), N, M, cons(K, L)) -> cons(M, L),
    ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)),
                   selsort cons(N, L) -> ifselsort(eq(N, min cons(N, L)), cons(N, L)),
                        selsort nil() -> nil(),
        ifselsort(true(), cons(N, L)) -> cons(N, selsort L),
       ifselsort(false(), cons(N, L)) -> cons(min cons(N, L), selsort replace(min cons(N, L), N, L))}
 DP:
  DP:
   {                       eq#(s X, s Y) -> eq#(X, Y),
                           le#(s X, s Y) -> le#(X, Y),
                min# cons(N, cons(M, L)) -> le#(N, M),
                min# cons(N, cons(M, L)) -> ifmin#(le(N, M), cons(N, cons(M, L))),
     ifmin#(true(), cons(N, cons(M, L))) -> min# cons(N, L),
    ifmin#(false(), cons(N, cons(M, L))) -> min# cons(M, L),
              replace#(N, M, cons(K, L)) -> eq#(N, K),
              replace#(N, M, cons(K, L)) -> ifrepl#(eq(N, K), N, M, cons(K, L)),
      ifrepl#(false(), N, M, cons(K, L)) -> replace#(N, M, L),
                     selsort# cons(N, L) -> eq#(N, min cons(N, L)),
                     selsort# cons(N, L) -> min# cons(N, L),
                     selsort# cons(N, L) -> ifselsort#(eq(N, min cons(N, L)), cons(N, L)),
          ifselsort#(true(), cons(N, L)) -> selsort# L,
         ifselsort#(false(), cons(N, L)) -> min# cons(N, L),
         ifselsort#(false(), cons(N, L)) -> replace#(min cons(N, L), N, L),
         ifselsort#(false(), cons(N, L)) -> selsort# replace(min cons(N, L), N, L)}
  TRS:
  {                       eq(0(), 0()) -> true(),
                          eq(0(), s Y) -> false(),
                          eq(s X, 0()) -> false(),
                          eq(s X, s Y) -> eq(X, Y),
                            le(0(), Y) -> true(),
                          le(s X, 0()) -> false(),
                          le(s X, s Y) -> le(X, Y),
               min cons(N, cons(M, L)) -> ifmin(le(N, M), cons(N, cons(M, L))),
                  min cons(0(), nil()) -> 0(),
                  min cons(s N, nil()) -> s N,
    ifmin(true(), cons(N, cons(M, L))) -> min cons(N, L),
   ifmin(false(), cons(N, cons(M, L))) -> min cons(M, L),
             replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)),
                  replace(N, M, nil()) -> nil(),
      ifrepl(true(), N, M, cons(K, L)) -> cons(M, L),
     ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)),
                    selsort cons(N, L) -> ifselsort(eq(N, min cons(N, L)), cons(N, L)),
                         selsort nil() -> nil(),
         ifselsort(true(), cons(N, L)) -> cons(N, selsort L),
        ifselsort(false(), cons(N, L)) -> cons(min cons(N, L), selsort replace(min cons(N, L), N, L))}
  UR:
   {                       eq(0(), 0()) -> true(),
                           eq(0(), s Y) -> false(),
                           eq(s X, 0()) -> false(),
                           eq(s X, s Y) -> eq(X, Y),
                             le(0(), Y) -> true(),
                           le(s X, 0()) -> false(),
                           le(s X, s Y) -> le(X, Y),
                min cons(N, cons(M, L)) -> ifmin(le(N, M), cons(N, cons(M, L))),
                   min cons(0(), nil()) -> 0(),
                   min cons(s N, nil()) -> s N,
     ifmin(true(), cons(N, cons(M, L))) -> min cons(N, L),
    ifmin(false(), cons(N, cons(M, L))) -> min cons(M, L),
              replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)),
                   replace(N, M, nil()) -> nil(),
       ifrepl(true(), N, M, cons(K, L)) -> cons(M, L),
      ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)),
                                a(x, y) -> x,
                                a(x, y) -> y}
   EDG:
    {(replace#(N, M, cons(K, L)) -> eq#(N, K), eq#(s X, s Y) -> eq#(X, Y))
     (ifmin#(false(), cons(N, cons(M, L))) -> min# cons(M, L), min# cons(N, cons(M, L)) -> ifmin#(le(N, M), cons(N, cons(M, L))))
     (ifmin#(false(), cons(N, cons(M, L))) -> min# cons(M, L), min# cons(N, cons(M, L)) -> le#(N, M))
     (ifselsort#(true(), cons(N, L)) -> selsort# L, selsort# cons(N, L) -> ifselsort#(eq(N, min cons(N, L)), cons(N, L)))
     (ifselsort#(true(), cons(N, L)) -> selsort# L, selsort# cons(N, L) -> min# cons(N, L))
     (ifselsort#(true(), cons(N, L)) -> selsort# L, selsort# cons(N, L) -> eq#(N, min cons(N, L)))
     (ifselsort#(false(), cons(N, L)) -> selsort# replace(min cons(N, L), N, L), selsort# cons(N, L) -> ifselsort#(eq(N, min cons(N, L)), cons(N, L)))
     (ifselsort#(false(), cons(N, L)) -> selsort# replace(min cons(N, L), N, L), selsort# cons(N, L) -> min# cons(N, L))
     (ifselsort#(false(), cons(N, L)) -> selsort# replace(min cons(N, L), N, L), selsort# cons(N, L) -> eq#(N, min cons(N, L)))
     (replace#(N, M, cons(K, L)) -> ifrepl#(eq(N, K), N, M, cons(K, L)), ifrepl#(false(), N, M, cons(K, L)) -> replace#(N, M, L))
     (le#(s X, s Y) -> le#(X, Y), le#(s X, s Y) -> le#(X, Y))
     (selsort# cons(N, L) -> ifselsort#(eq(N, min cons(N, L)), cons(N, L)), ifselsort#(false(), cons(N, L)) -> selsort# replace(min cons(N, L), N, L))
     (selsort# cons(N, L) -> ifselsort#(eq(N, min cons(N, L)), cons(N, L)), ifselsort#(false(), cons(N, L)) -> replace#(min cons(N, L), N, L))
     (selsort# cons(N, L) -> ifselsort#(eq(N, min cons(N, L)), cons(N, L)), ifselsort#(false(), cons(N, L)) -> min# cons(N, L))
     (selsort# cons(N, L) -> ifselsort#(eq(N, min cons(N, L)), cons(N, L)), ifselsort#(true(), cons(N, L)) -> selsort# L)
     (ifselsort#(false(), cons(N, L)) -> replace#(min cons(N, L), N, L), replace#(N, M, cons(K, L)) -> ifrepl#(eq(N, K), N, M, cons(K, L)))
     (ifselsort#(false(), cons(N, L)) -> replace#(min cons(N, L), N, L), replace#(N, M, cons(K, L)) -> eq#(N, K))
     (ifrepl#(false(), N, M, cons(K, L)) -> replace#(N, M, L), replace#(N, M, cons(K, L)) -> eq#(N, K))
     (ifrepl#(false(), N, M, cons(K, L)) -> replace#(N, M, L), replace#(N, M, cons(K, L)) -> ifrepl#(eq(N, K), N, M, cons(K, L)))
     (min# cons(N, cons(M, L)) -> le#(N, M), le#(s X, s Y) -> le#(X, Y))
     (eq#(s X, s Y) -> eq#(X, Y), eq#(s X, s Y) -> eq#(X, Y))
     (selsort# cons(N, L) -> eq#(N, min cons(N, L)), eq#(s X, s Y) -> eq#(X, Y))
     (ifselsort#(false(), cons(N, L)) -> min# cons(N, L), min# cons(N, cons(M, L)) -> le#(N, M))
     (ifselsort#(false(), cons(N, L)) -> min# cons(N, L), min# cons(N, cons(M, L)) -> ifmin#(le(N, M), cons(N, cons(M, L))))
     (selsort# cons(N, L) -> min# cons(N, L), min# cons(N, cons(M, L)) -> le#(N, M))
     (selsort# cons(N, L) -> min# cons(N, L), min# cons(N, cons(M, L)) -> ifmin#(le(N, M), cons(N, cons(M, L))))
     (ifmin#(true(), cons(N, cons(M, L))) -> min# cons(N, L), min# cons(N, cons(M, L)) -> le#(N, M))
     (ifmin#(true(), cons(N, cons(M, L))) -> min# cons(N, L), min# cons(N, cons(M, L)) -> ifmin#(le(N, M), cons(N, cons(M, L))))
     (min# cons(N, cons(M, L)) -> ifmin#(le(N, M), cons(N, cons(M, L))), ifmin#(true(), cons(N, cons(M, L))) -> min# cons(N, L))
     (min# cons(N, cons(M, L)) -> ifmin#(le(N, M), cons(N, cons(M, L))), ifmin#(false(), cons(N, cons(M, L))) -> min# cons(M, L))}
    STATUS:
     arrows: 0.882812
     SCCS (5):
      Scc:
       {            selsort# cons(N, L) -> ifselsort#(eq(N, min cons(N, L)), cons(N, L)),
         ifselsort#(true(), cons(N, L)) -> selsort# L,
        ifselsort#(false(), cons(N, L)) -> selsort# replace(min cons(N, L), N, L)}
      Scc:
       {        replace#(N, M, cons(K, L)) -> ifrepl#(eq(N, K), N, M, cons(K, L)),
        ifrepl#(false(), N, M, cons(K, L)) -> replace#(N, M, L)}
      Scc:
       {eq#(s X, s Y) -> eq#(X, Y)}
      Scc:
       {            min# cons(N, cons(M, L)) -> ifmin#(le(N, M), cons(N, cons(M, L))),
         ifmin#(true(), cons(N, cons(M, L))) -> min# cons(N, L),
        ifmin#(false(), cons(N, cons(M, L))) -> min# cons(M, L)}
      Scc:
       {le#(s X, s Y) -> le#(X, Y)}
      
      SCC (3):
       Strict:
        {            selsort# cons(N, L) -> ifselsort#(eq(N, min cons(N, L)), cons(N, L)),
          ifselsort#(true(), cons(N, L)) -> selsort# L,
         ifselsort#(false(), cons(N, L)) -> selsort# replace(min cons(N, L), N, L)}
       Weak:
       {                       eq(0(), 0()) -> true(),
                               eq(0(), s Y) -> false(),
                               eq(s X, 0()) -> false(),
                               eq(s X, s Y) -> eq(X, Y),
                                 le(0(), Y) -> true(),
                               le(s X, 0()) -> false(),
                               le(s X, s Y) -> le(X, Y),
                    min cons(N, cons(M, L)) -> ifmin(le(N, M), cons(N, cons(M, L))),
                       min cons(0(), nil()) -> 0(),
                       min cons(s N, nil()) -> s N,
         ifmin(true(), cons(N, cons(M, L))) -> min cons(N, L),
        ifmin(false(), cons(N, cons(M, L))) -> min cons(M, L),
                  replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)),
                       replace(N, M, nil()) -> nil(),
           ifrepl(true(), N, M, cons(K, L)) -> cons(M, L),
          ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)),
                         selsort cons(N, L) -> ifselsort(eq(N, min cons(N, L)), cons(N, L)),
                              selsort nil() -> nil(),
              ifselsort(true(), cons(N, L)) -> cons(N, selsort L),
             ifselsort(false(), cons(N, L)) -> cons(min cons(N, L), selsort replace(min cons(N, L), N, L))}
       Open
      
      SCC (2):
       Strict:
        {        replace#(N, M, cons(K, L)) -> ifrepl#(eq(N, K), N, M, cons(K, L)),
         ifrepl#(false(), N, M, cons(K, L)) -> replace#(N, M, L)}
       Weak:
       {                       eq(0(), 0()) -> true(),
                               eq(0(), s Y) -> false(),
                               eq(s X, 0()) -> false(),
                               eq(s X, s Y) -> eq(X, Y),
                                 le(0(), Y) -> true(),
                               le(s X, 0()) -> false(),
                               le(s X, s Y) -> le(X, Y),
                    min cons(N, cons(M, L)) -> ifmin(le(N, M), cons(N, cons(M, L))),
                       min cons(0(), nil()) -> 0(),
                       min cons(s N, nil()) -> s N,
         ifmin(true(), cons(N, cons(M, L))) -> min cons(N, L),
        ifmin(false(), cons(N, cons(M, L))) -> min cons(M, L),
                  replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)),
                       replace(N, M, nil()) -> nil(),
           ifrepl(true(), N, M, cons(K, L)) -> cons(M, L),
          ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)),
                         selsort cons(N, L) -> ifselsort(eq(N, min cons(N, L)), cons(N, L)),
                              selsort nil() -> nil(),
              ifselsort(true(), cons(N, L)) -> cons(N, selsort L),
             ifselsort(false(), cons(N, L)) -> cons(min cons(N, L), selsort replace(min cons(N, L), N, L))}
       Open
      
      
      
      
      SCC (1):
       Strict:
        {eq#(s X, s Y) -> eq#(X, Y)}
       Weak:
       {                       eq(0(), 0()) -> true(),
                               eq(0(), s Y) -> false(),
                               eq(s X, 0()) -> false(),
                               eq(s X, s Y) -> eq(X, Y),
                                 le(0(), Y) -> true(),
                               le(s X, 0()) -> false(),
                               le(s X, s Y) -> le(X, Y),
                    min cons(N, cons(M, L)) -> ifmin(le(N, M), cons(N, cons(M, L))),
                       min cons(0(), nil()) -> 0(),
                       min cons(s N, nil()) -> s N,
         ifmin(true(), cons(N, cons(M, L))) -> min cons(N, L),
        ifmin(false(), cons(N, cons(M, L))) -> min cons(M, L),
                  replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)),
                       replace(N, M, nil()) -> nil(),
           ifrepl(true(), N, M, cons(K, L)) -> cons(M, L),
          ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)),
                         selsort cons(N, L) -> ifselsort(eq(N, min cons(N, L)), cons(N, L)),
                              selsort nil() -> nil(),
              ifselsort(true(), cons(N, L)) -> cons(N, selsort L),
             ifselsort(false(), cons(N, L)) -> cons(min cons(N, L), selsort replace(min cons(N, L), N, L))}
       Open
      SCC (3):
       Strict:
        {            min# cons(N, cons(M, L)) -> ifmin#(le(N, M), cons(N, cons(M, L))),
          ifmin#(true(), cons(N, cons(M, L))) -> min# cons(N, L),
         ifmin#(false(), cons(N, cons(M, L))) -> min# cons(M, L)}
       Weak:
       {                       eq(0(), 0()) -> true(),
                               eq(0(), s Y) -> false(),
                               eq(s X, 0()) -> false(),
                               eq(s X, s Y) -> eq(X, Y),
                                 le(0(), Y) -> true(),
                               le(s X, 0()) -> false(),
                               le(s X, s Y) -> le(X, Y),
                    min cons(N, cons(M, L)) -> ifmin(le(N, M), cons(N, cons(M, L))),
                       min cons(0(), nil()) -> 0(),
                       min cons(s N, nil()) -> s N,
         ifmin(true(), cons(N, cons(M, L))) -> min cons(N, L),
        ifmin(false(), cons(N, cons(M, L))) -> min cons(M, L),
                  replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)),
                       replace(N, M, nil()) -> nil(),
           ifrepl(true(), N, M, cons(K, L)) -> cons(M, L),
          ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)),
                         selsort cons(N, L) -> ifselsort(eq(N, min cons(N, L)), cons(N, L)),
                              selsort nil() -> nil(),
              ifselsort(true(), cons(N, L)) -> cons(N, selsort L),
             ifselsort(false(), cons(N, L)) -> cons(min cons(N, L), selsort replace(min cons(N, L), N, L))}
       Open
      
      SCC (1):
       Strict:
        {le#(s X, s Y) -> le#(X, Y)}
       Weak:
       {                       eq(0(), 0()) -> true(),
                               eq(0(), s Y) -> false(),
                               eq(s X, 0()) -> false(),
                               eq(s X, s Y) -> eq(X, Y),
                                 le(0(), Y) -> true(),
                               le(s X, 0()) -> false(),
                               le(s X, s Y) -> le(X, Y),
                    min cons(N, cons(M, L)) -> ifmin(le(N, M), cons(N, cons(M, L))),
                       min cons(0(), nil()) -> 0(),
                       min cons(s N, nil()) -> s N,
         ifmin(true(), cons(N, cons(M, L))) -> min cons(N, L),
        ifmin(false(), cons(N, cons(M, L))) -> min cons(M, L),
                  replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)),
                       replace(N, M, nil()) -> nil(),
           ifrepl(true(), N, M, cons(K, L)) -> cons(M, L),
          ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)),
                         selsort cons(N, L) -> ifselsort(eq(N, min cons(N, L)), cons(N, L)),
                              selsort nil() -> nil(),
              ifselsort(true(), cons(N, L)) -> cons(N, selsort L),
             ifselsort(false(), cons(N, L)) -> cons(min cons(N, L), selsort replace(min cons(N, L), N, L))}
       Open