MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { isEmpty(cons(x, xs)) -> false() , isEmpty(nil()) -> true() , isZero(0()) -> true() , isZero(s(x)) -> false() , head(cons(x, xs)) -> x , tail(cons(x, xs)) -> xs , tail(nil()) -> nil() , p(0()) -> 0() , p(s(0())) -> 0() , p(s(s(x))) -> s(p(s(x))) , inc(0()) -> s(0()) , inc(s(x)) -> s(inc(x)) , sumList(xs, y) -> if(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)) , if(false(), false(), y, xs, ys, x) -> sumList(ys, x) , if(false(), true(), y, xs, ys, x) -> sumList(xs, y) , if(true(), b, y, xs, ys, x) -> y , sum(xs) -> sumList(xs, 0()) } 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 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) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed due to the following reason: We add the following weak dependency pairs: Strict DPs: { isEmpty^#(cons(x, xs)) -> c_1() , isEmpty^#(nil()) -> c_2() , isZero^#(0()) -> c_3() , isZero^#(s(x)) -> c_4() , head^#(cons(x, xs)) -> c_5(x) , tail^#(cons(x, xs)) -> c_6(xs) , tail^#(nil()) -> c_7() , p^#(0()) -> c_8() , p^#(s(0())) -> c_9() , p^#(s(s(x))) -> c_10(p^#(s(x))) , inc^#(0()) -> c_11() , inc^#(s(x)) -> c_12(inc^#(x)) , sumList^#(xs, y) -> c_13(if^#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y))) , if^#(false(), false(), y, xs, ys, x) -> c_14(sumList^#(ys, x)) , if^#(false(), true(), y, xs, ys, x) -> c_15(sumList^#(xs, y)) , if^#(true(), b, y, xs, ys, x) -> c_16(y) , sum^#(xs) -> c_17(sumList^#(xs, 0())) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { isEmpty^#(cons(x, xs)) -> c_1() , isEmpty^#(nil()) -> c_2() , isZero^#(0()) -> c_3() , isZero^#(s(x)) -> c_4() , head^#(cons(x, xs)) -> c_5(x) , tail^#(cons(x, xs)) -> c_6(xs) , tail^#(nil()) -> c_7() , p^#(0()) -> c_8() , p^#(s(0())) -> c_9() , p^#(s(s(x))) -> c_10(p^#(s(x))) , inc^#(0()) -> c_11() , inc^#(s(x)) -> c_12(inc^#(x)) , sumList^#(xs, y) -> c_13(if^#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y))) , if^#(false(), false(), y, xs, ys, x) -> c_14(sumList^#(ys, x)) , if^#(false(), true(), y, xs, ys, x) -> c_15(sumList^#(xs, y)) , if^#(true(), b, y, xs, ys, x) -> c_16(y) , sum^#(xs) -> c_17(sumList^#(xs, 0())) } Strict Trs: { isEmpty(cons(x, xs)) -> false() , isEmpty(nil()) -> true() , isZero(0()) -> true() , isZero(s(x)) -> false() , head(cons(x, xs)) -> x , tail(cons(x, xs)) -> xs , tail(nil()) -> nil() , p(0()) -> 0() , p(s(0())) -> 0() , p(s(s(x))) -> s(p(s(x))) , inc(0()) -> s(0()) , inc(s(x)) -> s(inc(x)) , sumList(xs, y) -> if(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)) , if(false(), false(), y, xs, ys, x) -> sumList(ys, x) , if(false(), true(), y, xs, ys, x) -> sumList(xs, y) , if(true(), b, y, xs, ys, x) -> y , sum(xs) -> sumList(xs, 0()) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {1,2,3,4,7,8,9,11} by applications of Pre({1,2,3,4,7,8,9,11}) = {5,6,10,12,16}. Here rules are labeled as follows: DPs: { 1: isEmpty^#(cons(x, xs)) -> c_1() , 2: isEmpty^#(nil()) -> c_2() , 3: isZero^#(0()) -> c_3() , 4: isZero^#(s(x)) -> c_4() , 5: head^#(cons(x, xs)) -> c_5(x) , 6: tail^#(cons(x, xs)) -> c_6(xs) , 7: tail^#(nil()) -> c_7() , 8: p^#(0()) -> c_8() , 9: p^#(s(0())) -> c_9() , 10: p^#(s(s(x))) -> c_10(p^#(s(x))) , 11: inc^#(0()) -> c_11() , 12: inc^#(s(x)) -> c_12(inc^#(x)) , 13: sumList^#(xs, y) -> c_13(if^#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y))) , 14: if^#(false(), false(), y, xs, ys, x) -> c_14(sumList^#(ys, x)) , 15: if^#(false(), true(), y, xs, ys, x) -> c_15(sumList^#(xs, y)) , 16: if^#(true(), b, y, xs, ys, x) -> c_16(y) , 17: sum^#(xs) -> c_17(sumList^#(xs, 0())) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { head^#(cons(x, xs)) -> c_5(x) , tail^#(cons(x, xs)) -> c_6(xs) , p^#(s(s(x))) -> c_10(p^#(s(x))) , inc^#(s(x)) -> c_12(inc^#(x)) , sumList^#(xs, y) -> c_13(if^#(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y))) , if^#(false(), false(), y, xs, ys, x) -> c_14(sumList^#(ys, x)) , if^#(false(), true(), y, xs, ys, x) -> c_15(sumList^#(xs, y)) , if^#(true(), b, y, xs, ys, x) -> c_16(y) , sum^#(xs) -> c_17(sumList^#(xs, 0())) } Strict Trs: { isEmpty(cons(x, xs)) -> false() , isEmpty(nil()) -> true() , isZero(0()) -> true() , isZero(s(x)) -> false() , head(cons(x, xs)) -> x , tail(cons(x, xs)) -> xs , tail(nil()) -> nil() , p(0()) -> 0() , p(s(0())) -> 0() , p(s(s(x))) -> s(p(s(x))) , inc(0()) -> s(0()) , inc(s(x)) -> s(inc(x)) , sumList(xs, y) -> if(isEmpty(xs), isZero(head(xs)), y, tail(xs), cons(p(head(xs)), tail(xs)), inc(y)) , if(false(), false(), y, xs, ys, x) -> sumList(ys, x) , if(false(), true(), y, xs, ys, x) -> sumList(xs, y) , if(true(), b, y, xs, ys, x) -> y , sum(xs) -> sumList(xs, 0()) } Weak DPs: { isEmpty^#(cons(x, xs)) -> c_1() , isEmpty^#(nil()) -> c_2() , isZero^#(0()) -> c_3() , isZero^#(s(x)) -> c_4() , tail^#(nil()) -> c_7() , p^#(0()) -> c_8() , p^#(s(0())) -> c_9() , inc^#(0()) -> c_11() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..