Input TRS:
    1: active(primes()) -> mark(sieve(from(s(s(0())))))
    2: active(from(X)) -> mark(cons(X,from(s(X))))
    3: active(head(cons(X,Y))) -> mark(X)
    4: active(tail(cons(X,Y))) -> mark(Y)
    5: active(if(true(),X,Y)) -> mark(X)
    6: active(if(false(),X,Y)) -> mark(Y)
    7: active(filter(s(s(X)),cons(Y,Z))) -> mark(if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))))
    8: active(sieve(cons(X,Y))) -> mark(cons(X,filter(X,sieve(Y))))
    9: mark(primes()) -> active(primes())
    10: mark(sieve(X)) -> active(sieve(mark(X)))
    11: mark(from(X)) -> active(from(mark(X)))
    12: mark(s(X)) -> active(s(mark(X)))
    13: mark(0()) -> active(0())
    14: mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
    15: mark(head(X)) -> active(head(mark(X)))
    16: mark(tail(X)) -> active(tail(mark(X)))
    17: mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
    18: mark(true()) -> active(true())
    19: mark(false()) -> active(false())
    20: mark(filter(X1,X2)) -> active(filter(mark(X1),mark(X2)))
    21: mark(divides(X1,X2)) -> active(divides(mark(X1),mark(X2)))
    22: sieve(mark(X)) -> sieve(X)
    23: sieve(active(X)) -> sieve(X)
    24: from(mark(X)) -> from(X)
    25: from(active(X)) -> from(X)
    26: s(mark(X)) -> s(X)
    27: s(active(X)) -> s(X)
    28: cons(mark(X1),X2) -> cons(X1,X2)
    29: cons(X1,mark(X2)) -> cons(X1,X2)
    30: cons(active(X1),X2) -> cons(X1,X2)
    31: cons(X1,active(X2)) -> cons(X1,X2)
    32: head(mark(X)) -> head(X)
    33: head(active(X)) -> head(X)
    34: tail(mark(X)) -> tail(X)
    35: tail(active(X)) -> tail(X)
    36: if(mark(X1),X2,X3) -> if(X1,X2,X3)
    37: if(X1,mark(X2),X3) -> if(X1,X2,X3)
    38: if(X1,X2,mark(X3)) -> if(X1,X2,X3)
    39: if(active(X1),X2,X3) -> if(X1,X2,X3)
    40: if(X1,active(X2),X3) -> if(X1,X2,X3)
    41: if(X1,X2,active(X3)) -> if(X1,X2,X3)
    42: filter(mark(X1),X2) -> filter(X1,X2)
    43: filter(X1,mark(X2)) -> filter(X1,X2)
    44: filter(active(X1),X2) -> filter(X1,X2)
    45: filter(X1,active(X2)) -> filter(X1,X2)
    46: divides(mark(X1),X2) -> divides(X1,X2)
    47: divides(X1,mark(X2)) -> divides(X1,X2)
    48: divides(active(X1),X2) -> divides(X1,X2)
    49: divides(X1,active(X2)) -> divides(X1,X2)
