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