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