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(), V1, V2) -> U12(isNat(V1), V2)
, U12(tt(), V2) -> U13(isNat(V2))
, U13(tt()) -> tt()
, U21(tt(), V1) -> U22(isNat(V1))
, U22(tt()) -> tt()
, U31(tt(), V1, V2) -> U32(isNat(V1), V2)
, U32(tt(), V2) -> U33(isNat(V2))
, U33(tt()) -> tt()
, U41(tt(), N) -> N
, U51(tt(), M, N) -> s(plus(N, M))
, U61(tt()) -> 0()
, U71(tt(), M, N) -> plus(x(N, M), N)
, and(tt(), X) -> X
, isNat(0()) -> tt()
, isNat(plus(V1, V2)) ->
U11(and(isNatKind(V1), isNatKind(V2)), V1, V2)
, isNat(s(V1)) -> U21(isNatKind(V1), V1)
, isNat(x(V1, V2)) ->
U31(and(isNatKind(V1), isNatKind(V2)), V1, V2)
, isNatKind(0()) -> tt()
, isNatKind(plus(V1, V2)) -> and(isNatKind(V1), isNatKind(V2))
, isNatKind(s(V1)) -> isNatKind(V1)
, isNatKind(x(V1, V2)) -> and(isNatKind(V1), isNatKind(V2))
, plus(N, 0()) -> U41(and(isNat(N), isNatKind(N)), N)
, plus(N, s(M)) ->
U51(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))),
M,
N)
, x(N, 0()) -> U61(and(isNat(N), isNatKind(N)))
, x(N, s(M)) ->
U71(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(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(), V1, V2) -> U12(isNat(V1), V2)
, U12(tt(), V2) -> U13(isNat(V2))
, U13(tt()) -> tt()
, U21(tt(), V1) -> U22(isNat(V1))
, U22(tt()) -> tt()
, U31(tt(), V1, V2) -> U32(isNat(V1), V2)
, U32(tt(), V2) -> U33(isNat(V2))
, U33(tt()) -> tt()
, U41(tt(), N) -> N
, U51(tt(), M, N) -> s(plus(N, M))
, U61(tt()) -> 0()
, U71(tt(), M, N) -> plus(x(N, M), N)
, and(tt(), X) -> X
, isNat(0()) -> tt()
, isNat(plus(V1, V2)) ->
U11(and(isNatKind(V1), isNatKind(V2)), V1, V2)
, isNat(s(V1)) -> U21(isNatKind(V1), V1)
, isNat(x(V1, V2)) ->
U31(and(isNatKind(V1), isNatKind(V2)), V1, V2)
, isNatKind(0()) -> tt()
, isNatKind(plus(V1, V2)) -> and(isNatKind(V1), isNatKind(V2))
, isNatKind(s(V1)) -> isNatKind(V1)
, isNatKind(x(V1, V2)) -> and(isNatKind(V1), isNatKind(V2))
, plus(N, 0()) -> U41(and(isNat(N), isNatKind(N)), N)
, plus(N, s(M)) ->
U51(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))),
M,
N)
, x(N, 0()) -> U61(and(isNat(N), isNatKind(N)))
, x(N, s(M)) ->
U71(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))),
M,
N)}
Proof Output:
Computation stopped due to timeout after 60.0 seconds