(STRATEGY
    INNERMOST)

(VAR
    N V1 V2 X X1 X2 XS Y YS ZS)
(DATATYPES
    A = µX.< tt, n__natsFrom(X), n__nil, n__afterNth(X, X), n__cons(X, X), n__fst(X), n__snd(X), n__tail(X), n__take(X, X), n__0, n__head(X), n__s(X), n__sel(X, X), n__pair(X, X), n__splitAt(X, X) >)
(SIGNATURES
    U101 :: [A x A x A] -> A
    U102 :: [A x A x A] -> A
    U103 :: [A x A x A] -> A
    U104 :: [A x A x A] -> A
    U105 :: [A x A] -> A
    U106 :: [A] -> A
    U11 :: [A x A x A] -> A
    U111 :: [A x A] -> A
    U112 :: [A] -> A
    U12 :: [A x A x A] -> A
    U121 :: [A x A] -> A
    U122 :: [A] -> A
    U13 :: [A x A x A] -> A
    U131 :: [A] -> A
    U14 :: [A x A x A] -> A
    U141 :: [A] -> A
    U151 :: [A] -> A
    U161 :: [A] -> A
    U171 :: [A x A] -> A
    U172 :: [A] -> A
    U181 :: [A x A] -> A
    U182 :: [A x A] -> A
    U183 :: [A] -> A
    U191 :: [A x A] -> A
    U192 :: [A x A] -> A
    U193 :: [A] -> A
    U201 :: [A x A x A] -> A
    U202 :: [A x A x A] -> A
    U203 :: [A x A x A] -> A
    U204 :: [A x A x A] -> A
    U205 :: [A x A] -> A
    U206 :: [A] -> A
    U21 :: [A x A x A] -> A
    U211 :: [A] -> A
    U22 :: [A x A x A] -> A
    U221 :: [A] -> A
    U23 :: [A x A x A] -> A
    U231 :: [A x A] -> A
    U232 :: [A] -> A
    U24 :: [A x A] -> A
    U241 :: [A x A x A] -> A
    U242 :: [A x A x A] -> A
    U243 :: [A x A x A] -> A
    U244 :: [A x A x A] -> A
    U245 :: [A x A] -> A
    U246 :: [A] -> A
    U251 :: [A x A x A] -> A
    U252 :: [A x A x A] -> A
    U253 :: [A x A x A] -> A
    U254 :: [A x A x A] -> A
    U255 :: [A x A] -> A
    U256 :: [A] -> A
    U261 :: [A x A] -> A
    U262 :: [A] -> A
    U271 :: [A x A] -> A
    U272 :: [A] -> A
    U281 :: [A x A] -> A
    U282 :: [A x A] -> A
    U291 :: [A x A x A] -> A
    U292 :: [A x A x A] -> A
    U293 :: [A x A x A] -> A
    U294 :: [A x A x A] -> A
    U301 :: [A x A x A] -> A
    U302 :: [A x A] -> A
    U303 :: [A x A] -> A
    U304 :: [A x A] -> A
    U31 :: [A x A x A] -> A
    U311 :: [A x A] -> A
    U312 :: [A x A] -> A
    U32 :: [A x A x A] -> A
    U321 :: [A x A x A x A] -> A
    U322 :: [A x A x A x A] -> A
    U323 :: [A x A x A x A] -> A
    U324 :: [A x A x A x A] -> A
    U325 :: [A x A x A x A] -> A
    U326 :: [A x A x A x A] -> A
    U327 :: [A x A] -> A
    U33 :: [A x A x A] -> A
    U331 :: [A x A x A] -> A
    U332 :: [A x A] -> A
    U333 :: [A x A] -> A
    U334 :: [A x A] -> A
    U34 :: [A x A] -> A
    U341 :: [A x A x A] -> A
    U342 :: [A x A x A] -> A
    U343 :: [A x A x A] -> A
    U344 :: [A x A x A] -> A
    U41 :: [A x A x A] -> A
    U42 :: [A x A x A] -> A
    U43 :: [A x A x A] -> A
    U44 :: [A x A x A] -> A
    U45 :: [A x A] -> A
    U46 :: [A] -> A
    U51 :: [A x A x A] -> A
    U52 :: [A x A x A] -> A
    U53 :: [A x A x A] -> A
    U54 :: [A x A x A] -> A
    U55 :: [A x A] -> A
    U56 :: [A] -> A
    U61 :: [A x A] -> A
    U62 :: [A x A] -> A
    U63 :: [A] -> A
    U71 :: [A x A] -> A
    U72 :: [A x A] -> A
    U73 :: [A] -> A
    U81 :: [A x A] -> A
    U82 :: [A x A] -> A
    U83 :: [A] -> A
    U91 :: [A x A] -> A
    U92 :: [A x A] -> A
    U93 :: [A] -> A
    afterNth :: [A x A] -> A
    fst :: [A] -> A
    head :: [A] -> A
    isLNat :: [A] -> A
    isLNatKind :: [A] -> A
    isNatural :: [A] -> A
    isNaturalKind :: [A] -> A
    isPLNat :: [A] -> A
    isPLNatKind :: [A] -> A
    natsFrom :: [A] -> A
    sel :: [A x A] -> A
    snd :: [A] -> A
    splitAt :: [A x A] -> A
    tail :: [A] -> A
    take :: [A x A] -> A
    nil :: [] -> A
    cons :: [A x A] -> A
    0 :: [] -> A
    s :: [A] -> A
    pair :: [A x A] -> A
    activate :: [A] -> A)
