Problem AG01 3.17

Tool CaT

Execution Time	Unknown
Answer	MAYBE
Input	AG01 3.17

stdout:

MAYBE

Problem:
app(nil(),k) -> k
app(l,nil()) -> l
app(cons(x,l),k) -> cons(x,app(l,k))
sum(cons(x,nil())) -> cons(x,nil())
sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l))
sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k)))))
plus(0(),y) -> y
plus(s(x),y) -> s(plus(x,y))

Proof:
Complexity Transformation Processor:
  strict:
   app(nil(),k) -> k
   app(l,nil()) -> l
   app(cons(x,l),k) -> cons(x,app(l,k))
   sum(cons(x,nil())) -> cons(x,nil())
   sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l))
   sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k)))))
   plus(0(),y) -> y
   plus(s(x),y) -> s(plus(x,y))
  weak:

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

     [0] = 19,

     [plus](x0, x1) = x0 + x1 + 47,

     [sum](x0) = x0 + 36,

     [cons](x0, x1) = x0 + x1 + 76,

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

     [nil] = 102
    orientation:
     app(nil(),k) = k + 114 >= k = k

     app(l,nil()) = l + 114 >= l = l

     app(cons(x,l),k) = k + l + x + 88 >= k + l + x + 88 = cons(x,app(l,k))

     sum(cons(x,nil())) = x + 214 >= x + 178 = cons(x,nil())

     sum(cons(x,cons(y,l))) = l + x + y + 188 >= l + x + y + 159 = sum(cons(plus(x,y),l))

     sum(app(l,cons(x,cons(y,k)))) = k + l + x + y + 200 >= k + l + x + y + 236 = sum(app(l,sum(cons(x,cons(y,k)))))

     plus(0(),y) = y + 66 >= y = y

     plus(s(x),y) = x + y + 112 >= x + y + 112 = s(plus(x,y))
    problem:
     strict:
      app(cons(x,l),k) -> cons(x,app(l,k))
      sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k)))))
      plus(s(x),y) -> s(plus(x,y))
     weak:
      app(nil(),k) -> k
      app(l,nil()) -> l
      sum(cons(x,nil())) -> cons(x,nil())
      sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l))
      plus(0(),y) -> y
    Bounds Processor:
     bound: 0
     enrichment: match
     automaton:
      final states: {7,6,5}
      transitions:
       app0(3,1) -> 5*
       app0(3,3) -> 5*
       app0(4,2) -> 5*
       app0(4,4) -> 5*
       app0(1,2) -> 5*
       app0(1,4) -> 5*
       app0(2,1) -> 5*
       app0(2,3) -> 5*
       app0(3,2) -> 5*
       app0(3,4) -> 5*
       app0(4,1) -> 5*
       app0(4,3) -> 5*
       app0(1,1) -> 5*
       app0(1,3) -> 5*
       app0(2,2) -> 5*
       app0(2,4) -> 5*
       cons0(3,1) -> 1*
       cons0(3,3) -> 6,1
       cons0(3,5) -> 5*
       cons0(4,2) -> 1*
       cons0(4,4) -> 1*
       cons0(1,2) -> 1*
       cons0(1,4) -> 1*
       cons0(7,1) -> 1*
       cons0(2,1) -> 1*
       cons0(7,3) -> 6,1
       cons0(2,3) -> 6,1
       cons0(7,5) -> 5*
       cons0(2,5) -> 5*
       cons0(3,2) -> 1*
       cons0(3,4) -> 1*
       cons0(4,1) -> 1*
       cons0(4,3) -> 6,1
       cons0(4,5) -> 5*
       cons0(1,1) -> 1*
       cons0(1,3) -> 6,1
       cons0(1,5) -> 5*
       cons0(7,2) -> 1*
       cons0(2,2) -> 1*
       cons0(7,4) -> 1*
       cons0(2,4) -> 1*
       sum0(2) -> 6*
       sum0(4) -> 6*
       sum0(1) -> 6*
       sum0(3) -> 6*
       plus0(3,1) -> 7*
       plus0(3,3) -> 7*
       plus0(3,7) -> 1*
       plus0(4,2) -> 7*
       plus0(4,4) -> 7*
       plus0(1,2) -> 7*
       plus0(1,4) -> 7*
       plus0(7,1) -> 1*
       plus0(2,1) -> 7*
       plus0(7,3) -> 1*
       plus0(2,3) -> 7*
       plus0(7,7) -> 1*
       plus0(3,2) -> 7*
       plus0(3,4) -> 7*
       plus0(4,1) -> 7*
       plus0(4,3) -> 7*
       plus0(1,1) -> 7*
       plus0(1,3) -> 7*
       plus0(2,2) -> 7*
       plus0(7,4) -> 1*
       plus0(2,4) -> 7*
       s0(7) -> 7*
       s0(2) -> 2*
       s0(4) -> 2*
       s0(1) -> 1,2
       s0(3) -> 2*
       nil0() -> 3*
       00() -> 4*
       1 -> 7,5
       2 -> 7,5
       3 -> 7,5
       4 -> 1,7,5
       7 -> 1*
     problem:
      strict:
       app(cons(x,l),k) -> cons(x,app(l,k))
       plus(s(x),y) -> s(plus(x,y))
      weak:
       sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k)))))
       app(nil(),k) -> k
       app(l,nil()) -> l
       sum(cons(x,nil())) -> cons(x,nil())
       sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l))
       plus(0(),y) -> y
     Bounds Processor:
      bound: 1
      enrichment: match
      automaton:
       final states: {7,6,5}
       transitions:
        cons1(4,8) -> 8,5
        cons1(4,10) -> 8,5
        cons1(6,8) -> 8,5
        cons1(1,8) -> 8,5
        cons1(6,10) -> 8,5
        cons1(1,10) -> 8,5
        cons1(3,8) -> 8,5
        cons1(3,10) -> 8,5
        cons1(2,8) -> 8,5
        cons1(2,10) -> 8,5
        app1(3,1) -> 8*
        app1(3,3) -> 8*
        app1(4,2) -> 8*
        app1(4,4) -> 8*
        app1(1,2) -> 8*
        app1(1,4) -> 8*
        app1(2,1) -> 8*
        app1(2,3) -> 10*
        app1(3,2) -> 8*
        app1(3,4) -> 8*
        app1(4,1) -> 8*
        app1(4,3) -> 10*
        app1(1,1) -> 8*
        app1(1,3) -> 8*
        app1(2,2) -> 8*
        app1(2,4) -> 8*
        app0(3,1) -> 5*
        app0(3,3) -> 5*
        app0(4,2) -> 5*
        app0(4,4) -> 5*
        app0(1,2) -> 5*
        app0(1,4) -> 5*
        app0(2,1) -> 5*
        app0(2,3) -> 5*
        app0(3,2) -> 5*
        app0(3,4) -> 5*
        app0(4,1) -> 5*
        app0(4,3) -> 5*
        app0(1,1) -> 5*
        app0(1,3) -> 5*
        app0(2,2) -> 5*
        app0(2,4) -> 5*
        cons0(3,1) -> 1*
        cons0(3,3) -> 7,1
        cons0(4,2) -> 1*
        cons0(4,4) -> 1*
        cons0(6,2) -> 1*
        cons0(1,2) -> 1*
        cons0(6,4) -> 1*
        cons0(1,4) -> 1*
        cons0(2,1) -> 1*
        cons0(2,3) -> 7,1
        cons0(3,2) -> 1*
        cons0(3,4) -> 1*
        cons0(4,1) -> 1*
        cons0(4,3) -> 7,1
        cons0(6,1) -> 1*
        cons0(1,1) -> 1*
        cons0(6,3) -> 7,1
        cons0(1,3) -> 7,1
        cons0(2,2) -> 1*
        cons0(2,4) -> 1*
        sum0(2) -> 7*
        sum0(4) -> 7*
        sum0(1) -> 7*
        sum0(3) -> 7*
        plus0(3,1) -> 6*
        plus0(3,3) -> 6*
        plus0(4,2) -> 6*
        plus0(4,4) -> 6*
        plus0(4,6) -> 1*
        plus0(1,2) -> 6*
        plus0(6,4) -> 1*
        plus0(1,4) -> 6*
        plus0(6,6) -> 1*
        plus0(2,1) -> 6*
        plus0(2,3) -> 6*
        plus0(3,2) -> 6*
        plus0(3,4) -> 6*
        plus0(3,6) -> 1*
        plus0(4,1) -> 6*
        plus0(4,3) -> 6*
        plus0(1,1) -> 6*
        plus0(6,3) -> 1*
        plus0(1,3) -> 6*
        plus0(2,2) -> 6*
        plus0(2,4) -> 6*
        plus0(2,6) -> 1*
        s0(2) -> 2*
        s0(4) -> 2*
        s0(6) -> 6*
        s0(1) -> 1,2
        s0(3) -> 2*
        nil0() -> 3*
        00() -> 4*
        1 -> 6,8,5
        2 -> 6,10,8,5
        3 -> 1,6,8,5
        4 -> 6,10,8,5
        6 -> 1*
      problem:
       strict:
        plus(s(x),y) -> s(plus(x,y))
       weak:
        app(cons(x,l),k) -> cons(x,app(l,k))
        sum(app(l,cons(x,cons(y,k)))) -> sum(app(l,sum(cons(x,cons(y,k)))))
        app(nil(),k) -> k
        app(l,nil()) -> l
        sum(cons(x,nil())) -> cons(x,nil())
        sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l))
        plus(0(),y) -> y
      Open

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	AG01 3.17

