WORST_CASE(?,O(n^3))
* Step 1: NaturalMI WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict TRS:
            a__from(X) -> cons(mark(X),from(s(X)))
            a__from(X) -> from(X)
            a__length(X) -> length(X)
            a__length(cons(X,Y)) -> s(a__length1(Y))
            a__length(nil()) -> 0()
            a__length1(X) -> a__length(X)
            a__length1(X) -> length1(X)
            mark(0()) -> 0()
            mark(cons(X1,X2)) -> cons(mark(X1),X2)
            mark(from(X)) -> a__from(mark(X))
            mark(length(X)) -> a__length(X)
            mark(length1(X)) -> a__length1(X)
            mark(nil()) -> nil()
            mark(s(X)) -> s(mark(X))
        - Signature:
            {a__from/1,a__length/1,a__length1/1,mark/1} / {0/0,cons/2,from/1,length/1,length1/1,nil/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a__from,a__length,a__length1,mark} and constructors {0
            ,cons,from,length,length1,nil,s}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(a__from) = {1},
          uargs(cons) = {1},
          uargs(s) = {1}
        
        Following symbols are considered usable:
          {a__from,a__length,a__length1,mark}
        TcT has computed the following interpretation:
                   p(0) = [0]         
             p(a__from) = [1] x1 + [4]
           p(a__length) = [2]         
          p(a__length1) = [2]         
                p(cons) = [1] x1 + [1]
                p(from) = [1] x1 + [4]
              p(length) = [1]         
             p(length1) = [1]         
                p(mark) = [1] x1 + [1]
                 p(nil) = [1]         
                   p(s) = [1] x1 + [0]
        
        Following rules are strictly oriented:
              a__from(X) = [1] X + [4]             
                         > [1] X + [2]             
                         = cons(mark(X),from(s(X)))
        
            a__length(X) = [2]                     
                         > [1]                     
                         = length(X)               
        
        a__length(nil()) = [2]                     
                         > [0]                     
                         = 0()                     
        
           a__length1(X) = [2]                     
                         > [1]                     
                         = length1(X)              
        
               mark(0()) = [1]                     
                         > [0]                     
                         = 0()                     
        
             mark(nil()) = [2]                     
                         > [1]                     
                         = nil()                   
        
        
        Following rules are (at-least) weakly oriented:
                  a__from(X) =  [1] X + [4]      
                             >= [1] X + [4]      
                             =  from(X)          
        
        a__length(cons(X,Y)) =  [2]              
                             >= [2]              
                             =  s(a__length1(Y)) 
        
               a__length1(X) =  [2]              
                             >= [2]              
                             =  a__length(X)     
        
           mark(cons(X1,X2)) =  [1] X1 + [2]     
                             >= [1] X1 + [2]     
                             =  cons(mark(X1),X2)
        
               mark(from(X)) =  [1] X + [5]      
                             >= [1] X + [5]      
                             =  a__from(mark(X)) 
        
             mark(length(X)) =  [2]              
                             >= [2]              
                             =  a__length(X)     
        
            mark(length1(X)) =  [2]              
                             >= [2]              
                             =  a__length1(X)    
        
                  mark(s(X)) =  [1] X + [1]      
                             >= [1] X + [1]      
                             =  s(mark(X))       
        