(RULES
    U101(tt(),V1,V2) ->
      U102(isNaturalKind(activate(V1))
          ,activate(V1)
          ,activate(V2))
    U102(tt(),V1,V2) ->
      U103(isLNatKind(activate(V2))
          ,activate(V1)
          ,activate(V2))
    U103(tt(),V1,V2) ->
      U104(isLNatKind(activate(V2))
          ,activate(V1)
          ,activate(V2))
    U104(tt(),V1,V2) ->
      U105(isNatural(activate(V1))
          ,activate(V2))
    U105(tt(),V2) ->
      U106(isLNat(activate(V2)))
    U106(tt()) -> tt()
    U11(tt(),N,XS) ->
      U12(isNaturalKind(activate(N))
         ,activate(N)
         ,activate(XS))
    U111(tt(),V2) ->
      U112(isLNatKind(activate(V2)))
    U112(tt()) -> tt()
    U12(tt(),N,XS) ->
      U13(isLNat(activate(XS))
         ,activate(N)
         ,activate(XS))
    U121(tt(),V2) ->
      U122(isLNatKind(activate(V2)))
    U122(tt()) -> tt()
    U13(tt(),N,XS) ->
      U14(isLNatKind(activate(XS))
         ,activate(N)
         ,activate(XS))
    U131(tt()) -> tt()
    U14(tt(),N,XS) ->
      snd(splitAt(activate(N)
                 ,activate(XS)))
    U141(tt()) -> tt()
    U151(tt()) -> tt()
    U161(tt()) -> tt()
    U171(tt(),V2) ->
      U172(isLNatKind(activate(V2)))
    U172(tt()) -> tt()
    U181(tt(),V1) ->
      U182(isLNatKind(activate(V1))
          ,activate(V1))
    U182(tt(),V1) ->
      U183(isLNat(activate(V1)))
    U183(tt()) -> tt()
    U191(tt(),V1) ->
      U192(isNaturalKind(activate(V1))
          ,activate(V1))
    U192(tt(),V1) ->
      U193(isNatural(activate(V1)))
    U193(tt()) -> tt()
    U201(tt(),V1,V2) ->
      U202(isNaturalKind(activate(V1))
          ,activate(V1)
          ,activate(V2))
    U202(tt(),V1,V2) ->
      U203(isLNatKind(activate(V2))
          ,activate(V1)
          ,activate(V2))
    U203(tt(),V1,V2) ->
      U204(isLNatKind(activate(V2))
          ,activate(V1)
          ,activate(V2))
    U204(tt(),V1,V2) ->
      U205(isNatural(activate(V1))
          ,activate(V2))
    U205(tt(),V2) ->
      U206(isLNat(activate(V2)))
    U206(tt()) -> tt()
    U21(tt(),X,Y) ->
      U22(isLNatKind(activate(X))
         ,activate(X)
         ,activate(Y))
    U211(tt()) -> tt()
    U22(tt(),X,Y) ->
      U23(isLNat(activate(Y))
         ,activate(X)
         ,activate(Y))
    U221(tt()) -> tt()
    U23(tt(),X,Y) ->
      U24(isLNatKind(activate(Y))
         ,activate(X))
    U231(tt(),V2) ->
      U232(isLNatKind(activate(V2)))
    U232(tt()) -> tt()
    U24(tt(),X) -> activate(X)
    U241(tt(),V1,V2) ->
      U242(isLNatKind(activate(V1))
          ,activate(V1)
          ,activate(V2))
    U242(tt(),V1,V2) ->
      U243(isLNatKind(activate(V2))
          ,activate(V1)
          ,activate(V2))
    U243(tt(),V1,V2) ->
      U244(isLNatKind(activate(V2))
          ,activate(V1)
          ,activate(V2))
    U244(tt(),V1,V2) ->
      U245(isLNat(activate(V1))
          ,activate(V2))
    U245(tt(),V2) ->
      U246(isLNat(activate(V2)))
    U246(tt()) -> tt()
    U251(tt(),V1,V2) ->
      U252(isNaturalKind(activate(V1))
          ,activate(V1)
          ,activate(V2))
    U252(tt(),V1,V2) ->
      U253(isLNatKind(activate(V2))
          ,activate(V1)
          ,activate(V2))
    U253(tt(),V1,V2) ->
      U254(isLNatKind(activate(V2))
          ,activate(V1)
          ,activate(V2))
    U254(tt(),V1,V2) ->
      U255(isNatural(activate(V1))
          ,activate(V2))
    U255(tt(),V2) ->
      U256(isLNat(activate(V2)))
    U256(tt()) -> tt()
    U261(tt(),V2) ->
      U262(isLNatKind(activate(V2)))
    U262(tt()) -> tt()
    U271(tt(),V2) ->
      U272(isLNatKind(activate(V2)))
    U272(tt()) -> tt()
    U281(tt(),N) ->
      U282(isNaturalKind(activate(N))
          ,activate(N))
    U282(tt(),N) -> cons(activate(N)
                        ,n__natsFrom(s(activate(N))))
    U291(tt(),N,XS) ->
      U292(isNaturalKind(activate(N))
          ,activate(N)
          ,activate(XS))
    U292(tt(),N,XS) ->
      U293(isLNat(activate(XS))
          ,activate(N)
          ,activate(XS))
    U293(tt(),N,XS) ->
      U294(isLNatKind(activate(XS))
          ,activate(N)
          ,activate(XS))
    U294(tt(),N,XS) ->
      head(afterNth(activate(N)
                   ,activate(XS)))
    U301(tt(),X,Y) ->
      U302(isLNatKind(activate(X))
          ,activate(Y))
    U302(tt(),Y) ->
      U303(isLNat(activate(Y))
          ,activate(Y))
    U303(tt(),Y) ->
      U304(isLNatKind(activate(Y))
          ,activate(Y))
    U304(tt(),Y) -> activate(Y)
    U31(tt(),N,XS) ->
      U32(isNaturalKind(activate(N))
         ,activate(N)
         ,activate(XS))
    U311(tt(),XS) ->
      U312(isLNatKind(activate(XS))
          ,activate(XS))
    U312(tt(),XS) -> pair(nil()
                         ,activate(XS))
    U32(tt(),N,XS) ->
      U33(isLNat(activate(XS))
         ,activate(N)
         ,activate(XS))
    U321(tt(),N,X,XS) ->
      U322(isNaturalKind(activate(N))
          ,activate(N)
          ,activate(X)
          ,activate(XS))
    U322(tt(),N,X,XS) ->
      U323(isNatural(activate(X))
          ,activate(N)
          ,activate(X)
          ,activate(XS))
    U323(tt(),N,X,XS) ->
      U324(isNaturalKind(activate(X))
          ,activate(N)
          ,activate(X)
          ,activate(XS))
    U324(tt(),N,X,XS) ->
      U325(isLNat(activate(XS))
          ,activate(N)
          ,activate(X)
          ,activate(XS))
    U325(tt(),N,X,XS) ->
      U326(isLNatKind(activate(XS))
          ,activate(N)
          ,activate(X)
          ,activate(XS))
    U326(tt(),N,X,XS) ->
      U327(splitAt(activate(N)
                  ,activate(XS))
          ,activate(X))
    U327(pair(YS,ZS),X) ->
      pair(cons(activate(X),YS),ZS)
    U33(tt(),N,XS) ->
      U34(isLNatKind(activate(XS))
         ,activate(N))
    U331(tt(),N,XS) ->
      U332(isNaturalKind(activate(N))
          ,activate(XS))
    U332(tt(),XS) ->
      U333(isLNat(activate(XS))
          ,activate(XS))
    U333(tt(),XS) ->
      U334(isLNatKind(activate(XS))
          ,activate(XS))
    U334(tt(),XS) -> activate(XS)
    U34(tt(),N) -> activate(N)
    U341(tt(),N,XS) ->
      U342(isNaturalKind(activate(N))
          ,activate(N)
          ,activate(XS))
    U342(tt(),N,XS) ->
      U343(isLNat(activate(XS))
          ,activate(N)
          ,activate(XS))
    U343(tt(),N,XS) ->
      U344(isLNatKind(activate(XS))
          ,activate(N)
          ,activate(XS))
    U344(tt(),N,XS) ->
      fst(splitAt(activate(N)
                 ,activate(XS)))
    U41(tt(),V1,V2) ->
      U42(isNaturalKind(activate(V1))
         ,activate(V1)
         ,activate(V2))
    U42(tt(),V1,V2) ->
      U43(isLNatKind(activate(V2))
         ,activate(V1)
         ,activate(V2))
    U43(tt(),V1,V2) ->
      U44(isLNatKind(activate(V2))
         ,activate(V1)
         ,activate(V2))
    U44(tt(),V1,V2) ->
      U45(isNatural(activate(V1))
         ,activate(V2))
    U45(tt(),V2) ->
      U46(isLNat(activate(V2)))
    U46(tt()) -> tt()
    U51(tt(),V1,V2) ->
      U52(isNaturalKind(activate(V1))
         ,activate(V1)
         ,activate(V2))
    U52(tt(),V1,V2) ->
      U53(isLNatKind(activate(V2))
         ,activate(V1)
         ,activate(V2))
    U53(tt(),V1,V2) ->
      U54(isLNatKind(activate(V2))
         ,activate(V1)
         ,activate(V2))
    U54(tt(),V1,V2) ->
      U55(isNatural(activate(V1))
         ,activate(V2))
    U55(tt(),V2) ->
      U56(isLNat(activate(V2)))
    U56(tt()) -> tt()
    U61(tt(),V1) ->
      U62(isPLNatKind(activate(V1))
         ,activate(V1))
    U62(tt(),V1) ->
      U63(isPLNat(activate(V1)))
    U63(tt()) -> tt()
    U71(tt(),V1) ->
      U72(isNaturalKind(activate(V1))
         ,activate(V1))
    U72(tt(),V1) ->
      U73(isNatural(activate(V1)))
    U73(tt()) -> tt()
    U81(tt(),V1) ->
      U82(isPLNatKind(activate(V1))
         ,activate(V1))
    U82(tt(),V1) ->
      U83(isPLNat(activate(V1)))
    U83(tt()) -> tt()
    U91(tt(),V1) ->
      U92(isLNatKind(activate(V1))
         ,activate(V1))
    U92(tt(),V1) ->
      U93(isLNat(activate(V1)))
    U93(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(isNaturalKind(activate(V1))
         ,activate(V1)
         ,activate(V2))
    isLNat(n__cons(V1,V2)) ->
      U51(isNaturalKind(activate(V1))
         ,activate(V1)
         ,activate(V2))
    isLNat(n__fst(V1)) ->
      U61(isPLNatKind(activate(V1))
         ,activate(V1))
    isLNat(n__natsFrom(V1)) ->
      U71(isNaturalKind(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(isNaturalKind(activate(V1))
          ,activate(V1)
          ,activate(V2))
    isLNatKind(n__nil()) -> tt()
    isLNatKind(n__afterNth(V1
                          ,V2)) ->
      U111(isNaturalKind(activate(V1))
          ,activate(V2))
    isLNatKind(n__cons(V1,V2)) ->
      U121(isNaturalKind(activate(V1))
          ,activate(V2))
    isLNatKind(n__fst(V1)) ->
      U131(isPLNatKind(activate(V1)))
    isLNatKind(n__natsFrom(V1)) ->
      U141(isNaturalKind(activate(V1)))
    isLNatKind(n__snd(V1)) ->
      U151(isPLNatKind(activate(V1)))
    isLNatKind(n__tail(V1)) ->
      U161(isLNatKind(activate(V1)))
    isLNatKind(n__take(V1,V2)) ->
      U171(isNaturalKind(activate(V1))
          ,activate(V2))
    isNatural(n__0()) -> tt()
    isNatural(n__head(V1)) ->
      U181(isLNatKind(activate(V1))
          ,activate(V1))
    isNatural(n__s(V1)) ->
      U191(isNaturalKind(activate(V1))
          ,activate(V1))
    isNatural(n__sel(V1,V2)) ->
      U201(isNaturalKind(activate(V1))
          ,activate(V1)
          ,activate(V2))
    isNaturalKind(n__0()) -> tt()
    isNaturalKind(n__head(V1)) ->
      U211(isLNatKind(activate(V1)))
    isNaturalKind(n__s(V1)) ->
      U221(isNaturalKind(activate(V1)))
    isNaturalKind(n__sel(V1,V2)) ->
      U231(isNaturalKind(activate(V1))
          ,activate(V2))
    isPLNat(n__pair(V1,V2)) ->
      U241(isLNatKind(activate(V1))
          ,activate(V1)
          ,activate(V2))
    isPLNat(n__splitAt(V1,V2)) ->
      U251(isNaturalKind(activate(V1))
          ,activate(V1)
          ,activate(V2))
    isPLNatKind(n__pair(V1,V2)) ->
      U261(isLNatKind(activate(V1))
          ,activate(V2))
    isPLNatKind(n__splitAt(V1
                          ,V2)) ->
      U271(isNaturalKind(activate(V1))
          ,activate(V2))
    natsFrom(N) -> U281(isNatural(N)
                       ,N)
    sel(N,XS) -> U291(isNatural(N)
                     ,N
                     ,XS)
    snd(pair(X,Y)) -> U301(isLNat(X)
                          ,X
                          ,Y)
    splitAt(0(),XS) ->
      U311(isLNat(XS),XS)
    splitAt(s(N),cons(X,XS)) ->
      U321(isNatural(N)
          ,N
          ,X
          ,activate(XS))
    tail(cons(N,XS)) ->
      U331(isNatural(N)
          ,N
          ,activate(XS))
    take(N,XS) -> U341(isNatural(N)
                      ,N
                      ,XS)
    natsFrom(X) -> n__natsFrom(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)
    s(X) -> n__s(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(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(X) -> X)