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