Tool CaT
Execution Time | Unknown |
---|
Answer | MAYBE |
---|
Input | AG01 3.40 |
---|
stdout:
MAYBE
Problem:
minus(x,0()) -> x
minus(s(x),s(y)) -> minus(x,y)
quot(0(),s(y)) -> 0()
quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
plus(0(),y) -> y
plus(s(x),y) -> s(plus(x,y))
plus(minus(x,s(0())),minus(y,s(s(z)))) -> plus(minus(y,s(s(z))),minus(x,s(0())))
plus(plus(x,s(0())),plus(y,s(s(z)))) -> plus(plus(y,s(s(z))),plus(x,s(0())))
Proof:
OpenTool IRC1
Execution Time | Unknown |
---|
Answer | MAYBE |
---|
Input | AG01 3.40 |
---|
stdout:
MAYBE
Tool IRC2
Execution Time | Unknown |
---|
Answer | TIMEOUT |
---|
Input | AG01 3.40 |
---|
stdout:
TIMEOUT
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: TIMEOUT
Input Problem: innermost runtime-complexity with respect to
Rules:
{ minus(x, 0()) -> x
, minus(s(x), s(y)) -> minus(x, y)
, quot(0(), s(y)) -> 0()
, quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
, plus(0(), y) -> y
, plus(s(x), y) -> s(plus(x, y))
, plus(minus(x, s(0())), minus(y, s(s(z)))) ->
plus(minus(y, s(s(z))), minus(x, s(0())))
, plus(plus(x, s(0())), plus(y, s(s(z)))) ->
plus(plus(y, s(s(z))), plus(x, s(0())))}
Proof Output:
Computation stopped due to timeout after 60.0 secondsTool RC1
Execution Time | Unknown |
---|
Answer | MAYBE |
---|
Input | AG01 3.40 |
---|
stdout:
MAYBE
Tool RC2
Execution Time | Unknown |
---|
Answer | TIMEOUT |
---|
Input | AG01 3.40 |
---|
stdout:
TIMEOUT
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: TIMEOUT
Input Problem: runtime-complexity with respect to
Rules:
{ minus(x, 0()) -> x
, minus(s(x), s(y)) -> minus(x, y)
, quot(0(), s(y)) -> 0()
, quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
, plus(0(), y) -> y
, plus(s(x), y) -> s(plus(x, y))
, plus(minus(x, s(0())), minus(y, s(s(z)))) ->
plus(minus(y, s(s(z))), minus(x, s(0())))
, plus(plus(x, s(0())), plus(y, s(s(z)))) ->
plus(plus(y, s(s(z))), plus(x, s(0())))}
Proof Output:
Computation stopped due to timeout after 60.0 secondsTool pair1rc
Execution Time | Unknown |
---|
Answer | TIMEOUT |
---|
Input | AG01 3.40 |
---|
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ minus(x, 0()) -> x
, minus(s(x), s(y)) -> minus(x, y)
, quot(0(), s(y)) -> 0()
, quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
, plus(0(), y) -> y
, plus(s(x), y) -> s(plus(x, y))
, plus(minus(x, s(0())), minus(y, s(s(z)))) ->
plus(minus(y, s(s(z))), minus(x, s(0())))
, plus(plus(x, s(0())), plus(y, s(s(z)))) ->
plus(plus(y, s(s(z))), plus(x, s(0())))}
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.40 |
---|
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ minus(x, 0()) -> x
, minus(s(x), s(y)) -> minus(x, y)
, quot(0(), s(y)) -> 0()
, quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
, plus(0(), y) -> y
, plus(s(x), y) -> s(plus(x, y))
, plus(minus(x, s(0())), minus(y, s(s(z)))) ->
plus(minus(y, s(s(z))), minus(x, s(0())))
, plus(plus(x, s(0())), plus(y, s(s(z)))) ->
plus(plus(y, s(s(z))), plus(x, s(0())))}
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.40 |
---|
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ minus(x, 0()) -> x
, minus(s(x), s(y)) -> minus(x, y)
, quot(0(), s(y)) -> 0()
, quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
, plus(0(), y) -> y
, plus(s(x), y) -> s(plus(x, y))
, plus(minus(x, s(0())), minus(y, s(s(z)))) ->
plus(minus(y, s(s(z))), minus(x, s(0())))
, plus(plus(x, s(0())), plus(y, s(s(z)))) ->
plus(plus(y, s(s(z))), plus(x, s(0())))}
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.40 |
---|
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ minus(x, 0()) -> x
, minus(s(x), s(y)) -> minus(x, y)
, quot(0(), s(y)) -> 0()
, quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
, plus(0(), y) -> y
, plus(s(x), y) -> s(plus(x, y))
, plus(minus(x, s(0())), minus(y, s(s(z)))) ->
plus(minus(y, s(s(z))), minus(x, s(0())))
, plus(plus(x, s(0())), plus(y, s(s(z)))) ->
plus(plus(y, s(s(z))), plus(x, s(0())))}
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.40 |
---|
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ minus(x, 0()) -> x
, minus(s(x), s(y)) -> minus(x, y)
, quot(0(), s(y)) -> 0()
, quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
, plus(0(), y) -> y
, plus(s(x), y) -> s(plus(x, y))
, plus(minus(x, s(0())), minus(y, s(s(z)))) ->
plus(minus(y, s(s(z))), minus(x, s(0())))
, plus(plus(x, s(0())), plus(y, s(s(z)))) ->
plus(plus(y, s(s(z))), plus(x, s(0())))}
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.06112ms |
---|
Answer | TIMEOUT |
---|
Input | AG01 3.40 |
---|
stdout:
TIMEOUT
We consider the following Problem:
Strict Trs:
{ minus(x, 0()) -> x
, minus(s(x), s(y)) -> minus(x, y)
, quot(0(), s(y)) -> 0()
, quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
, plus(0(), y) -> y
, plus(s(x), y) -> s(plus(x, y))
, plus(minus(x, s(0())), minus(y, s(s(z)))) ->
plus(minus(y, s(s(z))), minus(x, s(0())))
, plus(plus(x, s(0())), plus(y, s(s(z)))) ->
plus(plus(y, s(s(z))), plus(x, s(0())))}
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..