MAYBE 377.88/216.21 MAYBE 377.88/216.21 377.88/216.21 We are left with following problem, upon which TcT provides the 377.88/216.21 certificate MAYBE. 377.88/216.21 377.88/216.21 Strict Trs: 377.88/216.21 { plus(0(), y) -> y 377.88/216.21 , plus(s(x), y) -> s(plus(x, y)) 377.88/216.21 , lt(x, 0()) -> false() 377.88/216.21 , lt(0(), s(y)) -> true() 377.88/216.21 , lt(s(x), s(y)) -> lt(x, y) 377.88/216.21 , fib(x) -> fibiter(x, 0(), 0(), s(0())) 377.88/216.21 , fibiter(b, c, x, y) -> if(lt(c, b), b, c, x, y) 377.88/216.21 , if(true(), b, c, x, y) -> fibiter(b, s(c), y, plus(x, y)) 377.88/216.21 , if(false(), b, c, x, y) -> x } 377.88/216.21 Obligation: 377.88/216.21 runtime complexity 377.88/216.21 Answer: 377.88/216.21 MAYBE 377.88/216.21 377.88/216.21 None of the processors succeeded. 377.88/216.21 377.88/216.21 Details of failed attempt(s): 377.88/216.21 ----------------------------- 377.88/216.21 1) 'Best' failed due to the following reason: 377.88/216.21 377.88/216.21 None of the processors succeeded. 377.88/216.21 377.88/216.21 Details of failed attempt(s): 377.88/216.21 ----------------------------- 377.88/216.21 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 377.88/216.21 seconds)' failed due to the following reason: 377.88/216.21 377.88/216.21 None of the processors succeeded. 377.88/216.21 377.88/216.21 Details of failed attempt(s): 377.88/216.21 ----------------------------- 377.88/216.21 1) 'empty' failed due to the following reason: 377.88/216.21 377.88/216.21 Empty strict component of the problem is NOT empty. 377.88/216.21 377.88/216.21 2) 'With Problem ...' failed due to the following reason: 377.88/216.21 377.88/216.21 None of the processors succeeded. 377.88/216.21 377.88/216.21 Details of failed attempt(s): 377.88/216.21 ----------------------------- 377.88/216.21 1) 'empty' failed due to the following reason: 377.88/216.21 377.88/216.21 Empty strict component of the problem is NOT empty. 377.88/216.21 377.88/216.21 2) 'Fastest' failed due to the following reason: 377.88/216.21 377.88/216.21 None of the processors succeeded. 377.88/216.21 377.88/216.21 Details of failed attempt(s): 377.88/216.21 ----------------------------- 377.88/216.21 1) 'With Problem ...' failed due to the following reason: 377.88/216.21 377.88/216.21 None of the processors succeeded. 377.88/216.21 377.88/216.21 Details of failed attempt(s): 377.88/216.21 ----------------------------- 377.88/216.21 1) 'empty' failed due to the following reason: 377.88/216.21 377.88/216.21 Empty strict component of the problem is NOT empty. 377.88/216.21 377.88/216.21 2) 'With Problem ...' failed due to the following reason: 377.88/216.21 377.88/216.21 Empty strict component of the problem is NOT empty. 377.88/216.21 377.88/216.21 377.88/216.21 2) 'With Problem ...' failed due to the following reason: 377.88/216.21 377.88/216.21 None of the processors succeeded. 377.88/216.21 377.88/216.21 Details of failed attempt(s): 377.88/216.21 ----------------------------- 377.88/216.21 1) 'empty' failed due to the following reason: 377.88/216.21 377.88/216.21 Empty strict component of the problem is NOT empty. 377.88/216.21 377.88/216.21 2) 'With Problem ...' failed due to the following reason: 377.88/216.21 377.88/216.21 None of the processors succeeded. 377.88/216.21 377.88/216.21 Details of failed attempt(s): 377.88/216.21 ----------------------------- 377.88/216.21 1) 'empty' failed due to the following reason: 377.88/216.21 377.88/216.21 Empty strict component of the problem is NOT empty. 377.88/216.21 377.88/216.21 2) 'With Problem ...' failed due to the following reason: 377.88/216.21 377.88/216.21 None of the processors succeeded. 377.88/216.21 377.88/216.21 Details of failed attempt(s): 377.88/216.21 ----------------------------- 377.88/216.21 1) 'empty' failed due to the following reason: 377.88/216.21 377.88/216.21 Empty strict component of the problem is NOT empty. 377.88/216.21 377.88/216.21 2) 'With Problem ...' failed due to the following reason: 377.88/216.21 377.88/216.21 Empty strict component of the problem is NOT empty. 377.88/216.21 377.88/216.21 377.88/216.21 377.88/216.21 377.88/216.21 377.88/216.21 377.88/216.21 377.88/216.21 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 377.88/216.21 failed due to the following reason: 377.88/216.21 377.88/216.21 None of the processors succeeded. 377.88/216.21 377.88/216.21 Details of failed attempt(s): 377.88/216.21 ----------------------------- 377.88/216.21 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 377.88/216.21 failed due to the following reason: 377.88/216.21 377.88/216.21 match-boundness of the problem could not be verified. 377.88/216.21 377.88/216.21 2) 'Bounds with minimal-enrichment and initial automaton 'match'' 377.88/216.21 failed due to the following reason: 377.88/216.21 377.88/216.21 match-boundness of the problem could not be verified. 377.88/216.21 377.88/216.21 377.88/216.21 3) 'Best' failed due to the following reason: 377.88/216.21 377.88/216.21 None of the processors succeeded. 377.88/216.21 377.88/216.21 Details of failed attempt(s): 377.88/216.21 ----------------------------- 377.88/216.21 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 377.88/216.21 following reason: 377.88/216.21 377.88/216.21 The processor is inapplicable, reason: 377.88/216.21 Processor only applicable for innermost runtime complexity analysis 377.88/216.21 377.88/216.21 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 377.88/216.21 to the following reason: 377.88/216.21 377.88/216.21 The processor is inapplicable, reason: 377.88/216.21 Processor only applicable for innermost runtime complexity analysis 377.88/216.21 377.88/216.21 377.88/216.21 377.88/216.21 2) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 377.88/216.21 the following reason: 377.88/216.21 377.88/216.21 We add the following weak dependency pairs: 377.88/216.21 377.88/216.21 Strict DPs: 377.88/216.21 { plus^#(0(), y) -> c_1(y) 377.88/216.21 , plus^#(s(x), y) -> c_2(plus^#(x, y)) 377.88/216.21 , lt^#(x, 0()) -> c_3() 377.88/216.21 , lt^#(0(), s(y)) -> c_4() 377.88/216.21 , lt^#(s(x), s(y)) -> c_5(lt^#(x, y)) 377.88/216.21 , fib^#(x) -> c_6(fibiter^#(x, 0(), 0(), s(0()))) 377.88/216.21 , fibiter^#(b, c, x, y) -> c_7(if^#(lt(c, b), b, c, x, y)) 377.88/216.21 , if^#(true(), b, c, x, y) -> 377.88/216.21 c_8(fibiter^#(b, s(c), y, plus(x, y))) 377.88/216.21 , if^#(false(), b, c, x, y) -> c_9(x) } 377.88/216.21 377.88/216.21 and mark the set of starting terms. 377.88/216.21 377.88/216.21 We are left with following problem, upon which TcT provides the 377.88/216.21 certificate MAYBE. 377.88/216.21 377.88/216.21 Strict DPs: 377.88/216.21 { plus^#(0(), y) -> c_1(y) 377.88/216.21 , plus^#(s(x), y) -> c_2(plus^#(x, y)) 377.88/216.21 , lt^#(x, 0()) -> c_3() 377.88/216.21 , lt^#(0(), s(y)) -> c_4() 377.88/216.21 , lt^#(s(x), s(y)) -> c_5(lt^#(x, y)) 377.88/216.21 , fib^#(x) -> c_6(fibiter^#(x, 0(), 0(), s(0()))) 377.88/216.21 , fibiter^#(b, c, x, y) -> c_7(if^#(lt(c, b), b, c, x, y)) 377.88/216.21 , if^#(true(), b, c, x, y) -> 377.88/216.21 c_8(fibiter^#(b, s(c), y, plus(x, y))) 377.88/216.21 , if^#(false(), b, c, x, y) -> c_9(x) } 377.88/216.21 Strict Trs: 377.88/216.21 { plus(0(), y) -> y 377.88/216.21 , plus(s(x), y) -> s(plus(x, y)) 377.88/216.21 , lt(x, 0()) -> false() 377.88/216.21 , lt(0(), s(y)) -> true() 377.88/216.21 , lt(s(x), s(y)) -> lt(x, y) 377.88/216.21 , fib(x) -> fibiter(x, 0(), 0(), s(0())) 377.88/216.21 , fibiter(b, c, x, y) -> if(lt(c, b), b, c, x, y) 377.88/216.21 , if(true(), b, c, x, y) -> fibiter(b, s(c), y, plus(x, y)) 377.88/216.21 , if(false(), b, c, x, y) -> x } 377.88/216.21 Obligation: 377.88/216.21 runtime complexity 377.88/216.21 Answer: 377.88/216.21 MAYBE 377.88/216.21 377.88/216.21 We estimate the number of application of {3,4} by applications of 377.88/216.21 Pre({3,4}) = {1,5,9}. Here rules are labeled as follows: 377.88/216.21 377.88/216.21 DPs: 377.88/216.21 { 1: plus^#(0(), y) -> c_1(y) 377.88/216.21 , 2: plus^#(s(x), y) -> c_2(plus^#(x, y)) 377.88/216.21 , 3: lt^#(x, 0()) -> c_3() 377.88/216.21 , 4: lt^#(0(), s(y)) -> c_4() 377.88/216.21 , 5: lt^#(s(x), s(y)) -> c_5(lt^#(x, y)) 377.88/216.21 , 6: fib^#(x) -> c_6(fibiter^#(x, 0(), 0(), s(0()))) 377.88/216.21 , 7: fibiter^#(b, c, x, y) -> c_7(if^#(lt(c, b), b, c, x, y)) 377.88/216.21 , 8: if^#(true(), b, c, x, y) -> 377.88/216.21 c_8(fibiter^#(b, s(c), y, plus(x, y))) 377.88/216.21 , 9: if^#(false(), b, c, x, y) -> c_9(x) } 377.88/216.21 377.88/216.21 We are left with following problem, upon which TcT provides the 377.88/216.21 certificate MAYBE. 377.88/216.21 377.88/216.21 Strict DPs: 377.88/216.21 { plus^#(0(), y) -> c_1(y) 377.88/216.21 , plus^#(s(x), y) -> c_2(plus^#(x, y)) 377.88/216.21 , lt^#(s(x), s(y)) -> c_5(lt^#(x, y)) 377.88/216.21 , fib^#(x) -> c_6(fibiter^#(x, 0(), 0(), s(0()))) 377.88/216.21 , fibiter^#(b, c, x, y) -> c_7(if^#(lt(c, b), b, c, x, y)) 377.88/216.21 , if^#(true(), b, c, x, y) -> 377.88/216.21 c_8(fibiter^#(b, s(c), y, plus(x, y))) 377.88/216.21 , if^#(false(), b, c, x, y) -> c_9(x) } 377.88/216.21 Strict Trs: 377.88/216.21 { plus(0(), y) -> y 377.88/216.21 , plus(s(x), y) -> s(plus(x, y)) 377.88/216.21 , lt(x, 0()) -> false() 377.88/216.21 , lt(0(), s(y)) -> true() 377.88/216.21 , lt(s(x), s(y)) -> lt(x, y) 377.88/216.21 , fib(x) -> fibiter(x, 0(), 0(), s(0())) 377.88/216.21 , fibiter(b, c, x, y) -> if(lt(c, b), b, c, x, y) 377.88/216.21 , if(true(), b, c, x, y) -> fibiter(b, s(c), y, plus(x, y)) 377.88/216.21 , if(false(), b, c, x, y) -> x } 377.88/216.21 Weak DPs: 377.88/216.21 { lt^#(x, 0()) -> c_3() 377.88/216.21 , lt^#(0(), s(y)) -> c_4() } 377.88/216.21 Obligation: 377.88/216.21 runtime complexity 377.88/216.21 Answer: 377.88/216.21 MAYBE 377.88/216.21 377.88/216.21 Empty strict component of the problem is NOT empty. 377.88/216.21 377.88/216.21 377.88/216.21 Arrrr.. 378.08/216.49 EOF