Input TRS:
    1: eq(0(),0()) -> true()
    2: eq(0(),s(Y)) -> false()
    3: eq(s(X),0()) -> false()
    4: eq(s(X),s(Y)) -> eq(X,Y)
    5: le(0(),Y) -> true()
    6: le(s(X),0()) -> false()
    7: le(s(X),s(Y)) -> le(X,Y)
    8: min(cons(0(),nil())) -> 0()
    9: min(cons(s(N),nil())) -> s(N)
    10: min(cons(N,cons(M,L))) -> ifmin(le(N,M),cons(N,cons(M,L)))
    11: ifmin(true(),cons(N,cons(M,L))) -> min(cons(N,L))
    12: ifmin(false(),cons(N,cons(M,L))) -> min(cons(M,L))
    13: replace(N,M,nil()) -> nil()
    14: replace(N,M,cons(K,L)) -> ifrepl(eq(N,K),N,M,cons(K,L))
    15: ifrepl(true(),N,M,cons(K,L)) -> cons(M,L)
    16: ifrepl(false(),N,M,cons(K,L)) -> cons(K,replace(N,M,L))
    17: selsort(nil()) -> nil()
    18: selsort(cons(N,L)) -> ifselsort(eq(N,min(cons(N,L))),cons(N,L))
    19: ifselsort(true(),cons(N,L)) -> cons(N,selsort(L))
    20: ifselsort(false(),cons(N,L)) -> cons(min(cons(N,L)),selsort(replace(min(cons(N,L)),N,L)))
Number of strict rules: 20
Direct Order(PosReal,>,Poly) ... failed.
Freezing min
1: eq(0(),0()) -> true()
2: eq(0(),s(Y)) -> false()
3: eq(s(X),0()) -> false()
4: eq(s(X),s(Y)) -> eq(X,Y)
5: le(0(),Y) -> true()
6: le(s(X),0()) -> false()
7: le(s(X),s(Y)) -> le(X,Y)
8: min❆1_cons(0(),nil()) -> 0()
9: min❆1_cons(s(N),nil()) -> s(N)
10: min❆1_cons(N,cons(M,L)) -> ifmin(le(N,M),cons(N,cons(M,L)))
11: ifmin(true(),cons(N,cons(M,L))) -> min❆1_cons(N,L)
12: ifmin(false(),cons(N,cons(M,L))) -> min❆1_cons(M,L)
13: replace(N,M,nil()) -> nil()
14: replace(N,M,cons(K,L)) -> ifrepl(eq(N,K),N,M,cons(K,L))
15: ifrepl(true(),N,M,cons(K,L)) -> cons(M,L)
16: ifrepl(false(),N,M,cons(K,L)) -> cons(K,replace(N,M,L))
17: selsort(nil()) -> nil()
18: selsort(cons(N,L)) -> ifselsort(eq(N,min❆1_cons(N,L)),cons(N,L))
19: ifselsort(true(),cons(N,L)) -> cons(N,selsort(L))
20: ifselsort(false(),cons(N,L)) -> cons(min❆1_cons(N,L),selsort(replace(min❆1_cons(N,L),N,L)))
21: min(cons(_1,_2)) ->= min❆1_cons(_1,_2)
Number of strict rules: 20
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #ifmin(true(),cons(N,cons(M,L))) -> #min❆1_cons(N,L)
   #2: #ifmin(false(),cons(N,cons(M,L))) -> #min❆1_cons(M,L)
   #3: #replace(N,M,cons(K,L)) -> #ifrepl(eq(N,K),N,M,cons(K,L))
   #4: #replace(N,M,cons(K,L)) -> #eq(N,K)
   #5: #ifselsort(false(),cons(N,L)) -> #min❆1_cons(N,L)
   #6: #ifselsort(false(),cons(N,L)) -> #selsort(replace(min❆1_cons(N,L),N,L))
   #7: #ifselsort(false(),cons(N,L)) -> #replace(min❆1_cons(N,L),N,L)
   #8: #ifselsort(false(),cons(N,L)) -> #min❆1_cons(N,L)
   #9: #le(s(X),s(Y)) -> #le(X,Y)
   #10: #min❆1_cons(N,cons(M,L)) -> #ifmin(le(N,M),cons(N,cons(M,L)))
   #11: #min❆1_cons(N,cons(M,L)) -> #le(N,M)
   #12: #ifselsort(true(),cons(N,L)) -> #selsort(L)
   #13: #min(cons(_1,_2)) ->? #min❆1_cons(_1,_2)
   #14: #ifrepl(false(),N,M,cons(K,L)) -> #replace(N,M,L)
   #15: #eq(s(X),s(Y)) -> #eq(X,Y)
   #16: #selsort(cons(N,L)) -> #ifselsort(eq(N,min❆1_cons(N,L)),cons(N,L))
   #17: #selsort(cons(N,L)) -> #eq(N,min❆1_cons(N,L))
   #18: #selsort(cons(N,L)) -> #min❆1_cons(N,L)
