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