MAYBE 1037.86/297.03 MAYBE 1037.86/297.03 1037.86/297.03 We are left with following problem, upon which TcT provides the 1037.86/297.03 certificate MAYBE. 1037.86/297.03 1037.86/297.03 Strict Trs: 1037.86/297.03 { a__primes() -> a__sieve(a__from(s(s(0())))) 1037.86/297.03 , a__primes() -> primes() 1037.86/297.03 , a__sieve(X) -> sieve(X) 1037.86/297.03 , a__sieve(cons(X, Y)) -> cons(mark(X), filter(X, sieve(Y))) 1037.86/297.03 , a__from(X) -> cons(mark(X), from(s(X))) 1037.86/297.03 , a__from(X) -> from(X) 1037.86/297.03 , mark(s(X)) -> s(mark(X)) 1037.86/297.03 , mark(0()) -> 0() 1037.86/297.03 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 1037.86/297.03 , mark(from(X)) -> a__from(mark(X)) 1037.86/297.03 , mark(true()) -> true() 1037.86/297.03 , mark(false()) -> false() 1037.86/297.03 , mark(divides(X1, X2)) -> divides(mark(X1), mark(X2)) 1037.86/297.03 , mark(filter(X1, X2)) -> a__filter(mark(X1), mark(X2)) 1037.86/297.03 , mark(sieve(X)) -> a__sieve(mark(X)) 1037.86/297.03 , mark(primes()) -> a__primes() 1037.86/297.03 , mark(head(X)) -> a__head(mark(X)) 1037.86/297.03 , mark(tail(X)) -> a__tail(mark(X)) 1037.86/297.03 , mark(if(X1, X2, X3)) -> a__if(mark(X1), X2, X3) 1037.86/297.03 , a__head(X) -> head(X) 1037.86/297.03 , a__head(cons(X, Y)) -> mark(X) 1037.86/297.03 , a__tail(X) -> tail(X) 1037.86/297.03 , a__tail(cons(X, Y)) -> mark(Y) 1037.86/297.03 , a__if(X1, X2, X3) -> if(X1, X2, X3) 1037.86/297.03 , a__if(true(), X, Y) -> mark(X) 1037.86/297.03 , a__if(false(), X, Y) -> mark(Y) 1037.86/297.03 , a__filter(X1, X2) -> filter(X1, X2) 1037.86/297.03 , a__filter(s(s(X)), cons(Y, Z)) -> 1037.86/297.03 a__if(divides(s(s(mark(X))), mark(Y)), 1037.86/297.03 filter(s(s(X)), Z), 1037.86/297.03 cons(Y, filter(X, sieve(Y)))) } 1037.86/297.03 Obligation: 1037.86/297.03 innermost runtime complexity 1037.86/297.03 Answer: 1037.86/297.03 MAYBE 1037.86/297.03 1037.86/297.03 None of the processors succeeded. 1037.86/297.03 1037.86/297.03 Details of failed attempt(s): 1037.86/297.03 ----------------------------- 1037.86/297.03 1) 'empty' failed due to the following reason: 1037.86/297.03 1037.86/297.03 Empty strict component of the problem is NOT empty. 1037.86/297.03 1037.86/297.03 2) 'Best' failed due to the following reason: 1037.86/297.03 1037.86/297.03 None of the processors succeeded. 1037.86/297.03 1037.86/297.03 Details of failed attempt(s): 1037.86/297.03 ----------------------------- 1037.86/297.03 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1037.86/297.03 following reason: 1037.86/297.03 1037.86/297.03 Computation stopped due to timeout after 297.0 seconds. 1037.86/297.03 1037.86/297.03 2) 'Best' failed due to the following reason: 1037.86/297.03 1037.86/297.03 None of the processors succeeded. 1037.86/297.03 1037.86/297.03 Details of failed attempt(s): 1037.86/297.03 ----------------------------- 1037.86/297.03 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1037.86/297.03 seconds)' failed due to the following reason: 1037.86/297.03 1037.86/297.03 Computation stopped due to timeout after 148.0 seconds. 1037.86/297.03 1037.86/297.03 2) 'Best' failed due to the following reason: 1037.86/297.03 1037.86/297.03 None of the processors succeeded. 1037.86/297.03 1037.86/297.03 Details of failed attempt(s): 1037.86/297.03 ----------------------------- 1037.86/297.03 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1037.86/297.03 following reason: 1037.86/297.03 1037.86/297.03 The input cannot be shown compatible 1037.86/297.03 1037.86/297.03 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1037.86/297.03 to the following reason: 1037.86/297.03 1037.86/297.03 The input cannot be shown compatible 1037.86/297.03 1037.86/297.03 1037.86/297.03 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1037.86/297.03 failed due to the following reason: 1037.86/297.03 1037.86/297.03 None of the processors succeeded. 1037.86/297.03 1037.86/297.03 Details of failed attempt(s): 1037.86/297.03 ----------------------------- 1037.86/297.03 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1037.86/297.03 failed due to the following reason: 1037.86/297.03 1037.86/297.03 match-boundness of the problem could not be verified. 1037.86/297.03 1037.86/297.03 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1037.86/297.03 failed due to the following reason: 1037.86/297.03 1037.86/297.03 match-boundness of the problem could not be verified. 1037.86/297.03 1037.86/297.03 1037.86/297.03 1037.86/297.03 1037.86/297.03 1037.86/297.03 Arrrr.. 1040.91/300.39 EOF