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