MAYBE

Problem:
 U101(tt(),V2) -> U102(isLNat(activate(V2)))
 U102(tt()) -> tt()
 U11(tt(),N,XS) -> U12(isLNat(activate(XS)),activate(N),activate(XS))
 U111(tt()) -> tt()
 U12(tt(),N,XS) -> snd(splitAt(activate(N),activate(XS)))
 U121(tt()) -> tt()
 U131(tt(),V2) -> U132(isLNat(activate(V2)))
 U132(tt()) -> tt()
 U141(tt(),V2) -> U142(isLNat(activate(V2)))
 U142(tt()) -> tt()
 U151(tt(),V2) -> U152(isLNat(activate(V2)))
 U152(tt()) -> tt()
 U161(tt(),N) -> cons(activate(N),n__natsFrom(n__s(activate(N))))
 U171(tt(),N,XS) -> U172(isLNat(activate(XS)),activate(N),activate(XS))
 U172(tt(),N,XS) -> head(afterNth(activate(N),activate(XS)))
 U181(tt(),Y) -> U182(isLNat(activate(Y)),activate(Y))
 U182(tt(),Y) -> activate(Y)
 U191(tt(),XS) -> pair(nil(),activate(XS))
 U201(tt(),N,X,XS) -> U202(isNatural(activate(X)),activate(N),activate(X),activate(XS))
 U202(tt(),N,X,XS) -> U203(isLNat(activate(XS)),activate(N),activate(X),activate(XS))
 U203(tt(),N,X,XS) -> U204(splitAt(activate(N),activate(XS)),activate(X))
 U204(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS)
 U21(tt(),X,Y) -> U22(isLNat(activate(Y)),activate(X))
 U211(tt(),XS) -> U212(isLNat(activate(XS)),activate(XS))
 U212(tt(),XS) -> activate(XS)
 U22(tt(),X) -> activate(X)
 U221(tt(),N,XS) -> U222(isLNat(activate(XS)),activate(N),activate(XS))
 U222(tt(),N,XS) -> fst(splitAt(activate(N),activate(XS)))
 U31(tt(),N,XS) -> U32(isLNat(activate(XS)),activate(N))
 U32(tt(),N) -> activate(N)
 U41(tt(),V2) -> U42(isLNat(activate(V2)))
 U42(tt()) -> tt()
 U51(tt(),V2) -> U52(isLNat(activate(V2)))
 U52(tt()) -> tt()
 U61(tt()) -> tt()
 U71(tt()) -> tt()
 U81(tt()) -> tt()
 U91(tt()) -> tt()
 afterNth(N,XS) -> U11(isNatural(N),N,XS)
 fst(pair(X,Y)) -> U21(isLNat(X),X,Y)
 head(cons(N,XS)) -> U31(isNatural(N),N,activate(XS))
 isLNat(n__nil()) -> tt()
 isLNat(n__afterNth(V1,V2)) -> U41(isNatural(activate(V1)),activate(V2))
 isLNat(n__cons(V1,V2)) -> U51(isNatural(activate(V1)),activate(V2))
 isLNat(n__fst(V1)) -> U61(isPLNat(activate(V1)))
 isLNat(n__natsFrom(V1)) -> U71(isNatural(activate(V1)))
 isLNat(n__snd(V1)) -> U81(isPLNat(activate(V1)))
 isLNat(n__tail(V1)) -> U91(isLNat(activate(V1)))
 isLNat(n__take(V1,V2)) -> U101(isNatural(activate(V1)),activate(V2))
 isNatural(n__0()) -> tt()
 isNatural(n__head(V1)) -> U111(isLNat(activate(V1)))
 isNatural(n__s(V1)) -> U121(isNatural(activate(V1)))
 isNatural(n__sel(V1,V2)) -> U131(isNatural(activate(V1)),activate(V2))
 isPLNat(n__pair(V1,V2)) -> U141(isLNat(activate(V1)),activate(V2))
 isPLNat(n__splitAt(V1,V2)) -> U151(isNatural(activate(V1)),activate(V2))
 natsFrom(N) -> U161(isNatural(N),N)
 sel(N,XS) -> U171(isNatural(N),N,XS)
 snd(pair(X,Y)) -> U181(isLNat(X),Y)
 splitAt(0(),XS) -> U191(isLNat(XS),XS)
 splitAt(s(N),cons(X,XS)) -> U201(isNatural(N),N,X,activate(XS))
 tail(cons(N,XS)) -> U211(isNatural(N),activate(XS))
 take(N,XS) -> U221(isNatural(N),N,XS)
 natsFrom(X) -> n__natsFrom(X)
 s(X) -> n__s(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)
 activate(n__natsFrom(X)) -> natsFrom(activate(X))
 activate(n__s(X)) -> s(activate(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(X) -> X

Proof:
 DP Processor:
  DPs:
   U101#(tt(),V2) -> activate#(V2)
   U101#(tt(),V2) -> isLNat#(activate(V2))
   U101#(tt(),V2) -> U102#(isLNat(activate(V2)))
   U11#(tt(),N,XS) -> activate#(N)
   U11#(tt(),N,XS) -> activate#(XS)
   U11#(tt(),N,XS) -> isLNat#(activate(XS))
   U11#(tt(),N,XS) -> U12#(isLNat(activate(XS)),activate(N),activate(XS))
   U12#(tt(),N,XS) -> activate#(XS)
   U12#(tt(),N,XS) -> activate#(N)
   U12#(tt(),N,XS) -> splitAt#(activate(N),activate(XS))
   U12#(tt(),N,XS) -> snd#(splitAt(activate(N),activate(XS)))
   U131#(tt(),V2) -> activate#(V2)
   U131#(tt(),V2) -> isLNat#(activate(V2))
   U131#(tt(),V2) -> U132#(isLNat(activate(V2)))
   U141#(tt(),V2) -> activate#(V2)
   U141#(tt(),V2) -> isLNat#(activate(V2))
   U141#(tt(),V2) -> U142#(isLNat(activate(V2)))
   U151#(tt(),V2) -> activate#(V2)
   U151#(tt(),V2) -> isLNat#(activate(V2))
   U151#(tt(),V2) -> U152#(isLNat(activate(V2)))
   U161#(tt(),N) -> activate#(N)
   U161#(tt(),N) -> cons#(activate(N),n__natsFrom(n__s(activate(N))))
   U171#(tt(),N,XS) -> activate#(N)
   U171#(tt(),N,XS) -> activate#(XS)
   U171#(tt(),N,XS) -> isLNat#(activate(XS))
   U171#(tt(),N,XS) -> U172#(isLNat(activate(XS)),activate(N),activate(XS))
   U172#(tt(),N,XS) -> activate#(XS)
   U172#(tt(),N,XS) -> activate#(N)
   U172#(tt(),N,XS) -> afterNth#(activate(N),activate(XS))
   U172#(tt(),N,XS) -> head#(afterNth(activate(N),activate(XS)))
   U181#(tt(),Y) -> activate#(Y)
   U181#(tt(),Y) -> isLNat#(activate(Y))
   U181#(tt(),Y) -> U182#(isLNat(activate(Y)),activate(Y))
   U182#(tt(),Y) -> activate#(Y)
   U191#(tt(),XS) -> activate#(XS)
   U191#(tt(),XS) -> nil#()
   U191#(tt(),XS) -> pair#(nil(),activate(XS))
   U201#(tt(),N,X,XS) -> activate#(XS)
   U201#(tt(),N,X,XS) -> activate#(N)
   U201#(tt(),N,X,XS) -> activate#(X)
   U201#(tt(),N,X,XS) -> isNatural#(activate(X))
   U201#(tt(),N,X,XS) -> U202#(isNatural(activate(X)),activate(N),activate(X),activate(XS))
   U202#(tt(),N,X,XS) -> activate#(X)
   U202#(tt(),N,X,XS) -> activate#(N)
   U202#(tt(),N,X,XS) -> activate#(XS)
   U202#(tt(),N,X,XS) -> isLNat#(activate(XS))
   U202#(tt(),N,X,XS) -> U203#(isLNat(activate(XS)),activate(N),activate(X),activate(XS))
   U203#(tt(),N,X,XS) -> activate#(X)
   U203#(tt(),N,X,XS) -> activate#(XS)
   U203#(tt(),N,X,XS) -> activate#(N)
   U203#(tt(),N,X,XS) -> splitAt#(activate(N),activate(XS))
   U203#(tt(),N,X,XS) -> U204#(splitAt(activate(N),activate(XS)),activate(X))
   U204#(pair(YS,ZS),X) -> activate#(X)
   U204#(pair(YS,ZS),X) -> cons#(activate(X),YS)
   U204#(pair(YS,ZS),X) -> pair#(cons(activate(X),YS),ZS)
   U21#(tt(),X,Y) -> activate#(X)
   U21#(tt(),X,Y) -> activate#(Y)
   U21#(tt(),X,Y) -> isLNat#(activate(Y))
   U21#(tt(),X,Y) -> U22#(isLNat(activate(Y)),activate(X))
   U211#(tt(),XS) -> activate#(XS)
   U211#(tt(),XS) -> isLNat#(activate(XS))
   U211#(tt(),XS) -> U212#(isLNat(activate(XS)),activate(XS))
   U212#(tt(),XS) -> activate#(XS)
   U22#(tt(),X) -> activate#(X)
   U221#(tt(),N,XS) -> activate#(N)
   U221#(tt(),N,XS) -> activate#(XS)
   U221#(tt(),N,XS) -> isLNat#(activate(XS))
   U221#(tt(),N,XS) -> U222#(isLNat(activate(XS)),activate(N),activate(XS))
   U222#(tt(),N,XS) -> activate#(XS)
   U222#(tt(),N,XS) -> activate#(N)
   U222#(tt(),N,XS) -> splitAt#(activate(N),activate(XS))
   U222#(tt(),N,XS) -> fst#(splitAt(activate(N),activate(XS)))
   U31#(tt(),N,XS) -> activate#(N)
   U31#(tt(),N,XS) -> activate#(XS)
   U31#(tt(),N,XS) -> isLNat#(activate(XS))
   U31#(tt(),N,XS) -> U32#(isLNat(activate(XS)),activate(N))
   U32#(tt(),N) -> activate#(N)
   U41#(tt(),V2) -> activate#(V2)
   U41#(tt(),V2) -> isLNat#(activate(V2))
   U41#(tt(),V2) -> U42#(isLNat(activate(V2)))
   U51#(tt(),V2) -> activate#(V2)
   U51#(tt(),V2) -> isLNat#(activate(V2))
   U51#(tt(),V2) -> U52#(isLNat(activate(V2)))
   afterNth#(N,XS) -> isNatural#(N)
   afterNth#(N,XS) -> U11#(isNatural(N),N,XS)
   fst#(pair(X,Y)) -> isLNat#(X)
   fst#(pair(X,Y)) -> U21#(isLNat(X),X,Y)
   head#(cons(N,XS)) -> activate#(XS)
   head#(cons(N,XS)) -> isNatural#(N)
   head#(cons(N,XS)) -> U31#(isNatural(N),N,activate(XS))
   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)) -> U41#(isNatural(activate(V1)),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)) -> U51#(isNatural(activate(V1)),activate(V2))
   isLNat#(n__fst(V1)) -> activate#(V1)
   isLNat#(n__fst(V1)) -> isPLNat#(activate(V1))
   isLNat#(n__fst(V1)) -> U61#(isPLNat(activate(V1)))
   isLNat#(n__natsFrom(V1)) -> activate#(V1)
   isLNat#(n__natsFrom(V1)) -> isNatural#(activate(V1))
   isLNat#(n__natsFrom(V1)) -> U71#(isNatural(activate(V1)))
   isLNat#(n__snd(V1)) -> activate#(V1)
   isLNat#(n__snd(V1)) -> isPLNat#(activate(V1))
   isLNat#(n__snd(V1)) -> U81#(isPLNat(activate(V1)))
   isLNat#(n__tail(V1)) -> activate#(V1)
   isLNat#(n__tail(V1)) -> isLNat#(activate(V1))
   isLNat#(n__tail(V1)) -> U91#(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)) -> U101#(isNatural(activate(V1)),activate(V2))
   isNatural#(n__head(V1)) -> activate#(V1)
   isNatural#(n__head(V1)) -> isLNat#(activate(V1))
   isNatural#(n__head(V1)) -> U111#(isLNat(activate(V1)))
   isNatural#(n__s(V1)) -> activate#(V1)
   isNatural#(n__s(V1)) -> isNatural#(activate(V1))
   isNatural#(n__s(V1)) -> U121#(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)) -> U131#(isNatural(activate(V1)),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)) -> U141#(isLNat(activate(V1)),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)) -> U151#(isNatural(activate(V1)),activate(V2))
   natsFrom#(N) -> isNatural#(N)
   natsFrom#(N) -> U161#(isNatural(N),N)
   sel#(N,XS) -> isNatural#(N)
   sel#(N,XS) -> U171#(isNatural(N),N,XS)
   snd#(pair(X,Y)) -> isLNat#(X)
   snd#(pair(X,Y)) -> U181#(isLNat(X),Y)
   splitAt#(0(),XS) -> isLNat#(XS)
   splitAt#(0(),XS) -> U191#(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)) -> U201#(isNatural(N),N,X,activate(XS))
   tail#(cons(N,XS)) -> activate#(XS)
   tail#(cons(N,XS)) -> isNatural#(N)
   tail#(cons(N,XS)) -> U211#(isNatural(N),activate(XS))
   take#(N,XS) -> isNatural#(N)
   take#(N,XS) -> U221#(isNatural(N),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__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))
  TRS:
   U101(tt(),V2) -> U102(isLNat(activate(V2)))
   U102(tt()) -> tt()
   U11(tt(),N,XS) -> U12(isLNat(activate(XS)),activate(N),activate(XS))
   U111(tt()) -> tt()
   U12(tt(),N,XS) -> snd(splitAt(activate(N),activate(XS)))
   U121(tt()) -> tt()
   U131(tt(),V2) -> U132(isLNat(activate(V2)))
   U132(tt()) -> tt()
   U141(tt(),V2) -> U142(isLNat(activate(V2)))
   U142(tt()) -> tt()
   U151(tt(),V2) -> U152(isLNat(activate(V2)))
   U152(tt()) -> tt()
   U161(tt(),N) -> cons(activate(N),n__natsFrom(n__s(activate(N))))
   U171(tt(),N,XS) -> U172(isLNat(activate(XS)),activate(N),activate(XS))
   U172(tt(),N,XS) -> head(afterNth(activate(N),activate(XS)))
   U181(tt(),Y) -> U182(isLNat(activate(Y)),activate(Y))
   U182(tt(),Y) -> activate(Y)
   U191(tt(),XS) -> pair(nil(),activate(XS))
   U201(tt(),N,X,XS) -> U202(isNatural(activate(X)),activate(N),activate(X),activate(XS))
   U202(tt(),N,X,XS) -> U203(isLNat(activate(XS)),activate(N),activate(X),activate(XS))
   U203(tt(),N,X,XS) -> U204(splitAt(activate(N),activate(XS)),activate(X))
   U204(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS)
   U21(tt(),X,Y) -> U22(isLNat(activate(Y)),activate(X))
   U211(tt(),XS) -> U212(isLNat(activate(XS)),activate(XS))
   U212(tt(),XS) -> activate(XS)
   U22(tt(),X) -> activate(X)
   U221(tt(),N,XS) -> U222(isLNat(activate(XS)),activate(N),activate(XS))
   U222(tt(),N,XS) -> fst(splitAt(activate(N),activate(XS)))
   U31(tt(),N,XS) -> U32(isLNat(activate(XS)),activate(N))
   U32(tt(),N) -> activate(N)
   U41(tt(),V2) -> U42(isLNat(activate(V2)))
   U42(tt()) -> tt()
   U51(tt(),V2) -> U52(isLNat(activate(V2)))
   U52(tt()) -> tt()
   U61(tt()) -> tt()
   U71(tt()) -> tt()
   U81(tt()) -> tt()
   U91(tt()) -> tt()
   afterNth(N,XS) -> U11(isNatural(N),N,XS)
   fst(pair(X,Y)) -> U21(isLNat(X),X,Y)
   head(cons(N,XS)) -> U31(isNatural(N),N,activate(XS))
   isLNat(n__nil()) -> tt()
   isLNat(n__afterNth(V1,V2)) -> U41(isNatural(activate(V1)),activate(V2))
   isLNat(n__cons(V1,V2)) -> U51(isNatural(activate(V1)),activate(V2))
   isLNat(n__fst(V1)) -> U61(isPLNat(activate(V1)))
   isLNat(n__natsFrom(V1)) -> U71(isNatural(activate(V1)))
   isLNat(n__snd(V1)) -> U81(isPLNat(activate(V1)))
   isLNat(n__tail(V1)) -> U91(isLNat(activate(V1)))
   isLNat(n__take(V1,V2)) -> U101(isNatural(activate(V1)),activate(V2))
   isNatural(n__0()) -> tt()
   isNatural(n__head(V1)) -> U111(isLNat(activate(V1)))
   isNatural(n__s(V1)) -> U121(isNatural(activate(V1)))
   isNatural(n__sel(V1,V2)) -> U131(isNatural(activate(V1)),activate(V2))
   isPLNat(n__pair(V1,V2)) -> U141(isLNat(activate(V1)),activate(V2))
   isPLNat(n__splitAt(V1,V2)) -> U151(isNatural(activate(V1)),activate(V2))
   natsFrom(N) -> U161(isNatural(N),N)
   sel(N,XS) -> U171(isNatural(N),N,XS)
   snd(pair(X,Y)) -> U181(isLNat(X),Y)
   splitAt(0(),XS) -> U191(isLNat(XS),XS)
   splitAt(s(N),cons(X,XS)) -> U201(isNatural(N),N,X,activate(XS))
   tail(cons(N,XS)) -> U211(isNatural(N),activate(XS))
   take(N,XS) -> U221(isNatural(N),N,XS)
   natsFrom(X) -> n__natsFrom(X)
   s(X) -> n__s(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)
   activate(n__natsFrom(X)) -> natsFrom(activate(X))
   activate(n__s(X)) -> s(activate(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(X) -> X
  TDG Processor:
   DPs:
    U101#(tt(),V2) -> activate#(V2)
    U101#(tt(),V2) -> isLNat#(activate(V2))
    U101#(tt(),V2) -> U102#(isLNat(activate(V2)))
    U11#(tt(),N,XS) -> activate#(N)
    U11#(tt(),N,XS) -> activate#(XS)
    U11#(tt(),N,XS) -> isLNat#(activate(XS))
    U11#(tt(),N,XS) -> U12#(isLNat(activate(XS)),activate(N),activate(XS))
    U12#(tt(),N,XS) -> activate#(XS)
    U12#(tt(),N,XS) -> activate#(N)
    U12#(tt(),N,XS) -> splitAt#(activate(N),activate(XS))
    U12#(tt(),N,XS) -> snd#(splitAt(activate(N),activate(XS)))
    U131#(tt(),V2) -> activate#(V2)
    U131#(tt(),V2) -> isLNat#(activate(V2))
    U131#(tt(),V2) -> U132#(isLNat(activate(V2)))
    U141#(tt(),V2) -> activate#(V2)
    U141#(tt(),V2) -> isLNat#(activate(V2))
    U141#(tt(),V2) -> U142#(isLNat(activate(V2)))
    U151#(tt(),V2) -> activate#(V2)
    U151#(tt(),V2) -> isLNat#(activate(V2))
    U151#(tt(),V2) -> U152#(isLNat(activate(V2)))
    U161#(tt(),N) -> activate#(N)
    U161#(tt(),N) -> cons#(activate(N),n__natsFrom(n__s(activate(N))))
    U171#(tt(),N,XS) -> activate#(N)
    U171#(tt(),N,XS) -> activate#(XS)
    U171#(tt(),N,XS) -> isLNat#(activate(XS))
    U171#(tt(),N,XS) -> U172#(isLNat(activate(XS)),activate(N),activate(XS))
    U172#(tt(),N,XS) -> activate#(XS)
    U172#(tt(),N,XS) -> activate#(N)
    U172#(tt(),N,XS) -> afterNth#(activate(N),activate(XS))
    U172#(tt(),N,XS) -> head#(afterNth(activate(N),activate(XS)))
    U181#(tt(),Y) -> activate#(Y)
    U181#(tt(),Y) -> isLNat#(activate(Y))
    U181#(tt(),Y) -> U182#(isLNat(activate(Y)),activate(Y))
    U182#(tt(),Y) -> activate#(Y)
    U191#(tt(),XS) -> activate#(XS)
    U191#(tt(),XS) -> nil#()
    U191#(tt(),XS) -> pair#(nil(),activate(XS))
    U201#(tt(),N,X,XS) -> activate#(XS)
    U201#(tt(),N,X,XS) -> activate#(N)
    U201#(tt(),N,X,XS) -> activate#(X)
    U201#(tt(),N,X,XS) -> isNatural#(activate(X))
    U201#(tt(),N,X,XS) -> U202#(isNatural(activate(X)),activate(N),activate(X),activate(XS))
    U202#(tt(),N,X,XS) -> activate#(X)
    U202#(tt(),N,X,XS) -> activate#(N)
    U202#(tt(),N,X,XS) -> activate#(XS)
    U202#(tt(),N,X,XS) -> isLNat#(activate(XS))
    U202#(tt(),N,X,XS) -> U203#(isLNat(activate(XS)),activate(N),activate(X),activate(XS))
    U203#(tt(),N,X,XS) -> activate#(X)
    U203#(tt(),N,X,XS) -> activate#(XS)
    U203#(tt(),N,X,XS) -> activate#(N)
    U203#(tt(),N,X,XS) -> splitAt#(activate(N),activate(XS))
    U203#(tt(),N,X,XS) -> U204#(splitAt(activate(N),activate(XS)),activate(X))
    U204#(pair(YS,ZS),X) -> activate#(X)
    U204#(pair(YS,ZS),X) -> cons#(activate(X),YS)
    U204#(pair(YS,ZS),X) -> pair#(cons(activate(X),YS),ZS)
    U21#(tt(),X,Y) -> activate#(X)
    U21#(tt(),X,Y) -> activate#(Y)
    U21#(tt(),X,Y) -> isLNat#(activate(Y))
    U21#(tt(),X,Y) -> U22#(isLNat(activate(Y)),activate(X))
    U211#(tt(),XS) -> activate#(XS)
    U211#(tt(),XS) -> isLNat#(activate(XS))
    U211#(tt(),XS) -> U212#(isLNat(activate(XS)),activate(XS))
    U212#(tt(),XS) -> activate#(XS)
    U22#(tt(),X) -> activate#(X)
    U221#(tt(),N,XS) -> activate#(N)
    U221#(tt(),N,XS) -> activate#(XS)
    U221#(tt(),N,XS) -> isLNat#(activate(XS))
    U221#(tt(),N,XS) -> U222#(isLNat(activate(XS)),activate(N),activate(XS))
    U222#(tt(),N,XS) -> activate#(XS)
    U222#(tt(),N,XS) -> activate#(N)
    U222#(tt(),N,XS) -> splitAt#(activate(N),activate(XS))
    U222#(tt(),N,XS) -> fst#(splitAt(activate(N),activate(XS)))
    U31#(tt(),N,XS) -> activate#(N)
    U31#(tt(),N,XS) -> activate#(XS)
    U31#(tt(),N,XS) -> isLNat#(activate(XS))
    U31#(tt(),N,XS) -> U32#(isLNat(activate(XS)),activate(N))
    U32#(tt(),N) -> activate#(N)
    U41#(tt(),V2) -> activate#(V2)
    U41#(tt(),V2) -> isLNat#(activate(V2))
    U41#(tt(),V2) -> U42#(isLNat(activate(V2)))
    U51#(tt(),V2) -> activate#(V2)
    U51#(tt(),V2) -> isLNat#(activate(V2))
    U51#(tt(),V2) -> U52#(isLNat(activate(V2)))
    afterNth#(N,XS) -> isNatural#(N)
    afterNth#(N,XS) -> U11#(isNatural(N),N,XS)
    fst#(pair(X,Y)) -> isLNat#(X)
    fst#(pair(X,Y)) -> U21#(isLNat(X),X,Y)
    head#(cons(N,XS)) -> activate#(XS)
    head#(cons(N,XS)) -> isNatural#(N)
    head#(cons(N,XS)) -> U31#(isNatural(N),N,activate(XS))
    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)) -> U41#(isNatural(activate(V1)),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)) -> U51#(isNatural(activate(V1)),activate(V2))
    isLNat#(n__fst(V1)) -> activate#(V1)
    isLNat#(n__fst(V1)) -> isPLNat#(activate(V1))
    isLNat#(n__fst(V1)) -> U61#(isPLNat(activate(V1)))
    isLNat#(n__natsFrom(V1)) -> activate#(V1)
    isLNat#(n__natsFrom(V1)) -> isNatural#(activate(V1))
    isLNat#(n__natsFrom(V1)) -> U71#(isNatural(activate(V1)))
    isLNat#(n__snd(V1)) -> activate#(V1)
    isLNat#(n__snd(V1)) -> isPLNat#(activate(V1))
    isLNat#(n__snd(V1)) -> U81#(isPLNat(activate(V1)))
    isLNat#(n__tail(V1)) -> activate#(V1)
    isLNat#(n__tail(V1)) -> isLNat#(activate(V1))
    isLNat#(n__tail(V1)) -> U91#(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)) -> U101#(isNatural(activate(V1)),activate(V2))
    isNatural#(n__head(V1)) -> activate#(V1)
    isNatural#(n__head(V1)) -> isLNat#(activate(V1))
    isNatural#(n__head(V1)) -> U111#(isLNat(activate(V1)))
    isNatural#(n__s(V1)) -> activate#(V1)
    isNatural#(n__s(V1)) -> isNatural#(activate(V1))
    isNatural#(n__s(V1)) -> U121#(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)) -> U131#(isNatural(activate(V1)),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)) -> U141#(isLNat(activate(V1)),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)) -> U151#(isNatural(activate(V1)),activate(V2))
    natsFrom#(N) -> isNatural#(N)
    natsFrom#(N) -> U161#(isNatural(N),N)
    sel#(N,XS) -> isNatural#(N)
    sel#(N,XS) -> U171#(isNatural(N),N,XS)
    snd#(pair(X,Y)) -> isLNat#(X)
    snd#(pair(X,Y)) -> U181#(isLNat(X),Y)
    splitAt#(0(),XS) -> isLNat#(XS)
    splitAt#(0(),XS) -> U191#(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)) -> U201#(isNatural(N),N,X,activate(XS))
    tail#(cons(N,XS)) -> activate#(XS)
    tail#(cons(N,XS)) -> isNatural#(N)
    tail#(cons(N,XS)) -> U211#(isNatural(N),activate(XS))
    take#(N,XS) -> isNatural#(N)
    take#(N,XS) -> U221#(isNatural(N),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__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))
   TRS:
    U101(tt(),V2) -> U102(isLNat(activate(V2)))
    U102(tt()) -> tt()
    U11(tt(),N,XS) -> U12(isLNat(activate(XS)),activate(N),activate(XS))
    U111(tt()) -> tt()
    U12(tt(),N,XS) -> snd(splitAt(activate(N),activate(XS)))
    U121(tt()) -> tt()
    U131(tt(),V2) -> U132(isLNat(activate(V2)))
    U132(tt()) -> tt()
    U141(tt(),V2) -> U142(isLNat(activate(V2)))
    U142(tt()) -> tt()
    U151(tt(),V2) -> U152(isLNat(activate(V2)))
    U152(tt()) -> tt()
    U161(tt(),N) -> cons(activate(N),n__natsFrom(n__s(activate(N))))
    U171(tt(),N,XS) -> U172(isLNat(activate(XS)),activate(N),activate(XS))
    U172(tt(),N,XS) -> head(afterNth(activate(N),activate(XS)))
    U181(tt(),Y) -> U182(isLNat(activate(Y)),activate(Y))
    U182(tt(),Y) -> activate(Y)
    U191(tt(),XS) -> pair(nil(),activate(XS))
    U201(tt(),N,X,XS) -> U202(isNatural(activate(X)),activate(N),activate(X),activate(XS))
    U202(tt(),N,X,XS) -> U203(isLNat(activate(XS)),activate(N),activate(X),activate(XS))
    U203(tt(),N,X,XS) -> U204(splitAt(activate(N),activate(XS)),activate(X))
    U204(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS)
    U21(tt(),X,Y) -> U22(isLNat(activate(Y)),activate(X))
    U211(tt(),XS) -> U212(isLNat(activate(XS)),activate(XS))
    U212(tt(),XS) -> activate(XS)
    U22(tt(),X) -> activate(X)
    U221(tt(),N,XS) -> U222(isLNat(activate(XS)),activate(N),activate(XS))
    U222(tt(),N,XS) -> fst(splitAt(activate(N),activate(XS)))
    U31(tt(),N,XS) -> U32(isLNat(activate(XS)),activate(N))
    U32(tt(),N) -> activate(N)
    U41(tt(),V2) -> U42(isLNat(activate(V2)))
    U42(tt()) -> tt()
    U51(tt(),V2) -> U52(isLNat(activate(V2)))
    U52(tt()) -> tt()
    U61(tt()) -> tt()
    U71(tt()) -> tt()
    U81(tt()) -> tt()
    U91(tt()) -> tt()
    afterNth(N,XS) -> U11(isNatural(N),N,XS)
    fst(pair(X,Y)) -> U21(isLNat(X),X,Y)
    head(cons(N,XS)) -> U31(isNatural(N),N,activate(XS))
    isLNat(n__nil()) -> tt()
    isLNat(n__afterNth(V1,V2)) -> U41(isNatural(activate(V1)),activate(V2))
    isLNat(n__cons(V1,V2)) -> U51(isNatural(activate(V1)),activate(V2))
    isLNat(n__fst(V1)) -> U61(isPLNat(activate(V1)))
    isLNat(n__natsFrom(V1)) -> U71(isNatural(activate(V1)))
    isLNat(n__snd(V1)) -> U81(isPLNat(activate(V1)))
    isLNat(n__tail(V1)) -> U91(isLNat(activate(V1)))
    isLNat(n__take(V1,V2)) -> U101(isNatural(activate(V1)),activate(V2))
    isNatural(n__0()) -> tt()
    isNatural(n__head(V1)) -> U111(isLNat(activate(V1)))
    isNatural(n__s(V1)) -> U121(isNatural(activate(V1)))
    isNatural(n__sel(V1,V2)) -> U131(isNatural(activate(V1)),activate(V2))
    isPLNat(n__pair(V1,V2)) -> U141(isLNat(activate(V1)),activate(V2))
    isPLNat(n__splitAt(V1,V2)) -> U151(isNatural(activate(V1)),activate(V2))
    natsFrom(N) -> U161(isNatural(N),N)
    sel(N,XS) -> U171(isNatural(N),N,XS)
    snd(pair(X,Y)) -> U181(isLNat(X),Y)
    splitAt(0(),XS) -> U191(isLNat(XS),XS)
    splitAt(s(N),cons(X,XS)) -> U201(isNatural(N),N,X,activate(XS))
    tail(cons(N,XS)) -> U211(isNatural(N),activate(XS))
    take(N,XS) -> U221(isNatural(N),N,XS)
    natsFrom(X) -> n__natsFrom(X)
    s(X) -> n__s(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)
    activate(n__natsFrom(X)) -> natsFrom(activate(X))
    activate(n__s(X)) -> s(activate(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(X) -> X
   graph:
    ...
   SCC Processor:
    #sccs: 1
    #rules: 157
    #arcs: 3194/32041
    DPs:
     take#(N,XS) -> U221#(isNatural(N),N,XS)
     U221#(tt(),N,XS) -> activate#(N)
     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__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#(V2)
     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)) -> 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)) -> isNatural#(activate(V1))
     isNatural#(n__s(V1)) -> activate#(V1)
     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__afterNth(V1,V2)) -> U41#(isNatural(activate(V1)),activate(V2))
     U41#(tt(),V2) -> activate#(V2)
     U41#(tt(),V2) -> 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))
     isNatural#(n__sel(V1,V2)) -> isNatural#(activate(V1))
     isNatural#(n__sel(V1,V2)) -> U131#(isNatural(activate(V1)),activate(V2))
     U131#(tt(),V2) -> activate#(V2)
     U131#(tt(),V2) -> isLNat#(activate(V2))
     isLNat#(n__cons(V1,V2)) -> U51#(isNatural(activate(V1)),activate(V2))
     U51#(tt(),V2) -> activate#(V2)
     U51#(tt(),V2) -> 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)) -> U141#(isLNat(activate(V1)),activate(V2))
     U141#(tt(),V2) -> activate#(V2)
     U141#(tt(),V2) -> 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)) -> U101#(isNatural(activate(V1)),activate(V2))
     U101#(tt(),V2) -> activate#(V2)
     U101#(tt(),V2) -> 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)) -> U151#(isNatural(activate(V1)),activate(V2))
     U151#(tt(),V2) -> activate#(V2)
     U151#(tt(),V2) -> isLNat#(activate(V2))
     splitAt#(0(),XS) -> U191#(isLNat(XS),XS)
     U191#(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)) -> U201#(isNatural(N),N,X,activate(XS))
     U201#(tt(),N,X,XS) -> activate#(XS)
     U201#(tt(),N,X,XS) -> activate#(N)
     U201#(tt(),N,X,XS) -> activate#(X)
     U201#(tt(),N,X,XS) -> isNatural#(activate(X))
     U201#(tt(),N,X,XS) -> U202#(isNatural(activate(X)),activate(N),activate(X),activate(XS))
     U202#(tt(),N,X,XS) -> activate#(X)
     U202#(tt(),N,X,XS) -> activate#(N)
     U202#(tt(),N,X,XS) -> activate#(XS)
     U202#(tt(),N,X,XS) -> isLNat#(activate(XS))
     U202#(tt(),N,X,XS) -> U203#(isLNat(activate(XS)),activate(N),activate(X),activate(XS))
     U203#(tt(),N,X,XS) -> activate#(X)
     U203#(tt(),N,X,XS) -> activate#(XS)
     U203#(tt(),N,X,XS) -> activate#(N)
     U203#(tt(),N,X,XS) -> splitAt#(activate(N),activate(XS))
     U203#(tt(),N,X,XS) -> U204#(splitAt(activate(N),activate(XS)),activate(X))
     U204#(pair(YS,ZS),X) -> activate#(X)
     sel#(N,XS) -> U171#(isNatural(N),N,XS)
     U171#(tt(),N,XS) -> activate#(N)
     U171#(tt(),N,XS) -> activate#(XS)
     U171#(tt(),N,XS) -> isLNat#(activate(XS))
     U171#(tt(),N,XS) -> U172#(isLNat(activate(XS)),activate(N),activate(XS))
     U172#(tt(),N,XS) -> activate#(XS)
     U172#(tt(),N,XS) -> activate#(N)
     U172#(tt(),N,XS) -> afterNth#(activate(N),activate(XS))
     afterNth#(N,XS) -> U11#(isNatural(N),N,XS)
     U11#(tt(),N,XS) -> activate#(N)
     U11#(tt(),N,XS) -> activate#(XS)
     U11#(tt(),N,XS) -> isLNat#(activate(XS))
     U11#(tt(),N,XS) -> U12#(isLNat(activate(XS)),activate(N),activate(XS))
     U12#(tt(),N,XS) -> activate#(XS)
     U12#(tt(),N,XS) -> activate#(N)
     U12#(tt(),N,XS) -> splitAt#(activate(N),activate(XS))
     U12#(tt(),N,XS) -> snd#(splitAt(activate(N),activate(XS)))
     snd#(pair(X,Y)) -> U181#(isLNat(X),Y)
     U181#(tt(),Y) -> activate#(Y)
     U181#(tt(),Y) -> isLNat#(activate(Y))
     U181#(tt(),Y) -> U182#(isLNat(activate(Y)),activate(Y))
     U182#(tt(),Y) -> activate#(Y)
     U172#(tt(),N,XS) -> head#(afterNth(activate(N),activate(XS)))
     head#(cons(N,XS)) -> isNatural#(N)
     head#(cons(N,XS)) -> U31#(isNatural(N),N,activate(XS))
     U31#(tt(),N,XS) -> activate#(N)
     U31#(tt(),N,XS) -> activate#(XS)
     U31#(tt(),N,XS) -> isLNat#(activate(XS))
     U31#(tt(),N,XS) -> U32#(isLNat(activate(XS)),activate(N))
     U32#(tt(),N) -> activate#(N)
     tail#(cons(N,XS)) -> isNatural#(N)
     tail#(cons(N,XS)) -> U211#(isNatural(N),activate(XS))
     U211#(tt(),XS) -> activate#(XS)
     U211#(tt(),XS) -> isLNat#(activate(XS))
     U211#(tt(),XS) -> U212#(isLNat(activate(XS)),activate(XS))
     U212#(tt(),XS) -> activate#(XS)
     fst#(pair(X,Y)) -> U21#(isLNat(X),X,Y)
     U21#(tt(),X,Y) -> activate#(X)
     U21#(tt(),X,Y) -> activate#(Y)
     U21#(tt(),X,Y) -> isLNat#(activate(Y))
     U21#(tt(),X,Y) -> U22#(isLNat(activate(Y)),activate(X))
     U22#(tt(),X) -> activate#(X)
     natsFrom#(N) -> U161#(isNatural(N),N)
     U161#(tt(),N) -> activate#(N)
     U221#(tt(),N,XS) -> activate#(XS)
     U221#(tt(),N,XS) -> isLNat#(activate(XS))
     U221#(tt(),N,XS) -> U222#(isLNat(activate(XS)),activate(N),activate(XS))
     U222#(tt(),N,XS) -> activate#(XS)
     U222#(tt(),N,XS) -> activate#(N)
     U222#(tt(),N,XS) -> splitAt#(activate(N),activate(XS))
     U222#(tt(),N,XS) -> fst#(splitAt(activate(N),activate(XS)))
    TRS:
     U101(tt(),V2) -> U102(isLNat(activate(V2)))
     U102(tt()) -> tt()
     U11(tt(),N,XS) -> U12(isLNat(activate(XS)),activate(N),activate(XS))
     U111(tt()) -> tt()
     U12(tt(),N,XS) -> snd(splitAt(activate(N),activate(XS)))
     U121(tt()) -> tt()
     U131(tt(),V2) -> U132(isLNat(activate(V2)))
     U132(tt()) -> tt()
     U141(tt(),V2) -> U142(isLNat(activate(V2)))
     U142(tt()) -> tt()
     U151(tt(),V2) -> U152(isLNat(activate(V2)))
     U152(tt()) -> tt()
     U161(tt(),N) -> cons(activate(N),n__natsFrom(n__s(activate(N))))
     U171(tt(),N,XS) -> U172(isLNat(activate(XS)),activate(N),activate(XS))
     U172(tt(),N,XS) -> head(afterNth(activate(N),activate(XS)))
     U181(tt(),Y) -> U182(isLNat(activate(Y)),activate(Y))
     U182(tt(),Y) -> activate(Y)
     U191(tt(),XS) -> pair(nil(),activate(XS))
     U201(tt(),N,X,XS) -> U202(isNatural(activate(X)),activate(N),activate(X),activate(XS))
     U202(tt(),N,X,XS) -> U203(isLNat(activate(XS)),activate(N),activate(X),activate(XS))
     U203(tt(),N,X,XS) -> U204(splitAt(activate(N),activate(XS)),activate(X))
     U204(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS)
     U21(tt(),X,Y) -> U22(isLNat(activate(Y)),activate(X))
     U211(tt(),XS) -> U212(isLNat(activate(XS)),activate(XS))
     U212(tt(),XS) -> activate(XS)
     U22(tt(),X) -> activate(X)
     U221(tt(),N,XS) -> U222(isLNat(activate(XS)),activate(N),activate(XS))
     U222(tt(),N,XS) -> fst(splitAt(activate(N),activate(XS)))
     U31(tt(),N,XS) -> U32(isLNat(activate(XS)),activate(N))
     U32(tt(),N) -> activate(N)
     U41(tt(),V2) -> U42(isLNat(activate(V2)))
     U42(tt()) -> tt()
     U51(tt(),V2) -> U52(isLNat(activate(V2)))
     U52(tt()) -> tt()
     U61(tt()) -> tt()
     U71(tt()) -> tt()
     U81(tt()) -> tt()
     U91(tt()) -> tt()
     afterNth(N,XS) -> U11(isNatural(N),N,XS)
     fst(pair(X,Y)) -> U21(isLNat(X),X,Y)
     head(cons(N,XS)) -> U31(isNatural(N),N,activate(XS))
     isLNat(n__nil()) -> tt()
     isLNat(n__afterNth(V1,V2)) -> U41(isNatural(activate(V1)),activate(V2))
     isLNat(n__cons(V1,V2)) -> U51(isNatural(activate(V1)),activate(V2))
     isLNat(n__fst(V1)) -> U61(isPLNat(activate(V1)))
     isLNat(n__natsFrom(V1)) -> U71(isNatural(activate(V1)))
     isLNat(n__snd(V1)) -> U81(isPLNat(activate(V1)))
     isLNat(n__tail(V1)) -> U91(isLNat(activate(V1)))
     isLNat(n__take(V1,V2)) -> U101(isNatural(activate(V1)),activate(V2))
     isNatural(n__0()) -> tt()
     isNatural(n__head(V1)) -> U111(isLNat(activate(V1)))
     isNatural(n__s(V1)) -> U121(isNatural(activate(V1)))
     isNatural(n__sel(V1,V2)) -> U131(isNatural(activate(V1)),activate(V2))
     isPLNat(n__pair(V1,V2)) -> U141(isLNat(activate(V1)),activate(V2))
     isPLNat(n__splitAt(V1,V2)) -> U151(isNatural(activate(V1)),activate(V2))
     natsFrom(N) -> U161(isNatural(N),N)
     sel(N,XS) -> U171(isNatural(N),N,XS)
     snd(pair(X,Y)) -> U181(isLNat(X),Y)
     splitAt(0(),XS) -> U191(isLNat(XS),XS)
     splitAt(s(N),cons(X,XS)) -> U201(isNatural(N),N,X,activate(XS))
     tail(cons(N,XS)) -> U211(isNatural(N),activate(XS))
     take(N,XS) -> U221(isNatural(N),N,XS)
     natsFrom(X) -> n__natsFrom(X)
     s(X) -> n__s(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)
     activate(n__natsFrom(X)) -> natsFrom(activate(X))
     activate(n__s(X)) -> s(activate(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(X) -> X
    Open