MAYBE
823.82/297.03	MAYBE
823.82/297.03	
823.82/297.03	We are left with following problem, upon which TcT provides the
823.82/297.03	certificate MAYBE.
823.82/297.03	
823.82/297.03	Strict Trs:
823.82/297.03	  { qsort(xs) -> qs(half(length(xs)), xs)
823.82/297.03	  , qs(n, nil()) -> nil()
823.82/297.03	  , qs(n, cons(x, xs)) ->
823.82/297.03	    append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))),
823.82/297.03	           cons(get(n, cons(x, xs)),
823.82/297.03	                qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
823.82/297.03	  , half(0()) -> 0()
823.82/297.03	  , half(s(0())) -> 0()
823.82/297.03	  , half(s(s(x))) -> s(half(x))
823.82/297.03	  , length(nil()) -> 0()
823.82/297.03	  , length(cons(x, xs)) -> s(length(xs))
823.82/297.03	  , append(nil(), ys()) -> ys()
823.82/297.03	  , append(cons(x, xs), ys()) -> cons(x, append(xs, ys()))
823.82/297.03	  , filterlow(n, nil()) -> nil()
823.82/297.03	  , filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
823.82/297.03	  , get(n, nil()) -> 0()
823.82/297.03	  , get(n, cons(x, nil())) -> x
823.82/297.03	  , get(0(), cons(x, cons(y, xs))) -> x
823.82/297.03	  , get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))
823.82/297.03	  , filterhigh(n, nil()) -> nil()
823.82/297.03	  , filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
823.82/297.03	  , if1(true(), n, x, xs) -> filterlow(n, xs)
823.82/297.03	  , if1(false(), n, x, xs) -> cons(x, filterlow(n, xs))
823.82/297.03	  , ge(x, 0()) -> true()
823.82/297.03	  , ge(0(), s(x)) -> false()
823.82/297.03	  , ge(s(x), s(y)) -> ge(x, y)
823.82/297.03	  , if2(true(), n, x, xs) -> filterhigh(n, xs)
823.82/297.03	  , if2(false(), n, x, xs) -> cons(x, filterhigh(n, xs)) }
823.82/297.03	Obligation:
823.82/297.03	  runtime complexity
823.82/297.03	Answer:
823.82/297.03	  MAYBE
823.82/297.03	
823.82/297.03	None of the processors succeeded.
823.82/297.03	
823.82/297.03	Details of failed attempt(s):
823.82/297.03	-----------------------------
823.82/297.03	1) 'With Problem ... (timeout of 297 seconds)' failed due to the
823.82/297.03	   following reason:
823.82/297.03	   
823.82/297.03	   Computation stopped due to timeout after 297.0 seconds.
823.82/297.03	
823.82/297.03	2) 'Best' failed due to the following reason:
823.82/297.03	   
823.82/297.03	   None of the processors succeeded.
823.82/297.03	   
823.82/297.03	   Details of failed attempt(s):
823.82/297.03	   -----------------------------
823.82/297.03	   1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
823.82/297.03	      seconds)' failed due to the following reason:
823.82/297.03	      
823.82/297.03	      Computation stopped due to timeout after 148.0 seconds.
823.82/297.03	   
823.82/297.03	   2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
823.82/297.03	      failed due to the following reason:
823.82/297.03	      
823.82/297.03	      None of the processors succeeded.
823.82/297.03	      
823.82/297.03	      Details of failed attempt(s):
823.82/297.03	      -----------------------------
823.82/297.03	      1) 'Bounds with minimal-enrichment and initial automaton 'match''
823.82/297.03	         failed due to the following reason:
823.82/297.03	         
823.82/297.03	         match-boundness of the problem could not be verified.
823.82/297.03	      
823.82/297.03	      2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
823.82/297.03	         failed due to the following reason:
823.82/297.03	         
823.82/297.03	         match-boundness of the problem could not be verified.
823.82/297.03	      
823.82/297.03	   
823.82/297.03	   3) 'Best' failed due to the following reason:
823.82/297.03	      
823.82/297.03	      None of the processors succeeded.
823.82/297.03	      
823.82/297.03	      Details of failed attempt(s):
823.82/297.03	      -----------------------------
823.82/297.03	      1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
823.82/297.03	         following reason:
823.82/297.03	         
823.82/297.03	         The processor is inapplicable, reason:
823.82/297.03	           Processor only applicable for innermost runtime complexity analysis
823.82/297.03	      
823.82/297.03	      2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
823.82/297.03	         to the following reason:
823.82/297.03	         
823.82/297.03	         The processor is inapplicable, reason:
823.82/297.03	           Processor only applicable for innermost runtime complexity analysis
823.82/297.03	      
823.82/297.03	   
823.82/297.03	
823.82/297.03	3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to
823.82/297.03	   the following reason:
823.82/297.03	   
823.82/297.03	   We add the following weak dependency pairs:
823.82/297.03	   
823.82/297.03	   Strict DPs:
823.82/297.03	     { qsort^#(xs) -> c_1(qs^#(half(length(xs)), xs))
823.82/297.03	     , qs^#(n, nil()) -> c_2()
823.82/297.03	     , qs^#(n, cons(x, xs)) ->
823.82/297.03	       c_3(append^#(qs(half(n),
823.82/297.03	                       filterlow(get(n, cons(x, xs)), cons(x, xs))),
823.82/297.03	                    cons(get(n, cons(x, xs)),
823.82/297.03	                         qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs))))))
823.82/297.03	     , append^#(nil(), ys()) -> c_9()
823.82/297.03	     , append^#(cons(x, xs), ys()) -> c_10(x, append^#(xs, ys()))
823.82/297.03	     , half^#(0()) -> c_4()
823.82/297.03	     , half^#(s(0())) -> c_5()
823.82/297.03	     , half^#(s(s(x))) -> c_6(half^#(x))
823.82/297.03	     , length^#(nil()) -> c_7()
823.82/297.03	     , length^#(cons(x, xs)) -> c_8(length^#(xs))
823.82/297.03	     , filterlow^#(n, nil()) -> c_11()
823.82/297.03	     , filterlow^#(n, cons(x, xs)) -> c_12(if1^#(ge(n, x), n, x, xs))
823.82/297.03	     , if1^#(true(), n, x, xs) -> c_19(filterlow^#(n, xs))
823.82/297.03	     , if1^#(false(), n, x, xs) -> c_20(x, filterlow^#(n, xs))
823.82/297.03	     , get^#(n, nil()) -> c_13()
823.82/297.03	     , get^#(n, cons(x, nil())) -> c_14(x)
823.82/297.03	     , get^#(0(), cons(x, cons(y, xs))) -> c_15(x)
823.82/297.03	     , get^#(s(n), cons(x, cons(y, xs))) -> c_16(get^#(n, cons(y, xs)))
823.82/297.03	     , filterhigh^#(n, nil()) -> c_17()
823.82/297.03	     , filterhigh^#(n, cons(x, xs)) -> c_18(if2^#(ge(x, n), n, x, xs))
823.82/297.03	     , if2^#(true(), n, x, xs) -> c_24(filterhigh^#(n, xs))
823.82/297.03	     , if2^#(false(), n, x, xs) -> c_25(x, filterhigh^#(n, xs))
823.82/297.03	     , ge^#(x, 0()) -> c_21()
823.82/297.03	     , ge^#(0(), s(x)) -> c_22()
823.82/297.03	     , ge^#(s(x), s(y)) -> c_23(ge^#(x, y)) }
823.82/297.03	   
823.82/297.03	   and mark the set of starting terms.
823.82/297.03	   
823.82/297.03	   We are left with following problem, upon which TcT provides the
823.82/297.03	   certificate MAYBE.
823.82/297.03	   
823.82/297.03	   Strict DPs:
823.82/297.03	     { qsort^#(xs) -> c_1(qs^#(half(length(xs)), xs))
823.82/297.03	     , qs^#(n, nil()) -> c_2()
823.82/297.03	     , qs^#(n, cons(x, xs)) ->
823.82/297.03	       c_3(append^#(qs(half(n),
823.82/297.03	                       filterlow(get(n, cons(x, xs)), cons(x, xs))),
823.82/297.03	                    cons(get(n, cons(x, xs)),
823.82/297.03	                         qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs))))))
823.82/297.03	     , append^#(nil(), ys()) -> c_9()
823.82/297.03	     , append^#(cons(x, xs), ys()) -> c_10(x, append^#(xs, ys()))
823.82/297.03	     , half^#(0()) -> c_4()
823.82/297.03	     , half^#(s(0())) -> c_5()
823.82/297.03	     , half^#(s(s(x))) -> c_6(half^#(x))
823.82/297.03	     , length^#(nil()) -> c_7()
823.82/297.03	     , length^#(cons(x, xs)) -> c_8(length^#(xs))
823.82/297.03	     , filterlow^#(n, nil()) -> c_11()
823.82/297.03	     , filterlow^#(n, cons(x, xs)) -> c_12(if1^#(ge(n, x), n, x, xs))
823.82/297.03	     , if1^#(true(), n, x, xs) -> c_19(filterlow^#(n, xs))
823.82/297.03	     , if1^#(false(), n, x, xs) -> c_20(x, filterlow^#(n, xs))
823.82/297.03	     , get^#(n, nil()) -> c_13()
823.82/297.03	     , get^#(n, cons(x, nil())) -> c_14(x)
823.82/297.03	     , get^#(0(), cons(x, cons(y, xs))) -> c_15(x)
823.82/297.03	     , get^#(s(n), cons(x, cons(y, xs))) -> c_16(get^#(n, cons(y, xs)))
823.82/297.03	     , filterhigh^#(n, nil()) -> c_17()
823.82/297.03	     , filterhigh^#(n, cons(x, xs)) -> c_18(if2^#(ge(x, n), n, x, xs))
823.82/297.03	     , if2^#(true(), n, x, xs) -> c_24(filterhigh^#(n, xs))
823.82/297.03	     , if2^#(false(), n, x, xs) -> c_25(x, filterhigh^#(n, xs))
823.82/297.03	     , ge^#(x, 0()) -> c_21()
823.82/297.03	     , ge^#(0(), s(x)) -> c_22()
823.82/297.03	     , ge^#(s(x), s(y)) -> c_23(ge^#(x, y)) }
823.82/297.03	   Strict Trs:
823.82/297.03	     { qsort(xs) -> qs(half(length(xs)), xs)
823.82/297.03	     , qs(n, nil()) -> nil()
823.82/297.03	     , qs(n, cons(x, xs)) ->
823.82/297.03	       append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))),
823.82/297.03	              cons(get(n, cons(x, xs)),
823.82/297.03	                   qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
823.82/297.03	     , half(0()) -> 0()
823.82/297.03	     , half(s(0())) -> 0()
823.82/297.03	     , half(s(s(x))) -> s(half(x))
823.82/297.03	     , length(nil()) -> 0()
823.82/297.03	     , length(cons(x, xs)) -> s(length(xs))
823.82/297.03	     , append(nil(), ys()) -> ys()
823.82/297.03	     , append(cons(x, xs), ys()) -> cons(x, append(xs, ys()))
823.82/297.03	     , filterlow(n, nil()) -> nil()
823.82/297.03	     , filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
823.82/297.03	     , get(n, nil()) -> 0()
823.82/297.03	     , get(n, cons(x, nil())) -> x
823.82/297.03	     , get(0(), cons(x, cons(y, xs))) -> x
823.82/297.03	     , get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))
823.82/297.03	     , filterhigh(n, nil()) -> nil()
823.82/297.03	     , filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
823.82/297.03	     , if1(true(), n, x, xs) -> filterlow(n, xs)
823.82/297.03	     , if1(false(), n, x, xs) -> cons(x, filterlow(n, xs))
823.82/297.03	     , ge(x, 0()) -> true()
823.82/297.03	     , ge(0(), s(x)) -> false()
823.82/297.03	     , ge(s(x), s(y)) -> ge(x, y)
823.82/297.03	     , if2(true(), n, x, xs) -> filterhigh(n, xs)
823.82/297.03	     , if2(false(), n, x, xs) -> cons(x, filterhigh(n, xs)) }
823.82/297.03	   Obligation:
823.82/297.03	     runtime complexity
823.82/297.03	   Answer:
823.82/297.03	     MAYBE
823.82/297.03	   
823.82/297.03	   We estimate the number of application of
823.82/297.03	   {2,3,4,6,7,9,11,15,19,23,24} by applications of
823.82/297.03	   Pre({2,3,4,6,7,9,11,15,19,23,24}) =
823.82/297.03	   {1,5,8,10,13,14,16,17,21,22,25}. Here rules are labeled as follows:
823.82/297.03	   
823.82/297.03	     DPs:
823.82/297.03	       { 1: qsort^#(xs) -> c_1(qs^#(half(length(xs)), xs))
823.82/297.03	       , 2: qs^#(n, nil()) -> c_2()
823.82/297.03	       , 3: qs^#(n, cons(x, xs)) ->
823.82/297.03	            c_3(append^#(qs(half(n),
823.82/297.03	                            filterlow(get(n, cons(x, xs)), cons(x, xs))),
823.82/297.03	                         cons(get(n, cons(x, xs)),
823.82/297.03	                              qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs))))))
823.82/297.03	       , 4: append^#(nil(), ys()) -> c_9()
823.82/297.03	       , 5: append^#(cons(x, xs), ys()) -> c_10(x, append^#(xs, ys()))
823.82/297.03	       , 6: half^#(0()) -> c_4()
823.82/297.03	       , 7: half^#(s(0())) -> c_5()
823.82/297.03	       , 8: half^#(s(s(x))) -> c_6(half^#(x))
823.82/297.03	       , 9: length^#(nil()) -> c_7()
823.82/297.03	       , 10: length^#(cons(x, xs)) -> c_8(length^#(xs))
823.82/297.03	       , 11: filterlow^#(n, nil()) -> c_11()
823.82/297.03	       , 12: filterlow^#(n, cons(x, xs)) ->
823.82/297.03	             c_12(if1^#(ge(n, x), n, x, xs))
823.82/297.03	       , 13: if1^#(true(), n, x, xs) -> c_19(filterlow^#(n, xs))
823.82/297.03	       , 14: if1^#(false(), n, x, xs) -> c_20(x, filterlow^#(n, xs))
823.82/297.03	       , 15: get^#(n, nil()) -> c_13()
823.82/297.03	       , 16: get^#(n, cons(x, nil())) -> c_14(x)
823.82/297.03	       , 17: get^#(0(), cons(x, cons(y, xs))) -> c_15(x)
823.82/297.03	       , 18: get^#(s(n), cons(x, cons(y, xs))) ->
823.82/297.03	             c_16(get^#(n, cons(y, xs)))
823.82/297.03	       , 19: filterhigh^#(n, nil()) -> c_17()
823.82/297.03	       , 20: filterhigh^#(n, cons(x, xs)) ->
823.82/297.03	             c_18(if2^#(ge(x, n), n, x, xs))
823.82/297.03	       , 21: if2^#(true(), n, x, xs) -> c_24(filterhigh^#(n, xs))
823.82/297.03	       , 22: if2^#(false(), n, x, xs) -> c_25(x, filterhigh^#(n, xs))
823.82/297.03	       , 23: ge^#(x, 0()) -> c_21()
823.82/297.03	       , 24: ge^#(0(), s(x)) -> c_22()
823.82/297.03	       , 25: ge^#(s(x), s(y)) -> c_23(ge^#(x, y)) }
823.82/297.03	   
823.82/297.03	   We are left with following problem, upon which TcT provides the
823.82/297.03	   certificate MAYBE.
823.82/297.03	   
823.82/297.03	   Strict DPs:
823.82/297.03	     { qsort^#(xs) -> c_1(qs^#(half(length(xs)), xs))
823.82/297.03	     , append^#(cons(x, xs), ys()) -> c_10(x, append^#(xs, ys()))
823.82/297.03	     , half^#(s(s(x))) -> c_6(half^#(x))
823.82/297.03	     , length^#(cons(x, xs)) -> c_8(length^#(xs))
823.82/297.03	     , filterlow^#(n, cons(x, xs)) -> c_12(if1^#(ge(n, x), n, x, xs))
823.82/297.03	     , if1^#(true(), n, x, xs) -> c_19(filterlow^#(n, xs))
823.82/297.03	     , if1^#(false(), n, x, xs) -> c_20(x, filterlow^#(n, xs))
823.82/297.03	     , get^#(n, cons(x, nil())) -> c_14(x)
823.82/297.03	     , get^#(0(), cons(x, cons(y, xs))) -> c_15(x)
823.82/297.03	     , get^#(s(n), cons(x, cons(y, xs))) -> c_16(get^#(n, cons(y, xs)))
823.82/297.03	     , filterhigh^#(n, cons(x, xs)) -> c_18(if2^#(ge(x, n), n, x, xs))
823.82/297.03	     , if2^#(true(), n, x, xs) -> c_24(filterhigh^#(n, xs))
823.82/297.03	     , if2^#(false(), n, x, xs) -> c_25(x, filterhigh^#(n, xs))
823.82/297.03	     , ge^#(s(x), s(y)) -> c_23(ge^#(x, y)) }
823.82/297.03	   Strict Trs:
823.82/297.03	     { qsort(xs) -> qs(half(length(xs)), xs)
823.82/297.03	     , qs(n, nil()) -> nil()
823.82/297.03	     , qs(n, cons(x, xs)) ->
823.82/297.03	       append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))),
823.82/297.03	              cons(get(n, cons(x, xs)),
823.82/297.03	                   qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
823.82/297.03	     , half(0()) -> 0()
823.82/297.03	     , half(s(0())) -> 0()
823.82/297.03	     , half(s(s(x))) -> s(half(x))
823.82/297.03	     , length(nil()) -> 0()
823.82/297.03	     , length(cons(x, xs)) -> s(length(xs))
823.82/297.03	     , append(nil(), ys()) -> ys()
823.82/297.03	     , append(cons(x, xs), ys()) -> cons(x, append(xs, ys()))
823.82/297.03	     , filterlow(n, nil()) -> nil()
823.82/297.03	     , filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
823.82/297.03	     , get(n, nil()) -> 0()
823.82/297.03	     , get(n, cons(x, nil())) -> x
823.82/297.03	     , get(0(), cons(x, cons(y, xs))) -> x
823.82/297.03	     , get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))
823.82/297.03	     , filterhigh(n, nil()) -> nil()
823.82/297.03	     , filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
823.82/297.03	     , if1(true(), n, x, xs) -> filterlow(n, xs)
823.82/297.03	     , if1(false(), n, x, xs) -> cons(x, filterlow(n, xs))
823.82/297.03	     , ge(x, 0()) -> true()
823.82/297.03	     , ge(0(), s(x)) -> false()
823.82/297.03	     , ge(s(x), s(y)) -> ge(x, y)
823.82/297.03	     , if2(true(), n, x, xs) -> filterhigh(n, xs)
823.82/297.03	     , if2(false(), n, x, xs) -> cons(x, filterhigh(n, xs)) }
823.82/297.03	   Weak DPs:
823.82/297.03	     { qs^#(n, nil()) -> c_2()
823.82/297.03	     , qs^#(n, cons(x, xs)) ->
823.82/297.03	       c_3(append^#(qs(half(n),
823.82/297.03	                       filterlow(get(n, cons(x, xs)), cons(x, xs))),
823.82/297.03	                    cons(get(n, cons(x, xs)),
823.82/297.03	                         qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs))))))
823.82/297.03	     , append^#(nil(), ys()) -> c_9()
823.82/297.03	     , half^#(0()) -> c_4()
823.82/297.03	     , half^#(s(0())) -> c_5()
823.82/297.03	     , length^#(nil()) -> c_7()
823.82/297.03	     , filterlow^#(n, nil()) -> c_11()
823.82/297.03	     , get^#(n, nil()) -> c_13()
823.82/297.03	     , filterhigh^#(n, nil()) -> c_17()
823.82/297.03	     , ge^#(x, 0()) -> c_21()
823.82/297.03	     , ge^#(0(), s(x)) -> c_22() }
823.82/297.03	   Obligation:
823.82/297.03	     runtime complexity
823.82/297.03	   Answer:
823.82/297.03	     MAYBE
823.82/297.03	   
823.82/297.03	   We estimate the number of application of {1} by applications of
823.82/297.03	   Pre({1}) = {2,7,8,9,13}. Here rules are labeled as follows:
823.82/297.03	   
823.82/297.03	     DPs:
823.82/297.03	       { 1: qsort^#(xs) -> c_1(qs^#(half(length(xs)), xs))
823.82/297.03	       , 2: append^#(cons(x, xs), ys()) -> c_10(x, append^#(xs, ys()))
823.82/297.03	       , 3: half^#(s(s(x))) -> c_6(half^#(x))
823.82/297.03	       , 4: length^#(cons(x, xs)) -> c_8(length^#(xs))
823.82/297.03	       , 5: filterlow^#(n, cons(x, xs)) -> c_12(if1^#(ge(n, x), n, x, xs))
823.82/297.03	       , 6: if1^#(true(), n, x, xs) -> c_19(filterlow^#(n, xs))
823.82/297.03	       , 7: if1^#(false(), n, x, xs) -> c_20(x, filterlow^#(n, xs))
823.82/297.03	       , 8: get^#(n, cons(x, nil())) -> c_14(x)
823.82/297.03	       , 9: get^#(0(), cons(x, cons(y, xs))) -> c_15(x)
823.82/297.03	       , 10: get^#(s(n), cons(x, cons(y, xs))) ->
823.82/297.03	             c_16(get^#(n, cons(y, xs)))
823.82/297.03	       , 11: filterhigh^#(n, cons(x, xs)) ->
823.82/297.03	             c_18(if2^#(ge(x, n), n, x, xs))
823.82/297.03	       , 12: if2^#(true(), n, x, xs) -> c_24(filterhigh^#(n, xs))
823.82/297.03	       , 13: if2^#(false(), n, x, xs) -> c_25(x, filterhigh^#(n, xs))
823.82/297.03	       , 14: ge^#(s(x), s(y)) -> c_23(ge^#(x, y))
823.82/297.03	       , 15: qs^#(n, nil()) -> c_2()
823.82/297.03	       , 16: qs^#(n, cons(x, xs)) ->
823.82/297.03	             c_3(append^#(qs(half(n),
823.82/297.03	                             filterlow(get(n, cons(x, xs)), cons(x, xs))),
823.82/297.03	                          cons(get(n, cons(x, xs)),
823.82/297.03	                               qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs))))))
823.82/297.03	       , 17: append^#(nil(), ys()) -> c_9()
823.82/297.03	       , 18: half^#(0()) -> c_4()
823.82/297.03	       , 19: half^#(s(0())) -> c_5()
823.82/297.03	       , 20: length^#(nil()) -> c_7()
823.82/297.03	       , 21: filterlow^#(n, nil()) -> c_11()
823.82/297.03	       , 22: get^#(n, nil()) -> c_13()
823.82/297.03	       , 23: filterhigh^#(n, nil()) -> c_17()
823.82/297.03	       , 24: ge^#(x, 0()) -> c_21()
823.82/297.03	       , 25: ge^#(0(), s(x)) -> c_22() }
823.82/297.03	   
823.82/297.03	   We are left with following problem, upon which TcT provides the
823.82/297.03	   certificate MAYBE.
823.82/297.03	   
823.82/297.03	   Strict DPs:
823.82/297.03	     { append^#(cons(x, xs), ys()) -> c_10(x, append^#(xs, ys()))
823.82/297.03	     , half^#(s(s(x))) -> c_6(half^#(x))
823.82/297.03	     , length^#(cons(x, xs)) -> c_8(length^#(xs))
823.82/297.03	     , filterlow^#(n, cons(x, xs)) -> c_12(if1^#(ge(n, x), n, x, xs))
823.82/297.03	     , if1^#(true(), n, x, xs) -> c_19(filterlow^#(n, xs))
823.82/297.03	     , if1^#(false(), n, x, xs) -> c_20(x, filterlow^#(n, xs))
823.82/297.03	     , get^#(n, cons(x, nil())) -> c_14(x)
823.82/297.03	     , get^#(0(), cons(x, cons(y, xs))) -> c_15(x)
823.82/297.03	     , get^#(s(n), cons(x, cons(y, xs))) -> c_16(get^#(n, cons(y, xs)))
823.82/297.03	     , filterhigh^#(n, cons(x, xs)) -> c_18(if2^#(ge(x, n), n, x, xs))
823.82/297.03	     , if2^#(true(), n, x, xs) -> c_24(filterhigh^#(n, xs))
823.82/297.03	     , if2^#(false(), n, x, xs) -> c_25(x, filterhigh^#(n, xs))
823.82/297.03	     , ge^#(s(x), s(y)) -> c_23(ge^#(x, y)) }
823.82/297.03	   Strict Trs:
823.82/297.03	     { qsort(xs) -> qs(half(length(xs)), xs)
823.82/297.03	     , qs(n, nil()) -> nil()
823.82/297.03	     , qs(n, cons(x, xs)) ->
823.82/297.03	       append(qs(half(n), filterlow(get(n, cons(x, xs)), cons(x, xs))),
823.82/297.03	              cons(get(n, cons(x, xs)),
823.82/297.03	                   qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs)))))
823.82/297.03	     , half(0()) -> 0()
823.82/297.03	     , half(s(0())) -> 0()
823.82/297.03	     , half(s(s(x))) -> s(half(x))
823.82/297.03	     , length(nil()) -> 0()
823.82/297.03	     , length(cons(x, xs)) -> s(length(xs))
823.82/297.03	     , append(nil(), ys()) -> ys()
823.82/297.03	     , append(cons(x, xs), ys()) -> cons(x, append(xs, ys()))
823.82/297.03	     , filterlow(n, nil()) -> nil()
823.82/297.03	     , filterlow(n, cons(x, xs)) -> if1(ge(n, x), n, x, xs)
823.82/297.03	     , get(n, nil()) -> 0()
823.82/297.03	     , get(n, cons(x, nil())) -> x
823.82/297.03	     , get(0(), cons(x, cons(y, xs))) -> x
823.82/297.03	     , get(s(n), cons(x, cons(y, xs))) -> get(n, cons(y, xs))
823.82/297.03	     , filterhigh(n, nil()) -> nil()
823.82/297.03	     , filterhigh(n, cons(x, xs)) -> if2(ge(x, n), n, x, xs)
823.82/297.03	     , if1(true(), n, x, xs) -> filterlow(n, xs)
823.82/297.03	     , if1(false(), n, x, xs) -> cons(x, filterlow(n, xs))
823.82/297.03	     , ge(x, 0()) -> true()
823.82/297.03	     , ge(0(), s(x)) -> false()
823.82/297.03	     , ge(s(x), s(y)) -> ge(x, y)
823.82/297.03	     , if2(true(), n, x, xs) -> filterhigh(n, xs)
823.82/297.03	     , if2(false(), n, x, xs) -> cons(x, filterhigh(n, xs)) }
823.82/297.03	   Weak DPs:
823.82/297.03	     { qsort^#(xs) -> c_1(qs^#(half(length(xs)), xs))
823.82/297.03	     , qs^#(n, nil()) -> c_2()
823.82/297.03	     , qs^#(n, cons(x, xs)) ->
823.82/297.03	       c_3(append^#(qs(half(n),
823.82/297.03	                       filterlow(get(n, cons(x, xs)), cons(x, xs))),
823.82/297.03	                    cons(get(n, cons(x, xs)),
823.82/297.03	                         qs(half(n), filterhigh(get(n, cons(x, xs)), cons(x, xs))))))
823.82/297.03	     , append^#(nil(), ys()) -> c_9()
823.82/297.03	     , half^#(0()) -> c_4()
823.82/297.03	     , half^#(s(0())) -> c_5()
823.82/297.03	     , length^#(nil()) -> c_7()
823.82/297.03	     , filterlow^#(n, nil()) -> c_11()
823.82/297.03	     , get^#(n, nil()) -> c_13()
823.82/297.03	     , filterhigh^#(n, nil()) -> c_17()
823.82/297.03	     , ge^#(x, 0()) -> c_21()
823.82/297.03	     , ge^#(0(), s(x)) -> c_22() }
823.82/297.03	   Obligation:
823.82/297.03	     runtime complexity
823.82/297.03	   Answer:
823.82/297.03	     MAYBE
823.82/297.03	   
823.82/297.03	   Empty strict component of the problem is NOT empty.
823.82/297.03	
823.82/297.03	
823.82/297.03	Arrrr..
824.04/297.24	EOF