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