* Step 2: NaturalMI WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict TRS:
            a__from(X) -> from(X)
            a__length(cons(X,Y)) -> s(a__length1(Y))
            a__length1(X) -> a__length(X)
            mark(cons(X1,X2)) -> cons(mark(X1),X2)
            mark(from(X)) -> a__from(mark(X))
            mark(length(X)) -> a__length(X)
            mark(length1(X)) -> a__length1(X)
            mark(s(X)) -> s(mark(X))
        - Weak TRS:
            a__from(X) -> cons(mark(X),from(s(X)))
            a__length(X) -> length(X)
            a__length(nil()) -> 0()
            a__length1(X) -> length1(X)
            mark(0()) -> 0()
            mark(nil()) -> nil()
        - Signature:
            {a__from/1,a__length/1,a__length1/1,mark/1} / {0/0,cons/2,from/1,length/1,length1/1,nil/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a__from,a__length,a__length1,mark} and constructors {0
            ,cons,from,length,length1,nil,s}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(a__from) = {1},
          uargs(cons) = {1},
          uargs(s) = {1}
        
        Following symbols are considered usable:
          {a__from,a__length,a__length1,mark}
        TcT has computed the following interpretation:
                   p(0) = [0]         
             p(a__from) = [1] x1 + [8]
           p(a__length) = [4]         
          p(a__length1) = [4]         
                p(cons) = [1] x1 + [0]
                p(from) = [1] x1 + [8]
              p(length) = [4]         
             p(length1) = [4]         
                p(mark) = [1] x1 + [8]
                 p(nil) = [0]         
                   p(s) = [1] x1 + [0]
        
        Following rules are strictly oriented:
         mark(length(X)) = [12]         
                         > [4]          
                         = a__length(X) 
        
        mark(length1(X)) = [12]         
                         > [4]          
                         = a__length1(X)
        
        
        Following rules are (at-least) weakly oriented:
                  a__from(X) =  [1] X + [8]             
                             >= [1] X + [8]             
                             =  cons(mark(X),from(s(X)))
        
                  a__from(X) =  [1] X + [8]             
                             >= [1] X + [8]             
                             =  from(X)                 
        
                a__length(X) =  [4]                     
                             >= [4]                     
                             =  length(X)               
        
        a__length(cons(X,Y)) =  [4]                     
                             >= [4]                     
                             =  s(a__length1(Y))        
        
            a__length(nil()) =  [4]                     
                             >= [0]                     
                             =  0()                     
        
               a__length1(X) =  [4]                     
                             >= [4]                     
                             =  a__length(X)            
        
               a__length1(X) =  [4]                     
                             >= [4]                     
                             =  length1(X)              
        
                   mark(0()) =  [8]                     
                             >= [0]                     
                             =  0()                     
        
           mark(cons(X1,X2)) =  [1] X1 + [8]            
                             >= [1] X1 + [8]            
                             =  cons(mark(X1),X2)       
        
               mark(from(X)) =  [1] X + [16]            
                             >= [1] X + [16]            
                             =  a__from(mark(X))        
        
                 mark(nil()) =  [8]                     
                             >= [0]                     
                             =  nil()                   
        
                  mark(s(X)) =  [1] X + [8]             
                             >= [1] X + [8]             
                             =  s(mark(X))              
        
