Problem Transformed CSR 04 Ex4 7 77 Bor03 GM

Tool CaT

Execution Time	Unknown
Answer	YES(?,O(n^2))
Input	Transformed CSR 04 Ex4 7 77 Bor03 GM

stdout:

YES(?,O(n^2))

Problem:
a__zeros() -> cons(0(),zeros())
a__tail(cons(X,XS)) -> mark(XS)
mark(zeros()) -> a__zeros()
mark(tail(X)) -> a__tail(mark(X))
mark(cons(X1,X2)) -> cons(mark(X1),X2)
mark(0()) -> 0()
a__zeros() -> zeros()
a__tail(X) -> tail(X)

Proof:
Complexity Transformation Processor:
  strict:
   a__zeros() -> cons(0(),zeros())
   a__tail(cons(X,XS)) -> mark(XS)
   mark(zeros()) -> a__zeros()
   mark(tail(X)) -> a__tail(mark(X))
   mark(cons(X1,X2)) -> cons(mark(X1),X2)
   mark(0()) -> 0()
   a__zeros() -> zeros()
   a__tail(X) -> tail(X)
  weak:

  Matrix Interpretation Processor:
   dimension: 2
   max_matrix:
    [1 1]
    [0 1]
    interpretation:
                  [1 1]     [4]
     [tail](x0) = [0 1]x0 + [6],

                  [1 1]     [1]
     [mark](x0) = [0 1]x0 + [2],

                     [1 1]     [6]
     [a__tail](x0) = [0 1]x0 + [6],

                                [0]
     [cons](x0, x1) = x0 + x1 + [1],

               [2]
     [zeros] = [1],

           [0]
     [0] = [1],

                  [3]
     [a__zeros] = [3]
    orientation:
                  [3]    [2]
     a__zeros() = [3] >= [3] = cons(0(),zeros())

                           [1 1]    [1 1]     [7]    [1 1]     [1]
     a__tail(cons(X,XS)) = [0 1]X + [0 1]XS + [7] >= [0 1]XS + [2] = mark(XS)

                     [4]    [3]
     mark(zeros()) = [3] >= [3] = a__zeros()

                     [1 2]    [11]    [1 2]    [9]
     mark(tail(X)) = [0 1]X + [8 ] >= [0 1]X + [8] = a__tail(mark(X))

                         [1 1]     [1 1]     [2]    [1 1]          [1]
     mark(cons(X1,X2)) = [0 1]X1 + [0 1]X2 + [3] >= [0 1]X1 + X2 + [3] = cons(mark(X1),X2)

                 [2]    [0]
     mark(0()) = [3] >= [1] = 0()

                  [3]    [2]
     a__zeros() = [3] >= [1] = zeros()

                  [1 1]    [6]    [1 1]    [4]
     a__tail(X) = [0 1]X + [6] >= [0 1]X + [6] = tail(X)
    problem:
     strict:

     weak:
      a__zeros() -> cons(0(),zeros())
      a__tail(cons(X,XS)) -> mark(XS)
      mark(zeros()) -> a__zeros()
      mark(tail(X)) -> a__tail(mark(X))
      mark(cons(X1,X2)) -> cons(mark(X1),X2)
      mark(0()) -> 0()
      a__zeros() -> zeros()
      a__tail(X) -> tail(X)
    Qed

Tool IRC1

Execution Time	Unknown
Answer	YES(?,O(n^3))
Input	Transformed CSR 04 Ex4 7 77 Bor03 GM

stdout:

YES(?,O(n^3))

Tool IRC2

Execution Time	Unknown
Answer	YES(?,O(n^2))
Input	Transformed CSR 04 Ex4 7 77 Bor03 GM

stdout:

YES(?,O(n^2))

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           YES(?,O(n^2))
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  a__zeros() -> cons(0(), zeros())
     , a__tail(cons(X, XS)) -> mark(XS)
     , mark(zeros()) -> a__zeros()
     , mark(tail(X)) -> a__tail(mark(X))
     , mark(cons(X1, X2)) -> cons(mark(X1), X2)
     , mark(0()) -> 0()
     , a__zeros() -> zeros()
     , a__tail(X) -> tail(X)}

