MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. 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(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L))) , min(cons(0(), nil())) -> 0() , min(cons(s(N), nil())) -> s(N) , 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, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L)) , replace(N, M, nil()) -> nil() , ifrepl(true(), N, M, cons(K, L)) -> cons(M, L) , ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L)) , selsort(cons(N, L)) -> ifselsort(eq(N, min(cons(N, L))), cons(N, L)) , selsort(nil()) -> nil() , 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))) } Obligation: innermost runtime complexity Answer: MAYBE The input cannot be shown compatible Arrrr..