Tool CaT
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
stdout:
MAYBE
Tool IRC2
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 secondsTool RC1
stdout:
MAYBE
Tool RC2
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 secondsTool pair1rc
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
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
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
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
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 Time | 63.038643ms |
---|
Answer | TIMEOUT |
---|
Input | AG01 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..