MAYBE
MAYBE
TRS:
 {
                         fst(X) -> n__fst(X),
                fst(pair(X, Y)) -> U21(and(isLNat(X), n__isLNat(Y)), X),
                splitAt(X1, X2) -> n__splitAt(X1, X2),
     splitAt(s(N), cons(X, XS)) ->
  U81(
     and(isNatural(N), n__and(isNatural(X), n__isLNat(activate(XS)))), 
     N, X, activate(XS)
  ),
               splitAt(0(), XS) -> U71(isLNat(XS), XS),
                    activate(X) -> X,
       activate(n__natsFrom(X)) -> natsFrom(X),
         activate(n__isLNat(X)) -> isLNat(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),
       activate(n__and(X1, X2)) -> and(X1, X2),
              U101(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))),
                         snd(X) -> n__snd(X),
                snd(pair(X, Y)) -> U61(and(isLNat(X), n__isLNat(Y)), Y),
               U11(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))),
                   U21(tt(), X) -> activate(X),
                   U31(tt(), N) -> activate(N),
                   cons(X1, X2) -> n__cons(X1, X2),
                           s(X) -> n__s(X),
                   U41(tt(), N) ->
  cons(activate(N), n__natsFrom(s(activate(N)))),
                        head(X) -> n__head(X),
              head(cons(N, XS)) ->
  U31(and(isNatural(N), n__isLNat(activate(XS))), N),
                afterNth(N, XS) ->
  U11(and(isNatural(N), n__isLNat(XS)), N, XS),
               afterNth(X1, X2) -> n__afterNth(X1, X2),
               U51(tt(), N, XS) -> head(afterNth(activate(N), activate(XS))),
                   U61(tt(), Y) -> activate(Y),
                   pair(X1, X2) -> n__pair(X1, X2),
                          nil() -> n__nil(),
                  U71(tt(), XS) -> pair(nil(), activate(XS)),
           U82(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS),
            U81(tt(), N, X, XS) ->
  U82(splitAt(activate(N), activate(XS)), activate(X)),
                  U91(tt(), XS) -> activate(XS),
                    and(X1, X2) -> n__and(X1, X2),
                   and(tt(), X) -> activate(X),
              isNatural(n__0()) -> tt(),
         isNatural(n__head(V1)) -> isLNat(activate(V1)),
            isNatural(n__s(V1)) -> isNatural(activate(V1)),
      isNatural(n__sel(V1, V2)) ->
  and(isNatural(activate(V1)), n__isLNat(activate(V2))),
                      isLNat(X) -> n__isLNat(X),
        isLNat(n__natsFrom(V1)) -> isNatural(activate(V1)),
               isLNat(n__nil()) -> tt(),
    isLNat(n__afterNth(V1, V2)) ->
  and(isNatural(activate(V1)), n__isLNat(activate(V2))),
        isLNat(n__cons(V1, V2)) ->
  and(isNatural(activate(V1)), n__isLNat(activate(V2))),
             isLNat(n__fst(V1)) -> isPLNat(activate(V1)),
             isLNat(n__snd(V1)) -> isPLNat(activate(V1)),
            isLNat(n__tail(V1)) -> isLNat(activate(V1)),
        isLNat(n__take(V1, V2)) ->
  and(isNatural(activate(V1)), n__isLNat(activate(V2))),
       isPLNat(n__pair(V1, V2)) ->
  and(isLNat(activate(V1)), n__isLNat(activate(V2))),
    isPLNat(n__splitAt(V1, V2)) ->
  and(isNatural(activate(V1)), n__isLNat(activate(V2))),
                    natsFrom(N) -> U41(isNatural(N), N),
                    natsFrom(X) -> n__natsFrom(X),
                     sel(N, XS) ->
  U51(and(isNatural(N), n__isLNat(XS)), N, XS),
                    sel(X1, X2) -> n__sel(X1, X2),
                            0() -> n__0(),
                        tail(X) -> n__tail(X),
              tail(cons(N, XS)) ->
  U91(and(isNatural(N), n__isLNat(activate(XS))), activate(XS)),
                    take(N, XS) ->
  U101(and(isNatural(N), n__isLNat(XS)), N, XS),
                   take(X1, X2) -> n__take(X1, X2)
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                           fst(X) -> n__fst(X),
                  fst(pair(X, Y)) -> U21(and(isLNat(X), n__isLNat(Y)), X),
                  splitAt(X1, X2) -> n__splitAt(X1, X2),
       splitAt(s(N), cons(X, XS)) ->
    U81(
       and(isNatural(N), n__and(isNatural(X), n__isLNat(activate(XS)))), 
       N, X, activate(XS)
    ),
                 splitAt(0(), XS) -> U71(isLNat(XS), XS),
                      activate(X) -> X,
         activate(n__natsFrom(X)) -> natsFrom(X),
           activate(n__isLNat(X)) -> isLNat(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),
         activate(n__and(X1, X2)) -> and(X1, X2),
                U101(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS))),
                           snd(X) -> n__snd(X),
                  snd(pair(X, Y)) -> U61(and(isLNat(X), n__isLNat(Y)), Y),
                 U11(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS))),
                     U21(tt(), X) -> activate(X),
                     U31(tt(), N) -> activate(N),
                     cons(X1, X2) -> n__cons(X1, X2),
                             s(X) -> n__s(X),
                     U41(tt(), N) ->
    cons(activate(N), n__natsFrom(s(activate(N)))),
                          head(X) -> n__head(X),
                head(cons(N, XS)) ->
    U31(and(isNatural(N), n__isLNat(activate(XS))), N),
                  afterNth(N, XS) ->
    U11(and(isNatural(N), n__isLNat(XS)), N, XS),
                 afterNth(X1, X2) -> n__afterNth(X1, X2),
                 U51(tt(), N, XS) ->
    head(afterNth(activate(N), activate(XS))),
                     U61(tt(), Y) -> activate(Y),
                     pair(X1, X2) -> n__pair(X1, X2),
                            nil() -> n__nil(),
                    U71(tt(), XS) -> pair(nil(), activate(XS)),
             U82(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS),
              U81(tt(), N, X, XS) ->
    U82(splitAt(activate(N), activate(XS)), activate(X)),
                    U91(tt(), XS) -> activate(XS),
                      and(X1, X2) -> n__and(X1, X2),
                     and(tt(), X) -> activate(X),
                isNatural(n__0()) -> tt(),
           isNatural(n__head(V1)) -> isLNat(activate(V1)),
              isNatural(n__s(V1)) -> isNatural(activate(V1)),
        isNatural(n__sel(V1, V2)) ->
    and(isNatural(activate(V1)), n__isLNat(activate(V2))),
                        isLNat(X) -> n__isLNat(X),
          isLNat(n__natsFrom(V1)) -> isNatural(activate(V1)),
                 isLNat(n__nil()) -> tt(),
      isLNat(n__afterNth(V1, V2)) ->
    and(isNatural(activate(V1)), n__isLNat(activate(V2))),
          isLNat(n__cons(V1, V2)) ->
    and(isNatural(activate(V1)), n__isLNat(activate(V2))),
               isLNat(n__fst(V1)) -> isPLNat(activate(V1)),
               isLNat(n__snd(V1)) -> isPLNat(activate(V1)),
              isLNat(n__tail(V1)) -> isLNat(activate(V1)),
          isLNat(n__take(V1, V2)) ->
    and(isNatural(activate(V1)), n__isLNat(activate(V2))),
         isPLNat(n__pair(V1, V2)) ->
    and(isLNat(activate(V1)), n__isLNat(activate(V2))),
      isPLNat(n__splitAt(V1, V2)) ->
    and(isNatural(activate(V1)), n__isLNat(activate(V2))),
                      natsFrom(N) -> U41(isNatural(N), N),
                      natsFrom(X) -> n__natsFrom(X),
                       sel(N, XS) ->
    U51(and(isNatural(N), n__isLNat(XS)), N, XS),
                      sel(X1, X2) -> n__sel(X1, X2),
                              0() -> n__0(),
                          tail(X) -> n__tail(X),
                tail(cons(N, XS)) ->
    U91(and(isNatural(N), n__isLNat(activate(XS))), activate(XS)),
                      take(N, XS) ->
    U101(and(isNatural(N), n__isLNat(XS)), N, XS),
                     take(X1, X2) -> n__take(X1, X2)
   }
  Fail