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