MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { times(x, y) -> sum(generate(x, y)) , sum(xs) -> sum2(xs, 0()) , generate(x, y) -> gen(x, y, 0()) , gen(x, y, z) -> if(ge(z, x), x, y, z) , if(true(), x, y, z) -> nil() , if(false(), x, y, z) -> cons(y, gen(x, y, s(z))) , ge(x, 0()) -> true() , ge(0(), s(y)) -> false() , ge(s(x), s(y)) -> ge(x, y) , sum2(xs, y) -> ifsum(isNil(xs), isZero(head(xs)), xs, y) , ifsum(true(), b, xs, y) -> y , ifsum(false(), b, xs, y) -> ifsum2(b, xs, y) , isNil(nil()) -> true() , isNil(cons(x, xs)) -> false() , isZero(0()) -> true() , isZero(s(0())) -> false() , isZero(s(s(x))) -> isZero(s(x)) , head(nil()) -> error() , head(cons(x, xs)) -> x , ifsum2(true(), xs, y) -> sum2(tail(xs), y) , ifsum2(false(), xs, y) -> sum2(cons(p(head(xs)), tail(xs)), s(y)) , tail(nil()) -> nil() , tail(cons(x, xs)) -> xs , p(0()) -> s(s(0())) , p(s(0())) -> 0() , p(s(s(x))) -> s(p(s(x))) , a() -> c() , a() -> d() } 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) '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 minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 3) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) '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 2) '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 3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed due to the following reason: We add the following weak dependency pairs: Strict DPs: { times^#(x, y) -> c_1(sum^#(generate(x, y))) , sum^#(xs) -> c_2(sum2^#(xs, 0())) , sum2^#(xs, y) -> c_10(ifsum^#(isNil(xs), isZero(head(xs)), xs, y)) , generate^#(x, y) -> c_3(gen^#(x, y, 0())) , gen^#(x, y, z) -> c_4(if^#(ge(z, x), x, y, z)) , if^#(true(), x, y, z) -> c_5() , if^#(false(), x, y, z) -> c_6(y, gen^#(x, y, s(z))) , ge^#(x, 0()) -> c_7() , ge^#(0(), s(y)) -> c_8() , ge^#(s(x), s(y)) -> c_9(ge^#(x, y)) , ifsum^#(true(), b, xs, y) -> c_11(y) , ifsum^#(false(), b, xs, y) -> c_12(ifsum2^#(b, xs, y)) , ifsum2^#(true(), xs, y) -> c_20(sum2^#(tail(xs), y)) , ifsum2^#(false(), xs, y) -> c_21(sum2^#(cons(p(head(xs)), tail(xs)), s(y))) , isNil^#(nil()) -> c_13() , isNil^#(cons(x, xs)) -> c_14() , isZero^#(0()) -> c_15() , isZero^#(s(0())) -> c_16() , isZero^#(s(s(x))) -> c_17(isZero^#(s(x))) , head^#(nil()) -> c_18() , head^#(cons(x, xs)) -> c_19(x) , tail^#(nil()) -> c_22() , tail^#(cons(x, xs)) -> c_23(xs) , p^#(0()) -> c_24() , p^#(s(0())) -> c_25() , p^#(s(s(x))) -> c_26(p^#(s(x))) , a^#() -> c_27() , a^#() -> c_28() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { times^#(x, y) -> c_1(sum^#(generate(x, y))) , sum^#(xs) -> c_2(sum2^#(xs, 0())) , sum2^#(xs, y) -> c_10(ifsum^#(isNil(xs), isZero(head(xs)), xs, y)) , generate^#(x, y) -> c_3(gen^#(x, y, 0())) , gen^#(x, y, z) -> c_4(if^#(ge(z, x), x, y, z)) , if^#(true(), x, y, z) -> c_5() , if^#(false(), x, y, z) -> c_6(y, gen^#(x, y, s(z))) , ge^#(x, 0()) -> c_7() , ge^#(0(), s(y)) -> c_8() , ge^#(s(x), s(y)) -> c_9(ge^#(x, y)) , ifsum^#(true(), b, xs, y) -> c_11(y) , ifsum^#(false(), b, xs, y) -> c_12(ifsum2^#(b, xs, y)) , ifsum2^#(true(), xs, y) -> c_20(sum2^#(tail(xs), y)) , ifsum2^#(false(), xs, y) -> c_21(sum2^#(cons(p(head(xs)), tail(xs)), s(y))) , isNil^#(nil()) -> c_13() , isNil^#(cons(x, xs)) -> c_14() , isZero^#(0()) -> c_15() , isZero^#(s(0())) -> c_16() , isZero^#(s(s(x))) -> c_17(isZero^#(s(x))) , head^#(nil()) -> c_18() , head^#(cons(x, xs)) -> c_19(x) , tail^#(nil()) -> c_22() , tail^#(cons(x, xs)) -> c_23(xs) , p^#(0()) -> c_24() , p^#(s(0())) -> c_25() , p^#(s(s(x))) -> c_26(p^#(s(x))) , a^#() -> c_27() , a^#() -> c_28() } Strict Trs: { times(x, y) -> sum(generate(x, y)) , sum(xs) -> sum2(xs, 0()) , generate(x, y) -> gen(x, y, 0()) , gen(x, y, z) -> if(ge(z, x), x, y, z) , if(true(), x, y, z) -> nil() , if(false(), x, y, z) -> cons(y, gen(x, y, s(z))) , ge(x, 0()) -> true() , ge(0(), s(y)) -> false() , ge(s(x), s(y)) -> ge(x, y) , sum2(xs, y) -> ifsum(isNil(xs), isZero(head(xs)), xs, y) , ifsum(true(), b, xs, y) -> y , ifsum(false(), b, xs, y) -> ifsum2(b, xs, y) , isNil(nil()) -> true() , isNil(cons(x, xs)) -> false() , isZero(0()) -> true() , isZero(s(0())) -> false() , isZero(s(s(x))) -> isZero(s(x)) , head(nil()) -> error() , head(cons(x, xs)) -> x , ifsum2(true(), xs, y) -> sum2(tail(xs), y) , ifsum2(false(), xs, y) -> sum2(cons(p(head(xs)), tail(xs)), s(y)) , tail(nil()) -> nil() , tail(cons(x, xs)) -> xs , p(0()) -> s(s(0())) , p(s(0())) -> 0() , p(s(s(x))) -> s(p(s(x))) , a() -> c() , a() -> d() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {6,8,9,15,16,17,18,20,22,24,25,27,28} by applications of Pre({6,8,9,15,16,17,18,20,22,24,25,27,28}) = {5,7,10,11,19,21,23,26}. Here rules are labeled as follows: DPs: { 1: times^#(x, y) -> c_1(sum^#(generate(x, y))) , 2: sum^#(xs) -> c_2(sum2^#(xs, 0())) , 3: sum2^#(xs, y) -> c_10(ifsum^#(isNil(xs), isZero(head(xs)), xs, y)) , 4: generate^#(x, y) -> c_3(gen^#(x, y, 0())) , 5: gen^#(x, y, z) -> c_4(if^#(ge(z, x), x, y, z)) , 6: if^#(true(), x, y, z) -> c_5() , 7: if^#(false(), x, y, z) -> c_6(y, gen^#(x, y, s(z))) , 8: ge^#(x, 0()) -> c_7() , 9: ge^#(0(), s(y)) -> c_8() , 10: ge^#(s(x), s(y)) -> c_9(ge^#(x, y)) , 11: ifsum^#(true(), b, xs, y) -> c_11(y) , 12: ifsum^#(false(), b, xs, y) -> c_12(ifsum2^#(b, xs, y)) , 13: ifsum2^#(true(), xs, y) -> c_20(sum2^#(tail(xs), y)) , 14: ifsum2^#(false(), xs, y) -> c_21(sum2^#(cons(p(head(xs)), tail(xs)), s(y))) , 15: isNil^#(nil()) -> c_13() , 16: isNil^#(cons(x, xs)) -> c_14() , 17: isZero^#(0()) -> c_15() , 18: isZero^#(s(0())) -> c_16() , 19: isZero^#(s(s(x))) -> c_17(isZero^#(s(x))) , 20: head^#(nil()) -> c_18() , 21: head^#(cons(x, xs)) -> c_19(x) , 22: tail^#(nil()) -> c_22() , 23: tail^#(cons(x, xs)) -> c_23(xs) , 24: p^#(0()) -> c_24() , 25: p^#(s(0())) -> c_25() , 26: p^#(s(s(x))) -> c_26(p^#(s(x))) , 27: a^#() -> c_27() , 28: a^#() -> c_28() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { times^#(x, y) -> c_1(sum^#(generate(x, y))) , sum^#(xs) -> c_2(sum2^#(xs, 0())) , sum2^#(xs, y) -> c_10(ifsum^#(isNil(xs), isZero(head(xs)), xs, y)) , generate^#(x, y) -> c_3(gen^#(x, y, 0())) , gen^#(x, y, z) -> c_4(if^#(ge(z, x), x, y, z)) , if^#(false(), x, y, z) -> c_6(y, gen^#(x, y, s(z))) , ge^#(s(x), s(y)) -> c_9(ge^#(x, y)) , ifsum^#(true(), b, xs, y) -> c_11(y) , ifsum^#(false(), b, xs, y) -> c_12(ifsum2^#(b, xs, y)) , ifsum2^#(true(), xs, y) -> c_20(sum2^#(tail(xs), y)) , ifsum2^#(false(), xs, y) -> c_21(sum2^#(cons(p(head(xs)), tail(xs)), s(y))) , isZero^#(s(s(x))) -> c_17(isZero^#(s(x))) , head^#(cons(x, xs)) -> c_19(x) , tail^#(cons(x, xs)) -> c_23(xs) , p^#(s(s(x))) -> c_26(p^#(s(x))) } Strict Trs: { times(x, y) -> sum(generate(x, y)) , sum(xs) -> sum2(xs, 0()) , generate(x, y) -> gen(x, y, 0()) , gen(x, y, z) -> if(ge(z, x), x, y, z) , if(true(), x, y, z) -> nil() , if(false(), x, y, z) -> cons(y, gen(x, y, s(z))) , ge(x, 0()) -> true() , ge(0(), s(y)) -> false() , ge(s(x), s(y)) -> ge(x, y) , sum2(xs, y) -> ifsum(isNil(xs), isZero(head(xs)), xs, y) , ifsum(true(), b, xs, y) -> y , ifsum(false(), b, xs, y) -> ifsum2(b, xs, y) , isNil(nil()) -> true() , isNil(cons(x, xs)) -> false() , isZero(0()) -> true() , isZero(s(0())) -> false() , isZero(s(s(x))) -> isZero(s(x)) , head(nil()) -> error() , head(cons(x, xs)) -> x , ifsum2(true(), xs, y) -> sum2(tail(xs), y) , ifsum2(false(), xs, y) -> sum2(cons(p(head(xs)), tail(xs)), s(y)) , tail(nil()) -> nil() , tail(cons(x, xs)) -> xs , p(0()) -> s(s(0())) , p(s(0())) -> 0() , p(s(s(x))) -> s(p(s(x))) , a() -> c() , a() -> d() } Weak DPs: { if^#(true(), x, y, z) -> c_5() , ge^#(x, 0()) -> c_7() , ge^#(0(), s(y)) -> c_8() , isNil^#(nil()) -> c_13() , isNil^#(cons(x, xs)) -> c_14() , isZero^#(0()) -> c_15() , isZero^#(s(0())) -> c_16() , head^#(nil()) -> c_18() , tail^#(nil()) -> c_22() , p^#(0()) -> c_24() , p^#(s(0())) -> c_25() , a^#() -> c_27() , a^#() -> c_28() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..