Problem Transformed CSR 04 Ex1 2 Luc02c GM

Tool CaT

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 Ex1 2 Luc02c GM

stdout:

MAYBE

Problem:
a__2nd(cons(X,cons(Y,Z))) -> mark(Y)
a__from(X) -> cons(mark(X),from(s(X)))
mark(2nd(X)) -> a__2nd(mark(X))
mark(from(X)) -> a__from(mark(X))
mark(cons(X1,X2)) -> cons(mark(X1),X2)
mark(s(X)) -> s(mark(X))
a__2nd(X) -> 2nd(X)
a__from(X) -> from(X)

Proof:
Open

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 Ex1 2 Luc02c GM

stdout:

MAYBE

Tool IRC2

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 Ex1 2 Luc02c GM

stdout:

MAYBE

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           MAYBE
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  a__2nd(cons(X, cons(Y, Z))) -> mark(Y)
     , a__from(X) -> cons(mark(X), from(s(X)))
     , mark(2nd(X)) -> a__2nd(mark(X))
     , mark(from(X)) -> a__from(mark(X))
     , mark(cons(X1, X2)) -> cons(mark(X1), X2)
     , mark(s(X)) -> s(mark(X))
     , a__2nd(X) -> 2nd(X)
     , a__from(X) -> from(X)}

