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