Tool CaT
Execution Time | Unknown |
---|
Answer | MAYBE |
---|
Input | AG01 3.5b |
---|
stdout:
MAYBE
Problem:
le(0(),y) -> true()
le(s(x),0()) -> false()
le(s(x),s(y)) -> le(x,y)
minus(0(),y) -> 0()
minus(s(x),y) -> if_minus(le(s(x),y),s(x),y)
if_minus(true(),s(x),y) -> 0()
if_minus(false(),s(x),y) -> s(minus(x,y))
mod(0(),y) -> 0()
mod(s(x),0()) -> 0()
mod(s(x),s(y)) -> if_mod(le(y,x),s(x),s(y))
if_mod(true(),s(x),s(y)) -> mod(minus(x,y),s(y))
if_mod(false(),s(x),s(y)) -> s(x)
Proof:
OpenTool IRC1
Execution Time | Unknown |
---|
Answer | MAYBE |
---|
Input | AG01 3.5b |
---|
stdout:
MAYBE
Tool IRC2
Execution Time | Unknown |
---|
Answer | TIMEOUT |
---|
Input | AG01 3.5b |
---|
stdout:
TIMEOUT
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: TIMEOUT
Input Problem: innermost runtime-complexity with respect to
Rules:
{ le(0(), y) -> true()
, le(s(x), 0()) -> false()
, le(s(x), s(y)) -> le(x, y)
, minus(0(), y) -> 0()
, minus(s(x), y) -> if_minus(le(s(x), y), s(x), y)
, if_minus(true(), s(x), y) -> 0()
, if_minus(false(), s(x), y) -> s(minus(x, y))
, mod(0(), y) -> 0()
, mod(s(x), 0()) -> 0()
, mod(s(x), s(y)) -> if_mod(le(y, x), s(x), s(y))
, if_mod(true(), s(x), s(y)) -> mod(minus(x, y), s(y))
, if_mod(false(), s(x), s(y)) -> s(x)}
Proof Output:
Computation stopped due to timeout after 60.0 secondsTool RC1
Execution Time | Unknown |
---|
Answer | MAYBE |
---|
Input | AG01 3.5b |
---|
stdout:
MAYBE
Tool RC2
Execution Time | Unknown |
---|
Answer | TIMEOUT |
---|
Input | AG01 3.5b |
---|
stdout:
TIMEOUT
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: TIMEOUT
Input Problem: runtime-complexity with respect to
Rules:
{ le(0(), y) -> true()
, le(s(x), 0()) -> false()
, le(s(x), s(y)) -> le(x, y)
, minus(0(), y) -> 0()
, minus(s(x), y) -> if_minus(le(s(x), y), s(x), y)
, if_minus(true(), s(x), y) -> 0()
, if_minus(false(), s(x), y) -> s(minus(x, y))
, mod(0(), y) -> 0()
, mod(s(x), 0()) -> 0()
, mod(s(x), s(y)) -> if_mod(le(y, x), s(x), s(y))
, if_mod(true(), s(x), s(y)) -> mod(minus(x, y), s(y))
, if_mod(false(), s(x), s(y)) -> s(x)}
Proof Output:
Computation stopped due to timeout after 60.0 secondsTool pair1rc
Execution Time | Unknown |
---|
Answer | TIMEOUT |
---|
Input | AG01 3.5b |
---|
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ le(0(), y) -> true()
, le(s(x), 0()) -> false()
, le(s(x), s(y)) -> le(x, y)
, minus(0(), y) -> 0()
, minus(s(x), y) -> if_minus(le(s(x), y), s(x), y)
, if_minus(true(), s(x), y) -> 0()
, if_minus(false(), s(x), y) -> s(minus(x, y))
, mod(0(), y) -> 0()
, mod(s(x), 0()) -> 0()
, mod(s(x), s(y)) -> if_mod(le(y, x), s(x), s(y))
, if_mod(true(), s(x), s(y)) -> mod(minus(x, y), s(y))
, if_mod(false(), s(x), s(y)) -> 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.5b |
---|
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ le(0(), y) -> true()
, le(s(x), 0()) -> false()
, le(s(x), s(y)) -> le(x, y)
, minus(0(), y) -> 0()
, minus(s(x), y) -> if_minus(le(s(x), y), s(x), y)
, if_minus(true(), s(x), y) -> 0()
, if_minus(false(), s(x), y) -> s(minus(x, y))
, mod(0(), y) -> 0()
, mod(s(x), 0()) -> 0()
, mod(s(x), s(y)) -> if_mod(le(y, x), s(x), s(y))
, if_mod(true(), s(x), s(y)) -> mod(minus(x, y), s(y))
, if_mod(false(), s(x), s(y)) -> 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 | TIMEOUT |
---|
Input | AG01 3.5b |
---|
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ le(0(), y) -> true()
, le(s(x), 0()) -> false()
, le(s(x), s(y)) -> le(x, y)
, minus(0(), y) -> 0()
, minus(s(x), y) -> if_minus(le(s(x), y), s(x), y)
, if_minus(true(), s(x), y) -> 0()
, if_minus(false(), s(x), y) -> s(minus(x, y))
, mod(0(), y) -> 0()
, mod(s(x), 0()) -> 0()
, mod(s(x), s(y)) -> if_mod(le(y, x), s(x), s(y))
, if_mod(true(), s(x), s(y)) -> mod(minus(x, y), s(y))
, if_mod(false(), s(x), s(y)) -> s(x)}
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.5b |
---|
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ le(0(), y) -> true()
, le(s(x), 0()) -> false()
, le(s(x), s(y)) -> le(x, y)
, minus(0(), y) -> 0()
, minus(s(x), y) -> if_minus(le(s(x), y), s(x), y)
, if_minus(true(), s(x), y) -> 0()
, if_minus(false(), s(x), y) -> s(minus(x, y))
, mod(0(), y) -> 0()
, mod(s(x), 0()) -> 0()
, mod(s(x), s(y)) -> if_mod(le(y, x), s(x), s(y))
, if_mod(true(), s(x), s(y)) -> mod(minus(x, y), s(y))
, if_mod(false(), s(x), s(y)) -> 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.5b |
---|
stdout:
MAYBE
We consider the following Problem:
Strict Trs:
{ le(0(), y) -> true()
, le(s(x), 0()) -> false()
, le(s(x), s(y)) -> le(x, y)
, minus(0(), y) -> 0()
, minus(s(x), y) -> if_minus(le(s(x), y), s(x), y)
, if_minus(true(), s(x), y) -> 0()
, if_minus(false(), s(x), y) -> s(minus(x, y))
, mod(0(), y) -> 0()
, mod(s(x), 0()) -> 0()
, mod(s(x), s(y)) -> if_mod(le(y, x), s(x), s(y))
, if_mod(true(), s(x), s(y)) -> mod(minus(x, y), s(y))
, if_mod(false(), s(x), s(y)) -> 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:
{ le^#(0(), y) -> c_1()
, le^#(s(x), 0()) -> c_2()
, le^#(s(x), s(y)) -> c_3(le^#(x, y))
, minus^#(0(), y) -> c_4()
, minus^#(s(x), y) -> c_5(if_minus^#(le(s(x), y), s(x), y))
, if_minus^#(true(), s(x), y) -> c_6()
, if_minus^#(false(), s(x), y) -> c_7(minus^#(x, y))
, mod^#(0(), y) -> c_8()
, mod^#(s(x), 0()) -> c_9()
, mod^#(s(x), s(y)) -> c_10(if_mod^#(le(y, x), s(x), s(y)))
, if_mod^#(true(), s(x), s(y)) -> c_11(mod^#(minus(x, y), s(y)))
, if_mod^#(false(), s(x), s(y)) -> c_12(x)}
We consider the following Problem:
Strict DPs:
{ le^#(0(), y) -> c_1()
, le^#(s(x), 0()) -> c_2()
, le^#(s(x), s(y)) -> c_3(le^#(x, y))
, minus^#(0(), y) -> c_4()
, minus^#(s(x), y) -> c_5(if_minus^#(le(s(x), y), s(x), y))
, if_minus^#(true(), s(x), y) -> c_6()
, if_minus^#(false(), s(x), y) -> c_7(minus^#(x, y))
, mod^#(0(), y) -> c_8()
, mod^#(s(x), 0()) -> c_9()
, mod^#(s(x), s(y)) -> c_10(if_mod^#(le(y, x), s(x), s(y)))
, if_mod^#(true(), s(x), s(y)) -> c_11(mod^#(minus(x, y), s(y)))
, if_mod^#(false(), s(x), s(y)) -> c_12(x)}
Strict Trs:
{ le(0(), y) -> true()
, le(s(x), 0()) -> false()
, le(s(x), s(y)) -> le(x, y)
, minus(0(), y) -> 0()
, minus(s(x), y) -> if_minus(le(s(x), y), s(x), y)
, if_minus(true(), s(x), y) -> 0()
, if_minus(false(), s(x), y) -> s(minus(x, y))
, mod(0(), y) -> 0()
, mod(s(x), 0()) -> 0()
, mod(s(x), s(y)) -> if_mod(le(y, x), s(x), s(y))
, if_mod(true(), s(x), s(y)) -> mod(minus(x, y), s(y))
, if_mod(false(), s(x), s(y)) -> 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:
{ le(0(), y) -> true()
, le(s(x), 0()) -> false()
, le(s(x), s(y)) -> le(x, y)
, minus(0(), y) -> 0()
, minus(s(x), y) -> if_minus(le(s(x), y), s(x), y)
, if_minus(true(), s(x), y) -> 0()
, if_minus(false(), s(x), y) -> s(minus(x, y))}
We consider the following Problem:
Strict DPs:
{ le^#(0(), y) -> c_1()
, le^#(s(x), 0()) -> c_2()
, le^#(s(x), s(y)) -> c_3(le^#(x, y))
, minus^#(0(), y) -> c_4()
, minus^#(s(x), y) -> c_5(if_minus^#(le(s(x), y), s(x), y))
, if_minus^#(true(), s(x), y) -> c_6()
, if_minus^#(false(), s(x), y) -> c_7(minus^#(x, y))
, mod^#(0(), y) -> c_8()
, mod^#(s(x), 0()) -> c_9()
, mod^#(s(x), s(y)) -> c_10(if_mod^#(le(y, x), s(x), s(y)))
, if_mod^#(true(), s(x), s(y)) -> c_11(mod^#(minus(x, y), s(y)))
, if_mod^#(false(), s(x), s(y)) -> c_12(x)}
Strict Trs:
{ le(0(), y) -> true()
, le(s(x), 0()) -> false()
, le(s(x), s(y)) -> le(x, y)
, minus(0(), y) -> 0()
, minus(s(x), y) -> if_minus(le(s(x), y), s(x), y)
, if_minus(true(), s(x), y) -> 0()
, if_minus(false(), s(x), y) -> s(minus(x, y))}
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 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.
2) '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.
Arrrr..Tool tup3irc
Execution Time | 60.066612ms |
---|
Answer | TIMEOUT |
---|
Input | AG01 3.5b |
---|
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ le(0(), y) -> true()
, le(s(x), 0()) -> false()
, le(s(x), s(y)) -> le(x, y)
, minus(0(), y) -> 0()
, minus(s(x), y) -> if_minus(le(s(x), y), s(x), y)
, if_minus(true(), s(x), y) -> 0()
, if_minus(false(), s(x), y) -> s(minus(x, y))
, mod(0(), y) -> 0()
, mod(s(x), 0()) -> 0()
, mod(s(x), s(y)) -> if_mod(le(y, x), s(x), s(y))
, if_mod(true(), s(x), s(y)) -> mod(minus(x, y), s(y))
, if_mod(false(), s(x), s(y)) -> s(x)}
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..