The TRS could be proven non-terminating. The proof took 0 ms.
The rule sel(s(X), cons(Y)) -> sel(X, Z) contains extra variables, thus the system is non-terminating.