MAYBE
MAYBE
TRS:
 {
            U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))),
                 activate(X) -> X,
    activate(n__natsFrom(X)) -> natsFrom(activate(X)),
           activate(n__s(X)) -> s(activate(X)),
            U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS)),
             snd(pair(X, Y)) -> U51(tt(), Y),
            splitAt(0(), XS) -> pair(nil(), XS),
  splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(XS)),
                U22(tt(), X) -> activate(X),
                U21(tt(), X) -> U22(tt(), activate(X)),
                U32(tt(), N) -> activate(N),
                U31(tt(), N) -> U32(tt(), activate(N)),
            U42(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))),
            U41(tt(), N, XS) -> U42(tt(), activate(N), activate(XS)),
           head(cons(N, XS)) -> U31(tt(), N),
             afterNth(N, XS) -> U11(tt(), N, XS),
                U52(tt(), Y) -> activate(Y),
                U51(tt(), Y) -> U52(tt(), activate(Y)),
         U62(tt(), N, X, XS) ->
  U63(tt(), activate(N), activate(X), activate(XS)),
         U61(tt(), N, X, XS) ->
  U62(tt(), activate(N), activate(X), activate(XS)),
         U63(tt(), N, X, XS) ->
  U64(splitAt(activate(N), activate(XS)), activate(X)),
        U64(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS),
               U72(tt(), XS) -> activate(XS),
               U71(tt(), XS) -> U72(tt(), activate(XS)),
            U82(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))),
            U81(tt(), N, XS) -> U82(tt(), activate(N), activate(XS)),
             fst(pair(X, Y)) -> U21(tt(), X),
                 natsFrom(N) -> cons(N, n__natsFrom(n__s(N))),
                 natsFrom(X) -> n__natsFrom(X),
                  sel(N, XS) -> U41(tt(), N, XS),
                        s(X) -> n__s(X),
           tail(cons(N, XS)) -> U71(tt(), activate(XS)),
                 take(N, XS) -> U81(tt(), N, XS)
 }
 DUP: We consider a duplicating system.
  Trs:
   {
              U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))),
                   activate(X) -> X,
      activate(n__natsFrom(X)) -> natsFrom(activate(X)),
             activate(n__s(X)) -> s(activate(X)),
              U11(tt(), N, XS) -> U12(tt(), activate(N), activate(XS)),
               snd(pair(X, Y)) -> U51(tt(), Y),
              splitAt(0(), XS) -> pair(nil(), XS),
    splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, activate(XS)),
                  U22(tt(), X) -> activate(X),
                  U21(tt(), X) -> U22(tt(), activate(X)),
                  U32(tt(), N) -> activate(N),
                  U31(tt(), N) -> U32(tt(), activate(N)),
              U42(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))),
              U41(tt(), N, XS) -> U42(tt(), activate(N), activate(XS)),
             head(cons(N, XS)) -> U31(tt(), N),
               afterNth(N, XS) -> U11(tt(), N, XS),
                  U52(tt(), Y) -> activate(Y),
                  U51(tt(), Y) -> U52(tt(), activate(Y)),
           U62(tt(), N, X, XS) ->
    U63(tt(), activate(N), activate(X), activate(XS)),
           U61(tt(), N, X, XS) ->
    U62(tt(), activate(N), activate(X), activate(XS)),
           U63(tt(), N, X, XS) ->
    U64(splitAt(activate(N), activate(XS)), activate(X)),
          U64(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS),
                 U72(tt(), XS) -> activate(XS),
                 U71(tt(), XS) -> U72(tt(), activate(XS)),
              U82(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))),
              U81(tt(), N, XS) -> U82(tt(), activate(N), activate(XS)),
               fst(pair(X, Y)) -> U21(tt(), X),
                   natsFrom(N) -> cons(N, n__natsFrom(n__s(N))),
                   natsFrom(X) -> n__natsFrom(X),
                    sel(N, XS) -> U41(tt(), N, XS),
                          s(X) -> n__s(X),
             tail(cons(N, XS)) -> U71(tt(), activate(XS)),
                   take(N, XS) -> U81(tt(), N, XS)
   }
  Fail