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