Tool CaT
stdout:
MAYBE
Problem:
+(x,0()) -> x
+(x,s(y)) -> s(+(x,y))
*(x,0()) -> 0()
*(x,s(y)) -> +(*(x,y),x)
ge(x,0()) -> true()
ge(0(),s(y)) -> false()
ge(s(x),s(y)) -> ge(x,y)
-(x,0()) -> x
-(s(x),s(y)) -> -(x,y)
fact(x) -> iffact(x,ge(x,s(s(0()))))
iffact(x,true()) -> *(x,fact(-(x,s(0()))))
iffact(x,false()) -> s(0())
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:
{ +(x, 0()) -> x
, +(x, s(y)) -> s(+(x, y))
, *(x, 0()) -> 0()
, *(x, s(y)) -> +(*(x, y), x)
, ge(x, 0()) -> true()
, ge(0(), s(y)) -> false()
, ge(s(x), s(y)) -> ge(x, y)
, -(x, 0()) -> x
, -(s(x), s(y)) -> -(x, y)
, fact(x) -> iffact(x, ge(x, s(s(0()))))
, iffact(x, true()) -> *(x, fact(-(x, s(0()))))
, iffact(x, false()) -> s(0())}
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:
{ +(x, 0()) -> x
, +(x, s(y)) -> s(+(x, y))
, *(x, 0()) -> 0()
, *(x, s(y)) -> +(*(x, y), x)
, ge(x, 0()) -> true()
, ge(0(), s(y)) -> false()
, ge(s(x), s(y)) -> ge(x, y)
, -(x, 0()) -> x
, -(s(x), s(y)) -> -(x, y)
, fact(x) -> iffact(x, ge(x, s(s(0()))))
, iffact(x, true()) -> *(x, fact(-(x, s(0()))))
, iffact(x, false()) -> s(0())}
Proof Output:
Computation stopped due to timeout after 60.0 seconds