Number of strict rules: 49
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #active(from(X)) -> #mark(cons(X,from(s(X))))
   #2: #active(from(X)) -> #cons(X,from(s(X)))
   #3: #active(from(X)) -> #from(s(X))
   #4: #active(from(X)) -> #s(X)
   #5: #filter(X1,mark(X2)) -> #filter(X1,X2)
   #6: #cons(X1,mark(X2)) -> #cons(X1,X2)
   #7: #tail(active(X)) -> #tail(X)
   #8: #divides(mark(X1),X2) -> #divides(X1,X2)
   #9: #filter(mark(X1),X2) -> #filter(X1,X2)
   #10: #if(X1,X2,active(X3)) -> #if(X1,X2,X3)
   #11: #if(X1,mark(X2),X3) -> #if(X1,X2,X3)
   #12: #divides(X1,mark(X2)) -> #divides(X1,X2)
   #13: #divides(active(X1),X2) -> #divides(X1,X2)
   #14: #if(X1,X2,mark(X3)) -> #if(X1,X2,X3)
   #15: #active(if(false(),X,Y)) -> #mark(Y)
   #16: #if(X1,active(X2),X3) -> #if(X1,X2,X3)
   #17: #mark(0()) -> #active(0())
   #18: #mark(primes()) -> #active(primes())
   #19: #mark(from(X)) -> #active(from(mark(X)))
   #20: #mark(from(X)) -> #from(mark(X))
   #21: #mark(from(X)) -> #mark(X)
   #22: #from(mark(X)) -> #from(X)
   #23: #sieve(active(X)) -> #sieve(X)
   #24: #filter(X1,active(X2)) -> #filter(X1,X2)
   #25: #mark(s(X)) -> #active(s(mark(X)))
   #26: #mark(s(X)) -> #s(mark(X))
   #27: #mark(s(X)) -> #mark(X)
   #28: #cons(X1,active(X2)) -> #cons(X1,X2)
   #29: #mark(cons(X1,X2)) -> #active(cons(mark(X1),X2))
   #30: #mark(cons(X1,X2)) -> #cons(mark(X1),X2)
   #31: #mark(cons(X1,X2)) -> #mark(X1)
   #32: #cons(active(X1),X2) -> #cons(X1,X2)
   #33: #divides(X1,active(X2)) -> #divides(X1,X2)
   #34: #from(active(X)) -> #from(X)
   #35: #mark(filter(X1,X2)) -> #active(filter(mark(X1),mark(X2)))
   #36: #mark(filter(X1,X2)) -> #filter(mark(X1),mark(X2))
   #37: #mark(filter(X1,X2)) -> #mark(X1)
   #38: #mark(filter(X1,X2)) -> #mark(X2)
   #39: #active(filter(s(s(X)),cons(Y,Z))) -> #mark(if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y)))))
   #40: #active(filter(s(s(X)),cons(Y,Z))) -> #if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))
   #41: #active(filter(s(s(X)),cons(Y,Z))) -> #divides(s(s(X)),Y)
   #42: #active(filter(s(s(X)),cons(Y,Z))) -> #filter(s(s(X)),Z)
   #43: #active(filter(s(s(X)),cons(Y,Z))) -> #cons(Y,filter(X,sieve(Y)))
   #44: #active(filter(s(s(X)),cons(Y,Z))) -> #filter(X,sieve(Y))
   #45: #active(filter(s(s(X)),cons(Y,Z))) -> #sieve(Y)
   #46: #if(active(X1),X2,X3) -> #if(X1,X2,X3)
   #47: #mark(sieve(X)) -> #active(sieve(mark(X)))
   #48: #mark(sieve(X)) -> #sieve(mark(X))
   #49: #mark(sieve(X)) -> #mark(X)
   #50: #head(active(X)) -> #head(X)
   #51: #active(if(true(),X,Y)) -> #mark(X)
   #52: #filter(active(X1),X2) -> #filter(X1,X2)
   #53: #cons(mark(X1),X2) -> #cons(X1,X2)
   #54: #sieve(mark(X)) -> #sieve(X)
   #55: #tail(mark(X)) -> #tail(X)
   #56: #s(active(X)) -> #s(X)
   #57: #mark(if(X1,X2,X3)) -> #active(if(mark(X1),X2,X3))
   #58: #mark(if(X1,X2,X3)) -> #if(mark(X1),X2,X3)
   #59: #mark(if(X1,X2,X3)) -> #mark(X1)
   #60: #head(mark(X)) -> #head(X)
   #61: #mark(false()) -> #active(false())
   #62: #s(mark(X)) -> #s(X)
   #63: #if(mark(X1),X2,X3) -> #if(X1,X2,X3)
   #64: #mark(divides(X1,X2)) -> #active(divides(mark(X1),mark(X2)))
   #65: #mark(divides(X1,X2)) -> #divides(mark(X1),mark(X2))
   #66: #mark(divides(X1,X2)) -> #mark(X1)
   #67: #mark(divides(X1,X2)) -> #mark(X2)
   #68: #mark(tail(X)) -> #active(tail(mark(X)))
   #69: #mark(tail(X)) -> #tail(mark(X))
   #70: #mark(tail(X)) -> #mark(X)
   #71: #active(head(cons(X,Y))) -> #mark(X)
   #72: #active(primes()) -> #mark(sieve(from(s(s(0())))))
   #73: #active(primes()) -> #sieve(from(s(s(0()))))
   #74: #active(primes()) -> #from(s(s(0())))
   #75: #active(primes()) -> #s(s(0()))
   #76: #active(primes()) -> #s(0())
   #77: #active(sieve(cons(X,Y))) -> #mark(cons(X,filter(X,sieve(Y))))
   #78: #active(sieve(cons(X,Y))) -> #cons(X,filter(X,sieve(Y)))
   #79: #active(sieve(cons(X,Y))) -> #filter(X,sieve(Y))
   #80: #active(sieve(cons(X,Y))) -> #sieve(Y)
   #81: #mark(head(X)) -> #active(head(mark(X)))
   #82: #mark(head(X)) -> #head(mark(X))
   #83: #mark(head(X)) -> #mark(X)
   #84: #active(tail(cons(X,Y))) -> #mark(Y)
   #85: #mark(true()) -> #active(true())
