MAYBE 755.49/297.11 MAYBE 755.49/297.11 755.49/297.11 We are left with following problem, upon which TcT provides the 755.49/297.11 certificate MAYBE. 755.49/297.11 755.49/297.11 Strict Trs: 755.49/297.11 { lt(x, 0()) -> false() 755.49/297.11 , lt(0(), s(x)) -> true() 755.49/297.11 , lt(s(x), s(y)) -> lt(x, y) 755.49/297.11 , fibo(0()) -> fib(0()) 755.49/297.11 , fibo(s(0())) -> fib(s(0())) 755.49/297.11 , fibo(s(s(x))) -> sum(fibo(s(x)), fibo(x)) 755.49/297.11 , fib(0()) -> s(0()) 755.49/297.11 , fib(s(0())) -> s(0()) 755.49/297.11 , fib(s(s(x))) -> if(true(), 0(), s(s(x)), 0(), 0()) 755.49/297.11 , sum(x, 0()) -> x 755.49/297.11 , sum(x, s(y)) -> s(sum(x, y)) 755.49/297.11 , if(true(), c, s(s(x)), a, b) -> 755.49/297.11 if(lt(s(c), s(s(x))), s(c), s(s(x)), b, c) 755.49/297.11 , if(false(), c, s(s(x)), a, b) -> sum(fibo(a), fibo(b)) } 755.49/297.11 Obligation: 755.49/297.11 innermost runtime complexity 755.49/297.11 Answer: 755.49/297.11 MAYBE 755.49/297.11 755.49/297.11 None of the processors succeeded. 755.49/297.11 755.49/297.11 Details of failed attempt(s): 755.49/297.11 ----------------------------- 755.49/297.11 1) 'empty' failed due to the following reason: 755.49/297.11 755.49/297.11 Empty strict component of the problem is NOT empty. 755.49/297.11 755.49/297.11 2) 'Best' failed due to the following reason: 755.49/297.11 755.49/297.11 None of the processors succeeded. 755.49/297.11 755.49/297.11 Details of failed attempt(s): 755.49/297.11 ----------------------------- 755.49/297.11 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 755.49/297.11 following reason: 755.49/297.11 755.49/297.11 Computation stopped due to timeout after 297.0 seconds. 755.49/297.11 755.49/297.11 2) 'Best' failed due to the following reason: 755.49/297.11 755.49/297.11 None of the processors succeeded. 755.49/297.11 755.49/297.11 Details of failed attempt(s): 755.49/297.11 ----------------------------- 755.49/297.11 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 755.49/297.11 seconds)' failed due to the following reason: 755.49/297.11 755.49/297.11 Computation stopped due to timeout after 148.0 seconds. 755.49/297.11 755.49/297.11 2) 'Best' failed due to the following reason: 755.49/297.11 755.49/297.11 None of the processors succeeded. 755.49/297.11 755.49/297.11 Details of failed attempt(s): 755.49/297.11 ----------------------------- 755.49/297.11 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 755.49/297.11 to the following reason: 755.49/297.11 755.49/297.11 The input cannot be shown compatible 755.49/297.11 755.49/297.11 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 755.49/297.11 following reason: 755.49/297.11 755.49/297.11 The input cannot be shown compatible 755.49/297.11 755.49/297.11 755.49/297.11 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 755.49/297.11 failed due to the following reason: 755.49/297.11 755.49/297.11 None of the processors succeeded. 755.49/297.11 755.49/297.11 Details of failed attempt(s): 755.49/297.11 ----------------------------- 755.49/297.11 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 755.49/297.11 failed due to the following reason: 755.49/297.11 755.49/297.11 match-boundness of the problem could not be verified. 755.49/297.11 755.49/297.11 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 755.49/297.11 failed due to the following reason: 755.49/297.11 755.49/297.11 match-boundness of the problem could not be verified. 755.49/297.11 755.49/297.11 755.49/297.11 755.49/297.11 755.49/297.11 755.49/297.11 Arrrr.. 755.60/297.26 EOF