MAYBE
1111.08/297.03	MAYBE
1111.08/297.03	
1111.08/297.03	We are left with following problem, upon which TcT provides the
1111.08/297.03	certificate MAYBE.
1111.08/297.03	
1111.08/297.03	Strict Trs:
1111.08/297.03	  { msort(nil()) -> nil()
1111.08/297.03	  , msort(.(x, y)) -> .(min(x, y), msort(del(min(x, y), .(x, y))))
1111.08/297.03	  , min(x, nil()) -> x
1111.08/297.03	  , min(x, .(y, z)) -> if(<=(x, y), min(x, z), min(y, z))
1111.08/297.03	  , del(x, nil()) -> nil()
1111.08/297.03	  , del(x, .(y, z)) -> if(=(x, y), z, .(y, del(x, z))) }
1111.08/297.03	Obligation:
1111.08/297.03	  runtime complexity
1111.08/297.03	Answer:
1111.08/297.03	  MAYBE
1111.08/297.03	
1111.08/297.03	None of the processors succeeded.
1111.08/297.03	
1111.08/297.03	Details of failed attempt(s):
1111.08/297.03	-----------------------------
1111.08/297.03	1) 'With Problem ... (timeout of 297 seconds)' failed due to the
1111.08/297.03	   following reason:
1111.08/297.03	   
1111.08/297.03	   Computation stopped due to timeout after 297.0 seconds.
1111.08/297.03	
1111.08/297.03	2) 'Best' failed due to the following reason:
1111.08/297.03	   
1111.08/297.03	   None of the processors succeeded.
1111.08/297.03	   
1111.08/297.03	   Details of failed attempt(s):
1111.08/297.03	   -----------------------------
1111.08/297.03	   1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
1111.08/297.03	      seconds)' failed due to the following reason:
1111.08/297.03	      
1111.08/297.03	      Computation stopped due to timeout after 148.0 seconds.
1111.08/297.03	   
1111.08/297.03	   2) 'Best' failed due to the following reason:
1111.08/297.03	      
1111.08/297.03	      None of the processors succeeded.
1111.08/297.03	      
1111.08/297.03	      Details of failed attempt(s):
1111.08/297.03	      -----------------------------
1111.08/297.03	      1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
1111.08/297.03	         to the following reason:
1111.08/297.03	         
1111.08/297.03	         The processor is inapplicable, reason:
1111.08/297.03	           Processor only applicable for innermost runtime complexity analysis
1111.08/297.03	      
1111.08/297.03	      2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
1111.08/297.03	         following reason:
1111.08/297.03	         
1111.08/297.03	         The processor is inapplicable, reason:
1111.08/297.03	           Processor only applicable for innermost runtime complexity analysis
1111.08/297.03	      
1111.08/297.03	   
1111.08/297.03	   3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
1111.08/297.03	      failed due to the following reason:
1111.08/297.03	      
1111.08/297.03	      None of the processors succeeded.
1111.08/297.03	      
1111.08/297.03	      Details of failed attempt(s):
1111.08/297.03	      -----------------------------
1111.08/297.03	      1) 'Bounds with minimal-enrichment and initial automaton 'match''
1111.08/297.03	         failed due to the following reason:
1111.08/297.03	         
1111.08/297.03	         match-boundness of the problem could not be verified.
1111.08/297.03	      
1111.08/297.03	      2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
1111.08/297.03	         failed due to the following reason:
1111.08/297.03	         
1111.08/297.03	         match-boundness of the problem could not be verified.
1111.08/297.03	      
1111.08/297.03	   
1111.08/297.03	
1111.08/297.03	3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to
1111.08/297.03	   the following reason:
1111.08/297.03	   
1111.08/297.03	   We add the following weak dependency pairs:
1111.08/297.03	   
1111.08/297.03	   Strict DPs:
1111.08/297.03	     { msort^#(nil()) -> c_1()
1111.08/297.03	     , msort^#(.(x, y)) ->
1111.08/297.03	       c_2(min^#(x, y), msort^#(del(min(x, y), .(x, y))))
1111.08/297.03	     , min^#(x, nil()) -> c_3(x)
1111.08/297.03	     , min^#(x, .(y, z)) -> c_4(x, y, min^#(x, z), min^#(y, z))
1111.08/297.03	     , del^#(x, nil()) -> c_5()
1111.08/297.03	     , del^#(x, .(y, z)) -> c_6(x, y, z, y, del^#(x, z)) }
1111.08/297.03	   
1111.08/297.03	   and mark the set of starting terms.
1111.08/297.03	   
1111.08/297.03	   We are left with following problem, upon which TcT provides the
1111.08/297.03	   certificate MAYBE.
1111.08/297.03	   
1111.08/297.03	   Strict DPs:
1111.08/297.03	     { msort^#(nil()) -> c_1()
1111.08/297.03	     , msort^#(.(x, y)) ->
1111.08/297.03	       c_2(min^#(x, y), msort^#(del(min(x, y), .(x, y))))
1111.08/297.03	     , min^#(x, nil()) -> c_3(x)
1111.08/297.03	     , min^#(x, .(y, z)) -> c_4(x, y, min^#(x, z), min^#(y, z))
1111.08/297.03	     , del^#(x, nil()) -> c_5()
1111.08/297.03	     , del^#(x, .(y, z)) -> c_6(x, y, z, y, del^#(x, z)) }
1111.08/297.03	   Strict Trs:
1111.08/297.03	     { msort(nil()) -> nil()
1111.08/297.03	     , msort(.(x, y)) -> .(min(x, y), msort(del(min(x, y), .(x, y))))
1111.08/297.03	     , min(x, nil()) -> x
1111.08/297.03	     , min(x, .(y, z)) -> if(<=(x, y), min(x, z), min(y, z))
1111.08/297.03	     , del(x, nil()) -> nil()
1111.08/297.03	     , del(x, .(y, z)) -> if(=(x, y), z, .(y, del(x, z))) }
1111.08/297.03	   Obligation:
1111.08/297.03	     runtime complexity
1111.08/297.03	   Answer:
1111.08/297.03	     MAYBE
1111.08/297.03	   
1111.08/297.03	   We estimate the number of application of {1,5} by applications of
1111.08/297.03	   Pre({1,5}) = {2,3,4,6}. Here rules are labeled as follows:
1111.08/297.03	   
1111.08/297.03	     DPs:
1111.08/297.03	       { 1: msort^#(nil()) -> c_1()
1111.08/297.03	       , 2: msort^#(.(x, y)) ->
1111.08/297.03	            c_2(min^#(x, y), msort^#(del(min(x, y), .(x, y))))
1111.08/297.03	       , 3: min^#(x, nil()) -> c_3(x)
1111.08/297.03	       , 4: min^#(x, .(y, z)) -> c_4(x, y, min^#(x, z), min^#(y, z))
1111.08/297.03	       , 5: del^#(x, nil()) -> c_5()
1111.08/297.03	       , 6: del^#(x, .(y, z)) -> c_6(x, y, z, y, del^#(x, z)) }
1111.08/297.03	   
1111.08/297.03	   We are left with following problem, upon which TcT provides the
1111.08/297.03	   certificate MAYBE.
1111.08/297.03	   
1111.08/297.03	   Strict DPs:
1111.08/297.03	     { msort^#(.(x, y)) ->
1111.08/297.03	       c_2(min^#(x, y), msort^#(del(min(x, y), .(x, y))))
1111.08/297.03	     , min^#(x, nil()) -> c_3(x)
1111.08/297.03	     , min^#(x, .(y, z)) -> c_4(x, y, min^#(x, z), min^#(y, z))
1111.08/297.03	     , del^#(x, .(y, z)) -> c_6(x, y, z, y, del^#(x, z)) }
1111.08/297.03	   Strict Trs:
1111.08/297.03	     { msort(nil()) -> nil()
1111.08/297.03	     , msort(.(x, y)) -> .(min(x, y), msort(del(min(x, y), .(x, y))))
1111.08/297.03	     , min(x, nil()) -> x
1111.08/297.03	     , min(x, .(y, z)) -> if(<=(x, y), min(x, z), min(y, z))
1111.08/297.03	     , del(x, nil()) -> nil()
1111.08/297.03	     , del(x, .(y, z)) -> if(=(x, y), z, .(y, del(x, z))) }
1111.08/297.03	   Weak DPs:
1111.08/297.03	     { msort^#(nil()) -> c_1()
1111.08/297.03	     , del^#(x, nil()) -> c_5() }
1111.08/297.03	   Obligation:
1111.08/297.03	     runtime complexity
1111.08/297.03	   Answer:
1111.08/297.03	     MAYBE
1111.08/297.03	   
1111.08/297.03	   Empty strict component of the problem is NOT empty.
1111.08/297.03	
1111.08/297.03	
1111.08/297.03	Arrrr..
1112.05/297.95	EOF