Tool IRC1
stdout:
MAYBE
Tool IRC2
stdout:
TIMEOUT
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: TIMEOUT
Input Problem: innermost runtime-complexity with respect to
Rules:
{ U11(tt(), N) -> N
, U21(tt(), M, N) -> s(plus(N, M))
, U31(tt()) -> 0()
, U41(tt(), M, N) -> plus(x(N, M), N)
, and(tt(), X) -> X
, isNat(0()) -> tt()
, isNat(plus(V1, V2)) -> and(isNat(V1), isNat(V2))
, isNat(s(V1)) -> isNat(V1)
, isNat(x(V1, V2)) -> and(isNat(V1), isNat(V2))
, plus(N, 0()) -> U11(isNat(N), N)
, plus(N, s(M)) -> U21(and(isNat(M), isNat(N)), M, N)
, x(N, 0()) -> U31(isNat(N))
, x(N, s(M)) -> U41(and(isNat(M), isNat(N)), M, N)}
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:
{ U11(tt(), N) -> N
, U21(tt(), M, N) -> s(plus(N, M))
, U31(tt()) -> 0()
, U41(tt(), M, N) -> plus(x(N, M), N)
, and(tt(), X) -> X
, isNat(0()) -> tt()
, isNat(plus(V1, V2)) -> and(isNat(V1), isNat(V2))
, isNat(s(V1)) -> isNat(V1)
, isNat(x(V1, V2)) -> and(isNat(V1), isNat(V2))
, plus(N, 0()) -> U11(isNat(N), N)
, plus(N, s(M)) -> U21(and(isNat(M), isNat(N)), M, N)
, x(N, 0()) -> U31(isNat(N))
, x(N, s(M)) -> U41(and(isNat(M), isNat(N)), M, N)}
Proof Output:
Computation stopped due to timeout after 60.0 seconds