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