MAYBE
MAYBE
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)))
 }
 DUP: We consider a duplicating system.
  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)))
   }
  Fail