Tool CaT
stdout:
MAYBE
Problem:
eq(0(),0()) -> true()
eq(0(),s(Y)) -> false()
eq(s(X),0()) -> false()
eq(s(X),s(Y)) -> eq(X,Y)
le(0(),Y) -> true()
le(s(X),0()) -> false()
le(s(X),s(Y)) -> le(X,Y)
min(cons(0(),nil())) -> 0()
min(cons(s(N),nil())) -> s(N)
min(cons(N,cons(M,L))) -> ifmin(le(N,M),cons(N,cons(M,L)))
ifmin(true(),cons(N,cons(M,L))) -> min(cons(N,L))
ifmin(false(),cons(N,cons(M,L))) -> min(cons(M,L))
replace(N,M,nil()) -> nil()
replace(N,M,cons(K,L)) -> ifrepl(eq(N,K),N,M,cons(K,L))
ifrepl(true(),N,M,cons(K,L)) -> cons(M,L)
ifrepl(false(),N,M,cons(K,L)) -> cons(K,replace(N,M,L))
selsort(nil()) -> nil()
selsort(cons(N,L)) -> ifselsort(eq(N,min(cons(N,L))),cons(N,L))
ifselsort(true(),cons(N,L)) -> cons(N,selsort(L))
ifselsort(false(),cons(N,L)) -> cons(min(cons(N,L)),selsort(replace(min(cons(N,L)),N,L)))
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:
{ eq(0(), 0()) -> true()
, eq(0(), s(Y)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, le(0(), Y) -> true()
, le(s(X), 0()) -> false()
, le(s(X), s(Y)) -> le(X, Y)
, min(cons(0(), nil())) -> 0()
, min(cons(s(N), nil())) -> s(N)
, min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L)))
, ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L))
, ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L))
, replace(N, M, nil()) -> nil()
, replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L))
, ifrepl(true(), N, M, cons(K, L)) -> cons(M, L)
, ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L))
, selsort(nil()) -> nil()
, selsort(cons(N, L)) ->
ifselsort(eq(N, min(cons(N, L))), cons(N, L))
, ifselsort(true(), cons(N, L)) -> cons(N, selsort(L))
, ifselsort(false(), cons(N, L)) ->
cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L)))}
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:
{ eq(0(), 0()) -> true()
, eq(0(), s(Y)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, le(0(), Y) -> true()
, le(s(X), 0()) -> false()
, le(s(X), s(Y)) -> le(X, Y)
, min(cons(0(), nil())) -> 0()
, min(cons(s(N), nil())) -> s(N)
, min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L)))
, ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L))
, ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L))
, replace(N, M, nil()) -> nil()
, replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L))
, ifrepl(true(), N, M, cons(K, L)) -> cons(M, L)
, ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L))
, selsort(nil()) -> nil()
, selsort(cons(N, L)) ->
ifselsort(eq(N, min(cons(N, L))), cons(N, L))
, ifselsort(true(), cons(N, L)) -> cons(N, selsort(L))
, ifselsort(false(), cons(N, L)) ->
cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L)))}
Proof Output:
Computation stopped due to timeout after 60.0 seconds