LMPO

Execution Time (secs)	0.183
Answer	MAYBE
Input	Rubio 04 selsort

MAYBE

We consider the following Problem:

  Strict Trs:
    {  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)))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MPO

Execution Time (secs)	0.178
Answer	MAYBE
Input	Rubio 04 selsort

MAYBE

We consider the following Problem:

  Strict Trs:
    {  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)))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

POP*

Execution Time (secs)	0.251
Answer	MAYBE
Input	Rubio 04 selsort

MAYBE

We consider the following Problem:

  Strict Trs:
    {  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)))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

POP* (PS)

Execution Time (secs)	0.143
Answer	MAYBE
Input	Rubio 04 selsort

MAYBE

We consider the following Problem:

  Strict Trs:
    {  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)))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

Small POP*

Execution Time (secs)	0.154
Answer	MAYBE
Input	Rubio 04 selsort

MAYBE

We consider the following Problem:

  Strict Trs:
    {  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)))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

Small POP* (PS)

Execution Time (secs)	0.146
Answer	MAYBE
Input	Rubio 04 selsort

MAYBE

We consider the following Problem:

  Strict Trs:
    {  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)))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

Problem Rubio 04 selsort

LMPO

MPO

POP*

POP* (PS)

Small POP*

Small POP* (PS)