The TRS could be proven non-terminating. The proof took 0 ms.

The rule 2nd(cons(X)) -> 2nd(cons1(X, X1)) contains extra variables, thus the system is non-terminating.