MAYBE 573.60/297.08 MAYBE 573.60/297.08 573.60/297.08 We are left with following problem, upon which TcT provides the 573.60/297.08 certificate MAYBE. 573.60/297.08 573.60/297.08 Strict Trs: 573.60/297.08 { times(x, y) -> help(x, y, 0()) 573.60/297.08 , help(x, y, c) -> if(lt(c, y), x, y, c) 573.60/297.08 , if(true(), x, y, c) -> plus(x, help(x, y, s(c))) 573.60/297.08 , if(false(), x, y, c) -> 0() 573.60/297.08 , lt(0(), s(x)) -> true() 573.60/297.08 , lt(s(x), 0()) -> false() 573.60/297.08 , lt(s(x), s(y)) -> lt(x, y) 573.60/297.08 , plus(x, 0()) -> x 573.60/297.08 , plus(x, s(y)) -> s(plus(x, y)) 573.60/297.08 , plus(0(), x) -> x 573.60/297.08 , plus(s(x), y) -> s(plus(x, y)) } 573.60/297.08 Obligation: 573.60/297.08 runtime complexity 573.60/297.08 Answer: 573.60/297.08 MAYBE 573.60/297.08 573.60/297.08 None of the processors succeeded. 573.60/297.08 573.60/297.08 Details of failed attempt(s): 573.60/297.08 ----------------------------- 573.60/297.08 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 573.60/297.08 following reason: 573.60/297.08 573.60/297.08 Computation stopped due to timeout after 297.0 seconds. 573.60/297.08 573.60/297.08 2) 'Best' failed due to the following reason: 573.60/297.08 573.60/297.08 None of the processors succeeded. 573.60/297.08 573.60/297.08 Details of failed attempt(s): 573.60/297.08 ----------------------------- 573.60/297.08 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 573.60/297.08 seconds)' failed due to the following reason: 573.60/297.08 573.60/297.08 None of the processors succeeded. 573.60/297.08 573.60/297.08 Details of failed attempt(s): 573.60/297.08 ----------------------------- 573.60/297.08 1) 'empty' failed due to the following reason: 573.60/297.08 573.60/297.08 Empty strict component of the problem is NOT empty. 573.60/297.08 573.60/297.08 2) 'With Problem ...' failed due to the following reason: 573.60/297.08 573.60/297.08 None of the processors succeeded. 573.60/297.08 573.60/297.08 Details of failed attempt(s): 573.60/297.08 ----------------------------- 573.60/297.08 1) 'empty' failed due to the following reason: 573.60/297.08 573.60/297.08 Empty strict component of the problem is NOT empty. 573.60/297.08 573.60/297.08 2) 'Fastest' failed due to the following reason: 573.60/297.08 573.60/297.08 None of the processors succeeded. 573.60/297.08 573.60/297.08 Details of failed attempt(s): 573.60/297.08 ----------------------------- 573.60/297.08 1) 'With Problem ...' failed due to the following reason: 573.60/297.08 573.60/297.08 None of the processors succeeded. 573.60/297.08 573.60/297.08 Details of failed attempt(s): 573.60/297.08 ----------------------------- 573.60/297.08 1) 'empty' failed due to the following reason: 573.60/297.08 573.60/297.08 Empty strict component of the problem is NOT empty. 573.60/297.08 573.60/297.08 2) 'With Problem ...' failed due to the following reason: 573.60/297.08 573.60/297.08 Empty strict component of the problem is NOT empty. 573.60/297.08 573.60/297.08 573.60/297.08 2) 'With Problem ...' failed due to the following reason: 573.60/297.08 573.60/297.08 None of the processors succeeded. 573.60/297.08 573.60/297.08 Details of failed attempt(s): 573.60/297.08 ----------------------------- 573.60/297.08 1) 'empty' failed due to the following reason: 573.60/297.08 573.60/297.08 Empty strict component of the problem is NOT empty. 573.60/297.08 573.60/297.08 2) 'With Problem ...' failed due to the following reason: 573.60/297.08 573.60/297.08 None of the processors succeeded. 573.60/297.08 573.60/297.08 Details of failed attempt(s): 573.60/297.08 ----------------------------- 573.60/297.08 1) 'empty' failed due to the following reason: 573.60/297.08 573.60/297.08 Empty strict component of the problem is NOT empty. 573.60/297.08 573.60/297.08 2) 'With Problem ...' failed due to the following reason: 573.60/297.08 573.60/297.08 None of the processors succeeded. 573.60/297.08 573.60/297.08 Details of failed attempt(s): 573.60/297.08 ----------------------------- 573.60/297.08 1) 'empty' failed due to the following reason: 573.60/297.08 573.60/297.08 Empty strict component of the problem is NOT empty. 573.60/297.08 573.60/297.08 2) 'With Problem ...' failed due to the following reason: 573.60/297.08 573.60/297.08 Empty strict component of the problem is NOT empty. 573.60/297.08 573.60/297.08 573.60/297.08 573.60/297.08 573.60/297.08 573.60/297.08 573.60/297.08 573.60/297.08 2) 'Best' failed due to the following reason: 573.60/297.08 573.60/297.09 None of the processors succeeded. 573.60/297.09 573.60/297.09 Details of failed attempt(s): 573.60/297.09 ----------------------------- 573.60/297.09 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 573.60/297.09 following reason: 573.60/297.09 573.60/297.09 The processor is inapplicable, reason: 573.60/297.09 Processor only applicable for innermost runtime complexity analysis 573.60/297.09 573.60/297.09 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 573.60/297.09 to the following reason: 573.60/297.09 573.60/297.09 The processor is inapplicable, reason: 573.60/297.09 Processor only applicable for innermost runtime complexity analysis 573.60/297.09 573.60/297.09 573.60/297.09 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 573.60/297.09 failed due to the following reason: 573.60/297.09 573.60/297.09 None of the processors succeeded. 573.60/297.09 573.60/297.09 Details of failed attempt(s): 573.60/297.09 ----------------------------- 573.60/297.09 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 573.60/297.09 failed due to the following reason: 573.60/297.09 573.60/297.09 match-boundness of the problem could not be verified. 573.60/297.09 573.60/297.09 2) 'Bounds with minimal-enrichment and initial automaton 'match'' 573.60/297.09 failed due to the following reason: 573.60/297.09 573.60/297.09 match-boundness of the problem could not be verified. 573.60/297.09 573.60/297.09 573.60/297.09 573.60/297.09 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 573.60/297.09 the following reason: 573.60/297.09 573.60/297.09 We add the following weak dependency pairs: 573.60/297.09 573.60/297.09 Strict DPs: 573.60/297.09 { times^#(x, y) -> c_1(help^#(x, y, 0())) 573.60/297.09 , help^#(x, y, c) -> c_2(if^#(lt(c, y), x, y, c)) 573.60/297.09 , if^#(true(), x, y, c) -> c_3(plus^#(x, help(x, y, s(c)))) 573.60/297.09 , if^#(false(), x, y, c) -> c_4() 573.60/297.09 , plus^#(x, 0()) -> c_8(x) 573.60/297.09 , plus^#(x, s(y)) -> c_9(plus^#(x, y)) 573.60/297.09 , plus^#(0(), x) -> c_10(x) 573.60/297.09 , plus^#(s(x), y) -> c_11(plus^#(x, y)) 573.60/297.09 , lt^#(0(), s(x)) -> c_5() 573.60/297.09 , lt^#(s(x), 0()) -> c_6() 573.60/297.09 , lt^#(s(x), s(y)) -> c_7(lt^#(x, y)) } 573.60/297.09 573.60/297.09 and mark the set of starting terms. 573.60/297.09 573.60/297.09 We are left with following problem, upon which TcT provides the 573.60/297.09 certificate MAYBE. 573.60/297.09 573.60/297.09 Strict DPs: 573.60/297.09 { times^#(x, y) -> c_1(help^#(x, y, 0())) 573.60/297.09 , help^#(x, y, c) -> c_2(if^#(lt(c, y), x, y, c)) 573.60/297.09 , if^#(true(), x, y, c) -> c_3(plus^#(x, help(x, y, s(c)))) 573.60/297.09 , if^#(false(), x, y, c) -> c_4() 573.60/297.09 , plus^#(x, 0()) -> c_8(x) 573.60/297.09 , plus^#(x, s(y)) -> c_9(plus^#(x, y)) 573.60/297.09 , plus^#(0(), x) -> c_10(x) 573.60/297.09 , plus^#(s(x), y) -> c_11(plus^#(x, y)) 573.60/297.09 , lt^#(0(), s(x)) -> c_5() 573.60/297.09 , lt^#(s(x), 0()) -> c_6() 573.60/297.09 , lt^#(s(x), s(y)) -> c_7(lt^#(x, y)) } 573.60/297.09 Strict Trs: 573.60/297.09 { times(x, y) -> help(x, y, 0()) 573.60/297.09 , help(x, y, c) -> if(lt(c, y), x, y, c) 573.60/297.09 , if(true(), x, y, c) -> plus(x, help(x, y, s(c))) 573.60/297.09 , if(false(), x, y, c) -> 0() 573.60/297.09 , lt(0(), s(x)) -> true() 573.60/297.09 , lt(s(x), 0()) -> false() 573.60/297.09 , lt(s(x), s(y)) -> lt(x, y) 573.60/297.09 , plus(x, 0()) -> x 573.60/297.09 , plus(x, s(y)) -> s(plus(x, y)) 573.60/297.09 , plus(0(), x) -> x 573.60/297.09 , plus(s(x), y) -> s(plus(x, y)) } 573.60/297.09 Obligation: 573.60/297.09 runtime complexity 573.60/297.09 Answer: 573.60/297.09 MAYBE 573.60/297.09 573.60/297.09 We estimate the number of application of {4,9,10} by applications 573.60/297.09 of Pre({4,9,10}) = {2,5,7,11}. Here rules are labeled as follows: 573.60/297.09 573.60/297.09 DPs: 573.60/297.09 { 1: times^#(x, y) -> c_1(help^#(x, y, 0())) 573.60/297.09 , 2: help^#(x, y, c) -> c_2(if^#(lt(c, y), x, y, c)) 573.60/297.09 , 3: if^#(true(), x, y, c) -> c_3(plus^#(x, help(x, y, s(c)))) 573.60/297.09 , 4: if^#(false(), x, y, c) -> c_4() 573.60/297.09 , 5: plus^#(x, 0()) -> c_8(x) 573.60/297.09 , 6: plus^#(x, s(y)) -> c_9(plus^#(x, y)) 573.60/297.09 , 7: plus^#(0(), x) -> c_10(x) 573.60/297.09 , 8: plus^#(s(x), y) -> c_11(plus^#(x, y)) 573.60/297.09 , 9: lt^#(0(), s(x)) -> c_5() 573.60/297.09 , 10: lt^#(s(x), 0()) -> c_6() 573.60/297.09 , 11: lt^#(s(x), s(y)) -> c_7(lt^#(x, y)) } 573.60/297.09 573.60/297.09 We are left with following problem, upon which TcT provides the 573.60/297.09 certificate MAYBE. 573.60/297.09 573.60/297.09 Strict DPs: 573.60/297.09 { times^#(x, y) -> c_1(help^#(x, y, 0())) 573.60/297.09 , help^#(x, y, c) -> c_2(if^#(lt(c, y), x, y, c)) 573.60/297.09 , if^#(true(), x, y, c) -> c_3(plus^#(x, help(x, y, s(c)))) 573.60/297.09 , plus^#(x, 0()) -> c_8(x) 573.60/297.09 , plus^#(x, s(y)) -> c_9(plus^#(x, y)) 573.60/297.09 , plus^#(0(), x) -> c_10(x) 573.60/297.09 , plus^#(s(x), y) -> c_11(plus^#(x, y)) 573.60/297.09 , lt^#(s(x), s(y)) -> c_7(lt^#(x, y)) } 573.60/297.09 Strict Trs: 573.60/297.09 { times(x, y) -> help(x, y, 0()) 573.60/297.09 , help(x, y, c) -> if(lt(c, y), x, y, c) 573.60/297.09 , if(true(), x, y, c) -> plus(x, help(x, y, s(c))) 573.60/297.09 , if(false(), x, y, c) -> 0() 573.60/297.09 , lt(0(), s(x)) -> true() 573.60/297.09 , lt(s(x), 0()) -> false() 573.60/297.09 , lt(s(x), s(y)) -> lt(x, y) 573.60/297.09 , plus(x, 0()) -> x 573.60/297.09 , plus(x, s(y)) -> s(plus(x, y)) 573.60/297.09 , plus(0(), x) -> x 573.60/297.09 , plus(s(x), y) -> s(plus(x, y)) } 573.60/297.09 Weak DPs: 573.60/297.09 { if^#(false(), x, y, c) -> c_4() 573.60/297.09 , lt^#(0(), s(x)) -> c_5() 573.60/297.09 , lt^#(s(x), 0()) -> c_6() } 573.60/297.09 Obligation: 573.60/297.09 runtime complexity 573.60/297.09 Answer: 573.60/297.09 MAYBE 573.60/297.09 573.60/297.09 Empty strict component of the problem is NOT empty. 573.60/297.09 573.60/297.09 573.60/297.09 Arrrr.. 573.96/297.38 EOF