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