Problem AG01 3.42

Tool CaT

Execution TimeUnknown
Answer
MAYBE
InputAG01 3.42

stdout:

MAYBE

Problem:
 half(0()) -> 0()
 half(s(0())) -> 0()
 half(s(s(x))) -> s(half(x))
 lastbit(0()) -> 0()
 lastbit(s(0())) -> s(0())
 lastbit(s(s(x))) -> lastbit(x)
 conv(0()) -> cons(nil(),0())
 conv(s(x)) -> cons(conv(half(s(x))),lastbit(s(x)))

Proof:
 Open

Tool IRC1

Execution TimeUnknown
Answer
MAYBE
InputAG01 3.42

stdout:

MAYBE

Tool IRC2

Execution TimeUnknown
Answer
TIMEOUT
InputAG01 3.42

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  half(0()) -> 0()
     , half(s(0())) -> 0()
     , half(s(s(x))) -> s(half(x))
     , lastbit(0()) -> 0()
     , lastbit(s(0())) -> s(0())
     , lastbit(s(s(x))) -> lastbit(x)
     , conv(0()) -> cons(nil(), 0())
     , conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution TimeUnknown
Answer
MAYBE
InputAG01 3.42

stdout:

MAYBE

Tool RC2

Execution TimeUnknown
Answer
TIMEOUT
InputAG01 3.42

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  half(0()) -> 0()
     , half(s(0())) -> 0()
     , half(s(s(x))) -> s(half(x))
     , lastbit(0()) -> 0()
     , lastbit(s(0())) -> s(0())
     , lastbit(s(s(x))) -> lastbit(x)
     , conv(0()) -> cons(nil(), 0())
     , conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds

Tool pair1rc

Execution TimeUnknown
Answer
TIMEOUT
InputAG01 3.42

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  half(0()) -> 0()
     , half(s(0())) -> 0()
     , half(s(s(x))) -> s(half(x))
     , lastbit(0()) -> 0()
     , lastbit(s(0())) -> s(0())
     , lastbit(s(s(x))) -> lastbit(x)
     , conv(0()) -> cons(nil(), 0())
     , conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))}
  StartTerms: basic terms
  Strategy: none

Certificate: TIMEOUT

Application of 'pair1 (timeout of 60.0 seconds)':
-------------------------------------------------
  Computation stopped due to timeout after 60.0 seconds

Arrrr..

Tool pair2rc

Execution TimeUnknown
Answer
TIMEOUT
InputAG01 3.42

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  half(0()) -> 0()
     , half(s(0())) -> 0()
     , half(s(s(x))) -> s(half(x))
     , lastbit(0()) -> 0()
     , lastbit(s(0())) -> s(0())
     , lastbit(s(s(x))) -> lastbit(x)
     , conv(0()) -> cons(nil(), 0())
     , conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))}
  StartTerms: basic terms
  Strategy: none

Certificate: TIMEOUT

Application of 'pair2 (timeout of 60.0 seconds)':
-------------------------------------------------
  Computation stopped due to timeout after 60.0 seconds

Arrrr..

Tool pair3irc

Execution TimeUnknown
Answer
YES(?,O(n^3))
InputAG01 3.42

stdout:

YES(?,O(n^3))

We consider the following Problem:

  Strict Trs:
    {  half(0()) -> 0()
     , half(s(0())) -> 0()
     , half(s(s(x))) -> s(half(x))
     , lastbit(0()) -> 0()
     , lastbit(s(0())) -> s(0())
     , lastbit(s(s(x))) -> lastbit(x)
     , conv(0()) -> cons(nil(), 0())
     , conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,O(n^3))

Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
  The input problem contains no overlaps that give rise to inapplicable rules.
  
  We abort the transformation and continue with the subprocessor on the problem
  
  Strict Trs:
    {  half(0()) -> 0()
     , half(s(0())) -> 0()
     , half(s(s(x))) -> s(half(x))
     , lastbit(0()) -> 0()
     , lastbit(s(0())) -> s(0())
     , lastbit(s(s(x))) -> lastbit(x)
     , conv(0()) -> cons(nil(), 0())
     , conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))}
  StartTerms: basic terms
  Strategy: innermost
  
  1) 'Fastest' proved the goal fastest:
     
     'Sequentially' proved the goal fastest:
     
     'Fastest' succeeded:
     
     'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' proved the goal fastest:
     
     The following argument positions are usable:
       Uargs(half) = {}, Uargs(s) = {1}, Uargs(lastbit) = {},
       Uargs(conv) = {1}, Uargs(cons) = {1, 2}
     We have the following constructor-restricted (at most 3 in the main diagonals) matrix interpretation:
     Interpretation Functions:
      half(x1) = [1 0 0 0] x1 + [1]
                 [0 0 1 0]      [0]
                 [0 0 1 0]      [0]
                 [0 0 0 1]      [0]
      0() = [0]
            [2]
            [2]
            [1]
      s(x1) = [1 0 0 0] x1 + [1]
              [0 0 1 2]      [2]
              [0 0 1 1]      [0]
              [0 0 0 1]      [2]
      lastbit(x1) = [0 0 0 1] x1 + [0]
                    [2 0 1 0]      [1]
                    [1 0 0 0]      [2]
                    [1 0 0 0]      [2]
      conv(x1) = [1 2 0 0] x1 + [0]
                 [0 0 0 0]      [0]
                 [0 0 0 0]      [0]
                 [0 2 0 0]      [0]
      cons(x1, x2) = [1 0 0 0] x1 + [1 0 0 0] x2 + [0]
                     [0 0 0 0]      [0 0 0 0]      [0]
                     [0 0 0 0]      [0 0 0 0]      [0]
                     [0 0 0 0]      [0 0 0 0]      [0]
      nil() = [0]
              [0]
              [0]
              [0]
  

Hurray, we answered YES(?,O(n^3))

Tool pair3rc

Execution TimeUnknown
Answer
TIMEOUT
InputAG01 3.42

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  half(0()) -> 0()
     , half(s(0())) -> 0()
     , half(s(s(x))) -> s(half(x))
     , lastbit(0()) -> 0()
     , lastbit(s(0())) -> s(0())
     , lastbit(s(s(x))) -> lastbit(x)
     , conv(0()) -> cons(nil(), 0())
     , conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))}
  StartTerms: basic terms
  Strategy: none

Certificate: TIMEOUT

Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
  Computation stopped due to timeout after 60.0 seconds

Arrrr..

Tool rc

Execution TimeUnknown
Answer
MAYBE
InputAG01 3.42

stdout:

MAYBE

We consider the following Problem:

  Strict Trs:
    {  half(0()) -> 0()
     , half(s(0())) -> 0()
     , half(s(s(x))) -> s(half(x))
     , lastbit(0()) -> 0()
     , lastbit(s(0())) -> s(0())
     , lastbit(s(s(x))) -> lastbit(x)
     , conv(0()) -> cons(nil(), 0())
     , conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))}
  StartTerms: basic terms
  Strategy: none

Certificate: MAYBE

Application of 'rc (timeout of 60.0 seconds)':
----------------------------------------------
  None of the processors succeeded.
  
  Details of failed attempt(s):
  -----------------------------
    1) 'dp' failed due to the following reason:
         We have computed the following dependency pairs
         
         Strict Dependency Pairs:
           {  half^#(0()) -> c_1()
            , half^#(s(0())) -> c_2()
            , half^#(s(s(x))) -> c_3(half^#(x))
            , lastbit^#(0()) -> c_4()
            , lastbit^#(s(0())) -> c_5()
            , lastbit^#(s(s(x))) -> c_6(lastbit^#(x))
            , conv^#(0()) -> c_7()
            , conv^#(s(x)) -> c_8(conv^#(half(s(x))), lastbit^#(s(x)))}
         
         We consider the following Problem:
         
           Strict DPs:
             {  half^#(0()) -> c_1()
              , half^#(s(0())) -> c_2()
              , half^#(s(s(x))) -> c_3(half^#(x))
              , lastbit^#(0()) -> c_4()
              , lastbit^#(s(0())) -> c_5()
              , lastbit^#(s(s(x))) -> c_6(lastbit^#(x))
              , conv^#(0()) -> c_7()
              , conv^#(s(x)) -> c_8(conv^#(half(s(x))), lastbit^#(s(x)))}
           Strict Trs:
             {  half(0()) -> 0()
              , half(s(0())) -> 0()
              , half(s(s(x))) -> s(half(x))
              , lastbit(0()) -> 0()
              , lastbit(s(0())) -> s(0())
              , lastbit(s(s(x))) -> lastbit(x)
              , conv(0()) -> cons(nil(), 0())
              , conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))}
           StartTerms: basic terms
           Strategy: none
         
         Certificate: MAYBE
         
         Application of 'usablerules':
         -----------------------------
           We replace strict/weak-rules by the corresponding usable rules:
           
             Strict Usable Rules:
               {  half(0()) -> 0()
                , half(s(0())) -> 0()
                , half(s(s(x))) -> s(half(x))}
           
           We consider the following Problem:
           
             Strict DPs:
               {  half^#(0()) -> c_1()
                , half^#(s(0())) -> c_2()
                , half^#(s(s(x))) -> c_3(half^#(x))
                , lastbit^#(0()) -> c_4()
                , lastbit^#(s(0())) -> c_5()
                , lastbit^#(s(s(x))) -> c_6(lastbit^#(x))
                , conv^#(0()) -> c_7()
                , conv^#(s(x)) -> c_8(conv^#(half(s(x))), lastbit^#(s(x)))}
             Strict Trs:
               {  half(0()) -> 0()
                , half(s(0())) -> 0()
                , half(s(s(x))) -> s(half(x))}
             StartTerms: basic terms
             Strategy: none
           
           Certificate: MAYBE
           
           Application of 'Fastest':
           -------------------------
             None of the processors succeeded.
             
    
    2) 'Fastest' failed due to the following reason:
         None of the processors succeeded.
         
         Details of failed attempt(s):
         -----------------------------
           1) 'Sequentially' failed due to the following reason:
                None of the processors succeeded.
                
                Details of failed attempt(s):
                -----------------------------
                  1) 'empty' failed due to the following reason:
                       Empty strict component of the problem is NOT empty.
                  
                  2) 'Fastest' failed due to the following reason:
                       None of the processors succeeded.
                       
                       Details of failed attempt(s):
                       -----------------------------
                         1) 'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' failed due to the following reason:
                              The input cannot be shown compatible
                         
                         2) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
                              The input cannot be shown compatible
                         
                         3) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
                              The input cannot be shown compatible
                         
                  
           
           2) 'Fastest' failed due to the following reason:
                None of the processors succeeded.
                
                Details of failed attempt(s):
                -----------------------------
                  1) 'Bounds with perSymbol-enrichment and initial automaton 'match' (timeout of 5.0 seconds)' failed due to the following reason:
                       match-boundness of the problem could not be verified.
                  
                  2) 'Bounds with minimal-enrichment and initial automaton 'match' (timeout of 100.0 seconds)' failed due to the following reason:
                       match-boundness of the problem could not be verified.
                  
           
    

Arrrr..

Tool tup3irc

Execution Time53.256447ms
Answer
YES(?,O(n^3))
InputAG01 3.42

stdout:

YES(?,O(n^3))

We consider the following Problem:

  Strict Trs:
    {  half(0()) -> 0()
     , half(s(0())) -> 0()
     , half(s(s(x))) -> s(half(x))
     , lastbit(0()) -> 0()
     , lastbit(s(0())) -> s(0())
     , lastbit(s(s(x))) -> lastbit(x)
     , conv(0()) -> cons(nil(), 0())
     , conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,O(n^3))

Application of 'tup3 (timeout of 60.0 seconds)':
------------------------------------------------
  The input problem contains no overlaps that give rise to inapplicable rules.
  
  We abort the transformation and continue with the subprocessor on the problem
  
  Strict Trs:
    {  half(0()) -> 0()
     , half(s(0())) -> 0()
     , half(s(s(x))) -> s(half(x))
     , lastbit(0()) -> 0()
     , lastbit(s(0())) -> s(0())
     , lastbit(s(s(x))) -> lastbit(x)
     , conv(0()) -> cons(nil(), 0())
     , conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))}
  StartTerms: basic terms
  Strategy: innermost
  
  1) 'Fastest' proved the goal fastest:
     
     'Sequentially' proved the goal fastest:
     
     'Fastest' succeeded:
     
     'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' proved the goal fastest:
     
     The following argument positions are usable:
       Uargs(half) = {}, Uargs(s) = {1}, Uargs(lastbit) = {},
       Uargs(conv) = {1}, Uargs(cons) = {1, 2}
     We have the following constructor-restricted (at most 3 in the main diagonals) matrix interpretation:
     Interpretation Functions:
      half(x1) = [1 0 0 0] x1 + [1]
                 [0 0 1 0]      [0]
                 [0 0 1 0]      [0]
                 [0 0 0 1]      [0]
      0() = [0]
            [2]
            [2]
            [1]
      s(x1) = [1 0 0 0] x1 + [1]
              [0 0 1 2]      [2]
              [0 0 1 1]      [0]
              [0 0 0 1]      [2]
      lastbit(x1) = [0 0 0 1] x1 + [0]
                    [2 0 1 0]      [1]
                    [1 0 0 0]      [2]
                    [1 0 0 0]      [2]
      conv(x1) = [1 2 0 0] x1 + [0]
                 [0 0 0 0]      [0]
                 [0 0 0 0]      [0]
                 [0 2 0 0]      [0]
      cons(x1, x2) = [1 0 0 0] x1 + [1 0 0 0] x2 + [0]
                     [0 0 0 0]      [0 0 0 0]      [0]
                     [0 0 0 0]      [0 0 0 0]      [0]
                     [0 0 0 0]      [0 0 0 0]      [0]
      nil() = [0]
              [0]
              [0]
              [0]
  

Hurray, we answered YES(?,O(n^3))