MAYBE

Problem:
 U101(tt(),N,XS) -> fst(splitAt(activate(N),activate(XS)))
 U11(tt(),N,XS) -> snd(splitAt(activate(N),activate(XS)))
 U21(tt(),X) -> activate(X)
 U31(tt(),N) -> activate(N)
 U41(tt(),N) -> cons(activate(N),n__natsFrom(n__s(activate(N))))
 U51(tt(),N,XS) -> head(afterNth(activate(N),activate(XS)))
 U61(tt(),Y) -> activate(Y)
 U71(tt(),XS) -> pair(nil(),activate(XS))
 U81(tt(),N,X,XS) -> U82(splitAt(activate(N),activate(XS)),activate(X))
 U82(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS)
 U91(tt(),XS) -> activate(XS)
 afterNth(N,XS) -> U11(and(isNatural(N),n__isLNat(XS)),N,XS)
 and(tt(),X) -> activate(X)
 fst(pair(X,Y)) -> U21(and(isLNat(X),n__isLNat(Y)),X)
 head(cons(N,XS)) -> U31(and(isNatural(N),n__isLNat(activate(XS))),N)
 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__natsFrom(V1)) -> isNatural(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)))
 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)))
 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)
 sel(N,XS) -> U51(and(isNatural(N),n__isLNat(XS)),N,XS)
 snd(pair(X,Y)) -> U61(and(isLNat(X),n__isLNat(Y)),Y)
 splitAt(0(),XS) -> U71(isLNat(XS),XS)
 splitAt(s(N),cons(X,XS)) ->
 U81(and(isNatural(N),n__and(n__isNatural(X),n__isLNat(activate(XS)))),N,X,activate(XS))
 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)
 natsFrom(X) -> n__natsFrom(X)
 s(X) -> n__s(X)
 isLNat(X) -> n__isLNat(X)
 nil() -> n__nil()
 afterNth(X1,X2) -> n__afterNth(X1,X2)
 cons(X1,X2) -> n__cons(X1,X2)
 fst(X) -> n__fst(X)
 snd(X) -> n__snd(X)
 tail(X) -> n__tail(X)
 take(X1,X2) -> n__take(X1,X2)
 0() -> n__0()
 head(X) -> n__head(X)
 sel(X1,X2) -> n__sel(X1,X2)
 pair(X1,X2) -> n__pair(X1,X2)
 splitAt(X1,X2) -> n__splitAt(X1,X2)
 and(X1,X2) -> n__and(X1,X2)
 isNatural(X) -> n__isNatural(X)
 activate(n__natsFrom(X)) -> natsFrom(activate(X))
 activate(n__s(X)) -> s(activate(X))
 activate(n__isLNat(X)) -> isLNat(X)
 activate(n__nil()) -> nil()
 activate(n__afterNth(X1,X2)) -> afterNth(activate(X1),activate(X2))
 activate(n__cons(X1,X2)) -> cons(activate(X1),X2)
 activate(n__fst(X)) -> fst(activate(X))
 activate(n__snd(X)) -> snd(activate(X))
 activate(n__tail(X)) -> tail(activate(X))
 activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
 activate(n__0()) -> 0()
 activate(n__head(X)) -> head(activate(X))
 activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2))
 activate(n__pair(X1,X2)) -> pair(activate(X1),activate(X2))
 activate(n__splitAt(X1,X2)) -> splitAt(activate(X1),activate(X2))
 activate(n__and(X1,X2)) -> and(activate(X1),X2)
 activate(n__isNatural(X)) -> isNatural(X)
 activate(X) -> X

