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