MAYBE 808.27/298.33 MAYBE 808.27/298.33 808.27/298.33 We are left with following problem, upon which TcT provides the 808.27/298.33 certificate MAYBE. 808.27/298.33 808.27/298.33 Strict Trs: 808.27/298.33 { fib(0()) -> 0() 808.27/298.33 , fib(s(0())) -> s(0()) 808.27/298.33 , fib(s(s(x))) -> +(fib(s(x)), fib(x)) 808.27/298.33 , +(x, 0()) -> x 808.27/298.33 , +(x, s(y)) -> s(+(x, y)) } 808.27/298.33 Obligation: 808.27/298.33 innermost runtime complexity 808.27/298.33 Answer: 808.27/298.33 MAYBE 808.27/298.33 808.27/298.33 None of the processors succeeded. 808.27/298.33 808.27/298.33 Details of failed attempt(s): 808.27/298.33 ----------------------------- 808.27/298.33 1) 'empty' failed due to the following reason: 808.27/298.33 808.27/298.33 Empty strict component of the problem is NOT empty. 808.27/298.33 808.27/298.33 2) 'Best' failed due to the following reason: 808.27/298.33 808.27/298.33 None of the processors succeeded. 808.27/298.33 808.27/298.33 Details of failed attempt(s): 808.27/298.33 ----------------------------- 808.27/298.33 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 808.27/298.33 following reason: 808.27/298.33 808.27/298.33 Computation stopped due to timeout after 297.0 seconds. 808.27/298.33 808.27/298.33 2) 'Best' failed due to the following reason: 808.27/298.33 808.27/298.33 None of the processors succeeded. 808.27/298.33 808.27/298.33 Details of failed attempt(s): 808.27/298.33 ----------------------------- 808.27/298.33 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 808.27/298.33 seconds)' failed due to the following reason: 808.27/298.33 808.27/298.33 The weightgap principle applies (using the following nonconstant 808.27/298.33 growth matrix-interpretation) 808.27/298.33 808.27/298.33 The following argument positions are usable: 808.27/298.33 Uargs(s) = {1}, Uargs(+) = {1, 2} 808.27/298.33 808.27/298.33 TcT has computed the following matrix interpretation satisfying 808.27/298.33 not(EDA) and not(IDA(1)). 808.27/298.33 808.27/298.33 [fib](x1) = [0] 808.27/298.33 808.27/298.33 [0] = [4] 808.27/298.33 808.27/298.33 [s](x1) = [1] x1 + [0] 808.27/298.33 808.27/298.33 [+](x1, x2) = [1] x1 + [1] x2 + [0] 808.27/298.33 808.27/298.33 The order satisfies the following ordering constraints: 808.27/298.33 808.27/298.33 [fib(0())] = [0] 808.27/298.33 ? [4] 808.27/298.33 = [0()] 808.27/298.33 808.27/298.33 [fib(s(0()))] = [0] 808.27/298.33 ? [4] 808.27/298.33 = [s(0())] 808.27/298.33 808.27/298.33 [fib(s(s(x)))] = [0] 808.27/298.33 >= [0] 808.27/298.33 = [+(fib(s(x)), fib(x))] 808.27/298.33 808.27/298.33 [+(x, 0())] = [1] x + [4] 808.27/298.33 > [1] x + [0] 808.27/298.33 = [x] 808.27/298.33 808.27/298.33 [+(x, s(y))] = [1] x + [1] y + [0] 808.27/298.33 >= [1] x + [1] y + [0] 808.27/298.33 = [s(+(x, y))] 808.27/298.33 808.27/298.33 808.27/298.33 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 808.27/298.33 808.27/298.33 We are left with following problem, upon which TcT provides the 808.27/298.33 certificate MAYBE. 808.27/298.33 808.27/298.33 Strict Trs: 808.27/298.33 { fib(0()) -> 0() 808.27/298.33 , fib(s(0())) -> s(0()) 808.27/298.33 , fib(s(s(x))) -> +(fib(s(x)), fib(x)) 808.27/298.33 , +(x, s(y)) -> s(+(x, y)) } 808.27/298.33 Weak Trs: { +(x, 0()) -> x } 808.27/298.33 Obligation: 808.27/298.33 innermost runtime complexity 808.27/298.33 Answer: 808.27/298.33 MAYBE 808.27/298.33 808.27/298.33 The weightgap principle applies (using the following nonconstant 808.27/298.33 growth matrix-interpretation) 808.27/298.33 808.27/298.33 The following argument positions are usable: 808.27/298.33 Uargs(s) = {1}, Uargs(+) = {1, 2} 808.27/298.33 808.27/298.33 TcT has computed the following matrix interpretation satisfying 808.27/298.33 not(EDA) and not(IDA(1)). 808.27/298.33 808.27/298.33 [fib](x1) = [4] 808.27/298.33 808.27/298.33 [0] = [3] 808.27/298.33 808.27/298.33 [s](x1) = [1] x1 + [0] 808.27/298.33 808.27/298.33 [+](x1, x2) = [1] x1 + [1] x2 + [0] 808.27/298.33 808.27/298.33 The order satisfies the following ordering constraints: 808.27/298.33 808.27/298.33 [fib(0())] = [4] 808.27/298.33 > [3] 808.27/298.33 = [0()] 808.27/298.33 808.27/298.33 [fib(s(0()))] = [4] 808.27/298.33 > [3] 808.27/298.33 = [s(0())] 808.27/298.33 808.27/298.33 [fib(s(s(x)))] = [4] 808.27/298.33 ? [8] 808.27/298.33 = [+(fib(s(x)), fib(x))] 808.27/298.33 808.27/298.33 [+(x, 0())] = [1] x + [3] 808.27/298.33 > [1] x + [0] 808.27/298.33 = [x] 808.27/298.33 808.27/298.33 [+(x, s(y))] = [1] x + [1] y + [0] 808.27/298.33 >= [1] x + [1] y + [0] 808.27/298.33 = [s(+(x, y))] 808.27/298.33 808.27/298.33 808.27/298.33 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 808.27/298.33 808.27/298.33 We are left with following problem, upon which TcT provides the 808.27/298.33 certificate MAYBE. 808.27/298.33 808.27/298.33 Strict Trs: 808.27/298.33 { fib(s(s(x))) -> +(fib(s(x)), fib(x)) 808.27/298.33 , +(x, s(y)) -> s(+(x, y)) } 808.27/298.33 Weak Trs: 808.27/298.33 { fib(0()) -> 0() 808.27/298.33 , fib(s(0())) -> s(0()) 808.27/298.33 , +(x, 0()) -> x } 808.27/298.33 Obligation: 808.27/298.33 innermost runtime complexity 808.27/298.33 Answer: 808.27/298.33 MAYBE 808.27/298.33 808.27/298.33 None of the processors succeeded. 808.27/298.33 808.27/298.33 Details of failed attempt(s): 808.27/298.33 ----------------------------- 808.27/298.33 1) 'empty' failed due to the following reason: 808.27/298.33 808.27/298.33 Empty strict component of the problem is NOT empty. 808.27/298.33 808.27/298.33 2) 'With Problem ...' failed due to the following reason: 808.27/298.33 808.27/298.33 None of the processors succeeded. 808.27/298.33 808.27/298.33 Details of failed attempt(s): 808.27/298.33 ----------------------------- 808.27/298.33 1) 'empty' failed due to the following reason: 808.27/298.33 808.27/298.33 Empty strict component of the problem is NOT empty. 808.27/298.33 808.27/298.33 2) 'Fastest' failed due to the following reason: 808.27/298.33 808.27/298.33 None of the processors succeeded. 808.27/298.33 808.27/298.33 Details of failed attempt(s): 808.27/298.33 ----------------------------- 808.27/298.33 1) 'With Problem ...' failed due to the following reason: 808.27/298.33 808.27/298.33 None of the processors succeeded. 808.27/298.33 808.27/298.33 Details of failed attempt(s): 808.27/298.33 ----------------------------- 808.27/298.33 1) 'empty' failed due to the following reason: 808.27/298.33 808.27/298.33 Empty strict component of the problem is NOT empty. 808.27/298.33 808.27/298.33 2) 'With Problem ...' failed due to the following reason: 808.27/298.33 808.27/298.33 Empty strict component of the problem is NOT empty. 808.27/298.33 808.27/298.33 808.27/298.33 2) 'With Problem ...' failed due to the following reason: 808.27/298.33 808.27/298.33 None of the processors succeeded. 808.27/298.33 808.27/298.33 Details of failed attempt(s): 808.27/298.33 ----------------------------- 808.27/298.33 1) 'empty' failed due to the following reason: 808.27/298.33 808.27/298.33 Empty strict component of the problem is NOT empty. 808.27/298.33 808.27/298.33 2) 'With Problem ...' failed due to the following reason: 808.27/298.33 808.27/298.33 None of the processors succeeded. 808.27/298.33 808.27/298.33 Details of failed attempt(s): 808.27/298.33 ----------------------------- 808.27/298.33 1) 'empty' failed due to the following reason: 808.27/298.33 808.27/298.33 Empty strict component of the problem is NOT empty. 808.27/298.33 808.27/298.33 2) 'With Problem ...' failed due to the following reason: 808.27/298.33 808.27/298.33 None of the processors succeeded. 808.27/298.33 808.27/298.33 Details of failed attempt(s): 808.27/298.33 ----------------------------- 808.27/298.33 1) 'empty' failed due to the following reason: 808.27/298.33 808.27/298.33 Empty strict component of the problem is NOT empty. 808.27/298.33 808.27/298.33 2) 'With Problem ...' failed due to the following reason: 808.27/298.33 808.27/298.33 Empty strict component of the problem is NOT empty. 808.27/298.33 808.27/298.33 808.27/298.33 808.27/298.33 808.27/298.33 808.27/298.33 808.27/298.33 808.27/298.33 2) 'Best' failed due to the following reason: 808.27/298.33 808.27/298.33 None of the processors succeeded. 808.27/298.33 808.27/298.33 Details of failed attempt(s): 808.27/298.33 ----------------------------- 808.27/298.33 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 808.27/298.33 to the following reason: 808.27/298.33 808.27/298.33 The input cannot be shown compatible 808.27/298.33 808.27/298.33 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 808.27/298.33 following reason: 808.27/298.33 808.27/298.33 The input cannot be shown compatible 808.27/298.33 808.27/298.33 808.27/298.33 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 808.27/298.33 failed due to the following reason: 808.27/298.33 808.27/298.33 None of the processors succeeded. 808.27/298.33 808.27/298.33 Details of failed attempt(s): 808.27/298.33 ----------------------------- 808.27/298.33 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 808.27/298.33 failed due to the following reason: 808.27/298.33 808.27/298.33 match-boundness of the problem could not be verified. 808.27/298.33 808.27/298.33 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 808.27/298.33 failed due to the following reason: 808.27/298.33 808.27/298.33 match-boundness of the problem could not be verified. 808.27/298.33 808.27/298.33 808.27/298.33 808.27/298.33 808.27/298.33 808.27/298.33 Arrrr.. 808.68/298.69 EOF