Proof Output:
  None of the processors succeeded.

  Details of failed attempt(s):
  -----------------------------
    1) 'wdg' failed due to the following reason:
         Transformation Details:
         -----------------------
           We have computed the following set of weak (innermost) dependency pairs:

             {  1: a__2nd^#(cons(X, cons(Y, Z))) -> c_0(mark^#(Y))
              , 2: a__from^#(X) -> c_1(mark^#(X))
              , 3: mark^#(2nd(X)) -> c_2(a__2nd^#(mark(X)))
              , 4: mark^#(from(X)) -> c_3(a__from^#(mark(X)))
              , 5: mark^#(cons(X1, X2)) -> c_4(mark^#(X1))
              , 6: mark^#(s(X)) -> c_5(mark^#(X))
              , 7: a__2nd^#(X) -> c_6()
              , 8: a__from^#(X) -> c_7()}

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

             ->{1,3,6,5,2,4}                                             [     inherited      ]
                |
                |->{7}                                                   [         NA         ]
                |
                `->{8}                                                   [         NA         ]



         Sub-problems:
         -------------
           * Path {1,3,6,5,2,4}: inherited
             -----------------------------

             This path is subsumed by the proof of path {1,3,6,5,2,4}->{8}.

           * Path {1,3,6,5,2,4}->{7}: NA
             ---------------------------

             The usable rules for this path are:

               {  mark(2nd(X)) -> a__2nd(mark(X))
                , mark(from(X)) -> a__from(mark(X))
                , mark(cons(X1, X2)) -> cons(mark(X1), X2)
                , mark(s(X)) -> s(mark(X))
                , a__2nd(cons(X, cons(Y, Z))) -> mark(Y)
                , a__from(X) -> cons(mark(X), from(s(X)))
                , a__2nd(X) -> 2nd(X)
                , a__from(X) -> from(X)}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

             We have not generated a proof for the resulting sub-problem.

           * Path {1,3,6,5,2,4}->{8}: NA
             ---------------------------

             The usable rules for this path are:

               {  mark(2nd(X)) -> a__2nd(mark(X))
                , mark(from(X)) -> a__from(mark(X))
                , mark(cons(X1, X2)) -> cons(mark(X1), X2)
                , mark(s(X)) -> s(mark(X))
                , a__2nd(cons(X, cons(Y, Z))) -> mark(Y)
                , a__from(X) -> cons(mark(X), from(s(X)))
                , a__2nd(X) -> 2nd(X)
                , a__from(X) -> from(X)}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

             We have not generated a proof for the resulting sub-problem.

    2) 'wdg' failed due to the following reason:
         Transformation Details:
         -----------------------
           We have computed the following set of weak (innermost) dependency pairs:

             {  1: a__2nd^#(cons(X, cons(Y, Z))) -> c_0(mark^#(Y))
              , 2: a__from^#(X) -> c_1(mark^#(X))
              , 3: mark^#(2nd(X)) -> c_2(a__2nd^#(mark(X)))
              , 4: mark^#(from(X)) -> c_3(a__from^#(mark(X)))
              , 5: mark^#(cons(X1, X2)) -> c_4(mark^#(X1))
              , 6: mark^#(s(X)) -> c_5(mark^#(X))
              , 7: a__2nd^#(X) -> c_6()
              , 8: a__from^#(X) -> c_7()}

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

             ->{1,3,6,5,2,4}                                             [     inherited      ]
                |
                |->{7}                                                   [       MAYBE        ]
                |
                `->{8}                                                   [         NA         ]



         Sub-problems:
         -------------
           * Path {1,3,6,5,2,4}: inherited
             -----------------------------

             This path is subsumed by the proof of path {1,3,6,5,2,4}->{8}.

           * Path {1,3,6,5,2,4}->{7}: MAYBE
             ------------------------------

             The usable rules for this path are:

               {  mark(2nd(X)) -> a__2nd(mark(X))
                , mark(from(X)) -> a__from(mark(X))
                , mark(cons(X1, X2)) -> cons(mark(X1), X2)
                , mark(s(X)) -> s(mark(X))
                , a__2nd(cons(X, cons(Y, Z))) -> mark(Y)
                , a__from(X) -> cons(mark(X), from(s(X)))
                , a__2nd(X) -> 2nd(X)
                , a__from(X) -> from(X)}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

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

             'matrix-interpretation of dimension 2'
             --------------------------------------
             Answer:           MAYBE
             Input Problem:    innermost runtime-complexity with respect to
               Rules:
                 {  a__2nd^#(cons(X, cons(Y, Z))) -> c_0(mark^#(Y))
                  , mark^#(2nd(X)) -> c_2(a__2nd^#(mark(X)))
                  , mark^#(s(X)) -> c_5(mark^#(X))
                  , mark^#(cons(X1, X2)) -> c_4(mark^#(X1))
                  , a__from^#(X) -> c_1(mark^#(X))
                  , mark^#(from(X)) -> c_3(a__from^#(mark(X)))
                  , a__2nd^#(X) -> c_6()
                  , mark(2nd(X)) -> a__2nd(mark(X))
                  , mark(from(X)) -> a__from(mark(X))
                  , mark(cons(X1, X2)) -> cons(mark(X1), X2)
                  , mark(s(X)) -> s(mark(X))
                  , a__2nd(cons(X, cons(Y, Z))) -> mark(Y)
                  , a__from(X) -> cons(mark(X), from(s(X)))
                  , a__2nd(X) -> 2nd(X)
                  , a__from(X) -> from(X)}

             Proof Output:
               The input cannot be shown compatible

           * Path {1,3,6,5,2,4}->{8}: NA
             ---------------------------

             The usable rules for this path are:

               {  mark(2nd(X)) -> a__2nd(mark(X))
                , mark(from(X)) -> a__from(mark(X))
                , mark(cons(X1, X2)) -> cons(mark(X1), X2)
                , mark(s(X)) -> s(mark(X))
                , a__2nd(cons(X, cons(Y, Z))) -> mark(Y)
                , a__from(X) -> cons(mark(X), from(s(X)))
                , a__2nd(X) -> 2nd(X)
                , a__from(X) -> from(X)}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

             We have not generated a proof for the resulting sub-problem.

    3) 'wdg' failed due to the following reason:
         Transformation Details:
         -----------------------
           We have computed the following set of weak (innermost) dependency pairs:

             {  1: a__2nd^#(cons(X, cons(Y, Z))) -> c_0(mark^#(Y))
              , 2: a__from^#(X) -> c_1(mark^#(X))
              , 3: mark^#(2nd(X)) -> c_2(a__2nd^#(mark(X)))
              , 4: mark^#(from(X)) -> c_3(a__from^#(mark(X)))
              , 5: mark^#(cons(X1, X2)) -> c_4(mark^#(X1))
              , 6: mark^#(s(X)) -> c_5(mark^#(X))
              , 7: a__2nd^#(X) -> c_6()
              , 8: a__from^#(X) -> c_7()}

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

             ->{1,3,6,5,2,4}                                             [     inherited      ]
                |
                |->{7}                                                   [       MAYBE        ]
                |
                `->{8}                                                   [         NA         ]



         Sub-problems:
         -------------
           * Path {1,3,6,5,2,4}: inherited
             -----------------------------

             This path is subsumed by the proof of path {1,3,6,5,2,4}->{8}.

           * Path {1,3,6,5,2,4}->{7}: MAYBE
             ------------------------------

             The usable rules for this path are:

               {  mark(2nd(X)) -> a__2nd(mark(X))
                , mark(from(X)) -> a__from(mark(X))
                , mark(cons(X1, X2)) -> cons(mark(X1), X2)
                , mark(s(X)) -> s(mark(X))
                , a__2nd(cons(X, cons(Y, Z))) -> mark(Y)
                , a__from(X) -> cons(mark(X), from(s(X)))
                , a__2nd(X) -> 2nd(X)
                , a__from(X) -> from(X)}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

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

             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           MAYBE
             Input Problem:    innermost runtime-complexity with respect to
               Rules:
                 {  a__2nd^#(cons(X, cons(Y, Z))) -> c_0(mark^#(Y))
                  , mark^#(2nd(X)) -> c_2(a__2nd^#(mark(X)))
                  , mark^#(s(X)) -> c_5(mark^#(X))
                  , mark^#(cons(X1, X2)) -> c_4(mark^#(X1))
                  , a__from^#(X) -> c_1(mark^#(X))
                  , mark^#(from(X)) -> c_3(a__from^#(mark(X)))
                  , a__2nd^#(X) -> c_6()
                  , mark(2nd(X)) -> a__2nd(mark(X))
                  , mark(from(X)) -> a__from(mark(X))
                  , mark(cons(X1, X2)) -> cons(mark(X1), X2)
                  , mark(s(X)) -> s(mark(X))
                  , a__2nd(cons(X, cons(Y, Z))) -> mark(Y)
                  , a__from(X) -> cons(mark(X), from(s(X)))
                  , a__2nd(X) -> 2nd(X)
                  , a__from(X) -> from(X)}

             Proof Output:
               The input cannot be shown compatible

           * Path {1,3,6,5,2,4}->{8}: NA
             ---------------------------

             The usable rules for this path are:

               {  mark(2nd(X)) -> a__2nd(mark(X))
                , mark(from(X)) -> a__from(mark(X))
                , mark(cons(X1, X2)) -> cons(mark(X1), X2)
                , mark(s(X)) -> s(mark(X))
                , a__2nd(cons(X, cons(Y, Z))) -> mark(Y)
                , a__from(X) -> cons(mark(X), from(s(X)))
                , a__2nd(X) -> 2nd(X)
                , a__from(X) -> from(X)}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

             We have not generated a proof for the resulting sub-problem.

    4) 'matrix-interpretation of dimension 1' failed due to the following reason:
         The input cannot be shown compatible

    5) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason:
         match-boundness of the problem could not be verified.

    6) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason:
         match-boundness of the problem could not be verified.

Tool RC1

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 Ex1 2 Luc02c GM

stdout:

MAYBE

Tool RC2

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 Ex1 2 Luc02c GM

stdout:

MAYBE

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           MAYBE
Input Problem:    runtime-complexity with respect to
  Rules:
    {  a__2nd(cons(X, cons(Y, Z))) -> mark(Y)
     , a__from(X) -> cons(mark(X), from(s(X)))
     , mark(2nd(X)) -> a__2nd(mark(X))
     , mark(from(X)) -> a__from(mark(X))
     , mark(cons(X1, X2)) -> cons(mark(X1), X2)
     , mark(s(X)) -> s(mark(X))
     , a__2nd(X) -> 2nd(X)
     , a__from(X) -> from(X)}

Proof Output:
  None of the processors succeeded.

  Details of failed attempt(s):
  -----------------------------
    1) 'wdg' failed due to the following reason:
         Transformation Details:
         -----------------------
           We have computed the following set of weak (innermost) dependency pairs:

             {  1: a__2nd^#(cons(X, cons(Y, Z))) -> c_0(mark^#(Y))
              , 2: a__from^#(X) -> c_1(mark^#(X), X)
              , 3: mark^#(2nd(X)) -> c_2(a__2nd^#(mark(X)))
              , 4: mark^#(from(X)) -> c_3(a__from^#(mark(X)))
              , 5: mark^#(cons(X1, X2)) -> c_4(mark^#(X1), X2)
              , 6: mark^#(s(X)) -> c_5(mark^#(X))
              , 7: a__2nd^#(X) -> c_6(X)
              , 8: a__from^#(X) -> c_7(X)}

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

             ->{1,3,6,5,2,4}                                             [     inherited      ]
                |
                |->{7}                                                   [         NA         ]
                |
                `->{8}                                                   [         NA         ]



         Sub-problems:
         -------------
           * Path {1,3,6,5,2,4}: inherited
             -----------------------------

             This path is subsumed by the proof of path {1,3,6,5,2,4}->{8}.

           * Path {1,3,6,5,2,4}->{7}: NA
             ---------------------------

             The usable rules for this path are:

               {  mark(2nd(X)) -> a__2nd(mark(X))
                , mark(from(X)) -> a__from(mark(X))
                , mark(cons(X1, X2)) -> cons(mark(X1), X2)
                , mark(s(X)) -> s(mark(X))
                , a__2nd(cons(X, cons(Y, Z))) -> mark(Y)
                , a__from(X) -> cons(mark(X), from(s(X)))
                , a__2nd(X) -> 2nd(X)
                , a__from(X) -> from(X)}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

             We have not generated a proof for the resulting sub-problem.

           * Path {1,3,6,5,2,4}->{8}: NA
             ---------------------------

             The usable rules for this path are:

               {  mark(2nd(X)) -> a__2nd(mark(X))
                , mark(from(X)) -> a__from(mark(X))
                , mark(cons(X1, X2)) -> cons(mark(X1), X2)
                , mark(s(X)) -> s(mark(X))
                , a__2nd(cons(X, cons(Y, Z))) -> mark(Y)
                , a__from(X) -> cons(mark(X), from(s(X)))
                , a__2nd(X) -> 2nd(X)
                , a__from(X) -> from(X)}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

             We have not generated a proof for the resulting sub-problem.

    2) 'wdg' failed due to the following reason:
         Transformation Details:
         -----------------------
           We have computed the following set of weak (innermost) dependency pairs:

             {  1: a__2nd^#(cons(X, cons(Y, Z))) -> c_0(mark^#(Y))
              , 2: a__from^#(X) -> c_1(mark^#(X), X)
              , 3: mark^#(2nd(X)) -> c_2(a__2nd^#(mark(X)))
              , 4: mark^#(from(X)) -> c_3(a__from^#(mark(X)))
              , 5: mark^#(cons(X1, X2)) -> c_4(mark^#(X1), X2)
              , 6: mark^#(s(X)) -> c_5(mark^#(X))
              , 7: a__2nd^#(X) -> c_6(X)
              , 8: a__from^#(X) -> c_7(X)}

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

             ->{1,3,6,5,2,4}                                             [     inherited      ]
                |
                |->{7}                                                   [       MAYBE        ]
                |
                `->{8}                                                   [         NA         ]



         Sub-problems:
         -------------
           * Path {1,3,6,5,2,4}: inherited
             -----------------------------

             This path is subsumed by the proof of path {1,3,6,5,2,4}->{8}.

           * Path {1,3,6,5,2,4}->{7}: MAYBE
             ------------------------------

             The usable rules for this path are:

               {  mark(2nd(X)) -> a__2nd(mark(X))
                , mark(from(X)) -> a__from(mark(X))
                , mark(cons(X1, X2)) -> cons(mark(X1), X2)
                , mark(s(X)) -> s(mark(X))
                , a__2nd(cons(X, cons(Y, Z))) -> mark(Y)
                , a__from(X) -> cons(mark(X), from(s(X)))
                , a__2nd(X) -> 2nd(X)
                , a__from(X) -> from(X)}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

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

             'matrix-interpretation of dimension 2'
             --------------------------------------
             Answer:           MAYBE
             Input Problem:    runtime-complexity with respect to
               Rules:
                 {  a__2nd^#(cons(X, cons(Y, Z))) -> c_0(mark^#(Y))
                  , mark^#(2nd(X)) -> c_2(a__2nd^#(mark(X)))
                  , mark^#(s(X)) -> c_5(mark^#(X))
                  , mark^#(cons(X1, X2)) -> c_4(mark^#(X1), X2)
                  , a__from^#(X) -> c_1(mark^#(X), X)
                  , mark^#(from(X)) -> c_3(a__from^#(mark(X)))
                  , a__2nd^#(X) -> c_6(X)
                  , mark(2nd(X)) -> a__2nd(mark(X))
                  , mark(from(X)) -> a__from(mark(X))
                  , mark(cons(X1, X2)) -> cons(mark(X1), X2)
                  , mark(s(X)) -> s(mark(X))
                  , a__2nd(cons(X, cons(Y, Z))) -> mark(Y)
                  , a__from(X) -> cons(mark(X), from(s(X)))
                  , a__2nd(X) -> 2nd(X)
                  , a__from(X) -> from(X)}

             Proof Output:
               The input cannot be shown compatible

           * Path {1,3,6,5,2,4}->{8}: NA
             ---------------------------

             The usable rules for this path are:

               {  mark(2nd(X)) -> a__2nd(mark(X))
                , mark(from(X)) -> a__from(mark(X))
                , mark(cons(X1, X2)) -> cons(mark(X1), X2)
                , mark(s(X)) -> s(mark(X))
                , a__2nd(cons(X, cons(Y, Z))) -> mark(Y)
                , a__from(X) -> cons(mark(X), from(s(X)))
                , a__2nd(X) -> 2nd(X)
                , a__from(X) -> from(X)}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

             We have not generated a proof for the resulting sub-problem.

    3) 'wdg' failed due to the following reason:
         Transformation Details:
         -----------------------
           We have computed the following set of weak (innermost) dependency pairs:

             {  1: a__2nd^#(cons(X, cons(Y, Z))) -> c_0(mark^#(Y))
              , 2: a__from^#(X) -> c_1(mark^#(X), X)
              , 3: mark^#(2nd(X)) -> c_2(a__2nd^#(mark(X)))
              , 4: mark^#(from(X)) -> c_3(a__from^#(mark(X)))
              , 5: mark^#(cons(X1, X2)) -> c_4(mark^#(X1), X2)
              , 6: mark^#(s(X)) -> c_5(mark^#(X))
              , 7: a__2nd^#(X) -> c_6(X)
              , 8: a__from^#(X) -> c_7(X)}

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

             ->{1,3,6,5,2,4}                                             [     inherited      ]
                |
                |->{7}                                                   [       MAYBE        ]
                |
                `->{8}                                                   [         NA         ]



         Sub-problems:
         -------------
           * Path {1,3,6,5,2,4}: inherited
             -----------------------------

             This path is subsumed by the proof of path {1,3,6,5,2,4}->{8}.

           * Path {1,3,6,5,2,4}->{7}: MAYBE
             ------------------------------

             The usable rules for this path are:

               {  mark(2nd(X)) -> a__2nd(mark(X))
                , mark(from(X)) -> a__from(mark(X))
                , mark(cons(X1, X2)) -> cons(mark(X1), X2)
                , mark(s(X)) -> s(mark(X))
                , a__2nd(cons(X, cons(Y, Z))) -> mark(Y)
                , a__from(X) -> cons(mark(X), from(s(X)))
                , a__2nd(X) -> 2nd(X)
                , a__from(X) -> from(X)}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

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

             'matrix-interpretation of dimension 1'
             --------------------------------------
             Answer:           MAYBE
             Input Problem:    runtime-complexity with respect to
               Rules:
                 {  a__2nd^#(cons(X, cons(Y, Z))) -> c_0(mark^#(Y))
                  , mark^#(2nd(X)) -> c_2(a__2nd^#(mark(X)))
                  , mark^#(s(X)) -> c_5(mark^#(X))
                  , mark^#(cons(X1, X2)) -> c_4(mark^#(X1), X2)
                  , a__from^#(X) -> c_1(mark^#(X), X)
                  , mark^#(from(X)) -> c_3(a__from^#(mark(X)))
                  , a__2nd^#(X) -> c_6(X)
                  , mark(2nd(X)) -> a__2nd(mark(X))
                  , mark(from(X)) -> a__from(mark(X))
                  , mark(cons(X1, X2)) -> cons(mark(X1), X2)
                  , mark(s(X)) -> s(mark(X))
                  , a__2nd(cons(X, cons(Y, Z))) -> mark(Y)
                  , a__from(X) -> cons(mark(X), from(s(X)))
                  , a__2nd(X) -> 2nd(X)
                  , a__from(X) -> from(X)}

             Proof Output:
               The input cannot be shown compatible

           * Path {1,3,6,5,2,4}->{8}: NA
             ---------------------------

             The usable rules for this path are:

               {  mark(2nd(X)) -> a__2nd(mark(X))
                , mark(from(X)) -> a__from(mark(X))
                , mark(cons(X1, X2)) -> cons(mark(X1), X2)
                , mark(s(X)) -> s(mark(X))
                , a__2nd(cons(X, cons(Y, Z))) -> mark(Y)
                , a__from(X) -> cons(mark(X), from(s(X)))
                , a__2nd(X) -> 2nd(X)
                , a__from(X) -> from(X)}

             The weight gap principle does not apply:
               The input cannot be shown compatible
             Complexity induced by the adequate RMI: MAYBE

             We have not generated a proof for the resulting sub-problem.

    4) 'matrix-interpretation of dimension 1' failed due to the following reason:
         The input cannot be shown compatible

    5) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason:
         match-boundness of the problem could not be verified.

    6) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason:
         match-boundness of the problem could not be verified.