MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { primes() -> sieve(from(s(s(0()))))
  , sieve(cons(X, Y)) -> cons(X, filter(X, sieve(Y)))
  , from(X) -> cons(X, from(s(X)))
  , head(cons(X, Y)) -> X
  , tail(cons(X, Y)) -> Y
  , if(true(), X, Y) -> X
  , if(false(), X, Y) -> Y
  , filter(s(s(X)), cons(Y, Z)) ->
    if(divides(s(s(X)), Y),
       filter(s(s(X)), Z),
       cons(Y, filter(X, sieve(Y)))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { primes^#() -> c_1(sieve^#(from(s(s(0())))), from^#(s(s(0()))))
  , sieve^#(cons(X, Y)) -> c_2(filter^#(X, sieve(Y)), sieve^#(Y))
  , from^#(X) -> c_3(from^#(s(X)))
  , filter^#(s(s(X)), cons(Y, Z)) ->
    c_8(if^#(divides(s(s(X)), Y),
             filter(s(s(X)), Z),
             cons(Y, filter(X, sieve(Y)))),
        filter^#(s(s(X)), Z),
        filter^#(X, sieve(Y)),
        sieve^#(Y))
  , head^#(cons(X, Y)) -> c_4()
  , tail^#(cons(X, Y)) -> c_5()
  , if^#(true(), X, Y) -> c_6()
  , if^#(false(), X, Y) -> c_7() }

and mark the set of starting terms.

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { primes^#() -> c_1(sieve^#(from(s(s(0())))), from^#(s(s(0()))))
  , sieve^#(cons(X, Y)) -> c_2(filter^#(X, sieve(Y)), sieve^#(Y))
  , from^#(X) -> c_3(from^#(s(X)))
  , filter^#(s(s(X)), cons(Y, Z)) ->
    c_8(if^#(divides(s(s(X)), Y),
             filter(s(s(X)), Z),
             cons(Y, filter(X, sieve(Y)))),
        filter^#(s(s(X)), Z),
        filter^#(X, sieve(Y)),
        sieve^#(Y))
  , head^#(cons(X, Y)) -> c_4()
  , tail^#(cons(X, Y)) -> c_5()
  , if^#(true(), X, Y) -> c_6()
  , if^#(false(), X, Y) -> c_7() }
Weak Trs:
  { primes() -> sieve(from(s(s(0()))))
  , sieve(cons(X, Y)) -> cons(X, filter(X, sieve(Y)))
  , from(X) -> cons(X, from(s(X)))
  , head(cons(X, Y)) -> X
  , tail(cons(X, Y)) -> Y
  , if(true(), X, Y) -> X
  , if(false(), X, Y) -> Y
  , filter(s(s(X)), cons(Y, Z)) ->
    if(divides(s(s(X)), Y),
       filter(s(s(X)), Z),
       cons(Y, filter(X, sieve(Y)))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We estimate the number of application of {5,6,7,8} by applications
of Pre({5,6,7,8}) = {}. Here rules are labeled as follows:

  DPs:
    { 1: primes^#() -> c_1(sieve^#(from(s(s(0())))), from^#(s(s(0()))))
    , 2: sieve^#(cons(X, Y)) -> c_2(filter^#(X, sieve(Y)), sieve^#(Y))
    , 3: from^#(X) -> c_3(from^#(s(X)))
    , 4: filter^#(s(s(X)), cons(Y, Z)) ->
         c_8(if^#(divides(s(s(X)), Y),
                  filter(s(s(X)), Z),
                  cons(Y, filter(X, sieve(Y)))),
             filter^#(s(s(X)), Z),
             filter^#(X, sieve(Y)),
             sieve^#(Y))
    , 5: head^#(cons(X, Y)) -> c_4()
    , 6: tail^#(cons(X, Y)) -> c_5()
    , 7: if^#(true(), X, Y) -> c_6()
    , 8: if^#(false(), X, Y) -> c_7() }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { primes^#() -> c_1(sieve^#(from(s(s(0())))), from^#(s(s(0()))))
  , sieve^#(cons(X, Y)) -> c_2(filter^#(X, sieve(Y)), sieve^#(Y))
  , from^#(X) -> c_3(from^#(s(X)))
  , filter^#(s(s(X)), cons(Y, Z)) ->
    c_8(if^#(divides(s(s(X)), Y),
             filter(s(s(X)), Z),
             cons(Y, filter(X, sieve(Y)))),
        filter^#(s(s(X)), Z),
        filter^#(X, sieve(Y)),
        sieve^#(Y)) }
Weak DPs:
  { head^#(cons(X, Y)) -> c_4()
  , tail^#(cons(X, Y)) -> c_5()
  , if^#(true(), X, Y) -> c_6()
  , if^#(false(), X, Y) -> c_7() }
Weak Trs:
  { primes() -> sieve(from(s(s(0()))))
  , sieve(cons(X, Y)) -> cons(X, filter(X, sieve(Y)))
  , from(X) -> cons(X, from(s(X)))
  , head(cons(X, Y)) -> X
  , tail(cons(X, Y)) -> Y
  , if(true(), X, Y) -> X
  , if(false(), X, Y) -> Y
  , filter(s(s(X)), cons(Y, Z)) ->
    if(divides(s(s(X)), Y),
       filter(s(s(X)), Z),
       cons(Y, filter(X, sieve(Y)))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ head^#(cons(X, Y)) -> c_4()
, tail^#(cons(X, Y)) -> c_5()
, if^#(true(), X, Y) -> c_6()
, if^#(false(), X, Y) -> c_7() }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { primes^#() -> c_1(sieve^#(from(s(s(0())))), from^#(s(s(0()))))
  , sieve^#(cons(X, Y)) -> c_2(filter^#(X, sieve(Y)), sieve^#(Y))
  , from^#(X) -> c_3(from^#(s(X)))
  , filter^#(s(s(X)), cons(Y, Z)) ->
    c_8(if^#(divides(s(s(X)), Y),
             filter(s(s(X)), Z),
             cons(Y, filter(X, sieve(Y)))),
        filter^#(s(s(X)), Z),
        filter^#(X, sieve(Y)),
        sieve^#(Y)) }
Weak Trs:
  { primes() -> sieve(from(s(s(0()))))
  , sieve(cons(X, Y)) -> cons(X, filter(X, sieve(Y)))
  , from(X) -> cons(X, from(s(X)))
  , head(cons(X, Y)) -> X
  , tail(cons(X, Y)) -> Y
  , if(true(), X, Y) -> X
  , if(false(), X, Y) -> Y
  , filter(s(s(X)), cons(Y, Z)) ->
    if(divides(s(s(X)), Y),
       filter(s(s(X)), Z),
       cons(Y, filter(X, sieve(Y)))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:

  { filter^#(s(s(X)), cons(Y, Z)) ->
    c_8(if^#(divides(s(s(X)), Y),
             filter(s(s(X)), Z),
             cons(Y, filter(X, sieve(Y)))),
        filter^#(s(s(X)), Z),
        filter^#(X, sieve(Y)),
        sieve^#(Y)) }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { primes^#() -> c_1(sieve^#(from(s(s(0())))), from^#(s(s(0()))))
  , sieve^#(cons(X, Y)) -> c_2(filter^#(X, sieve(Y)), sieve^#(Y))
  , from^#(X) -> c_3(from^#(s(X)))
  , filter^#(s(s(X)), cons(Y, Z)) ->
    c_4(filter^#(s(s(X)), Z), filter^#(X, sieve(Y)), sieve^#(Y)) }
Weak Trs:
  { primes() -> sieve(from(s(s(0()))))
  , sieve(cons(X, Y)) -> cons(X, filter(X, sieve(Y)))
  , from(X) -> cons(X, from(s(X)))
  , head(cons(X, Y)) -> X
  , tail(cons(X, Y)) -> Y
  , if(true(), X, Y) -> X
  , if(false(), X, Y) -> Y
  , filter(s(s(X)), cons(Y, Z)) ->
    if(divides(s(s(X)), Y),
       filter(s(s(X)), Z),
       cons(Y, filter(X, sieve(Y)))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { sieve(cons(X, Y)) -> cons(X, filter(X, sieve(Y)))
    , from(X) -> cons(X, from(s(X)))
    , if(true(), X, Y) -> X
    , if(false(), X, Y) -> Y
    , filter(s(s(X)), cons(Y, Z)) ->
      if(divides(s(s(X)), Y),
         filter(s(s(X)), Z),
         cons(Y, filter(X, sieve(Y)))) }

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict DPs:
  { primes^#() -> c_1(sieve^#(from(s(s(0())))), from^#(s(s(0()))))
  , sieve^#(cons(X, Y)) -> c_2(filter^#(X, sieve(Y)), sieve^#(Y))
  , from^#(X) -> c_3(from^#(s(X)))
  , filter^#(s(s(X)), cons(Y, Z)) ->
    c_4(filter^#(s(s(X)), Z), filter^#(X, sieve(Y)), sieve^#(Y)) }
Weak Trs:
  { sieve(cons(X, Y)) -> cons(X, filter(X, sieve(Y)))
  , from(X) -> cons(X, from(s(X)))
  , if(true(), X, Y) -> X
  , if(false(), X, Y) -> Y
  , filter(s(s(X)), cons(Y, Z)) ->
    if(divides(s(s(X)), Y),
       filter(s(s(X)), Z),
       cons(Y, filter(X, sieve(Y)))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..