MAYBE

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

Strict Trs:
  { from(X) -> cons(X)
  , length() -> 0()
  , length() -> s(length1())
  , length1() -> length() }
Obligation:
  runtime complexity
Answer:
  MAYBE

The input is overlay and right-linear. Switching to innermost
rewriting.

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

Strict Trs:
  { from(X) -> cons(X)
  , length() -> 0()
  , length() -> s(length1())
  , length1() -> length() }
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) 'Best' failed due to the following reason:
      
      None of the processors succeeded.
      
      Details of failed attempt(s):
      -----------------------------
      1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)'
         failed due to the following reason:
         
         The weightgap principle applies (using the following nonconstant
         growth matrix-interpretation)
         
         The following argument positions are usable:
           Uargs(s) = {1}
         
         TcT has computed the following matrix interpretation satisfying
         not(EDA) and not(IDA(1)).
         
           [from](x1) = [1] x1 + [7]
                                    
           [cons](x1) = [1] x1 + [3]
                                    
             [length] = [6]         
                                    
                  [0] = [5]         
                                    
              [s](x1) = [1] x1 + [7]
                                    
            [length1] = [7]         
         
         The following symbols are considered usable
         
           {from, length, length1}
         
         The order satisfies the following ordering constraints:
         
             [from(X)] = [1] X + [7]   
                       > [1] X + [3]   
                       = [cons(X)]     
                                       
            [length()] = [6]           
                       > [5]           
                       = [0()]         
                                       
            [length()] = [6]           
                       ? [14]          
                       = [s(length1())]
                                       
           [length1()] = [7]           
                       > [6]           
                       = [length()]    
                                       
         
         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 Trs: { length() -> s(length1()) }
         Weak Trs:
           { from(X) -> cons(X)
           , length() -> 0()
           , length1() -> length() }
         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.
                  
               
            
         
      
      2) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed
         due to the following reason:
         
         Computation stopped due to timeout after 5.0 seconds.
      
      3) 'Best' failed due to the following reason:
         
         None of the processors succeeded.
         
         Details of failed attempt(s):
         -----------------------------
         1) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due
            to the following reason:
            
            The input cannot be shown compatible
         
         2) 'bsearch-popstar (timeout of 60 seconds)' failed due to the
            following reason:
            
            The input cannot be shown compatible
         
      
   
   2) 'WithProblem (timeout of 60 seconds)' failed due to the
      following reason:
      
      We add the following innermost weak dependency pairs:
      
      Strict DPs:
        { from^#(X) -> c_1()
        , length^#() -> c_2()
        , length^#() -> c_3(length1^#())
        , length1^#() -> c_4(length^#()) }
      
      and mark the set of starting terms.
      
      We are left with following problem, upon which TcT provides the
      certificate MAYBE.
      
      Strict DPs:
        { from^#(X) -> c_1()
        , length^#() -> c_2()
        , length^#() -> c_3(length1^#())
        , length1^#() -> c_4(length^#()) }
      Strict Trs:
        { from(X) -> cons(X)
        , length() -> 0()
        , length() -> s(length1())
        , length1() -> length() }
      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:
        { from^#(X) -> c_1()
        , length^#() -> c_2()
        , length^#() -> c_3(length1^#())
        , length1^#() -> c_4(length^#()) }
      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_3) = {1}, Uargs(c_4) = {1}
      
      TcT has computed the following constructor-restricted matrix
      interpretation.
      
        [from^#](x1) = [2]           
                       [1]           
                                     
               [c_1] = [1]           
                       [1]           
                                     
          [length^#] = [1]           
                       [1]           
                                     
               [c_2] = [0]           
                       [1]           
                                     
           [c_3](x1) = [1 0] x1 + [2]
                       [0 1]      [2]
                                     
         [length1^#] = [1]           
                       [1]           
                                     
           [c_4](x1) = [1 0] x1 + [2]
                       [0 1]      [2]
      
      The following symbols are considered usable
      
        {from^#, length^#, length1^#}
      
      The order satisfies the following ordering constraints:
      
          [from^#(X)] = [2]               
                        [1]               
                      > [1]               
                        [1]               
                      = [c_1()]           
                                          
         [length^#()] = [1]               
                        [1]               
                      > [0]               
                        [1]               
                      = [c_2()]           
                                          
         [length^#()] = [1]               
                        [1]               
                      ? [3]               
                        [3]               
                      = [c_3(length1^#())]
                                          
        [length1^#()] = [1]               
                        [1]               
                      ? [3]               
                        [3]               
                      = [c_4(length^#())] 
                                          
      
      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:
        { length^#() -> c_3(length1^#())
        , length1^#() -> c_4(length^#()) }
      Weak DPs:
        { from^#(X) -> c_1()
        , length^#() -> c_2() }
      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.
      
      { from^#(X) -> c_1()
      , length^#() -> c_2() }
      
      We are left with following problem, upon which TcT provides the
      certificate MAYBE.
      
      Strict DPs:
        { length^#() -> c_3(length1^#())
        , length1^#() -> c_4(length^#()) }
      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) 'Polynomial Path Order (PS)' failed due to the following reason:
                  
                  The input cannot be shown compatible
               
            
            2) 'Fastest (timeout of 5 seconds)' failed due to the following
               reason:
               
               Computation stopped due to timeout after 5.0 seconds.
            
            3) 'Polynomial Path Order (PS)' failed due to the following reason:
               
               The input cannot be shown compatible
            
         
      
   


Arrrr..