Problem AG01 3.17a

Tool CaT

Execution TimeUnknown
Answer
MAYBE
InputAG01 3.17a

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))
 sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l))))
 pred(cons(s(x),nil())) -> cons(x,nil())

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))
   sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l))))
   pred(cons(s(x),nil())) -> cons(x,nil())
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [pred](x0) = x0 + 25,
     
     [s](x0) = x0 + 88,
     
     [0] = 91,
     
     [plus](x0, x1) = x0 + x1 + 165,
     
     [sum](x0) = x0 + 11,
     
     [cons](x0, x1) = x0 + x1 + 65,
     
     [app](x0, x1) = x0 + x1 + 190,
     
     [nil] = 208
    orientation:
     app(nil(),k) = k + 398 >= k = k
     
     app(l,nil()) = l + 398 >= l = l
     
     app(cons(x,l),k) = k + l + x + 255 >= k + l + x + 255 = cons(x,app(l,k))
     
     sum(cons(x,nil())) = x + 284 >= x + 273 = cons(x,nil())
     
     sum(cons(x,cons(y,l))) = l + x + y + 141 >= l + x + y + 241 = sum(cons(plus(x,y),l))
     
     sum(app(l,cons(x,cons(y,k)))) = k + l + x + y + 331 >= k + l + x + y + 342 = sum(app(l,sum(cons(x,cons(y,k)))))
     
     plus(0(),y) = y + 256 >= y = y
     
     plus(s(x),y) = x + y + 253 >= x + y + 253 = s(plus(x,y))
     
     sum(plus(cons(0(),x),cons(y,l))) = l + x + y + 397 >= l + x + y + 254 = pred(sum(cons(s(x),cons(y,l))))
     
     pred(cons(s(x),nil())) = x + 386 >= x + 273 = cons(x,nil())
    problem:
     strict:
      app(cons(x,l),k) -> cons(x,app(l,k))
      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(s(x),y) -> s(plus(x,y))
     weak:
      app(nil(),k) -> k
      app(l,nil()) -> l
      sum(cons(x,nil())) -> cons(x,nil())
      plus(0(),y) -> y
      sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l))))
      pred(cons(s(x),nil())) -> cons(x,nil())
    Bounds Processor:
     bound: 0
     enrichment: match
     automaton:
      final states: {8,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) -> 8,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) -> 8,6,1
       cons0(2,3) -> 8,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) -> 8,6,1
       cons0(4,5) -> 5*
       cons0(1,1) -> 1*
       cons0(1,3) -> 8,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*
       pred0(2) -> 8*
       pred0(4) -> 8*
       pred0(6) -> 6*
       pred0(1) -> 8*
       pred0(3) -> 8*
       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))
       sum(cons(x,cons(y,l))) -> sum(cons(plus(x,y),l))
       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())
       plus(0(),y) -> y
       sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l))))
       pred(cons(s(x),nil())) -> cons(x,nil())
     Matrix Interpretation Processor:
      dimension: 1
      max_matrix:
       1
       interpretation:
        [pred](x0) = x0,
        
        [s](x0) = x0 + 83,
        
        [0] = 83,
        
        [plus](x0, x1) = x0 + x1,
        
        [sum](x0) = x0,
        
        [cons](x0, x1) = x0 + x1 + 2,
        
        [app](x0, x1) = x0 + x1 + 103,
        
        [nil] = 78
       orientation:
        app(cons(x,l),k) = k + l + x + 105 >= k + l + x + 105 = cons(x,app(l,k))
        
        sum(cons(x,cons(y,l))) = l + x + y + 4 >= l + x + y + 2 = sum(cons(plus(x,y),l))
        
        plus(s(x),y) = x + y + 83 >= x + y + 83 = s(plus(x,y))
        
        sum(app(l,cons(x,cons(y,k)))) = k + l + x + y + 107 >= k + l + x + y + 107 = sum(app(l,sum(cons(x,cons(y,k)))))
        
        app(nil(),k) = k + 181 >= k = k
        
        app(l,nil()) = l + 181 >= l = l
        
        sum(cons(x,nil())) = x + 80 >= x + 80 = cons(x,nil())
        
        plus(0(),y) = y + 83 >= y = y
        
        sum(plus(cons(0(),x),cons(y,l))) = l + x + y + 87 >= l + x + y + 87 = pred(sum(cons(s(x),cons(y,l))))
        
        pred(cons(s(x),nil())) = x + 163 >= x + 80 = cons(x,nil())
       problem:
        strict:
         app(cons(x,l),k) -> cons(x,app(l,k))
         plus(s(x),y) -> s(plus(x,y))
        weak:
         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)))))
         app(nil(),k) -> k
         app(l,nil()) -> l
         sum(cons(x,nil())) -> cons(x,nil())
         plus(0(),y) -> y
         sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l))))
         pred(cons(s(x),nil())) -> cons(x,nil())
       Bounds Processor:
        bound: 1
        enrichment: match
        automaton:
         final states: {8,7,6,5}
         transitions:
          cons1(3,9) -> 9,5
          cons1(3,11) -> 9,5
          cons1(2,9) -> 9,5
          cons1(2,11) -> 9,5
          cons1(4,9) -> 9,5
          cons1(4,11) -> 9,5
          cons1(6,9) -> 9,5
          cons1(1,9) -> 9,5
          cons1(6,11) -> 9,5
          cons1(1,11) -> 9,5
          app1(3,1) -> 9*
          app1(3,3) -> 9*
          app1(4,2) -> 9*
          app1(4,4) -> 9*
          app1(1,2) -> 9*
          app1(1,4) -> 9*
          app1(2,1) -> 9*
          app1(2,3) -> 11*
          app1(3,2) -> 9*
          app1(3,4) -> 9*
          app1(4,1) -> 9*
          app1(4,3) -> 11*
          app1(1,1) -> 9*
          app1(1,3) -> 9*
          app1(2,2) -> 9*
          app1(2,4) -> 9*
          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) -> 8,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) -> 8,7,1
          cons0(3,2) -> 1*
          cons0(3,4) -> 1*
          cons0(4,1) -> 1*
          cons0(4,3) -> 8,7,1
          cons0(6,1) -> 1*
          cons0(1,1) -> 1*
          cons0(6,3) -> 8,7,1
          cons0(1,3) -> 8,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*
          pred0(7) -> 7*
          pred0(2) -> 8*
          pred0(4) -> 8*
          pred0(1) -> 8*
          pred0(3) -> 8*
          1 -> 6,9,5
          2 -> 6,11,9,5
          3 -> 1,6,9,5
          4 -> 6,11,9,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(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)))))
          app(nil(),k) -> k
          app(l,nil()) -> l
          sum(cons(x,nil())) -> cons(x,nil())
          plus(0(),y) -> y
          sum(plus(cons(0(),x),cons(y,l))) -> pred(sum(cons(s(x),cons(y,l))))
          pred(cons(s(x),nil())) -> cons(x,nil())
        Open
  

