MAYBE
37.78/11.93	MAYBE
37.78/11.93	
37.78/11.93	We are left with following problem, upon which TcT provides the
37.78/11.93	certificate MAYBE.
37.78/11.93	
37.78/11.93	Strict Trs:
37.78/11.93	  { fib(0()) -> 0()
37.78/11.93	  , fib(s(0())) -> s(0())
37.78/11.93	  , fib(s(s(x))) -> +(fib(s(x)), fib(x)) }
37.78/11.93	Obligation:
37.78/11.93	  innermost runtime complexity
37.78/11.93	Answer:
37.78/11.93	  MAYBE
37.78/11.93	
37.78/11.93	None of the processors succeeded.
37.78/11.93	
37.78/11.93	Details of failed attempt(s):
37.78/11.93	-----------------------------
37.78/11.93	1) 'empty' failed due to the following reason:
37.78/11.93	   
37.78/11.93	   Empty strict component of the problem is NOT empty.
37.78/11.93	
37.78/11.93	2) 'Best' failed due to the following reason:
37.78/11.93	   
37.78/11.93	   None of the processors succeeded.
37.78/11.93	   
37.78/11.93	   Details of failed attempt(s):
37.78/11.93	   -----------------------------
37.78/11.93	   1) 'With Problem ... (timeout of 297 seconds)' failed due to the
37.78/11.93	      following reason:
37.78/11.93	      
37.78/11.93	      We add the following weak dependency pairs:
37.78/11.93	      
37.78/11.93	      Strict DPs:
37.78/11.93	        { fib^#(0()) -> c_1()
37.78/11.93	        , fib^#(s(0())) -> c_2()
37.78/11.93	        , fib^#(s(s(x))) -> c_3(fib^#(s(x)), fib^#(x)) }
37.78/11.93	      
37.78/11.93	      and mark the set of starting terms.
37.78/11.93	      
37.78/11.93	      We are left with following problem, upon which TcT provides the
37.78/11.93	      certificate MAYBE.
37.78/11.93	      
37.78/11.93	      Strict DPs:
37.78/11.93	        { fib^#(0()) -> c_1()
37.78/11.93	        , fib^#(s(0())) -> c_2()
37.78/11.93	        , fib^#(s(s(x))) -> c_3(fib^#(s(x)), fib^#(x)) }
37.78/11.93	      Strict Trs:
37.78/11.93	        { fib(0()) -> 0()
37.78/11.93	        , fib(s(0())) -> s(0())
37.78/11.93	        , fib(s(s(x))) -> +(fib(s(x)), fib(x)) }
37.78/11.93	      Obligation:
37.78/11.93	        innermost runtime complexity
37.78/11.93	      Answer:
37.78/11.93	        MAYBE
37.78/11.93	      
37.78/11.93	      No rule is usable, rules are removed from the input problem.
37.78/11.93	      
37.78/11.93	      We are left with following problem, upon which TcT provides the
37.78/11.93	      certificate MAYBE.
37.78/11.93	      
37.78/11.93	      Strict DPs:
37.78/11.93	        { fib^#(0()) -> c_1()
37.78/11.93	        , fib^#(s(0())) -> c_2()
37.78/11.93	        , fib^#(s(s(x))) -> c_3(fib^#(s(x)), fib^#(x)) }
37.78/11.93	      Obligation:
37.78/11.93	        innermost runtime complexity
37.78/11.93	      Answer:
37.78/11.93	        MAYBE
37.78/11.93	      
37.78/11.93	      The weightgap principle applies (using the following constant
37.78/11.93	      growth matrix-interpretation)
37.78/11.93	      
37.78/11.93	      The following argument positions are usable:
37.78/11.93	        Uargs(c_3) = {1, 2}
37.78/11.93	      
37.78/11.93	      TcT has computed the following constructor-restricted matrix
37.78/11.93	      interpretation.
37.78/11.93	      
37.78/11.93	                  [0] = [0]                      
37.78/11.93	                        [0]                      
37.78/11.93	                                                 
37.78/11.93	              [s](x1) = [0]                      
37.78/11.93	                        [0]                      
37.78/11.93	                                                 
37.78/11.93	          [fib^#](x1) = [1]                      
37.78/11.93	                        [0]                      
37.78/11.93	                                                 
37.78/11.93	                [c_1] = [0]                      
37.78/11.93	                        [0]                      
37.78/11.93	                                                 
37.78/11.93	                [c_2] = [0]                      
37.78/11.93	                        [0]                      
37.78/11.93	                                                 
37.78/11.93	        [c_3](x1, x2) = [1 0] x1 + [1 0] x2 + [1]
37.78/11.93	                        [0 1]      [0 1]      [2]
37.78/11.93	      
37.78/11.93	      The order satisfies the following ordering constraints:
37.78/11.93	      
37.78/11.93	            [fib^#(0())] = [1]                         
37.78/11.93	                           [0]                         
37.78/11.93	                         > [0]                         
37.78/11.93	                           [0]                         
37.78/11.93	                         = [c_1()]                     
37.78/11.93	                                                       
37.78/11.93	         [fib^#(s(0()))] = [1]                         
37.78/11.93	                           [0]                         
37.78/11.93	                         > [0]                         
37.78/11.93	                           [0]                         
37.78/11.93	                         = [c_2()]                     
37.78/11.93	                                                       
37.78/11.93	        [fib^#(s(s(x)))] = [1]                         
37.78/11.93	                           [0]                         
37.78/11.93	                         ? [3]                         
37.78/11.93	                           [2]                         
37.78/11.93	                         = [c_3(fib^#(s(x)), fib^#(x))]
37.78/11.93	                                                       
37.78/11.93	      
37.78/11.93	      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
37.78/11.93	      
37.78/11.93	      We are left with following problem, upon which TcT provides the
37.78/11.93	      certificate MAYBE.
37.78/11.93	      
37.78/11.93	      Strict DPs: { fib^#(s(s(x))) -> c_3(fib^#(s(x)), fib^#(x)) }
37.78/11.93	      Weak DPs:
37.78/11.93	        { fib^#(0()) -> c_1()
37.78/11.93	        , fib^#(s(0())) -> c_2() }
37.78/11.93	      Obligation:
37.78/11.93	        innermost runtime complexity
37.78/11.93	      Answer:
37.78/11.93	        MAYBE
37.78/11.93	      
37.78/11.93	      The following weak DPs constitute a sub-graph of the DG that is
37.78/11.93	      closed under successors. The DPs are removed.
37.78/11.93	      
37.78/11.93	      { fib^#(0()) -> c_1()
37.78/11.93	      , fib^#(s(0())) -> c_2() }
37.78/11.93	      
37.78/11.93	      We are left with following problem, upon which TcT provides the
37.78/11.93	      certificate MAYBE.
37.78/11.93	      
37.78/11.93	      Strict DPs: { fib^#(s(s(x))) -> c_3(fib^#(s(x)), fib^#(x)) }
37.78/11.93	      Obligation:
37.78/11.93	        innermost runtime complexity
37.78/11.93	      Answer:
37.78/11.93	        MAYBE
37.78/11.93	      
37.78/11.93	      None of the processors succeeded.
37.78/11.93	      
37.78/11.93	      Details of failed attempt(s):
37.78/11.93	      -----------------------------
37.78/11.93	      1) 'empty' failed due to the following reason:
37.78/11.93	         
37.78/11.93	         Empty strict component of the problem is NOT empty.
37.78/11.93	      
37.78/11.93	      2) 'With Problem ...' failed due to the following reason:
37.78/11.93	         
37.78/11.93	         None of the processors succeeded.
37.78/11.93	         
37.78/11.93	         Details of failed attempt(s):
37.78/11.93	         -----------------------------
37.78/11.93	         1) 'empty' failed due to the following reason:
37.78/11.93	            
37.78/11.93	            Empty strict component of the problem is NOT empty.
37.78/11.93	         
37.78/11.93	         2) 'Fastest' failed due to the following reason:
37.78/11.93	            
37.78/11.93	            None of the processors succeeded.
37.78/11.93	            
37.78/11.93	            Details of failed attempt(s):
37.78/11.93	            -----------------------------
37.78/11.93	            1) 'With Problem ...' failed due to the following reason:
37.78/11.93	               
37.78/11.93	               None of the processors succeeded.
37.78/11.93	               
37.78/11.93	               Details of failed attempt(s):
37.78/11.93	               -----------------------------
37.78/11.93	               1) 'empty' failed due to the following reason:
37.78/11.93	                  
37.78/11.93	                  Empty strict component of the problem is NOT empty.
37.78/11.93	               
37.78/11.93	               2) 'Polynomial Path Order (PS)' failed due to the following reason:
37.78/11.93	                  
37.78/11.93	                  The input cannot be shown compatible
37.78/11.93	               
37.78/11.93	            
37.78/11.93	            2) 'Polynomial Path Order (PS)' failed due to the following reason:
37.78/11.93	               
37.78/11.93	               The input cannot be shown compatible
37.78/11.93	            
37.78/11.93	            3) 'Fastest (timeout of 24 seconds)' failed due to the following
37.78/11.93	               reason:
37.78/11.93	               
37.78/11.93	               None of the processors succeeded.
37.78/11.93	               
37.78/11.93	               Details of failed attempt(s):
37.78/11.93	               -----------------------------
37.78/11.93	               1) 'Bounds with perSymbol-enrichment and initial automaton 'match''
37.78/11.93	                  failed due to the following reason:
37.78/11.93	                  
37.78/11.93	                  match-boundness of the problem could not be verified.
37.78/11.93	               
37.78/11.93	               2) 'Bounds with minimal-enrichment and initial automaton 'match''
37.78/11.93	                  failed due to the following reason:
37.78/11.93	                  
37.78/11.93	                  match-boundness of the problem could not be verified.
37.78/11.93	               
37.78/11.93	            
37.78/11.93	         
37.78/11.93	      
37.78/11.93	   
37.78/11.93	   2) 'Best' failed due to the following reason:
37.78/11.93	      
37.78/11.93	      None of the processors succeeded.
37.78/11.93	      
37.78/11.93	      Details of failed attempt(s):
37.78/11.93	      -----------------------------
37.78/11.93	      1) 'With Problem ... (timeout of 148 seconds) (timeout of 297
37.78/11.93	         seconds)' failed due to the following reason:
37.78/11.93	         
37.78/11.93	         The weightgap principle applies (using the following nonconstant
37.78/11.93	         growth matrix-interpretation)
37.78/11.93	         
37.78/11.93	         The following argument positions are usable:
37.78/11.93	           Uargs(+) = {1, 2}
37.78/11.93	         
37.78/11.93	         TcT has computed the following matrix interpretation satisfying
37.78/11.93	         not(EDA) and not(IDA(1)).
37.78/11.93	         
37.78/11.93	             [fib](x1) = [7]                  
37.78/11.93	                                              
37.78/11.93	                   [0] = [3]                  
37.78/11.93	                                              
37.78/11.93	               [s](x1) = [1] x1 + [3]         
37.78/11.93	                                              
37.78/11.93	           [+](x1, x2) = [1] x1 + [1] x2 + [0]
37.78/11.93	         
37.78/11.93	         The order satisfies the following ordering constraints:
37.78/11.93	         
37.78/11.93	               [fib(0())] = [7]                   
37.78/11.93	                          > [3]                   
37.78/11.93	                          = [0()]                 
37.78/11.93	                                                  
37.78/11.93	            [fib(s(0()))] = [7]                   
37.78/11.93	                          > [6]                   
37.78/11.93	                          = [s(0())]              
37.78/11.93	                                                  
37.78/11.93	           [fib(s(s(x)))] = [7]                   
37.78/11.93	                          ? [14]                  
37.78/11.93	                          = [+(fib(s(x)), fib(x))]
37.78/11.93	                                                  
37.78/11.93	         
37.78/11.93	         Further, it can be verified that all rules not oriented are covered by the weightgap condition.
37.78/11.93	         
37.78/11.93	         We are left with following problem, upon which TcT provides the
37.78/11.93	         certificate MAYBE.
37.78/11.93	         
37.78/11.93	         Strict Trs: { fib(s(s(x))) -> +(fib(s(x)), fib(x)) }
37.78/11.93	         Weak Trs:
37.78/11.93	           { fib(0()) -> 0()
37.78/11.93	           , fib(s(0())) -> s(0()) }
37.78/11.93	         Obligation:
37.78/11.93	           innermost runtime complexity
37.78/11.93	         Answer:
37.78/11.93	           MAYBE
37.78/11.93	         
37.78/11.93	         None of the processors succeeded.
37.78/11.93	         
37.78/11.93	         Details of failed attempt(s):
37.78/11.93	         -----------------------------
37.78/11.93	         1) 'empty' failed due to the following reason:
37.78/11.93	            
37.78/11.93	            Empty strict component of the problem is NOT empty.
37.78/11.93	         
37.78/11.93	         2) 'With Problem ...' failed due to the following reason:
37.78/11.93	            
37.78/11.93	            None of the processors succeeded.
37.78/11.93	            
37.78/11.93	            Details of failed attempt(s):
37.78/11.93	            -----------------------------
37.78/11.93	            1) 'empty' failed due to the following reason:
37.78/11.93	               
37.78/11.93	               Empty strict component of the problem is NOT empty.
37.78/11.93	            
37.78/11.93	            2) 'Fastest' failed due to the following reason:
37.78/11.93	               
37.78/11.93	               None of the processors succeeded.
37.78/11.93	               
37.78/11.93	               Details of failed attempt(s):
37.78/11.93	               -----------------------------
37.78/11.93	               1) 'With Problem ...' failed due to the following reason:
37.78/11.93	                  
37.78/11.93	                  None of the processors succeeded.
37.78/11.93	                  
37.78/11.93	                  Details of failed attempt(s):
37.78/11.93	                  -----------------------------
37.78/11.93	                  1) 'empty' failed due to the following reason:
37.78/11.93	                     
37.78/11.93	                     Empty strict component of the problem is NOT empty.
37.78/11.93	                  
37.78/11.93	                  2) 'With Problem ...' failed due to the following reason:
37.78/11.93	                     
37.78/11.93	                     None of the processors succeeded.
37.78/11.93	                     
37.78/11.93	                     Details of failed attempt(s):
37.78/11.93	                     -----------------------------
37.78/11.93	                     1) 'empty' failed due to the following reason:
37.78/11.93	                        
37.78/11.93	                        Empty strict component of the problem is NOT empty.
37.78/11.93	                     
37.78/11.93	                     2) 'With Problem ...' failed due to the following reason:
37.78/11.93	                        
37.78/11.93	                        None of the processors succeeded.
37.78/11.93	                        
37.78/11.93	                        Details of failed attempt(s):
37.78/11.93	                        -----------------------------
37.78/11.93	                        1) 'empty' failed due to the following reason:
37.78/11.93	                           
37.78/11.93	                           Empty strict component of the problem is NOT empty.
37.78/11.93	                        
37.78/11.93	                        2) 'With Problem ...' failed due to the following reason:
37.78/11.93	                           
37.78/11.93	                           Empty strict component of the problem is NOT empty.
37.78/11.93	                        
37.78/11.93	                     
37.78/11.93	                  
37.78/11.93	               
37.78/11.93	               2) 'With Problem ...' failed due to the following reason:
37.78/11.93	                  
37.78/11.93	                  None of the processors succeeded.
37.78/11.93	                  
37.78/11.93	                  Details of failed attempt(s):
37.78/11.93	                  -----------------------------
37.78/11.93	                  1) 'empty' failed due to the following reason:
37.78/11.93	                     
37.78/11.93	                     Empty strict component of the problem is NOT empty.
37.78/11.93	                  
37.78/11.93	                  2) 'With Problem ...' failed due to the following reason:
37.78/11.93	                     
37.78/11.93	                     Empty strict component of the problem is NOT empty.
37.78/11.93	                  
37.78/11.93	               
37.78/11.93	            
37.78/11.93	         
37.78/11.93	      
37.78/11.93	      2) 'Best' failed due to the following reason:
37.78/11.93	         
37.78/11.93	         None of the processors succeeded.
37.78/11.93	         
37.78/11.93	         Details of failed attempt(s):
37.78/11.93	         -----------------------------
37.78/11.93	         1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due
37.78/11.93	            to the following reason:
37.78/11.93	            
37.78/11.93	            The input cannot be shown compatible
37.78/11.93	         
37.78/11.93	         2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the
37.78/11.93	            following reason:
37.78/11.93	            
37.78/11.93	            The input cannot be shown compatible
37.78/11.93	         
37.78/11.93	      
37.78/11.93	      3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)'
37.78/11.93	         failed due to the following reason:
37.78/11.93	         
37.78/11.93	         None of the processors succeeded.
37.78/11.93	         
37.78/11.93	         Details of failed attempt(s):
37.78/11.93	         -----------------------------
37.78/11.93	         1) 'Bounds with minimal-enrichment and initial automaton 'match''
37.78/11.93	            failed due to the following reason:
37.78/11.93	            
37.78/11.93	            match-boundness of the problem could not be verified.
37.78/11.93	         
37.78/11.93	         2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
37.78/11.93	            failed due to the following reason:
37.78/11.93	            
37.78/11.93	            match-boundness of the problem could not be verified.
37.78/11.93	         
37.78/11.93	      
37.78/11.93	   
37.78/11.93	
37.78/11.93	
37.78/11.93	Arrrr..
37.78/11.96	EOF