stdout:

MAYBE

Tool IRC2

Execution Time	Unknown
Answer	TIMEOUT
Input	AG01 3.17

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  app(nil(), k) -> k
     , app(l, nil()) -> l
     , app(cons(x, l), k) -> cons(x, app(l, k))
     , sum(cons(x, nil())) -> cons(x, nil())
     , sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
     , sum(app(l, cons(x, cons(y, k)))) ->
       sum(app(l, sum(cons(x, cons(y, k)))))
     , plus(0(), y) -> y
     , plus(s(x), y) -> s(plus(x, y))}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution Time	Unknown
Answer	MAYBE
Input	AG01 3.17

stdout:

MAYBE

Tool RC2

Execution Time	Unknown
Answer	TIMEOUT
Input	AG01 3.17

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  app(nil(), k) -> k
     , app(l, nil()) -> l
     , app(cons(x, l), k) -> cons(x, app(l, k))
     , sum(cons(x, nil())) -> cons(x, nil())
     , sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
     , sum(app(l, cons(x, cons(y, k)))) ->
       sum(app(l, sum(cons(x, cons(y, k)))))
     , plus(0(), y) -> y
     , plus(s(x), y) -> s(plus(x, y))}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds

Tool pair1rc

Execution Time	Unknown
Answer	TIMEOUT
Input	AG01 3.17

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  app(nil(), k) -> k
     , app(l, nil()) -> l
     , app(cons(x, l), k) -> cons(x, app(l, k))
     , sum(cons(x, nil())) -> cons(x, nil())
     , sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
     , sum(app(l, cons(x, cons(y, k)))) ->
       sum(app(l, sum(cons(x, cons(y, k)))))
     , plus(0(), y) -> y
     , plus(s(x), y) -> s(plus(x, y))}
  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.17

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  app(nil(), k) -> k
     , app(l, nil()) -> l
     , app(cons(x, l), k) -> cons(x, app(l, k))
     , sum(cons(x, nil())) -> cons(x, nil())
     , sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
     , sum(app(l, cons(x, cons(y, k)))) ->
       sum(app(l, sum(cons(x, cons(y, k)))))
     , plus(0(), y) -> y
     , plus(s(x), y) -> s(plus(x, y))}
  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.17

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  app(nil(), k) -> k
     , app(l, nil()) -> l
     , app(cons(x, l), k) -> cons(x, app(l, k))
     , sum(cons(x, nil())) -> cons(x, nil())
     , sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
     , sum(app(l, cons(x, cons(y, k)))) ->
       sum(app(l, sum(cons(x, cons(y, k)))))
     , plus(0(), y) -> y
     , plus(s(x), y) -> s(plus(x, y))}
  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.17

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  app(nil(), k) -> k
     , app(l, nil()) -> l
     , app(cons(x, l), k) -> cons(x, app(l, k))
     , sum(cons(x, nil())) -> cons(x, nil())
     , sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
     , sum(app(l, cons(x, cons(y, k)))) ->
       sum(app(l, sum(cons(x, cons(y, k)))))
     , plus(0(), y) -> y
     , plus(s(x), y) -> s(plus(x, y))}
  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.17

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  app(nil(), k) -> k
     , app(l, nil()) -> l
     , app(cons(x, l), k) -> cons(x, app(l, k))
     , sum(cons(x, nil())) -> cons(x, nil())
     , sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
     , sum(app(l, cons(x, cons(y, k)))) ->
       sum(app(l, sum(cons(x, cons(y, k)))))
     , plus(0(), y) -> y
     , plus(s(x), y) -> s(plus(x, y))}
  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.313763ms
Answer	TIMEOUT
Input	AG01 3.17

stdout:

TIMEOUT

We consider the following Problem:

  Strict Trs:
    {  app(nil(), k) -> k
     , app(l, nil()) -> l
     , app(cons(x, l), k) -> cons(x, app(l, k))
     , sum(cons(x, nil())) -> cons(x, nil())
     , sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
     , sum(app(l, cons(x, cons(y, k)))) ->
       sum(app(l, sum(cons(x, cons(y, k)))))
     , plus(0(), y) -> y
     , plus(s(x), y) -> s(plus(x, y))}
  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..