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