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