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