Input TRS:
    1: eq(|0|(),|0|()) -> true()
    2: eq(|0|(),s(m)) -> false()
    3: eq(s(n),|0|()) -> false()
    4: eq(s(n),s(m)) -> eq(n,m)
    5: le(|0|(),m) -> true()
    6: le(s(n),|0|()) -> false()
    7: le(s(n),s(m)) -> le(n,m)
    8: min(cons(|0|(),nil())) -> |0|()
    9: min(cons(s(n),nil())) -> s(n)
    10: min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
    11: if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
    12: if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
    13: replace(n,m,nil()) -> nil()
    14: replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
    15: if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
    16: if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
    17: |sort|(nil()) -> nil()
    18: |sort|(cons(n,x)) -> cons(min(cons(n,x)),|sort|(replace(min(cons(n,x)),n,x)))
Number of strict rules: 18
Direct Order(PosReal,>,Poly) ... failed.
Freezing min
1: eq(|0|(),|0|()) -> true()
2: eq(|0|(),s(m)) -> false()
3: eq(s(n),|0|()) -> false()
4: eq(s(n),s(m)) -> eq(n,m)
5: le(|0|(),m) -> true()
6: le(s(n),|0|()) -> false()
7: le(s(n),s(m)) -> le(n,m)
8: min❆1_cons(|0|(),nil()) -> |0|()
9: min❆1_cons(s(n),nil()) -> s(n)
10: min❆1_cons(n,cons(m,x)) -> if_min(le(n,m),cons(n,cons(m,x)))
11: if_min(true(),cons(n,cons(m,x))) -> min❆1_cons(n,x)
12: if_min(false(),cons(n,cons(m,x))) -> min❆1_cons(m,x)
13: replace(n,m,nil()) -> nil()
14: replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
15: if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
16: if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
17: |sort|(nil()) -> nil()
18: |sort|(cons(n,x)) -> cons(min❆1_cons(n,x),|sort|(replace(min❆1_cons(n,x),n,x)))
19: min(cons(_1,_2)) ->= min❆1_cons(_1,_2)
Number of strict rules: 18
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #if_min(true(),cons(n,cons(m,x))) -> #min❆1_cons(n,x)
   #2: #if_min(false(),cons(n,cons(m,x))) -> #min❆1_cons(m,x)
   #3: #replace(n,m,cons(k,x)) -> #if_replace(eq(n,k),n,m,cons(k,x))
   #4: #replace(n,m,cons(k,x)) -> #eq(n,k)
   #5: #le(s(n),s(m)) -> #le(n,m)
   #6: #min❆1_cons(n,cons(m,x)) -> #if_min(le(n,m),cons(n,cons(m,x)))
   #7: #min❆1_cons(n,cons(m,x)) -> #le(n,m)
   #8: #min(cons(_1,_2)) ->? #min❆1_cons(_1,_2)
   #9: #if_replace(false(),n,m,cons(k,x)) -> #replace(n,m,x)
   #10: #eq(s(n),s(m)) -> #eq(n,m)
   #11: #|sort|(cons(n,x)) -> #min❆1_cons(n,x)
   #12: #|sort|(cons(n,x)) -> #|sort|(replace(min❆1_cons(n,x),n,x))
   #13: #|sort|(cons(n,x)) -> #replace(min❆1_cons(n,x),n,x)
   #14: #|sort|(cons(n,x)) -> #min❆1_cons(n,x)
