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