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