Tool IRC1

Execution TimeUnknown
Answer
MAYBE
InputAG01 3.17a

stdout:

MAYBE

Tool IRC2

Execution TimeUnknown
Answer
TIMEOUT
InputAG01 3.17a

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))
     , sum(plus(cons(0(), x), cons(y, l))) ->
       pred(sum(cons(s(x), cons(y, l))))
     , pred(cons(s(x), nil())) -> cons(x, nil())}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution TimeUnknown
Answer
MAYBE
InputAG01 3.17a

stdout:

MAYBE

Tool RC2

Execution TimeUnknown
Answer
TIMEOUT
InputAG01 3.17a

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))
     , sum(plus(cons(0(), x), cons(y, l))) ->
       pred(sum(cons(s(x), cons(y, l))))
     , pred(cons(s(x), nil())) -> cons(x, nil())}

Proof Output:    
  Computation stopped due to timeout after 60.0 seconds

Tool pair1rc

Execution TimeUnknown
Answer
TIMEOUT
InputAG01 3.17a

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))
     , sum(plus(cons(0(), x), cons(y, l))) ->
       pred(sum(cons(s(x), cons(y, l))))
     , pred(cons(s(x), nil())) -> cons(x, nil())}
  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.17a

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))
     , sum(plus(cons(0(), x), cons(y, l))) ->
       pred(sum(cons(s(x), cons(y, l))))
     , pred(cons(s(x), nil())) -> cons(x, nil())}
  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
TIMEOUT
InputAG01 3.17a

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))
     , sum(plus(cons(0(), x), cons(y, l))) ->
       pred(sum(cons(s(x), cons(y, l))))
     , pred(cons(s(x), nil())) -> cons(x, nil())}
  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 TimeUnknown
Answer
TIMEOUT
InputAG01 3.17a

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))
     , sum(plus(cons(0(), x), cons(y, l))) ->
       pred(sum(cons(s(x), cons(y, l))))
     , pred(cons(s(x), nil())) -> cons(x, nil())}
  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
TIMEOUT
InputAG01 3.17a

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))
     , sum(plus(cons(0(), x), cons(y, l))) ->
       pred(sum(cons(s(x), cons(y, l))))
     , pred(cons(s(x), nil())) -> cons(x, nil())}
  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 Time63.038643ms
Answer
TIMEOUT
InputAG01 3.17a

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))
     , sum(plus(cons(0(), x), cons(y, l))) ->
       pred(sum(cons(s(x), cons(y, l))))
     , pred(cons(s(x), nil())) -> cons(x, nil())}
  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..