MAYBE
860.26/297.56	MAYBE
860.26/297.56	
860.26/297.56	We are left with following problem, upon which TcT provides the
860.26/297.56	certificate MAYBE.
860.26/297.56	
860.26/297.56	Strict Trs:
860.26/297.56	  { a__and(X1, X2) -> and(X1, X2)
860.26/297.56	  , a__and(tt(), X) -> mark(X)
860.26/297.56	  , mark(tt()) -> tt()
860.26/297.56	  , mark(0()) -> 0()
860.26/297.56	  , mark(s(X)) -> s(mark(X))
860.26/297.56	  , mark(and(X1, X2)) -> a__and(mark(X1), X2)
860.26/297.56	  , mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2))
860.26/297.56	  , a__plus(X1, X2) -> plus(X1, X2)
860.26/297.56	  , a__plus(N, 0()) -> mark(N)
860.26/297.56	  , a__plus(N, s(M)) -> s(a__plus(mark(N), mark(M))) }
860.26/297.56	Obligation:
860.26/297.56	  runtime complexity
860.26/297.56	Answer:
860.26/297.56	  MAYBE
860.26/297.56	
860.26/297.56	The input is overlay and right-linear. Switching to innermost
860.26/297.56	rewriting.
860.26/297.56	
860.26/297.56	We are left with following problem, upon which TcT provides the
860.26/297.56	certificate MAYBE.
860.26/297.56	
860.26/297.56	Strict Trs:
860.26/297.56	  { a__and(X1, X2) -> and(X1, X2)
860.26/297.56	  , a__and(tt(), X) -> mark(X)
860.26/297.56	  , mark(tt()) -> tt()
860.26/297.56	  , mark(0()) -> 0()
860.26/297.56	  , mark(s(X)) -> s(mark(X))
860.26/297.56	  , mark(and(X1, X2)) -> a__and(mark(X1), X2)
860.26/297.56	  , mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2))
860.26/297.56	  , a__plus(X1, X2) -> plus(X1, X2)
860.26/297.56	  , a__plus(N, 0()) -> mark(N)
860.26/297.56	  , a__plus(N, s(M)) -> s(a__plus(mark(N), mark(M))) }
860.26/297.56	Obligation:
860.26/297.56	  innermost runtime complexity
860.26/297.56	Answer:
860.26/297.56	  MAYBE
860.26/297.56	
860.26/297.56	None of the processors succeeded.
860.26/297.56	
860.26/297.56	Details of failed attempt(s):
860.26/297.56	-----------------------------
860.26/297.56	1) 'empty' failed due to the following reason:
860.26/297.56	   
860.26/297.56	   Empty strict component of the problem is NOT empty.
860.26/297.56	
860.26/297.56	2) 'Best' failed due to the following reason:
860.26/297.56	   
860.26/297.56	   None of the processors succeeded.
860.26/297.56	   
860.26/297.56	   Details of failed attempt(s):
860.26/297.56	   -----------------------------
860.26/297.56	   1) 'With Problem ... (timeout of 297 seconds)' failed due to the
860.26/297.56	      following reason:
860.26/297.56	      
860.26/297.56	      Computation stopped due to timeout after 297.0 seconds.
860.26/297.56	   
860.26/297.56	   2) 'Best' failed due to the following reason:
860.26/297.56	      
860.26/297.56	      None of the processors succeeded.
860.26/297.56	      
860.26/297.56	      Details of failed attempt(s):
860.26/297.56	      -----------------------------
860.26/297.56	      1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
860.26/297.56	         seconds)' failed due to the following reason:
860.26/297.56	         
860.26/297.56	         We use the processor 'matrix interpretation of dimension 1' to
860.26/297.56	         orient following rules strictly.
860.26/297.56	         
860.26/297.56	         Trs: { a__plus(N, 0()) -> mark(N) }
860.26/297.56	         
860.26/297.56	         The induced complexity on above rules (modulo remaining rules) is
860.26/297.56	         YES(?,O(n^1)) . These rules are moved into the corresponding weak
860.26/297.56	         component(s).
860.26/297.56	         
860.26/297.56	         Sub-proof:
860.26/297.56	         ----------
860.26/297.56	           The following argument positions are usable:
860.26/297.56	             Uargs(a__and) = {1}, Uargs(a__plus) = {1, 2}, Uargs(s) = {1}
860.26/297.56	           
860.26/297.56	           TcT has computed the following constructor-based matrix
860.26/297.56	           interpretation satisfying not(EDA).
860.26/297.56	           
860.26/297.56	              [a__and](x1, x2) = [1] x1 + [1] x2 + [0]
860.26/297.56	                                                      
860.26/297.56	                          [tt] = [0]                  
860.26/297.56	                                                      
860.26/297.56	                    [mark](x1) = [1] x1 + [0]         
860.26/297.56	                                                      
860.26/297.56	             [a__plus](x1, x2) = [1] x1 + [1] x2 + [0]
860.26/297.56	                                                      
860.26/297.56	                           [0] = [4]                  
860.26/297.56	                                                      
860.26/297.56	                       [s](x1) = [1] x1 + [0]         
860.26/297.56	                                                      
860.26/297.56	                 [and](x1, x2) = [1] x1 + [1] x2 + [0]
860.26/297.56	                                                      
860.26/297.56	                [plus](x1, x2) = [1] x1 + [1] x2 + [0]
860.26/297.56	           
860.26/297.56	           The order satisfies the following ordering constraints:
860.26/297.56	           
860.26/297.56	                 [a__and(X1, X2)] =  [1] X1 + [1] X2 + [0]         
860.26/297.56	                                  >= [1] X1 + [1] X2 + [0]         
860.26/297.56	                                  =  [and(X1, X2)]                 
860.26/297.56	                                                                   
860.26/297.56	                [a__and(tt(), X)] =  [1] X + [0]                   
860.26/297.56	                                  >= [1] X + [0]                   
860.26/297.56	                                  =  [mark(X)]                     
860.26/297.56	                                                                   
860.26/297.56	                     [mark(tt())] =  [0]                           
860.26/297.56	                                  >= [0]                           
860.26/297.56	                                  =  [tt()]                        
860.26/297.56	                                                                   
860.26/297.56	                      [mark(0())] =  [4]                           
860.26/297.56	                                  >= [4]                           
860.26/297.56	                                  =  [0()]                         
860.26/297.56	                                                                   
860.26/297.56	                     [mark(s(X))] =  [1] X + [0]                   
860.26/297.56	                                  >= [1] X + [0]                   
860.26/297.56	                                  =  [s(mark(X))]                  
860.26/297.56	                                                                   
860.26/297.56	              [mark(and(X1, X2))] =  [1] X1 + [1] X2 + [0]         
860.26/297.56	                                  >= [1] X1 + [1] X2 + [0]         
860.26/297.56	                                  =  [a__and(mark(X1), X2)]        
860.26/297.56	                                                                   
860.26/297.56	             [mark(plus(X1, X2))] =  [1] X1 + [1] X2 + [0]         
860.26/297.56	                                  >= [1] X1 + [1] X2 + [0]         
860.26/297.56	                                  =  [a__plus(mark(X1), mark(X2))] 
860.26/297.56	                                                                   
860.26/297.56	                [a__plus(X1, X2)] =  [1] X1 + [1] X2 + [0]         
860.26/297.56	                                  >= [1] X1 + [1] X2 + [0]         
860.26/297.56	                                  =  [plus(X1, X2)]                
860.26/297.56	                                                                   
860.26/297.56	                [a__plus(N, 0())] =  [1] N + [4]                   
860.26/297.56	                                  >  [1] N + [0]                   
860.26/297.56	                                  =  [mark(N)]                     
860.26/297.56	                                                                   
860.26/297.56	               [a__plus(N, s(M))] =  [1] N + [1] M + [0]           
860.26/297.56	                                  >= [1] N + [1] M + [0]           
860.26/297.56	                                  =  [s(a__plus(mark(N), mark(M)))]
860.26/297.56	                                                                   
860.26/297.56	         
860.26/297.56	         We return to the main proof.
860.26/297.56	         
860.26/297.56	         We are left with following problem, upon which TcT provides the
860.26/297.56	         certificate MAYBE.
860.26/297.56	         
860.26/297.56	         Strict Trs:
860.26/297.56	           { a__and(X1, X2) -> and(X1, X2)
860.26/297.56	           , a__and(tt(), X) -> mark(X)
860.26/297.56	           , mark(tt()) -> tt()
860.26/297.56	           , mark(0()) -> 0()
860.26/297.56	           , mark(s(X)) -> s(mark(X))
860.26/297.56	           , mark(and(X1, X2)) -> a__and(mark(X1), X2)
860.26/297.56	           , mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2))
860.26/297.56	           , a__plus(X1, X2) -> plus(X1, X2)
860.26/297.56	           , a__plus(N, s(M)) -> s(a__plus(mark(N), mark(M))) }
860.26/297.56	         Weak Trs: { a__plus(N, 0()) -> mark(N) }
860.26/297.56	         Obligation:
860.26/297.56	           innermost runtime complexity
860.26/297.56	         Answer:
860.26/297.56	           MAYBE
860.26/297.56	         
860.26/297.56	         The weightgap principle applies (using the following nonconstant
860.26/297.56	         growth matrix-interpretation)
860.26/297.56	         
860.26/297.56	         The following argument positions are usable:
860.26/297.56	           Uargs(a__and) = {1}, Uargs(a__plus) = {1, 2}, Uargs(s) = {1}
860.26/297.56	         
860.26/297.56	         TcT has computed the following matrix interpretation satisfying
860.26/297.56	         not(EDA) and not(IDA(1)).
860.26/297.56	         
860.26/297.56	            [a__and](x1, x2) = [1] x1 + [1]         
860.26/297.56	                                                    
860.26/297.56	                        [tt] = [0]                  
860.26/297.56	                                                    
860.26/297.56	                  [mark](x1) = [0]                  
860.26/297.56	                                                    
860.26/297.56	           [a__plus](x1, x2) = [1] x1 + [1] x2 + [0]
860.26/297.56	                                                    
860.26/297.56	                         [0] = [4]                  
860.26/297.56	                                                    
860.26/297.56	                     [s](x1) = [1] x1 + [0]         
860.26/297.56	                                                    
860.26/297.56	               [and](x1, x2) = [1] x1 + [0]         
860.26/297.56	                                                    
860.26/297.56	              [plus](x1, x2) = [1] x1 + [1] x2 + [7]
860.26/297.56	         
860.26/297.56	         The order satisfies the following ordering constraints:
860.26/297.56	         
860.26/297.56	               [a__and(X1, X2)] =  [1] X1 + [1]                  
860.26/297.56	                                >  [1] X1 + [0]                  
860.26/297.56	                                =  [and(X1, X2)]                 
860.26/297.56	                                                                 
860.26/297.56	              [a__and(tt(), X)] =  [1]                           
860.26/297.56	                                >  [0]                           
860.26/297.56	                                =  [mark(X)]                     
860.26/297.56	                                                                 
860.26/297.56	                   [mark(tt())] =  [0]                           
860.26/297.56	                                >= [0]                           
860.26/297.56	                                =  [tt()]                        
860.26/297.56	                                                                 
860.26/297.56	                    [mark(0())] =  [0]                           
860.26/297.56	                                ?  [4]                           
860.26/297.56	                                =  [0()]                         
860.26/297.56	                                                                 
860.26/297.56	                   [mark(s(X))] =  [0]                           
860.26/297.56	                                >= [0]                           
860.26/297.56	                                =  [s(mark(X))]                  
860.26/297.56	                                                                 
860.26/297.56	            [mark(and(X1, X2))] =  [0]                           
860.26/297.56	                                ?  [1]                           
860.26/297.56	                                =  [a__and(mark(X1), X2)]        
860.26/297.56	                                                                 
860.26/297.56	           [mark(plus(X1, X2))] =  [0]                           
860.26/297.56	                                >= [0]                           
860.26/297.56	                                =  [a__plus(mark(X1), mark(X2))] 
860.26/297.56	                                                                 
860.26/297.56	              [a__plus(X1, X2)] =  [1] X1 + [1] X2 + [0]         
860.26/297.56	                                ?  [1] X1 + [1] X2 + [7]         
860.26/297.56	                                =  [plus(X1, X2)]                
860.26/297.56	                                                                 
860.26/297.56	              [a__plus(N, 0())] =  [1] N + [4]                   
860.26/297.56	                                >  [0]                           
860.26/297.56	                                =  [mark(N)]                     
860.26/297.56	                                                                 
860.26/297.56	             [a__plus(N, s(M))] =  [1] N + [1] M + [0]           
860.26/297.56	                                >= [0]                           
860.26/297.56	                                =  [s(a__plus(mark(N), mark(M)))]
860.26/297.56	                                                                 
860.26/297.56	         
860.26/297.56	         Further, it can be verified that all rules not oriented are covered by the weightgap condition.
860.26/297.56	         
860.26/297.56	         We are left with following problem, upon which TcT provides the
860.26/297.56	         certificate MAYBE.
860.26/297.56	         
860.26/297.56	         Strict Trs:
860.26/297.56	           { mark(tt()) -> tt()
860.26/297.56	           , mark(0()) -> 0()
860.26/297.56	           , mark(s(X)) -> s(mark(X))
860.26/297.56	           , mark(and(X1, X2)) -> a__and(mark(X1), X2)
860.26/297.56	           , mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2))
860.26/297.56	           , a__plus(X1, X2) -> plus(X1, X2)
860.26/297.56	           , a__plus(N, s(M)) -> s(a__plus(mark(N), mark(M))) }
860.26/297.56	         Weak Trs:
860.26/297.56	           { a__and(X1, X2) -> and(X1, X2)
860.26/297.56	           , a__and(tt(), X) -> mark(X)
860.26/297.56	           , a__plus(N, 0()) -> mark(N) }
860.26/297.56	         Obligation:
860.26/297.56	           innermost runtime complexity
860.26/297.56	         Answer:
860.26/297.56	           MAYBE
860.26/297.56	         
860.26/297.56	         The weightgap principle applies (using the following nonconstant
860.26/297.56	         growth matrix-interpretation)
860.26/297.56	         
860.26/297.56	         The following argument positions are usable:
860.26/297.56	           Uargs(a__and) = {1}, Uargs(a__plus) = {1, 2}, Uargs(s) = {1}
860.26/297.56	         
860.26/297.56	         TcT has computed the following matrix interpretation satisfying
860.26/297.56	         not(EDA) and not(IDA(1)).
860.26/297.56	         
860.26/297.56	            [a__and](x1, x2) = [1] x1 + [1] x2 + [4]
860.26/297.56	                                                    
860.26/297.56	                        [tt] = [4]                  
860.26/297.56	                                                    
860.26/297.56	                  [mark](x1) = [1] x1 + [0]         
860.26/297.56	                                                    
860.26/297.56	           [a__plus](x1, x2) = [1] x1 + [1] x2 + [0]
860.26/297.56	                                                    
860.26/297.56	                         [0] = [4]                  
860.26/297.56	                                                    
860.26/297.56	                     [s](x1) = [1] x1 + [0]         
860.26/297.56	                                                    
860.26/297.56	               [and](x1, x2) = [1] x1 + [1] x2 + [0]
860.26/297.56	                                                    
860.26/297.56	              [plus](x1, x2) = [1] x1 + [1] x2 + [1]
860.26/297.56	         
860.26/297.56	         The order satisfies the following ordering constraints:
860.26/297.56	         
860.26/297.56	               [a__and(X1, X2)] =  [1] X1 + [1] X2 + [4]         
860.26/297.56	                                >  [1] X1 + [1] X2 + [0]         
860.26/297.56	                                =  [and(X1, X2)]                 
860.26/297.56	                                                                 
860.26/297.56	              [a__and(tt(), X)] =  [1] X + [8]                   
860.26/297.56	                                >  [1] X + [0]                   
860.26/297.56	                                =  [mark(X)]                     
860.26/297.56	                                                                 
860.26/297.56	                   [mark(tt())] =  [4]                           
860.26/297.56	                                >= [4]                           
860.26/297.56	                                =  [tt()]                        
860.26/297.56	                                                                 
860.26/297.56	                    [mark(0())] =  [4]                           
860.26/297.56	                                >= [4]                           
860.26/297.56	                                =  [0()]                         
860.26/297.56	                                                                 
860.26/297.56	                   [mark(s(X))] =  [1] X + [0]                   
860.26/297.56	                                >= [1] X + [0]                   
860.26/297.56	                                =  [s(mark(X))]                  
860.26/297.56	                                                                 
860.26/297.56	            [mark(and(X1, X2))] =  [1] X1 + [1] X2 + [0]         
860.26/297.56	                                ?  [1] X1 + [1] X2 + [4]         
860.26/297.56	                                =  [a__and(mark(X1), X2)]        
860.26/297.56	                                                                 
860.26/297.56	           [mark(plus(X1, X2))] =  [1] X1 + [1] X2 + [1]         
860.26/297.56	                                >  [1] X1 + [1] X2 + [0]         
860.26/297.56	                                =  [a__plus(mark(X1), mark(X2))] 
860.26/297.56	                                                                 
860.26/297.56	              [a__plus(X1, X2)] =  [1] X1 + [1] X2 + [0]         
860.26/297.56	                                ?  [1] X1 + [1] X2 + [1]         
860.26/297.56	                                =  [plus(X1, X2)]                
860.26/297.56	                                                                 
860.26/297.56	              [a__plus(N, 0())] =  [1] N + [4]                   
860.26/297.56	                                >  [1] N + [0]                   
860.26/297.56	                                =  [mark(N)]                     
860.26/297.56	                                                                 
860.26/297.56	             [a__plus(N, s(M))] =  [1] N + [1] M + [0]           
860.26/297.56	                                >= [1] N + [1] M + [0]           
860.26/297.56	                                =  [s(a__plus(mark(N), mark(M)))]
860.26/297.56	                                                                 
860.26/297.56	         
860.26/297.56	         Further, it can be verified that all rules not oriented are covered by the weightgap condition.
860.26/297.56	         
860.26/297.56	         We are left with following problem, upon which TcT provides the
860.26/297.56	         certificate MAYBE.
860.26/297.56	         
860.26/297.56	         Strict Trs:
860.26/297.56	           { mark(tt()) -> tt()
860.26/297.56	           , mark(0()) -> 0()
860.26/297.56	           , mark(s(X)) -> s(mark(X))
860.26/297.56	           , mark(and(X1, X2)) -> a__and(mark(X1), X2)
860.26/297.56	           , a__plus(X1, X2) -> plus(X1, X2)
860.26/297.56	           , a__plus(N, s(M)) -> s(a__plus(mark(N), mark(M))) }
860.26/297.56	         Weak Trs:
860.26/297.56	           { a__and(X1, X2) -> and(X1, X2)
860.26/297.56	           , a__and(tt(), X) -> mark(X)
860.26/297.56	           , mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2))
860.26/297.56	           , a__plus(N, 0()) -> mark(N) }
860.26/297.56	         Obligation:
860.26/297.56	           innermost runtime complexity
860.26/297.56	         Answer:
860.26/297.56	           MAYBE
860.26/297.56	         
860.26/297.56	         The weightgap principle applies (using the following nonconstant
860.26/297.56	         growth matrix-interpretation)
860.26/297.56	         
860.26/297.56	         The following argument positions are usable:
860.26/297.56	           Uargs(a__and) = {1}, Uargs(a__plus) = {1, 2}, Uargs(s) = {1}
860.26/297.56	         
860.26/297.56	         TcT has computed the following matrix interpretation satisfying
860.26/297.56	         not(EDA) and not(IDA(1)).
860.26/297.56	         
860.26/297.56	            [a__and](x1, x2) = [1] x1 + [1] x2 + [7]
860.26/297.56	                                                    
860.26/297.56	                        [tt] = [4]                  
860.26/297.56	                                                    
860.26/297.56	                  [mark](x1) = [1] x1 + [1]         
860.26/297.56	                                                    
860.26/297.56	           [a__plus](x1, x2) = [1] x1 + [1] x2 + [0]
860.26/297.56	                                                    
860.26/297.56	                         [0] = [4]                  
860.26/297.56	                                                    
860.26/297.56	                     [s](x1) = [1] x1 + [0]         
860.26/297.56	                                                    
860.26/297.56	               [and](x1, x2) = [1] x1 + [1] x2 + [0]
860.26/297.56	                                                    
860.26/297.56	              [plus](x1, x2) = [1] x1 + [1] x2 + [2]
860.26/297.56	         
860.26/297.56	         The order satisfies the following ordering constraints:
860.26/297.56	         
860.26/297.56	               [a__and(X1, X2)] =  [1] X1 + [1] X2 + [7]         
860.26/297.56	                                >  [1] X1 + [1] X2 + [0]         
860.26/297.56	                                =  [and(X1, X2)]                 
860.26/297.56	                                                                 
860.26/297.56	              [a__and(tt(), X)] =  [1] X + [11]                  
860.26/297.56	                                >  [1] X + [1]                   
860.26/297.56	                                =  [mark(X)]                     
860.26/297.56	                                                                 
860.26/297.56	                   [mark(tt())] =  [5]                           
860.26/297.56	                                >  [4]                           
860.26/297.56	                                =  [tt()]                        
860.26/297.56	                                                                 
860.26/297.56	                    [mark(0())] =  [5]                           
860.26/297.56	                                >  [4]                           
860.26/297.56	                                =  [0()]                         
860.26/297.56	                                                                 
860.26/297.56	                   [mark(s(X))] =  [1] X + [1]                   
860.26/297.56	                                >= [1] X + [1]                   
860.26/297.56	                                =  [s(mark(X))]                  
860.26/297.56	                                                                 
860.26/297.56	            [mark(and(X1, X2))] =  [1] X1 + [1] X2 + [1]         
860.26/297.56	                                ?  [1] X1 + [1] X2 + [8]         
860.26/297.56	                                =  [a__and(mark(X1), X2)]        
860.26/297.56	                                                                 
860.26/297.56	           [mark(plus(X1, X2))] =  [1] X1 + [1] X2 + [3]         
860.26/297.56	                                >  [1] X1 + [1] X2 + [2]         
860.26/297.56	                                =  [a__plus(mark(X1), mark(X2))] 
860.26/297.56	                                                                 
860.26/297.56	              [a__plus(X1, X2)] =  [1] X1 + [1] X2 + [0]         
860.26/297.56	                                ?  [1] X1 + [1] X2 + [2]         
860.26/297.56	                                =  [plus(X1, X2)]                
860.26/297.56	                                                                 
860.26/297.56	              [a__plus(N, 0())] =  [1] N + [4]                   
860.26/297.56	                                >  [1] N + [1]                   
860.26/297.56	                                =  [mark(N)]                     
860.26/297.56	                                                                 
860.26/297.56	             [a__plus(N, s(M))] =  [1] N + [1] M + [0]           
860.26/297.56	                                ?  [1] N + [1] M + [2]           
860.26/297.56	                                =  [s(a__plus(mark(N), mark(M)))]
860.26/297.56	                                                                 
860.26/297.56	         
860.26/297.56	         Further, it can be verified that all rules not oriented are covered by the weightgap condition.
860.26/297.56	         
860.26/297.56	         We are left with following problem, upon which TcT provides the
860.26/297.56	         certificate MAYBE.
860.26/297.56	         
860.26/297.56	         Strict Trs:
860.26/297.56	           { mark(s(X)) -> s(mark(X))
860.26/297.56	           , mark(and(X1, X2)) -> a__and(mark(X1), X2)
860.26/297.56	           , a__plus(X1, X2) -> plus(X1, X2)
860.26/297.56	           , a__plus(N, s(M)) -> s(a__plus(mark(N), mark(M))) }
860.26/297.56	         Weak Trs:
860.26/297.56	           { a__and(X1, X2) -> and(X1, X2)
860.26/297.56	           , a__and(tt(), X) -> mark(X)
860.26/297.56	           , mark(tt()) -> tt()
860.26/297.56	           , mark(0()) -> 0()
860.26/297.56	           , mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2))
860.26/297.56	           , a__plus(N, 0()) -> mark(N) }
860.26/297.56	         Obligation:
860.26/297.56	           innermost runtime complexity
860.26/297.56	         Answer:
860.26/297.56	           MAYBE
860.26/297.56	         
860.26/297.56	         None of the processors succeeded.
860.26/297.56	         
860.26/297.56	         Details of failed attempt(s):
860.26/297.56	         -----------------------------
860.26/297.56	         1) 'empty' failed due to the following reason:
860.26/297.56	            
860.26/297.56	            Empty strict component of the problem is NOT empty.
860.26/297.56	         
860.26/297.56	         2) 'With Problem ...' failed due to the following reason:
860.26/297.56	            
860.26/297.56	            None of the processors succeeded.
860.26/297.56	            
860.26/297.56	            Details of failed attempt(s):
860.26/297.56	            -----------------------------
860.26/297.56	            1) 'empty' failed due to the following reason:
860.26/297.56	               
860.26/297.56	               Empty strict component of the problem is NOT empty.
860.26/297.56	            
860.26/297.56	            2) 'Fastest' failed due to the following reason:
860.26/297.56	               
860.26/297.56	               None of the processors succeeded.
860.26/297.56	               
860.26/297.56	               Details of failed attempt(s):
860.26/297.56	               -----------------------------
860.26/297.56	               1) 'With Problem ...' failed due to the following reason:
860.26/297.56	                  
860.26/297.56	                  None of the processors succeeded.
860.26/297.56	                  
860.26/297.56	                  Details of failed attempt(s):
860.26/297.56	                  -----------------------------
860.26/297.56	                  1) 'empty' failed due to the following reason:
860.26/297.56	                     
860.26/297.56	                     Empty strict component of the problem is NOT empty.
860.26/297.56	                  
860.26/297.56	                  2) 'With Problem ...' failed due to the following reason:
860.26/297.56	                     
860.26/297.56	                     We use the processor 'matrix interpretation of dimension 2' to
860.26/297.56	                     orient following rules strictly.
860.26/297.56	                     
860.26/297.56	                     Trs: { a__plus(N, s(M)) -> s(a__plus(mark(N), mark(M))) }
860.26/297.56	                     
860.26/297.56	                     The induced complexity on above rules (modulo remaining rules) is
860.26/297.56	                     YES(?,O(n^2)) . These rules are moved into the corresponding weak
860.26/297.56	                     component(s).
860.26/297.56	                     
860.26/297.56	                     Sub-proof:
860.26/297.56	                     ----------
860.26/297.56	                       The following argument positions are usable:
860.26/297.56	                         Uargs(a__and) = {1}, Uargs(a__plus) = {1, 2}, Uargs(s) = {1}
860.26/297.56	                       
860.26/297.56	                       TcT has computed the following constructor-based matrix
860.26/297.56	                       interpretation satisfying not(EDA).
860.26/297.56	                       
860.26/297.56	                          [a__and](x1, x2) = [1 0] x1 + [1 0] x2 + [0]
860.26/297.56	                                             [0 0]      [0 1]      [0]
860.26/297.56	                                                                      
860.26/297.56	                                      [tt] = [0]                      
860.26/297.56	                                             [0]                      
860.26/297.56	                                                                      
860.26/297.56	                                [mark](x1) = [1 0] x1 + [0]           
860.26/297.56	                                             [0 1]      [0]           
860.26/297.56	                                                                      
860.26/297.56	                         [a__plus](x1, x2) = [1 0] x1 + [1 1] x2 + [0]
860.26/297.56	                                             [0 1]      [0 1]      [0]
860.26/297.56	                                                                      
860.26/297.56	                                       [0] = [0]                      
860.26/297.56	                                             [0]                      
860.26/297.56	                                                                      
860.26/297.56	                                   [s](x1) = [1 0] x1 + [0]           
860.26/297.56	                                             [0 1]      [1]           
860.26/297.56	                                                                      
860.26/297.56	                             [and](x1, x2) = [1 0] x1 + [1 0] x2 + [0]
860.26/297.56	                                             [0 0]      [0 1]      [0]
860.26/297.56	                                                                      
860.26/297.56	                            [plus](x1, x2) = [1 0] x1 + [1 1] x2 + [0]
860.26/297.56	                                             [0 1]      [0 1]      [0]
860.26/297.56	                       
860.26/297.56	                       The order satisfies the following ordering constraints:
860.26/297.56	                       
860.26/297.56	                             [a__and(X1, X2)] =  [1 0] X1 + [1 0] X2 + [0]     
860.26/297.56	                                                 [0 0]      [0 1]      [0]     
860.26/297.56	                                              >= [1 0] X1 + [1 0] X2 + [0]     
860.26/297.56	                                                 [0 0]      [0 1]      [0]     
860.26/297.56	                                              =  [and(X1, X2)]                 
860.26/297.56	                                                                               
860.26/297.56	                            [a__and(tt(), X)] =  [1 0] X + [0]                 
860.26/297.56	                                                 [0 1]     [0]                 
860.26/297.56	                                              >= [1 0] X + [0]                 
860.26/297.56	                                                 [0 1]     [0]                 
860.26/297.56	                                              =  [mark(X)]                     
860.26/297.56	                                                                               
860.26/297.56	                                 [mark(tt())] =  [0]                           
860.26/297.56	                                                 [0]                           
860.26/297.56	                                              >= [0]                           
860.26/297.56	                                                 [0]                           
860.26/297.56	                                              =  [tt()]                        
860.26/297.56	                                                                               
860.26/297.56	                                  [mark(0())] =  [0]                           
860.26/297.56	                                                 [0]                           
860.26/297.56	                                              >= [0]                           
860.26/297.56	                                                 [0]                           
860.26/297.56	                                              =  [0()]                         
860.26/297.56	                                                                               
860.26/297.56	                                 [mark(s(X))] =  [1 0] X + [0]                 
860.26/297.56	                                                 [0 1]     [1]                 
860.26/297.56	                                              >= [1 0] X + [0]                 
860.26/297.56	                                                 [0 1]     [1]                 
860.26/297.56	                                              =  [s(mark(X))]                  
860.26/297.56	                                                                               
860.26/297.56	                          [mark(and(X1, X2))] =  [1 0] X1 + [1 0] X2 + [0]     
860.26/297.56	                                                 [0 0]      [0 1]      [0]     
860.26/297.56	                                              >= [1 0] X1 + [1 0] X2 + [0]     
860.26/297.56	                                                 [0 0]      [0 1]      [0]     
860.26/297.56	                                              =  [a__and(mark(X1), X2)]        
860.26/297.56	                                                                               
860.26/297.56	                         [mark(plus(X1, X2))] =  [1 0] X1 + [1 1] X2 + [0]     
860.26/297.56	                                                 [0 1]      [0 1]      [0]     
860.26/297.56	                                              >= [1 0] X1 + [1 1] X2 + [0]     
860.26/297.56	                                                 [0 1]      [0 1]      [0]     
860.26/297.56	                                              =  [a__plus(mark(X1), mark(X2))] 
860.26/297.56	                                                                               
860.26/297.56	                            [a__plus(X1, X2)] =  [1 0] X1 + [1 1] X2 + [0]     
860.26/297.56	                                                 [0 1]      [0 1]      [0]     
860.26/297.56	                                              >= [1 0] X1 + [1 1] X2 + [0]     
860.26/297.56	                                                 [0 1]      [0 1]      [0]     
860.26/297.56	                                              =  [plus(X1, X2)]                
860.26/297.56	                                                                               
860.26/297.56	                            [a__plus(N, 0())] =  [1 0] N + [0]                 
860.26/297.56	                                                 [0 1]     [0]                 
860.26/297.56	                                              >= [1 0] N + [0]                 
860.26/297.56	                                                 [0 1]     [0]                 
860.26/297.56	                                              =  [mark(N)]                     
860.26/297.56	                                                                               
860.26/297.56	                           [a__plus(N, s(M))] =  [1 0] N + [1 1] M + [1]       
860.26/297.56	                                                 [0 1]     [0 1]     [1]       
860.26/297.56	                                              >  [1 0] N + [1 1] M + [0]       
860.26/297.56	                                                 [0 1]     [0 1]     [1]       
860.26/297.56	                                              =  [s(a__plus(mark(N), mark(M)))]
860.26/297.56	                                                                               
860.26/297.56	                     
860.26/297.56	                     We return to the main proof.
860.26/297.56	                     
860.26/297.56	                     We are left with following problem, upon which TcT provides the
860.26/297.56	                     certificate MAYBE.
860.26/297.56	                     
860.26/297.56	                     Strict Trs:
860.26/297.56	                       { mark(s(X)) -> s(mark(X))
860.26/297.56	                       , mark(and(X1, X2)) -> a__and(mark(X1), X2)
860.26/297.56	                       , a__plus(X1, X2) -> plus(X1, X2) }
860.26/297.56	                     Weak Trs:
860.26/297.56	                       { a__and(X1, X2) -> and(X1, X2)
860.26/297.56	                       , a__and(tt(), X) -> mark(X)
860.26/297.56	                       , mark(tt()) -> tt()
860.26/297.56	                       , mark(0()) -> 0()
860.26/297.56	                       , mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2))
860.26/297.56	                       , a__plus(N, 0()) -> mark(N)
860.26/297.56	                       , a__plus(N, s(M)) -> s(a__plus(mark(N), mark(M))) }
860.26/297.56	                     Obligation:
860.26/297.56	                       innermost runtime complexity
860.26/297.56	                     Answer:
860.26/297.56	                       MAYBE
860.26/297.56	                     
860.26/297.56	                     None of the processors succeeded.
860.26/297.56	                     
860.26/297.56	                     Details of failed attempt(s):
860.26/297.56	                     -----------------------------
860.26/297.56	                     1) 'empty' failed due to the following reason:
860.26/297.56	                        
860.26/297.56	                        Empty strict component of the problem is NOT empty.
860.26/297.56	                     
860.26/297.56	                     2) 'With Problem ...' failed due to the following reason:
860.26/297.56	                        
860.26/297.56	                        None of the processors succeeded.
860.26/297.56	                        
860.26/297.56	                        Details of failed attempt(s):
860.26/297.56	                        -----------------------------
860.26/297.56	                        1) 'empty' failed due to the following reason:
860.26/297.56	                           
860.26/297.56	                           Empty strict component of the problem is NOT empty.
860.26/297.56	                        
860.26/297.56	                        2) 'With Problem ...' failed due to the following reason:
860.26/297.56	                           
860.26/297.56	                           Empty strict component of the problem is NOT empty.
860.26/297.56	                        
860.26/297.56	                     
860.26/297.56	                  
860.26/297.56	               
860.26/297.56	               2) 'With Problem ...' failed due to the following reason:
860.26/297.56	                  
860.26/297.56	                  None of the processors succeeded.
860.26/297.56	                  
860.26/297.56	                  Details of failed attempt(s):
860.26/297.56	                  -----------------------------
860.26/297.56	                  1) 'empty' failed due to the following reason:
860.26/297.56	                     
860.26/297.56	                     Empty strict component of the problem is NOT empty.
860.26/297.56	                  
860.26/297.56	                  2) 'With Problem ...' failed due to the following reason:
860.26/297.56	                     
860.26/297.56	                     Empty strict component of the problem is NOT empty.
860.26/297.56	                  
860.26/297.56	               
860.26/297.56	            
860.26/297.56	         
860.26/297.56	      
860.26/297.56	      2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
860.26/297.56	         failed due to the following reason:
860.26/297.56	         
860.26/297.56	         Computation stopped due to timeout after 24.0 seconds.
860.26/297.56	      
860.26/297.56	      3) 'Best' failed due to the following reason:
860.26/297.56	         
860.26/297.56	         None of the processors succeeded.
860.26/297.56	         
860.26/297.56	         Details of failed attempt(s):
860.26/297.56	         -----------------------------
860.26/297.56	         1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
860.26/297.56	            following reason:
860.26/297.56	            
860.26/297.56	            The input cannot be shown compatible
860.26/297.56	         
860.26/297.56	         2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
860.26/297.56	            to the following reason:
860.26/297.56	            
860.26/297.56	            The input cannot be shown compatible
860.26/297.56	         
860.26/297.56	      
860.26/297.56	   
860.26/297.56	
860.26/297.56	
860.26/297.56	Arrrr..
860.64/297.77	EOF