Proof Output:
  'wdg' proved the best result:

  Details:
  --------
    'wdg' succeeded with the following output:
     'wdg'
     -----
     Answer:           YES(?,O(n^2))
     Input Problem:    innermost runtime-complexity with respect to
       Rules:
         {  a__zeros() -> cons(0(), zeros())
          , a__tail(cons(X, XS)) -> mark(XS)
          , mark(zeros()) -> a__zeros()
          , mark(tail(X)) -> a__tail(mark(X))
          , mark(cons(X1, X2)) -> cons(mark(X1), X2)
          , mark(0()) -> 0()
          , a__zeros() -> zeros()
          , a__tail(X) -> tail(X)}

     Proof Output:
       Transformation Details:
       -----------------------
         We have computed the following set of weak (innermost) dependency pairs:

           {  1: a__zeros^#() -> c_0()
            , 2: a__tail^#(cons(X, XS)) -> c_1(mark^#(XS))
            , 3: mark^#(zeros()) -> c_2(a__zeros^#())
            , 4: mark^#(tail(X)) -> c_3(a__tail^#(mark(X)))
            , 5: mark^#(cons(X1, X2)) -> c_4(mark^#(X1))
            , 6: mark^#(0()) -> c_5()
            , 7: a__zeros^#() -> c_6()
            , 8: a__tail^#(X) -> c_7()}

         Following Dependency Graph (modulo SCCs) was computed. (Answers to
         subproofs are indicated to the right.)

           ->{2,4,5}                                                   [   YES(?,O(n^2))    ]
              |
              |->{3}                                                   [   YES(?,O(n^2))    ]
              |   |
              |   |->{1}                                               [   YES(?,O(n^2))    ]
              |   |
              |   `->{7}                                               [   YES(?,O(n^2))    ]
              |
              |->{6}                                                   [   YES(?,O(n^2))    ]
              |
              `->{8}                                                   [   YES(?,O(n^2))    ]



       Sub-problems:
       -------------
         * Path {2,4,5}: YES(?,O(n^2))
           ---------------------------

           The usable rules for this path are:

             {  mark(zeros()) -> a__zeros()
              , mark(tail(X)) -> a__tail(mark(X))
              , mark(cons(X1, X2)) -> cons(mark(X1), X2)
              , mark(0()) -> 0()
              , a__zeros() -> cons(0(), zeros())
              , a__tail(cons(X, XS)) -> mark(XS)
              , a__zeros() -> zeros()
              , a__tail(X) -> tail(X)}

           The weightgap principle applies, using the following adequate RMI:
             The following argument positions are usable:
               Uargs(cons) = {1}, Uargs(a__tail) = {1}, Uargs(mark) = {},
               Uargs(tail) = {}, Uargs(a__tail^#) = {1}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(c_2) = {}, Uargs(c_3) = {1},
               Uargs(c_4) = {1}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__zeros() = [1]
                           [3]
              cons(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                             [0 1]      [0 1]      [1]
              0() = [0]
                    [1]
              zeros() = [0]
                        [1]
              a__tail(x1) = [1 2] x1 + [1]
                            [0 1]      [3]
              mark(x1) = [1 2] x1 + [0]
                         [0 1]      [2]
              tail(x1) = [1 2] x1 + [0]
                         [0 1]      [3]
              a__zeros^#() = [0]
                             [0]
              c_0() = [0]
                      [0]
              a__tail^#(x1) = [2 0] x1 + [0]
                              [3 3]      [0]
              c_1(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              mark^#(x1) = [2 0] x1 + [0]
                           [3 3]      [0]
              c_2(x1) = [0 0] x1 + [0]
                        [0 0]      [0]
              c_3(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              c_4(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              c_5() = [0]
                      [0]
              c_6() = [0]
                      [0]
              c_7() = [0]
                      [0]
           Complexity induced by the adequate RMI: YES(?,O(n^2))

           We apply the sub-processor on the resulting sub-problem:

           'matrix-interpretation of dimension 2'
           --------------------------------------
           Answer:           YES(?,O(n^1))
           Input Problem:    innermost DP runtime-complexity with respect to
             Strict Rules:
               {  a__tail^#(cons(X, XS)) -> c_1(mark^#(XS))
                , mark^#(tail(X)) -> c_3(a__tail^#(mark(X)))
                , mark^#(cons(X1, X2)) -> c_4(mark^#(X1))}
             Weak Rules:
               {  mark(zeros()) -> a__zeros()
                , mark(tail(X)) -> a__tail(mark(X))
                , mark(cons(X1, X2)) -> cons(mark(X1), X2)
                , mark(0()) -> 0()
                , a__zeros() -> cons(0(), zeros())
                , a__tail(cons(X, XS)) -> mark(XS)
                , a__zeros() -> zeros()
                , a__tail(X) -> tail(X)}

           Proof Output:
             The following argument positions are usable:
               Uargs(cons) = {}, Uargs(a__tail) = {}, Uargs(mark) = {},
               Uargs(tail) = {}, Uargs(a__tail^#) = {}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(c_3) = {1}, Uargs(c_4) = {1}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__zeros() = [0]
                           [1]
              cons(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                             [0 1]      [0 1]      [1]
              0() = [0]
                    [0]
              zeros() = [0]
                        [0]
              a__tail(x1) = [0 0] x1 + [0]
                            [0 1]      [4]
              mark(x1) = [0 0] x1 + [0]
                         [0 1]      [2]
              tail(x1) = [0 0] x1 + [0]
                         [0 1]      [4]
              a__tail^#(x1) = [0 1] x1 + [0]
                              [0 0]      [0]
              c_1(x1) = [1 0] x1 + [0]
                        [0 0]      [0]
              mark^#(x1) = [0 1] x1 + [0]
                           [0 0]      [0]
              c_3(x1) = [1 0] x1 + [1]
                        [0 0]      [0]
              c_4(x1) = [1 0] x1 + [0]
                        [0 0]      [0]

         * Path {2,4,5}->{3}: YES(?,O(n^2))
           --------------------------------

           The usable rules for this path are:

             {  mark(zeros()) -> a__zeros()
              , mark(tail(X)) -> a__tail(mark(X))
              , mark(cons(X1, X2)) -> cons(mark(X1), X2)
              , mark(0()) -> 0()
              , a__zeros() -> cons(0(), zeros())
              , a__tail(cons(X, XS)) -> mark(XS)
              , a__zeros() -> zeros()
              , a__tail(X) -> tail(X)}

           The weightgap principle applies, using the following adequate RMI:
             The following argument positions are usable:
               Uargs(cons) = {1}, Uargs(a__tail) = {1}, Uargs(mark) = {},
               Uargs(tail) = {}, Uargs(a__tail^#) = {1}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(c_2) = {}, Uargs(c_3) = {1},
               Uargs(c_4) = {1}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__zeros() = [1]
                           [1]
              cons(x1, x2) = [1 0] x1 + [1 2] x2 + [0]
                             [0 1]      [0 1]      [1]
              0() = [0]
                    [0]
              zeros() = [0]
                        [0]
              a__tail(x1) = [1 3] x1 + [2]
                            [0 1]      [3]
              mark(x1) = [1 2] x1 + [3]
                         [0 1]      [1]
              tail(x1) = [1 3] x1 + [0]
                         [0 1]      [3]
              a__zeros^#() = [0]
                             [0]
              c_0() = [0]
                      [0]
              a__tail^#(x1) = [3 0] x1 + [0]
                              [0 0]      [0]
              c_1(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              mark^#(x1) = [0 0] x1 + [0]
                           [0 0]      [0]
              c_2(x1) = [0 0] x1 + [0]
                        [0 0]      [0]
              c_3(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              c_4(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              c_5() = [0]
                      [0]
              c_6() = [0]
                      [0]
              c_7() = [0]
                      [0]
           Complexity induced by the adequate RMI: YES(?,O(n^2))

           We apply the sub-processor on the resulting sub-problem:

           'matrix-interpretation of dimension 2'
           --------------------------------------
           Answer:           YES(?,O(n^2))
           Input Problem:    innermost DP runtime-complexity with respect to
             Strict Rules: {mark^#(zeros()) -> c_2(a__zeros^#())}
             Weak Rules:
               {  a__tail^#(cons(X, XS)) -> c_1(mark^#(XS))
                , mark^#(tail(X)) -> c_3(a__tail^#(mark(X)))
                , mark^#(cons(X1, X2)) -> c_4(mark^#(X1))
                , mark(zeros()) -> a__zeros()
                , mark(tail(X)) -> a__tail(mark(X))
                , mark(cons(X1, X2)) -> cons(mark(X1), X2)
                , mark(0()) -> 0()
                , a__zeros() -> cons(0(), zeros())
                , a__tail(cons(X, XS)) -> mark(XS)
                , a__zeros() -> zeros()
                , a__tail(X) -> tail(X)}

           Proof Output:
             The following argument positions are usable:
               Uargs(cons) = {}, Uargs(a__tail) = {}, Uargs(mark) = {},
               Uargs(tail) = {}, Uargs(a__tail^#) = {}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(c_2) = {}, Uargs(c_3) = {1},
               Uargs(c_4) = {1}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__zeros() = [6]
                           [3]
              cons(x1, x2) = [1 0] x1 + [1 2] x2 + [0]
                             [0 1]      [0 1]      [1]
              0() = [0]
                    [0]
              zeros() = [2]
                        [2]
              a__tail(x1) = [1 2] x1 + [0]
                            [0 1]      [2]
              mark(x1) = [1 2] x1 + [0]
                         [0 1]      [1]
              tail(x1) = [1 2] x1 + [0]
                         [0 1]      [2]
              a__zeros^#() = [2]
                             [2]
              a__tail^#(x1) = [3 2] x1 + [0]
                              [3 3]      [6]
              c_1(x1) = [1 0] x1 + [2]
                        [0 2]      [3]
              mark^#(x1) = [3 2] x1 + [0]
                           [0 3]      [2]
              c_2(x1) = [2 2] x1 + [1]
                        [2 2]      [0]
              c_3(x1) = [1 0] x1 + [0]
                        [0 0]      [7]
              c_4(x1) = [1 0] x1 + [2]
                        [0 0]      [2]

         * Path {2,4,5}->{3}->{1}: YES(?,O(n^2))
           -------------------------------------

           The usable rules for this path are:

             {  mark(zeros()) -> a__zeros()
              , mark(tail(X)) -> a__tail(mark(X))
              , mark(cons(X1, X2)) -> cons(mark(X1), X2)
              , mark(0()) -> 0()
              , a__zeros() -> cons(0(), zeros())
              , a__tail(cons(X, XS)) -> mark(XS)
              , a__zeros() -> zeros()
              , a__tail(X) -> tail(X)}

           The weightgap principle applies, using the following adequate RMI:
             The following argument positions are usable:
               Uargs(cons) = {1}, Uargs(a__tail) = {1}, Uargs(mark) = {},
               Uargs(tail) = {}, Uargs(a__tail^#) = {1}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(c_2) = {1}, Uargs(c_3) = {1},
               Uargs(c_4) = {1}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__zeros() = [1]
                           [3]
              cons(x1, x2) = [1 0] x1 + [1 1] x2 + [0]
                             [0 1]      [0 1]      [1]
              0() = [0]
                    [2]
              zeros() = [0]
                        [0]
              a__tail(x1) = [1 0] x1 + [3]
                            [0 1]      [3]
              mark(x1) = [1 1] x1 + [2]
                         [0 1]      [3]
              tail(x1) = [1 0] x1 + [1]
                         [0 1]      [3]
              a__zeros^#() = [0]
                             [0]
              c_0() = [0]
                      [0]
              a__tail^#(x1) = [3 0] x1 + [0]
                              [0 0]      [0]
              c_1(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              mark^#(x1) = [0 0] x1 + [0]
                           [0 0]      [0]
              c_2(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              c_3(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              c_4(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              c_5() = [0]
                      [0]
              c_6() = [0]
                      [0]
              c_7() = [0]
                      [0]
           Complexity induced by the adequate RMI: YES(?,O(n^2))

           We apply the sub-processor on the resulting sub-problem:

           'matrix-interpretation of dimension 2'
           --------------------------------------
           Answer:           YES(?,O(1))
           Input Problem:    innermost DP runtime-complexity with respect to
             Strict Rules: {a__zeros^#() -> c_0()}
             Weak Rules:
               {  mark^#(zeros()) -> c_2(a__zeros^#())
                , a__tail^#(cons(X, XS)) -> c_1(mark^#(XS))
                , mark^#(tail(X)) -> c_3(a__tail^#(mark(X)))
                , mark^#(cons(X1, X2)) -> c_4(mark^#(X1))
                , mark(zeros()) -> a__zeros()
                , mark(tail(X)) -> a__tail(mark(X))
                , mark(cons(X1, X2)) -> cons(mark(X1), X2)
                , mark(0()) -> 0()
                , a__zeros() -> cons(0(), zeros())
                , a__tail(cons(X, XS)) -> mark(XS)
                , a__zeros() -> zeros()
                , a__tail(X) -> tail(X)}

           Proof Output:
             The following argument positions are usable:
               Uargs(cons) = {}, Uargs(a__tail) = {}, Uargs(mark) = {},
               Uargs(tail) = {}, Uargs(a__tail^#) = {}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(c_2) = {1}, Uargs(c_3) = {1},
               Uargs(c_4) = {1}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__zeros() = [0]
                           [0]
              cons(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                             [0 0]      [0 0]      [0]
              0() = [0]
                    [0]
              zeros() = [0]
                        [0]
              a__tail(x1) = [0 0] x1 + [0]
                            [0 0]      [0]
              mark(x1) = [0 0] x1 + [0]
                         [0 0]      [0]
              tail(x1) = [0 0] x1 + [0]
                         [0 0]      [0]
              a__zeros^#() = [1]
                             [0]
              c_0() = [0]
                      [0]
              a__tail^#(x1) = [0 0] x1 + [1]
                              [0 0]      [0]
              c_1(x1) = [1 0] x1 + [0]
                        [0 0]      [0]
              mark^#(x1) = [0 0] x1 + [1]
                           [0 0]      [4]
              c_2(x1) = [1 0] x1 + [0]
                        [0 0]      [3]
              c_3(x1) = [1 0] x1 + [0]
                        [0 0]      [2]
              c_4(x1) = [1 0] x1 + [0]
                        [0 0]      [3]

         * Path {2,4,5}->{3}->{7}: YES(?,O(n^2))
           -------------------------------------

           The usable rules for this path are:

             {  mark(zeros()) -> a__zeros()
              , mark(tail(X)) -> a__tail(mark(X))
              , mark(cons(X1, X2)) -> cons(mark(X1), X2)
              , mark(0()) -> 0()
              , a__zeros() -> cons(0(), zeros())
              , a__tail(cons(X, XS)) -> mark(XS)
              , a__zeros() -> zeros()
              , a__tail(X) -> tail(X)}

           The weightgap principle applies, using the following adequate RMI:
             The following argument positions are usable:
               Uargs(cons) = {1}, Uargs(a__tail) = {1}, Uargs(mark) = {},
               Uargs(tail) = {}, Uargs(a__tail^#) = {1}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(c_2) = {1}, Uargs(c_3) = {1},
               Uargs(c_4) = {1}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__zeros() = [1]
                           [3]
              cons(x1, x2) = [1 0] x1 + [1 1] x2 + [0]
                             [0 1]      [0 1]      [1]
              0() = [0]
                    [2]
              zeros() = [0]
                        [0]
              a__tail(x1) = [1 0] x1 + [3]
                            [0 1]      [3]
              mark(x1) = [1 1] x1 + [2]
                         [0 1]      [3]
              tail(x1) = [1 0] x1 + [1]
                         [0 1]      [3]
              a__zeros^#() = [0]
                             [0]
              c_0() = [0]
                      [0]
              a__tail^#(x1) = [3 0] x1 + [0]
                              [0 0]      [0]
              c_1(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              mark^#(x1) = [0 0] x1 + [0]
                           [0 0]      [0]
              c_2(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              c_3(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              c_4(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              c_5() = [0]
                      [0]
              c_6() = [0]
                      [0]
              c_7() = [0]
                      [0]
           Complexity induced by the adequate RMI: YES(?,O(n^2))

           We apply the sub-processor on the resulting sub-problem:

           'matrix-interpretation of dimension 2'
           --------------------------------------
           Answer:           YES(?,O(1))
           Input Problem:    innermost DP runtime-complexity with respect to
             Strict Rules: {a__zeros^#() -> c_6()}
             Weak Rules:
               {  mark^#(zeros()) -> c_2(a__zeros^#())
                , a__tail^#(cons(X, XS)) -> c_1(mark^#(XS))
                , mark^#(tail(X)) -> c_3(a__tail^#(mark(X)))
                , mark^#(cons(X1, X2)) -> c_4(mark^#(X1))
                , mark(zeros()) -> a__zeros()
                , mark(tail(X)) -> a__tail(mark(X))
                , mark(cons(X1, X2)) -> cons(mark(X1), X2)
                , mark(0()) -> 0()
                , a__zeros() -> cons(0(), zeros())
                , a__tail(cons(X, XS)) -> mark(XS)
                , a__zeros() -> zeros()
                , a__tail(X) -> tail(X)}

           Proof Output:
             The following argument positions are usable:
               Uargs(cons) = {}, Uargs(a__tail) = {}, Uargs(mark) = {},
               Uargs(tail) = {}, Uargs(a__tail^#) = {}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(c_2) = {1}, Uargs(c_3) = {1},
               Uargs(c_4) = {1}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__zeros() = [0]
                           [0]
              cons(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                             [0 0]      [0 0]      [0]
              0() = [0]
                    [0]
              zeros() = [0]
                        [0]
              a__tail(x1) = [0 0] x1 + [0]
                            [0 0]      [0]
              mark(x1) = [0 0] x1 + [0]
                         [0 0]      [0]
              tail(x1) = [0 0] x1 + [0]
                         [0 0]      [0]
              a__zeros^#() = [1]
                             [0]
              a__tail^#(x1) = [0 0] x1 + [1]
                              [0 0]      [0]
              c_1(x1) = [1 0] x1 + [0]
                        [0 0]      [0]
              mark^#(x1) = [0 0] x1 + [1]
                           [0 0]      [4]
              c_2(x1) = [1 0] x1 + [0]
                        [0 0]      [3]
              c_3(x1) = [1 0] x1 + [0]
                        [0 0]      [2]
              c_4(x1) = [1 0] x1 + [0]
                        [0 0]      [3]
              c_6() = [0]
                      [0]

         * Path {2,4,5}->{6}: YES(?,O(n^2))
           --------------------------------

           The usable rules for this path are:

             {  mark(zeros()) -> a__zeros()
              , mark(tail(X)) -> a__tail(mark(X))
              , mark(cons(X1, X2)) -> cons(mark(X1), X2)
              , mark(0()) -> 0()
              , a__zeros() -> cons(0(), zeros())
              , a__tail(cons(X, XS)) -> mark(XS)
              , a__zeros() -> zeros()
              , a__tail(X) -> tail(X)}

           The weightgap principle applies, using the following adequate RMI:
             The following argument positions are usable:
               Uargs(cons) = {1}, Uargs(a__tail) = {1}, Uargs(mark) = {},
               Uargs(tail) = {}, Uargs(a__tail^#) = {1}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(c_2) = {}, Uargs(c_3) = {1},
               Uargs(c_4) = {1}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__zeros() = [1]
                           [1]
              cons(x1, x2) = [1 0] x1 + [1 2] x2 + [0]
                             [0 1]      [0 1]      [1]
              0() = [0]
                    [0]
              zeros() = [0]
                        [0]
              a__tail(x1) = [1 3] x1 + [2]
                            [0 1]      [3]
              mark(x1) = [1 2] x1 + [3]
                         [0 1]      [1]
              tail(x1) = [1 3] x1 + [0]
                         [0 1]      [3]
              a__zeros^#() = [0]
                             [0]
              c_0() = [0]
                      [0]
              a__tail^#(x1) = [3 0] x1 + [0]
                              [0 0]      [0]
              c_1(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              mark^#(x1) = [0 0] x1 + [0]
                           [0 0]      [0]
              c_2(x1) = [0 0] x1 + [0]
                        [0 0]      [0]
              c_3(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              c_4(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              c_5() = [0]
                      [0]
              c_6() = [0]
                      [0]
              c_7() = [0]
                      [0]
           Complexity induced by the adequate RMI: YES(?,O(n^2))

           We apply the sub-processor on the resulting sub-problem:

           'matrix-interpretation of dimension 2'
           --------------------------------------
           Answer:           YES(?,O(n^1))
           Input Problem:    innermost DP runtime-complexity with respect to
             Strict Rules: {mark^#(0()) -> c_5()}
             Weak Rules:
               {  a__tail^#(cons(X, XS)) -> c_1(mark^#(XS))
                , mark^#(tail(X)) -> c_3(a__tail^#(mark(X)))
                , mark^#(cons(X1, X2)) -> c_4(mark^#(X1))
                , mark(zeros()) -> a__zeros()
                , mark(tail(X)) -> a__tail(mark(X))
                , mark(cons(X1, X2)) -> cons(mark(X1), X2)
                , mark(0()) -> 0()
                , a__zeros() -> cons(0(), zeros())
                , a__tail(cons(X, XS)) -> mark(XS)
                , a__zeros() -> zeros()
                , a__tail(X) -> tail(X)}

           Proof Output:
             The following argument positions are usable:
               Uargs(cons) = {}, Uargs(a__tail) = {}, Uargs(mark) = {},
               Uargs(tail) = {}, Uargs(a__tail^#) = {}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(c_3) = {1}, Uargs(c_4) = {1}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__zeros() = [4]
                           [1]
              cons(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                             [0 0]      [0 0]      [0]
              0() = [2]
                    [0]
              zeros() = [2]
                        [0]
              a__tail(x1) = [1 0] x1 + [4]
                            [2 0]      [2]
              mark(x1) = [1 0] x1 + [2]
                         [2 0]      [0]
              tail(x1) = [1 0] x1 + [4]
                         [0 0]      [0]
              a__tail^#(x1) = [2 0] x1 + [0]
                              [0 0]      [0]
              c_1(x1) = [1 0] x1 + [0]
                        [0 0]      [0]
              mark^#(x1) = [2 0] x1 + [0]
                           [0 0]      [0]
              c_3(x1) = [1 0] x1 + [3]
                        [0 0]      [0]
              c_4(x1) = [1 0] x1 + [0]
                        [0 0]      [0]
              c_5() = [1]
                      [0]

         * Path {2,4,5}->{8}: YES(?,O(n^2))
           --------------------------------

           The usable rules for this path are:

             {  mark(zeros()) -> a__zeros()
              , mark(tail(X)) -> a__tail(mark(X))
              , mark(cons(X1, X2)) -> cons(mark(X1), X2)
              , mark(0()) -> 0()
              , a__zeros() -> cons(0(), zeros())
              , a__tail(cons(X, XS)) -> mark(XS)
              , a__zeros() -> zeros()
              , a__tail(X) -> tail(X)}

           The weightgap principle applies, using the following adequate RMI:
             The following argument positions are usable:
               Uargs(cons) = {1}, Uargs(a__tail) = {1}, Uargs(mark) = {},
               Uargs(tail) = {}, Uargs(a__tail^#) = {1}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(c_2) = {}, Uargs(c_3) = {1},
               Uargs(c_4) = {1}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__zeros() = [1]
                           [1]
              cons(x1, x2) = [1 0] x1 + [1 2] x2 + [0]
                             [0 1]      [0 1]      [1]
              0() = [0]
                    [0]
              zeros() = [0]
                        [0]
              a__tail(x1) = [1 3] x1 + [2]
                            [0 1]      [3]
              mark(x1) = [1 2] x1 + [3]
                         [0 1]      [1]
              tail(x1) = [1 3] x1 + [0]
                         [0 1]      [3]
              a__zeros^#() = [0]
                             [0]
              c_0() = [0]
                      [0]
              a__tail^#(x1) = [3 0] x1 + [0]
                              [0 0]      [0]
              c_1(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              mark^#(x1) = [0 0] x1 + [0]
                           [0 0]      [0]
              c_2(x1) = [0 0] x1 + [0]
                        [0 0]      [0]
              c_3(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              c_4(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              c_5() = [0]
                      [0]
              c_6() = [0]
                      [0]
              c_7() = [0]
                      [0]
           Complexity induced by the adequate RMI: YES(?,O(n^2))

           We apply the sub-processor on the resulting sub-problem:

           'matrix-interpretation of dimension 2'
           --------------------------------------
           Answer:           YES(?,O(n^1))
           Input Problem:    innermost DP runtime-complexity with respect to
             Strict Rules: {a__tail^#(X) -> c_7()}
             Weak Rules:
               {  a__tail^#(cons(X, XS)) -> c_1(mark^#(XS))
                , mark^#(tail(X)) -> c_3(a__tail^#(mark(X)))
                , mark^#(cons(X1, X2)) -> c_4(mark^#(X1))
                , mark(zeros()) -> a__zeros()
                , mark(tail(X)) -> a__tail(mark(X))
                , mark(cons(X1, X2)) -> cons(mark(X1), X2)
                , mark(0()) -> 0()
                , a__zeros() -> cons(0(), zeros())
                , a__tail(cons(X, XS)) -> mark(XS)
                , a__zeros() -> zeros()
                , a__tail(X) -> tail(X)}

           Proof Output:
             The following argument positions are usable:
               Uargs(cons) = {}, Uargs(a__tail) = {}, Uargs(mark) = {},
               Uargs(tail) = {}, Uargs(a__tail^#) = {}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(c_3) = {1}, Uargs(c_4) = {1}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__zeros() = [0]
                           [0]
              cons(x1, x2) = [0 0] x1 + [0 2] x2 + [0]
                             [0 1]      [0 1]      [0]
              0() = [0]
                    [0]
              zeros() = [0]
                        [0]
              a__tail(x1) = [0 2] x1 + [0]
                            [0 1]      [0]
              mark(x1) = [0 2] x1 + [0]
                         [0 1]      [0]
              tail(x1) = [0 0] x1 + [0]
                         [0 1]      [0]
              a__tail^#(x1) = [2 0] x1 + [1]
                              [0 1]      [0]
              c_1(x1) = [1 0] x1 + [0]
                        [0 0]      [0]
              mark^#(x1) = [0 4] x1 + [1]
                           [0 0]      [0]
              c_3(x1) = [1 0] x1 + [0]
                        [0 0]      [0]
              c_4(x1) = [1 0] x1 + [0]
                        [0 0]      [0]
              c_7() = [0]
                      [0]

Tool RC1

Execution Time	Unknown
Answer	YES(?,O(n^3))
Input	Transformed CSR 04 Ex4 7 77 Bor03 GM

stdout:

YES(?,O(n^3))

Tool RC2

Execution Time	Unknown
Answer	YES(?,O(n^2))
Input	Transformed CSR 04 Ex4 7 77 Bor03 GM

stdout:

YES(?,O(n^2))

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           YES(?,O(n^2))
Input Problem:    runtime-complexity with respect to
  Rules:
    {  a__zeros() -> cons(0(), zeros())
     , a__tail(cons(X, XS)) -> mark(XS)
     , mark(zeros()) -> a__zeros()
     , mark(tail(X)) -> a__tail(mark(X))
     , mark(cons(X1, X2)) -> cons(mark(X1), X2)
     , mark(0()) -> 0()
     , a__zeros() -> zeros()
     , a__tail(X) -> tail(X)}

Proof Output:
  'wdg' proved the best result:

  Details:
  --------
    'wdg' succeeded with the following output:
     'wdg'
     -----
     Answer:           YES(?,O(n^2))
     Input Problem:    runtime-complexity with respect to
       Rules:
         {  a__zeros() -> cons(0(), zeros())
          , a__tail(cons(X, XS)) -> mark(XS)
          , mark(zeros()) -> a__zeros()
          , mark(tail(X)) -> a__tail(mark(X))
          , mark(cons(X1, X2)) -> cons(mark(X1), X2)
          , mark(0()) -> 0()
          , a__zeros() -> zeros()
          , a__tail(X) -> tail(X)}

     Proof Output:
       Transformation Details:
       -----------------------
         We have computed the following set of weak (innermost) dependency pairs:

           {  1: a__zeros^#() -> c_0()
            , 2: a__tail^#(cons(X, XS)) -> c_1(mark^#(XS))
            , 3: mark^#(zeros()) -> c_2(a__zeros^#())
            , 4: mark^#(tail(X)) -> c_3(a__tail^#(mark(X)))
            , 5: mark^#(cons(X1, X2)) -> c_4(mark^#(X1), X2)
            , 6: mark^#(0()) -> c_5()
            , 7: a__zeros^#() -> c_6()
            , 8: a__tail^#(X) -> c_7(X)}

         Following Dependency Graph (modulo SCCs) was computed. (Answers to
         subproofs are indicated to the right.)

           ->{2,4,5}                                                   [   YES(?,O(n^2))    ]
              |
              |->{3}                                                   [   YES(?,O(n^2))    ]
              |   |
              |   |->{1}                                               [   YES(?,O(n^2))    ]
              |   |
              |   `->{7}                                               [   YES(?,O(n^2))    ]
              |
              |->{6}                                                   [   YES(?,O(n^2))    ]
              |
              `->{8}                                                   [   YES(?,O(n^2))    ]



       Sub-problems:
       -------------
         * Path {2,4,5}: YES(?,O(n^2))
           ---------------------------

           The usable rules for this path are:

             {  mark(zeros()) -> a__zeros()
              , mark(tail(X)) -> a__tail(mark(X))
              , mark(cons(X1, X2)) -> cons(mark(X1), X2)
              , mark(0()) -> 0()
              , a__zeros() -> cons(0(), zeros())
              , a__tail(cons(X, XS)) -> mark(XS)
              , a__zeros() -> zeros()
              , a__tail(X) -> tail(X)}

           The weightgap principle applies, using the following adequate RMI:
             The following argument positions are usable:
               Uargs(cons) = {1}, Uargs(a__tail) = {1}, Uargs(mark) = {},
               Uargs(tail) = {1}, Uargs(a__tail^#) = {1}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(c_2) = {}, Uargs(c_3) = {1},
               Uargs(c_4) = {1}, Uargs(c_7) = {}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__zeros() = [1]
                           [2]
              cons(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                             [0 1]      [0 1]      [1]
              0() = [0]
                    [0]
              zeros() = [0]
                        [1]
              a__tail(x1) = [1 1] x1 + [2]
                            [0 1]      [3]
              mark(x1) = [1 1] x1 + [1]
                         [0 1]      [1]
              tail(x1) = [1 1] x1 + [1]
                         [0 1]      [3]
              a__zeros^#() = [0]
                             [0]
              c_0() = [0]
                      [0]
              a__tail^#(x1) = [2 1] x1 + [0]
                              [3 3]      [0]
              c_1(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              mark^#(x1) = [2 1] x1 + [0]
                           [3 3]      [0]
              c_2(x1) = [0 0] x1 + [0]
                        [0 0]      [0]
              c_3(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              c_4(x1, x2) = [1 0] x1 + [0 1] x2 + [0]
                            [0 1]      [0 0]      [0]
              c_5() = [0]
                      [0]
              c_6() = [0]
                      [0]
              c_7(x1) = [0 0] x1 + [0]
                        [0 0]      [0]
           Complexity induced by the adequate RMI: YES(?,O(n^2))

           We apply the sub-processor on the resulting sub-problem:

           'matrix-interpretation of dimension 2'
           --------------------------------------
           Answer:           YES(?,O(n^1))
           Input Problem:    DP runtime-complexity with respect to
             Strict Rules:
               {  a__tail^#(cons(X, XS)) -> c_1(mark^#(XS))
                , mark^#(tail(X)) -> c_3(a__tail^#(mark(X)))
                , mark^#(cons(X1, X2)) -> c_4(mark^#(X1), X2)}
             Weak Rules:
               {  mark(zeros()) -> a__zeros()
                , mark(tail(X)) -> a__tail(mark(X))
                , mark(cons(X1, X2)) -> cons(mark(X1), X2)
                , mark(0()) -> 0()
                , a__zeros() -> cons(0(), zeros())
                , a__tail(cons(X, XS)) -> mark(XS)
                , a__zeros() -> zeros()
                , a__tail(X) -> tail(X)}

           Proof Output:
             The following argument positions are usable:
               Uargs(cons) = {}, Uargs(a__tail) = {}, Uargs(mark) = {},
               Uargs(tail) = {}, Uargs(a__tail^#) = {}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(c_3) = {1}, Uargs(c_4) = {1}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__zeros() = [2]
                           [4]
              cons(x1, x2) = [0 0] x1 + [0 2] x2 + [0]
                             [0 1]      [0 1]      [2]
              0() = [0]
                    [0]
              zeros() = [0]
                        [1]
              a__tail(x1) = [1 0] x1 + [1]
                            [0 1]      [1]
              mark(x1) = [0 2] x1 + [0]
                         [0 1]      [3]
              tail(x1) = [1 0] x1 + [1]
                         [0 1]      [1]
              a__tail^#(x1) = [2 0] x1 + [1]
                              [0 2]      [0]
              c_1(x1) = [1 0] x1 + [0]
                        [0 0]      [3]
              mark^#(x1) = [0 4] x1 + [0]
                           [5 4]      [3]
              c_3(x1) = [1 0] x1 + [1]
                        [0 2]      [0]
              c_4(x1, x2) = [1 0] x1 + [0 0] x2 + [5]
                            [0 0]      [0 0]      [7]

         * Path {2,4,5}->{3}: YES(?,O(n^2))
           --------------------------------

           The usable rules for this path are:

             {  mark(zeros()) -> a__zeros()
              , mark(tail(X)) -> a__tail(mark(X))
              , mark(cons(X1, X2)) -> cons(mark(X1), X2)
              , mark(0()) -> 0()
              , a__zeros() -> cons(0(), zeros())
              , a__tail(cons(X, XS)) -> mark(XS)
              , a__zeros() -> zeros()
              , a__tail(X) -> tail(X)}

           The weightgap principle applies, using the following adequate RMI:
             The following argument positions are usable:
               Uargs(cons) = {1}, Uargs(a__tail) = {1}, Uargs(mark) = {},
               Uargs(tail) = {1}, Uargs(a__tail^#) = {1}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(c_2) = {}, Uargs(c_3) = {1},
               Uargs(c_4) = {1}, Uargs(c_7) = {}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__zeros() = [1]
                           [3]
              cons(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                             [0 1]      [0 1]      [1]
              0() = [0]
                    [1]
              zeros() = [0]
                        [1]
              a__tail(x1) = [1 2] x1 + [3]
                            [0 1]      [3]
              mark(x1) = [1 2] x1 + [0]
                         [0 1]      [2]
              tail(x1) = [1 2] x1 + [2]
                         [0 1]      [3]
              a__zeros^#() = [0]
                             [0]
              c_0() = [0]
                      [0]
              a__tail^#(x1) = [3 0] x1 + [0]
                              [0 0]      [0]
              c_1(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              mark^#(x1) = [0 0] x1 + [0]
                           [0 0]      [0]
              c_2(x1) = [0 0] x1 + [0]
                        [0 0]      [0]
              c_3(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              c_4(x1, x2) = [1 0] x1 + [0 0] x2 + [0]
                            [0 1]      [0 0]      [0]
              c_5() = [0]
                      [0]
              c_6() = [0]
                      [0]
              c_7(x1) = [0 0] x1 + [0]
                        [0 0]      [0]
           Complexity induced by the adequate RMI: YES(?,O(n^2))

           We apply the sub-processor on the resulting sub-problem:

           'matrix-interpretation of dimension 2'
           --------------------------------------
           Answer:           YES(?,O(n^2))
           Input Problem:    DP runtime-complexity with respect to
             Strict Rules: {mark^#(zeros()) -> c_2(a__zeros^#())}
             Weak Rules:
               {  a__tail^#(cons(X, XS)) -> c_1(mark^#(XS))
                , mark^#(tail(X)) -> c_3(a__tail^#(mark(X)))
                , mark^#(cons(X1, X2)) -> c_4(mark^#(X1), X2)
                , mark(zeros()) -> a__zeros()
                , mark(tail(X)) -> a__tail(mark(X))
                , mark(cons(X1, X2)) -> cons(mark(X1), X2)
                , mark(0()) -> 0()
                , a__zeros() -> cons(0(), zeros())
                , a__tail(cons(X, XS)) -> mark(XS)
                , a__zeros() -> zeros()
                , a__tail(X) -> tail(X)}

           Proof Output:
             The following argument positions are usable:
               Uargs(cons) = {}, Uargs(a__tail) = {}, Uargs(mark) = {},
               Uargs(tail) = {}, Uargs(a__tail^#) = {}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(c_2) = {}, Uargs(c_3) = {1},
               Uargs(c_4) = {1}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__zeros() = [6]
                           [5]
              cons(x1, x2) = [1 0] x1 + [1 2] x2 + [0]
                             [0 1]      [0 1]      [3]
              0() = [0]
                    [0]
              zeros() = [2]
                        [2]
              a__tail(x1) = [1 3] x1 + [0]
                            [0 1]      [5]
              mark(x1) = [1 2] x1 + [0]
                         [0 1]      [3]
              tail(x1) = [1 3] x1 + [0]
                         [0 1]      [5]
              a__zeros^#() = [0]
                             [2]
              a__tail^#(x1) = [2 5] x1 + [0]
                              [0 5]      [0]
              c_1(x1) = [1 0] x1 + [6]
                        [0 0]      [3]
              mark^#(x1) = [2 3] x1 + [0]
                           [2 2]      [0]
              c_2(x1) = [0 2] x1 + [1]
                        [0 2]      [3]
              c_3(x1) = [1 0] x1 + [0]
                        [0 0]      [7]
              c_4(x1, x2) = [1 0] x1 + [0 1] x2 + [7]
                            [0 0]      [0 0]      [2]

         * Path {2,4,5}->{3}->{1}: YES(?,O(n^2))
           -------------------------------------

           The usable rules for this path are:

             {  mark(zeros()) -> a__zeros()
              , mark(tail(X)) -> a__tail(mark(X))
              , mark(cons(X1, X2)) -> cons(mark(X1), X2)
              , mark(0()) -> 0()
              , a__zeros() -> cons(0(), zeros())
              , a__tail(cons(X, XS)) -> mark(XS)
              , a__zeros() -> zeros()
              , a__tail(X) -> tail(X)}

           The weightgap principle applies, using the following adequate RMI:
             The following argument positions are usable:
               Uargs(cons) = {1}, Uargs(a__tail) = {1}, Uargs(mark) = {},
               Uargs(tail) = {1}, Uargs(a__tail^#) = {1}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(c_2) = {1}, Uargs(c_3) = {1},
               Uargs(c_4) = {1}, Uargs(c_7) = {}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__zeros() = [3]
                           [3]
              cons(x1, x2) = [1 0] x1 + [1 2] x2 + [0]
                             [0 1]      [0 1]      [1]
              0() = [0]
                    [1]
              zeros() = [0]
                        [1]
              a__tail(x1) = [1 1] x1 + [3]
                            [0 1]      [2]
              mark(x1) = [1 3] x1 + [1]
                         [0 1]      [3]
              tail(x1) = [1 1] x1 + [1]
                         [0 1]      [2]
              a__zeros^#() = [0]
                             [0]
              c_0() = [0]
                      [0]
              a__tail^#(x1) = [3 0] x1 + [0]
                              [0 0]      [0]
              c_1(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              mark^#(x1) = [0 0] x1 + [0]
                           [0 0]      [0]
              c_2(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              c_3(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              c_4(x1, x2) = [1 0] x1 + [0 0] x2 + [0]
                            [0 1]      [0 0]      [0]
              c_5() = [0]
                      [0]
              c_6() = [0]
                      [0]
              c_7(x1) = [0 0] x1 + [0]
                        [0 0]      [0]
           Complexity induced by the adequate RMI: YES(?,O(n^2))

           We apply the sub-processor on the resulting sub-problem:

           'matrix-interpretation of dimension 2'
           --------------------------------------
           Answer:           YES(?,O(n^2))
           Input Problem:    DP runtime-complexity with respect to
             Strict Rules: {a__zeros^#() -> c_0()}
             Weak Rules:
               {  mark^#(zeros()) -> c_2(a__zeros^#())
                , a__tail^#(cons(X, XS)) -> c_1(mark^#(XS))
                , mark^#(tail(X)) -> c_3(a__tail^#(mark(X)))
                , mark^#(cons(X1, X2)) -> c_4(mark^#(X1), X2)
                , mark(zeros()) -> a__zeros()
                , mark(tail(X)) -> a__tail(mark(X))
                , mark(cons(X1, X2)) -> cons(mark(X1), X2)
                , mark(0()) -> 0()
                , a__zeros() -> cons(0(), zeros())
                , a__tail(cons(X, XS)) -> mark(XS)
                , a__zeros() -> zeros()
                , a__tail(X) -> tail(X)}

           Proof Output:
             The following argument positions are usable:
               Uargs(cons) = {}, Uargs(a__tail) = {}, Uargs(mark) = {},
               Uargs(tail) = {}, Uargs(a__tail^#) = {}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(c_2) = {1}, Uargs(c_3) = {1},
               Uargs(c_4) = {1}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__zeros() = [6]
                           [2]
              cons(x1, x2) = [1 3] x1 + [1 2] x2 + [0]
                             [0 1]      [0 1]      [0]
              0() = [0]
                    [0]
              zeros() = [2]
                        [2]
              a__tail(x1) = [1 0] x1 + [6]
                            [0 1]      [0]
              mark(x1) = [1 1] x1 + [2]
                         [0 1]      [0]
              tail(x1) = [1 0] x1 + [6]
                         [0 1]      [0]
              a__zeros^#() = [2]
                             [2]
              c_0() = [1]
                      [0]
              a__tail^#(x1) = [2 0] x1 + [4]
                              [4 1]      [0]
              c_1(x1) = [1 0] x1 + [3]
                        [0 0]      [0]
              mark^#(x1) = [2 3] x1 + [0]
                           [2 2]      [0]
              c_2(x1) = [2 0] x1 + [2]
                        [2 2]      [0]
              c_3(x1) = [1 0] x1 + [3]
                        [0 0]      [7]
              c_4(x1, x2) = [1 0] x1 + [0 1] x2 + [0]
                            [0 0]      [0 0]      [0]

         * Path {2,4,5}->{3}->{7}: YES(?,O(n^2))
           -------------------------------------

           The usable rules for this path are:

             {  mark(zeros()) -> a__zeros()
              , mark(tail(X)) -> a__tail(mark(X))
              , mark(cons(X1, X2)) -> cons(mark(X1), X2)
              , mark(0()) -> 0()
              , a__zeros() -> cons(0(), zeros())
              , a__tail(cons(X, XS)) -> mark(XS)
              , a__zeros() -> zeros()
              , a__tail(X) -> tail(X)}

           The weightgap principle applies, using the following adequate RMI:
             The following argument positions are usable:
               Uargs(cons) = {1}, Uargs(a__tail) = {1}, Uargs(mark) = {},
               Uargs(tail) = {1}, Uargs(a__tail^#) = {1}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(c_2) = {1}, Uargs(c_3) = {1},
               Uargs(c_4) = {1}, Uargs(c_7) = {}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__zeros() = [3]
                           [3]
              cons(x1, x2) = [1 0] x1 + [1 2] x2 + [0]
                             [0 1]      [0 1]      [1]
              0() = [0]
                    [1]
              zeros() = [0]
                        [1]
              a__tail(x1) = [1 1] x1 + [3]
                            [0 1]      [2]
              mark(x1) = [1 3] x1 + [1]
                         [0 1]      [3]
              tail(x1) = [1 1] x1 + [1]
                         [0 1]      [2]
              a__zeros^#() = [0]
                             [0]
              c_0() = [0]
                      [0]
              a__tail^#(x1) = [3 0] x1 + [0]
                              [0 0]      [0]
              c_1(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              mark^#(x1) = [0 0] x1 + [0]
                           [0 0]      [0]
              c_2(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              c_3(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              c_4(x1, x2) = [1 0] x1 + [0 0] x2 + [0]
                            [0 1]      [0 0]      [0]
              c_5() = [0]
                      [0]
              c_6() = [0]
                      [0]
              c_7(x1) = [0 0] x1 + [0]
                        [0 0]      [0]
           Complexity induced by the adequate RMI: YES(?,O(n^2))

           We apply the sub-processor on the resulting sub-problem:

           'matrix-interpretation of dimension 2'
           --------------------------------------
           Answer:           YES(?,O(n^2))
           Input Problem:    DP runtime-complexity with respect to
             Strict Rules: {a__zeros^#() -> c_6()}
             Weak Rules:
               {  mark^#(zeros()) -> c_2(a__zeros^#())
                , a__tail^#(cons(X, XS)) -> c_1(mark^#(XS))
                , mark^#(tail(X)) -> c_3(a__tail^#(mark(X)))
                , mark^#(cons(X1, X2)) -> c_4(mark^#(X1), X2)
                , mark(zeros()) -> a__zeros()
                , mark(tail(X)) -> a__tail(mark(X))
                , mark(cons(X1, X2)) -> cons(mark(X1), X2)
                , mark(0()) -> 0()
                , a__zeros() -> cons(0(), zeros())
                , a__tail(cons(X, XS)) -> mark(XS)
                , a__zeros() -> zeros()
                , a__tail(X) -> tail(X)}

           Proof Output:
             The following argument positions are usable:
               Uargs(cons) = {}, Uargs(a__tail) = {}, Uargs(mark) = {},
               Uargs(tail) = {}, Uargs(a__tail^#) = {}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(c_2) = {1}, Uargs(c_3) = {1},
               Uargs(c_4) = {1}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__zeros() = [6]
                           [2]
              cons(x1, x2) = [1 3] x1 + [1 2] x2 + [0]
                             [0 1]      [0 1]      [0]
              0() = [0]
                    [0]
              zeros() = [2]
                        [2]
              a__tail(x1) = [1 0] x1 + [6]
                            [0 1]      [0]
              mark(x1) = [1 1] x1 + [2]
                         [0 1]      [0]
              tail(x1) = [1 0] x1 + [6]
                         [0 1]      [0]
              a__zeros^#() = [2]
                             [2]
              a__tail^#(x1) = [2 0] x1 + [4]
                              [4 1]      [0]
              c_1(x1) = [1 0] x1 + [3]
                        [0 0]      [0]
              mark^#(x1) = [2 3] x1 + [0]
                           [2 2]      [0]
              c_2(x1) = [2 0] x1 + [2]
                        [2 2]      [0]
              c_3(x1) = [1 0] x1 + [3]
                        [0 0]      [7]
              c_4(x1, x2) = [1 0] x1 + [0 1] x2 + [0]
                            [0 0]      [0 0]      [0]
              c_6() = [1]
                      [0]

         * Path {2,4,5}->{6}: YES(?,O(n^2))
           --------------------------------

           The usable rules for this path are:

             {  mark(zeros()) -> a__zeros()
              , mark(tail(X)) -> a__tail(mark(X))
              , mark(cons(X1, X2)) -> cons(mark(X1), X2)
              , mark(0()) -> 0()
              , a__zeros() -> cons(0(), zeros())
              , a__tail(cons(X, XS)) -> mark(XS)
              , a__zeros() -> zeros()
              , a__tail(X) -> tail(X)}

           The weightgap principle applies, using the following adequate RMI:
             The following argument positions are usable:
               Uargs(cons) = {1}, Uargs(a__tail) = {1}, Uargs(mark) = {},
               Uargs(tail) = {1}, Uargs(a__tail^#) = {1}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(c_2) = {}, Uargs(c_3) = {1},
               Uargs(c_4) = {1}, Uargs(c_7) = {}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__zeros() = [1]
                           [3]
              cons(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                             [0 1]      [0 1]      [1]
              0() = [0]
                    [1]
              zeros() = [0]
                        [1]
              a__tail(x1) = [1 2] x1 + [3]
                            [0 1]      [3]
              mark(x1) = [1 2] x1 + [0]
                         [0 1]      [2]
              tail(x1) = [1 2] x1 + [2]
                         [0 1]      [3]
              a__zeros^#() = [0]
                             [0]
              c_0() = [0]
                      [0]
              a__tail^#(x1) = [3 0] x1 + [0]
                              [0 0]      [0]
              c_1(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              mark^#(x1) = [0 0] x1 + [0]
                           [0 0]      [0]
              c_2(x1) = [0 0] x1 + [0]
                        [0 0]      [0]
              c_3(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              c_4(x1, x2) = [1 0] x1 + [0 0] x2 + [0]
                            [0 1]      [0 0]      [0]
              c_5() = [0]
                      [0]
              c_6() = [0]
                      [0]
              c_7(x1) = [0 0] x1 + [0]
                        [0 0]      [0]
           Complexity induced by the adequate RMI: YES(?,O(n^2))

           We apply the sub-processor on the resulting sub-problem:

           'matrix-interpretation of dimension 2'
           --------------------------------------
           Answer:           YES(?,O(n^1))
           Input Problem:    DP runtime-complexity with respect to
             Strict Rules: {mark^#(0()) -> c_5()}
             Weak Rules:
               {  a__tail^#(cons(X, XS)) -> c_1(mark^#(XS))
                , mark^#(tail(X)) -> c_3(a__tail^#(mark(X)))
                , mark^#(cons(X1, X2)) -> c_4(mark^#(X1), X2)
                , mark(zeros()) -> a__zeros()
                , mark(tail(X)) -> a__tail(mark(X))
                , mark(cons(X1, X2)) -> cons(mark(X1), X2)
                , mark(0()) -> 0()
                , a__zeros() -> cons(0(), zeros())
                , a__tail(cons(X, XS)) -> mark(XS)
                , a__zeros() -> zeros()
                , a__tail(X) -> tail(X)}

           Proof Output:
             The following argument positions are usable:
               Uargs(cons) = {}, Uargs(a__tail) = {}, Uargs(mark) = {},
               Uargs(tail) = {}, Uargs(a__tail^#) = {}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(c_3) = {1}, Uargs(c_4) = {1}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__zeros() = [0]
                           [3]
              cons(x1, x2) = [0 0] x1 + [0 1] x2 + [0]
                             [0 1]      [0 1]      [0]
              0() = [0]
                    [2]
              zeros() = [0]
                        [0]
              a__tail(x1) = [1 0] x1 + [0]
                            [0 1]      [4]
              mark(x1) = [0 1] x1 + [0]
                         [0 1]      [4]
              tail(x1) = [1 0] x1 + [0]
                         [0 1]      [4]
              a__tail^#(x1) = [1 0] x1 + [0]
                              [0 4]      [0]
              c_1(x1) = [1 0] x1 + [0]
                        [0 0]      [0]
              mark^#(x1) = [0 1] x1 + [0]
                           [4 0]      [4]
              c_3(x1) = [1 0] x1 + [2]
                        [0 0]      [3]
              c_4(x1, x2) = [1 0] x1 + [0 1] x2 + [0]
                            [0 0]      [0 0]      [4]
              c_5() = [1]
                      [0]

         * Path {2,4,5}->{8}: YES(?,O(n^2))
           --------------------------------

           The usable rules for this path are:

             {  mark(zeros()) -> a__zeros()
              , mark(tail(X)) -> a__tail(mark(X))
              , mark(cons(X1, X2)) -> cons(mark(X1), X2)
              , mark(0()) -> 0()
              , a__zeros() -> cons(0(), zeros())
              , a__tail(cons(X, XS)) -> mark(XS)
              , a__zeros() -> zeros()
              , a__tail(X) -> tail(X)}

           The weightgap principle applies, using the following adequate RMI:
             The following argument positions are usable:
               Uargs(cons) = {1}, Uargs(a__tail) = {1}, Uargs(mark) = {},
               Uargs(tail) = {1}, Uargs(a__tail^#) = {1}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(c_2) = {}, Uargs(c_3) = {1},
               Uargs(c_4) = {1}, Uargs(c_7) = {1}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__zeros() = [1]
                           [3]
              cons(x1, x2) = [1 0] x1 + [1 1] x2 + [0]
                             [0 1]      [0 1]      [2]
              0() = [0]
                    [1]
              zeros() = [0]
                        [0]
              a__tail(x1) = [1 2] x1 + [1]
                            [0 1]      [3]
              mark(x1) = [1 3] x1 + [2]
                         [0 1]      [3]
              tail(x1) = [1 2] x1 + [0]
                         [0 1]      [3]
              a__zeros^#() = [0]
                             [0]
              c_0() = [0]
                      [0]
              a__tail^#(x1) = [3 3] x1 + [0]
                              [0 0]      [0]
              c_1(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              mark^#(x1) = [0 0] x1 + [0]
                           [0 0]      [0]
              c_2(x1) = [0 0] x1 + [0]
                        [0 0]      [0]
              c_3(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              c_4(x1, x2) = [1 0] x1 + [0 0] x2 + [0]
                            [0 1]      [0 0]      [0]
              c_5() = [0]
                      [0]
              c_6() = [0]
                      [0]
              c_7(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
           Complexity induced by the adequate RMI: YES(?,O(n^2))

           We apply the sub-processor on the resulting sub-problem:

           'matrix-interpretation of dimension 2'
           --------------------------------------
           Answer:           YES(?,O(n^1))
           Input Problem:    DP runtime-complexity with respect to
             Strict Rules: {a__tail^#(X) -> c_7(X)}
             Weak Rules:
               {  a__tail^#(cons(X, XS)) -> c_1(mark^#(XS))
                , mark^#(tail(X)) -> c_3(a__tail^#(mark(X)))
                , mark^#(cons(X1, X2)) -> c_4(mark^#(X1), X2)
                , mark(zeros()) -> a__zeros()
                , mark(tail(X)) -> a__tail(mark(X))
                , mark(cons(X1, X2)) -> cons(mark(X1), X2)
                , mark(0()) -> 0()
                , a__zeros() -> cons(0(), zeros())
                , a__tail(cons(X, XS)) -> mark(XS)
                , a__zeros() -> zeros()
                , a__tail(X) -> tail(X)}

           Proof Output:
             The following argument positions are usable:
               Uargs(cons) = {}, Uargs(a__tail) = {}, Uargs(mark) = {},
               Uargs(tail) = {}, Uargs(a__tail^#) = {}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(c_3) = {1}, Uargs(c_4) = {1},
               Uargs(c_7) = {1}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__zeros() = [0]
                           [0]
              cons(x1, x2) = [0 0] x1 + [0 2] x2 + [0]
                             [0 1]      [0 1]      [0]
              0() = [0]
                    [0]
              zeros() = [0]
                        [0]
              a__tail(x1) = [1 0] x1 + [0]
                            [0 1]      [0]
              mark(x1) = [0 2] x1 + [0]
                         [0 1]      [0]
              tail(x1) = [1 0] x1 + [0]
                         [0 1]      [0]
              a__tail^#(x1) = [2 0] x1 + [2]
                              [1 7]      [0]
              c_1(x1) = [1 0] x1 + [0]
                        [0 0]      [0]
              mark^#(x1) = [0 4] x1 + [2]
                           [0 1]      [0]
              c_3(x1) = [1 0] x1 + [0]
                        [0 0]      [0]
              c_4(x1, x2) = [1 0] x1 + [0 0] x2 + [0]
                            [0 0]      [0 1]      [0]
              c_7(x1) = [1 0] x1 + [1]
                        [1 1]      [0]