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