Tool CaT
Execution Time | Unknown |
---|
Answer | MAYBE |
---|
Input | AG01 3.42 |
---|
stdout:
MAYBE
Problem:
half(0()) -> 0()
half(s(0())) -> 0()
half(s(s(x))) -> s(half(x))
lastbit(0()) -> 0()
lastbit(s(0())) -> s(0())
lastbit(s(s(x))) -> lastbit(x)
conv(0()) -> cons(nil(),0())
conv(s(x)) -> cons(conv(half(s(x))),lastbit(s(x)))
Proof:
OpenTool IRC1
Execution Time | Unknown |
---|
Answer | MAYBE |
---|
Input | AG01 3.42 |
---|
stdout:
MAYBE
Tool IRC2
Execution Time | Unknown |
---|
Answer | TIMEOUT |
---|
Input | AG01 3.42 |
---|
stdout:
TIMEOUT
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: TIMEOUT
Input Problem: innermost runtime-complexity with respect to
Rules:
{ half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(x))) -> s(half(x))
, lastbit(0()) -> 0()
, lastbit(s(0())) -> s(0())
, lastbit(s(s(x))) -> lastbit(x)
, conv(0()) -> cons(nil(), 0())
, conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))}
Proof Output:
Computation stopped due to timeout after 60.0 secondsTool RC1
Execution Time | Unknown |
---|
Answer | MAYBE |
---|
Input | AG01 3.42 |
---|
stdout:
MAYBE
Tool RC2
Execution Time | Unknown |
---|
Answer | TIMEOUT |
---|
Input | AG01 3.42 |
---|
stdout:
TIMEOUT
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: TIMEOUT
Input Problem: runtime-complexity with respect to
Rules:
{ half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(x))) -> s(half(x))
, lastbit(0()) -> 0()
, lastbit(s(0())) -> s(0())
, lastbit(s(s(x))) -> lastbit(x)
, conv(0()) -> cons(nil(), 0())
, conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))}
Proof Output:
Computation stopped due to timeout after 60.0 secondsTool pair1rc
Execution Time | Unknown |
---|
Answer | TIMEOUT |
---|
Input | AG01 3.42 |
---|
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(x))) -> s(half(x))
, lastbit(0()) -> 0()
, lastbit(s(0())) -> s(0())
, lastbit(s(s(x))) -> lastbit(x)
, conv(0()) -> cons(nil(), 0())
, conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(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.42 |
---|
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(x))) -> s(half(x))
, lastbit(0()) -> 0()
, lastbit(s(0())) -> s(0())
, lastbit(s(s(x))) -> lastbit(x)
, conv(0()) -> cons(nil(), 0())
, conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(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 | YES(?,O(n^3)) |
---|
Input | AG01 3.42 |
---|
stdout:
YES(?,O(n^3))
We consider the following Problem:
Strict Trs:
{ half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(x))) -> s(half(x))
, lastbit(0()) -> 0()
, lastbit(s(0())) -> s(0())
, lastbit(s(s(x))) -> lastbit(x)
, conv(0()) -> cons(nil(), 0())
, conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^3))
Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
The input problem contains no overlaps that give rise to inapplicable rules.
We abort the transformation and continue with the subprocessor on the problem
Strict Trs:
{ half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(x))) -> s(half(x))
, lastbit(0()) -> 0()
, lastbit(s(0())) -> s(0())
, lastbit(s(s(x))) -> lastbit(x)
, conv(0()) -> cons(nil(), 0())
, conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))}
StartTerms: basic terms
Strategy: innermost
1) 'Fastest' proved the goal fastest:
'Sequentially' proved the goal fastest:
'Fastest' succeeded:
'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' proved the goal fastest:
The following argument positions are usable:
Uargs(half) = {}, Uargs(s) = {1}, Uargs(lastbit) = {},
Uargs(conv) = {1}, Uargs(cons) = {1, 2}
We have the following constructor-restricted (at most 3 in the main diagonals) matrix interpretation:
Interpretation Functions:
half(x1) = [1 0 0 0] x1 + [1]
[0 0 1 0] [0]
[0 0 1 0] [0]
[0 0 0 1] [0]
0() = [0]
[2]
[2]
[1]
s(x1) = [1 0 0 0] x1 + [1]
[0 0 1 2] [2]
[0 0 1 1] [0]
[0 0 0 1] [2]
lastbit(x1) = [0 0 0 1] x1 + [0]
[2 0 1 0] [1]
[1 0 0 0] [2]
[1 0 0 0] [2]
conv(x1) = [1 2 0 0] x1 + [0]
[0 0 0 0] [0]
[0 0 0 0] [0]
[0 2 0 0] [0]
cons(x1, x2) = [1 0 0 0] x1 + [1 0 0 0] x2 + [0]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
nil() = [0]
[0]
[0]
[0]
Hurray, we answered YES(?,O(n^3))Tool pair3rc
Execution Time | Unknown |
---|
Answer | TIMEOUT |
---|
Input | AG01 3.42 |
---|
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(x))) -> s(half(x))
, lastbit(0()) -> 0()
, lastbit(s(0())) -> s(0())
, lastbit(s(s(x))) -> lastbit(x)
, conv(0()) -> cons(nil(), 0())
, conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(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 | MAYBE |
---|
Input | AG01 3.42 |
---|
stdout:
MAYBE
We consider the following Problem:
Strict Trs:
{ half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(x))) -> s(half(x))
, lastbit(0()) -> 0()
, lastbit(s(0())) -> s(0())
, lastbit(s(s(x))) -> lastbit(x)
, conv(0()) -> cons(nil(), 0())
, conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))}
StartTerms: basic terms
Strategy: none
Certificate: MAYBE
Application of 'rc (timeout of 60.0 seconds)':
----------------------------------------------
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'dp' failed due to the following reason:
We have computed the following dependency pairs
Strict Dependency Pairs:
{ half^#(0()) -> c_1()
, half^#(s(0())) -> c_2()
, half^#(s(s(x))) -> c_3(half^#(x))
, lastbit^#(0()) -> c_4()
, lastbit^#(s(0())) -> c_5()
, lastbit^#(s(s(x))) -> c_6(lastbit^#(x))
, conv^#(0()) -> c_7()
, conv^#(s(x)) -> c_8(conv^#(half(s(x))), lastbit^#(s(x)))}
We consider the following Problem:
Strict DPs:
{ half^#(0()) -> c_1()
, half^#(s(0())) -> c_2()
, half^#(s(s(x))) -> c_3(half^#(x))
, lastbit^#(0()) -> c_4()
, lastbit^#(s(0())) -> c_5()
, lastbit^#(s(s(x))) -> c_6(lastbit^#(x))
, conv^#(0()) -> c_7()
, conv^#(s(x)) -> c_8(conv^#(half(s(x))), lastbit^#(s(x)))}
Strict Trs:
{ half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(x))) -> s(half(x))
, lastbit(0()) -> 0()
, lastbit(s(0())) -> s(0())
, lastbit(s(s(x))) -> lastbit(x)
, conv(0()) -> cons(nil(), 0())
, conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))}
StartTerms: basic terms
Strategy: none
Certificate: MAYBE
Application of 'usablerules':
-----------------------------
We replace strict/weak-rules by the corresponding usable rules:
Strict Usable Rules:
{ half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(x))) -> s(half(x))}
We consider the following Problem:
Strict DPs:
{ half^#(0()) -> c_1()
, half^#(s(0())) -> c_2()
, half^#(s(s(x))) -> c_3(half^#(x))
, lastbit^#(0()) -> c_4()
, lastbit^#(s(0())) -> c_5()
, lastbit^#(s(s(x))) -> c_6(lastbit^#(x))
, conv^#(0()) -> c_7()
, conv^#(s(x)) -> c_8(conv^#(half(s(x))), lastbit^#(s(x)))}
Strict Trs:
{ half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(x))) -> s(half(x))}
StartTerms: basic terms
Strategy: none
Certificate: MAYBE
Application of 'Fastest':
-------------------------
None of the processors succeeded.
2) 'Fastest' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'Sequentially' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'empty' failed due to the following reason:
Empty strict component of the problem is NOT empty.
2) 'Fastest' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
2) 'matrix-interpretation of dimension 3 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
3) 'matrix-interpretation of dimension 2 (timeout of 100.0 seconds)' failed due to the following reason:
The input cannot be shown compatible
2) 'Fastest' failed due to the following reason:
None of the processors succeeded.
Details of failed attempt(s):
-----------------------------
1) 'Bounds with perSymbol-enrichment and initial automaton 'match' (timeout of 5.0 seconds)' failed due to the following reason:
match-boundness of the problem could not be verified.
2) 'Bounds with minimal-enrichment and initial automaton 'match' (timeout of 100.0 seconds)' failed due to the following reason:
match-boundness of the problem could not be verified.
Arrrr..Tool tup3irc
Execution Time | 53.256447ms |
---|
Answer | YES(?,O(n^3)) |
---|
Input | AG01 3.42 |
---|
stdout:
YES(?,O(n^3))
We consider the following Problem:
Strict Trs:
{ half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(x))) -> s(half(x))
, lastbit(0()) -> 0()
, lastbit(s(0())) -> s(0())
, lastbit(s(s(x))) -> lastbit(x)
, conv(0()) -> cons(nil(), 0())
, conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^3))
Application of 'tup3 (timeout of 60.0 seconds)':
------------------------------------------------
The input problem contains no overlaps that give rise to inapplicable rules.
We abort the transformation and continue with the subprocessor on the problem
Strict Trs:
{ half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(x))) -> s(half(x))
, lastbit(0()) -> 0()
, lastbit(s(0())) -> s(0())
, lastbit(s(s(x))) -> lastbit(x)
, conv(0()) -> cons(nil(), 0())
, conv(s(x)) -> cons(conv(half(s(x))), lastbit(s(x)))}
StartTerms: basic terms
Strategy: innermost
1) 'Fastest' proved the goal fastest:
'Sequentially' proved the goal fastest:
'Fastest' succeeded:
'matrix-interpretation of dimension 4 (timeout of 100.0 seconds)' proved the goal fastest:
The following argument positions are usable:
Uargs(half) = {}, Uargs(s) = {1}, Uargs(lastbit) = {},
Uargs(conv) = {1}, Uargs(cons) = {1, 2}
We have the following constructor-restricted (at most 3 in the main diagonals) matrix interpretation:
Interpretation Functions:
half(x1) = [1 0 0 0] x1 + [1]
[0 0 1 0] [0]
[0 0 1 0] [0]
[0 0 0 1] [0]
0() = [0]
[2]
[2]
[1]
s(x1) = [1 0 0 0] x1 + [1]
[0 0 1 2] [2]
[0 0 1 1] [0]
[0 0 0 1] [2]
lastbit(x1) = [0 0 0 1] x1 + [0]
[2 0 1 0] [1]
[1 0 0 0] [2]
[1 0 0 0] [2]
conv(x1) = [1 2 0 0] x1 + [0]
[0 0 0 0] [0]
[0 0 0 0] [0]
[0 2 0 0] [0]
cons(x1, x2) = [1 0 0 0] x1 + [1 0 0 0] x2 + [0]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
[0 0 0 0] [0 0 0 0] [0]
nil() = [0]
[0]
[0]
[0]
Hurray, we answered YES(?,O(n^3))