MAYBE
228.20/65.39	MAYBE
228.20/65.39	
228.20/65.39	We are left with following problem, upon which TcT provides the
228.20/65.39	certificate MAYBE.
228.20/65.39	
228.20/65.39	Strict Trs:
228.20/65.39	  { 1(1(x1)) -> 0(0(0(0(x1))))
228.20/65.39	  , 1(0(x1)) -> 0(0(0(1(x1))))
228.20/65.39	  , 0(1(x1)) -> 1(x1)
228.20/65.39	  , 0(0(x1)) -> 0(x1) }
228.20/65.39	Obligation:
228.20/65.39	  derivational complexity
228.20/65.39	Answer:
228.20/65.39	  MAYBE
228.20/65.39	
228.20/65.39	None of the processors succeeded.
228.20/65.39	
228.20/65.39	Details of failed attempt(s):
228.20/65.39	-----------------------------
228.20/65.39	1) 'Inspecting Problem... (timeout of 297 seconds)' failed due to
228.20/65.39	   the following reason:
228.20/65.39	   
228.20/65.39	   We use the processor 'matrix interpretation of dimension 1' to
228.20/65.39	   orient following rules strictly.
228.20/65.39	   
228.20/65.39	   Trs: { 1(1(x1)) -> 0(0(0(0(x1)))) }
228.20/65.39	   
228.20/65.39	   The induced complexity on above rules (modulo remaining rules) is
228.20/65.39	   YES(?,O(n^1)) . These rules are moved into the corresponding weak
228.20/65.39	   component(s).
228.20/65.39	   
228.20/65.39	   Sub-proof:
228.20/65.39	   ----------
228.20/65.39	     TcT has computed the following triangular matrix interpretation.
228.20/65.39	     
228.20/65.39	       [1](x1) = [1] x1 + [1]
228.20/65.39	                             
228.20/65.39	       [0](x1) = [1] x1 + [0]
228.20/65.39	     
228.20/65.39	     The order satisfies the following ordering constraints:
228.20/65.39	     
228.20/65.39	       [1(1(x1))] =  [1] x1 + [2]    
228.20/65.39	                  >  [1] x1 + [0]    
228.20/65.39	                  =  [0(0(0(0(x1))))]
228.20/65.39	                                     
228.20/65.39	       [1(0(x1))] =  [1] x1 + [1]    
228.20/65.39	                  >= [1] x1 + [1]    
228.20/65.39	                  =  [0(0(0(1(x1))))]
228.20/65.39	                                     
228.20/65.39	       [0(1(x1))] =  [1] x1 + [1]    
228.20/65.39	                  >= [1] x1 + [1]    
228.20/65.39	                  =  [1(x1)]         
228.20/65.39	                                     
228.20/65.39	       [0(0(x1))] =  [1] x1 + [0]    
228.20/65.39	                  >= [1] x1 + [0]    
228.20/65.39	                  =  [0(x1)]         
228.20/65.39	                                     
228.20/65.39	   
228.20/65.39	   We return to the main proof.
228.20/65.39	   
228.20/65.39	   We are left with following problem, upon which TcT provides the
228.20/65.39	   certificate MAYBE.
228.20/65.39	   
228.20/65.39	   Strict Trs:
228.20/65.39	     { 1(0(x1)) -> 0(0(0(1(x1))))
228.20/65.39	     , 0(1(x1)) -> 1(x1)
228.20/65.39	     , 0(0(x1)) -> 0(x1) }
228.20/65.39	   Weak Trs: { 1(1(x1)) -> 0(0(0(0(x1)))) }
228.20/65.39	   Obligation:
228.20/65.39	     derivational complexity
228.20/65.39	   Answer:
228.20/65.39	     MAYBE
228.20/65.39	   
228.20/65.39	   The weightgap principle applies (using the following nonconstant
228.20/65.39	   growth matrix-interpretation)
228.20/65.39	   
228.20/65.39	   TcT has computed the following triangular matrix interpretation.
228.20/65.39	   Note that the diagonal of the component-wise maxima of
228.20/65.39	   interpretation-entries contains no more than 1 non-zero entries.
228.20/65.39	   
228.20/65.39	     [1](x1) = [1] x1 + [2]
228.20/65.39	                           
228.20/65.39	     [0](x1) = [1] x1 + [1]
228.20/65.39	   
228.20/65.39	   The order satisfies the following ordering constraints:
228.20/65.39	   
228.20/65.39	     [1(1(x1))] =  [1] x1 + [4]    
228.20/65.39	                >= [1] x1 + [4]    
228.20/65.39	                =  [0(0(0(0(x1))))]
228.20/65.39	                                   
228.20/65.39	     [1(0(x1))] =  [1] x1 + [3]    
228.20/65.39	                ?  [1] x1 + [5]    
228.20/65.39	                =  [0(0(0(1(x1))))]
228.20/65.39	                                   
228.20/65.39	     [0(1(x1))] =  [1] x1 + [3]    
228.20/65.39	                >  [1] x1 + [2]    
228.20/65.39	                =  [1(x1)]         
228.20/65.39	                                   
228.20/65.39	     [0(0(x1))] =  [1] x1 + [2]    
228.20/65.39	                >  [1] x1 + [1]    
228.20/65.39	                =  [0(x1)]         
228.20/65.39	                                   
228.20/65.39	   
228.20/65.39	   Further, it can be verified that all rules not oriented are covered by the weightgap condition.
228.20/65.39	   
228.20/65.39	   We are left with following problem, upon which TcT provides the
228.20/65.39	   certificate MAYBE.
228.20/65.39	   
228.20/65.39	   Strict Trs: { 1(0(x1)) -> 0(0(0(1(x1)))) }
228.20/65.39	   Weak Trs:
228.20/65.39	     { 1(1(x1)) -> 0(0(0(0(x1))))
228.20/65.39	     , 0(1(x1)) -> 1(x1)
228.20/65.39	     , 0(0(x1)) -> 0(x1) }
228.20/65.39	   Obligation:
228.20/65.39	     derivational complexity
228.20/65.39	   Answer:
228.20/65.39	     MAYBE
228.20/65.39	   
228.20/65.39	   None of the processors succeeded.
228.20/65.39	   
228.20/65.39	   Details of failed attempt(s):
228.20/65.39	   -----------------------------
228.20/65.39	   1) 'empty' failed due to the following reason:
228.20/65.39	      
228.20/65.39	      Empty strict component of the problem is NOT empty.
228.20/65.39	   
228.20/65.39	   2) 'Fastest' failed due to the following reason:
228.20/65.39	      
228.20/65.39	      None of the processors succeeded.
228.20/65.39	      
228.20/65.39	      Details of failed attempt(s):
228.20/65.39	      -----------------------------
228.20/65.39	      1) 'Fastest' failed due to the following reason:
228.20/65.39	         
228.20/65.39	         None of the processors succeeded.
228.20/65.39	         
228.20/65.39	         Details of failed attempt(s):
228.20/65.39	         -----------------------------
228.20/65.39	         1) 'matrix interpretation of dimension 6' failed due to the
228.20/65.39	            following reason:
228.20/65.39	            
228.20/65.39	            The input cannot be shown compatible
228.20/65.39	         
228.20/65.39	         2) 'matrix interpretation of dimension 5' failed due to the
228.20/65.39	            following reason:
228.20/65.39	            
228.20/65.39	            The input cannot be shown compatible
228.20/65.39	         
228.20/65.39	         3) 'matrix interpretation of dimension 4' failed due to the
228.20/65.39	            following reason:
228.20/65.39	            
228.20/65.39	            The input cannot be shown compatible
228.20/65.39	         
228.20/65.39	         4) 'matrix interpretation of dimension 3' failed due to the
228.20/65.39	            following reason:
228.20/65.39	            
228.20/65.39	            The input cannot be shown compatible
228.20/65.39	         
228.20/65.39	         5) 'matrix interpretation of dimension 2' failed due to the
228.20/65.39	            following reason:
228.20/65.39	            
228.20/65.39	            The input cannot be shown compatible
228.20/65.39	         
228.20/65.39	         6) 'matrix interpretation of dimension 1' failed due to the
228.20/65.39	            following reason:
228.20/65.39	            
228.20/65.39	            The input cannot be shown compatible
228.20/65.39	         
228.20/65.39	      
228.20/65.39	      2) 'Fastest (timeout of 30 seconds)' failed due to the following
228.20/65.39	         reason:
228.20/65.39	         
228.20/65.39	         Computation stopped due to timeout after 30.0 seconds.
228.20/65.39	      
228.20/65.39	      3) 'iteProgress' failed due to the following reason:
228.20/65.39	         
228.20/65.39	         Fail
228.20/65.39	      
228.20/65.39	      4) 'bsearch-matrix' failed due to the following reason:
228.20/65.39	         
228.20/65.39	         The input cannot be shown compatible
228.20/65.39	      
228.20/65.39	   
228.20/65.39	
228.20/65.39	2) 'Fastest (timeout of 60 seconds)' failed due to the following
228.20/65.39	   reason:
228.20/65.39	   
228.20/65.39	   Computation stopped due to timeout after 60.0 seconds.
228.20/65.39	
228.20/65.39	3) 'iteProgress (timeout of 297 seconds)' failed due to the
228.20/65.39	   following reason:
228.20/65.39	   
228.20/65.39	   Fail
228.20/65.39	
228.20/65.39	4) 'bsearch-matrix (timeout of 297 seconds)' failed due to the
228.20/65.39	   following reason:
228.20/65.39	   
228.20/65.39	   The input cannot be shown compatible
228.20/65.39	
228.20/65.39	
228.20/65.39	Arrrr..
228.31/65.43	EOF