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