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