MAYBE 775.70/297.04 MAYBE 775.70/297.04 775.70/297.04 We are left with following problem, upon which TcT provides the 775.70/297.04 certificate MAYBE. 775.70/297.04 775.70/297.04 Strict Trs: 775.70/297.04 { prod(xs) -> prodIter(xs, s(0())) 775.70/297.04 , prodIter(xs, x) -> ifProd(isempty(xs), xs, x) 775.70/297.04 , ifProd(true(), xs, x) -> x 775.70/297.04 , ifProd(false(), xs, x) -> prodIter(tail(xs), times(x, head(xs))) 775.70/297.04 , isempty(nil()) -> true() 775.70/297.04 , isempty(cons(x, xs)) -> false() 775.70/297.04 , tail(nil()) -> nil() 775.70/297.04 , tail(cons(x, xs)) -> xs 775.70/297.04 , times(x, y) -> timesIter(x, y, 0(), 0()) 775.70/297.04 , head(nil()) -> error() 775.70/297.04 , head(cons(x, xs)) -> x 775.70/297.04 , plus(s(x), y) -> s(plus(x, y)) 775.70/297.04 , plus(0(), y) -> y 775.70/297.04 , timesIter(x, y, z, u) -> ifTimes(ge(u, x), x, y, z, u) 775.70/297.04 , ifTimes(true(), x, y, z, u) -> z 775.70/297.04 , ifTimes(false(), x, y, z, u) -> timesIter(x, y, plus(y, z), s(u)) 775.70/297.04 , ge(x, 0()) -> true() 775.70/297.04 , ge(s(x), s(y)) -> ge(x, y) 775.70/297.04 , ge(0(), s(y)) -> false() 775.70/297.04 , a() -> b() 775.70/297.04 , a() -> c() } 775.70/297.04 Obligation: 775.70/297.04 runtime complexity 775.70/297.04 Answer: 775.70/297.04 MAYBE 775.70/297.04 775.70/297.04 None of the processors succeeded. 775.70/297.04 775.70/297.04 Details of failed attempt(s): 775.70/297.04 ----------------------------- 775.70/297.04 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 775.70/297.04 following reason: 775.70/297.04 775.70/297.04 Computation stopped due to timeout after 297.0 seconds. 775.70/297.04 775.70/297.04 2) 'Best' failed due to the following reason: 775.70/297.04 775.70/297.04 None of the processors succeeded. 775.70/297.04 775.70/297.04 Details of failed attempt(s): 775.70/297.04 ----------------------------- 775.70/297.04 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 775.70/297.04 seconds)' failed due to the following reason: 775.70/297.04 775.70/297.04 Computation stopped due to timeout after 148.0 seconds. 775.70/297.04 775.70/297.04 2) 'Best' failed due to the following reason: 775.70/297.04 775.70/297.04 None of the processors succeeded. 775.70/297.04 775.70/297.04 Details of failed attempt(s): 775.70/297.04 ----------------------------- 775.70/297.04 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 775.70/297.04 to the following reason: 775.70/297.04 775.70/297.04 The processor is inapplicable, reason: 775.70/297.04 Processor only applicable for innermost runtime complexity analysis 775.70/297.04 775.70/297.04 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 775.70/297.04 following reason: 775.70/297.04 775.70/297.04 The processor is inapplicable, reason: 775.70/297.04 Processor only applicable for innermost runtime complexity analysis 775.70/297.04 775.70/297.04 775.70/297.04 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 775.70/297.04 failed due to the following reason: 775.70/297.04 775.70/297.04 None of the processors succeeded. 775.70/297.04 775.70/297.04 Details of failed attempt(s): 775.70/297.04 ----------------------------- 775.70/297.04 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 775.70/297.04 failed due to the following reason: 775.70/297.04 775.70/297.04 match-boundness of the problem could not be verified. 775.70/297.04 775.70/297.04 2) 'Bounds with minimal-enrichment and initial automaton 'match'' 775.70/297.04 failed due to the following reason: 775.70/297.04 775.70/297.04 match-boundness of the problem could not be verified. 775.70/297.04 775.70/297.04 775.70/297.04 775.70/297.04 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 775.70/297.04 the following reason: 775.70/297.04 775.70/297.04 We add the following weak dependency pairs: 775.70/297.04 775.70/297.04 Strict DPs: 775.70/297.04 { prod^#(xs) -> c_1(prodIter^#(xs, s(0()))) 775.70/297.04 , prodIter^#(xs, x) -> c_2(ifProd^#(isempty(xs), xs, x)) 775.70/297.04 , ifProd^#(true(), xs, x) -> c_3(x) 775.70/297.04 , ifProd^#(false(), xs, x) -> 775.70/297.04 c_4(prodIter^#(tail(xs), times(x, head(xs)))) 775.70/297.04 , isempty^#(nil()) -> c_5() 775.70/297.04 , isempty^#(cons(x, xs)) -> c_6() 775.70/297.04 , tail^#(nil()) -> c_7() 775.70/297.04 , tail^#(cons(x, xs)) -> c_8(xs) 775.70/297.04 , times^#(x, y) -> c_9(timesIter^#(x, y, 0(), 0())) 775.70/297.04 , timesIter^#(x, y, z, u) -> c_14(ifTimes^#(ge(u, x), x, y, z, u)) 775.70/297.04 , head^#(nil()) -> c_10() 775.70/297.04 , head^#(cons(x, xs)) -> c_11(x) 775.70/297.04 , plus^#(s(x), y) -> c_12(plus^#(x, y)) 775.70/297.04 , plus^#(0(), y) -> c_13(y) 775.70/297.04 , ifTimes^#(true(), x, y, z, u) -> c_15(z) 775.70/297.04 , ifTimes^#(false(), x, y, z, u) -> 775.70/297.04 c_16(timesIter^#(x, y, plus(y, z), s(u))) 775.70/297.04 , ge^#(x, 0()) -> c_17() 775.70/297.04 , ge^#(s(x), s(y)) -> c_18(ge^#(x, y)) 775.70/297.04 , ge^#(0(), s(y)) -> c_19() 775.70/297.04 , a^#() -> c_20() 775.70/297.04 , a^#() -> c_21() } 775.70/297.04 775.70/297.04 and mark the set of starting terms. 775.70/297.04 775.70/297.04 We are left with following problem, upon which TcT provides the 775.70/297.04 certificate MAYBE. 775.70/297.04 775.70/297.04 Strict DPs: 775.70/297.04 { prod^#(xs) -> c_1(prodIter^#(xs, s(0()))) 775.70/297.04 , prodIter^#(xs, x) -> c_2(ifProd^#(isempty(xs), xs, x)) 775.70/297.04 , ifProd^#(true(), xs, x) -> c_3(x) 775.70/297.04 , ifProd^#(false(), xs, x) -> 775.70/297.04 c_4(prodIter^#(tail(xs), times(x, head(xs)))) 775.70/297.04 , isempty^#(nil()) -> c_5() 775.70/297.04 , isempty^#(cons(x, xs)) -> c_6() 775.70/297.04 , tail^#(nil()) -> c_7() 775.70/297.04 , tail^#(cons(x, xs)) -> c_8(xs) 775.70/297.04 , times^#(x, y) -> c_9(timesIter^#(x, y, 0(), 0())) 775.70/297.04 , timesIter^#(x, y, z, u) -> c_14(ifTimes^#(ge(u, x), x, y, z, u)) 775.70/297.04 , head^#(nil()) -> c_10() 775.70/297.04 , head^#(cons(x, xs)) -> c_11(x) 775.70/297.04 , plus^#(s(x), y) -> c_12(plus^#(x, y)) 775.70/297.04 , plus^#(0(), y) -> c_13(y) 775.70/297.04 , ifTimes^#(true(), x, y, z, u) -> c_15(z) 775.70/297.04 , ifTimes^#(false(), x, y, z, u) -> 775.70/297.04 c_16(timesIter^#(x, y, plus(y, z), s(u))) 775.70/297.04 , ge^#(x, 0()) -> c_17() 775.70/297.04 , ge^#(s(x), s(y)) -> c_18(ge^#(x, y)) 775.70/297.04 , ge^#(0(), s(y)) -> c_19() 775.70/297.04 , a^#() -> c_20() 775.70/297.04 , a^#() -> c_21() } 775.70/297.04 Strict Trs: 775.70/297.04 { prod(xs) -> prodIter(xs, s(0())) 775.70/297.04 , prodIter(xs, x) -> ifProd(isempty(xs), xs, x) 775.70/297.04 , ifProd(true(), xs, x) -> x 775.70/297.04 , ifProd(false(), xs, x) -> prodIter(tail(xs), times(x, head(xs))) 775.70/297.04 , isempty(nil()) -> true() 775.70/297.04 , isempty(cons(x, xs)) -> false() 775.70/297.04 , tail(nil()) -> nil() 775.70/297.04 , tail(cons(x, xs)) -> xs 775.70/297.04 , times(x, y) -> timesIter(x, y, 0(), 0()) 775.70/297.04 , head(nil()) -> error() 775.70/297.04 , head(cons(x, xs)) -> x 775.70/297.04 , plus(s(x), y) -> s(plus(x, y)) 775.70/297.04 , plus(0(), y) -> y 775.70/297.04 , timesIter(x, y, z, u) -> ifTimes(ge(u, x), x, y, z, u) 775.70/297.04 , ifTimes(true(), x, y, z, u) -> z 775.70/297.04 , ifTimes(false(), x, y, z, u) -> timesIter(x, y, plus(y, z), s(u)) 775.70/297.04 , ge(x, 0()) -> true() 775.70/297.04 , ge(s(x), s(y)) -> ge(x, y) 775.70/297.04 , ge(0(), s(y)) -> false() 775.70/297.04 , a() -> b() 775.70/297.04 , a() -> c() } 775.70/297.04 Obligation: 775.70/297.04 runtime complexity 775.70/297.04 Answer: 775.70/297.04 MAYBE 775.70/297.04 775.70/297.04 We estimate the number of application of {5,6,7,11,17,19,20,21} by 775.70/297.04 applications of Pre({5,6,7,11,17,19,20,21}) = {3,8,12,14,15,18}. 775.70/297.04 Here rules are labeled as follows: 775.70/297.04 775.70/297.04 DPs: 775.70/297.04 { 1: prod^#(xs) -> c_1(prodIter^#(xs, s(0()))) 775.70/297.04 , 2: prodIter^#(xs, x) -> c_2(ifProd^#(isempty(xs), xs, x)) 775.70/297.04 , 3: ifProd^#(true(), xs, x) -> c_3(x) 775.70/297.04 , 4: ifProd^#(false(), xs, x) -> 775.70/297.04 c_4(prodIter^#(tail(xs), times(x, head(xs)))) 775.70/297.04 , 5: isempty^#(nil()) -> c_5() 775.70/297.04 , 6: isempty^#(cons(x, xs)) -> c_6() 775.70/297.04 , 7: tail^#(nil()) -> c_7() 775.70/297.04 , 8: tail^#(cons(x, xs)) -> c_8(xs) 775.70/297.04 , 9: times^#(x, y) -> c_9(timesIter^#(x, y, 0(), 0())) 775.70/297.04 , 10: timesIter^#(x, y, z, u) -> 775.70/297.04 c_14(ifTimes^#(ge(u, x), x, y, z, u)) 775.70/297.04 , 11: head^#(nil()) -> c_10() 775.70/297.04 , 12: head^#(cons(x, xs)) -> c_11(x) 775.70/297.04 , 13: plus^#(s(x), y) -> c_12(plus^#(x, y)) 775.70/297.04 , 14: plus^#(0(), y) -> c_13(y) 775.70/297.04 , 15: ifTimes^#(true(), x, y, z, u) -> c_15(z) 775.70/297.04 , 16: ifTimes^#(false(), x, y, z, u) -> 775.70/297.04 c_16(timesIter^#(x, y, plus(y, z), s(u))) 775.70/297.04 , 17: ge^#(x, 0()) -> c_17() 775.70/297.04 , 18: ge^#(s(x), s(y)) -> c_18(ge^#(x, y)) 775.70/297.04 , 19: ge^#(0(), s(y)) -> c_19() 775.70/297.04 , 20: a^#() -> c_20() 775.70/297.04 , 21: a^#() -> c_21() } 775.70/297.04 775.70/297.04 We are left with following problem, upon which TcT provides the 775.70/297.04 certificate MAYBE. 775.70/297.04 775.70/297.04 Strict DPs: 775.70/297.04 { prod^#(xs) -> c_1(prodIter^#(xs, s(0()))) 775.70/297.04 , prodIter^#(xs, x) -> c_2(ifProd^#(isempty(xs), xs, x)) 775.70/297.04 , ifProd^#(true(), xs, x) -> c_3(x) 775.70/297.04 , ifProd^#(false(), xs, x) -> 775.70/297.04 c_4(prodIter^#(tail(xs), times(x, head(xs)))) 775.70/297.04 , tail^#(cons(x, xs)) -> c_8(xs) 775.70/297.04 , times^#(x, y) -> c_9(timesIter^#(x, y, 0(), 0())) 775.70/297.04 , timesIter^#(x, y, z, u) -> c_14(ifTimes^#(ge(u, x), x, y, z, u)) 775.70/297.04 , head^#(cons(x, xs)) -> c_11(x) 775.70/297.04 , plus^#(s(x), y) -> c_12(plus^#(x, y)) 775.70/297.04 , plus^#(0(), y) -> c_13(y) 775.70/297.04 , ifTimes^#(true(), x, y, z, u) -> c_15(z) 775.70/297.04 , ifTimes^#(false(), x, y, z, u) -> 775.70/297.04 c_16(timesIter^#(x, y, plus(y, z), s(u))) 775.70/297.04 , ge^#(s(x), s(y)) -> c_18(ge^#(x, y)) } 775.70/297.04 Strict Trs: 775.70/297.04 { prod(xs) -> prodIter(xs, s(0())) 775.70/297.04 , prodIter(xs, x) -> ifProd(isempty(xs), xs, x) 775.70/297.04 , ifProd(true(), xs, x) -> x 775.70/297.04 , ifProd(false(), xs, x) -> prodIter(tail(xs), times(x, head(xs))) 775.70/297.04 , isempty(nil()) -> true() 775.70/297.04 , isempty(cons(x, xs)) -> false() 775.70/297.04 , tail(nil()) -> nil() 775.70/297.04 , tail(cons(x, xs)) -> xs 775.70/297.04 , times(x, y) -> timesIter(x, y, 0(), 0()) 775.70/297.04 , head(nil()) -> error() 775.70/297.04 , head(cons(x, xs)) -> x 775.70/297.04 , plus(s(x), y) -> s(plus(x, y)) 775.70/297.04 , plus(0(), y) -> y 775.70/297.04 , timesIter(x, y, z, u) -> ifTimes(ge(u, x), x, y, z, u) 775.70/297.04 , ifTimes(true(), x, y, z, u) -> z 775.70/297.04 , ifTimes(false(), x, y, z, u) -> timesIter(x, y, plus(y, z), s(u)) 775.70/297.04 , ge(x, 0()) -> true() 775.70/297.04 , ge(s(x), s(y)) -> ge(x, y) 775.70/297.04 , ge(0(), s(y)) -> false() 775.70/297.04 , a() -> b() 775.70/297.04 , a() -> c() } 775.70/297.04 Weak DPs: 775.70/297.04 { isempty^#(nil()) -> c_5() 775.70/297.04 , isempty^#(cons(x, xs)) -> c_6() 775.70/297.04 , tail^#(nil()) -> c_7() 775.70/297.04 , head^#(nil()) -> c_10() 775.70/297.04 , ge^#(x, 0()) -> c_17() 775.70/297.04 , ge^#(0(), s(y)) -> c_19() 775.70/297.04 , a^#() -> c_20() 775.70/297.04 , a^#() -> c_21() } 775.70/297.04 Obligation: 775.70/297.04 runtime complexity 775.70/297.04 Answer: 775.70/297.04 MAYBE 775.70/297.04 775.70/297.04 Empty strict component of the problem is NOT empty. 775.70/297.04 775.70/297.04 775.70/297.04 Arrrr.. 775.92/297.26 EOF