YES

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(0(),nil())) -> 0()
  min(cons(s(N),nil())) -> s(N)
  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,nil()) -> nil()
  replace(N,M,cons(K,L)) -> ifrepl(eq(N,K),N,M,cons(K,L))
  ifrepl(true(),N,M,cons(K,L)) -> cons(M,L)
  ifrepl(false(),N,M,cons(K,L)) -> cons(K,replace(N,M,L))
  selsort(nil()) -> nil()
  selsort(cons(N,L)) -> ifselsort(eq(N,min(cons(N,L))),cons(N,L))
  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)))

linear polynomial interpretations on N:

  eq_A(x1,x2) = 1
  eq#_A(x1,x2) = 1
  0_A = 1
  0#_A = 3
  true_A = 1
  true#_A = 2
  s_A(x1) = 1
  s#_A(x1) = 6
  false_A = 1
  false#_A = 0
  le_A(x1,x2) = 1
  le#_A(x1,x2) = 6
  min_A(x1) = 1
  min#_A(x1) = x1 + 1
  cons_A(x1,x2) = x2 + 3
  cons#_A(x1,x2) = 5
  nil_A = 3
  nil#_A = 0
  ifmin_A(x1,x2) = 1
  ifmin#_A(x1,x2) = x2
  replace_A(x1,x2,x3) = x3
  replace#_A(x1,x2,x3) = x1 + x3 + 4
  ifrepl_A(x1,x2,x3,x4) = x4
  ifrepl#_A(x1,x2,x3,x4) = x2 + x4 + 3
  selsort_A(x1) = x1 + 1
  selsort#_A(x1) = x1 + 4
  ifselsort_A(x1,x2) = x2 + 1
  ifselsort#_A(x1,x2) = x2 + 3

precedence:

  replace > eq = s = ifrepl > false = selsort > le = nil = ifmin = ifselsort > cons > 0 > true = min