MAYBE
MAYBE
TRS:
 {
                   mark(U12(X1, X2)) -> active(U12(mark(X1), X2)),
               mark(splitAt(X1, X2)) -> active(splitAt(mark(X1), mark(X2))),
           mark(U11(X1, X2, X3, X4)) -> active(U11(mark(X1), X2, X3, X4)),
                          mark(tt()) -> active(tt()),
                  mark(pair(X1, X2)) -> active(pair(mark(X1), mark(X2))),
                  mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                        mark(snd(X)) -> active(snd(mark(X))),
              mark(afterNth(X1, X2)) -> active(afterNth(mark(X1), mark(X2))),
                   mark(and(X1, X2)) -> active(and(mark(X1), X2)),
                        mark(fst(X)) -> active(fst(mark(X))),
                       mark(head(X)) -> active(head(mark(X))),
                   mark(natsFrom(X)) -> active(natsFrom(mark(X))),
                          mark(s(X)) -> active(s(mark(X))),
                   mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))),
                         mark(nil()) -> active(nil()),
                           mark(0()) -> active(0()),
                       mark(tail(X)) -> active(tail(mark(X))),
                  mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))),
                   U12(X1, mark(X2)) -> U12(X1, X2),
                 U12(X1, active(X2)) -> U12(X1, X2),
                   U12(mark(X1), X2) -> U12(X1, X2),
                 U12(active(X1), X2) -> U12(X1, X2),
               splitAt(X1, mark(X2)) -> splitAt(X1, X2),
             splitAt(X1, active(X2)) -> splitAt(X1, X2),
               splitAt(mark(X1), X2) -> splitAt(X1, X2),
             splitAt(active(X1), X2) -> splitAt(X1, X2),
        active(U12(pair(YS, ZS), X)) -> mark(pair(cons(X, YS), ZS)),
  active(splitAt(s(N), cons(X, XS))) -> mark(U11(tt(), N, X, XS)),
            active(splitAt(0(), XS)) -> mark(pair(nil(), XS)),
         active(U11(tt(), N, X, XS)) -> mark(U12(splitAt(N, XS), X)),
             active(snd(pair(X, Y))) -> mark(Y),
             active(afterNth(N, XS)) -> mark(snd(splitAt(N, XS))),
                active(and(tt(), X)) -> mark(X),
             active(fst(pair(X, Y))) -> mark(X),
           active(head(cons(N, XS))) -> mark(N),
                 active(natsFrom(N)) -> mark(cons(N, natsFrom(s(N)))),
                  active(sel(N, XS)) -> mark(head(afterNth(N, XS))),
           active(tail(cons(N, XS))) -> mark(XS),
                 active(take(N, XS)) -> mark(fst(splitAt(N, XS))),
           U11(X1, X2, X3, mark(X4)) -> U11(X1, X2, X3, X4),
         U11(X1, X2, X3, active(X4)) -> U11(X1, X2, X3, X4),
           U11(X1, X2, mark(X3), X4) -> U11(X1, X2, X3, X4),
         U11(X1, X2, active(X3), X4) -> U11(X1, X2, X3, X4),
           U11(X1, mark(X2), X3, X4) -> U11(X1, X2, X3, X4),
         U11(X1, active(X2), X3, X4) -> U11(X1, X2, X3, X4),
           U11(mark(X1), X2, X3, X4) -> U11(X1, X2, X3, X4),
         U11(active(X1), X2, X3, X4) -> U11(X1, X2, X3, X4),
                  pair(X1, mark(X2)) -> pair(X1, X2),
                pair(X1, active(X2)) -> pair(X1, X2),
                  pair(mark(X1), X2) -> pair(X1, X2),
                pair(active(X1), X2) -> pair(X1, X2),
                  cons(X1, mark(X2)) -> cons(X1, X2),
                cons(X1, active(X2)) -> cons(X1, X2),
                  cons(mark(X1), X2) -> cons(X1, X2),
                cons(active(X1), X2) -> cons(X1, X2),
                        snd(mark(X)) -> snd(X),
                      snd(active(X)) -> snd(X),
              afterNth(X1, mark(X2)) -> afterNth(X1, X2),
            afterNth(X1, active(X2)) -> afterNth(X1, X2),
              afterNth(mark(X1), X2) -> afterNth(X1, X2),
            afterNth(active(X1), X2) -> afterNth(X1, X2),
                   and(X1, mark(X2)) -> and(X1, X2),
                 and(X1, active(X2)) -> and(X1, X2),
                   and(mark(X1), X2) -> and(X1, X2),
                 and(active(X1), X2) -> and(X1, X2),
                        fst(mark(X)) -> fst(X),
                      fst(active(X)) -> fst(X),
                       head(mark(X)) -> head(X),
                     head(active(X)) -> head(X),
                   natsFrom(mark(X)) -> natsFrom(X),
                 natsFrom(active(X)) -> natsFrom(X),
                          s(mark(X)) -> s(X),
                        s(active(X)) -> s(X),
                   sel(X1, mark(X2)) -> sel(X1, X2),
                 sel(X1, active(X2)) -> sel(X1, X2),
                   sel(mark(X1), X2) -> sel(X1, X2),
                 sel(active(X1), X2) -> sel(X1, X2),
                       tail(mark(X)) -> tail(X),
                     tail(active(X)) -> tail(X),
                  take(X1, mark(X2)) -> take(X1, X2),
                take(X1, active(X2)) -> take(X1, X2),
                  take(mark(X1), X2) -> take(X1, X2),
                take(active(X1), X2) -> take(X1, X2)
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                     mark(U12(X1, X2)) -> active(U12(mark(X1), X2)),
                 mark(splitAt(X1, X2)) -> active(splitAt(mark(X1), mark(X2))),
             mark(U11(X1, X2, X3, X4)) -> active(U11(mark(X1), X2, X3, X4)),
                            mark(tt()) -> active(tt()),
                    mark(pair(X1, X2)) -> active(pair(mark(X1), mark(X2))),
                    mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                          mark(snd(X)) -> active(snd(mark(X))),
                mark(afterNth(X1, X2)) ->
    active(afterNth(mark(X1), mark(X2))),
                     mark(and(X1, X2)) -> active(and(mark(X1), X2)),
                          mark(fst(X)) -> active(fst(mark(X))),
                         mark(head(X)) -> active(head(mark(X))),
                     mark(natsFrom(X)) -> active(natsFrom(mark(X))),
                            mark(s(X)) -> active(s(mark(X))),
                     mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))),
                           mark(nil()) -> active(nil()),
                             mark(0()) -> active(0()),
                         mark(tail(X)) -> active(tail(mark(X))),
                    mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))),
                     U12(X1, mark(X2)) -> U12(X1, X2),
                   U12(X1, active(X2)) -> U12(X1, X2),
                     U12(mark(X1), X2) -> U12(X1, X2),
                   U12(active(X1), X2) -> U12(X1, X2),
                 splitAt(X1, mark(X2)) -> splitAt(X1, X2),
               splitAt(X1, active(X2)) -> splitAt(X1, X2),
                 splitAt(mark(X1), X2) -> splitAt(X1, X2),
               splitAt(active(X1), X2) -> splitAt(X1, X2),
          active(U12(pair(YS, ZS), X)) -> mark(pair(cons(X, YS), ZS)),
    active(splitAt(s(N), cons(X, XS))) -> mark(U11(tt(), N, X, XS)),
              active(splitAt(0(), XS)) -> mark(pair(nil(), XS)),
           active(U11(tt(), N, X, XS)) -> mark(U12(splitAt(N, XS), X)),
               active(snd(pair(X, Y))) -> mark(Y),
               active(afterNth(N, XS)) -> mark(snd(splitAt(N, XS))),
                  active(and(tt(), X)) -> mark(X),
               active(fst(pair(X, Y))) -> mark(X),
             active(head(cons(N, XS))) -> mark(N),
                   active(natsFrom(N)) -> mark(cons(N, natsFrom(s(N)))),
                    active(sel(N, XS)) -> mark(head(afterNth(N, XS))),
             active(tail(cons(N, XS))) -> mark(XS),
                   active(take(N, XS)) -> mark(fst(splitAt(N, XS))),
             U11(X1, X2, X3, mark(X4)) -> U11(X1, X2, X3, X4),
           U11(X1, X2, X3, active(X4)) -> U11(X1, X2, X3, X4),
             U11(X1, X2, mark(X3), X4) -> U11(X1, X2, X3, X4),
           U11(X1, X2, active(X3), X4) -> U11(X1, X2, X3, X4),
             U11(X1, mark(X2), X3, X4) -> U11(X1, X2, X3, X4),
           U11(X1, active(X2), X3, X4) -> U11(X1, X2, X3, X4),
             U11(mark(X1), X2, X3, X4) -> U11(X1, X2, X3, X4),
           U11(active(X1), X2, X3, X4) -> U11(X1, X2, X3, X4),
                    pair(X1, mark(X2)) -> pair(X1, X2),
                  pair(X1, active(X2)) -> pair(X1, X2),
                    pair(mark(X1), X2) -> pair(X1, X2),
                  pair(active(X1), X2) -> pair(X1, X2),
                    cons(X1, mark(X2)) -> cons(X1, X2),
                  cons(X1, active(X2)) -> cons(X1, X2),
                    cons(mark(X1), X2) -> cons(X1, X2),
                  cons(active(X1), X2) -> cons(X1, X2),
                          snd(mark(X)) -> snd(X),
                        snd(active(X)) -> snd(X),
                afterNth(X1, mark(X2)) -> afterNth(X1, X2),
              afterNth(X1, active(X2)) -> afterNth(X1, X2),
                afterNth(mark(X1), X2) -> afterNth(X1, X2),
              afterNth(active(X1), X2) -> afterNth(X1, X2),
                     and(X1, mark(X2)) -> and(X1, X2),
                   and(X1, active(X2)) -> and(X1, X2),
                     and(mark(X1), X2) -> and(X1, X2),
                   and(active(X1), X2) -> and(X1, X2),
                          fst(mark(X)) -> fst(X),
                        fst(active(X)) -> fst(X),
                         head(mark(X)) -> head(X),
                       head(active(X)) -> head(X),
                     natsFrom(mark(X)) -> natsFrom(X),
                   natsFrom(active(X)) -> natsFrom(X),
                            s(mark(X)) -> s(X),
                          s(active(X)) -> s(X),
                     sel(X1, mark(X2)) -> sel(X1, X2),
                   sel(X1, active(X2)) -> sel(X1, X2),
                     sel(mark(X1), X2) -> sel(X1, X2),
                   sel(active(X1), X2) -> sel(X1, X2),
                         tail(mark(X)) -> tail(X),
                       tail(active(X)) -> tail(X),
                    take(X1, mark(X2)) -> take(X1, X2),
                  take(X1, active(X2)) -> take(X1, X2),
                    take(mark(X1), X2) -> take(X1, X2),
                  take(active(X1), X2) -> take(X1, X2)
   }
  Fail