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