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