Proof:
 DP Processor:
  DPs:
   U101#(tt(),N,XS) -> activate#(XS)
   U101#(tt(),N,XS) -> activate#(N)
   U101#(tt(),N,XS) -> splitAt#(activate(N),activate(XS))
   U101#(tt(),N,XS) -> fst#(splitAt(activate(N),activate(XS)))
   U11#(tt(),N,XS) -> activate#(XS)
   U11#(tt(),N,XS) -> activate#(N)
   U11#(tt(),N,XS) -> splitAt#(activate(N),activate(XS))
   U11#(tt(),N,XS) -> snd#(splitAt(activate(N),activate(XS)))
   U21#(tt(),X) -> activate#(X)
   U31#(tt(),N) -> activate#(N)
   U41#(tt(),N) -> activate#(N)
   U41#(tt(),N) -> cons#(activate(N),n__natsFrom(n__s(activate(N))))
   U51#(tt(),N,XS) -> activate#(XS)
   U51#(tt(),N,XS) -> activate#(N)
   U51#(tt(),N,XS) -> afterNth#(activate(N),activate(XS))
   U51#(tt(),N,XS) -> head#(afterNth(activate(N),activate(XS)))
   U61#(tt(),Y) -> activate#(Y)
   U71#(tt(),XS) -> activate#(XS)
   U71#(tt(),XS) -> nil#()
   U71#(tt(),XS) -> pair#(nil(),activate(XS))
   U81#(tt(),N,X,XS) -> activate#(X)
   U81#(tt(),N,X,XS) -> activate#(XS)
   U81#(tt(),N,X,XS) -> activate#(N)
   U81#(tt(),N,X,XS) -> splitAt#(activate(N),activate(XS))
   U81#(tt(),N,X,XS) -> U82#(splitAt(activate(N),activate(XS)),activate(X))
   U82#(pair(YS,ZS),X) -> activate#(X)
   U82#(pair(YS,ZS),X) -> cons#(activate(X),YS)
   U82#(pair(YS,ZS),X) -> pair#(cons(activate(X),YS),ZS)
   U91#(tt(),XS) -> activate#(XS)
   afterNth#(N,XS) -> isNatural#(N)
   afterNth#(N,XS) -> and#(isNatural(N),n__isLNat(XS))
   afterNth#(N,XS) -> U11#(and(isNatural(N),n__isLNat(XS)),N,XS)
   and#(tt(),X) -> activate#(X)
   fst#(pair(X,Y)) -> isLNat#(X)
   fst#(pair(X,Y)) -> and#(isLNat(X),n__isLNat(Y))
   fst#(pair(X,Y)) -> U21#(and(isLNat(X),n__isLNat(Y)),X)
   head#(cons(N,XS)) -> activate#(XS)
   head#(cons(N,XS)) -> isNatural#(N)
   head#(cons(N,XS)) -> and#(isNatural(N),n__isLNat(activate(XS)))
   head#(cons(N,XS)) -> U31#(and(isNatural(N),n__isLNat(activate(XS))),N)
   isLNat#(n__afterNth(V1,V2)) -> activate#(V2)
   isLNat#(n__afterNth(V1,V2)) -> activate#(V1)
   isLNat#(n__afterNth(V1,V2)) -> isNatural#(activate(V1))
   isLNat#(n__afterNth(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2)))
   isLNat#(n__cons(V1,V2)) -> activate#(V2)
   isLNat#(n__cons(V1,V2)) -> activate#(V1)
   isLNat#(n__cons(V1,V2)) -> isNatural#(activate(V1))
   isLNat#(n__cons(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2)))
   isLNat#(n__fst(V1)) -> activate#(V1)
   isLNat#(n__fst(V1)) -> isPLNat#(activate(V1))
   isLNat#(n__natsFrom(V1)) -> activate#(V1)
   isLNat#(n__natsFrom(V1)) -> isNatural#(activate(V1))
   isLNat#(n__snd(V1)) -> activate#(V1)
   isLNat#(n__snd(V1)) -> isPLNat#(activate(V1))
   isLNat#(n__tail(V1)) -> activate#(V1)
   isLNat#(n__tail(V1)) -> isLNat#(activate(V1))
   isLNat#(n__take(V1,V2)) -> activate#(V2)
   isLNat#(n__take(V1,V2)) -> activate#(V1)
   isLNat#(n__take(V1,V2)) -> isNatural#(activate(V1))
   isLNat#(n__take(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2)))
   isNatural#(n__head(V1)) -> activate#(V1)
   isNatural#(n__head(V1)) -> isLNat#(activate(V1))
   isNatural#(n__s(V1)) -> activate#(V1)
   isNatural#(n__s(V1)) -> isNatural#(activate(V1))
   isNatural#(n__sel(V1,V2)) -> activate#(V2)
   isNatural#(n__sel(V1,V2)) -> activate#(V1)
   isNatural#(n__sel(V1,V2)) -> isNatural#(activate(V1))
   isNatural#(n__sel(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2)))
   isPLNat#(n__pair(V1,V2)) -> activate#(V2)
   isPLNat#(n__pair(V1,V2)) -> activate#(V1)
   isPLNat#(n__pair(V1,V2)) -> isLNat#(activate(V1))
   isPLNat#(n__pair(V1,V2)) -> and#(isLNat(activate(V1)),n__isLNat(activate(V2)))
   isPLNat#(n__splitAt(V1,V2)) -> activate#(V2)
   isPLNat#(n__splitAt(V1,V2)) -> activate#(V1)
   isPLNat#(n__splitAt(V1,V2)) -> isNatural#(activate(V1))
   isPLNat#(n__splitAt(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2)))
   natsFrom#(N) -> isNatural#(N)
   natsFrom#(N) -> U41#(isNatural(N),N)
   sel#(N,XS) -> isNatural#(N)
   sel#(N,XS) -> and#(isNatural(N),n__isLNat(XS))
   sel#(N,XS) -> U51#(and(isNatural(N),n__isLNat(XS)),N,XS)
   snd#(pair(X,Y)) -> isLNat#(X)
   snd#(pair(X,Y)) -> and#(isLNat(X),n__isLNat(Y))
   snd#(pair(X,Y)) -> U61#(and(isLNat(X),n__isLNat(Y)),Y)
   splitAt#(0(),XS) -> isLNat#(XS)
   splitAt#(0(),XS) -> U71#(isLNat(XS),XS)
   splitAt#(s(N),cons(X,XS)) -> activate#(XS)
   splitAt#(s(N),cons(X,XS)) -> isNatural#(N)
   splitAt#(s(N),cons(X,XS)) -> and#(isNatural(N),n__and(n__isNatural(X),n__isLNat(activate(XS))))
   splitAt#(s(N),cons(X,XS)) ->
   U81#(and(isNatural(N),n__and(n__isNatural(X),n__isLNat(activate(XS)))),N,X,activate(XS))
   tail#(cons(N,XS)) -> activate#(XS)
   tail#(cons(N,XS)) -> isNatural#(N)
   tail#(cons(N,XS)) -> and#(isNatural(N),n__isLNat(activate(XS)))
   tail#(cons(N,XS)) -> U91#(and(isNatural(N),n__isLNat(activate(XS))),activate(XS))
   take#(N,XS) -> isNatural#(N)
   take#(N,XS) -> and#(isNatural(N),n__isLNat(XS))
   take#(N,XS) -> U101#(and(isNatural(N),n__isLNat(XS)),N,XS)
   activate#(n__natsFrom(X)) -> activate#(X)
   activate#(n__natsFrom(X)) -> natsFrom#(activate(X))
   activate#(n__s(X)) -> activate#(X)
   activate#(n__s(X)) -> s#(activate(X))
   activate#(n__isLNat(X)) -> isLNat#(X)
   activate#(n__nil()) -> nil#()
   activate#(n__afterNth(X1,X2)) -> activate#(X2)
   activate#(n__afterNth(X1,X2)) -> activate#(X1)
   activate#(n__afterNth(X1,X2)) -> afterNth#(activate(X1),activate(X2))
   activate#(n__cons(X1,X2)) -> activate#(X1)
   activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2)
   activate#(n__fst(X)) -> activate#(X)
   activate#(n__fst(X)) -> fst#(activate(X))
   activate#(n__snd(X)) -> activate#(X)
   activate#(n__snd(X)) -> snd#(activate(X))
   activate#(n__tail(X)) -> activate#(X)
   activate#(n__tail(X)) -> tail#(activate(X))
   activate#(n__take(X1,X2)) -> activate#(X2)
   activate#(n__take(X1,X2)) -> activate#(X1)
   activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2))
   activate#(n__0()) -> 0#()
   activate#(n__head(X)) -> activate#(X)
   activate#(n__head(X)) -> head#(activate(X))
   activate#(n__sel(X1,X2)) -> activate#(X2)
   activate#(n__sel(X1,X2)) -> activate#(X1)
   activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2))
   activate#(n__pair(X1,X2)) -> activate#(X2)
   activate#(n__pair(X1,X2)) -> activate#(X1)
   activate#(n__pair(X1,X2)) -> pair#(activate(X1),activate(X2))
   activate#(n__splitAt(X1,X2)) -> activate#(X2)
   activate#(n__splitAt(X1,X2)) -> activate#(X1)
   activate#(n__splitAt(X1,X2)) -> splitAt#(activate(X1),activate(X2))
   activate#(n__and(X1,X2)) -> activate#(X1)
   activate#(n__and(X1,X2)) -> and#(activate(X1),X2)
   activate#(n__isNatural(X)) -> isNatural#(X)
  TRS:
   U101(tt(),N,XS) -> fst(splitAt(activate(N),activate(XS)))
   U11(tt(),N,XS) -> snd(splitAt(activate(N),activate(XS)))
   U21(tt(),X) -> activate(X)
   U31(tt(),N) -> activate(N)
   U41(tt(),N) -> cons(activate(N),n__natsFrom(n__s(activate(N))))
   U51(tt(),N,XS) -> head(afterNth(activate(N),activate(XS)))
   U61(tt(),Y) -> activate(Y)
   U71(tt(),XS) -> pair(nil(),activate(XS))
   U81(tt(),N,X,XS) -> U82(splitAt(activate(N),activate(XS)),activate(X))
   U82(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS)
   U91(tt(),XS) -> activate(XS)
   afterNth(N,XS) -> U11(and(isNatural(N),n__isLNat(XS)),N,XS)
   and(tt(),X) -> activate(X)
   fst(pair(X,Y)) -> U21(and(isLNat(X),n__isLNat(Y)),X)
   head(cons(N,XS)) -> U31(and(isNatural(N),n__isLNat(activate(XS))),N)
   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__natsFrom(V1)) -> isNatural(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)))
   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)))
   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)
   sel(N,XS) -> U51(and(isNatural(N),n__isLNat(XS)),N,XS)
   snd(pair(X,Y)) -> U61(and(isLNat(X),n__isLNat(Y)),Y)
   splitAt(0(),XS) -> U71(isLNat(XS),XS)
   splitAt(s(N),cons(X,XS)) ->
   U81(and(isNatural(N),n__and(n__isNatural(X),n__isLNat(activate(XS)))),N,X,activate(XS))
   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)
   natsFrom(X) -> n__natsFrom(X)
   s(X) -> n__s(X)
   isLNat(X) -> n__isLNat(X)
   nil() -> n__nil()
   afterNth(X1,X2) -> n__afterNth(X1,X2)
   cons(X1,X2) -> n__cons(X1,X2)
   fst(X) -> n__fst(X)
   snd(X) -> n__snd(X)
   tail(X) -> n__tail(X)
   take(X1,X2) -> n__take(X1,X2)
   0() -> n__0()
   head(X) -> n__head(X)
   sel(X1,X2) -> n__sel(X1,X2)
   pair(X1,X2) -> n__pair(X1,X2)
   splitAt(X1,X2) -> n__splitAt(X1,X2)
   and(X1,X2) -> n__and(X1,X2)
   isNatural(X) -> n__isNatural(X)
   activate(n__natsFrom(X)) -> natsFrom(activate(X))
   activate(n__s(X)) -> s(activate(X))
   activate(n__isLNat(X)) -> isLNat(X)
   activate(n__nil()) -> nil()
   activate(n__afterNth(X1,X2)) -> afterNth(activate(X1),activate(X2))
   activate(n__cons(X1,X2)) -> cons(activate(X1),X2)
   activate(n__fst(X)) -> fst(activate(X))
   activate(n__snd(X)) -> snd(activate(X))
   activate(n__tail(X)) -> tail(activate(X))
   activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
   activate(n__0()) -> 0()
   activate(n__head(X)) -> head(activate(X))
   activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2))
   activate(n__pair(X1,X2)) -> pair(activate(X1),activate(X2))
   activate(n__splitAt(X1,X2)) -> splitAt(activate(X1),activate(X2))
   activate(n__and(X1,X2)) -> and(activate(X1),X2)
   activate(n__isNatural(X)) -> isNatural(X)
   activate(X) -> X
  TDG Processor:
   DPs:
    U101#(tt(),N,XS) -> activate#(XS)
    U101#(tt(),N,XS) -> activate#(N)
    U101#(tt(),N,XS) -> splitAt#(activate(N),activate(XS))
    U101#(tt(),N,XS) -> fst#(splitAt(activate(N),activate(XS)))
    U11#(tt(),N,XS) -> activate#(XS)
    U11#(tt(),N,XS) -> activate#(N)
    U11#(tt(),N,XS) -> splitAt#(activate(N),activate(XS))
    U11#(tt(),N,XS) -> snd#(splitAt(activate(N),activate(XS)))
    U21#(tt(),X) -> activate#(X)
    U31#(tt(),N) -> activate#(N)
    U41#(tt(),N) -> activate#(N)
    U41#(tt(),N) -> cons#(activate(N),n__natsFrom(n__s(activate(N))))
    U51#(tt(),N,XS) -> activate#(XS)
    U51#(tt(),N,XS) -> activate#(N)
    U51#(tt(),N,XS) -> afterNth#(activate(N),activate(XS))
    U51#(tt(),N,XS) -> head#(afterNth(activate(N),activate(XS)))
    U61#(tt(),Y) -> activate#(Y)
    U71#(tt(),XS) -> activate#(XS)
    U71#(tt(),XS) -> nil#()
    U71#(tt(),XS) -> pair#(nil(),activate(XS))
    U81#(tt(),N,X,XS) -> activate#(X)
    U81#(tt(),N,X,XS) -> activate#(XS)
    U81#(tt(),N,X,XS) -> activate#(N)
    U81#(tt(),N,X,XS) -> splitAt#(activate(N),activate(XS))
    U81#(tt(),N,X,XS) -> U82#(splitAt(activate(N),activate(XS)),activate(X))
    U82#(pair(YS,ZS),X) -> activate#(X)
    U82#(pair(YS,ZS),X) -> cons#(activate(X),YS)
    U82#(pair(YS,ZS),X) -> pair#(cons(activate(X),YS),ZS)
    U91#(tt(),XS) -> activate#(XS)
    afterNth#(N,XS) -> isNatural#(N)
    afterNth#(N,XS) -> and#(isNatural(N),n__isLNat(XS))
    afterNth#(N,XS) -> U11#(and(isNatural(N),n__isLNat(XS)),N,XS)
    and#(tt(),X) -> activate#(X)
    fst#(pair(X,Y)) -> isLNat#(X)
    fst#(pair(X,Y)) -> and#(isLNat(X),n__isLNat(Y))
    fst#(pair(X,Y)) -> U21#(and(isLNat(X),n__isLNat(Y)),X)
    head#(cons(N,XS)) -> activate#(XS)
    head#(cons(N,XS)) -> isNatural#(N)
    head#(cons(N,XS)) -> and#(isNatural(N),n__isLNat(activate(XS)))
    head#(cons(N,XS)) -> U31#(and(isNatural(N),n__isLNat(activate(XS))),N)
    isLNat#(n__afterNth(V1,V2)) -> activate#(V2)
    isLNat#(n__afterNth(V1,V2)) -> activate#(V1)
    isLNat#(n__afterNth(V1,V2)) -> isNatural#(activate(V1))
    isLNat#(n__afterNth(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2)))
    isLNat#(n__cons(V1,V2)) -> activate#(V2)
    isLNat#(n__cons(V1,V2)) -> activate#(V1)
    isLNat#(n__cons(V1,V2)) -> isNatural#(activate(V1))
    isLNat#(n__cons(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2)))
    isLNat#(n__fst(V1)) -> activate#(V1)
    isLNat#(n__fst(V1)) -> isPLNat#(activate(V1))
    isLNat#(n__natsFrom(V1)) -> activate#(V1)
    isLNat#(n__natsFrom(V1)) -> isNatural#(activate(V1))
    isLNat#(n__snd(V1)) -> activate#(V1)
    isLNat#(n__snd(V1)) -> isPLNat#(activate(V1))
    isLNat#(n__tail(V1)) -> activate#(V1)
    isLNat#(n__tail(V1)) -> isLNat#(activate(V1))
    isLNat#(n__take(V1,V2)) -> activate#(V2)
    isLNat#(n__take(V1,V2)) -> activate#(V1)
    isLNat#(n__take(V1,V2)) -> isNatural#(activate(V1))
    isLNat#(n__take(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2)))
    isNatural#(n__head(V1)) -> activate#(V1)
    isNatural#(n__head(V1)) -> isLNat#(activate(V1))
    isNatural#(n__s(V1)) -> activate#(V1)
    isNatural#(n__s(V1)) -> isNatural#(activate(V1))
    isNatural#(n__sel(V1,V2)) -> activate#(V2)
    isNatural#(n__sel(V1,V2)) -> activate#(V1)
    isNatural#(n__sel(V1,V2)) -> isNatural#(activate(V1))
    isNatural#(n__sel(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2)))
    isPLNat#(n__pair(V1,V2)) -> activate#(V2)
    isPLNat#(n__pair(V1,V2)) -> activate#(V1)
    isPLNat#(n__pair(V1,V2)) -> isLNat#(activate(V1))
    isPLNat#(n__pair(V1,V2)) -> and#(isLNat(activate(V1)),n__isLNat(activate(V2)))
    isPLNat#(n__splitAt(V1,V2)) -> activate#(V2)
    isPLNat#(n__splitAt(V1,V2)) -> activate#(V1)
    isPLNat#(n__splitAt(V1,V2)) -> isNatural#(activate(V1))
    isPLNat#(n__splitAt(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2)))
    natsFrom#(N) -> isNatural#(N)
    natsFrom#(N) -> U41#(isNatural(N),N)
    sel#(N,XS) -> isNatural#(N)
    sel#(N,XS) -> and#(isNatural(N),n__isLNat(XS))
    sel#(N,XS) -> U51#(and(isNatural(N),n__isLNat(XS)),N,XS)
    snd#(pair(X,Y)) -> isLNat#(X)
    snd#(pair(X,Y)) -> and#(isLNat(X),n__isLNat(Y))
    snd#(pair(X,Y)) -> U61#(and(isLNat(X),n__isLNat(Y)),Y)
    splitAt#(0(),XS) -> isLNat#(XS)
    splitAt#(0(),XS) -> U71#(isLNat(XS),XS)
    splitAt#(s(N),cons(X,XS)) -> activate#(XS)
    splitAt#(s(N),cons(X,XS)) -> isNatural#(N)
    splitAt#(s(N),cons(X,XS)) -> and#(isNatural(N),n__and(n__isNatural(X),n__isLNat(activate(XS))))
    splitAt#(s(N),cons(X,XS)) ->
    U81#(and(isNatural(N),n__and(n__isNatural(X),n__isLNat(activate(XS)))),N,X,activate(XS))
    tail#(cons(N,XS)) -> activate#(XS)
    tail#(cons(N,XS)) -> isNatural#(N)
    tail#(cons(N,XS)) -> and#(isNatural(N),n__isLNat(activate(XS)))
    tail#(cons(N,XS)) -> U91#(and(isNatural(N),n__isLNat(activate(XS))),activate(XS))
    take#(N,XS) -> isNatural#(N)
    take#(N,XS) -> and#(isNatural(N),n__isLNat(XS))
    take#(N,XS) -> U101#(and(isNatural(N),n__isLNat(XS)),N,XS)
    activate#(n__natsFrom(X)) -> activate#(X)
    activate#(n__natsFrom(X)) -> natsFrom#(activate(X))
    activate#(n__s(X)) -> activate#(X)
    activate#(n__s(X)) -> s#(activate(X))
    activate#(n__isLNat(X)) -> isLNat#(X)
    activate#(n__nil()) -> nil#()
    activate#(n__afterNth(X1,X2)) -> activate#(X2)
    activate#(n__afterNth(X1,X2)) -> activate#(X1)
    activate#(n__afterNth(X1,X2)) -> afterNth#(activate(X1),activate(X2))
    activate#(n__cons(X1,X2)) -> activate#(X1)
    activate#(n__cons(X1,X2)) -> cons#(activate(X1),X2)
    activate#(n__fst(X)) -> activate#(X)
    activate#(n__fst(X)) -> fst#(activate(X))
    activate#(n__snd(X)) -> activate#(X)
    activate#(n__snd(X)) -> snd#(activate(X))
    activate#(n__tail(X)) -> activate#(X)
    activate#(n__tail(X)) -> tail#(activate(X))
    activate#(n__take(X1,X2)) -> activate#(X2)
    activate#(n__take(X1,X2)) -> activate#(X1)
    activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2))
    activate#(n__0()) -> 0#()
    activate#(n__head(X)) -> activate#(X)
    activate#(n__head(X)) -> head#(activate(X))
    activate#(n__sel(X1,X2)) -> activate#(X2)
    activate#(n__sel(X1,X2)) -> activate#(X1)
    activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2))
    activate#(n__pair(X1,X2)) -> activate#(X2)
    activate#(n__pair(X1,X2)) -> activate#(X1)
    activate#(n__pair(X1,X2)) -> pair#(activate(X1),activate(X2))
    activate#(n__splitAt(X1,X2)) -> activate#(X2)
    activate#(n__splitAt(X1,X2)) -> activate#(X1)
    activate#(n__splitAt(X1,X2)) -> splitAt#(activate(X1),activate(X2))
    activate#(n__and(X1,X2)) -> activate#(X1)
    activate#(n__and(X1,X2)) -> and#(activate(X1),X2)
    activate#(n__isNatural(X)) -> isNatural#(X)
   TRS:
    U101(tt(),N,XS) -> fst(splitAt(activate(N),activate(XS)))
    U11(tt(),N,XS) -> snd(splitAt(activate(N),activate(XS)))
    U21(tt(),X) -> activate(X)
    U31(tt(),N) -> activate(N)
    U41(tt(),N) -> cons(activate(N),n__natsFrom(n__s(activate(N))))
    U51(tt(),N,XS) -> head(afterNth(activate(N),activate(XS)))
    U61(tt(),Y) -> activate(Y)
    U71(tt(),XS) -> pair(nil(),activate(XS))
    U81(tt(),N,X,XS) -> U82(splitAt(activate(N),activate(XS)),activate(X))
    U82(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS)
    U91(tt(),XS) -> activate(XS)
    afterNth(N,XS) -> U11(and(isNatural(N),n__isLNat(XS)),N,XS)
    and(tt(),X) -> activate(X)
    fst(pair(X,Y)) -> U21(and(isLNat(X),n__isLNat(Y)),X)
    head(cons(N,XS)) -> U31(and(isNatural(N),n__isLNat(activate(XS))),N)
    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__natsFrom(V1)) -> isNatural(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)))
    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)))
    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)
    sel(N,XS) -> U51(and(isNatural(N),n__isLNat(XS)),N,XS)
    snd(pair(X,Y)) -> U61(and(isLNat(X),n__isLNat(Y)),Y)
    splitAt(0(),XS) -> U71(isLNat(XS),XS)
    splitAt(s(N),cons(X,XS)) ->
    U81(and(isNatural(N),n__and(n__isNatural(X),n__isLNat(activate(XS)))),N,X,activate(XS))
    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)
    natsFrom(X) -> n__natsFrom(X)
    s(X) -> n__s(X)
    isLNat(X) -> n__isLNat(X)
    nil() -> n__nil()
    afterNth(X1,X2) -> n__afterNth(X1,X2)
    cons(X1,X2) -> n__cons(X1,X2)
    fst(X) -> n__fst(X)
    snd(X) -> n__snd(X)
    tail(X) -> n__tail(X)
    take(X1,X2) -> n__take(X1,X2)
    0() -> n__0()
    head(X) -> n__head(X)
    sel(X1,X2) -> n__sel(X1,X2)
    pair(X1,X2) -> n__pair(X1,X2)
    splitAt(X1,X2) -> n__splitAt(X1,X2)
    and(X1,X2) -> n__and(X1,X2)
    isNatural(X) -> n__isNatural(X)
    activate(n__natsFrom(X)) -> natsFrom(activate(X))
    activate(n__s(X)) -> s(activate(X))
    activate(n__isLNat(X)) -> isLNat(X)
    activate(n__nil()) -> nil()
    activate(n__afterNth(X1,X2)) -> afterNth(activate(X1),activate(X2))
    activate(n__cons(X1,X2)) -> cons(activate(X1),X2)
    activate(n__fst(X)) -> fst(activate(X))
    activate(n__snd(X)) -> snd(activate(X))
    activate(n__tail(X)) -> tail(activate(X))
    activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
    activate(n__0()) -> 0()
    activate(n__head(X)) -> head(activate(X))
    activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2))
    activate(n__pair(X1,X2)) -> pair(activate(X1),activate(X2))
    activate(n__splitAt(X1,X2)) -> splitAt(activate(X1),activate(X2))
    activate(n__and(X1,X2)) -> and(activate(X1),X2)
    activate(n__isNatural(X)) -> isNatural(X)
    activate(X) -> X
   graph:
    ...
   SCC Processor:
    #sccs: 1
    #rules: 122
    #arcs: 2342/17424
    DPs:
     take#(N,XS) -> and#(isNatural(N),n__isLNat(XS))
     and#(tt(),X) -> activate#(X)
     activate#(n__natsFrom(X)) -> activate#(X)
     activate#(n__natsFrom(X)) -> natsFrom#(activate(X))
     natsFrom#(N) -> isNatural#(N)
     isNatural#(n__head(V1)) -> activate#(V1)
     activate#(n__s(X)) -> activate#(X)
     activate#(n__isLNat(X)) -> isLNat#(X)
     isLNat#(n__afterNth(V1,V2)) -> activate#(V2)
     activate#(n__afterNth(X1,X2)) -> activate#(X2)
     activate#(n__afterNth(X1,X2)) -> activate#(X1)
     activate#(n__afterNth(X1,X2)) -> afterNth#(activate(X1),activate(X2))
     afterNth#(N,XS) -> isNatural#(N)
     isNatural#(n__head(V1)) -> isLNat#(activate(V1))
     isLNat#(n__afterNth(V1,V2)) -> activate#(V1)
     activate#(n__cons(X1,X2)) -> activate#(X1)
     activate#(n__fst(X)) -> activate#(X)
     activate#(n__fst(X)) -> fst#(activate(X))
     fst#(pair(X,Y)) -> isLNat#(X)
     isLNat#(n__afterNth(V1,V2)) -> isNatural#(activate(V1))
     isNatural#(n__s(V1)) -> activate#(V1)
     activate#(n__snd(X)) -> activate#(X)
     activate#(n__snd(X)) -> snd#(activate(X))
     snd#(pair(X,Y)) -> isLNat#(X)
     isLNat#(n__afterNth(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2)))
     isLNat#(n__cons(V1,V2)) -> activate#(V2)
     activate#(n__tail(X)) -> activate#(X)
     activate#(n__tail(X)) -> tail#(activate(X))
     tail#(cons(N,XS)) -> activate#(XS)
     activate#(n__take(X1,X2)) -> activate#(X2)
     activate#(n__take(X1,X2)) -> activate#(X1)
     activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2))
     take#(N,XS) -> isNatural#(N)
     isNatural#(n__s(V1)) -> isNatural#(activate(V1))
     isNatural#(n__sel(V1,V2)) -> activate#(V2)
     activate#(n__head(X)) -> activate#(X)
     activate#(n__head(X)) -> head#(activate(X))
     head#(cons(N,XS)) -> activate#(XS)
     activate#(n__sel(X1,X2)) -> activate#(X2)
     activate#(n__sel(X1,X2)) -> activate#(X1)
     activate#(n__sel(X1,X2)) -> sel#(activate(X1),activate(X2))
     sel#(N,XS) -> isNatural#(N)
     isNatural#(n__sel(V1,V2)) -> activate#(V1)
     activate#(n__pair(X1,X2)) -> activate#(X2)
     activate#(n__pair(X1,X2)) -> activate#(X1)
     activate#(n__splitAt(X1,X2)) -> activate#(X2)
     activate#(n__splitAt(X1,X2)) -> activate#(X1)
     activate#(n__splitAt(X1,X2)) -> splitAt#(activate(X1),activate(X2))
     splitAt#(0(),XS) -> isLNat#(XS)
     isLNat#(n__cons(V1,V2)) -> activate#(V1)
     activate#(n__and(X1,X2)) -> activate#(X1)
     activate#(n__and(X1,X2)) -> and#(activate(X1),X2)
     activate#(n__isNatural(X)) -> isNatural#(X)
     isNatural#(n__sel(V1,V2)) -> isNatural#(activate(V1))
     isNatural#(n__sel(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2)))
     isLNat#(n__cons(V1,V2)) -> isNatural#(activate(V1))
     isLNat#(n__cons(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2)))
     isLNat#(n__fst(V1)) -> activate#(V1)
     isLNat#(n__fst(V1)) -> isPLNat#(activate(V1))
     isPLNat#(n__pair(V1,V2)) -> activate#(V2)
     isPLNat#(n__pair(V1,V2)) -> activate#(V1)
     isPLNat#(n__pair(V1,V2)) -> isLNat#(activate(V1))
     isLNat#(n__natsFrom(V1)) -> activate#(V1)
     isLNat#(n__natsFrom(V1)) -> isNatural#(activate(V1))
     isLNat#(n__snd(V1)) -> activate#(V1)
     isLNat#(n__snd(V1)) -> isPLNat#(activate(V1))
     isPLNat#(n__pair(V1,V2)) -> and#(isLNat(activate(V1)),n__isLNat(activate(V2)))
     isPLNat#(n__splitAt(V1,V2)) -> activate#(V2)
     isPLNat#(n__splitAt(V1,V2)) -> activate#(V1)
     isPLNat#(n__splitAt(V1,V2)) -> isNatural#(activate(V1))
     isPLNat#(n__splitAt(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2)))
     isLNat#(n__tail(V1)) -> activate#(V1)
     isLNat#(n__tail(V1)) -> isLNat#(activate(V1))
     isLNat#(n__take(V1,V2)) -> activate#(V2)
     isLNat#(n__take(V1,V2)) -> activate#(V1)
     isLNat#(n__take(V1,V2)) -> isNatural#(activate(V1))
     isLNat#(n__take(V1,V2)) -> and#(isNatural(activate(V1)),n__isLNat(activate(V2)))
     splitAt#(0(),XS) -> U71#(isLNat(XS),XS)
     U71#(tt(),XS) -> activate#(XS)
     splitAt#(s(N),cons(X,XS)) -> activate#(XS)
     splitAt#(s(N),cons(X,XS)) -> isNatural#(N)
     splitAt#(s(N),cons(X,XS)) ->
     and#(isNatural(N),n__and(n__isNatural(X),n__isLNat(activate(XS))))
     splitAt#(s(N),cons(X,XS)) ->
     U81#(and(isNatural(N),n__and(n__isNatural(X),n__isLNat(activate(XS)))),N,X,activate(XS))
     U81#(tt(),N,X,XS) -> activate#(X)
     U81#(tt(),N,X,XS) -> activate#(XS)
     U81#(tt(),N,X,XS) -> activate#(N)
     U81#(tt(),N,X,XS) -> splitAt#(activate(N),activate(XS))
     U81#(tt(),N,X,XS) -> U82#(splitAt(activate(N),activate(XS)),activate(X))
     U82#(pair(YS,ZS),X) -> activate#(X)
     sel#(N,XS) -> and#(isNatural(N),n__isLNat(XS))
     sel#(N,XS) -> U51#(and(isNatural(N),n__isLNat(XS)),N,XS)
     U51#(tt(),N,XS) -> activate#(XS)
     U51#(tt(),N,XS) -> activate#(N)
     U51#(tt(),N,XS) -> afterNth#(activate(N),activate(XS))
     afterNth#(N,XS) -> and#(isNatural(N),n__isLNat(XS))
     afterNth#(N,XS) -> U11#(and(isNatural(N),n__isLNat(XS)),N,XS)
     U11#(tt(),N,XS) -> activate#(XS)
     U11#(tt(),N,XS) -> activate#(N)
     U11#(tt(),N,XS) -> splitAt#(activate(N),activate(XS))
     U11#(tt(),N,XS) -> snd#(splitAt(activate(N),activate(XS)))
     snd#(pair(X,Y)) -> and#(isLNat(X),n__isLNat(Y))
     snd#(pair(X,Y)) -> U61#(and(isLNat(X),n__isLNat(Y)),Y)
     U61#(tt(),Y) -> activate#(Y)
     U51#(tt(),N,XS) -> head#(afterNth(activate(N),activate(XS)))
     head#(cons(N,XS)) -> isNatural#(N)
     head#(cons(N,XS)) -> and#(isNatural(N),n__isLNat(activate(XS)))
     head#(cons(N,XS)) -> U31#(and(isNatural(N),n__isLNat(activate(XS))),N)
     U31#(tt(),N) -> activate#(N)
     take#(N,XS) -> U101#(and(isNatural(N),n__isLNat(XS)),N,XS)
     U101#(tt(),N,XS) -> activate#(XS)
     U101#(tt(),N,XS) -> activate#(N)
     U101#(tt(),N,XS) -> splitAt#(activate(N),activate(XS))
     U101#(tt(),N,XS) -> fst#(splitAt(activate(N),activate(XS)))
     fst#(pair(X,Y)) -> and#(isLNat(X),n__isLNat(Y))
     fst#(pair(X,Y)) -> U21#(and(isLNat(X),n__isLNat(Y)),X)
     U21#(tt(),X) -> activate#(X)
     tail#(cons(N,XS)) -> isNatural#(N)
     tail#(cons(N,XS)) -> and#(isNatural(N),n__isLNat(activate(XS)))
     tail#(cons(N,XS)) -> U91#(and(isNatural(N),n__isLNat(activate(XS))),activate(XS))
     U91#(tt(),XS) -> activate#(XS)
     natsFrom#(N) -> U41#(isNatural(N),N)
     U41#(tt(),N) -> activate#(N)
    TRS:
     U101(tt(),N,XS) -> fst(splitAt(activate(N),activate(XS)))
     U11(tt(),N,XS) -> snd(splitAt(activate(N),activate(XS)))
     U21(tt(),X) -> activate(X)
     U31(tt(),N) -> activate(N)
     U41(tt(),N) -> cons(activate(N),n__natsFrom(n__s(activate(N))))
     U51(tt(),N,XS) -> head(afterNth(activate(N),activate(XS)))
     U61(tt(),Y) -> activate(Y)
     U71(tt(),XS) -> pair(nil(),activate(XS))
     U81(tt(),N,X,XS) -> U82(splitAt(activate(N),activate(XS)),activate(X))
     U82(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS)
     U91(tt(),XS) -> activate(XS)
     afterNth(N,XS) -> U11(and(isNatural(N),n__isLNat(XS)),N,XS)
     and(tt(),X) -> activate(X)
     fst(pair(X,Y)) -> U21(and(isLNat(X),n__isLNat(Y)),X)
     head(cons(N,XS)) -> U31(and(isNatural(N),n__isLNat(activate(XS))),N)
     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__natsFrom(V1)) -> isNatural(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)))
     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)))
     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)
     sel(N,XS) -> U51(and(isNatural(N),n__isLNat(XS)),N,XS)
     snd(pair(X,Y)) -> U61(and(isLNat(X),n__isLNat(Y)),Y)
     splitAt(0(),XS) -> U71(isLNat(XS),XS)
     splitAt(s(N),cons(X,XS)) ->
     U81(and(isNatural(N),n__and(n__isNatural(X),n__isLNat(activate(XS)))),N,X,activate(XS))
     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)
     natsFrom(X) -> n__natsFrom(X)
     s(X) -> n__s(X)
     isLNat(X) -> n__isLNat(X)
     nil() -> n__nil()
     afterNth(X1,X2) -> n__afterNth(X1,X2)
     cons(X1,X2) -> n__cons(X1,X2)
     fst(X) -> n__fst(X)
     snd(X) -> n__snd(X)
     tail(X) -> n__tail(X)
     take(X1,X2) -> n__take(X1,X2)
     0() -> n__0()
     head(X) -> n__head(X)
     sel(X1,X2) -> n__sel(X1,X2)
     pair(X1,X2) -> n__pair(X1,X2)
     splitAt(X1,X2) -> n__splitAt(X1,X2)
     and(X1,X2) -> n__and(X1,X2)
     isNatural(X) -> n__isNatural(X)
     activate(n__natsFrom(X)) -> natsFrom(activate(X))
     activate(n__s(X)) -> s(activate(X))
     activate(n__isLNat(X)) -> isLNat(X)
     activate(n__nil()) -> nil()
     activate(n__afterNth(X1,X2)) -> afterNth(activate(X1),activate(X2))
     activate(n__cons(X1,X2)) -> cons(activate(X1),X2)
     activate(n__fst(X)) -> fst(activate(X))
     activate(n__snd(X)) -> snd(activate(X))
     activate(n__tail(X)) -> tail(activate(X))
     activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
     activate(n__0()) -> 0()
     activate(n__head(X)) -> head(activate(X))
     activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2))
     activate(n__pair(X1,X2)) -> pair(activate(X1),activate(X2))
     activate(n__splitAt(X1,X2)) -> splitAt(activate(X1),activate(X2))
     activate(n__and(X1,X2)) -> and(activate(X1),X2)
     activate(n__isNatural(X)) -> isNatural(X)
     activate(X) -> X
    Open