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