Number of SCCs: 10, DPs: 54, edges: 388
	SCC { #22 #34 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
#filter(x1,x2)	weight: 0
 false()	weight: 0
#head(x1)	weight: 0
  true()	weight: 0
  tail(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
    if(x1,x2,x3)	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: 0
#tail(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
 sieve(x1)	weight: 0
#divides(x1,x2)	weight: 0
#from(x1)	weight: x1
active(x1)	weight: (/ 1 2) + x1
  head(x1)	weight: 0
  cons(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: 0
filter(x1,x2)	weight: 0
primes()	weight: 0
#sieve(x1)	weight: 0
divides(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #22 #34
Number of SCCs: 9, DPs: 52, edges: 384
	SCC { #23 #54 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
#filter(x1,x2)	weight: 0
 false()	weight: 0
#head(x1)	weight: 0
  true()	weight: 0
  tail(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
    if(x1,x2,x3)	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: 0
#tail(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
 sieve(x1)	weight: 0
#divides(x1,x2)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  head(x1)	weight: 0
  cons(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: 0
filter(x1,x2)	weight: 0
primes()	weight: 0
#sieve(x1)	weight: x1
divides(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #23 #54
Number of SCCs: 8, DPs: 50, edges: 380
	SCC { #50 #60 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
#filter(x1,x2)	weight: 0
 false()	weight: 0
#head(x1)	weight: x1
  true()	weight: 0
  tail(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
    if(x1,x2,x3)	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: 0
#tail(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
 sieve(x1)	weight: 0
#divides(x1,x2)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  head(x1)	weight: 0
  cons(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: 0
filter(x1,x2)	weight: 0
primes()	weight: 0
#sieve(x1)	weight: 0
divides(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #50 #60
Number of SCCs: 7, DPs: 48, edges: 376
	SCC { #7 #55 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
#filter(x1,x2)	weight: 0
 false()	weight: 0
#head(x1)	weight: 0
  true()	weight: 0
  tail(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
    if(x1,x2,x3)	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: 0
#tail(x1)	weight: x1
  mark(x1)	weight: (/ 1 2) + x1
 sieve(x1)	weight: 0
#divides(x1,x2)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  head(x1)	weight: 0
  cons(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: 0
filter(x1,x2)	weight: 0
primes()	weight: 0
#sieve(x1)	weight: 0
divides(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #7 #55
Number of SCCs: 6, DPs: 46, edges: 372
	SCC { #56 #62 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
#filter(x1,x2)	weight: 0
 false()	weight: 0
#head(x1)	weight: 0
  true()	weight: 0
  tail(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
    if(x1,x2,x3)	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: x1
#tail(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
 sieve(x1)	weight: 0
#divides(x1,x2)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  head(x1)	weight: 0
  cons(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: 0
filter(x1,x2)	weight: 0
primes()	weight: 0
#sieve(x1)	weight: 0
divides(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #56 #62
Number of SCCs: 5, DPs: 44, edges: 368
	SCC { #6 #28 #32 #53 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: x1
     s(x1)	weight: 0
#filter(x1,x2)	weight: 0
 false()	weight: 0
#head(x1)	weight: 0
  true()	weight: 0
  tail(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
    if(x1,x2,x3)	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: 0
#tail(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
 sieve(x1)	weight: 0
#divides(x1,x2)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  head(x1)	weight: 0
  cons(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: 0
filter(x1,x2)	weight: 0
primes()	weight: 0
#sieve(x1)	weight: 0
divides(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #32 #53
Number of SCCs: 5, DPs: 42, edges: 356
	SCC { #6 #28 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: x2
     s(x1)	weight: 0
#filter(x1,x2)	weight: 0
 false()	weight: 0
#head(x1)	weight: 0
  true()	weight: 0
  tail(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
    if(x1,x2,x3)	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: 0
#tail(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
 sieve(x1)	weight: 0
#divides(x1,x2)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  head(x1)	weight: 0
  cons(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: 0
filter(x1,x2)	weight: 0
primes()	weight: 0
#sieve(x1)	weight: 0
divides(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #6 #28
Number of SCCs: 4, DPs: 40, edges: 352
	SCC { #5 #9 #24 #52 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
#filter(x1,x2)	weight: x1
 false()	weight: 0
#head(x1)	weight: 0
  true()	weight: 0
  tail(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
    if(x1,x2,x3)	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: 0
#tail(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
 sieve(x1)	weight: 0
#divides(x1,x2)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  head(x1)	weight: 0
  cons(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: 0
filter(x1,x2)	weight: 0
primes()	weight: 0
#sieve(x1)	weight: 0
divides(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #9 #52
Number of SCCs: 5, DPs: 38, edges: 340
	SCC { #5 #24 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
#filter(x1,x2)	weight: x2
 false()	weight: 0
#head(x1)	weight: 0
  true()	weight: 0
  tail(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
    if(x1,x2,x3)	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: 0
#tail(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
 sieve(x1)	weight: 0
#divides(x1,x2)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  head(x1)	weight: 0
  cons(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: 0
filter(x1,x2)	weight: 0
primes()	weight: 0
#sieve(x1)	weight: 0
divides(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #5 #24
Number of SCCs: 4, DPs: 36, edges: 336
	SCC { #8 #12 #13 #33 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
#filter(x1,x2)	weight: 0
 false()	weight: 0
#head(x1)	weight: 0
  true()	weight: 0
  tail(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
    if(x1,x2,x3)	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: 0
#tail(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
 sieve(x1)	weight: 0
#divides(x1,x2)	weight: x1
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  head(x1)	weight: 0
  cons(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: 0
filter(x1,x2)	weight: 0
primes()	weight: 0
#sieve(x1)	weight: 0
divides(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #8 #13
Number of SCCs: 5, DPs: 34, edges: 324
	SCC { #12 #33 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
#filter(x1,x2)	weight: 0
 false()	weight: 0
#head(x1)	weight: 0
  true()	weight: 0
  tail(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
    if(x1,x2,x3)	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: 0
#tail(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
 sieve(x1)	weight: 0
#divides(x1,x2)	weight: x2
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  head(x1)	weight: 0
  cons(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: 0
filter(x1,x2)	weight: 0
primes()	weight: 0
#sieve(x1)	weight: 0
divides(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #12 #33
Number of SCCs: 4, DPs: 32, edges: 320
	SCC { #10 #11 #14 #16 #46 #63 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
#filter(x1,x2)	weight: 0
 false()	weight: 0
#head(x1)	weight: 0
  true()	weight: 0
  tail(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
    if(x1,x2,x3)	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: 0
#tail(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
 sieve(x1)	weight: 0
#divides(x1,x2)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  head(x1)	weight: 0
  cons(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: x2 + x3
#active(x1)	weight: 0
filter(x1,x2)	weight: 0
primes()	weight: 0
#sieve(x1)	weight: 0
divides(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #10 #11 #14 #16
Number of SCCs: 5, DPs: 28, edges: 288
	SCC { #46 #63 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: 0
#filter(x1,x2)	weight: 0
 false()	weight: 0
#head(x1)	weight: 0
  true()	weight: 0
  tail(x1)	weight: 0
#mark(x1)	weight: 0
     0()	weight: 0
    if(x1,x2,x3)	weight: 0
  from(x1)	weight: 0
   #s(x1)	weight: 0
#tail(x1)	weight: 0
  mark(x1)	weight: (/ 1 2) + x1
 sieve(x1)	weight: 0
#divides(x1,x2)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: (/ 1 2) + x1
  head(x1)	weight: 0
  cons(x1,x2)	weight: 0
  #if(x1,x2,x3)	weight: x1
#active(x1)	weight: 0
filter(x1,x2)	weight: 0
primes()	weight: 0
#sieve(x1)	weight: 0
divides(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #46 #63
Number of SCCs: 4, DPs: 26, edges: 284
	SCC { #1 #15 #18 #19 #21 #27 #31 #35 #37..39 #47 #49 #51 #57 #59 #66..68 #70..72 #77 #81 #83 #84 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... succeeded.
#cons(x1,x2)	weight: 0
     s(x1)	weight: x1
#filter(x1,x2)	weight: 0
 false()	weight: (/ 1 16)
#head(x1)	weight: 0
  true()	weight: (/ 1 16)
  tail(x1)	weight: (/ 1 16) + x1
#mark(x1)	weight: x1
     0()	weight: 0
    if(x1,x2,x3)	weight: max{x3, x2, (/ 1 16) + x1}
  from(x1)	weight: (/ 5 16) + x1
   #s(x1)	weight: 0
#tail(x1)	weight: 0
  mark(x1)	weight: x1
 sieve(x1)	weight: (/ 3 16) + x1
#divides(x1,x2)	weight: 0
#from(x1)	weight: 0
active(x1)	weight: x1
  head(x1)	weight: (/ 1 16) + x1
  cons(x1,x2)	weight: max{x2, (/ 1 4) + x1}
  #if(x1,x2,x3)	weight: 0
#active(x1)	weight: x1
filter(x1,x2)	weight: max{x2, (/ 1 8) + x1}
primes()	weight: (/ 9 16)
#sieve(x1)	weight: 0
divides(x1,x2)	weight: max{(/ 3 16) + x2, (/ 1 16) + x1}
    Usable rules: { 1..49 }
    Removed DPs: #21 #31 #37 #49 #59 #66 #67 #70..72 #83 #84
Number of SCCs: 5, DPs: 7, edges: 20
	SCC { #15 #27 #35 #38 #39 #51 #57 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... Order(PosReal,>,Sum-Sum; PosReal,≥,Sum-Sum)... Order(PosReal,>,Sum-Sum; NegReal,≥,Sum)... succeeded.
#cons(x1,x2)	weight: 0; 0
     s(x1)	weight: (max (/ 1 8) 0); 0
#filter(x1,x2)	weight: 0; 0
 false()	weight: 0; 0
#head(x1)	weight: 0; 0
  true()	weight: (/ 1 8); 0
  tail(x1)	weight: (max (- (/ 1 2)) 0); 0
#mark(x1)	weight: max{0, (/ 5 8) + x1_2}; 0
     0()	weight: (/ 1 2); (- (/ 1 8))
    if(x1,x2,x3)	weight: (max (/ 3 8) 0); x1_2
  from(x1)	weight: (max (- (/ 1 4)) 0); (- (/ 1 8))
   #s(x1)	weight: 0; 0
#tail(x1)	weight: 0; 0
  mark(x1)	weight: (max (- (/ 7 8)) 0); x1_2
 sieve(x1)	weight: (max (- (/ 3 8)) 0); (- (/ 1 8))
#divides(x1,x2)	weight: 0; 0
#from(x1)	weight: 0; 0
active(x1)	weight: max{0, (- (/ 3 8)) + x1_1 + x1_2}; x1_2
  head(x1)	weight: (max (- (/ 3 8)) 0); 0
  cons(x1,x2)	weight: (max (- (/ 1 8)) 0); (- (/ 1 8))
  #if(x1,x2,x3)	weight: 0; 0
#active(x1)	weight: max{0, (/ 1 4) + x1_1 + x1_2}; 0
filter(x1,x2)	weight: max{0, (/ 3 8) + x2_2 + x1_2}; x2_2
primes()	weight: (/ 1 8); (- (/ 1 8))
#sieve(x1)	weight: 0; 0
divides(x1,x2)	weight: max{0, (/ 1 8) + x1_2}; (- (/ 3 8)) + x2_2
    Usable rules: { 1..49 }
    Removed DPs: #39
Number of SCCs: 5, DPs: 5, edges: 14
	SCC { #15 #27 #38 #51 #57 }
Removing DPs: Order(PosReal,>,Sum)... Order(PosReal,>,Max)... QLPOpS... Order(PosReal,>,MaxSum)... QWPOpS(PosReal,>,MaxSum)... Order(PosReal,>,Sum-Sum; PosReal,≥,Sum-Sum)... Order(PosReal,>,Sum-Sum; NegReal,≥,Sum)... Order(PosReal,>,MaxSum-Sum; NegReal,≥,Sum)... succeeded.
#cons(x1,x2)	weight: 0; 0
     s(x1)	weight: max{0, (/ 29 64) + x1_1}; (- (/ 5 32)) + x1_2
#filter(x1,x2)	weight: 0; 0
 false()	weight: (/ 41 32); (- (/ 3 8))
#head(x1)	weight: 0; 0
  true()	weight: 0; (- (/ 7 16))
  tail(x1)	weight: max{0, (/ 61 32) + x1_2 + x1_1}; (- (/ 1 16)) + x1_2
#mark(x1)	weight: max{0, (/ 1 8) + x1_1}; (- (/ 9 16))
     0()	weight: 0; (- (/ 1 16))
    if(x1,x2,x3)	weight: max{0, (/ 1 8) + x2_1, (/ 3 8) + x3_1}; (- (/ 9 16))
  from(x1)	weight: (max (/ 1 16) 0); (- (/ 9 16)) + x1_2
   #s(x1)	weight: 0; 0
#tail(x1)	weight: 0; 0
  mark(x1)	weight: max{0, (/ 41 32) + x1_1}; (- (/ 51 16))
 sieve(x1)	weight: max{0, (/ 35 32) + x1_1}; (- (/ 1 16))
#divides(x1,x2)	weight: 0; 0
#from(x1)	weight: 0; 0
active(x1)	weight: max{0, (/ 3 16) + x1_1}; (- (/ 43 16)) + x1_2
  head(x1)	weight: 0; (- (/ 7 16))
  cons(x1,x2)	weight: max{0, (- (/ 1 4)) + x1_1, (- (/ 1 4)) + x2_2}; (- (/ 53 32)) + x2_2
  #if(x1,x2,x3)	weight: 0; 0
#active(x1)	weight: max{0, (/ 5 8) + x1_2 + x1_1}; x1_2
filter(x1,x2)	weight: max{0, (/ 3 16) + x1_2, (/ 1 8) + x1_1, (/ 53 32) + x2_2, (/ 1 4) + x2_1}; (- (/ 1 16)) + x2_2 + x1_2
primes()	weight: 0; (- (/ 9 16))
#sieve(x1)	weight: 0; 0
divides(x1,x2)	weight: max{0, (- (/ 41 32)) + x1_2, (- (/ 45 32)) + x1_1, (/ 41 32) + x2_2, (- (/ 43 32)) + x2_1}; (- (/ 1 16)) + x2_2 + x1_2
    Usable rules: { 22 23 36..41 }
    Removed DPs: #15 #27 #38 #51 #57
Number of SCCs: 4, DPs: 0, edges: 0
YES