MAYBE
MAYBE
TRS:
 {
                        mark(fst(X)) -> active(fst(mark(X))),
               mark(splitAt(X1, X2)) -> active(splitAt(mark(X1), mark(X2))),
              mark(U101(X1, X2, X3)) -> active(U101(mark(X1), X2, X3)),
                          mark(tt()) -> active(tt()),
                        mark(snd(X)) -> active(snd(mark(X))),
               mark(U11(X1, X2, X3)) -> active(U11(mark(X1), X2, X3)),
                   mark(U21(X1, X2)) -> active(U21(mark(X1), X2)),
                   mark(U31(X1, X2)) -> active(U31(mark(X1), X2)),
                  mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                   mark(natsFrom(X)) -> active(natsFrom(mark(X))),
                          mark(s(X)) -> active(s(mark(X))),
                   mark(U41(X1, X2)) -> active(U41(mark(X1), X2)),
                       mark(head(X)) -> active(head(mark(X))),
              mark(afterNth(X1, X2)) -> active(afterNth(mark(X1), mark(X2))),
               mark(U51(X1, X2, X3)) -> active(U51(mark(X1), X2, X3)),
                   mark(U61(X1, X2)) -> active(U61(mark(X1), X2)),
                  mark(pair(X1, X2)) -> active(pair(mark(X1), mark(X2))),
                         mark(nil()) -> active(nil()),
                   mark(U71(X1, X2)) -> active(U71(mark(X1), X2)),
                   mark(U82(X1, X2)) -> active(U82(mark(X1), X2)),
           mark(U81(X1, X2, X3, X4)) -> active(U81(mark(X1), X2, X3, X4)),
                   mark(U91(X1, X2)) -> active(U91(mark(X1), X2)),
                   mark(and(X1, X2)) -> active(and(mark(X1), X2)),
                  mark(isNatural(X)) -> active(isNatural(X)),
                     mark(isLNat(X)) -> active(isLNat(X)),
                    mark(isPLNat(X)) -> active(isPLNat(X)),
                       mark(tail(X)) -> active(tail(mark(X))),
                  mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))),
                           mark(0()) -> active(0()),
                   mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))),
                        fst(mark(X)) -> fst(X),
                      fst(active(X)) -> fst(X),
               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(fst(pair(X, Y))) ->
  mark(U21(and(isLNat(X), isLNat(Y)), X)),
  active(splitAt(s(N), cons(X, XS))) ->
  mark(U81(and(isNatural(N), and(isNatural(X), isLNat(XS))), N, X, XS)),
            active(splitAt(0(), XS)) -> mark(U71(isLNat(XS), XS)),
           active(U101(tt(), N, XS)) -> mark(fst(splitAt(N, XS))),
             active(snd(pair(X, Y))) ->
  mark(U61(and(isLNat(X), isLNat(Y)), Y)),
            active(U11(tt(), N, XS)) -> mark(snd(splitAt(N, XS))),
                active(U21(tt(), X)) -> mark(X),
                active(U31(tt(), N)) -> mark(N),
                 active(natsFrom(N)) -> mark(U41(isNatural(N), N)),
                active(U41(tt(), N)) -> mark(cons(N, natsFrom(s(N)))),
           active(head(cons(N, XS))) ->
  mark(U31(and(isNatural(N), isLNat(XS)), N)),
             active(afterNth(N, XS)) ->
  mark(U11(and(isNatural(N), isLNat(XS)), N, XS)),
            active(U51(tt(), N, XS)) -> mark(head(afterNth(N, XS))),
                active(U61(tt(), Y)) -> mark(Y),
               active(U71(tt(), XS)) -> mark(pair(nil(), XS)),
        active(U82(pair(YS, ZS), X)) -> mark(pair(cons(X, YS), ZS)),
         active(U81(tt(), N, X, XS)) -> mark(U82(splitAt(N, XS), X)),
               active(U91(tt(), XS)) -> mark(XS),
                active(and(tt(), X)) -> mark(X),
            active(isNatural(s(V1))) -> mark(isNatural(V1)),
         active(isNatural(head(V1))) -> mark(isLNat(V1)),
              active(isNatural(0())) -> mark(tt()),
      active(isNatural(sel(V1, V2))) -> mark(and(isNatural(V1), isLNat(V2))),
             active(isLNat(fst(V1))) -> mark(isPLNat(V1)),
             active(isLNat(snd(V1))) -> mark(isPLNat(V1)),
        active(isLNat(cons(V1, V2))) -> mark(and(isNatural(V1), isLNat(V2))),
        active(isLNat(natsFrom(V1))) -> mark(isNatural(V1)),
    active(isLNat(afterNth(V1, V2))) -> mark(and(isNatural(V1), isLNat(V2))),
               active(isLNat(nil())) -> mark(tt()),
            active(isLNat(tail(V1))) -> mark(isLNat(V1)),
        active(isLNat(take(V1, V2))) -> mark(and(isNatural(V1), isLNat(V2))),
    active(isPLNat(splitAt(V1, V2))) -> mark(and(isNatural(V1), isLNat(V2))),
       active(isPLNat(pair(V1, V2))) -> mark(and(isLNat(V1), isLNat(V2))),
           active(tail(cons(N, XS))) ->
  mark(U91(and(isNatural(N), isLNat(XS)), XS)),
                 active(take(N, XS)) ->
  mark(U101(and(isNatural(N), isLNat(XS)), N, XS)),
                  active(sel(N, XS)) ->
  mark(U51(and(isNatural(N), isLNat(XS)), N, XS)),
              U101(X1, X2, mark(X3)) -> U101(X1, X2, X3),
            U101(X1, X2, active(X3)) -> U101(X1, X2, X3),
              U101(X1, mark(X2), X3) -> U101(X1, X2, X3),
            U101(X1, active(X2), X3) -> U101(X1, X2, X3),
              U101(mark(X1), X2, X3) -> U101(X1, X2, X3),
            U101(active(X1), X2, X3) -> U101(X1, X2, X3),
                        snd(mark(X)) -> snd(X),
                      snd(active(X)) -> snd(X),
               U11(X1, X2, mark(X3)) -> U11(X1, X2, X3),
             U11(X1, X2, active(X3)) -> U11(X1, X2, X3),
               U11(X1, mark(X2), X3) -> U11(X1, X2, X3),
             U11(X1, active(X2), X3) -> U11(X1, X2, X3),
               U11(mark(X1), X2, X3) -> U11(X1, X2, X3),
             U11(active(X1), X2, X3) -> U11(X1, X2, X3),
                   U21(X1, mark(X2)) -> U21(X1, X2),
                 U21(X1, active(X2)) -> U21(X1, X2),
                   U21(mark(X1), X2) -> U21(X1, X2),
                 U21(active(X1), X2) -> U21(X1, X2),
                   U31(X1, mark(X2)) -> U31(X1, X2),
                 U31(X1, active(X2)) -> U31(X1, X2),
                   U31(mark(X1), X2) -> U31(X1, X2),
                 U31(active(X1), X2) -> U31(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),
                   natsFrom(mark(X)) -> natsFrom(X),
                 natsFrom(active(X)) -> natsFrom(X),
                          s(mark(X)) -> s(X),
                        s(active(X)) -> s(X),
                   U41(X1, mark(X2)) -> U41(X1, X2),
                 U41(X1, active(X2)) -> U41(X1, X2),
                   U41(mark(X1), X2) -> U41(X1, X2),
                 U41(active(X1), X2) -> U41(X1, X2),
                       head(mark(X)) -> head(X),
                     head(active(X)) -> head(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),
               U51(X1, X2, mark(X3)) -> U51(X1, X2, X3),
             U51(X1, X2, active(X3)) -> U51(X1, X2, X3),
               U51(X1, mark(X2), X3) -> U51(X1, X2, X3),
             U51(X1, active(X2), X3) -> U51(X1, X2, X3),
               U51(mark(X1), X2, X3) -> U51(X1, X2, X3),
             U51(active(X1), X2, X3) -> U51(X1, X2, X3),
                   U61(X1, mark(X2)) -> U61(X1, X2),
                 U61(X1, active(X2)) -> U61(X1, X2),
                   U61(mark(X1), X2) -> U61(X1, X2),
                 U61(active(X1), X2) -> U61(X1, X2),
                  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),
                   U71(X1, mark(X2)) -> U71(X1, X2),
                 U71(X1, active(X2)) -> U71(X1, X2),
                   U71(mark(X1), X2) -> U71(X1, X2),
                 U71(active(X1), X2) -> U71(X1, X2),
                   U82(X1, mark(X2)) -> U82(X1, X2),
                 U82(X1, active(X2)) -> U82(X1, X2),
                   U82(mark(X1), X2) -> U82(X1, X2),
                 U82(active(X1), X2) -> U82(X1, X2),
           U81(X1, X2, X3, mark(X4)) -> U81(X1, X2, X3, X4),
         U81(X1, X2, X3, active(X4)) -> U81(X1, X2, X3, X4),
           U81(X1, X2, mark(X3), X4) -> U81(X1, X2, X3, X4),
         U81(X1, X2, active(X3), X4) -> U81(X1, X2, X3, X4),
           U81(X1, mark(X2), X3, X4) -> U81(X1, X2, X3, X4),
         U81(X1, active(X2), X3, X4) -> U81(X1, X2, X3, X4),
           U81(mark(X1), X2, X3, X4) -> U81(X1, X2, X3, X4),
         U81(active(X1), X2, X3, X4) -> U81(X1, X2, X3, X4),
                   U91(X1, mark(X2)) -> U91(X1, X2),
                 U91(X1, active(X2)) -> U91(X1, X2),
                   U91(mark(X1), X2) -> U91(X1, X2),
                 U91(active(X1), X2) -> U91(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),
                  isNatural(mark(X)) -> isNatural(X),
                isNatural(active(X)) -> isNatural(X),
                     isLNat(mark(X)) -> isLNat(X),
                   isLNat(active(X)) -> isLNat(X),
                    isPLNat(mark(X)) -> isPLNat(X),
                  isPLNat(active(X)) -> isPLNat(X),
                       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),
                   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)
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                          mark(fst(X)) -> active(fst(mark(X))),
                 mark(splitAt(X1, X2)) -> active(splitAt(mark(X1), mark(X2))),
                mark(U101(X1, X2, X3)) -> active(U101(mark(X1), X2, X3)),
                            mark(tt()) -> active(tt()),
                          mark(snd(X)) -> active(snd(mark(X))),
                 mark(U11(X1, X2, X3)) -> active(U11(mark(X1), X2, X3)),
                     mark(U21(X1, X2)) -> active(U21(mark(X1), X2)),
                     mark(U31(X1, X2)) -> active(U31(mark(X1), X2)),
                    mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                     mark(natsFrom(X)) -> active(natsFrom(mark(X))),
                            mark(s(X)) -> active(s(mark(X))),
                     mark(U41(X1, X2)) -> active(U41(mark(X1), X2)),
                         mark(head(X)) -> active(head(mark(X))),
                mark(afterNth(X1, X2)) ->
    active(afterNth(mark(X1), mark(X2))),
                 mark(U51(X1, X2, X3)) -> active(U51(mark(X1), X2, X3)),
                     mark(U61(X1, X2)) -> active(U61(mark(X1), X2)),
                    mark(pair(X1, X2)) -> active(pair(mark(X1), mark(X2))),
                           mark(nil()) -> active(nil()),
                     mark(U71(X1, X2)) -> active(U71(mark(X1), X2)),
                     mark(U82(X1, X2)) -> active(U82(mark(X1), X2)),
             mark(U81(X1, X2, X3, X4)) -> active(U81(mark(X1), X2, X3, X4)),
                     mark(U91(X1, X2)) -> active(U91(mark(X1), X2)),
                     mark(and(X1, X2)) -> active(and(mark(X1), X2)),
                    mark(isNatural(X)) -> active(isNatural(X)),
                       mark(isLNat(X)) -> active(isLNat(X)),
                      mark(isPLNat(X)) -> active(isPLNat(X)),
                         mark(tail(X)) -> active(tail(mark(X))),
                    mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))),
                             mark(0()) -> active(0()),
                     mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))),
                          fst(mark(X)) -> fst(X),
                        fst(active(X)) -> fst(X),
                 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(fst(pair(X, Y))) ->
    mark(U21(and(isLNat(X), isLNat(Y)), X)),
    active(splitAt(s(N), cons(X, XS))) ->
    mark(U81(and(isNatural(N), and(isNatural(X), isLNat(XS))), N, X, XS)),
              active(splitAt(0(), XS)) -> mark(U71(isLNat(XS), XS)),
             active(U101(tt(), N, XS)) -> mark(fst(splitAt(N, XS))),
               active(snd(pair(X, Y))) ->
    mark(U61(and(isLNat(X), isLNat(Y)), Y)),
              active(U11(tt(), N, XS)) -> mark(snd(splitAt(N, XS))),
                  active(U21(tt(), X)) -> mark(X),
                  active(U31(tt(), N)) -> mark(N),
                   active(natsFrom(N)) -> mark(U41(isNatural(N), N)),
                  active(U41(tt(), N)) -> mark(cons(N, natsFrom(s(N)))),
             active(head(cons(N, XS))) ->
    mark(U31(and(isNatural(N), isLNat(XS)), N)),
               active(afterNth(N, XS)) ->
    mark(U11(and(isNatural(N), isLNat(XS)), N, XS)),
              active(U51(tt(), N, XS)) -> mark(head(afterNth(N, XS))),
                  active(U61(tt(), Y)) -> mark(Y),
                 active(U71(tt(), XS)) -> mark(pair(nil(), XS)),
          active(U82(pair(YS, ZS), X)) -> mark(pair(cons(X, YS), ZS)),
           active(U81(tt(), N, X, XS)) -> mark(U82(splitAt(N, XS), X)),
                 active(U91(tt(), XS)) -> mark(XS),
                  active(and(tt(), X)) -> mark(X),
              active(isNatural(s(V1))) -> mark(isNatural(V1)),
           active(isNatural(head(V1))) -> mark(isLNat(V1)),
                active(isNatural(0())) -> mark(tt()),
        active(isNatural(sel(V1, V2))) ->
    mark(and(isNatural(V1), isLNat(V2))),
               active(isLNat(fst(V1))) -> mark(isPLNat(V1)),
               active(isLNat(snd(V1))) -> mark(isPLNat(V1)),
          active(isLNat(cons(V1, V2))) ->
    mark(and(isNatural(V1), isLNat(V2))),
          active(isLNat(natsFrom(V1))) -> mark(isNatural(V1)),
      active(isLNat(afterNth(V1, V2))) ->
    mark(and(isNatural(V1), isLNat(V2))),
                 active(isLNat(nil())) -> mark(tt()),
              active(isLNat(tail(V1))) -> mark(isLNat(V1)),
          active(isLNat(take(V1, V2))) ->
    mark(and(isNatural(V1), isLNat(V2))),
      active(isPLNat(splitAt(V1, V2))) ->
    mark(and(isNatural(V1), isLNat(V2))),
         active(isPLNat(pair(V1, V2))) -> mark(and(isLNat(V1), isLNat(V2))),
             active(tail(cons(N, XS))) ->
    mark(U91(and(isNatural(N), isLNat(XS)), XS)),
                   active(take(N, XS)) ->
    mark(U101(and(isNatural(N), isLNat(XS)), N, XS)),
                    active(sel(N, XS)) ->
    mark(U51(and(isNatural(N), isLNat(XS)), N, XS)),
                U101(X1, X2, mark(X3)) -> U101(X1, X2, X3),
              U101(X1, X2, active(X3)) -> U101(X1, X2, X3),
                U101(X1, mark(X2), X3) -> U101(X1, X2, X3),
              U101(X1, active(X2), X3) -> U101(X1, X2, X3),
                U101(mark(X1), X2, X3) -> U101(X1, X2, X3),
              U101(active(X1), X2, X3) -> U101(X1, X2, X3),
                          snd(mark(X)) -> snd(X),
                        snd(active(X)) -> snd(X),
                 U11(X1, X2, mark(X3)) -> U11(X1, X2, X3),
               U11(X1, X2, active(X3)) -> U11(X1, X2, X3),
                 U11(X1, mark(X2), X3) -> U11(X1, X2, X3),
               U11(X1, active(X2), X3) -> U11(X1, X2, X3),
                 U11(mark(X1), X2, X3) -> U11(X1, X2, X3),
               U11(active(X1), X2, X3) -> U11(X1, X2, X3),
                     U21(X1, mark(X2)) -> U21(X1, X2),
                   U21(X1, active(X2)) -> U21(X1, X2),
                     U21(mark(X1), X2) -> U21(X1, X2),
                   U21(active(X1), X2) -> U21(X1, X2),
                     U31(X1, mark(X2)) -> U31(X1, X2),
                   U31(X1, active(X2)) -> U31(X1, X2),
                     U31(mark(X1), X2) -> U31(X1, X2),
                   U31(active(X1), X2) -> U31(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),
                     natsFrom(mark(X)) -> natsFrom(X),
                   natsFrom(active(X)) -> natsFrom(X),
                            s(mark(X)) -> s(X),
                          s(active(X)) -> s(X),
                     U41(X1, mark(X2)) -> U41(X1, X2),
                   U41(X1, active(X2)) -> U41(X1, X2),
                     U41(mark(X1), X2) -> U41(X1, X2),
                   U41(active(X1), X2) -> U41(X1, X2),
                         head(mark(X)) -> head(X),
                       head(active(X)) -> head(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),
                 U51(X1, X2, mark(X3)) -> U51(X1, X2, X3),
               U51(X1, X2, active(X3)) -> U51(X1, X2, X3),
                 U51(X1, mark(X2), X3) -> U51(X1, X2, X3),
               U51(X1, active(X2), X3) -> U51(X1, X2, X3),
                 U51(mark(X1), X2, X3) -> U51(X1, X2, X3),
               U51(active(X1), X2, X3) -> U51(X1, X2, X3),
                     U61(X1, mark(X2)) -> U61(X1, X2),
                   U61(X1, active(X2)) -> U61(X1, X2),
                     U61(mark(X1), X2) -> U61(X1, X2),
                   U61(active(X1), X2) -> U61(X1, X2),
                    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),
                     U71(X1, mark(X2)) -> U71(X1, X2),
                   U71(X1, active(X2)) -> U71(X1, X2),
                     U71(mark(X1), X2) -> U71(X1, X2),
                   U71(active(X1), X2) -> U71(X1, X2),
                     U82(X1, mark(X2)) -> U82(X1, X2),
                   U82(X1, active(X2)) -> U82(X1, X2),
                     U82(mark(X1), X2) -> U82(X1, X2),
                   U82(active(X1), X2) -> U82(X1, X2),
             U81(X1, X2, X3, mark(X4)) -> U81(X1, X2, X3, X4),
           U81(X1, X2, X3, active(X4)) -> U81(X1, X2, X3, X4),
             U81(X1, X2, mark(X3), X4) -> U81(X1, X2, X3, X4),
           U81(X1, X2, active(X3), X4) -> U81(X1, X2, X3, X4),
             U81(X1, mark(X2), X3, X4) -> U81(X1, X2, X3, X4),
           U81(X1, active(X2), X3, X4) -> U81(X1, X2, X3, X4),
             U81(mark(X1), X2, X3, X4) -> U81(X1, X2, X3, X4),
           U81(active(X1), X2, X3, X4) -> U81(X1, X2, X3, X4),
                     U91(X1, mark(X2)) -> U91(X1, X2),
                   U91(X1, active(X2)) -> U91(X1, X2),
                     U91(mark(X1), X2) -> U91(X1, X2),
                   U91(active(X1), X2) -> U91(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),
                    isNatural(mark(X)) -> isNatural(X),
                  isNatural(active(X)) -> isNatural(X),
                       isLNat(mark(X)) -> isLNat(X),
                     isLNat(active(X)) -> isLNat(X),
                      isPLNat(mark(X)) -> isPLNat(X),
                    isPLNat(active(X)) -> isPLNat(X),
                         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),
                     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)
   }
  Fail