YES(?,O(n^1))
10.25/5.85	YES(?,O(n^1))
10.25/5.85	
10.25/5.85	We are left with following problem, upon which TcT provides the
10.25/5.85	certificate YES(?,O(n^1)).
10.25/5.85	
10.25/5.85	Strict Trs:
10.25/5.85	  { app(app(app(uncurry(), f), x), y) -> app(app(f, x), y) }
10.25/5.85	Obligation:
10.25/5.85	  derivational complexity
10.25/5.85	Answer:
10.25/5.85	  YES(?,O(n^1))
10.25/5.85	
10.25/5.85	We uncurry the input using the following uncurry rules.
10.25/5.85	
10.25/5.85	  { app(uncurry(), x_1) -> uncurry_1(x_1)
10.25/5.85	  , app(uncurry_1(x_1), x_2) -> uncurry_2(x_1, x_2)
10.25/5.85	  , app(uncurry_2(x_1, x_2), x_3) -> uncurry_3(x_1, x_2, x_3) }
10.25/5.85	
10.25/5.85	We are left with following problem, upon which TcT provides the
10.25/5.85	certificate YES(?,O(n^1)).
10.25/5.85	
10.25/5.85	Strict Trs: { uncurry_3(f, x, y) -> app(app(f, x), y) }
10.25/5.85	Weak Trs:
10.25/5.85	  { app(uncurry(), x_1) -> uncurry_1(x_1)
10.25/5.85	  , app(uncurry_1(x_1), x_2) -> uncurry_2(x_1, x_2)
10.25/5.85	  , app(uncurry_2(x_1, x_2), x_3) -> uncurry_3(x_1, x_2, x_3) }
10.25/5.85	Obligation:
10.25/5.85	  derivational complexity
10.25/5.85	Answer:
10.25/5.85	  YES(?,O(n^1))
10.25/5.85	
10.25/5.85	TcT has computed the following matrix interpretation satisfying
10.25/5.85	not(EDA) and not(IDA(1)).
10.25/5.85	
10.25/5.85	                            [1 1 0 0]      [1 1 0 0]      [0]         
10.25/5.85	            [app](x1, x2) = [0 0 0 1] x1 + [0 0 0 1] x2 + [0]         
10.25/5.85	                            [0 0 0 0]      [0 0 0 0]      [0]         
10.25/5.85	                            [0 0 0 0]      [0 0 0 0]      [1]         
10.25/5.85	                                                                      
10.25/5.85	                            [1 1 0 1]      [1 1 0 1]      [1 1 0      
10.25/5.85	                                                           0]      [1]
10.25/5.85	  [uncurry_3](x1, x2, x3) = [0 0 0 0] x1 + [0 0 0 0] x2 + [0 0 0      
10.25/5.85	                                                           1] x3 + [1]
10.25/5.85	                            [0 0 0 0]      [0 0 0 0]      [0 0 0      
10.25/5.85	                                                           0]      [0]
10.25/5.85	                            [0 0 0 0]      [0 0 0 0]      [0 0 0      
10.25/5.85	                                                           0]      [1]
10.25/5.85	                                                                      
10.25/5.85	                            [0]                                       
10.25/5.85	                [uncurry] = [0]                                       
10.25/5.85	                            [0]                                       
10.25/5.85	                            [0]                                       
10.25/5.85	                                                                      
10.25/5.85	                            [1 1 0 0]      [0]                        
10.25/5.85	          [uncurry_1](x1) = [0 0 0 1] x1 + [0]                        
10.25/5.85	                            [0 0 0 0]      [0]                        
10.25/5.85	                            [0 0 0 0]      [1]                        
10.25/5.85	                                                                      
10.25/5.85	                            [1 1 0 1]      [1 1 0 0]      [0]         
10.25/5.85	      [uncurry_2](x1, x2) = [0 0 0 0] x1 + [0 0 0 1] x2 + [1]         
10.25/5.85	                            [0 0 0 0]      [0 0 0 0]      [0]         
10.25/5.85	                            [0 0 0 0]      [0 0 0 0]      [1]         
10.25/5.85	
10.25/5.85	The order satisfies the following ordering constraints:
10.25/5.85	
10.25/5.85	            [app(uncurry(), x_1)] =  [1 1 0 0]       [0]                                
10.25/5.85	                                     [0 0 0 1] x_1 + [0]                                
10.25/5.85	                                     [0 0 0 0]       [0]                                
10.25/5.85	                                     [0 0 0 0]       [1]                                
10.25/5.85	                                  >= [1 1 0 0]       [0]                                
10.25/5.85	                                     [0 0 0 1] x_1 + [0]                                
10.25/5.85	                                     [0 0 0 0]       [0]                                
10.25/5.85	                                     [0 0 0 0]       [1]                                
10.25/5.85	                                  =  [uncurry_1(x_1)]                                   
10.25/5.85	                                                                                        
10.25/5.85	       [app(uncurry_1(x_1), x_2)] =  [1 1 0 1]       [1 1 0 0]       [0]                
10.25/5.85	                                     [0 0 0 0] x_1 + [0 0 0 1] x_2 + [1]                
10.25/5.85	                                     [0 0 0 0]       [0 0 0 0]       [0]                
10.25/5.85	                                     [0 0 0 0]       [0 0 0 0]       [1]                
10.25/5.85	                                  >= [1 1 0 1]       [1 1 0 0]       [0]                
10.25/5.85	                                     [0 0 0 0] x_1 + [0 0 0 1] x_2 + [1]                
10.25/5.85	                                     [0 0 0 0]       [0 0 0 0]       [0]                
10.25/5.85	                                     [0 0 0 0]       [0 0 0 0]       [1]                
10.25/5.85	                                  =  [uncurry_2(x_1, x_2)]                              
10.25/5.85	                                                                                        
10.25/5.85	  [app(uncurry_2(x_1, x_2), x_3)] =  [1 1 0 1]       [1 1 0 1]       [1 1 0 0]       [1]
10.25/5.85	                                     [0 0 0 0] x_1 + [0 0 0 0] x_2 + [0 0 0 1] x_3 + [1]
10.25/5.85	                                     [0 0 0 0]       [0 0 0 0]       [0 0 0 0]       [0]
10.25/5.85	                                     [0 0 0 0]       [0 0 0 0]       [0 0 0 0]       [1]
10.25/5.85	                                  >= [1 1 0 1]       [1 1 0 1]       [1 1 0 0]       [1]
10.25/5.85	                                     [0 0 0 0] x_1 + [0 0 0 0] x_2 + [0 0 0 1] x_3 + [1]
10.25/5.85	                                     [0 0 0 0]       [0 0 0 0]       [0 0 0 0]       [0]
10.25/5.85	                                     [0 0 0 0]       [0 0 0 0]       [0 0 0 0]       [1]
10.25/5.85	                                  =  [uncurry_3(x_1, x_2, x_3)]                         
10.25/5.85	                                                                                        
10.25/5.85	             [uncurry_3(f, x, y)] =  [1 1 0 1]     [1 1 0 1]     [1 1 0 0]     [1]      
10.25/5.85	                                     [0 0 0 0] f + [0 0 0 0] x + [0 0 0 1] y + [1]      
10.25/5.85	                                     [0 0 0 0]     [0 0 0 0]     [0 0 0 0]     [0]      
10.25/5.85	                                     [0 0 0 0]     [0 0 0 0]     [0 0 0 0]     [1]      
10.25/5.85	                                  >  [1 1 0 1]     [1 1 0 1]     [1 1 0 0]     [0]      
10.25/5.85	                                     [0 0 0 0] f + [0 0 0 0] x + [0 0 0 1] y + [1]      
10.25/5.85	                                     [0 0 0 0]     [0 0 0 0]     [0 0 0 0]     [0]      
10.25/5.85	                                     [0 0 0 0]     [0 0 0 0]     [0 0 0 0]     [1]      
10.25/5.85	                                  =  [app(app(f, x), y)]                                
10.25/5.85	                                                                                        
10.25/5.85	
10.25/5.85	Hurray, we answered YES(?,O(n^1))
10.25/5.87	EOF