MAYBE
992.91/297.02	MAYBE
992.91/297.02	
992.91/297.02	We are left with following problem, upon which TcT provides the
992.91/297.02	certificate MAYBE.
992.91/297.02	
992.91/297.02	Strict Trs:
992.91/297.02	  { ack(0(), y) -> s(y)
992.91/297.02	  , ack(s(x), 0()) -> ack(x, s(0()))
992.91/297.02	  , ack(s(x), s(y)) -> ack(x, ack(s(x), y)) }
992.91/297.02	Obligation:
992.91/297.02	  runtime complexity
992.91/297.02	Answer:
992.91/297.02	  MAYBE
992.91/297.02	
992.91/297.02	None of the processors succeeded.
992.91/297.02	
992.91/297.02	Details of failed attempt(s):
992.91/297.02	-----------------------------
992.91/297.02	1) 'With Problem ... (timeout of 297 seconds)' failed due to the
992.91/297.02	   following reason:
992.91/297.02	   
992.91/297.02	   Computation stopped due to timeout after 297.0 seconds.
992.91/297.02	
992.91/297.02	2) 'Best' failed due to the following reason:
992.91/297.02	   
992.91/297.02	   None of the processors succeeded.
992.91/297.02	   
992.91/297.02	   Details of failed attempt(s):
992.91/297.02	   -----------------------------
992.91/297.02	   1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
992.91/297.02	      seconds)' failed due to the following reason:
992.91/297.02	      
992.91/297.02	      The weightgap principle applies (using the following nonconstant
992.91/297.02	      growth matrix-interpretation)
992.91/297.02	      
992.91/297.02	      The following argument positions are usable:
992.91/297.02	        Uargs(ack) = {2}, Uargs(s) = {1}
992.91/297.02	      
992.91/297.02	      TcT has computed the following matrix interpretation satisfying
992.91/297.02	      not(EDA) and not(IDA(1)).
992.91/297.02	      
992.91/297.02	        [ack](x1, x2) = [1] x2 + [0]
992.91/297.02	                                    
992.91/297.02	                  [0] = [4]         
992.91/297.02	                                    
992.91/297.02	              [s](x1) = [1] x1 + [4]
992.91/297.02	      
992.91/297.02	      The order satisfies the following ordering constraints:
992.91/297.02	      
992.91/297.02	            [ack(0(), y)] = [1] y + [0]           
992.91/297.02	                          ? [1] y + [4]           
992.91/297.02	                          = [s(y)]                
992.91/297.02	                                                  
992.91/297.02	         [ack(s(x), 0())] = [4]                   
992.91/297.02	                          ? [8]                   
992.91/297.02	                          = [ack(x, s(0()))]      
992.91/297.02	                                                  
992.91/297.02	        [ack(s(x), s(y))] = [1] y + [4]           
992.91/297.02	                          > [1] y + [0]           
992.91/297.02	                          = [ack(x, ack(s(x), y))]
992.91/297.02	                                                  
992.91/297.02	      
992.91/297.02	      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
992.91/297.02	      
992.91/297.02	      We are left with following problem, upon which TcT provides the
992.91/297.02	      certificate MAYBE.
992.91/297.02	      
992.91/297.02	      Strict Trs:
992.91/297.02	        { ack(0(), y) -> s(y)
992.91/297.02	        , ack(s(x), 0()) -> ack(x, s(0())) }
992.91/297.02	      Weak Trs: { ack(s(x), s(y)) -> ack(x, ack(s(x), y)) }
992.91/297.02	      Obligation:
992.91/297.02	        runtime complexity
992.91/297.02	      Answer:
992.91/297.02	        MAYBE
992.91/297.02	      
992.91/297.02	      None of the processors succeeded.
992.91/297.02	      
992.91/297.02	      Details of failed attempt(s):
992.91/297.02	      -----------------------------
992.91/297.02	      1) 'empty' failed due to the following reason:
992.91/297.02	         
992.91/297.02	         Empty strict component of the problem is NOT empty.
992.91/297.02	      
992.91/297.02	      2) 'With Problem ...' failed due to the following reason:
992.91/297.02	         
992.91/297.02	         None of the processors succeeded.
992.91/297.02	         
992.91/297.02	         Details of failed attempt(s):
992.91/297.02	         -----------------------------
992.91/297.02	         1) 'empty' failed due to the following reason:
992.91/297.02	            
992.91/297.02	            Empty strict component of the problem is NOT empty.
992.91/297.02	         
992.91/297.02	         2) 'Fastest' failed due to the following reason:
992.91/297.02	            
992.91/297.02	            None of the processors succeeded.
992.91/297.02	            
992.91/297.02	            Details of failed attempt(s):
992.91/297.02	            -----------------------------
992.91/297.02	            1) 'With Problem ...' failed due to the following reason:
992.91/297.02	               
992.91/297.02	               None of the processors succeeded.
992.91/297.02	               
992.91/297.02	               Details of failed attempt(s):
992.91/297.02	               -----------------------------
992.91/297.02	               1) 'empty' failed due to the following reason:
992.91/297.02	                  
992.91/297.02	                  Empty strict component of the problem is NOT empty.
992.91/297.02	               
992.91/297.02	               2) 'With Problem ...' failed due to the following reason:
992.91/297.02	                  
992.91/297.02	                  Empty strict component of the problem is NOT empty.
992.91/297.02	               
992.91/297.02	            
992.91/297.02	            2) 'With Problem ...' failed due to the following reason:
992.91/297.02	               
992.91/297.02	               None of the processors succeeded.
992.91/297.02	               
992.91/297.02	               Details of failed attempt(s):
992.91/297.02	               -----------------------------
992.91/297.02	               1) 'empty' failed due to the following reason:
992.91/297.02	                  
992.91/297.02	                  Empty strict component of the problem is NOT empty.
992.91/297.02	               
992.91/297.02	               2) 'With Problem ...' failed due to the following reason:
992.91/297.02	                  
992.91/297.02	                  None of the processors succeeded.
992.91/297.02	                  
992.91/297.02	                  Details of failed attempt(s):
992.91/297.02	                  -----------------------------
992.91/297.02	                  1) 'empty' failed due to the following reason:
992.91/297.02	                     
992.91/297.02	                     Empty strict component of the problem is NOT empty.
992.91/297.02	                  
992.91/297.02	                  2) 'With Problem ...' failed due to the following reason:
992.91/297.02	                     
992.91/297.02	                     None of the processors succeeded.
992.91/297.02	                     
992.91/297.02	                     Details of failed attempt(s):
992.91/297.02	                     -----------------------------
992.91/297.02	                     1) 'empty' failed due to the following reason:
992.91/297.02	                        
992.91/297.02	                        Empty strict component of the problem is NOT empty.
992.91/297.02	                     
992.91/297.02	                     2) 'With Problem ...' failed due to the following reason:
992.91/297.02	                        
992.91/297.02	                        Empty strict component of the problem is NOT empty.
992.91/297.02	                     
992.91/297.02	                  
992.91/297.02	               
992.91/297.02	            
992.91/297.02	         
992.91/297.02	      
992.91/297.02	   
992.91/297.02	   2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
992.91/297.02	      failed due to the following reason:
992.91/297.02	      
992.91/297.02	      None of the processors succeeded.
992.91/297.02	      
992.91/297.02	      Details of failed attempt(s):
992.91/297.02	      -----------------------------
992.91/297.02	      1) 'Bounds with minimal-enrichment and initial automaton 'match''
992.91/297.02	         failed due to the following reason:
992.91/297.02	         
992.91/297.02	         match-boundness of the problem could not be verified.
992.91/297.02	      
992.91/297.02	      2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
992.91/297.02	         failed due to the following reason:
992.91/297.02	         
992.91/297.02	         match-boundness of the problem could not be verified.
992.91/297.02	      
992.91/297.02	   
992.91/297.02	   3) 'Best' failed due to the following reason:
992.91/297.02	      
992.91/297.02	      None of the processors succeeded.
992.91/297.02	      
992.91/297.02	      Details of failed attempt(s):
992.91/297.02	      -----------------------------
992.91/297.02	      1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
992.91/297.02	         following reason:
992.91/297.02	         
992.91/297.02	         The processor is inapplicable, reason:
992.91/297.02	           Processor only applicable for innermost runtime complexity analysis
992.91/297.02	      
992.91/297.02	      2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
992.91/297.02	         to the following reason:
992.91/297.02	         
992.91/297.02	         The processor is inapplicable, reason:
992.91/297.02	           Processor only applicable for innermost runtime complexity analysis
992.91/297.02	      
992.91/297.02	   
992.91/297.02	
992.91/297.02	3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to
992.91/297.02	   the following reason:
992.91/297.02	   
992.91/297.02	   We add the following weak dependency pairs:
992.91/297.02	   
992.91/297.02	   Strict DPs:
992.91/297.02	     { ack^#(0(), y) -> c_1(y)
992.91/297.02	     , ack^#(s(x), 0()) -> c_2(ack^#(x, s(0())))
992.91/297.02	     , ack^#(s(x), s(y)) -> c_3(ack^#(x, ack(s(x), y))) }
992.91/297.02	   
992.91/297.02	   and mark the set of starting terms.
992.91/297.02	   
992.91/297.02	   We are left with following problem, upon which TcT provides the
992.91/297.02	   certificate MAYBE.
992.91/297.02	   
992.91/297.02	   Strict DPs:
992.91/297.02	     { ack^#(0(), y) -> c_1(y)
992.91/297.02	     , ack^#(s(x), 0()) -> c_2(ack^#(x, s(0())))
992.91/297.02	     , ack^#(s(x), s(y)) -> c_3(ack^#(x, ack(s(x), y))) }
992.91/297.02	   Strict Trs:
992.91/297.02	     { ack(0(), y) -> s(y)
992.91/297.02	     , ack(s(x), 0()) -> ack(x, s(0()))
992.91/297.02	     , ack(s(x), s(y)) -> ack(x, ack(s(x), y)) }
992.91/297.02	   Obligation:
992.91/297.02	     runtime complexity
992.91/297.02	   Answer:
992.91/297.02	     MAYBE
992.91/297.02	   
992.91/297.02	   Empty strict component of the problem is NOT empty.
992.91/297.02	
992.91/297.02	
992.91/297.02	Arrrr..
993.95/298.03	EOF