Number of SCCs: 5, DPs: 8, edges: 9
	SCC { #5 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   |0|()	weight: 0
    le(x1,x2)	weight: 0
|sort|(x1)	weight: 0
     s(x1)	weight: (/ 1 2) + x1
  #le(x1,x2)	weight: x2
#if_min(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
if_replace(x1,x2,x3,x4)	weight: 0
#|sort|(x1)	weight: 0
   nil()	weight: 0
#replace(x1,x2,x3)	weight: 0
#if_replace(x1,x2,x3,x4)	weight: 0
   min(x1)	weight: 0
#min❆1_cons(x1,x2)	weight: 0
  cons(x1,x2)	weight: 0
if_min(x1,x2)	weight: 0
replace(x1,x2,x3)	weight: 0
    Usable rules: { }
    Removed DPs: #5
Number of SCCs: 4, DPs: 7, edges: 8
	SCC { #10 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   |0|()	weight: 0
    le(x1,x2)	weight: 0
|sort|(x1)	weight: 0
     s(x1)	weight: (/ 1 2) + x1
  #le(x1,x2)	weight: 0
#if_min(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
if_replace(x1,x2,x3,x4)	weight: 0
#|sort|(x1)	weight: 0
   nil()	weight: 0
#replace(x1,x2,x3)	weight: 0
#if_replace(x1,x2,x3,x4)	weight: 0
   min(x1)	weight: 0
#min❆1_cons(x1,x2)	weight: 0
  cons(x1,x2)	weight: 0
if_min(x1,x2)	weight: 0
replace(x1,x2,x3)	weight: 0
    Usable rules: { }
    Removed DPs: #10
Number of SCCs: 3, DPs: 6, edges: 7
	SCC { #12 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   |0|()	weight: 0
    le(x1,x2)	weight: (/ 1 4) + x2
|sort|(x1)	weight: 0
     s(x1)	weight: (/ 3 4)
  #le(x1,x2)	weight: 0
#if_min(x1,x2)	weight: 0
    eq(x1,x2)	weight: (/ 1 8)
 false()	weight: 0
 #min(x1)	weight: 0
min❆1_cons(x1,x2)	weight: (/ 5 8)
  true()	weight: 0
  #eq(x1,x2)	weight: 0
if_replace(x1,x2,x3,x4)	weight: (/ 1 8) + x4
#|sort|(x1)	weight: x1
   nil()	weight: 0
#replace(x1,x2,x3)	weight: 0
#if_replace(x1,x2,x3,x4)	weight: 0
   min(x1)	weight: 0
#min❆1_cons(x1,x2)	weight: 0
  cons(x1,x2)	weight: (/ 1 4) + x2
if_min(x1,x2)	weight: x1 + x2
replace(x1,x2,x3)	weight: (/ 1 8) + x3
    Usable rules: { 1..4 13..16 }
    Removed DPs: #12
Number of SCCs: 2, DPs: 5, edges: 6
	SCC { #3 #9 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   |0|()	weight: 0
    le(x1,x2)	weight: (/ 1 4) + x2
|sort|(x1)	weight: 0
     s(x1)	weight: (/ 3 4)
  #le(x1,x2)	weight: 0
#if_min(x1,x2)	weight: 0
    eq(x1,x2)	weight: (/ 1 8)
 false()	weight: 0
 #min(x1)	weight: 0
min❆1_cons(x1,x2)	weight: (/ 5 8)
  true()	weight: 0
  #eq(x1,x2)	weight: 0
if_replace(x1,x2,x3,x4)	weight: x1 + x4
#|sort|(x1)	weight: 0
   nil()	weight: 0
#replace(x1,x2,x3)	weight: (/ 1 8) + x3
#if_replace(x1,x2,x3,x4)	weight: x4
   min(x1)	weight: 0
#min❆1_cons(x1,x2)	weight: 0
  cons(x1,x2)	weight: (/ 1 4) + x1 + x2
if_min(x1,x2)	weight: x1 + x2
replace(x1,x2,x3)	weight: (/ 1 8) + x3
    Usable rules: { }
    Removed DPs: #3 #9
Number of SCCs: 1, DPs: 3, edges: 4
	SCC { #1 #2 #6 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
   |0|()	weight: 0
    le(x1,x2)	weight: (/ 1 4) + x2
|sort|(x1)	weight: 0
     s(x1)	weight: (/ 3 4)
  #le(x1,x2)	weight: 0
#if_min(x1,x2)	weight: x2
    eq(x1,x2)	weight: (/ 1 8)
 false()	weight: 0
 #min(x1)	weight: 0
min❆1_cons(x1,x2)	weight: (/ 5 8)
  true()	weight: 0
  #eq(x1,x2)	weight: 0
if_replace(x1,x2,x3,x4)	weight: x1 + x4
#|sort|(x1)	weight: 0
   nil()	weight: 0
#replace(x1,x2,x3)	weight: (/ 1 8)
#if_replace(x1,x2,x3,x4)	weight: 0
   min(x1)	weight: 0
#min❆1_cons(x1,x2)	weight: (/ 3 8) + x1 + x2
  cons(x1,x2)	weight: (/ 1 4) + x1 + x2
if_min(x1,x2)	weight: x1 + x2
replace(x1,x2,x3)	weight: (/ 1 8) + x3
    Usable rules: { }
    Removed DPs: #1 #2 #6
Number of SCCs: 0, DPs: 0, edges: 0
YES