MAYBE
MAYBE
TRS:
 {
              U102(tt()) -> tt(),
                isLNat() -> U101(isNatural()),
                isLNat() -> tt(),
                isLNat() -> U41(isNatural()),
                isLNat() -> U51(isNatural()),
                isLNat() -> U61(isPLNat()),
                isLNat() -> U71(isNatural()),
                isLNat() -> U81(isPLNat()),
                isLNat() -> U91(isLNat()),
              U101(tt()) -> U102(isLNat()),
               U12(tt()) -> snd(splitAt(N, XS)),
               U11(tt()) -> U12(isLNat()),
              U111(tt()) -> tt(),
         snd(pair(X, Y)) -> U181(isLNat()),
        splitAt(0(), XS) -> U191(isLNat()),
  splitAt(s(N), cons(X)) -> U201(isNatural()),
              U121(tt()) -> tt(),
              U132(tt()) -> tt(),
              U131(tt()) -> U132(isLNat()),
              U142(tt()) -> tt(),
              U141(tt()) -> U142(isLNat()),
              U152(tt()) -> tt(),
              U151(tt()) -> U152(isLNat()),
              U161(tt()) -> cons(N),
              U172(tt()) -> head(afterNth(N, XS)),
              U171(tt()) -> U172(isLNat()),
           head(cons(N)) -> U31(isNatural()),
         afterNth(N, XS) -> U11(isNatural()),
              U182(tt()) -> Y,
              U181(tt()) -> U182(isLNat()),
              U191(tt()) -> pair(nil(), XS),
              U202(tt()) -> U203(isLNat()),
             isNatural() -> tt(),
             isNatural() -> U111(isLNat()),
             isNatural() -> U121(isNatural()),
             isNatural() -> U131(isNatural()),
              U201(tt()) -> U202(isNatural()),
              U203(tt()) -> U204(splitAt(N, XS)),
      U204(pair(YS, ZS)) -> pair(cons(X), ZS),
               U22(tt()) -> X,
               U21(tt()) -> U22(isLNat()),
              U212(tt()) -> XS,
              U211(tt()) -> U212(isLNat()),
              U222(tt()) -> fst(splitAt(N, XS)),
              U221(tt()) -> U222(isLNat()),
         fst(pair(X, Y)) -> U21(isLNat()),
               U32(tt()) -> N,
               U31(tt()) -> U32(isLNat()),
               U42(tt()) -> tt(),
               U41(tt()) -> U42(isLNat()),
               U52(tt()) -> tt(),
               U51(tt()) -> U52(isLNat()),
               U61(tt()) -> tt(),
               U71(tt()) -> tt(),
               U81(tt()) -> tt(),
               U91(tt()) -> tt(),
               isPLNat() -> U141(isLNat()),
               isPLNat() -> U151(isNatural()),
             natsFrom(N) -> U161(isNatural()),
              sel(N, XS) -> U171(isNatural()),
           tail(cons(N)) -> U211(isNatural()),
             take(N, XS) -> U221(isNatural())
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                U102(tt()) -> tt(),
                  isLNat() -> U101(isNatural()),
                  isLNat() -> tt(),
                  isLNat() -> U41(isNatural()),
                  isLNat() -> U51(isNatural()),
                  isLNat() -> U61(isPLNat()),
                  isLNat() -> U71(isNatural()),
                  isLNat() -> U81(isPLNat()),
                  isLNat() -> U91(isLNat()),
                U101(tt()) -> U102(isLNat()),
                 U12(tt()) -> snd(splitAt(N, XS)),
                 U11(tt()) -> U12(isLNat()),
                U111(tt()) -> tt(),
           snd(pair(X, Y)) -> U181(isLNat()),
          splitAt(0(), XS) -> U191(isLNat()),
    splitAt(s(N), cons(X)) -> U201(isNatural()),
                U121(tt()) -> tt(),
                U132(tt()) -> tt(),
                U131(tt()) -> U132(isLNat()),
                U142(tt()) -> tt(),
                U141(tt()) -> U142(isLNat()),
                U152(tt()) -> tt(),
                U151(tt()) -> U152(isLNat()),
                U161(tt()) -> cons(N),
                U172(tt()) -> head(afterNth(N, XS)),
                U171(tt()) -> U172(isLNat()),
             head(cons(N)) -> U31(isNatural()),
           afterNth(N, XS) -> U11(isNatural()),
                U182(tt()) -> Y,
                U181(tt()) -> U182(isLNat()),
                U191(tt()) -> pair(nil(), XS),
                U202(tt()) -> U203(isLNat()),
               isNatural() -> tt(),
               isNatural() -> U111(isLNat()),
               isNatural() -> U121(isNatural()),
               isNatural() -> U131(isNatural()),
                U201(tt()) -> U202(isNatural()),
                U203(tt()) -> U204(splitAt(N, XS)),
        U204(pair(YS, ZS)) -> pair(cons(X), ZS),
                 U22(tt()) -> X,
                 U21(tt()) -> U22(isLNat()),
                U212(tt()) -> XS,
                U211(tt()) -> U212(isLNat()),
                U222(tt()) -> fst(splitAt(N, XS)),
                U221(tt()) -> U222(isLNat()),
           fst(pair(X, Y)) -> U21(isLNat()),
                 U32(tt()) -> N,
                 U31(tt()) -> U32(isLNat()),
                 U42(tt()) -> tt(),
                 U41(tt()) -> U42(isLNat()),
                 U52(tt()) -> tt(),
                 U51(tt()) -> U52(isLNat()),
                 U61(tt()) -> tt(),
                 U71(tt()) -> tt(),
                 U81(tt()) -> tt(),
                 U91(tt()) -> tt(),
                 isPLNat() -> U141(isLNat()),
                 isPLNat() -> U151(isNatural()),
               natsFrom(N) -> U161(isNatural()),
                sel(N, XS) -> U171(isNatural()),
             tail(cons(N)) -> U211(isNatural()),
               take(N, XS) -> U221(isNatural())
   }
  Fail