Problem Transformed CSR 04 Ex6 Luc98 GM

Tool CaT

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 Ex6 Luc98 GM

stdout:

MAYBE

Problem:
a__first(0(),X) -> nil()
a__first(s(X),cons(Y,Z)) -> cons(mark(Y),first(X,Z))
a__from(X) -> cons(mark(X),from(s(X)))
mark(first(X1,X2)) -> a__first(mark(X1),mark(X2))
mark(from(X)) -> a__from(mark(X))
mark(0()) -> 0()
mark(nil()) -> nil()
mark(s(X)) -> s(mark(X))
mark(cons(X1,X2)) -> cons(mark(X1),X2)
a__first(X1,X2) -> first(X1,X2)
a__from(X) -> from(X)

Proof:
Open

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 Ex6 Luc98 GM

stdout:

MAYBE

Tool IRC2

Execution Time	Unknown
Answer	YES(?,O(n^2))
Input	Transformed CSR 04 Ex6 Luc98 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__first(0(), X) -> nil()
     , a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z))
     , a__from(X) -> cons(mark(X), from(s(X)))
     , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
     , mark(from(X)) -> a__from(mark(X))
     , mark(0()) -> 0()
     , mark(nil()) -> nil()
     , mark(s(X)) -> s(mark(X))
     , mark(cons(X1, X2)) -> cons(mark(X1), X2)
     , a__first(X1, X2) -> first(X1, X2)
     , a__from(X) -> from(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__first(0(), X) -> nil()
          , a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z))
          , a__from(X) -> cons(mark(X), from(s(X)))
          , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
          , mark(from(X)) -> a__from(mark(X))
          , mark(0()) -> 0()
          , mark(nil()) -> nil()
          , mark(s(X)) -> s(mark(X))
          , mark(cons(X1, X2)) -> cons(mark(X1), X2)
          , a__first(X1, X2) -> first(X1, X2)
          , a__from(X) -> from(X)}

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

           {  1: a__first^#(0(), X) -> c_0()
            , 2: a__first^#(s(X), cons(Y, Z)) -> c_1(mark^#(Y))
            , 3: a__from^#(X) -> c_2(mark^#(X))
            , 4: mark^#(first(X1, X2)) -> c_3(a__first^#(mark(X1), mark(X2)))
            , 5: mark^#(from(X)) -> c_4(a__from^#(mark(X)))
            , 6: mark^#(0()) -> c_5()
            , 7: mark^#(nil()) -> c_6()
            , 8: mark^#(s(X)) -> c_7(mark^#(X))
            , 9: mark^#(cons(X1, X2)) -> c_8(mark^#(X1))
            , 10: a__first^#(X1, X2) -> c_9()
            , 11: a__from^#(X) -> c_10()}

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

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



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

           The usable rules for this path are:

             {  mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
              , mark(from(X)) -> a__from(mark(X))
              , mark(0()) -> 0()
              , mark(nil()) -> nil()
              , mark(s(X)) -> s(mark(X))
              , mark(cons(X1, X2)) -> cons(mark(X1), X2)
              , a__first(0(), X) -> nil()
              , a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z))
              , a__from(X) -> cons(mark(X), from(s(X)))
              , a__first(X1, X2) -> first(X1, X2)
              , a__from(X) -> from(X)}

           The weightgap principle applies, using the following adequate RMI:
             The following argument positions are usable:
               Uargs(a__first) = {1, 2}, Uargs(s) = {1}, Uargs(cons) = {1},
               Uargs(mark) = {}, Uargs(first) = {}, Uargs(a__from) = {1},
               Uargs(from) = {}, Uargs(a__first^#) = {1, 2}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(a__from^#) = {1}, Uargs(c_2) = {1},
               Uargs(c_3) = {1}, Uargs(c_4) = {1}, Uargs(c_7) = {1},
               Uargs(c_8) = {1}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__first(x1, x2) = [1 0] x1 + [1 3] x2 + [3]
                                 [0 1]      [0 1]      [3]
              0() = [0]
                    [2]
              nil() = [0]
                      [1]
              s(x1) = [1 2] x1 + [0]
                      [0 1]      [2]
              cons(x1, x2) = [1 0] x1 + [0 0] x2 + [0]
                             [0 1]      [0 0]      [1]
              mark(x1) = [1 2] x1 + [0]
                         [0 1]      [0]
              first(x1, x2) = [1 0] x1 + [1 3] x2 + [2]
                              [0 1]      [0 1]      [3]
              a__from(x1) = [1 2] x1 + [1]
                            [0 1]      [2]
              from(x1) = [1 2] x1 + [0]
                         [0 1]      [2]
              a__first^#(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                                   [3 3]      [3 3]      [0]
              c_0() = [0]
                      [0]
              c_1(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              mark^#(x1) = [1 2] x1 + [0]
                           [3 3]      [0]
              a__from^#(x1) = [1 2] x1 + [0]
                              [3 3]      [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(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              c_8(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              c_9() = [0]
                      [0]
              c_10() = [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__first^#(s(X), cons(Y, Z)) -> c_1(mark^#(Y))
                , mark^#(first(X1, X2)) -> c_3(a__first^#(mark(X1), mark(X2)))
                , mark^#(cons(X1, X2)) -> c_8(mark^#(X1))
                , mark^#(s(X)) -> c_7(mark^#(X))
                , a__from^#(X) -> c_2(mark^#(X))
                , mark^#(from(X)) -> c_4(a__from^#(mark(X)))}
             Weak Rules:
               {  mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
                , mark(from(X)) -> a__from(mark(X))
                , mark(0()) -> 0()
                , mark(nil()) -> nil()
                , mark(s(X)) -> s(mark(X))
                , mark(cons(X1, X2)) -> cons(mark(X1), X2)
                , a__first(0(), X) -> nil()
                , a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z))
                , a__from(X) -> cons(mark(X), from(s(X)))
                , a__first(X1, X2) -> first(X1, X2)
                , a__from(X) -> from(X)}

           Proof Output:
             The following argument positions are usable:
               Uargs(a__first) = {}, Uargs(s) = {}, Uargs(cons) = {},
               Uargs(mark) = {}, Uargs(first) = {}, Uargs(a__from) = {},
               Uargs(from) = {}, Uargs(a__first^#) = {}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(a__from^#) = {}, Uargs(c_2) = {1},
               Uargs(c_3) = {1}, Uargs(c_4) = {1}, Uargs(c_7) = {1},
               Uargs(c_8) = {1}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__first(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
                                 [0 1]      [0 1]      [3]
              0() = [0]
                    [0]
              nil() = [0]
                      [0]
              s(x1) = [0 0] x1 + [0]
                      [0 1]      [2]
              cons(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
                             [0 1]      [0 0]      [1]
              mark(x1) = [4 4] x1 + [0]
                         [0 1]      [0]
              first(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                              [0 1]      [0 1]      [3]
              a__from(x1) = [0 0] x1 + [1]
                            [0 1]      [3]
              from(x1) = [0 0] x1 + [0]
                         [0 1]      [3]
              a__first^#(x1, x2) = [0 1] x1 + [0 1] x2 + [5]
                                   [0 4]      [0 0]      [0]
              c_1(x1) = [1 1] x1 + [1]
                        [0 0]      [3]
              mark^#(x1) = [0 1] x1 + [3]
                           [0 0]      [1]
              a__from^#(x1) = [0 1] x1 + [5]
                              [0 0]      [0]
              c_2(x1) = [1 1] x1 + [0]
                        [0 0]      [0]
              c_3(x1) = [1 0] x1 + [0]
                        [0 0]      [1]
              c_4(x1) = [1 0] x1 + [0]
                        [0 0]      [1]
              c_7(x1) = [1 0] x1 + [0]
                        [0 0]      [1]
              c_8(x1) = [1 0] x1 + [0]
                        [0 0]      [0]

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

           The usable rules for this path are:

             {  mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
              , mark(from(X)) -> a__from(mark(X))
              , mark(0()) -> 0()
              , mark(nil()) -> nil()
              , mark(s(X)) -> s(mark(X))
              , mark(cons(X1, X2)) -> cons(mark(X1), X2)
              , a__first(0(), X) -> nil()
              , a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z))
              , a__from(X) -> cons(mark(X), from(s(X)))
              , a__first(X1, X2) -> first(X1, X2)
              , a__from(X) -> from(X)}

           The weightgap principle applies, using the following adequate RMI:
             The following argument positions are usable:
               Uargs(a__first) = {1, 2}, Uargs(s) = {1}, Uargs(cons) = {1},
               Uargs(mark) = {}, Uargs(first) = {}, Uargs(a__from) = {1},
               Uargs(from) = {}, Uargs(a__first^#) = {1, 2}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(a__from^#) = {1}, Uargs(c_2) = {1},
               Uargs(c_3) = {1}, Uargs(c_4) = {1}, Uargs(c_7) = {1},
               Uargs(c_8) = {1}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__first(x1, x2) = [1 2] x1 + [1 3] x2 + [1]
                                 [0 1]      [0 1]      [1]
              0() = [0]
                    [2]
              nil() = [0]
                      [2]
              s(x1) = [1 2] x1 + [0]
                      [0 1]      [2]
              cons(x1, x2) = [1 0] x1 + [0 0] x2 + [0]
                             [0 1]      [0 0]      [2]
              mark(x1) = [1 2] x1 + [0]
                         [0 1]      [0]
              first(x1, x2) = [1 2] x1 + [1 3] x2 + [0]
                              [0 1]      [0 1]      [1]
              a__from(x1) = [1 2] x1 + [1]
                            [0 1]      [2]
              from(x1) = [1 2] x1 + [0]
                         [0 1]      [2]
              a__first^#(x1, x2) = [3 0] x1 + [3 0] x2 + [0]
                                   [0 0]      [0 0]      [0]
              c_0() = [0]
                      [0]
              c_1(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              mark^#(x1) = [0 0] x1 + [0]
                           [0 0]      [0]
              a__from^#(x1) = [3 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(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              c_8(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              c_9() = [0]
                      [0]
              c_10() = [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__first^#(0(), X) -> c_0()}
             Weak Rules:
               {  a__first^#(s(X), cons(Y, Z)) -> c_1(mark^#(Y))
                , mark^#(first(X1, X2)) -> c_3(a__first^#(mark(X1), mark(X2)))
                , mark^#(cons(X1, X2)) -> c_8(mark^#(X1))
                , mark^#(s(X)) -> c_7(mark^#(X))
                , a__from^#(X) -> c_2(mark^#(X))
                , mark^#(from(X)) -> c_4(a__from^#(mark(X)))
                , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
                , mark(from(X)) -> a__from(mark(X))
                , mark(0()) -> 0()
                , mark(nil()) -> nil()
                , mark(s(X)) -> s(mark(X))
                , mark(cons(X1, X2)) -> cons(mark(X1), X2)
                , a__first(0(), X) -> nil()
                , a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z))
                , a__from(X) -> cons(mark(X), from(s(X)))
                , a__first(X1, X2) -> first(X1, X2)
                , a__from(X) -> from(X)}

           Proof Output:
             The following argument positions are usable:
               Uargs(a__first) = {}, Uargs(s) = {}, Uargs(cons) = {},
               Uargs(mark) = {}, Uargs(first) = {}, Uargs(a__from) = {},
               Uargs(from) = {}, Uargs(a__first^#) = {}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(a__from^#) = {}, Uargs(c_2) = {1},
               Uargs(c_3) = {1}, Uargs(c_4) = {1}, Uargs(c_7) = {1},
               Uargs(c_8) = {1}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__first(x1, x2) = [1 4] x1 + [1 2] x2 + [0]
                                 [0 0]      [0 0]      [0]
              0() = [2]
                    [2]
              nil() = [0]
                      [0]
              s(x1) = [1 0] x1 + [0]
                      [0 1]      [2]
              cons(x1, x2) = [1 2] x1 + [0 0] x2 + [0]
                             [0 0]      [0 0]      [0]
              mark(x1) = [1 0] x1 + [0]
                         [0 1]      [0]
              first(x1, x2) = [1 4] x1 + [1 2] x2 + [0]
                              [0 0]      [0 0]      [0]
              a__from(x1) = [1 2] x1 + [0]
                            [0 0]      [2]
              from(x1) = [1 2] x1 + [0]
                         [0 0]      [2]
              a__first^#(x1, x2) = [2 2] x1 + [2 0] x2 + [0]
                                   [0 4]      [4 0]      [0]
              c_0() = [1]
                      [0]
              c_1(x1) = [1 0] x1 + [3]
                        [2 2]      [0]
              mark^#(x1) = [2 2] x1 + [0]
                           [0 2]      [4]
              a__from^#(x1) = [2 4] x1 + [4]
                              [0 0]      [0]
              c_2(x1) = [1 1] x1 + [0]
                        [0 0]      [0]
              c_3(x1) = [1 0] x1 + [0]
                        [0 0]      [3]
              c_4(x1) = [1 0] x1 + [0]
                        [0 0]      [7]
              c_7(x1) = [1 0] x1 + [2]
                        [0 0]      [7]
              c_8(x1) = [1 0] x1 + [0]
                        [0 0]      [3]

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

           The usable rules for this path are:

             {  mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
              , mark(from(X)) -> a__from(mark(X))
              , mark(0()) -> 0()
              , mark(nil()) -> nil()
              , mark(s(X)) -> s(mark(X))
              , mark(cons(X1, X2)) -> cons(mark(X1), X2)
              , a__first(0(), X) -> nil()
              , a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z))
              , a__from(X) -> cons(mark(X), from(s(X)))
              , a__first(X1, X2) -> first(X1, X2)
              , a__from(X) -> from(X)}

           The weightgap principle applies, using the following adequate RMI:
             The following argument positions are usable:
               Uargs(a__first) = {1, 2}, Uargs(s) = {1}, Uargs(cons) = {1},
               Uargs(mark) = {}, Uargs(first) = {}, Uargs(a__from) = {1},
               Uargs(from) = {}, Uargs(a__first^#) = {1, 2}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(a__from^#) = {1}, Uargs(c_2) = {1},
               Uargs(c_3) = {1}, Uargs(c_4) = {1}, Uargs(c_7) = {1},
               Uargs(c_8) = {1}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__first(x1, x2) = [1 2] x1 + [1 3] x2 + [1]
                                 [0 1]      [0 1]      [1]
              0() = [0]
                    [2]
              nil() = [0]
                      [2]
              s(x1) = [1 2] x1 + [0]
                      [0 1]      [2]
              cons(x1, x2) = [1 0] x1 + [0 0] x2 + [0]
                             [0 1]      [0 0]      [2]
              mark(x1) = [1 2] x1 + [0]
                         [0 1]      [0]
              first(x1, x2) = [1 2] x1 + [1 3] x2 + [0]
                              [0 1]      [0 1]      [1]
              a__from(x1) = [1 2] x1 + [1]
                            [0 1]      [2]
              from(x1) = [1 2] x1 + [0]
                         [0 1]      [2]
              a__first^#(x1, x2) = [3 0] x1 + [3 0] x2 + [0]
                                   [0 0]      [0 0]      [0]
              c_0() = [0]
                      [0]
              c_1(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              mark^#(x1) = [0 0] x1 + [0]
                           [0 0]      [0]
              a__from^#(x1) = [3 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(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              c_8(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              c_9() = [0]
                      [0]
              c_10() = [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__first^#(s(X), cons(Y, Z)) -> c_1(mark^#(Y))
                , mark^#(first(X1, X2)) -> c_3(a__first^#(mark(X1), mark(X2)))
                , mark^#(cons(X1, X2)) -> c_8(mark^#(X1))
                , mark^#(s(X)) -> c_7(mark^#(X))
                , a__from^#(X) -> c_2(mark^#(X))
                , mark^#(from(X)) -> c_4(a__from^#(mark(X)))
                , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
                , mark(from(X)) -> a__from(mark(X))
                , mark(0()) -> 0()
                , mark(nil()) -> nil()
                , mark(s(X)) -> s(mark(X))
                , mark(cons(X1, X2)) -> cons(mark(X1), X2)
                , a__first(0(), X) -> nil()
                , a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z))
                , a__from(X) -> cons(mark(X), from(s(X)))
                , a__first(X1, X2) -> first(X1, X2)
                , a__from(X) -> from(X)}

           Proof Output:
             The following argument positions are usable:
               Uargs(a__first) = {}, Uargs(s) = {}, Uargs(cons) = {},
               Uargs(mark) = {}, Uargs(first) = {}, Uargs(a__from) = {},
               Uargs(from) = {}, Uargs(a__first^#) = {}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(a__from^#) = {}, Uargs(c_2) = {1},
               Uargs(c_3) = {1}, Uargs(c_4) = {1}, Uargs(c_7) = {1},
               Uargs(c_8) = {1}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__first(x1, x2) = [0 0] x1 + [0 0] x2 + [4]
                                 [0 0]      [0 0]      [0]
              0() = [2]
                    [0]
              nil() = [0]
                      [0]
              s(x1) = [1 4] x1 + [0]
                      [0 0]      [0]
              cons(x1, x2) = [1 0] x1 + [0 0] x2 + [0]
                             [0 0]      [0 0]      [0]
              mark(x1) = [0 0] x1 + [4]
                         [0 0]      [0]
              first(x1, x2) = [0 0] x1 + [0 0] x2 + [4]
                              [0 0]      [0 0]      [0]
              a__from(x1) = [0 0] x1 + [4]
                            [0 0]      [0]
              from(x1) = [0 0] x1 + [4]
                         [0 0]      [0]
              a__first^#(x1, x2) = [0 0] x1 + [2 0] x2 + [0]
                                   [0 0]      [0 2]      [0]
              c_1(x1) = [1 0] x1 + [0]
                        [0 0]      [0]
              mark^#(x1) = [2 0] x1 + [0]
                           [2 0]      [0]
              a__from^#(x1) = [2 4] x1 + [0]
                              [4 4]      [0]
              c_2(x1) = [1 0] x1 + [0]
                        [0 0]      [0]
              c_3(x1) = [1 2] x1 + [0]
                        [0 0]      [7]
              c_4(x1) = [1 0] x1 + [0]
                        [0 0]      [7]
              c_5() = [1]
                      [0]
              c_7(x1) = [1 0] x1 + [0]
                        [0 0]      [0]
              c_8(x1) = [1 0] x1 + [0]
                        [0 0]      [0]

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

           The usable rules for this path are:

             {  mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
              , mark(from(X)) -> a__from(mark(X))
              , mark(0()) -> 0()
              , mark(nil()) -> nil()
              , mark(s(X)) -> s(mark(X))
              , mark(cons(X1, X2)) -> cons(mark(X1), X2)
              , a__first(0(), X) -> nil()
              , a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z))
              , a__from(X) -> cons(mark(X), from(s(X)))
              , a__first(X1, X2) -> first(X1, X2)
              , a__from(X) -> from(X)}

           The weightgap principle applies, using the following adequate RMI:
             The following argument positions are usable:
               Uargs(a__first) = {1, 2}, Uargs(s) = {1}, Uargs(cons) = {1},
               Uargs(mark) = {}, Uargs(first) = {}, Uargs(a__from) = {1},
               Uargs(from) = {}, Uargs(a__first^#) = {1, 2}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(a__from^#) = {1}, Uargs(c_2) = {1},
               Uargs(c_3) = {1}, Uargs(c_4) = {1}, Uargs(c_7) = {1},
               Uargs(c_8) = {1}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__first(x1, x2) = [1 2] x1 + [1 3] x2 + [1]
                                 [0 1]      [0 1]      [1]
              0() = [0]
                    [2]
              nil() = [0]
                      [2]
              s(x1) = [1 2] x1 + [0]
                      [0 1]      [2]
              cons(x1, x2) = [1 0] x1 + [0 0] x2 + [0]
                             [0 1]      [0 0]      [2]
              mark(x1) = [1 2] x1 + [0]
                         [0 1]      [0]
              first(x1, x2) = [1 2] x1 + [1 3] x2 + [0]
                              [0 1]      [0 1]      [1]
              a__from(x1) = [1 2] x1 + [1]
                            [0 1]      [2]
              from(x1) = [1 2] x1 + [0]
                         [0 1]      [2]
              a__first^#(x1, x2) = [3 0] x1 + [3 0] x2 + [0]
                                   [0 0]      [0 0]      [0]
              c_0() = [0]
                      [0]
              c_1(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              mark^#(x1) = [0 0] x1 + [0]
                           [0 0]      [0]
              a__from^#(x1) = [3 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(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              c_8(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              c_9() = [0]
                      [0]
              c_10() = [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^#(nil()) -> c_6()}
             Weak Rules:
               {  a__first^#(s(X), cons(Y, Z)) -> c_1(mark^#(Y))
                , mark^#(first(X1, X2)) -> c_3(a__first^#(mark(X1), mark(X2)))
                , mark^#(cons(X1, X2)) -> c_8(mark^#(X1))
                , mark^#(s(X)) -> c_7(mark^#(X))
                , a__from^#(X) -> c_2(mark^#(X))
                , mark^#(from(X)) -> c_4(a__from^#(mark(X)))
                , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
                , mark(from(X)) -> a__from(mark(X))
                , mark(0()) -> 0()
                , mark(nil()) -> nil()
                , mark(s(X)) -> s(mark(X))
                , mark(cons(X1, X2)) -> cons(mark(X1), X2)
                , a__first(0(), X) -> nil()
                , a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z))
                , a__from(X) -> cons(mark(X), from(s(X)))
                , a__first(X1, X2) -> first(X1, X2)
                , a__from(X) -> from(X)}

           Proof Output:
             The following argument positions are usable:
               Uargs(a__first) = {}, Uargs(s) = {}, Uargs(cons) = {},
               Uargs(mark) = {}, Uargs(first) = {}, Uargs(a__from) = {},
               Uargs(from) = {}, Uargs(a__first^#) = {}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(a__from^#) = {}, Uargs(c_2) = {1},
               Uargs(c_3) = {1}, Uargs(c_4) = {1}, Uargs(c_7) = {1},
               Uargs(c_8) = {1}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__first(x1, x2) = [1 2] x1 + [1 2] x2 + [1]
                                 [0 0]      [0 1]      [3]
              0() = [0]
                    [0]
              nil() = [0]
                      [2]
              s(x1) = [1 0] x1 + [6]
                      [0 1]      [1]
              cons(x1, x2) = [1 2] x1 + [0 0] x2 + [0]
                             [0 1]      [0 0]      [0]
              mark(x1) = [1 0] x1 + [0]
                         [0 1]      [0]
              first(x1, x2) = [1 2] x1 + [1 2] x2 + [1]
                              [0 0]      [0 1]      [3]
              a__from(x1) = [1 4] x1 + [0]
                            [0 1]      [2]
              from(x1) = [1 4] x1 + [0]
                         [0 1]      [2]
              a__first^#(x1, x2) = [0 2] x1 + [2 4] x2 + [6]
                                   [0 0]      [4 0]      [0]
              c_1(x1) = [1 2] x1 + [0]
                        [2 0]      [0]
              mark^#(x1) = [2 2] x1 + [0]
                           [0 2]      [4]
              a__from^#(x1) = [2 2] x1 + [0]
                              [4 0]      [0]
              c_2(x1) = [1 0] x1 + [0]
                        [0 0]      [0]
              c_3(x1) = [1 0] x1 + [1]
                        [0 0]      [7]
              c_4(x1) = [1 0] x1 + [3]
                        [0 0]      [7]
              c_6() = [1]
                      [0]
              c_7(x1) = [1 0] x1 + [7]
                        [0 0]      [2]
              c_8(x1) = [1 0] x1 + [0]
                        [0 0]      [2]

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

           The usable rules for this path are:

             {  mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
              , mark(from(X)) -> a__from(mark(X))
              , mark(0()) -> 0()
              , mark(nil()) -> nil()
              , mark(s(X)) -> s(mark(X))
              , mark(cons(X1, X2)) -> cons(mark(X1), X2)
              , a__first(0(), X) -> nil()
              , a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z))
              , a__from(X) -> cons(mark(X), from(s(X)))
              , a__first(X1, X2) -> first(X1, X2)
              , a__from(X) -> from(X)}

           The weightgap principle applies, using the following adequate RMI:
             The following argument positions are usable:
               Uargs(a__first) = {1, 2}, Uargs(s) = {1}, Uargs(cons) = {1},
               Uargs(mark) = {}, Uargs(first) = {}, Uargs(a__from) = {1},
               Uargs(from) = {}, Uargs(a__first^#) = {1, 2}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(a__from^#) = {1}, Uargs(c_2) = {1},
               Uargs(c_3) = {1}, Uargs(c_4) = {1}, Uargs(c_7) = {1},
               Uargs(c_8) = {1}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__first(x1, x2) = [1 2] x1 + [1 3] x2 + [1]
                                 [0 1]      [0 1]      [1]
              0() = [0]
                    [2]
              nil() = [0]
                      [2]
              s(x1) = [1 2] x1 + [0]
                      [0 1]      [2]
              cons(x1, x2) = [1 0] x1 + [0 0] x2 + [0]
                             [0 1]      [0 0]      [2]
              mark(x1) = [1 2] x1 + [0]
                         [0 1]      [0]
              first(x1, x2) = [1 2] x1 + [1 3] x2 + [0]
                              [0 1]      [0 1]      [1]
              a__from(x1) = [1 2] x1 + [1]
                            [0 1]      [2]
              from(x1) = [1 2] x1 + [0]
                         [0 1]      [2]
              a__first^#(x1, x2) = [3 0] x1 + [3 0] x2 + [0]
                                   [0 0]      [0 0]      [0]
              c_0() = [0]
                      [0]
              c_1(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              mark^#(x1) = [0 0] x1 + [0]
                           [0 0]      [0]
              a__from^#(x1) = [3 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(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              c_8(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              c_9() = [0]
                      [0]
              c_10() = [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: {a__first^#(X1, X2) -> c_9()}
             Weak Rules:
               {  a__first^#(s(X), cons(Y, Z)) -> c_1(mark^#(Y))
                , mark^#(first(X1, X2)) -> c_3(a__first^#(mark(X1), mark(X2)))
                , mark^#(cons(X1, X2)) -> c_8(mark^#(X1))
                , mark^#(s(X)) -> c_7(mark^#(X))
                , a__from^#(X) -> c_2(mark^#(X))
                , mark^#(from(X)) -> c_4(a__from^#(mark(X)))
                , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
                , mark(from(X)) -> a__from(mark(X))
                , mark(0()) -> 0()
                , mark(nil()) -> nil()
                , mark(s(X)) -> s(mark(X))
                , mark(cons(X1, X2)) -> cons(mark(X1), X2)
                , a__first(0(), X) -> nil()
                , a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z))
                , a__from(X) -> cons(mark(X), from(s(X)))
                , a__first(X1, X2) -> first(X1, X2)
                , a__from(X) -> from(X)}

           Proof Output:
             The following argument positions are usable:
               Uargs(a__first) = {}, Uargs(s) = {}, Uargs(cons) = {},
               Uargs(mark) = {}, Uargs(first) = {}, Uargs(a__from) = {},
               Uargs(from) = {}, Uargs(a__first^#) = {}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(a__from^#) = {}, Uargs(c_2) = {1},
               Uargs(c_3) = {1}, Uargs(c_4) = {1}, Uargs(c_7) = {1},
               Uargs(c_8) = {1}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__first(x1, x2) = [2 0] x1 + [4 0] x2 + [0]
                                 [0 0]      [0 0]      [0]
              0() = [0]
                    [0]
              nil() = [0]
                      [0]
              s(x1) = [0 4] x1 + [0]
                      [0 0]      [0]
              cons(x1, x2) = [0 2] x1 + [0 0] x2 + [0]
                             [0 1]      [0 0]      [0]
              mark(x1) = [0 0] x1 + [0]
                         [0 0]      [0]
              first(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                              [0 0]      [0 0]      [0]
              a__from(x1) = [0 4] x1 + [0]
                            [0 4]      [0]
              from(x1) = [0 0] x1 + [0]
                         [0 0]      [0]
              a__first^#(x1, x2) = [0 0] x1 + [2 5] x2 + [2]
                                   [0 0]      [0 0]      [2]
              c_1(x1) = [1 0] x1 + [0]
                        [0 0]      [2]
              mark^#(x1) = [0 0] x1 + [2]
                           [0 1]      [4]
              a__from^#(x1) = [2 2] x1 + [2]
                              [4 4]      [0]
              c_2(x1) = [1 0] x1 + [0]
                        [0 0]      [0]
              c_3(x1) = [1 0] x1 + [0]
                        [0 2]      [0]
              c_4(x1) = [1 0] x1 + [0]
                        [2 0]      [0]
              c_7(x1) = [1 0] x1 + [0]
                        [0 0]      [3]
              c_8(x1) = [1 0] x1 + [0]
                        [0 0]      [3]
              c_9() = [1]
                      [0]

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

           The usable rules for this path are:

             {  mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
              , mark(from(X)) -> a__from(mark(X))
              , mark(0()) -> 0()
              , mark(nil()) -> nil()
              , mark(s(X)) -> s(mark(X))
              , mark(cons(X1, X2)) -> cons(mark(X1), X2)
              , a__first(0(), X) -> nil()
              , a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z))
              , a__from(X) -> cons(mark(X), from(s(X)))
              , a__first(X1, X2) -> first(X1, X2)
              , a__from(X) -> from(X)}

           The weightgap principle applies, using the following adequate RMI:
             The following argument positions are usable:
               Uargs(a__first) = {1, 2}, Uargs(s) = {1}, Uargs(cons) = {1},
               Uargs(mark) = {}, Uargs(first) = {}, Uargs(a__from) = {1},
               Uargs(from) = {}, Uargs(a__first^#) = {1, 2}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(a__from^#) = {1}, Uargs(c_2) = {1},
               Uargs(c_3) = {1}, Uargs(c_4) = {1}, Uargs(c_7) = {1},
               Uargs(c_8) = {1}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__first(x1, x2) = [1 2] x1 + [1 3] x2 + [1]
                                 [0 1]      [0 1]      [1]
              0() = [0]
                    [2]
              nil() = [0]
                      [2]
              s(x1) = [1 2] x1 + [0]
                      [0 1]      [2]
              cons(x1, x2) = [1 0] x1 + [0 0] x2 + [0]
                             [0 1]      [0 0]      [2]
              mark(x1) = [1 2] x1 + [0]
                         [0 1]      [0]
              first(x1, x2) = [1 2] x1 + [1 3] x2 + [0]
                              [0 1]      [0 1]      [1]
              a__from(x1) = [1 2] x1 + [1]
                            [0 1]      [2]
              from(x1) = [1 2] x1 + [0]
                         [0 1]      [2]
              a__first^#(x1, x2) = [3 0] x1 + [3 0] x2 + [0]
                                   [0 0]      [0 0]      [0]
              c_0() = [0]
                      [0]
              c_1(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              mark^#(x1) = [0 0] x1 + [0]
                           [0 0]      [0]
              a__from^#(x1) = [3 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(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              c_8(x1) = [1 0] x1 + [0]
                        [0 1]      [0]
              c_9() = [0]
                      [0]
              c_10() = [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__from^#(X) -> c_10()}
             Weak Rules:
               {  a__first^#(s(X), cons(Y, Z)) -> c_1(mark^#(Y))
                , mark^#(first(X1, X2)) -> c_3(a__first^#(mark(X1), mark(X2)))
                , mark^#(cons(X1, X2)) -> c_8(mark^#(X1))
                , mark^#(s(X)) -> c_7(mark^#(X))
                , a__from^#(X) -> c_2(mark^#(X))
                , mark^#(from(X)) -> c_4(a__from^#(mark(X)))
                , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
                , mark(from(X)) -> a__from(mark(X))
                , mark(0()) -> 0()
                , mark(nil()) -> nil()
                , mark(s(X)) -> s(mark(X))
                , mark(cons(X1, X2)) -> cons(mark(X1), X2)
                , a__first(0(), X) -> nil()
                , a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z))
                , a__from(X) -> cons(mark(X), from(s(X)))
                , a__first(X1, X2) -> first(X1, X2)
                , a__from(X) -> from(X)}

           Proof Output:
             The following argument positions are usable:
               Uargs(a__first) = {}, Uargs(s) = {}, Uargs(cons) = {},
               Uargs(mark) = {}, Uargs(first) = {}, Uargs(a__from) = {},
               Uargs(from) = {}, Uargs(a__first^#) = {}, Uargs(c_1) = {1},
               Uargs(mark^#) = {}, Uargs(a__from^#) = {}, Uargs(c_2) = {1},
               Uargs(c_3) = {1}, Uargs(c_4) = {1}, Uargs(c_7) = {1},
               Uargs(c_8) = {1}
             We have the following constructor-restricted matrix interpretation:
             Interpretation Functions:
              a__first(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                                 [0 0]      [0 0]      [0]
              0() = [1]
                    [0]
              nil() = [0]
                      [0]
              s(x1) = [0 0] x1 + [1]
                      [0 0]      [0]
              cons(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                             [0 0]      [0 0]      [0]
              mark(x1) = [1 0] x1 + [3]
                         [0 1]      [1]
              first(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                              [0 0]      [0 0]      [0]
              a__from(x1) = [0 0] x1 + [1]
                            [0 0]      [3]
              from(x1) = [0 0] x1 + [1]
                         [0 0]      [3]
              a__first^#(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
                                   [0 0]      [0 0]      [0]
              c_1(x1) = [1 0] x1 + [0]
                        [0 0]      [0]
              mark^#(x1) = [0 0] x1 + [1]
                           [0 0]      [0]
              a__from^#(x1) = [0 0] x1 + [1]
                              [0 0]      [0]
              c_2(x1) = [1 0] x1 + [0]
                        [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(x1) = [1 0] x1 + [0]
                        [0 0]      [0]
              c_8(x1) = [1 0] x1 + [0]
                        [0 0]      [0]
              c_10() = [0]
                       [0]

Tool RC1

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 Ex6 Luc98 GM

stdout:

MAYBE

Tool RC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Transformed CSR 04 Ex6 Luc98 GM

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  a__first(0(), X) -> nil()
     , a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z))
     , a__from(X) -> cons(mark(X), from(s(X)))
     , mark(first(X1, X2)) -> a__first(mark(X1), mark(X2))
     , mark(from(X)) -> a__from(mark(X))
     , mark(0()) -> 0()
     , mark(nil()) -> nil()
     , mark(s(X)) -> s(mark(X))
     , mark(cons(X1, X2)) -> cons(mark(X1), X2)
     , a__first(X1, X2) -> first(X1, X2)
     , a__from(X) -> from(X)}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds