Problem AG01 3.12

Tool CaT

Execution Time	Unknown
Answer	MAYBE
Input	AG01 3.12

stdout:

MAYBE

Problem:
app(nil(),y) -> y
app(add(n,x),y) -> add(n,app(x,y))
reverse(nil()) -> nil()
reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
shuffle(nil()) -> nil()
shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))

Proof:
Complexity Transformation Processor:
  strict:
   app(nil(),y) -> y
   app(add(n,x),y) -> add(n,app(x,y))
   reverse(nil()) -> nil()
   reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
   shuffle(nil()) -> nil()
   shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
  weak:

  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [shuffle](x0) = x0 + 16,

     [reverse](x0) = x0,

     [add](x0, x1) = x0 + x1 + 145,

     [app](x0, x1) = x0 + x1 + 154,

     [nil] = 7
    orientation:
     app(nil(),y) = y + 161 >= y = y

     app(add(n,x),y) = n + x + y + 299 >= n + x + y + 299 = add(n,app(x,y))

     reverse(nil()) = 7 >= 7 = nil()

     reverse(add(n,x)) = n + x + 145 >= n + x + 306 = app(reverse(x),add(n,nil()))

     shuffle(nil()) = 23 >= 7 = nil()

     shuffle(add(n,x)) = n + x + 161 >= n + x + 161 = add(n,shuffle(reverse(x)))
    problem:
     strict:
      app(add(n,x),y) -> add(n,app(x,y))
      reverse(nil()) -> nil()
      reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
      shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
     weak:
      app(nil(),y) -> y
      shuffle(nil()) -> nil()
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [shuffle](x0) = x0 + 12,

       [reverse](x0) = x0 + 4,

       [add](x0, x1) = x0 + x1 + 8,

       [app](x0, x1) = x0 + x1,

       [nil] = 0
      orientation:
       app(add(n,x),y) = n + x + y + 8 >= n + x + y + 8 = add(n,app(x,y))

       reverse(nil()) = 4 >= 0 = nil()

       reverse(add(n,x)) = n + x + 12 >= n + x + 12 = app(reverse(x),add(n,nil()))

       shuffle(add(n,x)) = n + x + 20 >= n + x + 24 = add(n,shuffle(reverse(x)))

       app(nil(),y) = y >= y = y

       shuffle(nil()) = 12 >= 0 = nil()
      problem:
       strict:
        app(add(n,x),y) -> add(n,app(x,y))
        reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
        shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
       weak:
        reverse(nil()) -> nil()
        app(nil(),y) -> y
        shuffle(nil()) -> nil()
      Matrix Interpretation Processor:
       dimension: 2
       max_matrix:
        [1 1]
        [0 1]
        interpretation:
                         [1 1]     [1]
         [shuffle](x0) = [0 1]x0 + [1],

                              [1]
         [reverse](x0) = x0 + [0],

                         [1 0]          [0]
         [add](x0, x1) = [0 0]x0 + x1 + [2],


         [app](x0, x1) = x0 + x1,

                 [0]
         [nil] = [0]
        orientation:
                           [1 0]            [0]    [1 0]            [0]
         app(add(n,x),y) = [0 0]n + x + y + [2] >= [0 0]n + x + y + [2] = add(n,app(x,y))

                             [1 0]        [1]    [1 0]        [1]
         reverse(add(n,x)) = [0 0]n + x + [2] >= [0 0]n + x + [2] = app(reverse(x),add(n,nil()))

                             [1 0]    [1 1]    [3]    [1 0]    [1 1]    [2]
         shuffle(add(n,x)) = [0 0]n + [0 1]x + [3] >= [0 0]n + [0 1]x + [3] = add(n,shuffle(reverse(x)))

                          [1]    [0]
         reverse(nil()) = [0] >= [0] = nil()


         app(nil(),y) = y >= y = y

                          [1]    [0]
         shuffle(nil()) = [1] >= [0] = nil()
        problem:
         strict:
          app(add(n,x),y) -> add(n,app(x,y))
          reverse(add(n,x)) -> app(reverse(x),add(n,nil()))
         weak:
          shuffle(add(n,x)) -> add(n,shuffle(reverse(x)))
          reverse(nil()) -> nil()
          app(nil(),y) -> y
          shuffle(nil()) -> nil()
        Open

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	AG01 3.12

stdout:

MAYBE

Tool IRC2

Execution Time	Unknown
Answer	TIMEOUT
Input	AG01 3.12

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  app(nil(), y) -> y
     , app(add(n, x), y) -> add(n, app(x, y))
     , reverse(nil()) -> nil()
     , reverse(add(n, x)) -> app(reverse(x), add(n, nil()))
     , shuffle(nil()) -> nil()
     , shuffle(add(n, x)) -> add(n, shuffle(reverse(x)))}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution Time	Unknown
Answer	MAYBE
Input	AG01 3.12

stdout:

MAYBE

Tool RC2

Execution Time	Unknown
Answer	TIMEOUT
Input	AG01 3.12

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  app(nil(), y) -> y
     , app(add(n, x), y) -> add(n, app(x, y))
     , reverse(nil()) -> nil()
     , reverse(add(n, x)) -> app(reverse(x), add(n, nil()))
     , shuffle(nil()) -> nil()
     , shuffle(add(n, x)) -> add(n, shuffle(reverse(x)))}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds

Tool pair1rc

Execution Time	Unknown
Answer	TIMEOUT
Input	AG01 3.12

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  app(nil(), y) -> y
     , app(add(n, x), y) -> add(n, app(x, y))
     , reverse(nil()) -> nil()
     , reverse(add(n, x)) -> app(reverse(x), add(n, nil()))
     , shuffle(nil()) -> nil()
     , shuffle(add(n, x)) -> add(n, shuffle(reverse(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 Time	Unknown
Answer	TIMEOUT
Input	AG01 3.12

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  app(nil(), y) -> y
     , app(add(n, x), y) -> add(n, app(x, y))
     , reverse(nil()) -> nil()
     , reverse(add(n, x)) -> app(reverse(x), add(n, nil()))
     , shuffle(nil()) -> nil()
     , shuffle(add(n, x)) -> add(n, shuffle(reverse(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 Time	Unknown
Answer	TIMEOUT
Input	AG01 3.12

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  app(nil(), y) -> y
     , app(add(n, x), y) -> add(n, app(x, y))
     , reverse(nil()) -> nil()
     , reverse(add(n, x)) -> app(reverse(x), add(n, nil()))
     , shuffle(nil()) -> nil()
     , shuffle(add(n, x)) -> add(n, shuffle(reverse(x)))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: TIMEOUT

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

Arrrr..

Tool pair3rc

Execution Time	Unknown
Answer	TIMEOUT
Input	AG01 3.12

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  app(nil(), y) -> y
     , app(add(n, x), y) -> add(n, app(x, y))
     , reverse(nil()) -> nil()
     , reverse(add(n, x)) -> app(reverse(x), add(n, nil()))
     , shuffle(nil()) -> nil()
     , shuffle(add(n, x)) -> add(n, shuffle(reverse(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 Time	Unknown
Answer	TIMEOUT
Input	AG01 3.12

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  app(nil(), y) -> y
     , app(add(n, x), y) -> add(n, app(x, y))
     , reverse(nil()) -> nil()
     , reverse(add(n, x)) -> app(reverse(x), add(n, nil()))
     , shuffle(nil()) -> nil()
     , shuffle(add(n, x)) -> add(n, shuffle(reverse(x)))}
  StartTerms: basic terms
  Strategy: none

Certificate: TIMEOUT

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

Arrrr..

Tool tup3irc

Execution Time	60.21536ms
Answer	TIMEOUT
Input	AG01 3.12

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  app(nil(), y) -> y
     , app(add(n, x), y) -> add(n, app(x, y))
     , reverse(nil()) -> nil()
     , reverse(add(n, x)) -> app(reverse(x), add(n, nil()))
     , shuffle(nil()) -> nil()
     , shuffle(add(n, x)) -> add(n, shuffle(reverse(x)))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: TIMEOUT

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

Arrrr..