Problem Rubio 04 selsort

Tool CaT

Execution TimeUnknown
Answer
MAYBE
InputRubio 04 selsort

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:
 Open

Tool IRC1

Execution TimeUnknown
Answer
MAYBE
InputRubio 04 selsort

stdout:

MAYBE

Tool IRC2

Execution TimeUnknown
Answer
TIMEOUT
InputRubio 04 selsort

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 seconds

Tool RC1

Execution TimeUnknown
Answer
MAYBE
InputRubio 04 selsort

stdout:

MAYBE

Tool RC2

Execution TimeUnknown
Answer
TIMEOUT
InputRubio 04 selsort

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