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