Tool CaT
stdout:
MAYBE
Problem:
minus(x,x) -> 0()
minus(x,y) -> cond(equal(min(x,y),y),x,y)
cond(true(),x,y) -> s(minus(x,s(y)))
min(0(),v) -> 0()
min(u,0()) -> 0()
min(s(u),s(v)) -> s(min(u,v))
equal(0(),0()) -> true()
equal(s(x),0()) -> false()
equal(0(),s(y)) -> false()
equal(s(x),s(y)) -> equal(x,y)
Proof:
OpenTool IRC1
stdout:
MAYBE
Tool IRC2
stdout:
TIMEOUT
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: TIMEOUT
Input Problem: innermost runtime-complexity with respect to
Rules:
{ minus(x, x) -> 0()
, minus(x, y) -> cond(equal(min(x, y), y), x, y)
, cond(true(), x, y) -> s(minus(x, s(y)))
, min(0(), v) -> 0()
, min(u, 0()) -> 0()
, min(s(u), s(v)) -> s(min(u, v))
, equal(0(), 0()) -> true()
, equal(s(x), 0()) -> false()
, equal(0(), s(y)) -> false()
, equal(s(x), s(y)) -> equal(x, y)}
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:
{ minus(x, x) -> 0()
, minus(x, y) -> cond(equal(min(x, y), y), x, y)
, cond(true(), x, y) -> s(minus(x, s(y)))
, min(0(), v) -> 0()
, min(u, 0()) -> 0()
, min(s(u), s(v)) -> s(min(u, v))
, equal(0(), 0()) -> true()
, equal(s(x), 0()) -> false()
, equal(0(), s(y)) -> false()
, equal(s(x), s(y)) -> equal(x, y)}
Proof Output:
Computation stopped due to timeout after 60.0 seconds