Problem AProVE 04 rta3

Tool CaT

Execution TimeUnknown
Answer
MAYBE
InputAProVE 04 rta3

stdout:

MAYBE

Problem:
 ack(0(),y) -> s(y)
 ack(s(x),0()) -> ack(x,s(0()))
 ack(s(x),s(y)) -> ack(x,ack(s(x),y))
 f(s(x),y) -> f(x,s(x))
 f(x,s(y)) -> f(y,x)
 f(x,y) -> ack(x,y)
 ack(s(x),y) -> f(x,x)

Proof:
 Open

Tool IRC1

Execution TimeUnknown
Answer
MAYBE
InputAProVE 04 rta3

stdout:

MAYBE

Tool IRC2

Execution TimeUnknown
Answer
MAYBE
InputAProVE 04 rta3

stdout:

MAYBE

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           MAYBE
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  ack(0(), y) -> s(y)
     , ack(s(x), 0()) -> ack(x, s(0()))
     , ack(s(x), s(y)) -> ack(x, ack(s(x), y))
     , f(s(x), y) -> f(x, s(x))
     , f(x, s(y)) -> f(y, x)
     , f(x, y) -> ack(x, y)
     , ack(s(x), y) -> f(x, 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: ack^#(0(), y) -> c_0()
              , 2: ack^#(s(x), 0()) -> c_1(ack^#(x, s(0())))
              , 3: ack^#(s(x), s(y)) -> c_2(ack^#(x, ack(s(x), y)))
              , 4: f^#(s(x), y) -> c_3(f^#(x, s(x)))
              , 5: f^#(x, s(y)) -> c_4(f^#(y, x))
              , 6: f^#(x, y) -> c_5(ack^#(x, y))
              , 7: ack^#(s(x), y) -> c_6(f^#(x, x))}
           
           Following Dependency Graph (modulo SCCs) was computed. (Answers to
           subproofs are indicated to the right.)
           
             ->{2,6,7,3,5,4}                                             [     inherited      ]
                |
                `->{1}                                                   [         NA         ]
             
           
         
         Sub-problems:
         -------------
           * Path {2,6,7,3,5,4}: inherited
             -----------------------------
             
             This path is subsumed by the proof of path {2,6,7,3,5,4}->{1}.
           
           * Path {2,6,7,3,5,4}->{1}: NA
             ---------------------------
             
             The usable rules for this path are:
             
               {  ack(0(), y) -> s(y)
                , ack(s(x), 0()) -> ack(x, s(0()))
                , ack(s(x), s(y)) -> ack(x, ack(s(x), y))
                , ack(s(x), y) -> f(x, x)
                , f(s(x), y) -> f(x, s(x))
                , f(x, s(y)) -> f(y, x)
                , f(x, y) -> ack(x, y)}
             
             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: ack^#(0(), y) -> c_0()
              , 2: ack^#(s(x), 0()) -> c_1(ack^#(x, s(0())))
              , 3: ack^#(s(x), s(y)) -> c_2(ack^#(x, ack(s(x), y)))
              , 4: f^#(s(x), y) -> c_3(f^#(x, s(x)))
              , 5: f^#(x, s(y)) -> c_4(f^#(y, x))
              , 6: f^#(x, y) -> c_5(ack^#(x, y))
              , 7: ack^#(s(x), y) -> c_6(f^#(x, x))}
           
           Following Dependency Graph (modulo SCCs) was computed. (Answers to
           subproofs are indicated to the right.)
           
             ->{2,6,7,3,5,4}                                             [     inherited      ]
                |
                `->{1}                                                   [       MAYBE        ]
             
           
         
         Sub-problems:
         -------------
           * Path {2,6,7,3,5,4}: inherited
             -----------------------------
             
             This path is subsumed by the proof of path {2,6,7,3,5,4}->{1}.
           
           * Path {2,6,7,3,5,4}->{1}: MAYBE
             ------------------------------
             
             The usable rules for this path are:
             
               {  ack(0(), y) -> s(y)
                , ack(s(x), 0()) -> ack(x, s(0()))
                , ack(s(x), s(y)) -> ack(x, ack(s(x), y))
                , ack(s(x), y) -> f(x, x)
                , f(s(x), y) -> f(x, s(x))
                , f(x, s(y)) -> f(y, x)
                , f(x, y) -> ack(x, y)}
             
             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:
                 {  ack^#(s(x), 0()) -> c_1(ack^#(x, s(0())))
                  , f^#(x, y) -> c_5(ack^#(x, y))
                  , ack^#(s(x), y) -> c_6(f^#(x, x))
                  , ack^#(s(x), s(y)) -> c_2(ack^#(x, ack(s(x), y)))
                  , f^#(x, s(y)) -> c_4(f^#(y, x))
                  , f^#(s(x), y) -> c_3(f^#(x, s(x)))
                  , ack^#(0(), y) -> c_0()
                  , ack(0(), y) -> s(y)
                  , ack(s(x), 0()) -> ack(x, s(0()))
                  , ack(s(x), s(y)) -> ack(x, ack(s(x), y))
                  , ack(s(x), y) -> f(x, x)
                  , f(s(x), y) -> f(x, s(x))
                  , f(x, s(y)) -> f(y, x)
                  , f(x, y) -> ack(x, y)}
             
             Proof Output:    
               The input cannot be shown compatible
    
    3) 'wdg' failed due to the following reason:
         Transformation Details:
         -----------------------
           We have computed the following set of weak (innermost) dependency pairs:
           
             {  1: ack^#(0(), y) -> c_0()
              , 2: ack^#(s(x), 0()) -> c_1(ack^#(x, s(0())))
              , 3: ack^#(s(x), s(y)) -> c_2(ack^#(x, ack(s(x), y)))
              , 4: f^#(s(x), y) -> c_3(f^#(x, s(x)))
              , 5: f^#(x, s(y)) -> c_4(f^#(y, x))
              , 6: f^#(x, y) -> c_5(ack^#(x, y))
              , 7: ack^#(s(x), y) -> c_6(f^#(x, x))}
           
           Following Dependency Graph (modulo SCCs) was computed. (Answers to
           subproofs are indicated to the right.)
           
             ->{2,6,7,3,5,4}                                             [     inherited      ]
                |
                `->{1}                                                   [       MAYBE        ]
             
           
         
         Sub-problems:
         -------------
           * Path {2,6,7,3,5,4}: inherited
             -----------------------------
             
             This path is subsumed by the proof of path {2,6,7,3,5,4}->{1}.
           
           * Path {2,6,7,3,5,4}->{1}: MAYBE
             ------------------------------
             
             The usable rules for this path are:
             
               {  ack(0(), y) -> s(y)
                , ack(s(x), 0()) -> ack(x, s(0()))
                , ack(s(x), s(y)) -> ack(x, ack(s(x), y))
                , ack(s(x), y) -> f(x, x)
                , f(s(x), y) -> f(x, s(x))
                , f(x, s(y)) -> f(y, x)
                , f(x, y) -> ack(x, y)}
             
             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:
                 {  ack^#(s(x), 0()) -> c_1(ack^#(x, s(0())))
                  , f^#(x, y) -> c_5(ack^#(x, y))
                  , ack^#(s(x), y) -> c_6(f^#(x, x))
                  , ack^#(s(x), s(y)) -> c_2(ack^#(x, ack(s(x), y)))
                  , f^#(x, s(y)) -> c_4(f^#(y, x))
                  , f^#(s(x), y) -> c_3(f^#(x, s(x)))
                  , ack^#(0(), y) -> c_0()
                  , ack(0(), y) -> s(y)
                  , ack(s(x), 0()) -> ack(x, s(0()))
                  , ack(s(x), s(y)) -> ack(x, ack(s(x), y))
                  , ack(s(x), y) -> f(x, x)
                  , f(s(x), y) -> f(x, s(x))
                  , f(x, s(y)) -> f(y, x)
                  , f(x, y) -> ack(x, y)}
             
             Proof Output:    
               The input cannot be shown compatible
    
    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 TimeUnknown
Answer
MAYBE
InputAProVE 04 rta3

stdout:

MAYBE

Tool RC2

Execution TimeUnknown
Answer
MAYBE
InputAProVE 04 rta3

stdout:

MAYBE

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           MAYBE
Input Problem:    runtime-complexity with respect to
  Rules:
    {  ack(0(), y) -> s(y)
     , ack(s(x), 0()) -> ack(x, s(0()))
     , ack(s(x), s(y)) -> ack(x, ack(s(x), y))
     , f(s(x), y) -> f(x, s(x))
     , f(x, s(y)) -> f(y, x)
     , f(x, y) -> ack(x, y)
     , ack(s(x), y) -> f(x, 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: ack^#(0(), y) -> c_0(y)
              , 2: ack^#(s(x), 0()) -> c_1(ack^#(x, s(0())))
              , 3: ack^#(s(x), s(y)) -> c_2(ack^#(x, ack(s(x), y)))
              , 4: f^#(s(x), y) -> c_3(f^#(x, s(x)))
              , 5: f^#(x, s(y)) -> c_4(f^#(y, x))
              , 6: f^#(x, y) -> c_5(ack^#(x, y))
              , 7: ack^#(s(x), y) -> c_6(f^#(x, x))}
           
           Following Dependency Graph (modulo SCCs) was computed. (Answers to
           subproofs are indicated to the right.)
           
             ->{2,6,7,3,5,4}                                             [     inherited      ]
                |
                `->{1}                                                   [         NA         ]
             
           
         
         Sub-problems:
         -------------
           * Path {2,6,7,3,5,4}: inherited
             -----------------------------
             
             This path is subsumed by the proof of path {2,6,7,3,5,4}->{1}.
           
           * Path {2,6,7,3,5,4}->{1}: NA
             ---------------------------
             
             The usable rules for this path are:
             
               {  ack(0(), y) -> s(y)
                , ack(s(x), 0()) -> ack(x, s(0()))
                , ack(s(x), s(y)) -> ack(x, ack(s(x), y))
                , ack(s(x), y) -> f(x, x)
                , f(s(x), y) -> f(x, s(x))
                , f(x, s(y)) -> f(y, x)
                , f(x, y) -> ack(x, y)}
             
             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: ack^#(0(), y) -> c_0(y)
              , 2: ack^#(s(x), 0()) -> c_1(ack^#(x, s(0())))
              , 3: ack^#(s(x), s(y)) -> c_2(ack^#(x, ack(s(x), y)))
              , 4: f^#(s(x), y) -> c_3(f^#(x, s(x)))
              , 5: f^#(x, s(y)) -> c_4(f^#(y, x))
              , 6: f^#(x, y) -> c_5(ack^#(x, y))
              , 7: ack^#(s(x), y) -> c_6(f^#(x, x))}
           
           Following Dependency Graph (modulo SCCs) was computed. (Answers to
           subproofs are indicated to the right.)
           
             ->{2,6,7,3,5,4}                                             [     inherited      ]
                |
                `->{1}                                                   [       MAYBE        ]
             
           
         
         Sub-problems:
         -------------
           * Path {2,6,7,3,5,4}: inherited
             -----------------------------
             
             This path is subsumed by the proof of path {2,6,7,3,5,4}->{1}.
           
           * Path {2,6,7,3,5,4}->{1}: MAYBE
             ------------------------------
             
             The usable rules for this path are:
             
               {  ack(0(), y) -> s(y)
                , ack(s(x), 0()) -> ack(x, s(0()))
                , ack(s(x), s(y)) -> ack(x, ack(s(x), y))
                , ack(s(x), y) -> f(x, x)
                , f(s(x), y) -> f(x, s(x))
                , f(x, s(y)) -> f(y, x)
                , f(x, y) -> ack(x, y)}
             
             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:
                 {  ack^#(s(x), 0()) -> c_1(ack^#(x, s(0())))
                  , f^#(x, y) -> c_5(ack^#(x, y))
                  , ack^#(s(x), y) -> c_6(f^#(x, x))
                  , ack^#(s(x), s(y)) -> c_2(ack^#(x, ack(s(x), y)))
                  , f^#(x, s(y)) -> c_4(f^#(y, x))
                  , f^#(s(x), y) -> c_3(f^#(x, s(x)))
                  , ack^#(0(), y) -> c_0(y)
                  , ack(0(), y) -> s(y)
                  , ack(s(x), 0()) -> ack(x, s(0()))
                  , ack(s(x), s(y)) -> ack(x, ack(s(x), y))
                  , ack(s(x), y) -> f(x, x)
                  , f(s(x), y) -> f(x, s(x))
                  , f(x, s(y)) -> f(y, x)
                  , f(x, y) -> ack(x, y)}
             
             Proof Output:    
               The input cannot be shown compatible
    
    3) 'wdg' failed due to the following reason:
         Transformation Details:
         -----------------------
           We have computed the following set of weak (innermost) dependency pairs:
           
             {  1: ack^#(0(), y) -> c_0(y)
              , 2: ack^#(s(x), 0()) -> c_1(ack^#(x, s(0())))
              , 3: ack^#(s(x), s(y)) -> c_2(ack^#(x, ack(s(x), y)))
              , 4: f^#(s(x), y) -> c_3(f^#(x, s(x)))
              , 5: f^#(x, s(y)) -> c_4(f^#(y, x))
              , 6: f^#(x, y) -> c_5(ack^#(x, y))
              , 7: ack^#(s(x), y) -> c_6(f^#(x, x))}
           
           Following Dependency Graph (modulo SCCs) was computed. (Answers to
           subproofs are indicated to the right.)
           
             ->{2,6,7,3,5,4}                                             [     inherited      ]
                |
                `->{1}                                                   [       MAYBE        ]
             
           
         
         Sub-problems:
         -------------
           * Path {2,6,7,3,5,4}: inherited
             -----------------------------
             
             This path is subsumed by the proof of path {2,6,7,3,5,4}->{1}.
           
           * Path {2,6,7,3,5,4}->{1}: MAYBE
             ------------------------------
             
             The usable rules for this path are:
             
               {  ack(0(), y) -> s(y)
                , ack(s(x), 0()) -> ack(x, s(0()))
                , ack(s(x), s(y)) -> ack(x, ack(s(x), y))
                , ack(s(x), y) -> f(x, x)
                , f(s(x), y) -> f(x, s(x))
                , f(x, s(y)) -> f(y, x)
                , f(x, y) -> ack(x, y)}
             
             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:
                 {  ack^#(s(x), 0()) -> c_1(ack^#(x, s(0())))
                  , f^#(x, y) -> c_5(ack^#(x, y))
                  , ack^#(s(x), y) -> c_6(f^#(x, x))
                  , ack^#(s(x), s(y)) -> c_2(ack^#(x, ack(s(x), y)))
                  , f^#(x, s(y)) -> c_4(f^#(y, x))
                  , f^#(s(x), y) -> c_3(f^#(x, s(x)))
                  , ack^#(0(), y) -> c_0(y)
                  , ack(0(), y) -> s(y)
                  , ack(s(x), 0()) -> ack(x, s(0()))
                  , ack(s(x), s(y)) -> ack(x, ack(s(x), y))
                  , ack(s(x), y) -> f(x, x)
                  , f(s(x), y) -> f(x, s(x))
                  , f(x, s(y)) -> f(y, x)
                  , f(x, y) -> ack(x, y)}
             
             Proof Output:    
               The input cannot be shown compatible
    
    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.