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 secondsTool 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 secondsTool 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..