MAYBE 1083.42/298.59 MAYBE 1083.42/298.59 1083.42/298.59 We are left with following problem, upon which TcT provides the 1083.42/298.59 certificate MAYBE. 1083.42/298.59 1083.42/298.59 Strict Trs: 1083.42/298.59 { fib(0()) -> 0() 1083.42/298.59 , fib(s(0())) -> s(0()) 1083.42/298.59 , fib(s(s(x))) -> +(fib(s(x)), fib(x)) 1083.42/298.59 , +(x, 0()) -> x 1083.42/298.59 , +(x, s(y)) -> s(+(x, y)) } 1083.42/298.59 Obligation: 1083.42/298.59 runtime complexity 1083.42/298.59 Answer: 1083.42/298.59 MAYBE 1083.42/298.59 1083.42/298.59 None of the processors succeeded. 1083.42/298.59 1083.42/298.59 Details of failed attempt(s): 1083.42/298.59 ----------------------------- 1083.42/298.59 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1083.42/298.59 following reason: 1083.42/298.59 1083.42/298.59 Computation stopped due to timeout after 297.0 seconds. 1083.42/298.59 1083.42/298.59 2) 'Best' failed due to the following reason: 1083.42/298.59 1083.42/298.59 None of the processors succeeded. 1083.42/298.59 1083.42/298.59 Details of failed attempt(s): 1083.42/298.59 ----------------------------- 1083.42/298.59 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1083.42/298.59 seconds)' failed due to the following reason: 1083.42/298.59 1083.42/298.59 The weightgap principle applies (using the following nonconstant 1083.42/298.59 growth matrix-interpretation) 1083.42/298.59 1083.42/298.59 The following argument positions are usable: 1083.42/298.59 Uargs(s) = {1}, Uargs(+) = {1, 2} 1083.42/298.59 1083.42/298.59 TcT has computed the following matrix interpretation satisfying 1083.42/298.59 not(EDA) and not(IDA(1)). 1083.42/298.59 1083.42/298.59 [fib](x1) = [0] 1083.42/298.59 1083.42/298.59 [0] = [4] 1083.42/298.59 1083.42/298.59 [s](x1) = [1] x1 + [0] 1083.42/298.59 1083.42/298.59 [+](x1, x2) = [1] x1 + [1] x2 + [0] 1083.42/298.59 1083.42/298.59 The order satisfies the following ordering constraints: 1083.42/298.59 1083.42/298.59 [fib(0())] = [0] 1083.42/298.59 ? [4] 1083.42/298.59 = [0()] 1083.42/298.59 1083.42/298.59 [fib(s(0()))] = [0] 1083.42/298.59 ? [4] 1083.42/298.59 = [s(0())] 1083.42/298.59 1083.42/298.59 [fib(s(s(x)))] = [0] 1083.42/298.59 >= [0] 1083.42/298.59 = [+(fib(s(x)), fib(x))] 1083.42/298.59 1083.42/298.59 [+(x, 0())] = [1] x + [4] 1083.42/298.59 > [1] x + [0] 1083.42/298.59 = [x] 1083.42/298.59 1083.42/298.59 [+(x, s(y))] = [1] x + [1] y + [0] 1083.42/298.59 >= [1] x + [1] y + [0] 1083.42/298.59 = [s(+(x, y))] 1083.42/298.59 1083.42/298.59 1083.42/298.59 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 1083.42/298.59 1083.42/298.59 We are left with following problem, upon which TcT provides the 1083.42/298.59 certificate MAYBE. 1083.42/298.59 1083.42/298.59 Strict Trs: 1083.42/298.59 { fib(0()) -> 0() 1083.42/298.59 , fib(s(0())) -> s(0()) 1083.42/298.59 , fib(s(s(x))) -> +(fib(s(x)), fib(x)) 1083.42/298.59 , +(x, s(y)) -> s(+(x, y)) } 1083.42/298.59 Weak Trs: { +(x, 0()) -> x } 1083.42/298.59 Obligation: 1083.42/298.59 runtime complexity 1083.42/298.59 Answer: 1083.42/298.59 MAYBE 1083.42/298.59 1083.42/298.59 The weightgap principle applies (using the following nonconstant 1083.42/298.59 growth matrix-interpretation) 1083.42/298.59 1083.42/298.59 The following argument positions are usable: 1083.42/298.59 Uargs(s) = {1}, Uargs(+) = {1, 2} 1083.42/298.59 1083.42/298.59 TcT has computed the following matrix interpretation satisfying 1083.42/298.59 not(EDA) and not(IDA(1)). 1083.42/298.59 1083.42/298.59 [fib](x1) = [4] 1083.42/298.59 1083.42/298.59 [0] = [3] 1083.42/298.59 1083.42/298.59 [s](x1) = [1] x1 + [0] 1083.42/298.59 1083.42/298.59 [+](x1, x2) = [1] x1 + [1] x2 + [0] 1083.42/298.59 1083.42/298.59 The order satisfies the following ordering constraints: 1083.42/298.59 1083.42/298.59 [fib(0())] = [4] 1083.42/298.59 > [3] 1083.42/298.59 = [0()] 1083.42/298.59 1083.42/298.59 [fib(s(0()))] = [4] 1083.42/298.59 > [3] 1083.42/298.59 = [s(0())] 1083.42/298.59 1083.42/298.59 [fib(s(s(x)))] = [4] 1083.42/298.59 ? [8] 1083.42/298.59 = [+(fib(s(x)), fib(x))] 1083.42/298.59 1083.42/298.59 [+(x, 0())] = [1] x + [3] 1083.42/298.59 > [1] x + [0] 1083.42/298.59 = [x] 1083.42/298.59 1083.42/298.59 [+(x, s(y))] = [1] x + [1] y + [0] 1083.42/298.59 >= [1] x + [1] y + [0] 1083.42/298.59 = [s(+(x, y))] 1083.42/298.59 1083.42/298.59 1083.42/298.59 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 1083.42/298.59 1083.42/298.59 We are left with following problem, upon which TcT provides the 1083.42/298.59 certificate MAYBE. 1083.42/298.59 1083.42/298.59 Strict Trs: 1083.42/298.59 { fib(s(s(x))) -> +(fib(s(x)), fib(x)) 1083.42/298.59 , +(x, s(y)) -> s(+(x, y)) } 1083.42/298.59 Weak Trs: 1083.42/298.59 { fib(0()) -> 0() 1083.42/298.59 , fib(s(0())) -> s(0()) 1083.42/298.59 , +(x, 0()) -> x } 1083.42/298.59 Obligation: 1083.42/298.59 runtime complexity 1083.42/298.59 Answer: 1083.42/298.59 MAYBE 1083.42/298.59 1083.42/298.59 None of the processors succeeded. 1083.42/298.59 1083.42/298.59 Details of failed attempt(s): 1083.42/298.59 ----------------------------- 1083.42/298.59 1) 'empty' failed due to the following reason: 1083.42/298.59 1083.42/298.59 Empty strict component of the problem is NOT empty. 1083.42/298.59 1083.42/298.59 2) 'With Problem ...' failed due to the following reason: 1083.42/298.59 1083.42/298.59 None of the processors succeeded. 1083.42/298.59 1083.42/298.59 Details of failed attempt(s): 1083.42/298.59 ----------------------------- 1083.42/298.59 1) 'empty' failed due to the following reason: 1083.42/298.59 1083.42/298.59 Empty strict component of the problem is NOT empty. 1083.42/298.59 1083.42/298.59 2) 'Fastest' failed due to the following reason: 1083.42/298.59 1083.42/298.59 None of the processors succeeded. 1083.42/298.59 1083.42/298.59 Details of failed attempt(s): 1083.42/298.59 ----------------------------- 1083.42/298.59 1) 'With Problem ...' failed due to the following reason: 1083.42/298.59 1083.42/298.59 None of the processors succeeded. 1083.42/298.59 1083.42/298.59 Details of failed attempt(s): 1083.42/298.59 ----------------------------- 1083.42/298.59 1) 'empty' failed due to the following reason: 1083.42/298.59 1083.42/298.59 Empty strict component of the problem is NOT empty. 1083.42/298.59 1083.42/298.59 2) 'With Problem ...' failed due to the following reason: 1083.42/298.59 1083.42/298.59 None of the processors succeeded. 1083.42/298.59 1083.42/298.59 Details of failed attempt(s): 1083.42/298.59 ----------------------------- 1083.42/298.59 1) 'empty' failed due to the following reason: 1083.42/298.59 1083.42/298.59 Empty strict component of the problem is NOT empty. 1083.42/298.59 1083.42/298.59 2) 'With Problem ...' failed due to the following reason: 1083.42/298.59 1083.42/298.59 None of the processors succeeded. 1083.42/298.59 1083.42/298.59 Details of failed attempt(s): 1083.42/298.59 ----------------------------- 1083.42/298.59 1) 'empty' failed due to the following reason: 1083.42/298.59 1083.42/298.59 Empty strict component of the problem is NOT empty. 1083.42/298.59 1083.42/298.59 2) 'With Problem ...' failed due to the following reason: 1083.42/298.59 1083.42/298.59 Empty strict component of the problem is NOT empty. 1083.42/298.59 1083.42/298.59 1083.42/298.59 1083.42/298.59 1083.42/298.59 2) 'With Problem ...' failed due to the following reason: 1083.42/298.59 1083.42/298.59 None of the processors succeeded. 1083.42/298.59 1083.42/298.59 Details of failed attempt(s): 1083.42/298.59 ----------------------------- 1083.42/298.59 1) 'empty' failed due to the following reason: 1083.42/298.59 1083.42/298.59 Empty strict component of the problem is NOT empty. 1083.42/298.59 1083.42/298.59 2) 'With Problem ...' failed due to the following reason: 1083.42/298.59 1083.42/298.59 Empty strict component of the problem is NOT empty. 1083.42/298.59 1083.42/298.59 1083.42/298.59 1083.42/298.59 1083.42/298.59 1083.42/298.59 2) 'Best' failed due to the following reason: 1083.42/298.59 1083.42/298.59 None of the processors succeeded. 1083.42/298.59 1083.42/298.59 Details of failed attempt(s): 1083.42/298.59 ----------------------------- 1083.42/298.59 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1083.42/298.59 following reason: 1083.42/298.59 1083.42/298.59 The processor is inapplicable, reason: 1083.42/298.59 Processor only applicable for innermost runtime complexity analysis 1083.42/298.59 1083.42/298.59 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1083.42/298.59 to the following reason: 1083.42/298.59 1083.42/298.59 The processor is inapplicable, reason: 1083.42/298.59 Processor only applicable for innermost runtime complexity analysis 1083.42/298.59 1083.42/298.59 1083.42/298.59 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1083.42/298.59 failed due to the following reason: 1083.42/298.59 1083.42/298.59 None of the processors succeeded. 1083.42/298.59 1083.42/298.59 Details of failed attempt(s): 1083.42/298.59 ----------------------------- 1083.42/298.59 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1083.42/298.59 failed due to the following reason: 1083.42/298.59 1083.42/298.59 match-boundness of the problem could not be verified. 1083.42/298.59 1083.42/298.59 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1083.42/298.59 failed due to the following reason: 1083.42/298.59 1083.42/298.59 match-boundness of the problem could not be verified. 1083.42/298.59 1083.42/298.59 1083.42/298.59 1083.42/298.59 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 1083.42/298.59 the following reason: 1083.42/298.59 1083.42/298.59 We add the following weak dependency pairs: 1083.42/298.59 1083.42/298.59 Strict DPs: 1083.42/298.59 { fib^#(0()) -> c_1() 1083.42/298.59 , fib^#(s(0())) -> c_2() 1083.42/298.59 , fib^#(s(s(x))) -> c_3(+^#(fib(s(x)), fib(x))) 1083.42/298.59 , +^#(x, 0()) -> c_4(x) 1083.42/298.59 , +^#(x, s(y)) -> c_5(+^#(x, y)) } 1083.42/298.59 1083.42/298.59 and mark the set of starting terms. 1083.42/298.59 1083.42/298.59 We are left with following problem, upon which TcT provides the 1083.42/298.59 certificate MAYBE. 1083.42/298.59 1083.42/298.59 Strict DPs: 1083.42/298.59 { fib^#(0()) -> c_1() 1083.42/298.59 , fib^#(s(0())) -> c_2() 1083.42/298.59 , fib^#(s(s(x))) -> c_3(+^#(fib(s(x)), fib(x))) 1083.42/298.59 , +^#(x, 0()) -> c_4(x) 1083.42/298.59 , +^#(x, s(y)) -> c_5(+^#(x, y)) } 1083.42/298.59 Strict Trs: 1083.42/298.59 { fib(0()) -> 0() 1083.42/298.59 , fib(s(0())) -> s(0()) 1083.42/298.59 , fib(s(s(x))) -> +(fib(s(x)), fib(x)) 1083.42/298.59 , +(x, 0()) -> x 1083.42/298.59 , +(x, s(y)) -> s(+(x, y)) } 1083.42/298.59 Obligation: 1083.42/298.59 runtime complexity 1083.42/298.59 Answer: 1083.42/298.59 MAYBE 1083.42/298.59 1083.42/298.59 We estimate the number of application of {1,2} by applications of 1083.42/298.59 Pre({1,2}) = {4}. Here rules are labeled as follows: 1083.42/298.59 1083.42/298.59 DPs: 1083.42/298.59 { 1: fib^#(0()) -> c_1() 1083.42/298.59 , 2: fib^#(s(0())) -> c_2() 1083.42/298.59 , 3: fib^#(s(s(x))) -> c_3(+^#(fib(s(x)), fib(x))) 1083.42/298.59 , 4: +^#(x, 0()) -> c_4(x) 1083.42/298.59 , 5: +^#(x, s(y)) -> c_5(+^#(x, y)) } 1083.42/298.59 1083.42/298.59 We are left with following problem, upon which TcT provides the 1083.42/298.59 certificate MAYBE. 1083.42/298.59 1083.42/298.59 Strict DPs: 1083.42/298.59 { fib^#(s(s(x))) -> c_3(+^#(fib(s(x)), fib(x))) 1083.42/298.59 , +^#(x, 0()) -> c_4(x) 1083.42/298.59 , +^#(x, s(y)) -> c_5(+^#(x, y)) } 1083.42/298.59 Strict Trs: 1083.42/298.59 { fib(0()) -> 0() 1083.42/298.59 , fib(s(0())) -> s(0()) 1083.42/298.59 , fib(s(s(x))) -> +(fib(s(x)), fib(x)) 1083.42/298.59 , +(x, 0()) -> x 1083.42/298.59 , +(x, s(y)) -> s(+(x, y)) } 1083.42/298.59 Weak DPs: 1083.42/298.59 { fib^#(0()) -> c_1() 1083.42/298.59 , fib^#(s(0())) -> c_2() } 1083.42/298.59 Obligation: 1083.42/298.59 runtime complexity 1083.42/298.59 Answer: 1083.42/298.59 MAYBE 1083.42/298.59 1083.42/298.59 Empty strict component of the problem is NOT empty. 1083.42/298.59 1083.42/298.59 1083.42/298.59 Arrrr.. 1084.88/299.76 EOF