MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { eq() -> eq()
  , eq() -> true()
  , eq() -> false()
  , inf(X) -> cons()
  , take(0(), X) -> nil()
  , take(s(), cons()) -> cons()
  , length(cons()) -> s()
  , length(nil()) -> 0() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

None of the processors succeeded.

Details of failed attempt(s):
-----------------------------
1) 'empty' failed due to the following reason:
   
   Empty strict component of the problem is NOT empty.

2) 'Best' failed due to the following reason:
   
   None of the processors succeeded.
   
   Details of failed attempt(s):
   -----------------------------
   1) 'WithProblem (timeout of 60 seconds)' failed due to the
      following reason:
      
      We add the following innermost weak dependency pairs:
      
      Strict DPs:
        { eq^#() -> c_1(eq^#())
        , eq^#() -> c_2()
        , eq^#() -> c_3()
        , inf^#(X) -> c_4()
        , take^#(0(), X) -> c_5()
        , take^#(s(), cons()) -> c_6()
        , length^#(cons()) -> c_7()
        , length^#(nil()) -> c_8() }
      
      and mark the set of starting terms.
      
      We are left with following problem, upon which TcT provides the
      certificate MAYBE.
      
      Strict DPs:
        { eq^#() -> c_1(eq^#())
        , eq^#() -> c_2()
        , eq^#() -> c_3()
        , inf^#(X) -> c_4()
        , take^#(0(), X) -> c_5()
        , take^#(s(), cons()) -> c_6()
        , length^#(cons()) -> c_7()
        , length^#(nil()) -> c_8() }
      Strict Trs:
        { eq() -> eq()
        , eq() -> true()
        , eq() -> false()
        , inf(X) -> cons()
        , take(0(), X) -> nil()
        , take(s(), cons()) -> cons()
        , length(cons()) -> s()
        , length(nil()) -> 0() }
      Obligation:
        innermost runtime complexity
      Answer:
        MAYBE
      
      No rule is usable, rules are removed from the input problem.
      
      We are left with following problem, upon which TcT provides the
      certificate MAYBE.
      
      Strict DPs:
        { eq^#() -> c_1(eq^#())
        , eq^#() -> c_2()
        , eq^#() -> c_3()
        , inf^#(X) -> c_4()
        , take^#(0(), X) -> c_5()
        , take^#(s(), cons()) -> c_6()
        , length^#(cons()) -> c_7()
        , length^#(nil()) -> c_8() }
      Obligation:
        innermost runtime complexity
      Answer:
        MAYBE
      
      The weightgap principle applies (using the following constant
      growth matrix-interpretation)
      
      The following argument positions are usable:
        Uargs(c_1) = {1}
      
      TcT has computed the following constructor-restricted matrix
      interpretation.
      
                  [cons] = [1]                      
                           [1]                      
                                                    
                     [0] = [2]                      
                           [2]                      
                                                    
                   [nil] = [2]                      
                           [2]                      
                                                    
                     [s] = [1]                      
                           [2]                      
                                                    
                  [eq^#] = [1]                      
                           [1]                      
                                                    
               [c_1](x1) = [1 0] x1 + [2]           
                           [0 1]      [2]           
                                                    
                   [c_2] = [0]                      
                           [1]                      
                                                    
                   [c_3] = [0]                      
                           [1]                      
                                                    
             [inf^#](x1) = [2]                      
                           [1]                      
                                                    
                   [c_4] = [1]                      
                           [1]                      
                                                    
        [take^#](x1, x2) = [1 1] x1 + [2 2] x2 + [0]
                           [1 1]      [2 2]      [0]
                                                    
                   [c_5] = [1]                      
                           [0]                      
                                                    
                   [c_6] = [2]                      
                           [1]                      
                                                    
          [length^#](x1) = [1 1] x1 + [2]           
                           [1 1]      [2]           
                                                    
                   [c_7] = [1]                      
                           [0]                      
                                                    
                   [c_8] = [1]                      
                           [1]                      
      
      The following symbols are considered usable
      
        {eq^#, inf^#, take^#, length^#}
      
      The order satisfies the following ordering constraints:
      
                     [eq^#()] = [1]          
                                [1]          
                              ? [3]          
                                [3]          
                              = [c_1(eq^#())]
                                             
                     [eq^#()] = [1]          
                                [1]          
                              > [0]          
                                [1]          
                              = [c_2()]      
                                             
                     [eq^#()] = [1]          
                                [1]          
                              > [0]          
                                [1]          
                              = [c_3()]      
                                             
                   [inf^#(X)] = [2]          
                                [1]          
                              > [1]          
                                [1]          
                              = [c_4()]      
                                             
             [take^#(0(), X)] = [2 2] X + [4]
                                [2 2]     [4]
                              > [1]          
                                [0]          
                              = [c_5()]      
                                             
        [take^#(s(), cons())] = [7]          
                                [7]          
                              > [2]          
                                [1]          
                              = [c_6()]      
                                             
           [length^#(cons())] = [4]          
                                [4]          
                              > [1]          
                                [0]          
                              = [c_7()]      
                                             
            [length^#(nil())] = [6]          
                                [6]          
                              > [1]          
                                [1]          
                              = [c_8()]      
                                             
      
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
      
      We are left with following problem, upon which TcT provides the
      certificate MAYBE.
      
      Strict DPs: { eq^#() -> c_1(eq^#()) }
      Weak DPs:
        { eq^#() -> c_2()
        , eq^#() -> c_3()
        , inf^#(X) -> c_4()
        , take^#(0(), X) -> c_5()
        , take^#(s(), cons()) -> c_6()
        , length^#(cons()) -> c_7()
        , length^#(nil()) -> c_8() }
      Obligation:
        innermost runtime complexity
      Answer:
        MAYBE
      
      The following weak DPs constitute a sub-graph of the DG that is
      closed under successors. The DPs are removed.
      
      { eq^#() -> c_2()
      , eq^#() -> c_3()
      , inf^#(X) -> c_4()
      , take^#(0(), X) -> c_5()
      , take^#(s(), cons()) -> c_6()
      , length^#(cons()) -> c_7()
      , length^#(nil()) -> c_8() }
      
      We are left with following problem, upon which TcT provides the
      certificate MAYBE.
      
      Strict DPs: { eq^#() -> c_1(eq^#()) }
      Obligation:
        innermost runtime complexity
      Answer:
        MAYBE
      
      None of the processors succeeded.
      
      Details of failed attempt(s):
      -----------------------------
      1) 'empty' failed due to the following reason:
         
         Empty strict component of the problem is NOT empty.
      
      2) 'WithProblem' failed due to the following reason:
         
         None of the processors succeeded.
         
         Details of failed attempt(s):
         -----------------------------
         1) 'empty' failed due to the following reason:
            
            Empty strict component of the problem is NOT empty.
         
         2) 'Fastest' failed due to the following reason:
            
            None of the processors succeeded.
            
            Details of failed attempt(s):
            -----------------------------
            1) 'Fastest (timeout of 5 seconds)' failed due to the following
               reason:
               
               Computation stopped due to timeout after 5.0 seconds.
            
            2) 'WithProblem' failed due to the following reason:
               
               None of the processors succeeded.
               
               Details of failed attempt(s):
               -----------------------------
               1) 'empty' failed due to the following reason:
                  
                  Empty strict component of the problem is NOT empty.
               
               2) 'Polynomial Path Order (PS)' failed due to the following reason:
                  
                  The input cannot be shown compatible
               
            
            3) 'Polynomial Path Order (PS)' failed due to the following reason:
               
               The input cannot be shown compatible
            
         
      
   
   2) 'Best' failed due to the following reason:
      
      None of the processors succeeded.
      
      Details of failed attempt(s):
      -----------------------------
      1) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed
         due to the following reason:
         
         Computation stopped due to timeout after 5.0 seconds.
      
      2) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)'
         failed due to the following reason:
         
         We use the processor 'Small Polynomial Path Order (PS,1-bounded)'
         to orient following rules strictly.
         
         Trs:
           { eq() -> true()
           , eq() -> false()
           , inf(X) -> cons()
           , take(0(), X) -> nil()
           , take(s(), cons()) -> cons()
           , length(cons()) -> s()
           , length(nil()) -> 0() }
         
         The induced complexity on above rules (modulo remaining rules) is
         YES(?,O(1)) . These rules are moved into the corresponding weak
         component(s).
         
         Sub-proof:
         ----------
           The input was oriented with the instance of 'Small Polynomial Path
           Order (PS,1-bounded)' as induced by the safe mapping
           
            safe(eq) = {}, safe(true) = {}, safe(false) = {}, safe(inf) = {},
            safe(cons) = {}, safe(take) = {}, safe(0) = {}, safe(nil) = {},
            safe(s) = {}, safe(length) = {}
           
           and precedence
           
            take > inf, length > inf, take ~ length .
           
           Following symbols are considered recursive:
           
            {}
           
           The recursion depth is 0.
           
           For your convenience, here are the satisfied ordering constraints:
           
                            eq() >= eq()   
                                           
                            eq() >  true() 
                                           
                            eq() >  false()
                                           
                         inf(X;) >  cons() 
                                           
                  take(0(),  X;) >  nil()  
                                           
             take(s(),  cons();) >  cons() 
                                           
                 length(cons();) >  s()    
                                           
                  length(nil();) >  0()    
                                           
         
         We return to the main proof.
         
         We are left with following problem, upon which TcT provides the
         certificate MAYBE.
         
         Strict Trs: { eq() -> eq() }
         Weak Trs:
           { eq() -> true()
           , eq() -> false()
           , inf(X) -> cons()
           , take(0(), X) -> nil()
           , take(s(), cons()) -> cons()
           , length(cons()) -> s()
           , length(nil()) -> 0() }
         Obligation:
           innermost runtime complexity
         Answer:
           MAYBE
         
         None of the processors succeeded.
         
         Details of failed attempt(s):
         -----------------------------
         1) 'empty' failed due to the following reason:
            
            Empty strict component of the problem is NOT empty.
         
         2) 'WithProblem' failed due to the following reason:
            
            None of the processors succeeded.
            
            Details of failed attempt(s):
            -----------------------------
            1) 'empty' failed due to the following reason:
               
               Empty strict component of the problem is NOT empty.
            
            2) 'Fastest' failed due to the following reason:
               
               None of the processors succeeded.
               
               Details of failed attempt(s):
               -----------------------------
               1) 'WithProblem' failed due to the following reason:
                  
                  None of the processors succeeded.
                  
                  Details of failed attempt(s):
                  -----------------------------
                  1) 'empty' failed due to the following reason:
                     
                     Empty strict component of the problem is NOT empty.
                  
                  2) 'WithProblem' failed due to the following reason:
                     
                     None of the processors succeeded.
                     
                     Details of failed attempt(s):
                     -----------------------------
                     1) 'empty' failed due to the following reason:
                        
                        Empty strict component of the problem is NOT empty.
                     
                     2) 'WithProblem' failed due to the following reason:
                        
                        None of the processors succeeded.
                        
                        Details of failed attempt(s):
                        -----------------------------
                        1) 'empty' failed due to the following reason:
                           
                           Empty strict component of the problem is NOT empty.
                        
                        2) 'WithProblem' failed due to the following reason:
                           
                           Empty strict component of the problem is NOT empty.
                        
                     
                  
               
               2) 'WithProblem' failed due to the following reason:
                  
                  None of the processors succeeded.
                  
                  Details of failed attempt(s):
                  -----------------------------
                  1) 'empty' failed due to the following reason:
                     
                     Empty strict component of the problem is NOT empty.
                  
                  2) 'WithProblem' failed due to the following reason:
                     
                     Empty strict component of the problem is NOT empty.
                  
               
            
         
      
      3) 'Best' failed due to the following reason:
         
         None of the processors succeeded.
         
         Details of failed attempt(s):
         -----------------------------
         1) 'bsearch-popstar (timeout of 60 seconds)' failed due to the
            following reason:
            
            The input cannot be shown compatible
         
         2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due
            to the following reason:
            
            The input cannot be shown compatible
         
      
   


Arrrr..