MAYBE
759.45/297.10	MAYBE
759.45/297.10	
759.45/297.10	We are left with following problem, upon which TcT provides the
759.45/297.10	certificate MAYBE.
759.45/297.10	
759.45/297.10	Strict Trs:
759.45/297.10	  { merge#1(nil(), @l2) -> @l2
759.45/297.10	  , merge#1(::(@x, @xs), @l2) -> merge#2(@l2, @x, @xs)
759.45/297.10	  , msplit#3(tuple#2(@l1, @l2), @x1, @x2) ->
759.45/297.10	    tuple#2(::(@x1, @l1), ::(@x2, @l2))
759.45/297.10	  , mergesort#1(nil()) -> nil()
759.45/297.10	  , mergesort#1(::(@x1, @xs)) -> mergesort#2(@xs, @x1)
759.45/297.10	  , mergesort#2(nil(), @x1) -> ::(@x1, nil())
759.45/297.10	  , mergesort#2(::(@x2, @xs'), @x1) ->
759.45/297.10	    mergesort#3(msplit(::(@x1, ::(@x2, @xs'))))
759.45/297.10	  , mergesort#3(tuple#2(@l1, @l2)) ->
759.45/297.10	    merge(mergesort(@l1), mergesort(@l2))
759.45/297.10	  , merge#3(#true(), @x, @xs, @y, @ys) ->
759.45/297.10	    ::(@x, merge(@xs, ::(@y, @ys)))
759.45/297.10	  , merge#3(#false(), @x, @xs, @y, @ys) ->
759.45/297.10	    ::(@y, merge(::(@x, @xs), @ys))
759.45/297.10	  , merge(@l1, @l2) -> merge#1(@l1, @l2)
759.45/297.10	  , msplit#2(nil(), @x1) -> tuple#2(::(@x1, nil()), nil())
759.45/297.10	  , msplit#2(::(@x2, @xs'), @x1) -> msplit#3(msplit(@xs'), @x1, @x2)
759.45/297.10	  , merge#2(nil(), @x, @xs) -> ::(@x, @xs)
759.45/297.10	  , merge#2(::(@y, @ys), @x, @xs) ->
759.45/297.10	    merge#3(#less(@x, @y), @x, @xs, @y, @ys)
759.45/297.10	  , msplit(@l) -> msplit#1(@l)
759.45/297.10	  , msplit#1(nil()) -> tuple#2(nil(), nil())
759.45/297.10	  , msplit#1(::(@x1, @xs)) -> msplit#2(@xs, @x1)
759.45/297.10	  , mergesort(@l) -> mergesort#1(@l)
759.45/297.10	  , #less(@x, @y) -> #cklt(#compare(@x, @y)) }
759.45/297.10	Weak Trs:
759.45/297.10	  { #cklt(#EQ()) -> #false()
759.45/297.10	  , #cklt(#LT()) -> #true()
759.45/297.10	  , #cklt(#GT()) -> #false()
759.45/297.10	  , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
759.45/297.10	  , #compare(#pos(@x), #0()) -> #GT()
759.45/297.10	  , #compare(#pos(@x), #neg(@y)) -> #GT()
759.45/297.10	  , #compare(#0(), #pos(@y)) -> #LT()
759.45/297.10	  , #compare(#0(), #0()) -> #EQ()
759.45/297.10	  , #compare(#0(), #neg(@y)) -> #GT()
759.45/297.10	  , #compare(#0(), #s(@y)) -> #LT()
759.45/297.10	  , #compare(#neg(@x), #pos(@y)) -> #LT()
759.45/297.10	  , #compare(#neg(@x), #0()) -> #LT()
759.45/297.10	  , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
759.45/297.10	  , #compare(#s(@x), #0()) -> #GT()
759.45/297.10	  , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) }
759.45/297.10	Obligation:
759.45/297.10	  innermost runtime complexity
759.45/297.10	Answer:
759.45/297.10	  MAYBE
759.45/297.10	
759.45/297.10	None of the processors succeeded.
759.45/297.10	
759.45/297.10	Details of failed attempt(s):
759.45/297.10	-----------------------------
759.45/297.10	1) 'empty' failed due to the following reason:
759.45/297.10	   
759.45/297.10	   Empty strict component of the problem is NOT empty.
759.45/297.10	
759.45/297.10	2) 'Best' failed due to the following reason:
759.45/297.10	   
759.45/297.10	   None of the processors succeeded.
759.45/297.10	   
759.45/297.10	   Details of failed attempt(s):
759.45/297.10	   -----------------------------
759.45/297.10	   1) 'With Problem ... (timeout of 297 seconds)' failed due to the
759.45/297.10	      following reason:
759.45/297.10	      
759.45/297.10	      Computation stopped due to timeout after 297.0 seconds.
759.45/297.10	   
759.45/297.10	   2) 'Best' failed due to the following reason:
759.45/297.10	      
759.45/297.10	      None of the processors succeeded.
759.45/297.10	      
759.45/297.10	      Details of failed attempt(s):
759.45/297.10	      -----------------------------
759.45/297.10	      1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
759.45/297.10	         seconds)' failed due to the following reason:
759.45/297.10	         
759.45/297.10	         Computation stopped due to timeout after 148.0 seconds.
759.45/297.10	      
759.45/297.10	      2) 'Best' failed due to the following reason:
759.45/297.10	         
759.45/297.10	         None of the processors succeeded.
759.45/297.10	         
759.45/297.10	         Details of failed attempt(s):
759.45/297.10	         -----------------------------
759.45/297.10	         1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
759.45/297.10	            to the following reason:
759.45/297.10	            
759.45/297.10	            The input cannot be shown compatible
759.45/297.10	         
759.45/297.10	         2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
759.45/297.10	            following reason:
759.45/297.10	            
759.45/297.10	            The input cannot be shown compatible
759.45/297.10	         
759.45/297.10	      
759.45/297.10	      3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
759.45/297.10	         failed due to the following reason:
759.45/297.10	         
759.45/297.10	         None of the processors succeeded.
759.45/297.10	         
759.45/297.10	         Details of failed attempt(s):
759.45/297.10	         -----------------------------
759.45/297.10	         1) 'Bounds with minimal-enrichment and initial automaton 'match''
759.45/297.10	            failed due to the following reason:
759.45/297.10	            
759.45/297.10	            match-boundness of the problem could not be verified.
759.45/297.10	         
759.45/297.10	         2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
759.45/297.10	            failed due to the following reason:
759.45/297.10	            
759.45/297.10	            match-boundness of the problem could not be verified.
759.45/297.10	         
759.45/297.10	      
759.45/297.10	   
759.45/297.10	
759.45/297.10	
759.45/297.10	Arrrr..
759.45/297.13	EOF