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 The input cannot be shown compatible Arrrr..