Tool CaT
stdout:
MAYBE
Problem:
div(x,s(y)) -> d(x,s(y),0())
d(x,s(y),z) -> cond(ge(x,z),x,y,z)
cond(true(),x,y,z) -> s(d(x,s(y),plus(s(y),z)))
cond(false(),x,y,z) -> 0()
ge(u,0()) -> true()
ge(0(),s(v)) -> false()
ge(s(u),s(v)) -> ge(u,v)
plus(n,0()) -> n
plus(n,s(m)) -> s(plus(n,m))
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:
{ div(x, s(y)) -> d(x, s(y), 0())
, d(x, s(y), z) -> cond(ge(x, z), x, y, z)
, cond(true(), x, y, z) -> s(d(x, s(y), plus(s(y), z)))
, cond(false(), x, y, z) -> 0()
, ge(u, 0()) -> true()
, ge(0(), s(v)) -> false()
, ge(s(u), s(v)) -> ge(u, v)
, plus(n, 0()) -> n
, plus(n, s(m)) -> s(plus(n, m))}
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:
{ div(x, s(y)) -> d(x, s(y), 0())
, d(x, s(y), z) -> cond(ge(x, z), x, y, z)
, cond(true(), x, y, z) -> s(d(x, s(y), plus(s(y), z)))
, cond(false(), x, y, z) -> 0()
, ge(u, 0()) -> true()
, ge(0(), s(v)) -> false()
, ge(s(u), s(v)) -> ge(u, v)
, plus(n, 0()) -> n
, plus(n, s(m)) -> s(plus(n, m))}
Proof Output:
Computation stopped due to timeout after 60.0 seconds