MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { qsort(nil()) -> nil() , qsort(cons(x, xs)) -> append(qsort(filterlow(last(cons(x, xs)), cons(x, xs))), cons(last(cons(x, xs)), qsort(filterhigh(last(cons(x, xs)), cons(x, xs))))) , append(nil(), ys()) -> ys() , append(cons(x, xs), ys()) -> cons(x, append(xs, ys())) , filterlow(n, nil()) -> nil() , filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs) , last(nil()) -> 0() , last(cons(x, nil())) -> x , last(cons(x, cons(y, xs))) -> last(cons(y, xs)) , filterhigh(n, nil()) -> nil() , filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs) , if1(true(), n, x, xs) -> filterlow(n, xs) , if1(false(), n, x, xs) -> cons(x, filterlow(n, xs)) , ge(x, 0()) -> true() , ge(0(), s(x)) -> false() , ge(s(x), s(y)) -> ge(x, y) , if2(true(), n, x, xs) -> filterhigh(n, xs) , if2(false(), n, x, xs) -> cons(x, filterhigh(n, xs)) } 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: { qsort^#(nil()) -> c_1() , qsort^#(cons(x, xs)) -> c_2(append^#(qsort(filterlow(last(cons(x, xs)), cons(x, xs))), cons(last(cons(x, xs)), qsort(filterhigh(last(cons(x, xs)), cons(x, xs)))))) , append^#(nil(), ys()) -> c_3() , append^#(cons(x, xs), ys()) -> c_4(x, append^#(xs, ys())) , filterlow^#(n, nil()) -> c_5() , filterlow^#(n, cons(x, xs)) -> c_6(if1^#(ge(n, x), n, x, xs)) , if1^#(true(), n, x, xs) -> c_12(filterlow^#(n, xs)) , if1^#(false(), n, x, xs) -> c_13(x, filterlow^#(n, xs)) , last^#(nil()) -> c_7() , last^#(cons(x, nil())) -> c_8(x) , last^#(cons(x, cons(y, xs))) -> c_9(last^#(cons(y, xs))) , filterhigh^#(n, nil()) -> c_10() , filterhigh^#(n, cons(x, xs)) -> c_11(if2^#(ge(x, n), n, x, xs)) , if2^#(true(), n, x, xs) -> c_17(filterhigh^#(n, xs)) , if2^#(false(), n, x, xs) -> c_18(x, filterhigh^#(n, xs)) , ge^#(x, 0()) -> c_14() , ge^#(0(), s(x)) -> c_15() , ge^#(s(x), s(y)) -> c_16(ge^#(x, y)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { qsort^#(nil()) -> c_1() , qsort^#(cons(x, xs)) -> c_2(append^#(qsort(filterlow(last(cons(x, xs)), cons(x, xs))), cons(last(cons(x, xs)), qsort(filterhigh(last(cons(x, xs)), cons(x, xs)))))) , append^#(nil(), ys()) -> c_3() , append^#(cons(x, xs), ys()) -> c_4(x, append^#(xs, ys())) , filterlow^#(n, nil()) -> c_5() , filterlow^#(n, cons(x, xs)) -> c_6(if1^#(ge(n, x), n, x, xs)) , if1^#(true(), n, x, xs) -> c_12(filterlow^#(n, xs)) , if1^#(false(), n, x, xs) -> c_13(x, filterlow^#(n, xs)) , last^#(nil()) -> c_7() , last^#(cons(x, nil())) -> c_8(x) , last^#(cons(x, cons(y, xs))) -> c_9(last^#(cons(y, xs))) , filterhigh^#(n, nil()) -> c_10() , filterhigh^#(n, cons(x, xs)) -> c_11(if2^#(ge(x, n), n, x, xs)) , if2^#(true(), n, x, xs) -> c_17(filterhigh^#(n, xs)) , if2^#(false(), n, x, xs) -> c_18(x, filterhigh^#(n, xs)) , ge^#(x, 0()) -> c_14() , ge^#(0(), s(x)) -> c_15() , ge^#(s(x), s(y)) -> c_16(ge^#(x, y)) } Strict Trs: { qsort(nil()) -> nil() , qsort(cons(x, xs)) -> append(qsort(filterlow(last(cons(x, xs)), cons(x, xs))), cons(last(cons(x, xs)), qsort(filterhigh(last(cons(x, xs)), cons(x, xs))))) , append(nil(), ys()) -> ys() , append(cons(x, xs), ys()) -> cons(x, append(xs, ys())) , filterlow(n, nil()) -> nil() , filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs) , last(nil()) -> 0() , last(cons(x, nil())) -> x , last(cons(x, cons(y, xs))) -> last(cons(y, xs)) , filterhigh(n, nil()) -> nil() , filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs) , if1(true(), n, x, xs) -> filterlow(n, xs) , if1(false(), n, x, xs) -> cons(x, filterlow(n, xs)) , ge(x, 0()) -> true() , ge(0(), s(x)) -> false() , ge(s(x), s(y)) -> ge(x, y) , if2(true(), n, x, xs) -> filterhigh(n, xs) , if2(false(), n, x, xs) -> cons(x, filterhigh(n, xs)) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {1,2,3,5,9,12,16,17} by applications of Pre({1,2,3,5,9,12,16,17}) = {4,7,8,10,14,15,18}. Here rules are labeled as follows: DPs: { 1: qsort^#(nil()) -> c_1() , 2: qsort^#(cons(x, xs)) -> c_2(append^#(qsort(filterlow(last(cons(x, xs)), cons(x, xs))), cons(last(cons(x, xs)), qsort(filterhigh(last(cons(x, xs)), cons(x, xs)))))) , 3: append^#(nil(), ys()) -> c_3() , 4: append^#(cons(x, xs), ys()) -> c_4(x, append^#(xs, ys())) , 5: filterlow^#(n, nil()) -> c_5() , 6: filterlow^#(n, cons(x, xs)) -> c_6(if1^#(ge(n, x), n, x, xs)) , 7: if1^#(true(), n, x, xs) -> c_12(filterlow^#(n, xs)) , 8: if1^#(false(), n, x, xs) -> c_13(x, filterlow^#(n, xs)) , 9: last^#(nil()) -> c_7() , 10: last^#(cons(x, nil())) -> c_8(x) , 11: last^#(cons(x, cons(y, xs))) -> c_9(last^#(cons(y, xs))) , 12: filterhigh^#(n, nil()) -> c_10() , 13: filterhigh^#(n, cons(x, xs)) -> c_11(if2^#(ge(x, n), n, x, xs)) , 14: if2^#(true(), n, x, xs) -> c_17(filterhigh^#(n, xs)) , 15: if2^#(false(), n, x, xs) -> c_18(x, filterhigh^#(n, xs)) , 16: ge^#(x, 0()) -> c_14() , 17: ge^#(0(), s(x)) -> c_15() , 18: ge^#(s(x), s(y)) -> c_16(ge^#(x, y)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { append^#(cons(x, xs), ys()) -> c_4(x, append^#(xs, ys())) , filterlow^#(n, cons(x, xs)) -> c_6(if1^#(ge(n, x), n, x, xs)) , if1^#(true(), n, x, xs) -> c_12(filterlow^#(n, xs)) , if1^#(false(), n, x, xs) -> c_13(x, filterlow^#(n, xs)) , last^#(cons(x, nil())) -> c_8(x) , last^#(cons(x, cons(y, xs))) -> c_9(last^#(cons(y, xs))) , filterhigh^#(n, cons(x, xs)) -> c_11(if2^#(ge(x, n), n, x, xs)) , if2^#(true(), n, x, xs) -> c_17(filterhigh^#(n, xs)) , if2^#(false(), n, x, xs) -> c_18(x, filterhigh^#(n, xs)) , ge^#(s(x), s(y)) -> c_16(ge^#(x, y)) } Strict Trs: { qsort(nil()) -> nil() , qsort(cons(x, xs)) -> append(qsort(filterlow(last(cons(x, xs)), cons(x, xs))), cons(last(cons(x, xs)), qsort(filterhigh(last(cons(x, xs)), cons(x, xs))))) , append(nil(), ys()) -> ys() , append(cons(x, xs), ys()) -> cons(x, append(xs, ys())) , filterlow(n, nil()) -> nil() , filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs) , last(nil()) -> 0() , last(cons(x, nil())) -> x , last(cons(x, cons(y, xs))) -> last(cons(y, xs)) , filterhigh(n, nil()) -> nil() , filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs) , if1(true(), n, x, xs) -> filterlow(n, xs) , if1(false(), n, x, xs) -> cons(x, filterlow(n, xs)) , ge(x, 0()) -> true() , ge(0(), s(x)) -> false() , ge(s(x), s(y)) -> ge(x, y) , if2(true(), n, x, xs) -> filterhigh(n, xs) , if2(false(), n, x, xs) -> cons(x, filterhigh(n, xs)) } Weak DPs: { qsort^#(nil()) -> c_1() , qsort^#(cons(x, xs)) -> c_2(append^#(qsort(filterlow(last(cons(x, xs)), cons(x, xs))), cons(last(cons(x, xs)), qsort(filterhigh(last(cons(x, xs)), cons(x, xs)))))) , append^#(nil(), ys()) -> c_3() , filterlow^#(n, nil()) -> c_5() , last^#(nil()) -> c_7() , filterhigh^#(n, nil()) -> c_10() , ge^#(x, 0()) -> c_14() , ge^#(0(), s(x)) -> c_15() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..