MAYBE
715.12/297.03	MAYBE
715.12/297.03	
715.12/297.03	We are left with following problem, upon which TcT provides the
715.12/297.03	certificate MAYBE.
715.12/297.03	
715.12/297.03	Strict Trs:
715.12/297.03	  { plus(x, y) -> ifPlus(isZero(x), x, inc(y))
715.12/297.03	  , ifPlus(true(), x, y) -> p(y)
715.12/297.03	  , ifPlus(false(), x, y) -> plus(p(x), y)
715.12/297.03	  , isZero(0()) -> true()
715.12/297.03	  , isZero(s(0())) -> false()
715.12/297.03	  , isZero(s(s(x))) -> isZero(s(x))
715.12/297.03	  , inc(x) -> s(x)
715.12/297.03	  , inc(0()) -> s(0())
715.12/297.03	  , inc(s(x)) -> s(inc(x))
715.12/297.03	  , p(0()) -> 0()
715.12/297.03	  , p(s(x)) -> x
715.12/297.03	  , p(s(s(x))) -> s(p(s(x)))
715.12/297.03	  , times(x, y) -> timesIter(0(), x, y, 0())
715.12/297.03	  , timesIter(i, x, y, z) -> ifTimes(ge(i, x), i, x, y, z)
715.12/297.03	  , ifTimes(true(), i, x, y, z) -> z
715.12/297.03	  , ifTimes(false(), i, x, y, z) ->
715.12/297.03	    timesIter(inc(i), x, y, plus(z, y))
715.12/297.03	  , ge(x, 0()) -> true()
715.12/297.03	  , ge(0(), s(y)) -> false()
715.12/297.03	  , ge(s(x), s(y)) -> ge(x, y)
715.12/297.03	  , f0(x, y, z) -> d()
715.12/297.03	  , f0(0(), y, x) -> f1(x, y, x)
715.12/297.03	  , f1(x, y, z) -> f2(x, y, z)
715.12/297.03	  , f1(x, y, z) -> c()
715.12/297.03	  , f2(x, 1(), z) -> f0(x, z, z) }
715.12/297.03	Obligation:
715.12/297.03	  innermost runtime complexity
715.12/297.03	Answer:
715.12/297.03	  MAYBE
715.12/297.03	
715.12/297.03	None of the processors succeeded.
715.12/297.03	
715.12/297.03	Details of failed attempt(s):
715.12/297.03	-----------------------------
715.12/297.03	1) 'empty' failed due to the following reason:
715.12/297.03	   
715.12/297.03	   Empty strict component of the problem is NOT empty.
715.12/297.03	
715.12/297.03	2) 'Best' failed due to the following reason:
715.12/297.03	   
715.12/297.03	   None of the processors succeeded.
715.12/297.03	   
715.12/297.03	   Details of failed attempt(s):
715.12/297.03	   -----------------------------
715.12/297.03	   1) 'With Problem ... (timeout of 297 seconds)' failed due to the
715.12/297.03	      following reason:
715.12/297.03	      
715.12/297.03	      Computation stopped due to timeout after 297.0 seconds.
715.12/297.03	   
715.12/297.03	   2) 'Best' failed due to the following reason:
715.12/297.03	      
715.12/297.03	      None of the processors succeeded.
715.12/297.03	      
715.12/297.03	      Details of failed attempt(s):
715.12/297.03	      -----------------------------
715.12/297.03	      1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
715.12/297.03	         seconds)' failed due to the following reason:
715.12/297.03	         
715.12/297.03	         None of the processors succeeded.
715.12/297.03	         
715.12/297.03	         Details of failed attempt(s):
715.12/297.03	         -----------------------------
715.12/297.03	         1) 'empty' failed due to the following reason:
715.12/297.03	            
715.12/297.03	            Empty strict component of the problem is NOT empty.
715.12/297.03	         
715.12/297.03	         2) 'With Problem ...' failed due to the following reason:
715.12/297.03	            
715.12/297.03	            None of the processors succeeded.
715.12/297.03	            
715.12/297.03	            Details of failed attempt(s):
715.12/297.03	            -----------------------------
715.12/297.03	            1) 'empty' failed due to the following reason:
715.12/297.03	               
715.12/297.03	               Empty strict component of the problem is NOT empty.
715.12/297.03	            
715.12/297.03	            2) 'Fastest' failed due to the following reason:
715.12/297.03	               
715.12/297.03	               None of the processors succeeded.
715.12/297.03	               
715.12/297.03	               Details of failed attempt(s):
715.12/297.03	               -----------------------------
715.12/297.03	               1) 'With Problem ...' failed due to the following reason:
715.12/297.03	                  
715.12/297.03	                  None of the processors succeeded.
715.12/297.03	                  
715.12/297.03	                  Details of failed attempt(s):
715.12/297.03	                  -----------------------------
715.12/297.03	                  1) 'empty' failed due to the following reason:
715.12/297.03	                     
715.12/297.03	                     Empty strict component of the problem is NOT empty.
715.12/297.03	                  
715.12/297.03	                  2) 'With Problem ...' failed due to the following reason:
715.12/297.03	                     
715.12/297.03	                     Empty strict component of the problem is NOT empty.
715.12/297.03	                  
715.12/297.03	               
715.12/297.03	               2) 'With Problem ...' failed due to the following reason:
715.12/297.03	                  
715.12/297.03	                  None of the processors succeeded.
715.12/297.03	                  
715.12/297.03	                  Details of failed attempt(s):
715.12/297.03	                  -----------------------------
715.12/297.03	                  1) 'empty' failed due to the following reason:
715.12/297.03	                     
715.12/297.03	                     Empty strict component of the problem is NOT empty.
715.12/297.03	                  
715.12/297.03	                  2) 'With Problem ...' failed due to the following reason:
715.12/297.03	                     
715.12/297.03	                     None of the processors succeeded.
715.12/297.03	                     
715.12/297.03	                     Details of failed attempt(s):
715.12/297.03	                     -----------------------------
715.12/297.03	                     1) 'empty' failed due to the following reason:
715.12/297.03	                        
715.12/297.03	                        Empty strict component of the problem is NOT empty.
715.12/297.03	                     
715.12/297.03	                     2) 'With Problem ...' failed due to the following reason:
715.12/297.03	                        
715.12/297.03	                        None of the processors succeeded.
715.12/297.03	                        
715.12/297.03	                        Details of failed attempt(s):
715.12/297.03	                        -----------------------------
715.12/297.03	                        1) 'empty' failed due to the following reason:
715.12/297.03	                           
715.12/297.03	                           Empty strict component of the problem is NOT empty.
715.12/297.03	                        
715.12/297.03	                        2) 'With Problem ...' failed due to the following reason:
715.12/297.03	                           
715.12/297.03	                           Empty strict component of the problem is NOT empty.
715.12/297.03	                        
715.12/297.03	                     
715.12/297.03	                  
715.12/297.03	               
715.12/297.03	            
715.12/297.03	         
715.12/297.03	      
715.12/297.03	      2) 'Best' failed due to the following reason:
715.12/297.03	         
715.12/297.03	         None of the processors succeeded.
715.12/297.03	         
715.12/297.03	         Details of failed attempt(s):
715.12/297.03	         -----------------------------
715.12/297.03	         1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
715.12/297.03	            following reason:
715.12/297.03	            
715.12/297.03	            The input cannot be shown compatible
715.12/297.03	         
715.12/297.03	         2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
715.12/297.03	            to the following reason:
715.12/297.03	            
715.12/297.03	            The input cannot be shown compatible
715.12/297.03	         
715.12/297.03	      
715.12/297.03	      3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
715.12/297.03	         failed due to the following reason:
715.12/297.03	         
715.12/297.03	         None of the processors succeeded.
715.12/297.03	         
715.12/297.03	         Details of failed attempt(s):
715.12/297.03	         -----------------------------
715.12/297.03	         1) 'Bounds with minimal-enrichment and initial automaton 'match''
715.12/297.03	            failed due to the following reason:
715.12/297.03	            
715.12/297.03	            match-boundness of the problem could not be verified.
715.12/297.03	         
715.12/297.03	         2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
715.12/297.03	            failed due to the following reason:
715.12/297.03	            
715.12/297.03	            match-boundness of the problem could not be verified.
715.12/297.03	         
715.12/297.03	      
715.12/297.03	   
715.12/297.03	
715.12/297.03	
715.12/297.03	Arrrr..
715.23/297.17	EOF