MAYBE
Trs:
 {      U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS),
                and(tt(), X) -> activate(X),
                  sel(N, XS) -> head(afterNth(N, XS)),
             afterNth(N, XS) -> snd(splitAt(N, XS)),
           head(cons(N, XS)) -> N,
             snd(pair(X, Y)) -> Y,
         U11(tt(), N, X, XS) -> U12(splitAt(activate(N), activate(XS)), activate(X)),
           tail(cons(N, XS)) -> activate(XS),
                 take(N, XS) -> fst(splitAt(N, XS)),
            splitAt(0(), XS) -> pair(nil(), XS),
  splitAt(s(N), cons(X, XS)) -> U11(tt(), N, X, activate(XS)),
             fst(pair(X, Y)) -> X,
                 natsFrom(N) -> cons(N, n__natsFrom(s(N))),
                 natsFrom(X) -> n__natsFrom(X),
    activate(n__natsFrom(X)) -> natsFrom(X),
                 activate(X) -> X}
 Comment:
  We consider a duplicating trs.
  FAIL:
   Open