* Step 3: Ara WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict TRS:
            a__from(X) -> from(X)
            a__length(cons(X,Y)) -> s(a__length1(Y))
            a__length1(X) -> a__length(X)
            mark(cons(X1,X2)) -> cons(mark(X1),X2)
            mark(from(X)) -> a__from(mark(X))
            mark(s(X)) -> s(mark(X))
        - Weak TRS:
            a__from(X) -> cons(mark(X),from(s(X)))
            a__length(X) -> length(X)
            a__length(nil()) -> 0()
            a__length1(X) -> length1(X)
            mark(0()) -> 0()
            mark(length(X)) -> a__length(X)
            mark(length1(X)) -> a__length1(X)
            mark(nil()) -> nil()
        - Signature:
            {a__from/1,a__length/1,a__length1/1,mark/1} / {0/0,cons/2,from/1,length/1,length1/1,nil/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a__from,a__length,a__length1,mark} and constructors {0
            ,cons,from,length,length1,nil,s}
    + Applied Processor:
        Ara {araHeuristics = NoHeuristics, minDegree = 2, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
    + Details:
        Signatures used:
        ----------------
          0 :: [] -(0)-> "A"(0, 13)
          0 :: [] -(0)-> "A"(5, 15)
          0 :: [] -(0)-> "A"(6, 15)
          a__from :: ["A"(0, 13)] -(13)-> "A"(2, 13)
          a__length :: ["A"(13, 0)] -(0)-> "A"(3, 13)
          a__length1 :: ["A"(13, 0)] -(0)-> "A"(3, 13)
          cons :: ["A"(0, 0) x "A"(13, 0)] -(13)-> "A"(13, 0)
          cons :: ["A"(0, 13) x "A"(0, 0)] -(0)-> "A"(0, 13)
          cons :: ["A"(0, 13) x "A"(6, 0)] -(6)-> "A"(6, 13)
          from :: ["A"(0, 13)] -(13)-> "A"(0, 13)
          from :: ["A"(0, 13)] -(13)-> "A"(2, 13)
          from :: ["A"(0, 0)] -(0)-> "A"(12, 0)
          length :: ["A"(13, 0)] -(0)-> "A"(0, 13)
          length :: ["A"(13, 0)] -(0)-> "A"(13, 13)
          length1 :: ["A"(13, 0)] -(0)-> "A"(0, 13)
          length1 :: ["A"(13, 0)] -(0)-> "A"(14, 13)
          mark :: ["A"(0, 13)] -(0)-> "A"(0, 13)
          nil :: [] -(0)-> "A"(13, 0)
          nil :: [] -(0)-> "A"(0, 13)
          nil :: [] -(0)-> "A"(6, 15)
          s :: ["A"(0, 13)] -(0)-> "A"(0, 13)
          s :: ["A"(0, 13)] -(11)-> "A"(11, 13)
          s :: ["A"(0, 0)] -(0)-> "A"(0, 0)
        
        
        Cost-free Signatures used:
        --------------------------
        
        
        
        Base Constructor Signatures used:
        ---------------------------------
          "0_A" :: [] -(0)-> "A"(1, 0)
          "0_A" :: [] -(0)-> "A"(0, 1)
          "cons_A" :: ["A"(0, 0) x "A"(1, 0)] -(1)-> "A"(1, 0)
          "cons_A" :: ["A"(0, 1) x "A"(0, 0)] -(0)-> "A"(0, 1)
          "from_A" :: ["A"(0, 0)] -(0)-> "A"(1, 0)
          "from_A" :: ["A"(0, 1)] -(1)-> "A"(0, 1)
          "length1_A" :: ["A"(0, 0)] -(0)-> "A"(1, 0)
          "length1_A" :: ["A"(1, 0)] -(0)-> "A"(0, 1)
          "length_A" :: ["A"(0, 0)] -(0)-> "A"(1, 0)
          "length_A" :: ["A"(1, 0)] -(0)-> "A"(0, 1)
          "nil_A" :: [] -(0)-> "A"(1, 0)
          "nil_A" :: [] -(0)-> "A"(0, 1)
          "s_A" :: ["A"(0, 0)] -(1)-> "A"(1, 0)
          "s_A" :: ["A"(0, 1)] -(0)-> "A"(0, 1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          a__length(cons(X,Y)) -> s(a__length1(Y))
        2. Weak:
          a__from(X) -> from(X)
          a__length1(X) -> a__length(X)
          mark(cons(X1,X2)) -> cons(mark(X1),X2)
          mark(from(X)) -> a__from(mark(X))
          mark(s(X)) -> s(mark(X))
* Step 4: Ara WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict TRS:
            a__from(X) -> from(X)
            a__length1(X) -> a__length(X)
            mark(cons(X1,X2)) -> cons(mark(X1),X2)
            mark(from(X)) -> a__from(mark(X))
            mark(s(X)) -> s(mark(X))
        - Weak TRS:
            a__from(X) -> cons(mark(X),from(s(X)))
            a__length(X) -> length(X)
            a__length(cons(X,Y)) -> s(a__length1(Y))
            a__length(nil()) -> 0()
            a__length1(X) -> length1(X)
            mark(0()) -> 0()
            mark(length(X)) -> a__length(X)
            mark(length1(X)) -> a__length1(X)
            mark(nil()) -> nil()
        - Signature:
            {a__from/1,a__length/1,a__length1/1,mark/1} / {0/0,cons/2,from/1,length/1,length1/1,nil/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a__from,a__length,a__length1,mark} and constructors {0
            ,cons,from,length,length1,nil,s}
    + Applied Processor:
        Ara {araHeuristics = NoHeuristics, minDegree = 2, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
    + Details:
        Signatures used:
        ----------------
          0 :: [] -(0)-> "A"(0, 9)
          0 :: [] -(0)-> "A"(14, 15)
          0 :: [] -(0)-> "A"(6, 15)
          a__from :: ["A"(0, 9)] -(9)-> "A"(0, 9)
          a__length :: ["A"(9, 0)] -(1)-> "A"(8, 9)
          a__length1 :: ["A"(9, 0)] -(2)-> "A"(8, 9)
          cons :: ["A"(0, 9) x "A"(0, 0)] -(0)-> "A"(0, 9)
          cons :: ["A"(0, 0) x "A"(9, 0)] -(9)-> "A"(9, 0)
          from :: ["A"(0, 9)] -(9)-> "A"(0, 9)
          from :: ["A"(0, 9)] -(9)-> "A"(2, 9)
          from :: ["A"(0, 0)] -(0)-> "A"(4, 0)
          length :: ["A"(9, 0)] -(0)-> "A"(0, 9)
          length :: ["A"(9, 0)] -(0)-> "A"(10, 9)
          length1 :: ["A"(9, 0)] -(0)-> "A"(0, 9)
          length1 :: ["A"(9, 0)] -(0)-> "A"(10, 9)
          mark :: ["A"(0, 9)] -(2)-> "A"(0, 9)
          nil :: [] -(0)-> "A"(9, 0)
          nil :: [] -(0)-> "A"(0, 9)
          nil :: [] -(0)-> "A"(6, 15)
          s :: ["A"(0, 9)] -(0)-> "A"(0, 9)
          s :: ["A"(0, 9)] -(0)-> "A"(3, 9)
          s :: ["A"(0, 0)] -(0)-> "A"(2, 0)
          s :: ["A"(0, 9)] -(0)-> "A"(11, 9)
        
        
        Cost-free Signatures used:
        --------------------------
        
        
        
        Base Constructor Signatures used:
        ---------------------------------
          "0_A" :: [] -(0)-> "A"(1, 0)
          "0_A" :: [] -(0)-> "A"(0, 1)
          "cons_A" :: ["A"(0, 0) x "A"(1, 0)] -(1)-> "A"(1, 0)
          "cons_A" :: ["A"(0, 1) x "A"(0, 0)] -(0)-> "A"(0, 1)
          "from_A" :: ["A"(0, 0)] -(0)-> "A"(1, 0)
          "from_A" :: ["A"(0, 1)] -(1)-> "A"(0, 1)
          "length1_A" :: ["A"(0, 0)] -(0)-> "A"(1, 0)
          "length1_A" :: ["A"(1, 0)] -(0)-> "A"(0, 1)
          "length_A" :: ["A"(0, 0)] -(0)-> "A"(1, 0)
          "length_A" :: ["A"(1, 0)] -(0)-> "A"(0, 1)
          "nil_A" :: [] -(0)-> "A"(1, 0)
          "nil_A" :: [] -(0)-> "A"(0, 1)
          "s_A" :: ["A"(0, 0)] -(0)-> "A"(1, 0)
          "s_A" :: ["A"(0, 1)] -(0)-> "A"(0, 1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          a__length1(X) -> a__length(X)
        2. Weak:
          a__from(X) -> from(X)
          mark(cons(X1,X2)) -> cons(mark(X1),X2)
          mark(from(X)) -> a__from(mark(X))
          mark(s(X)) -> s(mark(X))
* Step 5: NaturalMI WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict TRS:
            a__from(X) -> from(X)
            mark(cons(X1,X2)) -> cons(mark(X1),X2)
            mark(from(X)) -> a__from(mark(X))
            mark(s(X)) -> s(mark(X))
        - Weak TRS:
            a__from(X) -> cons(mark(X),from(s(X)))
            a__length(X) -> length(X)
            a__length(cons(X,Y)) -> s(a__length1(Y))
            a__length(nil()) -> 0()
            a__length1(X) -> a__length(X)
            a__length1(X) -> length1(X)
            mark(0()) -> 0()
            mark(length(X)) -> a__length(X)
            mark(length1(X)) -> a__length1(X)
            mark(nil()) -> nil()
        - Signature:
            {a__from/1,a__length/1,a__length1/1,mark/1} / {0/0,cons/2,from/1,length/1,length1/1,nil/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a__from,a__length,a__length1,mark} and constructors {0
            ,cons,from,length,length1,nil,s}
    + Applied Processor:
        NaturalMI {miDimension = 3, miDegree = 3, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(a__from) = {1},
          uargs(cons) = {1},
          uargs(s) = {1}
        
        Following symbols are considered usable:
          {a__from,a__length,a__length1,mark}
        TcT has computed the following interpretation:
                   p(0) = [0]                          
                          [0]                          
                          [0]                          
             p(a__from) = [1 2 0]      [0]             
                          [0 1 0] x1 + [0]             
                          [0 0 0]      [2]             
           p(a__length) = [0 0 2]      [0]             
                          [0 0 2] x1 + [0]             
                          [0 0 0]      [0]             
          p(a__length1) = [0 0 2]      [0]             
                          [0 0 2] x1 + [0]             
                          [0 0 0]      [0]             
                p(cons) = [1 0 0]      [0 0 0]      [0]
                          [0 1 0] x1 + [0 0 0] x2 + [0]
                          [0 0 0]      [0 0 1]      [1]
                p(from) = [1 2 0]      [0]             
                          [0 1 0] x1 + [0]             
                          [0 0 0]      [1]             
              p(length) = [0 0 0]      [0]             
                          [0 0 2] x1 + [0]             
                          [0 0 0]      [0]             
             p(length1) = [0 0 1]      [0]             
                          [0 0 2] x1 + [0]             
                          [0 0 0]      [0]             
                p(mark) = [1 2 0]      [0]             
                          [0 1 0] x1 + [0]             
                          [0 0 2]      [0]             
                 p(nil) = [0]                          
                          [2]                          
                          [2]                          
                   p(s) = [1 0 0]      [2]             
                          [0 1 0] x1 + [2]             
                          [0 0 0]      [0]             
        
        Following rules are strictly oriented:
        mark(s(X)) = [1 2 0]     [6]
                     [0 1 0] X + [2]
                     [0 0 0]     [0]
                   > [1 2 0]     [2]
                     [0 1 0] X + [2]
                     [0 0 0]     [0]
                   = s(mark(X))     
        
        
        Following rules are (at-least) weakly oriented:
                  a__from(X) =  [1 2 0]     [0]              
                                [0 1 0] X + [0]              
                                [0 0 0]     [2]              
                             >= [1 2 0]     [0]              
                                [0 1 0] X + [0]              
                                [0 0 0]     [2]              
                             =  cons(mark(X),from(s(X)))     
        
                  a__from(X) =  [1 2 0]     [0]              
                                [0 1 0] X + [0]              
                                [0 0 0]     [2]              
                             >= [1 2 0]     [0]              
                                [0 1 0] X + [0]              
                                [0 0 0]     [1]              
                             =  from(X)                      
        
                a__length(X) =  [0 0 2]     [0]              
                                [0 0 2] X + [0]              
                                [0 0 0]     [0]              
                             >= [0 0 0]     [0]              
                                [0 0 2] X + [0]              
                                [0 0 0]     [0]              
                             =  length(X)                    
        
        a__length(cons(X,Y)) =  [0 0 2]     [2]              
                                [0 0 2] Y + [2]              
                                [0 0 0]     [0]              
                             >= [0 0 2]     [2]              
                                [0 0 2] Y + [2]              
                                [0 0 0]     [0]              
                             =  s(a__length1(Y))             
        
            a__length(nil()) =  [4]                          
                                [4]                          
                                [0]                          
                             >= [0]                          
                                [0]                          
                                [0]                          
                             =  0()                          
        
               a__length1(X) =  [0 0 2]     [0]              
                                [0 0 2] X + [0]              
                                [0 0 0]     [0]              
                             >= [0 0 2]     [0]              
                                [0 0 2] X + [0]              
                                [0 0 0]     [0]              
                             =  a__length(X)                 
        
               a__length1(X) =  [0 0 2]     [0]              
                                [0 0 2] X + [0]              
                                [0 0 0]     [0]              
                             >= [0 0 1]     [0]              
                                [0 0 2] X + [0]              
                                [0 0 0]     [0]              
                             =  length1(X)                   
        
                   mark(0()) =  [0]                          
                                [0]                          
                                [0]                          
                             >= [0]                          
                                [0]                          
                                [0]                          
                             =  0()                          
        
           mark(cons(X1,X2)) =  [1 2 0]      [0 0 0]      [0]
                                [0 1 0] X1 + [0 0 0] X2 + [0]
                                [0 0 0]      [0 0 2]      [2]
                             >= [1 2 0]      [0 0 0]      [0]
                                [0 1 0] X1 + [0 0 0] X2 + [0]
                                [0 0 0]      [0 0 1]      [1]
                             =  cons(mark(X1),X2)            
        
               mark(from(X)) =  [1 4 0]     [0]              
                                [0 1 0] X + [0]              
                                [0 0 0]     [2]              
                             >= [1 4 0]     [0]              
                                [0 1 0] X + [0]              
                                [0 0 0]     [2]              
                             =  a__from(mark(X))             
        
             mark(length(X)) =  [0 0 4]     [0]              
                                [0 0 2] X + [0]              
                                [0 0 0]     [0]              
                             >= [0 0 2]     [0]              
                                [0 0 2] X + [0]              
                                [0 0 0]     [0]              
                             =  a__length(X)                 
        
            mark(length1(X)) =  [0 0 5]     [0]              
                                [0 0 2] X + [0]              
                                [0 0 0]     [0]              
                             >= [0 0 2]     [0]              
                                [0 0 2] X + [0]              
                                [0 0 0]     [0]              
                             =  a__length1(X)                
        
                 mark(nil()) =  [4]                          
                                [2]                          
                                [4]                          
                             >= [0]                          
                                [2]                          
                                [2]                          
                             =  nil()                        
        
* Step 6: NaturalMI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            a__from(X) -> from(X)
            mark(cons(X1,X2)) -> cons(mark(X1),X2)
            mark(from(X)) -> a__from(mark(X))
        - Weak TRS:
            a__from(X) -> cons(mark(X),from(s(X)))
            a__length(X) -> length(X)
            a__length(cons(X,Y)) -> s(a__length1(Y))
            a__length(nil()) -> 0()
            a__length1(X) -> a__length(X)
            a__length1(X) -> length1(X)
            mark(0()) -> 0()
            mark(length(X)) -> a__length(X)
            mark(length1(X)) -> a__length1(X)
            mark(nil()) -> nil()
            mark(s(X)) -> s(mark(X))
        - Signature:
            {a__from/1,a__length/1,a__length1/1,mark/1} / {0/0,cons/2,from/1,length/1,length1/1,nil/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a__from,a__length,a__length1,mark} and constructors {0
            ,cons,from,length,length1,nil,s}
    + Applied Processor:
        NaturalMI {miDimension = 3, miDegree = 3, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(a__from) = {1},
          uargs(cons) = {1},
          uargs(s) = {1}
        
        Following symbols are considered usable:
          {a__from,a__length,a__length1,mark}
        TcT has computed the following interpretation:
                   p(0) = [0]             
                          [0]             
                          [0]             
             p(a__from) = [1 0 1]      [1]
                          [0 2 0] x1 + [0]
                          [0 0 1]      [2]
           p(a__length) = [0]             
                          [0]             
                          [0]             
          p(a__length1) = [0]             
                          [0]             
                          [0]             
                p(cons) = [1 0 0]      [0]
                          [0 0 0] x1 + [0]
                          [0 0 1]      [0]
                p(from) = [1 0 1]      [0]
                          [0 0 0] x1 + [0]
                          [0 0 1]      [2]
              p(length) = [0]             
                          [0]             
                          [0]             
             p(length1) = [0]             
                          [0]             
                          [0]             
                p(mark) = [1 0 1]      [1]
                          [0 0 0] x1 + [0]
                          [0 0 1]      [0]
                 p(nil) = [3]             
                          [0]             
                          [0]             
                   p(s) = [1 0 0]      [0]
                          [0 0 0] x1 + [0]
                          [0 0 1]      [0]
        
        Following rules are strictly oriented:
           a__from(X) = [1 0 1]     [1] 
                        [0 2 0] X + [0] 
                        [0 0 1]     [2] 
                      > [1 0 1]     [0] 
                        [0 0 0] X + [0] 
                        [0 0 1]     [2] 
                      = from(X)         
        
        mark(from(X)) = [1 0 2]     [3] 
                        [0 0 0] X + [0] 
                        [0 0 1]     [2] 
                      > [1 0 2]     [2] 
                        [0 0 0] X + [0] 
                        [0 0 1]     [2] 
                      = a__from(mark(X))
        
        
        Following rules are (at-least) weakly oriented:
                  a__from(X) =  [1 0 1]     [1]         
                                [0 2 0] X + [0]         
                                [0 0 1]     [2]         
                             >= [1 0 1]     [1]         
                                [0 0 0] X + [0]         
                                [0 0 1]     [0]         
                             =  cons(mark(X),from(s(X)))
        
                a__length(X) =  [0]                     
                                [0]                     
                                [0]                     
                             >= [0]                     
                                [0]                     
                                [0]                     
                             =  length(X)               
        
        a__length(cons(X,Y)) =  [0]                     
                                [0]                     
                                [0]                     
                             >= [0]                     
                                [0]                     
                                [0]                     
                             =  s(a__length1(Y))        
        
            a__length(nil()) =  [0]                     
                                [0]                     
                                [0]                     
                             >= [0]                     
                                [0]                     
                                [0]                     
                             =  0()                     
        
               a__length1(X) =  [0]                     
                                [0]                     
                                [0]                     
                             >= [0]                     
                                [0]                     
                                [0]                     
                             =  a__length(X)            
        
               a__length1(X) =  [0]                     
                                [0]                     
                                [0]                     
                             >= [0]                     
                                [0]                     
                                [0]                     
                             =  length1(X)              
        
                   mark(0()) =  [1]                     
                                [0]                     
                                [0]                     
                             >= [0]                     
                                [0]                     
                                [0]                     
                             =  0()                     
        
           mark(cons(X1,X2)) =  [1 0 1]      [1]        
                                [0 0 0] X1 + [0]        
                                [0 0 1]      [0]        
                             >= [1 0 1]      [1]        
                                [0 0 0] X1 + [0]        
                                [0 0 1]      [0]        
                             =  cons(mark(X1),X2)       
        
             mark(length(X)) =  [1]                     
                                [0]                     
                                [0]                     
                             >= [0]                     
                                [0]                     
                                [0]                     
                             =  a__length(X)            
        
            mark(length1(X)) =  [1]                     
                                [0]                     
                                [0]                     
                             >= [0]                     
                                [0]                     
                                [0]                     
                             =  a__length1(X)           
        
                 mark(nil()) =  [4]                     
                                [0]                     
                                [0]                     
                             >= [3]                     
                                [0]                     
                                [0]                     
                             =  nil()                   
        
                  mark(s(X)) =  [1 0 1]     [1]         
                                [0 0 0] X + [0]         
                                [0 0 1]     [0]         
                             >= [1 0 1]     [1]         
                                [0 0 0] X + [0]         
                                [0 0 1]     [0]         
                             =  s(mark(X))              
        
* Step 7: NaturalMI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            mark(cons(X1,X2)) -> cons(mark(X1),X2)
        - Weak TRS:
            a__from(X) -> cons(mark(X),from(s(X)))
            a__from(X) -> from(X)
            a__length(X) -> length(X)
            a__length(cons(X,Y)) -> s(a__length1(Y))
            a__length(nil()) -> 0()
            a__length1(X) -> a__length(X)
            a__length1(X) -> length1(X)
            mark(0()) -> 0()
            mark(from(X)) -> a__from(mark(X))
            mark(length(X)) -> a__length(X)
            mark(length1(X)) -> a__length1(X)
            mark(nil()) -> nil()
            mark(s(X)) -> s(mark(X))
        - Signature:
            {a__from/1,a__length/1,a__length1/1,mark/1} / {0/0,cons/2,from/1,length/1,length1/1,nil/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a__from,a__length,a__length1,mark} and constructors {0
            ,cons,from,length,length1,nil,s}
    + Applied Processor:
        NaturalMI {miDimension = 3, miDegree = 3, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(a__from) = {1},
          uargs(cons) = {1},
          uargs(s) = {1}
        
        Following symbols are considered usable:
          {a__from,a__length,a__length1,mark}
        TcT has computed the following interpretation:
                   p(0) = [0]                          
                          [0]                          
                          [0]                          
             p(a__from) = [1 2 0]      [1]             
                          [0 1 1] x1 + [2]             
                          [0 0 3]      [0]             
           p(a__length) = [0]                          
                          [0]                          
                          [0]                          
          p(a__length1) = [0]                          
                          [0]                          
                          [0]                          
                p(cons) = [1 0 3]      [0 0 1]      [0]
                          [0 1 0] x1 + [0 0 1] x2 + [2]
                          [0 0 0]      [0 0 0]      [0]
                p(from) = [1 2 0]      [1]             
                          [0 1 0] x1 + [2]             
                          [0 0 0]      [0]             
              p(length) = [0]                          
                          [0]                          
                          [0]                          
             p(length1) = [0]                          
                          [0]                          
                          [0]                          
                p(mark) = [1 2 0]      [1]             
                          [0 1 0] x1 + [0]             
                          [0 0 0]      [0]             
                 p(nil) = [3]                          
                          [0]                          
                          [0]                          
                   p(s) = [1 1 1]      [0]             
                          [0 1 0] x1 + [0]             
                          [0 0 0]      [0]             
        
        Following rules are strictly oriented:
        mark(cons(X1,X2)) = [1 2 3]      [0 0 3]      [5]
                            [0 1 0] X1 + [0 0 1] X2 + [2]
                            [0 0 0]      [0 0 0]      [0]
                          > [1 2 0]      [0 0 1]      [1]
                            [0 1 0] X1 + [0 0 1] X2 + [2]
                            [0 0 0]      [0 0 0]      [0]
                          = cons(mark(X1),X2)            
        
        
        Following rules are (at-least) weakly oriented:
                  a__from(X) =  [1 2 0]     [1]         
                                [0 1 1] X + [2]         
                                [0 0 3]     [0]         
                             >= [1 2 0]     [1]         
                                [0 1 0] X + [2]         
                                [0 0 0]     [0]         
                             =  cons(mark(X),from(s(X)))
        
                  a__from(X) =  [1 2 0]     [1]         
                                [0 1 1] X + [2]         
                                [0 0 3]     [0]         
                             >= [1 2 0]     [1]         
                                [0 1 0] X + [2]         
                                [0 0 0]     [0]         
                             =  from(X)                 
        
                a__length(X) =  [0]                     
                                [0]                     
                                [0]                     
                             >= [0]                     
                                [0]                     
                                [0]                     
                             =  length(X)               
        
        a__length(cons(X,Y)) =  [0]                     
                                [0]                     
                                [0]                     
                             >= [0]                     
                                [0]                     
                                [0]                     
                             =  s(a__length1(Y))        
        
            a__length(nil()) =  [0]                     
                                [0]                     
                                [0]                     
                             >= [0]                     
                                [0]                     
                                [0]                     
                             =  0()                     
        
               a__length1(X) =  [0]                     
                                [0]                     
                                [0]                     
                             >= [0]                     
                                [0]                     
                                [0]                     
                             =  a__length(X)            
        
               a__length1(X) =  [0]                     
                                [0]                     
                                [0]                     
                             >= [0]                     
                                [0]                     
                                [0]                     
                             =  length1(X)              
        
                   mark(0()) =  [1]                     
                                [0]                     
                                [0]                     
                             >= [0]                     
                                [0]                     
                                [0]                     
                             =  0()                     
        
               mark(from(X)) =  [1 4 0]     [6]         
                                [0 1 0] X + [2]         
                                [0 0 0]     [0]         
                             >= [1 4 0]     [2]         
                                [0 1 0] X + [2]         
                                [0 0 0]     [0]         
                             =  a__from(mark(X))        
        
             mark(length(X)) =  [1]                     
                                [0]                     
                                [0]                     
                             >= [0]                     
                                [0]                     
                                [0]                     
                             =  a__length(X)            
        
            mark(length1(X)) =  [1]                     
                                [0]                     
                                [0]                     
                             >= [0]                     
                                [0]                     
                                [0]                     
                             =  a__length1(X)           
        
                 mark(nil()) =  [4]                     
                                [0]                     
                                [0]                     
                             >= [3]                     
                                [0]                     
                                [0]                     
                             =  nil()                   
        
                  mark(s(X)) =  [1 3 1]     [1]         
                                [0 1 0] X + [0]         
                                [0 0 0]     [0]         
                             >= [1 3 0]     [1]         
                                [0 1 0] X + [0]         
                                [0 0 0]     [0]         
                             =  s(mark(X))              
        
* Step 8: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            a__from(X) -> cons(mark(X),from(s(X)))
            a__from(X) -> from(X)
            a__length(X) -> length(X)
            a__length(cons(X,Y)) -> s(a__length1(Y))
            a__length(nil()) -> 0()
            a__length1(X) -> a__length(X)
            a__length1(X) -> length1(X)
            mark(0()) -> 0()
            mark(cons(X1,X2)) -> cons(mark(X1),X2)
            mark(from(X)) -> a__from(mark(X))
            mark(length(X)) -> a__length(X)
            mark(length1(X)) -> a__length1(X)
            mark(nil()) -> nil()
            mark(s(X)) -> s(mark(X))
        - Signature:
            {a__from/1,a__length/1,a__length1/1,mark/1} / {0/0,cons/2,from/1,length/1,length1/1,nil/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {a__from,a__length,a__length1,mark} and constructors {0
            ,cons,from,length,length1,nil,s}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^3))