MAYBE
139.11/72.52	MAYBE
139.11/72.52	
139.11/72.52	We are left with following problem, upon which TcT provides the
139.11/72.52	certificate MAYBE.
139.11/72.52	
139.11/72.52	Strict Trs:
139.11/72.52	  { le(0(), y) -> true()
139.11/72.52	  , le(s(x), 0()) -> false()
139.11/72.52	  , le(s(x), s(y)) -> le(x, y)
139.11/72.52	  , int(x, y) -> if(le(x, y), x, y)
139.11/72.52	  , if(true(), x, y) -> cons(x, int(s(x), y))
139.11/72.52	  , if(false(), x, y) -> nil() }
139.11/72.52	Obligation:
139.11/72.52	  runtime complexity
139.11/72.52	Answer:
139.11/72.52	  MAYBE
139.11/72.52	
139.11/72.52	None of the processors succeeded.
139.11/72.52	
139.11/72.52	Details of failed attempt(s):
139.11/72.52	-----------------------------
139.11/72.52	1) 'Best' failed due to the following reason:
139.11/72.52	   
139.11/72.52	   None of the processors succeeded.
139.11/72.52	   
139.11/72.52	   Details of failed attempt(s):
139.11/72.52	   -----------------------------
139.11/72.52	   1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
139.11/72.52	      seconds)' failed due to the following reason:
139.11/72.52	      
139.11/72.52	      The weightgap principle applies (using the following nonconstant
139.11/72.52	      growth matrix-interpretation)
139.11/72.52	      
139.11/72.52	      The following argument positions are usable:
139.11/72.52	        Uargs(if) = {1}, Uargs(cons) = {2}
139.11/72.52	      
139.11/72.52	      TcT has computed the following matrix interpretation satisfying
139.11/72.52	      not(EDA) and not(IDA(1)).
139.11/72.53	      
139.11/72.53	            [le](x1, x2) = [4]                           
139.11/72.53	                                                         
139.11/72.53	                     [0] = [7]                           
139.11/72.53	                                                         
139.11/72.53	                  [true] = [1]                           
139.11/72.53	                                                         
139.11/72.53	                 [s](x1) = [1] x1 + [0]                  
139.11/72.53	                                                         
139.11/72.53	                 [false] = [1]                           
139.11/72.53	                                                         
139.11/72.53	           [int](x1, x2) = [1] x1 + [1] x2 + [5]         
139.11/72.53	                                                         
139.11/72.53	        [if](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
139.11/72.53	                                                         
139.11/72.53	          [cons](x1, x2) = [1] x2 + [2]                  
139.11/72.53	                                                         
139.11/72.53	                   [nil] = [0]                           
139.11/72.53	      
139.11/72.53	      The order satisfies the following ordering constraints:
139.11/72.53	      
139.11/72.53	               [le(0(), y)] =  [4]                    
139.11/72.53	                            >  [1]                    
139.11/72.53	                            =  [true()]               
139.11/72.53	                                                      
139.11/72.53	            [le(s(x), 0())] =  [4]                    
139.11/72.53	                            >  [1]                    
139.11/72.53	                            =  [false()]              
139.11/72.53	                                                      
139.11/72.53	           [le(s(x), s(y))] =  [4]                    
139.11/72.53	                            >= [4]                    
139.11/72.53	                            =  [le(x, y)]             
139.11/72.53	                                                      
139.11/72.53	                [int(x, y)] =  [1] y + [1] x + [5]    
139.11/72.53	                            >  [1] y + [1] x + [4]    
139.11/72.53	                            =  [if(le(x, y), x, y)]   
139.11/72.53	                                                      
139.11/72.53	         [if(true(), x, y)] =  [1] y + [1] x + [1]    
139.11/72.53	                            ?  [1] y + [1] x + [7]    
139.11/72.53	                            =  [cons(x, int(s(x), y))]
139.11/72.53	                                                      
139.11/72.53	        [if(false(), x, y)] =  [1] y + [1] x + [1]    
139.11/72.53	                            >  [0]                    
139.11/72.53	                            =  [nil()]                
139.11/72.53	                                                      
139.11/72.53	      
139.11/72.53	      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
139.11/72.53	      
139.11/72.53	      We are left with following problem, upon which TcT provides the
139.11/72.53	      certificate MAYBE.
139.11/72.53	      
139.11/72.53	      Strict Trs:
139.11/72.53	        { le(s(x), s(y)) -> le(x, y)
139.11/72.53	        , if(true(), x, y) -> cons(x, int(s(x), y)) }
139.11/72.53	      Weak Trs:
139.11/72.53	        { le(0(), y) -> true()
139.11/72.53	        , le(s(x), 0()) -> false()
139.11/72.53	        , int(x, y) -> if(le(x, y), x, y)
139.11/72.53	        , if(false(), x, y) -> nil() }
139.11/72.53	      Obligation:
139.11/72.53	        runtime complexity
139.11/72.53	      Answer:
139.11/72.53	        MAYBE
139.11/72.53	      
139.11/72.53	      None of the processors succeeded.
139.11/72.53	      
139.11/72.53	      Details of failed attempt(s):
139.11/72.53	      -----------------------------
139.11/72.53	      1) 'empty' failed due to the following reason:
139.11/72.53	         
139.11/72.53	         Empty strict component of the problem is NOT empty.
139.11/72.53	      
139.11/72.53	      2) 'With Problem ...' failed due to the following reason:
139.11/72.53	         
139.11/72.53	         None of the processors succeeded.
139.11/72.53	         
139.11/72.53	         Details of failed attempt(s):
139.11/72.53	         -----------------------------
139.11/72.53	         1) 'empty' failed due to the following reason:
139.11/72.53	            
139.11/72.53	            Empty strict component of the problem is NOT empty.
139.11/72.53	         
139.11/72.53	         2) 'Fastest' failed due to the following reason:
139.11/72.53	            
139.11/72.53	            None of the processors succeeded.
139.11/72.53	            
139.11/72.53	            Details of failed attempt(s):
139.11/72.53	            -----------------------------
139.11/72.53	            1) 'With Problem ...' failed due to the following reason:
139.11/72.53	               
139.11/72.53	               None of the processors succeeded.
139.11/72.53	               
139.11/72.53	               Details of failed attempt(s):
139.11/72.53	               -----------------------------
139.11/72.53	               1) 'empty' failed due to the following reason:
139.11/72.53	                  
139.11/72.53	                  Empty strict component of the problem is NOT empty.
139.11/72.53	               
139.11/72.53	               2) 'With Problem ...' failed due to the following reason:
139.11/72.53	                  
139.11/72.53	                  The weightgap principle applies (using the following nonconstant
139.11/72.53	                  growth matrix-interpretation)
139.11/72.53	                  
139.11/72.53	                  The following argument positions are usable:
139.11/72.53	                    Uargs(if) = {1}, Uargs(cons) = {2}
139.11/72.53	                  
139.11/72.53	                  TcT has computed the following matrix interpretation satisfying
139.11/72.53	                  not(EDA) and not(IDA(1)).
139.11/72.53	                  
139.11/72.53	                        [le](x1, x2) = [0 0] x1 + [0]
139.11/72.53	                                       [1 0]      [1]
139.11/72.53	                                                     
139.11/72.53	                                 [0] = [3]           
139.11/72.53	                                       [0]           
139.11/72.53	                                                     
139.11/72.53	                              [true] = [0]           
139.11/72.53	                                       [4]           
139.11/72.53	                                                     
139.11/72.53	                             [s](x1) = [0]           
139.11/72.53	                                       [0]           
139.11/72.53	                                                     
139.11/72.53	                             [false] = [0]           
139.11/72.53	                                       [0]           
139.11/72.53	                                                     
139.11/72.53	                       [int](x1, x2) = [1 0] x1 + [1]
139.11/72.53	                                       [0 0]      [4]
139.11/72.53	                                                     
139.11/72.53	                    [if](x1, x2, x3) = [1 1] x1 + [0]
139.11/72.53	                                       [0 0]      [0]
139.11/72.53	                                                     
139.11/72.53	                      [cons](x1, x2) = [1 0] x2 + [1]
139.11/72.53	                                       [0 0]      [0]
139.11/72.53	                                                     
139.11/72.53	                               [nil] = [0]           
139.11/72.53	                                       [0]           
139.11/72.53	                  
139.11/72.53	                  The order satisfies the following ordering constraints:
139.11/72.53	                  
139.11/72.53	                           [le(0(), y)] =  [0]                    
139.11/72.53	                                           [4]                    
139.11/72.53	                                        >= [0]                    
139.11/72.53	                                           [4]                    
139.11/72.53	                                        =  [true()]               
139.11/72.53	                                                                  
139.11/72.53	                        [le(s(x), 0())] =  [0]                    
139.11/72.53	                                           [1]                    
139.11/72.53	                                        >= [0]                    
139.11/72.53	                                           [0]                    
139.11/72.53	                                        =  [false()]              
139.11/72.53	                                                                  
139.11/72.53	                       [le(s(x), s(y))] =  [0]                    
139.11/72.53	                                           [1]                    
139.11/72.53	                                        ?  [0 0] x + [0]          
139.11/72.53	                                           [1 0]     [1]          
139.11/72.53	                                        =  [le(x, y)]             
139.11/72.53	                                                                  
139.11/72.53	                            [int(x, y)] =  [1 0] x + [1]          
139.11/72.53	                                           [0 0]     [4]          
139.11/72.53	                                        >= [1 0] x + [1]          
139.11/72.53	                                           [0 0]     [0]          
139.11/72.53	                                        =  [if(le(x, y), x, y)]   
139.11/72.53	                                                                  
139.11/72.53	                     [if(true(), x, y)] =  [4]                    
139.11/72.53	                                           [0]                    
139.11/72.53	                                        >  [2]                    
139.11/72.53	                                           [0]                    
139.11/72.53	                                        =  [cons(x, int(s(x), y))]
139.11/72.53	                                                                  
139.11/72.53	                    [if(false(), x, y)] =  [0]                    
139.11/72.53	                                           [0]                    
139.11/72.53	                                        >= [0]                    
139.11/72.53	                                           [0]                    
139.11/72.53	                                        =  [nil()]                
139.11/72.53	                                                                  
139.11/72.53	                  
139.11/72.53	                  Further, it can be verified that all rules not oriented are covered by the weightgap condition.
139.11/72.53	                  
139.11/72.53	                  We are left with following problem, upon which TcT provides the
139.11/72.53	                  certificate MAYBE.
139.11/72.53	                  
139.11/72.53	                  Strict Trs: { le(s(x), s(y)) -> le(x, y) }
139.11/72.53	                  Weak Trs:
139.11/72.53	                    { le(0(), y) -> true()
139.11/72.53	                    , le(s(x), 0()) -> false()
139.11/72.53	                    , int(x, y) -> if(le(x, y), x, y)
139.11/72.53	                    , if(true(), x, y) -> cons(x, int(s(x), y))
139.11/72.53	                    , if(false(), x, y) -> nil() }
139.11/72.53	                  Obligation:
139.11/72.53	                    runtime complexity
139.11/72.53	                  Answer:
139.11/72.53	                    MAYBE
139.11/72.53	                  
139.11/72.53	                  None of the processors succeeded.
139.11/72.53	                  
139.11/72.53	                  Details of failed attempt(s):
139.11/72.53	                  -----------------------------
139.11/72.53	                  1) 'empty' failed due to the following reason:
139.11/72.53	                     
139.11/72.53	                     Empty strict component of the problem is NOT empty.
139.11/72.53	                  
139.11/72.53	                  2) 'With Problem ...' failed due to the following reason:
139.11/72.53	                     
139.11/72.53	                     None of the processors succeeded.
139.11/72.53	                     
139.11/72.53	                     Details of failed attempt(s):
139.11/72.53	                     -----------------------------
139.11/72.53	                     1) 'empty' failed due to the following reason:
139.11/72.53	                        
139.11/72.53	                        Empty strict component of the problem is NOT empty.
139.11/72.53	                     
139.11/72.53	                     2) 'With Problem ...' failed due to the following reason:
139.11/72.53	                        
139.11/72.53	                        Empty strict component of the problem is NOT empty.
139.11/72.53	                     
139.11/72.53	                  
139.11/72.53	               
139.11/72.53	            
139.11/72.53	            2) 'With Problem ...' failed due to the following reason:
139.11/72.53	               
139.11/72.53	               None of the processors succeeded.
139.11/72.53	               
139.11/72.53	               Details of failed attempt(s):
139.11/72.53	               -----------------------------
139.11/72.53	               1) 'empty' failed due to the following reason:
139.11/72.53	                  
139.11/72.53	                  Empty strict component of the problem is NOT empty.
139.11/72.53	               
139.11/72.53	               2) 'With Problem ...' failed due to the following reason:
139.11/72.53	                  
139.11/72.53	                  Empty strict component of the problem is NOT empty.
139.11/72.53	               
139.11/72.53	            
139.11/72.53	         
139.11/72.53	      
139.11/72.53	   
139.11/72.53	   2) 'Best' failed due to the following reason:
139.11/72.53	      
139.11/72.53	      None of the processors succeeded.
139.11/72.53	      
139.11/72.53	      Details of failed attempt(s):
139.11/72.53	      -----------------------------
139.11/72.53	      1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
139.11/72.53	         following reason:
139.11/72.53	         
139.11/72.53	         The processor is inapplicable, reason:
139.11/72.53	           Processor only applicable for innermost runtime complexity analysis
139.11/72.53	      
139.11/72.53	      2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
139.11/72.53	         to the following reason:
139.11/72.53	         
139.11/72.53	         The processor is inapplicable, reason:
139.11/72.53	           Processor only applicable for innermost runtime complexity analysis
139.11/72.53	      
139.11/72.53	   
139.11/72.53	   3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
139.11/72.53	      failed due to the following reason:
139.11/72.53	      
139.11/72.53	      None of the processors succeeded.
139.11/72.53	      
139.11/72.53	      Details of failed attempt(s):
139.11/72.53	      -----------------------------
139.11/72.53	      1) 'Bounds with perSymbol-enrichment and initial automaton 'match''
139.11/72.53	         failed due to the following reason:
139.11/72.53	         
139.11/72.53	         match-boundness of the problem could not be verified.
139.11/72.53	      
139.11/72.53	      2) 'Bounds with minimal-enrichment and initial automaton 'match''
139.11/72.53	         failed due to the following reason:
139.11/72.53	         
139.11/72.53	         match-boundness of the problem could not be verified.
139.11/72.53	      
139.11/72.53	   
139.11/72.53	
139.11/72.53	2) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to
139.11/72.53	   the following reason:
139.11/72.53	   
139.11/72.53	   We add the following weak dependency pairs:
139.11/72.53	   
139.11/72.53	   Strict DPs:
139.11/72.53	     { le^#(0(), y) -> c_1()
139.11/72.53	     , le^#(s(x), 0()) -> c_2()
139.11/72.53	     , le^#(s(x), s(y)) -> c_3(le^#(x, y))
139.11/72.53	     , int^#(x, y) -> c_4(if^#(le(x, y), x, y))
139.11/72.53	     , if^#(true(), x, y) -> c_5(x, int^#(s(x), y))
139.11/72.53	     , if^#(false(), x, y) -> c_6() }
139.11/72.53	   
139.11/72.53	   and mark the set of starting terms.
139.11/72.53	   
139.11/72.53	   We are left with following problem, upon which TcT provides the
139.11/72.53	   certificate MAYBE.
139.11/72.53	   
139.11/72.53	   Strict DPs:
139.11/72.53	     { le^#(0(), y) -> c_1()
139.11/72.53	     , le^#(s(x), 0()) -> c_2()
139.11/72.53	     , le^#(s(x), s(y)) -> c_3(le^#(x, y))
139.11/72.53	     , int^#(x, y) -> c_4(if^#(le(x, y), x, y))
139.11/72.53	     , if^#(true(), x, y) -> c_5(x, int^#(s(x), y))
139.11/72.53	     , if^#(false(), x, y) -> c_6() }
139.11/72.53	   Strict Trs:
139.11/72.53	     { le(0(), y) -> true()
139.11/72.53	     , le(s(x), 0()) -> false()
139.11/72.53	     , le(s(x), s(y)) -> le(x, y)
139.11/72.53	     , int(x, y) -> if(le(x, y), x, y)
139.11/72.53	     , if(true(), x, y) -> cons(x, int(s(x), y))
139.11/72.53	     , if(false(), x, y) -> nil() }
139.11/72.53	   Obligation:
139.11/72.53	     runtime complexity
139.11/72.53	   Answer:
139.11/72.53	     MAYBE
139.11/72.53	   
139.11/72.53	   We estimate the number of application of {1,2,6} by applications of
139.11/72.53	   Pre({1,2,6}) = {3,4,5}. Here rules are labeled as follows:
139.11/72.53	   
139.11/72.53	     DPs:
139.11/72.53	       { 1: le^#(0(), y) -> c_1()
139.11/72.53	       , 2: le^#(s(x), 0()) -> c_2()
139.11/72.53	       , 3: le^#(s(x), s(y)) -> c_3(le^#(x, y))
139.11/72.53	       , 4: int^#(x, y) -> c_4(if^#(le(x, y), x, y))
139.11/72.53	       , 5: if^#(true(), x, y) -> c_5(x, int^#(s(x), y))
139.11/72.53	       , 6: if^#(false(), x, y) -> c_6() }
139.11/72.53	   
139.11/72.53	   We are left with following problem, upon which TcT provides the
139.11/72.53	   certificate MAYBE.
139.11/72.53	   
139.11/72.53	   Strict DPs:
139.11/72.53	     { le^#(s(x), s(y)) -> c_3(le^#(x, y))
139.11/72.53	     , int^#(x, y) -> c_4(if^#(le(x, y), x, y))
139.11/72.53	     , if^#(true(), x, y) -> c_5(x, int^#(s(x), y)) }
139.11/72.53	   Strict Trs:
139.11/72.53	     { le(0(), y) -> true()
139.11/72.53	     , le(s(x), 0()) -> false()
139.11/72.53	     , le(s(x), s(y)) -> le(x, y)
139.11/72.53	     , int(x, y) -> if(le(x, y), x, y)
139.11/72.53	     , if(true(), x, y) -> cons(x, int(s(x), y))
139.11/72.53	     , if(false(), x, y) -> nil() }
139.11/72.53	   Weak DPs:
139.11/72.53	     { le^#(0(), y) -> c_1()
139.11/72.53	     , le^#(s(x), 0()) -> c_2()
139.11/72.53	     , if^#(false(), x, y) -> c_6() }
139.11/72.53	   Obligation:
139.11/72.53	     runtime complexity
139.11/72.53	   Answer:
139.11/72.53	     MAYBE
139.11/72.53	   
139.11/72.53	   Empty strict component of the problem is NOT empty.
139.11/72.53	
139.11/72.53	
139.11/72.53	Arrrr..
139.22/72.69	EOF