MAYBE
21.35/6.96	MAYBE
21.35/6.96	
21.35/6.96	We are left with following problem, upon which TcT provides the
21.35/6.96	certificate MAYBE.
21.35/6.96	
21.35/6.96	Strict Trs:
21.35/6.96	  { f(s(x), x) -> f(s(x), round(s(x)))
21.35/6.96	  , round(s(s(x))) -> s(s(round(x)))
21.35/6.96	  , round(s(0())) -> s(0())
21.35/6.96	  , round(0()) -> s(0())
21.35/6.96	  , round(0()) -> 0() }
21.35/6.96	Obligation:
21.35/6.96	  derivational complexity
21.35/6.96	Answer:
21.35/6.96	  MAYBE
21.35/6.96	
21.35/6.96	None of the processors succeeded.
21.35/6.96	
21.35/6.96	Details of failed attempt(s):
21.35/6.96	-----------------------------
21.35/6.96	1) 'Inspecting Problem... (timeout of 297 seconds)' failed due to
21.35/6.96	   the following reason:
21.35/6.96	   
21.35/6.96	   The weightgap principle applies (using the following nonconstant
21.35/6.96	   growth matrix-interpretation)
21.35/6.96	   
21.35/6.96	   TcT has computed the following triangular matrix interpretation.
21.35/6.96	   Note that the diagonal of the component-wise maxima of
21.35/6.96	   interpretation-entries contains no more than 1 non-zero entries.
21.35/6.96	   
21.35/6.96	     [f](x1, x2) = [1] x1 + [1] x2 + [0]
21.35/6.96	                                        
21.35/6.96	         [s](x1) = [1] x1 + [0]         
21.35/6.96	                                        
21.35/6.96	     [round](x1) = [1] x1 + [1]         
21.35/6.96	                                        
21.35/6.96	             [0] = [0]                  
21.35/6.96	   
21.35/6.96	   The order satisfies the following ordering constraints:
21.35/6.96	   
21.35/6.96	         [f(s(x), x)] =  [2] x + [0]           
21.35/6.96	                      ?  [2] x + [1]           
21.35/6.96	                      =  [f(s(x), round(s(x)))]
21.35/6.96	                                               
21.35/6.96	     [round(s(s(x)))] =  [1] x + [1]           
21.35/6.96	                      >= [1] x + [1]           
21.35/6.96	                      =  [s(s(round(x)))]      
21.35/6.96	                                               
21.35/6.96	      [round(s(0()))] =  [1]                   
21.35/6.96	                      >  [0]                   
21.35/6.96	                      =  [s(0())]              
21.35/6.96	                                               
21.35/6.96	         [round(0())] =  [1]                   
21.35/6.96	                      >  [0]                   
21.35/6.96	                      =  [s(0())]              
21.35/6.96	                                               
21.35/6.96	         [round(0())] =  [1]                   
21.35/6.96	                      >  [0]                   
21.35/6.96	                      =  [0()]                 
21.35/6.96	                                               
21.35/6.96	   
21.35/6.96	   Further, it can be verified that all rules not oriented are covered by the weightgap condition.
21.35/6.96	   
21.35/6.96	   We are left with following problem, upon which TcT provides the
21.35/6.96	   certificate MAYBE.
21.35/6.96	   
21.35/6.96	   Strict Trs:
21.35/6.96	     { f(s(x), x) -> f(s(x), round(s(x)))
21.35/6.96	     , round(s(s(x))) -> s(s(round(x))) }
21.35/6.96	   Weak Trs:
21.35/6.96	     { round(s(0())) -> s(0())
21.35/6.96	     , round(0()) -> s(0())
21.35/6.96	     , round(0()) -> 0() }
21.35/6.96	   Obligation:
21.35/6.96	     derivational complexity
21.35/6.96	   Answer:
21.35/6.96	     MAYBE
21.35/6.96	   
21.35/6.96	   None of the processors succeeded.
21.35/6.96	   
21.35/6.96	   Details of failed attempt(s):
21.35/6.96	   -----------------------------
21.35/6.96	   1) 'empty' failed due to the following reason:
21.35/6.96	      
21.35/6.96	      Empty strict component of the problem is NOT empty.
21.35/6.96	   
21.35/6.96	   2) 'Fastest' failed due to the following reason:
21.35/6.96	      
21.35/6.96	      None of the processors succeeded.
21.35/6.96	      
21.35/6.96	      Details of failed attempt(s):
21.35/6.96	      -----------------------------
21.35/6.96	      1) 'Fastest' failed due to the following reason:
21.35/6.96	         
21.35/6.96	         None of the processors succeeded.
21.35/6.96	         
21.35/6.96	         Details of failed attempt(s):
21.35/6.96	         -----------------------------
21.35/6.96	         1) 'matrix interpretation of dimension 6' failed due to the
21.35/6.96	            following reason:
21.35/6.96	            
21.35/6.96	            The input cannot be shown compatible
21.35/6.96	         
21.35/6.96	         2) 'matrix interpretation of dimension 5' failed due to the
21.35/6.96	            following reason:
21.35/6.96	            
21.35/6.96	            The input cannot be shown compatible
21.35/6.96	         
21.35/6.96	         3) 'matrix interpretation of dimension 4' failed due to the
21.35/6.96	            following reason:
21.35/6.96	            
21.35/6.96	            The input cannot be shown compatible
21.35/6.96	         
21.35/6.96	         4) 'matrix interpretation of dimension 3' failed due to the
21.35/6.96	            following reason:
21.35/6.96	            
21.35/6.96	            The input cannot be shown compatible
21.35/6.96	         
21.35/6.96	         5) 'matrix interpretation of dimension 2' failed due to the
21.35/6.96	            following reason:
21.35/6.96	            
21.35/6.96	            The input cannot be shown compatible
21.35/6.96	         
21.35/6.96	         6) 'matrix interpretation of dimension 1' failed due to the
21.35/6.96	            following reason:
21.35/6.96	            
21.35/6.96	            The input cannot be shown compatible
21.35/6.96	         
21.35/6.96	      
21.35/6.96	      2) 'iteProgress' failed due to the following reason:
21.35/6.96	         
21.35/6.96	         Fail
21.35/6.96	      
21.35/6.96	      3) 'bsearch-matrix' failed due to the following reason:
21.35/6.96	         
21.35/6.96	         The input cannot be shown compatible
21.35/6.96	      
21.35/6.96	      4) 'Fastest (timeout of 30 seconds)' failed due to the following
21.35/6.96	         reason:
21.35/6.96	         
21.35/6.96	         None of the processors succeeded.
21.35/6.96	         
21.35/6.96	         Details of failed attempt(s):
21.35/6.96	         -----------------------------
21.35/6.96	         1) 'Bounds with minimal-enrichment and initial automaton 'match''
21.35/6.96	            failed due to the following reason:
21.35/6.96	            
21.35/6.96	            match-boundness of the problem could not be verified.
21.35/6.96	         
21.35/6.96	         2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
21.35/6.96	            failed due to the following reason:
21.35/6.96	            
21.35/6.96	            match-boundness of the problem could not be verified.
21.35/6.96	         
21.35/6.96	      
21.35/6.96	   
21.35/6.96	
21.35/6.96	2) 'iteProgress (timeout of 297 seconds)' failed due to the
21.35/6.96	   following reason:
21.35/6.96	   
21.35/6.96	   Fail
21.35/6.96	
21.35/6.96	3) 'bsearch-matrix (timeout of 297 seconds)' failed due to the
21.35/6.96	   following reason:
21.35/6.96	   
21.35/6.96	   The input cannot be shown compatible
21.35/6.96	
21.35/6.96	4) 'Fastest (timeout of 60 seconds)' failed due to the following
21.35/6.96	   reason:
21.35/6.96	   
21.35/6.96	   None of the processors succeeded.
21.35/6.96	   
21.35/6.96	   Details of failed attempt(s):
21.35/6.96	   -----------------------------
21.35/6.96	   1) 'Bounds with minimal-enrichment and initial automaton 'match''
21.35/6.96	      failed due to the following reason:
21.35/6.96	      
21.35/6.96	      match-boundness of the problem could not be verified.
21.35/6.96	   
21.35/6.96	   2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
21.35/6.96	      failed due to the following reason:
21.35/6.96	      
21.35/6.96	      match-boundness of the problem could not be verified.
21.35/6.96	   
21.35/6.96	
21.35/6.96	
21.35/6.96	Arrrr..
21.35/6.97	EOF