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