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