MAYBE
MAYBE
TRS:
 {
              U102(tt()) -> U103(isLNat()),
             isNatural() -> tt(),
             isNatural() -> U111(isLNatKind()),
             isNatural() -> U121(isNaturalKind()),
             isNatural() -> U131(and(isNaturalKind())),
              U101(tt()) -> U102(isNatural()),
              U103(tt()) -> tt(),
                isLNat() -> U101(and(isNaturalKind())),
                isLNat() -> tt(),
                isLNat() -> U41(and(isNaturalKind())),
                isLNat() -> U51(and(isNaturalKind())),
                isLNat() -> U61(isPLNatKind()),
                isLNat() -> U71(isNaturalKind()),
                isLNat() -> U81(isPLNatKind()),
                isLNat() -> U91(isLNatKind()),
         snd(pair(X, Y)) -> U181(and(and(isLNat()))),
        splitAt(0(), XS) -> U191(and(isLNat())),
  splitAt(s(N), cons(X)) -> U201(and(and(isNatural()))),
               U11(tt()) -> snd(splitAt(N, XS)),
              U112(tt()) -> tt(),
              U111(tt()) -> U112(isLNat()),
              U122(tt()) -> tt(),
              U121(tt()) -> U122(isNatural()),
              U132(tt()) -> U133(isLNat()),
              U131(tt()) -> U132(isNatural()),
              U133(tt()) -> tt(),
              U142(tt()) -> U143(isLNat()),
              U141(tt()) -> U142(isLNat()),
              U143(tt()) -> tt(),
              U152(tt()) -> U153(isLNat()),
              U151(tt()) -> U152(isNatural()),
              U153(tt()) -> tt(),
              U161(tt()) -> cons(N),
           head(cons(N)) -> U31(and(and(isNatural()))),
         afterNth(N, XS) -> U11(and(and(isNatural()))),
              U171(tt()) -> head(afterNth(N, XS)),
              U181(tt()) -> Y,
              U191(tt()) -> pair(nil(), XS),
      U202(pair(YS, ZS)) -> pair(cons(X), ZS),
              U201(tt()) -> U202(splitAt(N, XS)),
               U21(tt()) -> X,
              U211(tt()) -> XS,
         fst(pair(X, Y)) -> U21(and(and(isLNat()))),
              U221(tt()) -> fst(splitAt(N, XS)),
               U31(tt()) -> N,
               U42(tt()) -> U43(isLNat()),
               U41(tt()) -> U42(isNatural()),
               U43(tt()) -> tt(),
               U52(tt()) -> U53(isLNat()),
               U51(tt()) -> U52(isNatural()),
               U53(tt()) -> tt(),
               U62(tt()) -> tt(),
               isPLNat() -> U141(and(isLNatKind())),
               isPLNat() -> U151(and(isNaturalKind())),
               U61(tt()) -> U62(isPLNat()),
               U72(tt()) -> tt(),
               U71(tt()) -> U72(isNatural()),
               U82(tt()) -> tt(),
               U81(tt()) -> U82(isPLNat()),
               U92(tt()) -> tt(),
               U91(tt()) -> U92(isLNat()),
               and(tt()) -> X,
         isNaturalKind() -> tt(),
         isNaturalKind() -> and(isNaturalKind()),
         isNaturalKind() -> isNaturalKind(),
         isNaturalKind() -> isLNatKind(),
           isPLNatKind() -> and(isNaturalKind()),
           isPLNatKind() -> and(isLNatKind()),
            isLNatKind() -> tt(),
            isLNatKind() -> and(isNaturalKind()),
            isLNatKind() -> isNaturalKind(),
            isLNatKind() -> isPLNatKind(),
            isLNatKind() -> isLNatKind(),
             natsFrom(N) -> U161(and(isNatural())),
              sel(N, XS) -> U171(and(and(isNatural()))),
           tail(cons(N)) -> U211(and(and(isNatural()))),
             take(N, XS) -> U221(and(and(isNatural())))
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                U102(tt()) -> U103(isLNat()),
               isNatural() -> tt(),
               isNatural() -> U111(isLNatKind()),
               isNatural() -> U121(isNaturalKind()),
               isNatural() -> U131(and(isNaturalKind())),
                U101(tt()) -> U102(isNatural()),
                U103(tt()) -> tt(),
                  isLNat() -> U101(and(isNaturalKind())),
                  isLNat() -> tt(),
                  isLNat() -> U41(and(isNaturalKind())),
                  isLNat() -> U51(and(isNaturalKind())),
                  isLNat() -> U61(isPLNatKind()),
                  isLNat() -> U71(isNaturalKind()),
                  isLNat() -> U81(isPLNatKind()),
                  isLNat() -> U91(isLNatKind()),
           snd(pair(X, Y)) -> U181(and(and(isLNat()))),
          splitAt(0(), XS) -> U191(and(isLNat())),
    splitAt(s(N), cons(X)) -> U201(and(and(isNatural()))),
                 U11(tt()) -> snd(splitAt(N, XS)),
                U112(tt()) -> tt(),
                U111(tt()) -> U112(isLNat()),
                U122(tt()) -> tt(),
                U121(tt()) -> U122(isNatural()),
                U132(tt()) -> U133(isLNat()),
                U131(tt()) -> U132(isNatural()),
                U133(tt()) -> tt(),
                U142(tt()) -> U143(isLNat()),
                U141(tt()) -> U142(isLNat()),
                U143(tt()) -> tt(),
                U152(tt()) -> U153(isLNat()),
                U151(tt()) -> U152(isNatural()),
                U153(tt()) -> tt(),
                U161(tt()) -> cons(N),
             head(cons(N)) -> U31(and(and(isNatural()))),
           afterNth(N, XS) -> U11(and(and(isNatural()))),
                U171(tt()) -> head(afterNth(N, XS)),
                U181(tt()) -> Y,
                U191(tt()) -> pair(nil(), XS),
        U202(pair(YS, ZS)) -> pair(cons(X), ZS),
                U201(tt()) -> U202(splitAt(N, XS)),
                 U21(tt()) -> X,
                U211(tt()) -> XS,
           fst(pair(X, Y)) -> U21(and(and(isLNat()))),
                U221(tt()) -> fst(splitAt(N, XS)),
                 U31(tt()) -> N,
                 U42(tt()) -> U43(isLNat()),
                 U41(tt()) -> U42(isNatural()),
                 U43(tt()) -> tt(),
                 U52(tt()) -> U53(isLNat()),
                 U51(tt()) -> U52(isNatural()),
                 U53(tt()) -> tt(),
                 U62(tt()) -> tt(),
                 isPLNat() -> U141(and(isLNatKind())),
                 isPLNat() -> U151(and(isNaturalKind())),
                 U61(tt()) -> U62(isPLNat()),
                 U72(tt()) -> tt(),
                 U71(tt()) -> U72(isNatural()),
                 U82(tt()) -> tt(),
                 U81(tt()) -> U82(isPLNat()),
                 U92(tt()) -> tt(),
                 U91(tt()) -> U92(isLNat()),
                 and(tt()) -> X,
           isNaturalKind() -> tt(),
           isNaturalKind() -> and(isNaturalKind()),
           isNaturalKind() -> isNaturalKind(),
           isNaturalKind() -> isLNatKind(),
             isPLNatKind() -> and(isNaturalKind()),
             isPLNatKind() -> and(isLNatKind()),
              isLNatKind() -> tt(),
              isLNatKind() -> and(isNaturalKind()),
              isLNatKind() -> isNaturalKind(),
              isLNatKind() -> isPLNatKind(),
              isLNatKind() -> isLNatKind(),
               natsFrom(N) -> U161(and(isNatural())),
                sel(N, XS) -> U171(and(and(isNatural()))),
             tail(cons(N)) -> U211(and(and(isNatural()))),
               take(N, XS) -> U221(and(and(isNatural())))
   }
  Fail