Number of SCCs: 5, DPs: 10, edges: 12
	SCC { #9 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
ifselsort(x1,x2)	weight: 0
    le(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 2) + x1
  #le(x1,x2)	weight: x2
 ifmin(x1,x2)	weight: 0
    eq(x1,x2)	weight: 0
 false()	weight: 0
 #min(x1)	weight: 0
min❆1_cons(x1,x2)	weight: 0
  true()	weight: 0
  #eq(x1,x2)	weight: 0
     0()	weight: 0
   nil()	weight: 0
ifrepl(x1,x2,x3,x4)	weight: 0
selsort(x1)	weight: 0
#ifrepl(x1,x2,x3,x4)	weight: 0
#selsort(x1)	weight: 0
#replace(x1,x2,x3)	weight: 0
#ifselsort(x1,x2)	weight: 0
   min(x1)	weight: 0
#min❆1_cons(x1,x2)	weight: 0
  cons(x1,x2)	weight: 0
#ifmin(x1,x2)	weight: 0
replace(x1,x2,x3)	weight: 0
    Usable rules: { }
    Removed DPs: #9
Number of SCCs: 4, DPs: 9, edges: 11
	SCC { #15 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
ifselsort(x1,x2)	weight: 0
    le(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 2) + x1
  #le(x1,x2)	weight: 0
 ifmin(x1,x2)	weight: 0
    eq(x1,x2)	weight: 0
 false()	weight: 0
 #min(x1)	weight: 0
min❆1_cons(x1,x2)	weight: 0
  true()	weight: 0
  #eq(x1,x2)	weight: x2
     0()	weight: 0
   nil()	weight: 0
ifrepl(x1,x2,x3,x4)	weight: 0
selsort(x1)	weight: 0
#ifrepl(x1,x2,x3,x4)	weight: 0
#selsort(x1)	weight: 0
#replace(x1,x2,x3)	weight: 0
#ifselsort(x1,x2)	weight: 0
   min(x1)	weight: 0
#min❆1_cons(x1,x2)	weight: 0
  cons(x1,x2)	weight: 0
#ifmin(x1,x2)	weight: 0
replace(x1,x2,x3)	weight: 0
    Usable rules: { }
    Removed DPs: #15
Number of SCCs: 3, DPs: 8, edges: 10
	SCC { #3 #14 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
ifselsort(x1,x2)	weight: 0
    le(x1,x2)	weight: 0
     s(x1)	weight: (/ 1 4)
  #le(x1,x2)	weight: 0
 ifmin(x1,x2)	weight: 0
    eq(x1,x2)	weight: (/ 1 4) + x2
 false()	weight: 0
 #min(x1)	weight: 0
min❆1_cons(x1,x2)	weight: 0
  true()	weight: 0
  #eq(x1,x2)	weight: 0
     0()	weight: 0
   nil()	weight: 0
ifrepl(x1,x2,x3,x4)	weight: 0
selsort(x1)	weight: 0
#ifrepl(x1,x2,x3,x4)	weight: x4
#selsort(x1)	weight: 0
#replace(x1,x2,x3)	weight: (/ 1 4) + x3
#ifselsort(x1,x2)	weight: 0
   min(x1)	weight: 0
#min❆1_cons(x1,x2)	weight: 0
  cons(x1,x2)	weight: (/ 1 2) + x1 + x2
#ifmin(x1,x2)	weight: 0
replace(x1,x2,x3)	weight: 0
    Usable rules: { }
    Removed DPs: #3 #14
Number of SCCs: 2, DPs: 6, edges: 8
	SCC { #6 #12 #16 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
ifselsort(x1,x2)	weight: 0
    le(x1,x2)	weight: (/ 1 8)
     s(x1)	weight: (/ 1 8)
  #le(x1,x2)	weight: 0
 ifmin(x1,x2)	weight: x2
    eq(x1,x2)	weight: (/ 1 8) + x2
 false()	weight: 0
 #min(x1)	weight: 0
min❆1_cons(x1,x2)	weight: (/ 3 8) + x1 + x2
  true()	weight: 0
  #eq(x1,x2)	weight: 0
     0()	weight: 0
   nil()	weight: 0
ifrepl(x1,x2,x3,x4)	weight: (/ 1 8) + x3 + x4
selsort(x1)	weight: 0
#ifrepl(x1,x2,x3,x4)	weight: 0
#selsort(x1)	weight: (/ 1 8) + x1
#replace(x1,x2,x3)	weight: (/ 1 8)
#ifselsort(x1,x2)	weight: x2
   min(x1)	weight: 0
#min❆1_cons(x1,x2)	weight: 0
  cons(x1,x2)	weight: (/ 3 8) + x1 + x2
#ifmin(x1,x2)	weight: 0
replace(x1,x2,x3)	weight: (/ 1 8) + x2 + x3
    Usable rules: { 5..16 }
    Removed DPs: #6 #12 #16
Number of SCCs: 1, DPs: 3, edges: 4
	SCC { #1 #2 #10 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
ifselsort(x1,x2)	weight: 0
    le(x1,x2)	weight: (/ 1 8)
     s(x1)	weight: (/ 1 8)
  #le(x1,x2)	weight: 0
 ifmin(x1,x2)	weight: x2
    eq(x1,x2)	weight: (/ 1 8) + x2
 false()	weight: 0
 #min(x1)	weight: 0
min❆1_cons(x1,x2)	weight: (/ 1 4) + x1 + x2
  true()	weight: 0
  #eq(x1,x2)	weight: 0
     0()	weight: 0
   nil()	weight: 0
ifrepl(x1,x2,x3,x4)	weight: (/ 1 8) + x3 + x4
selsort(x1)	weight: 0
#ifrepl(x1,x2,x3,x4)	weight: 0
#selsort(x1)	weight: (/ 1 8) + x1
#replace(x1,x2,x3)	weight: (/ 1 8)
#ifselsort(x1,x2)	weight: 0
   min(x1)	weight: 0
#min❆1_cons(x1,x2)	weight: (/ 3 8) + x2
  cons(x1,x2)	weight: (/ 1 4) + x2
#ifmin(x1,x2)	weight: x2
replace(x1,x2,x3)	weight: (/ 1 8) + x2 + x3
    Usable rules: { }
    Removed DPs: #1 #2 #10
Number of SCCs: 0, DPs: 0, edges: 0
YES