MAYBE 567.49/297.04 MAYBE 567.49/297.04 567.49/297.04 We are left with following problem, upon which TcT provides the 567.49/297.04 certificate MAYBE. 567.49/297.04 567.49/297.04 Strict Trs: 567.49/297.04 { div(x, y) -> div2(x, y, 0()) 567.49/297.04 , div2(x, y, i) -> 567.49/297.04 if1(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)) 567.49/297.04 , if1(true(), b, x, y, i, j) -> divZeroError() 567.49/297.04 , if1(false(), b, x, y, i, j) -> if2(b, x, y, i, j) 567.49/297.04 , le(0(), y) -> true() 567.49/297.04 , le(s(x), 0()) -> false() 567.49/297.04 , le(s(x), s(y)) -> le(x, y) 567.49/297.04 , plus(x, y) -> plusIter(x, y, 0()) 567.49/297.04 , inc(0()) -> 0() 567.49/297.04 , inc(s(i)) -> s(inc(i)) 567.49/297.04 , if2(true(), x, y, i, j) -> div2(minus(x, y), y, j) 567.49/297.04 , if2(false(), x, y, i, j) -> i 567.49/297.04 , minus(x, 0()) -> x 567.49/297.04 , minus(0(), y) -> 0() 567.49/297.04 , minus(s(x), s(y)) -> minus(x, y) 567.49/297.04 , plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z) 567.49/297.04 , ifPlus(true(), x, y, z) -> y 567.49/297.04 , ifPlus(false(), x, y, z) -> plusIter(x, s(y), s(z)) 567.49/297.04 , a() -> c() 567.49/297.04 , a() -> d() } 567.49/297.04 Obligation: 567.49/297.04 runtime complexity 567.49/297.04 Answer: 567.49/297.04 MAYBE 567.49/297.04 567.49/297.04 None of the processors succeeded. 567.49/297.04 567.49/297.04 Details of failed attempt(s): 567.49/297.04 ----------------------------- 567.49/297.04 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 567.49/297.04 following reason: 567.49/297.04 567.49/297.04 Computation stopped due to timeout after 297.0 seconds. 567.49/297.04 567.49/297.04 2) 'Best' failed due to the following reason: 567.49/297.04 567.49/297.04 None of the processors succeeded. 567.49/297.04 567.49/297.04 Details of failed attempt(s): 567.49/297.04 ----------------------------- 567.49/297.04 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 567.49/297.04 seconds)' failed due to the following reason: 567.49/297.04 567.49/297.04 None of the processors succeeded. 567.49/297.04 567.49/297.04 Details of failed attempt(s): 567.49/297.04 ----------------------------- 567.49/297.04 1) 'empty' failed due to the following reason: 567.49/297.04 567.49/297.04 Empty strict component of the problem is NOT empty. 567.49/297.04 567.49/297.04 2) 'With Problem ...' failed due to the following reason: 567.49/297.04 567.49/297.04 None of the processors succeeded. 567.49/297.04 567.49/297.04 Details of failed attempt(s): 567.49/297.04 ----------------------------- 567.49/297.04 1) 'empty' failed due to the following reason: 567.49/297.04 567.49/297.04 Empty strict component of the problem is NOT empty. 567.49/297.04 567.49/297.04 2) 'Fastest' failed due to the following reason: 567.49/297.04 567.49/297.04 None of the processors succeeded. 567.49/297.04 567.49/297.04 Details of failed attempt(s): 567.49/297.04 ----------------------------- 567.49/297.04 1) 'With Problem ...' failed due to the following reason: 567.49/297.04 567.49/297.04 None of the processors succeeded. 567.49/297.04 567.49/297.04 Details of failed attempt(s): 567.49/297.04 ----------------------------- 567.49/297.04 1) 'empty' failed due to the following reason: 567.49/297.04 567.49/297.04 Empty strict component of the problem is NOT empty. 567.49/297.04 567.49/297.04 2) 'With Problem ...' failed due to the following reason: 567.49/297.04 567.49/297.04 Empty strict component of the problem is NOT empty. 567.49/297.04 567.49/297.04 567.49/297.04 2) 'With Problem ...' failed due to the following reason: 567.49/297.04 567.49/297.04 None of the processors succeeded. 567.49/297.04 567.49/297.04 Details of failed attempt(s): 567.49/297.04 ----------------------------- 567.49/297.04 1) 'empty' failed due to the following reason: 567.49/297.04 567.49/297.04 Empty strict component of the problem is NOT empty. 567.49/297.04 567.49/297.04 2) 'With Problem ...' failed due to the following reason: 567.49/297.04 567.49/297.04 None of the processors succeeded. 567.49/297.04 567.49/297.04 Details of failed attempt(s): 567.49/297.04 ----------------------------- 567.49/297.04 1) 'empty' failed due to the following reason: 567.49/297.04 567.49/297.04 Empty strict component of the problem is NOT empty. 567.49/297.04 567.49/297.04 2) 'With Problem ...' failed due to the following reason: 567.49/297.04 567.49/297.04 None of the processors succeeded. 567.49/297.04 567.49/297.04 Details of failed attempt(s): 567.49/297.04 ----------------------------- 567.49/297.04 1) 'empty' failed due to the following reason: 567.49/297.04 567.49/297.04 Empty strict component of the problem is NOT empty. 567.49/297.04 567.49/297.04 2) 'With Problem ...' failed due to the following reason: 567.49/297.04 567.49/297.04 Empty strict component of the problem is NOT empty. 567.49/297.04 567.49/297.04 567.49/297.04 567.49/297.04 567.49/297.04 567.49/297.04 567.49/297.04 567.49/297.04 2) 'Best' failed due to the following reason: 567.49/297.04 567.49/297.04 None of the processors succeeded. 567.49/297.04 567.49/297.04 Details of failed attempt(s): 567.49/297.04 ----------------------------- 567.49/297.04 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 567.49/297.04 following reason: 567.49/297.04 567.49/297.04 The processor is inapplicable, reason: 567.49/297.04 Processor only applicable for innermost runtime complexity analysis 567.49/297.04 567.49/297.04 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 567.49/297.04 to the following reason: 567.49/297.04 567.49/297.04 The processor is inapplicable, reason: 567.49/297.04 Processor only applicable for innermost runtime complexity analysis 567.49/297.04 567.49/297.04 567.49/297.04 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 567.49/297.04 failed due to the following reason: 567.49/297.04 567.49/297.04 None of the processors succeeded. 567.49/297.04 567.49/297.04 Details of failed attempt(s): 567.49/297.04 ----------------------------- 567.49/297.04 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 567.49/297.04 failed due to the following reason: 567.49/297.04 567.49/297.04 match-boundness of the problem could not be verified. 567.49/297.04 567.49/297.04 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 567.49/297.04 failed due to the following reason: 567.49/297.04 567.49/297.04 match-boundness of the problem could not be verified. 567.49/297.04 567.49/297.04 567.49/297.04 567.49/297.04 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 567.49/297.04 the following reason: 567.49/297.04 567.49/297.04 We add the following weak dependency pairs: 567.49/297.04 567.49/297.04 Strict DPs: 567.49/297.04 { div^#(x, y) -> c_1(div2^#(x, y, 0())) 567.49/297.04 , div2^#(x, y, i) -> 567.49/297.04 c_2(if1^#(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i))) 567.49/297.04 , if1^#(true(), b, x, y, i, j) -> c_3() 567.49/297.04 , if1^#(false(), b, x, y, i, j) -> c_4(if2^#(b, x, y, i, j)) 567.49/297.04 , if2^#(true(), x, y, i, j) -> c_11(div2^#(minus(x, y), y, j)) 567.49/297.04 , if2^#(false(), x, y, i, j) -> c_12(i) 567.49/297.04 , le^#(0(), y) -> c_5() 567.49/297.04 , le^#(s(x), 0()) -> c_6() 567.49/297.04 , le^#(s(x), s(y)) -> c_7(le^#(x, y)) 567.49/297.04 , plus^#(x, y) -> c_8(plusIter^#(x, y, 0())) 567.49/297.04 , plusIter^#(x, y, z) -> c_16(ifPlus^#(le(x, z), x, y, z)) 567.49/297.04 , inc^#(0()) -> c_9() 567.49/297.04 , inc^#(s(i)) -> c_10(inc^#(i)) 567.49/297.04 , minus^#(x, 0()) -> c_13(x) 567.49/297.04 , minus^#(0(), y) -> c_14() 567.49/297.04 , minus^#(s(x), s(y)) -> c_15(minus^#(x, y)) 567.49/297.04 , ifPlus^#(true(), x, y, z) -> c_17(y) 567.49/297.04 , ifPlus^#(false(), x, y, z) -> c_18(plusIter^#(x, s(y), s(z))) 567.49/297.04 , a^#() -> c_19() 567.49/297.04 , a^#() -> c_20() } 567.49/297.04 567.49/297.04 and mark the set of starting terms. 567.49/297.04 567.49/297.04 We are left with following problem, upon which TcT provides the 567.49/297.04 certificate MAYBE. 567.49/297.04 567.49/297.04 Strict DPs: 567.49/297.04 { div^#(x, y) -> c_1(div2^#(x, y, 0())) 567.49/297.04 , div2^#(x, y, i) -> 567.49/297.04 c_2(if1^#(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i))) 567.49/297.04 , if1^#(true(), b, x, y, i, j) -> c_3() 567.49/297.04 , if1^#(false(), b, x, y, i, j) -> c_4(if2^#(b, x, y, i, j)) 567.49/297.04 , if2^#(true(), x, y, i, j) -> c_11(div2^#(minus(x, y), y, j)) 567.49/297.04 , if2^#(false(), x, y, i, j) -> c_12(i) 567.49/297.04 , le^#(0(), y) -> c_5() 567.49/297.04 , le^#(s(x), 0()) -> c_6() 567.49/297.04 , le^#(s(x), s(y)) -> c_7(le^#(x, y)) 567.49/297.04 , plus^#(x, y) -> c_8(plusIter^#(x, y, 0())) 567.49/297.04 , plusIter^#(x, y, z) -> c_16(ifPlus^#(le(x, z), x, y, z)) 567.49/297.04 , inc^#(0()) -> c_9() 567.49/297.04 , inc^#(s(i)) -> c_10(inc^#(i)) 567.49/297.04 , minus^#(x, 0()) -> c_13(x) 567.49/297.04 , minus^#(0(), y) -> c_14() 567.49/297.04 , minus^#(s(x), s(y)) -> c_15(minus^#(x, y)) 567.49/297.04 , ifPlus^#(true(), x, y, z) -> c_17(y) 567.49/297.04 , ifPlus^#(false(), x, y, z) -> c_18(plusIter^#(x, s(y), s(z))) 567.49/297.04 , a^#() -> c_19() 567.49/297.04 , a^#() -> c_20() } 567.49/297.04 Strict Trs: 567.49/297.04 { div(x, y) -> div2(x, y, 0()) 567.49/297.04 , div2(x, y, i) -> 567.49/297.04 if1(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)) 567.49/297.04 , if1(true(), b, x, y, i, j) -> divZeroError() 567.49/297.04 , if1(false(), b, x, y, i, j) -> if2(b, x, y, i, j) 567.49/297.05 , le(0(), y) -> true() 567.49/297.05 , le(s(x), 0()) -> false() 567.49/297.05 , le(s(x), s(y)) -> le(x, y) 567.49/297.05 , plus(x, y) -> plusIter(x, y, 0()) 567.49/297.05 , inc(0()) -> 0() 567.49/297.05 , inc(s(i)) -> s(inc(i)) 567.49/297.05 , if2(true(), x, y, i, j) -> div2(minus(x, y), y, j) 567.49/297.05 , if2(false(), x, y, i, j) -> i 567.49/297.05 , minus(x, 0()) -> x 567.49/297.05 , minus(0(), y) -> 0() 567.49/297.05 , minus(s(x), s(y)) -> minus(x, y) 567.49/297.05 , plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z) 567.49/297.05 , ifPlus(true(), x, y, z) -> y 567.49/297.05 , ifPlus(false(), x, y, z) -> plusIter(x, s(y), s(z)) 567.49/297.05 , a() -> c() 567.49/297.05 , a() -> d() } 567.49/297.05 Obligation: 567.49/297.05 runtime complexity 567.49/297.05 Answer: 567.49/297.05 MAYBE 567.49/297.05 567.49/297.05 We estimate the number of application of {3,7,8,12,15,19,20} by 567.49/297.05 applications of Pre({3,7,8,12,15,19,20}) = {2,6,9,13,14,16,17}. 567.49/297.05 Here rules are labeled as follows: 567.49/297.05 567.49/297.05 DPs: 567.49/297.05 { 1: div^#(x, y) -> c_1(div2^#(x, y, 0())) 567.49/297.05 , 2: div2^#(x, y, i) -> 567.49/297.05 c_2(if1^#(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i))) 567.49/297.05 , 3: if1^#(true(), b, x, y, i, j) -> c_3() 567.49/297.05 , 4: if1^#(false(), b, x, y, i, j) -> c_4(if2^#(b, x, y, i, j)) 567.49/297.05 , 5: if2^#(true(), x, y, i, j) -> c_11(div2^#(minus(x, y), y, j)) 567.49/297.05 , 6: if2^#(false(), x, y, i, j) -> c_12(i) 567.49/297.05 , 7: le^#(0(), y) -> c_5() 567.49/297.05 , 8: le^#(s(x), 0()) -> c_6() 567.49/297.05 , 9: le^#(s(x), s(y)) -> c_7(le^#(x, y)) 567.49/297.05 , 10: plus^#(x, y) -> c_8(plusIter^#(x, y, 0())) 567.49/297.05 , 11: plusIter^#(x, y, z) -> c_16(ifPlus^#(le(x, z), x, y, z)) 567.49/297.05 , 12: inc^#(0()) -> c_9() 567.49/297.05 , 13: inc^#(s(i)) -> c_10(inc^#(i)) 567.49/297.05 , 14: minus^#(x, 0()) -> c_13(x) 567.49/297.05 , 15: minus^#(0(), y) -> c_14() 567.49/297.05 , 16: minus^#(s(x), s(y)) -> c_15(minus^#(x, y)) 567.49/297.05 , 17: ifPlus^#(true(), x, y, z) -> c_17(y) 567.49/297.05 , 18: ifPlus^#(false(), x, y, z) -> c_18(plusIter^#(x, s(y), s(z))) 567.49/297.05 , 19: a^#() -> c_19() 567.49/297.05 , 20: a^#() -> c_20() } 567.49/297.05 567.49/297.05 We are left with following problem, upon which TcT provides the 567.49/297.05 certificate MAYBE. 567.49/297.05 567.49/297.05 Strict DPs: 567.49/297.05 { div^#(x, y) -> c_1(div2^#(x, y, 0())) 567.49/297.05 , div2^#(x, y, i) -> 567.49/297.05 c_2(if1^#(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i))) 567.49/297.05 , if1^#(false(), b, x, y, i, j) -> c_4(if2^#(b, x, y, i, j)) 567.49/297.05 , if2^#(true(), x, y, i, j) -> c_11(div2^#(minus(x, y), y, j)) 567.49/297.05 , if2^#(false(), x, y, i, j) -> c_12(i) 567.49/297.05 , le^#(s(x), s(y)) -> c_7(le^#(x, y)) 567.49/297.05 , plus^#(x, y) -> c_8(plusIter^#(x, y, 0())) 567.49/297.05 , plusIter^#(x, y, z) -> c_16(ifPlus^#(le(x, z), x, y, z)) 567.49/297.05 , inc^#(s(i)) -> c_10(inc^#(i)) 567.49/297.05 , minus^#(x, 0()) -> c_13(x) 567.49/297.05 , minus^#(s(x), s(y)) -> c_15(minus^#(x, y)) 567.49/297.05 , ifPlus^#(true(), x, y, z) -> c_17(y) 567.49/297.05 , ifPlus^#(false(), x, y, z) -> c_18(plusIter^#(x, s(y), s(z))) } 567.49/297.05 Strict Trs: 567.49/297.05 { div(x, y) -> div2(x, y, 0()) 567.49/297.05 , div2(x, y, i) -> 567.49/297.05 if1(le(y, 0()), le(y, x), x, y, plus(i, 0()), inc(i)) 567.49/297.05 , if1(true(), b, x, y, i, j) -> divZeroError() 567.49/297.05 , if1(false(), b, x, y, i, j) -> if2(b, x, y, i, j) 567.49/297.05 , le(0(), y) -> true() 567.49/297.05 , le(s(x), 0()) -> false() 567.49/297.05 , le(s(x), s(y)) -> le(x, y) 567.49/297.05 , plus(x, y) -> plusIter(x, y, 0()) 567.49/297.05 , inc(0()) -> 0() 567.49/297.05 , inc(s(i)) -> s(inc(i)) 567.49/297.05 , if2(true(), x, y, i, j) -> div2(minus(x, y), y, j) 567.49/297.05 , if2(false(), x, y, i, j) -> i 567.49/297.05 , minus(x, 0()) -> x 567.49/297.05 , minus(0(), y) -> 0() 567.49/297.05 , minus(s(x), s(y)) -> minus(x, y) 567.49/297.05 , plusIter(x, y, z) -> ifPlus(le(x, z), x, y, z) 567.49/297.05 , ifPlus(true(), x, y, z) -> y 567.49/297.05 , ifPlus(false(), x, y, z) -> plusIter(x, s(y), s(z)) 567.49/297.05 , a() -> c() 567.49/297.05 , a() -> d() } 567.49/297.05 Weak DPs: 567.49/297.05 { if1^#(true(), b, x, y, i, j) -> c_3() 567.49/297.05 , le^#(0(), y) -> c_5() 567.49/297.05 , le^#(s(x), 0()) -> c_6() 567.49/297.05 , inc^#(0()) -> c_9() 567.49/297.05 , minus^#(0(), y) -> c_14() 567.49/297.05 , a^#() -> c_19() 567.49/297.05 , a^#() -> c_20() } 567.49/297.05 Obligation: 567.49/297.05 runtime complexity 567.49/297.05 Answer: 567.49/297.05 MAYBE 567.49/297.05 567.49/297.05 Empty strict component of the problem is NOT empty. 567.49/297.05 567.49/297.05 567.49/297.05 Arrrr.. 567.82/297.32 EOF