YES
Time: 0.156820
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))}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [ifrepl](x0, x1, x2, x3) = x0,
         
         [replace](x0, x1, x2) = x0,
         
         [eq](x0, x1) = 0,
         
         [le](x0, x1) = x0 + 1,
         
         [cons](x0, x1) = x0 + 1,
         
         [ifmin](x0, x1) = x0 + x1 + 1,
         
         [ifselsort](x0, x1) = 0,
         
         [s](x0) = 1,
         
         [min](x0) = 0,
         
         [selsort](x0) = 0,
         
         [true] = 0,
         
         [0] = 0,
         
         [false] = 0,
         
         [nil] = 1,
         
         [ifselsort#](x0, x1) = x0,
         
         [selsort#](x0) = x0 + 1
        Strict:
         ifselsort#(false(), cons(N, L)) -> selsort# replace(min cons(N, L), N, L)
         1 + 0N + 1L >= 1 + 0N + 1L
         ifselsort#(true(), cons(N, L)) -> selsort# L
         1 + 0N + 1L >= 1 + 1L
         selsort# cons(N, L) -> ifselsort#(eq(N, min cons(N, L)), cons(N, L))
         2 + 0N + 1L >= 1 + 0N + 1L
        Weak:
         ifselsort(false(), cons(N, L)) -> cons(min cons(N, L), selsort replace(min cons(N, L), N, L))
         0 + 0N + 0L >= 1 + 0N + 0L
         ifselsort(true(), cons(N, L)) -> cons(N, selsort L)
         0 + 0N + 0L >= 1 + 0N + 0L
         selsort nil() -> nil()
         0 >= 1
         selsort cons(N, L) -> ifselsort(eq(N, min cons(N, L)), cons(N, L))
         0 + 0N + 0L >= 0 + 0N + 0L
         ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L))
         1 + 0N + 0M + 1L + 0K >= 1 + 0N + 0M + 1L + 0K
         ifrepl(true(), N, M, cons(K, L)) -> cons(M, L)
         1 + 0N + 0M + 1L + 0K >= 1 + 0M + 1L
         replace(N, M, nil()) -> nil()
         1 + 0N + 0M >= 1
         replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L))
         1 + 0N + 0M + 1L + 0K >= 1 + 0N + 0M + 1L + 0K
         ifmin(false(), cons(N, cons(M, L))) -> min cons(M, L)
         3 + 0N + 0M + 1L >= 0 + 0M + 0L
         ifmin(true(), cons(N, cons(M, L))) -> min cons(N, L)
         3 + 0N + 0M + 1L >= 0 + 0N + 0L
         min cons(s N, nil()) -> s N
         0 + 0N >= 1 + 0N
         min cons(0(), nil()) -> 0()
         0 >= 0
         min cons(N, cons(M, L)) -> ifmin(le(N, M), cons(N, cons(M, L)))
         0 + 0N + 0M + 0L >= 4 + 0N + 1M + 1L
         le(s X, s Y) -> le(X, Y)
         2 + 0Y + 0X >= 1 + 1Y + 0X
         le(s X, 0()) -> false()
         1 + 0X >= 0
         le(0(), Y) -> true()
         1 + 1Y >= 0
         eq(s X, s Y) -> eq(X, Y)
         0 + 0Y + 0X >= 0 + 0Y + 0X
         eq(s X, 0()) -> false()
         0 + 0X >= 0
         eq(0(), s Y) -> false()
         0 + 0Y >= 0
         eq(0(), 0()) -> true()
         0 >= 0
       SCCS (0):
        
        
        
     
     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))}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [ifrepl](x0, x1, x2, x3) = x0 + x1,
        
        [replace](x0, x1, x2) = x0 + 1,
        
        [eq](x0, x1) = x0 + x1,
        
        [le](x0, x1) = 0,
        
        [cons](x0, x1) = x0 + 1,
        
        [ifmin](x0, x1) = 0,
        
        [ifselsort](x0, x1) = x0 + 1,
        
        [s](x0) = 0,
        
        [min](x0) = x0,
        
        [selsort](x0) = x0 + 1,
        
        [true] = 0,
        
        [0] = 0,
        
        [false] = 0,
        
        [nil] = 1,
        
        [ifrepl#](x0, x1, x2, x3) = x0 + 1,
        
        [replace#](x0, x1, x2) = x0 + 1
       Strict:
        ifrepl#(false(), N, M, cons(K, L)) -> replace#(N, M, L)
        2 + 0N + 0M + 1L + 0K >= 1 + 0N + 0M + 1L
        replace#(N, M, cons(K, L)) -> ifrepl#(eq(N, K), N, M, cons(K, L))
        2 + 0N + 0M + 1L + 0K >= 2 + 0N + 0M + 1L + 0K
       Weak:
        ifselsort(false(), cons(N, L)) -> cons(min cons(N, L), selsort replace(min cons(N, L), N, L))
        1 + 0N + 0L >= 3 + 0N + 1L
        ifselsort(true(), cons(N, L)) -> cons(N, selsort L)
        1 + 0N + 0L >= 2 + 0N + 1L
        selsort nil() -> nil()
        2 >= 1
        selsort cons(N, L) -> ifselsort(eq(N, min cons(N, L)), cons(N, L))
        2 + 0N + 1L >= 2 + 1N + 1L
        ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L))
        0 + 1N + 0M + 0L + 0K >= 2 + 0N + 0M + 1L + 0K
        ifrepl(true(), N, M, cons(K, L)) -> cons(M, L)
        0 + 1N + 0M + 0L + 0K >= 1 + 0M + 1L
        replace(N, M, nil()) -> nil()
        2 + 0N + 0M >= 1
        replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L))
        2 + 0N + 0M + 1L + 0K >= 0 + 2N + 0M + 0L + 1K
        ifmin(false(), cons(N, cons(M, L))) -> min cons(M, L)
        0 + 0N + 0M + 0L >= 1 + 0M + 1L
        ifmin(true(), cons(N, cons(M, L))) -> min cons(N, L)
        0 + 0N + 0M + 0L >= 1 + 0N + 1L
        min cons(s N, nil()) -> s N
        2 + 0N >= 0 + 0N
        min cons(0(), nil()) -> 0()
        2 >= 0
        min cons(N, cons(M, L)) -> ifmin(le(N, M), cons(N, cons(M, L)))
        2 + 0N + 0M + 1L >= 0 + 0N + 0M + 0L
        le(s X, s Y) -> le(X, Y)
        0 + 0Y + 0X >= 0 + 0Y + 0X
        le(s X, 0()) -> false()
        0 + 0X >= 0
        le(0(), Y) -> true()
        0 + 0Y >= 0
        eq(s X, s Y) -> eq(X, Y)
        0 + 0Y + 0X >= 0 + 1Y + 1X
        eq(s X, 0()) -> false()
        0 + 0X >= 0
        eq(0(), s Y) -> false()
        0 + 0Y >= 0
        eq(0(), 0()) -> true()
        0 >= 0
      SCCS (0):
       
       
     
     
     
     
     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))}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [ifrepl](x0, x1, x2, x3) = 0,
        
        [replace](x0, x1, x2) = x0 + 1,
        
        [eq](x0, x1) = x0 + 1,
        
        [le](x0, x1) = x0 + 1,
        
        [cons](x0, x1) = x0 + x1 + 1,
        
        [ifmin](x0, x1) = x0 + x1 + 1,
        
        [ifselsort](x0, x1) = x0 + 1,
        
        [s](x0) = x0 + 1,
        
        [min](x0) = 0,
        
        [selsort](x0) = 0,
        
        [true] = 1,
        
        [0] = 1,
        
        [false] = 1,
        
        [nil] = 0,
        
        [eq#](x0, x1) = x0 + 1
       Strict:
        eq#(s X, s Y) -> eq#(X, Y)
        2 + 0Y + 1X >= 1 + 0Y + 1X
       Weak:
        ifselsort(false(), cons(N, L)) -> cons(min cons(N, L), selsort replace(min cons(N, L), N, L))
        2 + 0N + 0L >= 1 + 0N + 0L
        ifselsort(true(), cons(N, L)) -> cons(N, selsort L)
        2 + 0N + 0L >= 1 + 1N + 0L
        selsort nil() -> nil()
        0 >= 0
        selsort cons(N, L) -> ifselsort(eq(N, min cons(N, L)), cons(N, L))
        0 + 0N + 0L >= 2 + 1N + 0L
        ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L))
        0 + 0N + 0M + 0L + 0K >= 2 + 0N + 0M + 1L + 1K
        ifrepl(true(), N, M, cons(K, L)) -> cons(M, L)
        0 + 0N + 0M + 0L + 0K >= 1 + 1M + 1L
        replace(N, M, nil()) -> nil()
        1 + 0N + 0M >= 0
        replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L))
        2 + 0N + 0M + 1L + 1K >= 0 + 0N + 0M + 0L + 0K
        ifmin(false(), cons(N, cons(M, L))) -> min cons(M, L)
        4 + 1N + 1M + 1L >= 0 + 0M + 0L
        ifmin(true(), cons(N, cons(M, L))) -> min cons(N, L)
        4 + 1N + 1M + 1L >= 0 + 0N + 0L
        min cons(s N, nil()) -> s N
        0 + 0N >= 1 + 1N
        min cons(0(), nil()) -> 0()
        0 >= 1
        min cons(N, cons(M, L)) -> ifmin(le(N, M), cons(N, cons(M, L)))
        0 + 0N + 0M + 0L >= 4 + 2N + 1M + 1L
        le(s X, s Y) -> le(X, Y)
        2 + 0Y + 1X >= 1 + 0Y + 1X
        le(s X, 0()) -> false()
        2 + 1X >= 1
        le(0(), Y) -> true()
        2 + 0Y >= 1
        eq(s X, s Y) -> eq(X, Y)
        2 + 0Y + 1X >= 1 + 0Y + 1X
        eq(s X, 0()) -> false()
        2 + 1X >= 1
        eq(0(), s Y) -> false()
        2 + 0Y >= 1
        eq(0(), 0()) -> true()
        2 >= 1
      Qed
    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))}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [ifrepl](x0, x1, x2, x3) = 0,
       
       [replace](x0, x1, x2) = x0 + 1,
       
       [eq](x0, x1) = x0 + 1,
       
       [le](x0, x1) = 0,
       
       [cons](x0, x1) = x0 + 1,
       
       [ifmin](x0, x1) = 0,
       
       [ifselsort](x0, x1) = x0 + 1,
       
       [s](x0) = 1,
       
       [min](x0) = x0 + 1,
       
       [selsort](x0) = x0 + 1,
       
       [true] = 0,
       
       [0] = 1,
       
       [false] = 0,
       
       [nil] = 0,
       
       [ifmin#](x0, x1) = x0,
       
       [min#](x0) = x0
      Strict:
       ifmin#(false(), cons(N, cons(M, L))) -> min# cons(M, L)
       2 + 0N + 0M + 1L >= 1 + 0M + 1L
       ifmin#(true(), cons(N, cons(M, L))) -> min# cons(N, L)
       2 + 0N + 0M + 1L >= 1 + 0N + 1L
       min# cons(N, cons(M, L)) -> ifmin#(le(N, M), cons(N, cons(M, L)))
       2 + 0N + 0M + 1L >= 2 + 0N + 0M + 1L
      Weak:
       ifselsort(false(), cons(N, L)) -> cons(min cons(N, L), selsort replace(min cons(N, L), N, L))
       2 + 0N + 1L >= 3 + 0N + 1L
       ifselsort(true(), cons(N, L)) -> cons(N, selsort L)
       2 + 0N + 1L >= 2 + 0N + 1L
       selsort nil() -> nil()
       1 >= 0
       selsort cons(N, L) -> ifselsort(eq(N, min cons(N, L)), cons(N, L))
       2 + 0N + 1L >= 2 + 0N + 1L
       ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L))
       0 + 0N + 0M + 0L + 0K >= 2 + 0N + 0M + 1L + 0K
       ifrepl(true(), N, M, cons(K, L)) -> cons(M, L)
       0 + 0N + 0M + 0L + 0K >= 1 + 0M + 1L
       replace(N, M, nil()) -> nil()
       1 + 0N + 0M >= 0
       replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L))
       2 + 0N + 0M + 1L + 0K >= 0 + 0N + 0M + 0L + 0K
       ifmin(false(), cons(N, cons(M, L))) -> min cons(M, L)
       0 + 0N + 0M + 0L >= 2 + 0M + 1L
       ifmin(true(), cons(N, cons(M, L))) -> min cons(N, L)
       0 + 0N + 0M + 0L >= 2 + 0N + 1L
       min cons(s N, nil()) -> s N
       2 + 0N >= 1 + 0N
       min cons(0(), nil()) -> 0()
       2 >= 1
       min cons(N, cons(M, L)) -> ifmin(le(N, M), cons(N, cons(M, L)))
       3 + 0N + 0M + 1L >= 0 + 0N + 0M + 0L
       le(s X, s Y) -> le(X, Y)
       0 + 0Y + 0X >= 0 + 0Y + 0X
       le(s X, 0()) -> false()
       0 + 0X >= 0
       le(0(), Y) -> true()
       0 + 0Y >= 0
       eq(s X, s Y) -> eq(X, Y)
       2 + 0Y + 0X >= 1 + 0Y + 1X
       eq(s X, 0()) -> false()
       2 + 0X >= 0
       eq(0(), s Y) -> false()
       2 + 0Y >= 0
       eq(0(), 0()) -> true()
       2 >= 0
     SCCS (0):
      
      
    
    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))}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [ifrepl](x0, x1, x2, x3) = 0,
       
       [replace](x0, x1, x2) = x0 + 1,
       
       [eq](x0, x1) = x0 + 1,
       
       [le](x0, x1) = x0 + 1,
       
       [cons](x0, x1) = x0 + x1 + 1,
       
       [ifmin](x0, x1) = x0 + x1 + 1,
       
       [ifselsort](x0, x1) = x0 + 1,
       
       [s](x0) = x0 + 1,
       
       [min](x0) = 0,
       
       [selsort](x0) = 0,
       
       [true] = 1,
       
       [0] = 1,
       
       [false] = 1,
       
       [nil] = 0,
       
       [le#](x0, x1) = x0 + 1
      Strict:
       le#(s X, s Y) -> le#(X, Y)
       2 + 0Y + 1X >= 1 + 0Y + 1X
      Weak:
       ifselsort(false(), cons(N, L)) -> cons(min cons(N, L), selsort replace(min cons(N, L), N, L))
       2 + 0N + 0L >= 1 + 0N + 0L
       ifselsort(true(), cons(N, L)) -> cons(N, selsort L)
       2 + 0N + 0L >= 1 + 1N + 0L
       selsort nil() -> nil()
       0 >= 0
       selsort cons(N, L) -> ifselsort(eq(N, min cons(N, L)), cons(N, L))
       0 + 0N + 0L >= 2 + 1N + 0L
       ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L))
       0 + 0N + 0M + 0L + 0K >= 2 + 0N + 0M + 1L + 1K
       ifrepl(true(), N, M, cons(K, L)) -> cons(M, L)
       0 + 0N + 0M + 0L + 0K >= 1 + 1M + 1L
       replace(N, M, nil()) -> nil()
       1 + 0N + 0M >= 0
       replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L))
       2 + 0N + 0M + 1L + 1K >= 0 + 0N + 0M + 0L + 0K
       ifmin(false(), cons(N, cons(M, L))) -> min cons(M, L)
       4 + 1N + 1M + 1L >= 0 + 0M + 0L
       ifmin(true(), cons(N, cons(M, L))) -> min cons(N, L)
       4 + 1N + 1M + 1L >= 0 + 0N + 0L
       min cons(s N, nil()) -> s N
       0 + 0N >= 1 + 1N
       min cons(0(), nil()) -> 0()
       0 >= 1
       min cons(N, cons(M, L)) -> ifmin(le(N, M), cons(N, cons(M, L)))
       0 + 0N + 0M + 0L >= 4 + 2N + 1M + 1L
       le(s X, s Y) -> le(X, Y)
       2 + 0Y + 1X >= 1 + 0Y + 1X
       le(s X, 0()) -> false()
       2 + 1X >= 1
       le(0(), Y) -> true()
       2 + 0Y >= 1
       eq(s X, s Y) -> eq(X, Y)
       2 + 0Y + 1X >= 1 + 0Y + 1X
       eq(s X, 0()) -> false()
       2 + 1X >= 1
       eq(0(), s Y) -> false()
       2 + 0Y >= 1
       eq(0(), 0()) -> true()
       2 >= 1
     Qed