Input TRS:
    1: primes() -> sieve(from(s(s(0()))))
    2: from(X) -> cons(X,from(s(X)))
    3: head(cons(X,Y)) -> X
    4: tail(cons(X,Y)) -> Y
    5: if(true(),X,Y) -> X
    6: if(false(),X,Y) -> Y
    7: filter(s(s(X)),cons(Y,Z)) -> if(divides(s(s(X)),Y),filter(s(s(X)),Z),cons(Y,filter(X,sieve(Y))))
    8: sieve(cons(X,Y)) -> cons(X,filter(X,sieve(Y)))
Number of strict rules: 8
Direct Order(PosReal,>,Poly) ... failed.
Freezing filter if
1: primes() -> sieve(from(s(s(0()))))
2: from(X) -> cons(X,from(s(X)))
3: head(cons(X,Y)) -> X
4: tail(cons(X,Y)) -> Y
5: if❆1_true(X,Y) -> X
6: if❆1_false(X,Y) -> Y
7: filter❆1_s(s(X),cons(Y,Z)) -> if❆1_divides(s(s(X)),Y,filter❆1_s(s(X),Z),cons(Y,filter(X,sieve(Y))))
8: sieve(cons(X,Y)) -> cons(X,filter(X,sieve(Y)))
9: if(false(),_2,_3) ->= if❆1_false(_2,_3)
10: if(divides(_1,_2),_4,_5) ->= if❆1_divides(_1,_2,_4,_5)
11: if(true(),_2,_3) ->= if❆1_true(_2,_3)
12: filter(s(_1),_2) ->= filter❆1_s(_1,_2)
Number of strict rules: 8
Direct Order(PosReal,>,Poly) ... failed.
Dependency Pairs:
   #1: #from(X) -> #from(s(X))
   #2: #if(false(),_2,_3) ->? #if❆1_false(_2,_3)
   #3: #if(true(),_2,_3) ->? #if❆1_true(_2,_3)
   #4: #filter(s(_1),_2) ->? #filter❆1_s(_1,_2)
   #5: #filter❆1_s(s(X),cons(Y,Z)) -> #filter❆1_s(s(X),Z)
   #6: #filter❆1_s(s(X),cons(Y,Z)) -> #filter(X,sieve(Y))
   #7: #filter❆1_s(s(X),cons(Y,Z)) -> #sieve(Y)
   #8: #primes() -> #sieve(from(s(s(0()))))
   #9: #primes() -> #from(s(s(0())))
   #10: #sieve(cons(X,Y)) -> #filter(X,sieve(Y))
   #11: #sieve(cons(X,Y)) -> #sieve(Y)
Number of SCCs: 2, DPs: 7, edges: 13
	SCC { #1 }
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)... failed.
Removing edges: failed.
Finding a loop...  found.
  #from(X)	-#1->
  #from(s(X))	--->*
  #from(s(X))
  Looping with: [ X := s(X); ]
NO