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