MAYBE

We are left with following problem, upon which TcT provides the
certificate MAYBE.

Strict Trs:
  { U101(tt(), V2) -> U102(isLNat(activate(V2)))
  , U102(tt()) -> tt()
  , isLNat(n__natsFrom(V1)) -> U71(isNatural(activate(V1)))
  , 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__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))
  , activate(X) -> X
  , 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)
  , U11(tt(), N, XS) ->
    U12(isLNat(activate(XS)), activate(N), activate(XS))
  , U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
  , U111(tt()) -> tt()
  , snd(X) -> n__snd(X)
  , snd(pair(X, Y)) -> U181(isLNat(X), Y)
  , splitAt(X1, X2) -> n__splitAt(X1, X2)
  , splitAt(s(N), cons(X, XS)) ->
    U201(isNatural(N), N, X, activate(XS))
  , splitAt(0(), XS) -> U191(isLNat(XS), 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(s(activate(N))))
  , cons(X1, X2) -> n__cons(X1, X2)
  , s(X) -> n__s(X)
  , U171(tt(), N, XS) ->
    U172(isLNat(activate(XS)), activate(N), activate(XS))
  , U172(tt(), N, XS) -> head(afterNth(activate(N), activate(XS)))
  , head(X) -> n__head(X)
  , head(cons(N, XS)) -> U31(isNatural(N), N, activate(XS))
  , afterNth(N, XS) -> U11(isNatural(N), N, XS)
  , afterNth(X1, X2) -> n__afterNth(X1, X2)
  , U181(tt(), Y) -> U182(isLNat(activate(Y)), activate(Y))
  , U182(tt(), Y) -> activate(Y)
  , U191(tt(), XS) -> pair(nil(), activate(XS))
  , pair(X1, X2) -> n__pair(X1, X2)
  , nil() -> n__nil()
  , 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))
  , 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))
  , 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))
  , U22(tt(), X) -> activate(X)
  , U211(tt(), XS) -> U212(isLNat(activate(XS)), activate(XS))
  , U212(tt(), XS) -> activate(XS)
  , U221(tt(), N, XS) ->
    U222(isLNat(activate(XS)), activate(N), activate(XS))
  , U222(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS)))
  , fst(X) -> n__fst(X)
  , fst(pair(X, Y)) -> U21(isLNat(X), X, Y)
  , 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()
  , 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)
  , natsFrom(X) -> n__natsFrom(X)
  , sel(N, XS) -> U171(isNatural(N), N, XS)
  , sel(X1, X2) -> n__sel(X1, X2)
  , 0() -> n__0()
  , tail(X) -> n__tail(X)
  , tail(cons(N, XS)) -> U211(isNatural(N), activate(XS))
  , take(N, XS) -> U221(isNatural(N), N, XS)
  , take(X1, X2) -> n__take(X1, X2) }
Obligation:
  runtime complexity
Answer:
  MAYBE

None of the processors succeeded.

Details of failed attempt(s):
-----------------------------
1) 'WithProblem (timeout of 60 seconds)' failed due to the
   following reason:
   
   Computation stopped due to timeout after 60.0 seconds.

2) 'Best' failed due to the following reason:
   
   None of the processors succeeded.
   
   Details of failed attempt(s):
   -----------------------------
   1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)'
      failed due to the following reason:
      
      Computation stopped due to timeout after 30.0 seconds.
   
   2) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed
      due to the following reason:
      
      None of the processors succeeded.
      
      Details of failed attempt(s):
      -----------------------------
      1) 'Bounds with minimal-enrichment and initial automaton 'match''
         failed due to the following reason:
         
         match-boundness of the problem could not be verified.
      
      2) 'Bounds with perSymbol-enrichment and initial automaton 'match''
         failed due to the following reason:
         
         match-boundness of the problem could not be verified.
      
   
   3) 'Best' failed due to the following reason:
      
      None of the processors succeeded.
      
      Details of failed attempt(s):
      -----------------------------
      1) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due
         to the following reason:
         
         The processor is inapplicable, reason:
           Processor only applicable for innermost runtime complexity analysis
      
      2) 'bsearch-popstar (timeout of 60 seconds)' failed due to the
         following reason:
         
         The processor is inapplicable, reason:
           Processor only applicable for innermost runtime complexity analysis
      
   

3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed
   due to the following reason:
   
   We add the following weak dependency pairs:
   
   Strict DPs:
     { U101^#(tt(), V2) -> c_1(U102^#(isLNat(activate(V2))))
     , U102^#(tt()) -> c_2()
     , isLNat^#(n__natsFrom(V1)) -> c_3(U71^#(isNatural(activate(V1))))
     , isLNat^#(n__nil()) -> c_4()
     , isLNat^#(n__afterNth(V1, V2)) ->
       c_5(U41^#(isNatural(activate(V1)), activate(V2)))
     , isLNat^#(n__cons(V1, V2)) ->
       c_6(U51^#(isNatural(activate(V1)), activate(V2)))
     , isLNat^#(n__fst(V1)) -> c_7(U61^#(isPLNat(activate(V1))))
     , isLNat^#(n__snd(V1)) -> c_8(U81^#(isPLNat(activate(V1))))
     , isLNat^#(n__tail(V1)) -> c_9(U91^#(isLNat(activate(V1))))
     , isLNat^#(n__take(V1, V2)) ->
       c_10(U101^#(isNatural(activate(V1)), activate(V2)))
     , U71^#(tt()) -> c_78()
     , U41^#(tt(), V2) -> c_73(U42^#(isLNat(activate(V2))))
     , U51^#(tt(), V2) -> c_75(U52^#(isLNat(activate(V2))))
     , U61^#(tt()) -> c_77()
     , U81^#(tt()) -> c_79()
     , U91^#(tt()) -> c_80()
     , activate^#(X) -> c_11(X)
     , activate^#(n__natsFrom(X)) -> c_12(natsFrom^#(X))
     , activate^#(n__nil()) -> c_13(nil^#())
     , activate^#(n__afterNth(X1, X2)) -> c_14(afterNth^#(X1, X2))
     , activate^#(n__cons(X1, X2)) -> c_15(cons^#(X1, X2))
     , activate^#(n__fst(X)) -> c_16(fst^#(X))
     , activate^#(n__snd(X)) -> c_17(snd^#(X))
     , activate^#(n__tail(X)) -> c_18(tail^#(X))
     , activate^#(n__take(X1, X2)) -> c_19(take^#(X1, X2))
     , activate^#(n__0()) -> c_20(0^#())
     , activate^#(n__head(X)) -> c_21(head^#(X))
     , activate^#(n__s(X)) -> c_22(s^#(X))
     , activate^#(n__sel(X1, X2)) -> c_23(sel^#(X1, X2))
     , activate^#(n__pair(X1, X2)) -> c_24(pair^#(X1, X2))
     , activate^#(n__splitAt(X1, X2)) -> c_25(splitAt^#(X1, X2))
     , natsFrom^#(N) -> c_83(U161^#(isNatural(N), N))
     , natsFrom^#(X) -> c_84(X)
     , nil^#() -> c_54()
     , afterNth^#(N, XS) -> c_48(U11^#(isNatural(N), N, XS))
     , afterNth^#(X1, X2) -> c_49(X1, X2)
     , cons^#(X1, X2) -> c_42(X1, X2)
     , fst^#(X) -> c_69(X)
     , fst^#(pair(X, Y)) -> c_70(U21^#(isLNat(X), X, Y))
     , snd^#(X) -> c_29(X)
     , snd^#(pair(X, Y)) -> c_30(U181^#(isLNat(X), Y))
     , tail^#(X) -> c_88(X)
     , tail^#(cons(N, XS)) -> c_89(U211^#(isNatural(N), activate(XS)))
     , take^#(N, XS) -> c_90(U221^#(isNatural(N), N, XS))
     , take^#(X1, X2) -> c_91(X1, X2)
     , 0^#() -> c_87()
     , head^#(X) -> c_46(X)
     , head^#(cons(N, XS)) -> c_47(U31^#(isNatural(N), N, activate(XS)))
     , s^#(X) -> c_43(X)
     , sel^#(N, XS) -> c_85(U171^#(isNatural(N), N, XS))
     , sel^#(X1, X2) -> c_86(X1, X2)
     , pair^#(X1, X2) -> c_53(X1, X2)
     , splitAt^#(X1, X2) -> c_31(X1, X2)
     , splitAt^#(s(N), cons(X, XS)) ->
       c_32(U201^#(isNatural(N), N, X, activate(XS)))
     , splitAt^#(0(), XS) -> c_33(U191^#(isLNat(XS), XS))
     , U11^#(tt(), N, XS) ->
       c_26(U12^#(isLNat(activate(XS)), activate(N), activate(XS)))
     , U12^#(tt(), N, XS) ->
       c_27(snd^#(splitAt(activate(N), activate(XS))))
     , U111^#(tt()) -> c_28()
     , U181^#(tt(), Y) -> c_50(U182^#(isLNat(activate(Y)), activate(Y)))
     , U201^#(tt(), N, X, XS) ->
       c_55(U202^#(isNatural(activate(X)),
                   activate(N),
                   activate(X),
                   activate(XS)))
     , U191^#(tt(), XS) -> c_52(pair^#(nil(), activate(XS)))
     , U121^#(tt()) -> c_34()
     , U131^#(tt(), V2) -> c_35(U132^#(isLNat(activate(V2))))
     , U132^#(tt()) -> c_36()
     , U141^#(tt(), V2) -> c_37(U142^#(isLNat(activate(V2))))
     , U142^#(tt()) -> c_38()
     , U151^#(tt(), V2) -> c_39(U152^#(isLNat(activate(V2))))
     , U152^#(tt()) -> c_40()
     , U161^#(tt(), N) ->
       c_41(cons^#(activate(N), n__natsFrom(s(activate(N)))))
     , U171^#(tt(), N, XS) ->
       c_44(U172^#(isLNat(activate(XS)), activate(N), activate(XS)))
     , U172^#(tt(), N, XS) ->
       c_45(head^#(afterNth(activate(N), activate(XS))))
     , U31^#(tt(), N, XS) ->
       c_71(U32^#(isLNat(activate(XS)), activate(N)))
     , U182^#(tt(), Y) -> c_51(activate^#(Y))
     , U202^#(tt(), N, X, XS) ->
       c_56(U203^#(isLNat(activate(XS)),
                   activate(N),
                   activate(X),
                   activate(XS)))
     , U203^#(tt(), N, X, XS) ->
       c_61(U204^#(splitAt(activate(N), activate(XS)), activate(X)))
     , isNatural^#(n__0()) -> c_57()
     , isNatural^#(n__head(V1)) -> c_58(U111^#(isLNat(activate(V1))))
     , isNatural^#(n__s(V1)) -> c_59(U121^#(isNatural(activate(V1))))
     , isNatural^#(n__sel(V1, V2)) ->
       c_60(U131^#(isNatural(activate(V1)), activate(V2)))
     , U204^#(pair(YS, ZS), X) ->
       c_62(pair^#(cons(activate(X), YS), ZS))
     , U21^#(tt(), X, Y) ->
       c_63(U22^#(isLNat(activate(Y)), activate(X)))
     , U22^#(tt(), X) -> c_64(activate^#(X))
     , U211^#(tt(), XS) ->
       c_65(U212^#(isLNat(activate(XS)), activate(XS)))
     , U212^#(tt(), XS) -> c_66(activate^#(XS))
     , U221^#(tt(), N, XS) ->
       c_67(U222^#(isLNat(activate(XS)), activate(N), activate(XS)))
     , U222^#(tt(), N, XS) ->
       c_68(fst^#(splitAt(activate(N), activate(XS))))
     , U32^#(tt(), N) -> c_72(activate^#(N))
     , U42^#(tt()) -> c_74()
     , U52^#(tt()) -> c_76()
     , isPLNat^#(n__pair(V1, V2)) ->
       c_81(U141^#(isLNat(activate(V1)), activate(V2)))
     , isPLNat^#(n__splitAt(V1, V2)) ->
       c_82(U151^#(isNatural(activate(V1)), activate(V2))) }
   
   and mark the set of starting terms.
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { U101^#(tt(), V2) -> c_1(U102^#(isLNat(activate(V2))))
     , U102^#(tt()) -> c_2()
     , isLNat^#(n__natsFrom(V1)) -> c_3(U71^#(isNatural(activate(V1))))
     , isLNat^#(n__nil()) -> c_4()
     , isLNat^#(n__afterNth(V1, V2)) ->
       c_5(U41^#(isNatural(activate(V1)), activate(V2)))
     , isLNat^#(n__cons(V1, V2)) ->
       c_6(U51^#(isNatural(activate(V1)), activate(V2)))
     , isLNat^#(n__fst(V1)) -> c_7(U61^#(isPLNat(activate(V1))))
     , isLNat^#(n__snd(V1)) -> c_8(U81^#(isPLNat(activate(V1))))
     , isLNat^#(n__tail(V1)) -> c_9(U91^#(isLNat(activate(V1))))
     , isLNat^#(n__take(V1, V2)) ->
       c_10(U101^#(isNatural(activate(V1)), activate(V2)))
     , U71^#(tt()) -> c_78()
     , U41^#(tt(), V2) -> c_73(U42^#(isLNat(activate(V2))))
     , U51^#(tt(), V2) -> c_75(U52^#(isLNat(activate(V2))))
     , U61^#(tt()) -> c_77()
     , U81^#(tt()) -> c_79()
     , U91^#(tt()) -> c_80()
     , activate^#(X) -> c_11(X)
     , activate^#(n__natsFrom(X)) -> c_12(natsFrom^#(X))
     , activate^#(n__nil()) -> c_13(nil^#())
     , activate^#(n__afterNth(X1, X2)) -> c_14(afterNth^#(X1, X2))
     , activate^#(n__cons(X1, X2)) -> c_15(cons^#(X1, X2))
     , activate^#(n__fst(X)) -> c_16(fst^#(X))
     , activate^#(n__snd(X)) -> c_17(snd^#(X))
     , activate^#(n__tail(X)) -> c_18(tail^#(X))
     , activate^#(n__take(X1, X2)) -> c_19(take^#(X1, X2))
     , activate^#(n__0()) -> c_20(0^#())
     , activate^#(n__head(X)) -> c_21(head^#(X))
     , activate^#(n__s(X)) -> c_22(s^#(X))
     , activate^#(n__sel(X1, X2)) -> c_23(sel^#(X1, X2))
     , activate^#(n__pair(X1, X2)) -> c_24(pair^#(X1, X2))
     , activate^#(n__splitAt(X1, X2)) -> c_25(splitAt^#(X1, X2))
     , natsFrom^#(N) -> c_83(U161^#(isNatural(N), N))
     , natsFrom^#(X) -> c_84(X)
     , nil^#() -> c_54()
     , afterNth^#(N, XS) -> c_48(U11^#(isNatural(N), N, XS))
     , afterNth^#(X1, X2) -> c_49(X1, X2)
     , cons^#(X1, X2) -> c_42(X1, X2)
     , fst^#(X) -> c_69(X)
     , fst^#(pair(X, Y)) -> c_70(U21^#(isLNat(X), X, Y))
     , snd^#(X) -> c_29(X)
     , snd^#(pair(X, Y)) -> c_30(U181^#(isLNat(X), Y))
     , tail^#(X) -> c_88(X)
     , tail^#(cons(N, XS)) -> c_89(U211^#(isNatural(N), activate(XS)))
     , take^#(N, XS) -> c_90(U221^#(isNatural(N), N, XS))
     , take^#(X1, X2) -> c_91(X1, X2)
     , 0^#() -> c_87()
     , head^#(X) -> c_46(X)
     , head^#(cons(N, XS)) -> c_47(U31^#(isNatural(N), N, activate(XS)))
     , s^#(X) -> c_43(X)
     , sel^#(N, XS) -> c_85(U171^#(isNatural(N), N, XS))
     , sel^#(X1, X2) -> c_86(X1, X2)
     , pair^#(X1, X2) -> c_53(X1, X2)
     , splitAt^#(X1, X2) -> c_31(X1, X2)
     , splitAt^#(s(N), cons(X, XS)) ->
       c_32(U201^#(isNatural(N), N, X, activate(XS)))
     , splitAt^#(0(), XS) -> c_33(U191^#(isLNat(XS), XS))
     , U11^#(tt(), N, XS) ->
       c_26(U12^#(isLNat(activate(XS)), activate(N), activate(XS)))
     , U12^#(tt(), N, XS) ->
       c_27(snd^#(splitAt(activate(N), activate(XS))))
     , U111^#(tt()) -> c_28()
     , U181^#(tt(), Y) -> c_50(U182^#(isLNat(activate(Y)), activate(Y)))
     , U201^#(tt(), N, X, XS) ->
       c_55(U202^#(isNatural(activate(X)),
                   activate(N),
                   activate(X),
                   activate(XS)))
     , U191^#(tt(), XS) -> c_52(pair^#(nil(), activate(XS)))
     , U121^#(tt()) -> c_34()
     , U131^#(tt(), V2) -> c_35(U132^#(isLNat(activate(V2))))
     , U132^#(tt()) -> c_36()
     , U141^#(tt(), V2) -> c_37(U142^#(isLNat(activate(V2))))
     , U142^#(tt()) -> c_38()
     , U151^#(tt(), V2) -> c_39(U152^#(isLNat(activate(V2))))
     , U152^#(tt()) -> c_40()
     , U161^#(tt(), N) ->
       c_41(cons^#(activate(N), n__natsFrom(s(activate(N)))))
     , U171^#(tt(), N, XS) ->
       c_44(U172^#(isLNat(activate(XS)), activate(N), activate(XS)))
     , U172^#(tt(), N, XS) ->
       c_45(head^#(afterNth(activate(N), activate(XS))))
     , U31^#(tt(), N, XS) ->
       c_71(U32^#(isLNat(activate(XS)), activate(N)))
     , U182^#(tt(), Y) -> c_51(activate^#(Y))
     , U202^#(tt(), N, X, XS) ->
       c_56(U203^#(isLNat(activate(XS)),
                   activate(N),
                   activate(X),
                   activate(XS)))
     , U203^#(tt(), N, X, XS) ->
       c_61(U204^#(splitAt(activate(N), activate(XS)), activate(X)))
     , isNatural^#(n__0()) -> c_57()
     , isNatural^#(n__head(V1)) -> c_58(U111^#(isLNat(activate(V1))))
     , isNatural^#(n__s(V1)) -> c_59(U121^#(isNatural(activate(V1))))
     , isNatural^#(n__sel(V1, V2)) ->
       c_60(U131^#(isNatural(activate(V1)), activate(V2)))
     , U204^#(pair(YS, ZS), X) ->
       c_62(pair^#(cons(activate(X), YS), ZS))
     , U21^#(tt(), X, Y) ->
       c_63(U22^#(isLNat(activate(Y)), activate(X)))
     , U22^#(tt(), X) -> c_64(activate^#(X))
     , U211^#(tt(), XS) ->
       c_65(U212^#(isLNat(activate(XS)), activate(XS)))
     , U212^#(tt(), XS) -> c_66(activate^#(XS))
     , U221^#(tt(), N, XS) ->
       c_67(U222^#(isLNat(activate(XS)), activate(N), activate(XS)))
     , U222^#(tt(), N, XS) ->
       c_68(fst^#(splitAt(activate(N), activate(XS))))
     , U32^#(tt(), N) -> c_72(activate^#(N))
     , U42^#(tt()) -> c_74()
     , U52^#(tt()) -> c_76()
     , isPLNat^#(n__pair(V1, V2)) ->
       c_81(U141^#(isLNat(activate(V1)), activate(V2)))
     , isPLNat^#(n__splitAt(V1, V2)) ->
       c_82(U151^#(isNatural(activate(V1)), activate(V2))) }
   Strict Trs:
     { U101(tt(), V2) -> U102(isLNat(activate(V2)))
     , U102(tt()) -> tt()
     , isLNat(n__natsFrom(V1)) -> U71(isNatural(activate(V1)))
     , 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__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))
     , activate(X) -> X
     , 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)
     , U11(tt(), N, XS) ->
       U12(isLNat(activate(XS)), activate(N), activate(XS))
     , U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
     , U111(tt()) -> tt()
     , snd(X) -> n__snd(X)
     , snd(pair(X, Y)) -> U181(isLNat(X), Y)
     , splitAt(X1, X2) -> n__splitAt(X1, X2)
     , splitAt(s(N), cons(X, XS)) ->
       U201(isNatural(N), N, X, activate(XS))
     , splitAt(0(), XS) -> U191(isLNat(XS), 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(s(activate(N))))
     , cons(X1, X2) -> n__cons(X1, X2)
     , s(X) -> n__s(X)
     , U171(tt(), N, XS) ->
       U172(isLNat(activate(XS)), activate(N), activate(XS))
     , U172(tt(), N, XS) -> head(afterNth(activate(N), activate(XS)))
     , head(X) -> n__head(X)
     , head(cons(N, XS)) -> U31(isNatural(N), N, activate(XS))
     , afterNth(N, XS) -> U11(isNatural(N), N, XS)
     , afterNth(X1, X2) -> n__afterNth(X1, X2)
     , U181(tt(), Y) -> U182(isLNat(activate(Y)), activate(Y))
     , U182(tt(), Y) -> activate(Y)
     , U191(tt(), XS) -> pair(nil(), activate(XS))
     , pair(X1, X2) -> n__pair(X1, X2)
     , nil() -> n__nil()
     , 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))
     , 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))
     , 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))
     , U22(tt(), X) -> activate(X)
     , U211(tt(), XS) -> U212(isLNat(activate(XS)), activate(XS))
     , U212(tt(), XS) -> activate(XS)
     , U221(tt(), N, XS) ->
       U222(isLNat(activate(XS)), activate(N), activate(XS))
     , U222(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS)))
     , fst(X) -> n__fst(X)
     , fst(pair(X, Y)) -> U21(isLNat(X), X, Y)
     , 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()
     , 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)
     , natsFrom(X) -> n__natsFrom(X)
     , sel(N, XS) -> U171(isNatural(N), N, XS)
     , sel(X1, X2) -> n__sel(X1, X2)
     , 0() -> n__0()
     , tail(X) -> n__tail(X)
     , tail(cons(N, XS)) -> U211(isNatural(N), activate(XS))
     , take(N, XS) -> U221(isNatural(N), N, XS)
     , take(X1, X2) -> n__take(X1, X2) }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   We estimate the number of application of
   {2,4,11,14,15,16,34,46,58,62,64,66,68,76,88,89} by applications of
   Pre({2,4,11,14,15,16,34,46,58,62,64,66,68,76,88,89}) =
   {1,3,7,8,9,12,13,17,19,26,33,36,37,38,40,42,45,47,49,51,52,53,63,65,67,77,78}.
   Here rules are labeled as follows:
   
     DPs:
       { 1: U101^#(tt(), V2) -> c_1(U102^#(isLNat(activate(V2))))
       , 2: U102^#(tt()) -> c_2()
       , 3: isLNat^#(n__natsFrom(V1)) ->
            c_3(U71^#(isNatural(activate(V1))))
       , 4: isLNat^#(n__nil()) -> c_4()
       , 5: isLNat^#(n__afterNth(V1, V2)) ->
            c_5(U41^#(isNatural(activate(V1)), activate(V2)))
       , 6: isLNat^#(n__cons(V1, V2)) ->
            c_6(U51^#(isNatural(activate(V1)), activate(V2)))
       , 7: isLNat^#(n__fst(V1)) -> c_7(U61^#(isPLNat(activate(V1))))
       , 8: isLNat^#(n__snd(V1)) -> c_8(U81^#(isPLNat(activate(V1))))
       , 9: isLNat^#(n__tail(V1)) -> c_9(U91^#(isLNat(activate(V1))))
       , 10: isLNat^#(n__take(V1, V2)) ->
             c_10(U101^#(isNatural(activate(V1)), activate(V2)))
       , 11: U71^#(tt()) -> c_78()
       , 12: U41^#(tt(), V2) -> c_73(U42^#(isLNat(activate(V2))))
       , 13: U51^#(tt(), V2) -> c_75(U52^#(isLNat(activate(V2))))
       , 14: U61^#(tt()) -> c_77()
       , 15: U81^#(tt()) -> c_79()
       , 16: U91^#(tt()) -> c_80()
       , 17: activate^#(X) -> c_11(X)
       , 18: activate^#(n__natsFrom(X)) -> c_12(natsFrom^#(X))
       , 19: activate^#(n__nil()) -> c_13(nil^#())
       , 20: activate^#(n__afterNth(X1, X2)) -> c_14(afterNth^#(X1, X2))
       , 21: activate^#(n__cons(X1, X2)) -> c_15(cons^#(X1, X2))
       , 22: activate^#(n__fst(X)) -> c_16(fst^#(X))
       , 23: activate^#(n__snd(X)) -> c_17(snd^#(X))
       , 24: activate^#(n__tail(X)) -> c_18(tail^#(X))
       , 25: activate^#(n__take(X1, X2)) -> c_19(take^#(X1, X2))
       , 26: activate^#(n__0()) -> c_20(0^#())
       , 27: activate^#(n__head(X)) -> c_21(head^#(X))
       , 28: activate^#(n__s(X)) -> c_22(s^#(X))
       , 29: activate^#(n__sel(X1, X2)) -> c_23(sel^#(X1, X2))
       , 30: activate^#(n__pair(X1, X2)) -> c_24(pair^#(X1, X2))
       , 31: activate^#(n__splitAt(X1, X2)) -> c_25(splitAt^#(X1, X2))
       , 32: natsFrom^#(N) -> c_83(U161^#(isNatural(N), N))
       , 33: natsFrom^#(X) -> c_84(X)
       , 34: nil^#() -> c_54()
       , 35: afterNth^#(N, XS) -> c_48(U11^#(isNatural(N), N, XS))
       , 36: afterNth^#(X1, X2) -> c_49(X1, X2)
       , 37: cons^#(X1, X2) -> c_42(X1, X2)
       , 38: fst^#(X) -> c_69(X)
       , 39: fst^#(pair(X, Y)) -> c_70(U21^#(isLNat(X), X, Y))
       , 40: snd^#(X) -> c_29(X)
       , 41: snd^#(pair(X, Y)) -> c_30(U181^#(isLNat(X), Y))
       , 42: tail^#(X) -> c_88(X)
       , 43: tail^#(cons(N, XS)) ->
             c_89(U211^#(isNatural(N), activate(XS)))
       , 44: take^#(N, XS) -> c_90(U221^#(isNatural(N), N, XS))
       , 45: take^#(X1, X2) -> c_91(X1, X2)
       , 46: 0^#() -> c_87()
       , 47: head^#(X) -> c_46(X)
       , 48: head^#(cons(N, XS)) ->
             c_47(U31^#(isNatural(N), N, activate(XS)))
       , 49: s^#(X) -> c_43(X)
       , 50: sel^#(N, XS) -> c_85(U171^#(isNatural(N), N, XS))
       , 51: sel^#(X1, X2) -> c_86(X1, X2)
       , 52: pair^#(X1, X2) -> c_53(X1, X2)
       , 53: splitAt^#(X1, X2) -> c_31(X1, X2)
       , 54: splitAt^#(s(N), cons(X, XS)) ->
             c_32(U201^#(isNatural(N), N, X, activate(XS)))
       , 55: splitAt^#(0(), XS) -> c_33(U191^#(isLNat(XS), XS))
       , 56: U11^#(tt(), N, XS) ->
             c_26(U12^#(isLNat(activate(XS)), activate(N), activate(XS)))
       , 57: U12^#(tt(), N, XS) ->
             c_27(snd^#(splitAt(activate(N), activate(XS))))
       , 58: U111^#(tt()) -> c_28()
       , 59: U181^#(tt(), Y) ->
             c_50(U182^#(isLNat(activate(Y)), activate(Y)))
       , 60: U201^#(tt(), N, X, XS) ->
             c_55(U202^#(isNatural(activate(X)),
                         activate(N),
                         activate(X),
                         activate(XS)))
       , 61: U191^#(tt(), XS) -> c_52(pair^#(nil(), activate(XS)))
       , 62: U121^#(tt()) -> c_34()
       , 63: U131^#(tt(), V2) -> c_35(U132^#(isLNat(activate(V2))))
       , 64: U132^#(tt()) -> c_36()
       , 65: U141^#(tt(), V2) -> c_37(U142^#(isLNat(activate(V2))))
       , 66: U142^#(tt()) -> c_38()
       , 67: U151^#(tt(), V2) -> c_39(U152^#(isLNat(activate(V2))))
       , 68: U152^#(tt()) -> c_40()
       , 69: U161^#(tt(), N) ->
             c_41(cons^#(activate(N), n__natsFrom(s(activate(N)))))
       , 70: U171^#(tt(), N, XS) ->
             c_44(U172^#(isLNat(activate(XS)), activate(N), activate(XS)))
       , 71: U172^#(tt(), N, XS) ->
             c_45(head^#(afterNth(activate(N), activate(XS))))
       , 72: U31^#(tt(), N, XS) ->
             c_71(U32^#(isLNat(activate(XS)), activate(N)))
       , 73: U182^#(tt(), Y) -> c_51(activate^#(Y))
       , 74: U202^#(tt(), N, X, XS) ->
             c_56(U203^#(isLNat(activate(XS)),
                         activate(N),
                         activate(X),
                         activate(XS)))
       , 75: U203^#(tt(), N, X, XS) ->
             c_61(U204^#(splitAt(activate(N), activate(XS)), activate(X)))
       , 76: isNatural^#(n__0()) -> c_57()
       , 77: isNatural^#(n__head(V1)) ->
             c_58(U111^#(isLNat(activate(V1))))
       , 78: isNatural^#(n__s(V1)) ->
             c_59(U121^#(isNatural(activate(V1))))
       , 79: isNatural^#(n__sel(V1, V2)) ->
             c_60(U131^#(isNatural(activate(V1)), activate(V2)))
       , 80: U204^#(pair(YS, ZS), X) ->
             c_62(pair^#(cons(activate(X), YS), ZS))
       , 81: U21^#(tt(), X, Y) ->
             c_63(U22^#(isLNat(activate(Y)), activate(X)))
       , 82: U22^#(tt(), X) -> c_64(activate^#(X))
       , 83: U211^#(tt(), XS) ->
             c_65(U212^#(isLNat(activate(XS)), activate(XS)))
       , 84: U212^#(tt(), XS) -> c_66(activate^#(XS))
       , 85: U221^#(tt(), N, XS) ->
             c_67(U222^#(isLNat(activate(XS)), activate(N), activate(XS)))
       , 86: U222^#(tt(), N, XS) ->
             c_68(fst^#(splitAt(activate(N), activate(XS))))
       , 87: U32^#(tt(), N) -> c_72(activate^#(N))
       , 88: U42^#(tt()) -> c_74()
       , 89: U52^#(tt()) -> c_76()
       , 90: isPLNat^#(n__pair(V1, V2)) ->
             c_81(U141^#(isLNat(activate(V1)), activate(V2)))
       , 91: isPLNat^#(n__splitAt(V1, V2)) ->
             c_82(U151^#(isNatural(activate(V1)), activate(V2))) }
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { U101^#(tt(), V2) -> c_1(U102^#(isLNat(activate(V2))))
     , isLNat^#(n__natsFrom(V1)) -> c_3(U71^#(isNatural(activate(V1))))
     , isLNat^#(n__afterNth(V1, V2)) ->
       c_5(U41^#(isNatural(activate(V1)), activate(V2)))
     , isLNat^#(n__cons(V1, V2)) ->
       c_6(U51^#(isNatural(activate(V1)), activate(V2)))
     , isLNat^#(n__fst(V1)) -> c_7(U61^#(isPLNat(activate(V1))))
     , isLNat^#(n__snd(V1)) -> c_8(U81^#(isPLNat(activate(V1))))
     , isLNat^#(n__tail(V1)) -> c_9(U91^#(isLNat(activate(V1))))
     , isLNat^#(n__take(V1, V2)) ->
       c_10(U101^#(isNatural(activate(V1)), activate(V2)))
     , U41^#(tt(), V2) -> c_73(U42^#(isLNat(activate(V2))))
     , U51^#(tt(), V2) -> c_75(U52^#(isLNat(activate(V2))))
     , activate^#(X) -> c_11(X)
     , activate^#(n__natsFrom(X)) -> c_12(natsFrom^#(X))
     , activate^#(n__nil()) -> c_13(nil^#())
     , activate^#(n__afterNth(X1, X2)) -> c_14(afterNth^#(X1, X2))
     , activate^#(n__cons(X1, X2)) -> c_15(cons^#(X1, X2))
     , activate^#(n__fst(X)) -> c_16(fst^#(X))
     , activate^#(n__snd(X)) -> c_17(snd^#(X))
     , activate^#(n__tail(X)) -> c_18(tail^#(X))
     , activate^#(n__take(X1, X2)) -> c_19(take^#(X1, X2))
     , activate^#(n__0()) -> c_20(0^#())
     , activate^#(n__head(X)) -> c_21(head^#(X))
     , activate^#(n__s(X)) -> c_22(s^#(X))
     , activate^#(n__sel(X1, X2)) -> c_23(sel^#(X1, X2))
     , activate^#(n__pair(X1, X2)) -> c_24(pair^#(X1, X2))
     , activate^#(n__splitAt(X1, X2)) -> c_25(splitAt^#(X1, X2))
     , natsFrom^#(N) -> c_83(U161^#(isNatural(N), N))
     , natsFrom^#(X) -> c_84(X)
     , afterNth^#(N, XS) -> c_48(U11^#(isNatural(N), N, XS))
     , afterNth^#(X1, X2) -> c_49(X1, X2)
     , cons^#(X1, X2) -> c_42(X1, X2)
     , fst^#(X) -> c_69(X)
     , fst^#(pair(X, Y)) -> c_70(U21^#(isLNat(X), X, Y))
     , snd^#(X) -> c_29(X)
     , snd^#(pair(X, Y)) -> c_30(U181^#(isLNat(X), Y))
     , tail^#(X) -> c_88(X)
     , tail^#(cons(N, XS)) -> c_89(U211^#(isNatural(N), activate(XS)))
     , take^#(N, XS) -> c_90(U221^#(isNatural(N), N, XS))
     , take^#(X1, X2) -> c_91(X1, X2)
     , head^#(X) -> c_46(X)
     , head^#(cons(N, XS)) -> c_47(U31^#(isNatural(N), N, activate(XS)))
     , s^#(X) -> c_43(X)
     , sel^#(N, XS) -> c_85(U171^#(isNatural(N), N, XS))
     , sel^#(X1, X2) -> c_86(X1, X2)
     , pair^#(X1, X2) -> c_53(X1, X2)
     , splitAt^#(X1, X2) -> c_31(X1, X2)
     , splitAt^#(s(N), cons(X, XS)) ->
       c_32(U201^#(isNatural(N), N, X, activate(XS)))
     , splitAt^#(0(), XS) -> c_33(U191^#(isLNat(XS), XS))
     , U11^#(tt(), N, XS) ->
       c_26(U12^#(isLNat(activate(XS)), activate(N), activate(XS)))
     , U12^#(tt(), N, XS) ->
       c_27(snd^#(splitAt(activate(N), activate(XS))))
     , U181^#(tt(), Y) -> c_50(U182^#(isLNat(activate(Y)), activate(Y)))
     , U201^#(tt(), N, X, XS) ->
       c_55(U202^#(isNatural(activate(X)),
                   activate(N),
                   activate(X),
                   activate(XS)))
     , U191^#(tt(), XS) -> c_52(pair^#(nil(), activate(XS)))
     , U131^#(tt(), V2) -> c_35(U132^#(isLNat(activate(V2))))
     , U141^#(tt(), V2) -> c_37(U142^#(isLNat(activate(V2))))
     , U151^#(tt(), V2) -> c_39(U152^#(isLNat(activate(V2))))
     , U161^#(tt(), N) ->
       c_41(cons^#(activate(N), n__natsFrom(s(activate(N)))))
     , U171^#(tt(), N, XS) ->
       c_44(U172^#(isLNat(activate(XS)), activate(N), activate(XS)))
     , U172^#(tt(), N, XS) ->
       c_45(head^#(afterNth(activate(N), activate(XS))))
     , U31^#(tt(), N, XS) ->
       c_71(U32^#(isLNat(activate(XS)), activate(N)))
     , U182^#(tt(), Y) -> c_51(activate^#(Y))
     , U202^#(tt(), N, X, XS) ->
       c_56(U203^#(isLNat(activate(XS)),
                   activate(N),
                   activate(X),
                   activate(XS)))
     , U203^#(tt(), N, X, XS) ->
       c_61(U204^#(splitAt(activate(N), activate(XS)), activate(X)))
     , isNatural^#(n__head(V1)) -> c_58(U111^#(isLNat(activate(V1))))
     , isNatural^#(n__s(V1)) -> c_59(U121^#(isNatural(activate(V1))))
     , isNatural^#(n__sel(V1, V2)) ->
       c_60(U131^#(isNatural(activate(V1)), activate(V2)))
     , U204^#(pair(YS, ZS), X) ->
       c_62(pair^#(cons(activate(X), YS), ZS))
     , U21^#(tt(), X, Y) ->
       c_63(U22^#(isLNat(activate(Y)), activate(X)))
     , U22^#(tt(), X) -> c_64(activate^#(X))
     , U211^#(tt(), XS) ->
       c_65(U212^#(isLNat(activate(XS)), activate(XS)))
     , U212^#(tt(), XS) -> c_66(activate^#(XS))
     , U221^#(tt(), N, XS) ->
       c_67(U222^#(isLNat(activate(XS)), activate(N), activate(XS)))
     , U222^#(tt(), N, XS) ->
       c_68(fst^#(splitAt(activate(N), activate(XS))))
     , U32^#(tt(), N) -> c_72(activate^#(N))
     , isPLNat^#(n__pair(V1, V2)) ->
       c_81(U141^#(isLNat(activate(V1)), activate(V2)))
     , isPLNat^#(n__splitAt(V1, V2)) ->
       c_82(U151^#(isNatural(activate(V1)), activate(V2))) }
   Strict Trs:
     { U101(tt(), V2) -> U102(isLNat(activate(V2)))
     , U102(tt()) -> tt()
     , isLNat(n__natsFrom(V1)) -> U71(isNatural(activate(V1)))
     , 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__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))
     , activate(X) -> X
     , 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)
     , U11(tt(), N, XS) ->
       U12(isLNat(activate(XS)), activate(N), activate(XS))
     , U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
     , U111(tt()) -> tt()
     , snd(X) -> n__snd(X)
     , snd(pair(X, Y)) -> U181(isLNat(X), Y)
     , splitAt(X1, X2) -> n__splitAt(X1, X2)
     , splitAt(s(N), cons(X, XS)) ->
       U201(isNatural(N), N, X, activate(XS))
     , splitAt(0(), XS) -> U191(isLNat(XS), 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(s(activate(N))))
     , cons(X1, X2) -> n__cons(X1, X2)
     , s(X) -> n__s(X)
     , U171(tt(), N, XS) ->
       U172(isLNat(activate(XS)), activate(N), activate(XS))
     , U172(tt(), N, XS) -> head(afterNth(activate(N), activate(XS)))
     , head(X) -> n__head(X)
     , head(cons(N, XS)) -> U31(isNatural(N), N, activate(XS))
     , afterNth(N, XS) -> U11(isNatural(N), N, XS)
     , afterNth(X1, X2) -> n__afterNth(X1, X2)
     , U181(tt(), Y) -> U182(isLNat(activate(Y)), activate(Y))
     , U182(tt(), Y) -> activate(Y)
     , U191(tt(), XS) -> pair(nil(), activate(XS))
     , pair(X1, X2) -> n__pair(X1, X2)
     , nil() -> n__nil()
     , 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))
     , 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))
     , 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))
     , U22(tt(), X) -> activate(X)
     , U211(tt(), XS) -> U212(isLNat(activate(XS)), activate(XS))
     , U212(tt(), XS) -> activate(XS)
     , U221(tt(), N, XS) ->
       U222(isLNat(activate(XS)), activate(N), activate(XS))
     , U222(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS)))
     , fst(X) -> n__fst(X)
     , fst(pair(X, Y)) -> U21(isLNat(X), X, Y)
     , 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()
     , 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)
     , natsFrom(X) -> n__natsFrom(X)
     , sel(N, XS) -> U171(isNatural(N), N, XS)
     , sel(X1, X2) -> n__sel(X1, X2)
     , 0() -> n__0()
     , tail(X) -> n__tail(X)
     , tail(cons(N, XS)) -> U211(isNatural(N), activate(XS))
     , take(N, XS) -> U221(isNatural(N), N, XS)
     , take(X1, X2) -> n__take(X1, X2) }
   Weak DPs:
     { U102^#(tt()) -> c_2()
     , isLNat^#(n__nil()) -> c_4()
     , U71^#(tt()) -> c_78()
     , U61^#(tt()) -> c_77()
     , U81^#(tt()) -> c_79()
     , U91^#(tt()) -> c_80()
     , nil^#() -> c_54()
     , 0^#() -> c_87()
     , U111^#(tt()) -> c_28()
     , U121^#(tt()) -> c_34()
     , U132^#(tt()) -> c_36()
     , U142^#(tt()) -> c_38()
     , U152^#(tt()) -> c_40()
     , isNatural^#(n__0()) -> c_57()
     , U42^#(tt()) -> c_74()
     , U52^#(tt()) -> c_76() }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   We estimate the number of application of
   {1,2,5,6,7,9,10,13,20,53,54,55,63,64} by applications of
   Pre({1,2,5,6,7,9,10,13,20,53,54,55,63,64}) =
   {3,4,8,11,27,29,30,31,33,35,38,39,41,43,44,45,60,65,68,70,73,74,75}.
   Here rules are labeled as follows:
   
     DPs:
       { 1: U101^#(tt(), V2) -> c_1(U102^#(isLNat(activate(V2))))
       , 2: isLNat^#(n__natsFrom(V1)) ->
            c_3(U71^#(isNatural(activate(V1))))
       , 3: isLNat^#(n__afterNth(V1, V2)) ->
            c_5(U41^#(isNatural(activate(V1)), activate(V2)))
       , 4: isLNat^#(n__cons(V1, V2)) ->
            c_6(U51^#(isNatural(activate(V1)), activate(V2)))
       , 5: isLNat^#(n__fst(V1)) -> c_7(U61^#(isPLNat(activate(V1))))
       , 6: isLNat^#(n__snd(V1)) -> c_8(U81^#(isPLNat(activate(V1))))
       , 7: isLNat^#(n__tail(V1)) -> c_9(U91^#(isLNat(activate(V1))))
       , 8: isLNat^#(n__take(V1, V2)) ->
            c_10(U101^#(isNatural(activate(V1)), activate(V2)))
       , 9: U41^#(tt(), V2) -> c_73(U42^#(isLNat(activate(V2))))
       , 10: U51^#(tt(), V2) -> c_75(U52^#(isLNat(activate(V2))))
       , 11: activate^#(X) -> c_11(X)
       , 12: activate^#(n__natsFrom(X)) -> c_12(natsFrom^#(X))
       , 13: activate^#(n__nil()) -> c_13(nil^#())
       , 14: activate^#(n__afterNth(X1, X2)) -> c_14(afterNth^#(X1, X2))
       , 15: activate^#(n__cons(X1, X2)) -> c_15(cons^#(X1, X2))
       , 16: activate^#(n__fst(X)) -> c_16(fst^#(X))
       , 17: activate^#(n__snd(X)) -> c_17(snd^#(X))
       , 18: activate^#(n__tail(X)) -> c_18(tail^#(X))
       , 19: activate^#(n__take(X1, X2)) -> c_19(take^#(X1, X2))
       , 20: activate^#(n__0()) -> c_20(0^#())
       , 21: activate^#(n__head(X)) -> c_21(head^#(X))
       , 22: activate^#(n__s(X)) -> c_22(s^#(X))
       , 23: activate^#(n__sel(X1, X2)) -> c_23(sel^#(X1, X2))
       , 24: activate^#(n__pair(X1, X2)) -> c_24(pair^#(X1, X2))
       , 25: activate^#(n__splitAt(X1, X2)) -> c_25(splitAt^#(X1, X2))
       , 26: natsFrom^#(N) -> c_83(U161^#(isNatural(N), N))
       , 27: natsFrom^#(X) -> c_84(X)
       , 28: afterNth^#(N, XS) -> c_48(U11^#(isNatural(N), N, XS))
       , 29: afterNth^#(X1, X2) -> c_49(X1, X2)
       , 30: cons^#(X1, X2) -> c_42(X1, X2)
       , 31: fst^#(X) -> c_69(X)
       , 32: fst^#(pair(X, Y)) -> c_70(U21^#(isLNat(X), X, Y))
       , 33: snd^#(X) -> c_29(X)
       , 34: snd^#(pair(X, Y)) -> c_30(U181^#(isLNat(X), Y))
       , 35: tail^#(X) -> c_88(X)
       , 36: tail^#(cons(N, XS)) ->
             c_89(U211^#(isNatural(N), activate(XS)))
       , 37: take^#(N, XS) -> c_90(U221^#(isNatural(N), N, XS))
       , 38: take^#(X1, X2) -> c_91(X1, X2)
       , 39: head^#(X) -> c_46(X)
       , 40: head^#(cons(N, XS)) ->
             c_47(U31^#(isNatural(N), N, activate(XS)))
       , 41: s^#(X) -> c_43(X)
       , 42: sel^#(N, XS) -> c_85(U171^#(isNatural(N), N, XS))
       , 43: sel^#(X1, X2) -> c_86(X1, X2)
       , 44: pair^#(X1, X2) -> c_53(X1, X2)
       , 45: splitAt^#(X1, X2) -> c_31(X1, X2)
       , 46: splitAt^#(s(N), cons(X, XS)) ->
             c_32(U201^#(isNatural(N), N, X, activate(XS)))
       , 47: splitAt^#(0(), XS) -> c_33(U191^#(isLNat(XS), XS))
       , 48: U11^#(tt(), N, XS) ->
             c_26(U12^#(isLNat(activate(XS)), activate(N), activate(XS)))
       , 49: U12^#(tt(), N, XS) ->
             c_27(snd^#(splitAt(activate(N), activate(XS))))
       , 50: U181^#(tt(), Y) ->
             c_50(U182^#(isLNat(activate(Y)), activate(Y)))
       , 51: U201^#(tt(), N, X, XS) ->
             c_55(U202^#(isNatural(activate(X)),
                         activate(N),
                         activate(X),
                         activate(XS)))
       , 52: U191^#(tt(), XS) -> c_52(pair^#(nil(), activate(XS)))
       , 53: U131^#(tt(), V2) -> c_35(U132^#(isLNat(activate(V2))))
       , 54: U141^#(tt(), V2) -> c_37(U142^#(isLNat(activate(V2))))
       , 55: U151^#(tt(), V2) -> c_39(U152^#(isLNat(activate(V2))))
       , 56: U161^#(tt(), N) ->
             c_41(cons^#(activate(N), n__natsFrom(s(activate(N)))))
       , 57: U171^#(tt(), N, XS) ->
             c_44(U172^#(isLNat(activate(XS)), activate(N), activate(XS)))
       , 58: U172^#(tt(), N, XS) ->
             c_45(head^#(afterNth(activate(N), activate(XS))))
       , 59: U31^#(tt(), N, XS) ->
             c_71(U32^#(isLNat(activate(XS)), activate(N)))
       , 60: U182^#(tt(), Y) -> c_51(activate^#(Y))
       , 61: U202^#(tt(), N, X, XS) ->
             c_56(U203^#(isLNat(activate(XS)),
                         activate(N),
                         activate(X),
                         activate(XS)))
       , 62: U203^#(tt(), N, X, XS) ->
             c_61(U204^#(splitAt(activate(N), activate(XS)), activate(X)))
       , 63: isNatural^#(n__head(V1)) ->
             c_58(U111^#(isLNat(activate(V1))))
       , 64: isNatural^#(n__s(V1)) ->
             c_59(U121^#(isNatural(activate(V1))))
       , 65: isNatural^#(n__sel(V1, V2)) ->
             c_60(U131^#(isNatural(activate(V1)), activate(V2)))
       , 66: U204^#(pair(YS, ZS), X) ->
             c_62(pair^#(cons(activate(X), YS), ZS))
       , 67: U21^#(tt(), X, Y) ->
             c_63(U22^#(isLNat(activate(Y)), activate(X)))
       , 68: U22^#(tt(), X) -> c_64(activate^#(X))
       , 69: U211^#(tt(), XS) ->
             c_65(U212^#(isLNat(activate(XS)), activate(XS)))
       , 70: U212^#(tt(), XS) -> c_66(activate^#(XS))
       , 71: U221^#(tt(), N, XS) ->
             c_67(U222^#(isLNat(activate(XS)), activate(N), activate(XS)))
       , 72: U222^#(tt(), N, XS) ->
             c_68(fst^#(splitAt(activate(N), activate(XS))))
       , 73: U32^#(tt(), N) -> c_72(activate^#(N))
       , 74: isPLNat^#(n__pair(V1, V2)) ->
             c_81(U141^#(isLNat(activate(V1)), activate(V2)))
       , 75: isPLNat^#(n__splitAt(V1, V2)) ->
             c_82(U151^#(isNatural(activate(V1)), activate(V2)))
       , 76: U102^#(tt()) -> c_2()
       , 77: isLNat^#(n__nil()) -> c_4()
       , 78: U71^#(tt()) -> c_78()
       , 79: U61^#(tt()) -> c_77()
       , 80: U81^#(tt()) -> c_79()
       , 81: U91^#(tt()) -> c_80()
       , 82: nil^#() -> c_54()
       , 83: 0^#() -> c_87()
       , 84: U111^#(tt()) -> c_28()
       , 85: U121^#(tt()) -> c_34()
       , 86: U132^#(tt()) -> c_36()
       , 87: U142^#(tt()) -> c_38()
       , 88: U152^#(tt()) -> c_40()
       , 89: isNatural^#(n__0()) -> c_57()
       , 90: U42^#(tt()) -> c_74()
       , 91: U52^#(tt()) -> c_76() }
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { isLNat^#(n__afterNth(V1, V2)) ->
       c_5(U41^#(isNatural(activate(V1)), activate(V2)))
     , isLNat^#(n__cons(V1, V2)) ->
       c_6(U51^#(isNatural(activate(V1)), activate(V2)))
     , isLNat^#(n__take(V1, V2)) ->
       c_10(U101^#(isNatural(activate(V1)), activate(V2)))
     , activate^#(X) -> c_11(X)
     , activate^#(n__natsFrom(X)) -> c_12(natsFrom^#(X))
     , activate^#(n__afterNth(X1, X2)) -> c_14(afterNth^#(X1, X2))
     , activate^#(n__cons(X1, X2)) -> c_15(cons^#(X1, X2))
     , activate^#(n__fst(X)) -> c_16(fst^#(X))
     , activate^#(n__snd(X)) -> c_17(snd^#(X))
     , activate^#(n__tail(X)) -> c_18(tail^#(X))
     , activate^#(n__take(X1, X2)) -> c_19(take^#(X1, X2))
     , activate^#(n__head(X)) -> c_21(head^#(X))
     , activate^#(n__s(X)) -> c_22(s^#(X))
     , activate^#(n__sel(X1, X2)) -> c_23(sel^#(X1, X2))
     , activate^#(n__pair(X1, X2)) -> c_24(pair^#(X1, X2))
     , activate^#(n__splitAt(X1, X2)) -> c_25(splitAt^#(X1, X2))
     , natsFrom^#(N) -> c_83(U161^#(isNatural(N), N))
     , natsFrom^#(X) -> c_84(X)
     , afterNth^#(N, XS) -> c_48(U11^#(isNatural(N), N, XS))
     , afterNth^#(X1, X2) -> c_49(X1, X2)
     , cons^#(X1, X2) -> c_42(X1, X2)
     , fst^#(X) -> c_69(X)
     , fst^#(pair(X, Y)) -> c_70(U21^#(isLNat(X), X, Y))
     , snd^#(X) -> c_29(X)
     , snd^#(pair(X, Y)) -> c_30(U181^#(isLNat(X), Y))
     , tail^#(X) -> c_88(X)
     , tail^#(cons(N, XS)) -> c_89(U211^#(isNatural(N), activate(XS)))
     , take^#(N, XS) -> c_90(U221^#(isNatural(N), N, XS))
     , take^#(X1, X2) -> c_91(X1, X2)
     , head^#(X) -> c_46(X)
     , head^#(cons(N, XS)) -> c_47(U31^#(isNatural(N), N, activate(XS)))
     , s^#(X) -> c_43(X)
     , sel^#(N, XS) -> c_85(U171^#(isNatural(N), N, XS))
     , sel^#(X1, X2) -> c_86(X1, X2)
     , pair^#(X1, X2) -> c_53(X1, X2)
     , splitAt^#(X1, X2) -> c_31(X1, X2)
     , splitAt^#(s(N), cons(X, XS)) ->
       c_32(U201^#(isNatural(N), N, X, activate(XS)))
     , splitAt^#(0(), XS) -> c_33(U191^#(isLNat(XS), XS))
     , U11^#(tt(), N, XS) ->
       c_26(U12^#(isLNat(activate(XS)), activate(N), activate(XS)))
     , U12^#(tt(), N, XS) ->
       c_27(snd^#(splitAt(activate(N), activate(XS))))
     , U181^#(tt(), Y) -> c_50(U182^#(isLNat(activate(Y)), activate(Y)))
     , U201^#(tt(), N, X, XS) ->
       c_55(U202^#(isNatural(activate(X)),
                   activate(N),
                   activate(X),
                   activate(XS)))
     , U191^#(tt(), XS) -> c_52(pair^#(nil(), activate(XS)))
     , U161^#(tt(), N) ->
       c_41(cons^#(activate(N), n__natsFrom(s(activate(N)))))
     , U171^#(tt(), N, XS) ->
       c_44(U172^#(isLNat(activate(XS)), activate(N), activate(XS)))
     , U172^#(tt(), N, XS) ->
       c_45(head^#(afterNth(activate(N), activate(XS))))
     , U31^#(tt(), N, XS) ->
       c_71(U32^#(isLNat(activate(XS)), activate(N)))
     , U182^#(tt(), Y) -> c_51(activate^#(Y))
     , U202^#(tt(), N, X, XS) ->
       c_56(U203^#(isLNat(activate(XS)),
                   activate(N),
                   activate(X),
                   activate(XS)))
     , U203^#(tt(), N, X, XS) ->
       c_61(U204^#(splitAt(activate(N), activate(XS)), activate(X)))
     , isNatural^#(n__sel(V1, V2)) ->
       c_60(U131^#(isNatural(activate(V1)), activate(V2)))
     , U204^#(pair(YS, ZS), X) ->
       c_62(pair^#(cons(activate(X), YS), ZS))
     , U21^#(tt(), X, Y) ->
       c_63(U22^#(isLNat(activate(Y)), activate(X)))
     , U22^#(tt(), X) -> c_64(activate^#(X))
     , U211^#(tt(), XS) ->
       c_65(U212^#(isLNat(activate(XS)), activate(XS)))
     , U212^#(tt(), XS) -> c_66(activate^#(XS))
     , U221^#(tt(), N, XS) ->
       c_67(U222^#(isLNat(activate(XS)), activate(N), activate(XS)))
     , U222^#(tt(), N, XS) ->
       c_68(fst^#(splitAt(activate(N), activate(XS))))
     , U32^#(tt(), N) -> c_72(activate^#(N))
     , isPLNat^#(n__pair(V1, V2)) ->
       c_81(U141^#(isLNat(activate(V1)), activate(V2)))
     , isPLNat^#(n__splitAt(V1, V2)) ->
       c_82(U151^#(isNatural(activate(V1)), activate(V2))) }
   Strict Trs:
     { U101(tt(), V2) -> U102(isLNat(activate(V2)))
     , U102(tt()) -> tt()
     , isLNat(n__natsFrom(V1)) -> U71(isNatural(activate(V1)))
     , 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__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))
     , activate(X) -> X
     , 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)
     , U11(tt(), N, XS) ->
       U12(isLNat(activate(XS)), activate(N), activate(XS))
     , U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
     , U111(tt()) -> tt()
     , snd(X) -> n__snd(X)
     , snd(pair(X, Y)) -> U181(isLNat(X), Y)
     , splitAt(X1, X2) -> n__splitAt(X1, X2)
     , splitAt(s(N), cons(X, XS)) ->
       U201(isNatural(N), N, X, activate(XS))
     , splitAt(0(), XS) -> U191(isLNat(XS), 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(s(activate(N))))
     , cons(X1, X2) -> n__cons(X1, X2)
     , s(X) -> n__s(X)
     , U171(tt(), N, XS) ->
       U172(isLNat(activate(XS)), activate(N), activate(XS))
     , U172(tt(), N, XS) -> head(afterNth(activate(N), activate(XS)))
     , head(X) -> n__head(X)
     , head(cons(N, XS)) -> U31(isNatural(N), N, activate(XS))
     , afterNth(N, XS) -> U11(isNatural(N), N, XS)
     , afterNth(X1, X2) -> n__afterNth(X1, X2)
     , U181(tt(), Y) -> U182(isLNat(activate(Y)), activate(Y))
     , U182(tt(), Y) -> activate(Y)
     , U191(tt(), XS) -> pair(nil(), activate(XS))
     , pair(X1, X2) -> n__pair(X1, X2)
     , nil() -> n__nil()
     , 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))
     , 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))
     , 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))
     , U22(tt(), X) -> activate(X)
     , U211(tt(), XS) -> U212(isLNat(activate(XS)), activate(XS))
     , U212(tt(), XS) -> activate(XS)
     , U221(tt(), N, XS) ->
       U222(isLNat(activate(XS)), activate(N), activate(XS))
     , U222(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS)))
     , fst(X) -> n__fst(X)
     , fst(pair(X, Y)) -> U21(isLNat(X), X, Y)
     , 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()
     , 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)
     , natsFrom(X) -> n__natsFrom(X)
     , sel(N, XS) -> U171(isNatural(N), N, XS)
     , sel(X1, X2) -> n__sel(X1, X2)
     , 0() -> n__0()
     , tail(X) -> n__tail(X)
     , tail(cons(N, XS)) -> U211(isNatural(N), activate(XS))
     , take(N, XS) -> U221(isNatural(N), N, XS)
     , take(X1, X2) -> n__take(X1, X2) }
   Weak DPs:
     { U101^#(tt(), V2) -> c_1(U102^#(isLNat(activate(V2))))
     , U102^#(tt()) -> c_2()
     , isLNat^#(n__natsFrom(V1)) -> c_3(U71^#(isNatural(activate(V1))))
     , isLNat^#(n__nil()) -> c_4()
     , isLNat^#(n__fst(V1)) -> c_7(U61^#(isPLNat(activate(V1))))
     , isLNat^#(n__snd(V1)) -> c_8(U81^#(isPLNat(activate(V1))))
     , isLNat^#(n__tail(V1)) -> c_9(U91^#(isLNat(activate(V1))))
     , U71^#(tt()) -> c_78()
     , U41^#(tt(), V2) -> c_73(U42^#(isLNat(activate(V2))))
     , U51^#(tt(), V2) -> c_75(U52^#(isLNat(activate(V2))))
     , U61^#(tt()) -> c_77()
     , U81^#(tt()) -> c_79()
     , U91^#(tt()) -> c_80()
     , activate^#(n__nil()) -> c_13(nil^#())
     , activate^#(n__0()) -> c_20(0^#())
     , nil^#() -> c_54()
     , 0^#() -> c_87()
     , U111^#(tt()) -> c_28()
     , U121^#(tt()) -> c_34()
     , U131^#(tt(), V2) -> c_35(U132^#(isLNat(activate(V2))))
     , U132^#(tt()) -> c_36()
     , U141^#(tt(), V2) -> c_37(U142^#(isLNat(activate(V2))))
     , U142^#(tt()) -> c_38()
     , U151^#(tt(), V2) -> c_39(U152^#(isLNat(activate(V2))))
     , U152^#(tt()) -> c_40()
     , isNatural^#(n__0()) -> c_57()
     , isNatural^#(n__head(V1)) -> c_58(U111^#(isLNat(activate(V1))))
     , isNatural^#(n__s(V1)) -> c_59(U121^#(isNatural(activate(V1))))
     , U42^#(tt()) -> c_74()
     , U52^#(tt()) -> c_76() }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   We estimate the number of application of {1,2,3,51,60,61} by
   applications of Pre({1,2,3,51,60,61}) =
   {4,18,20,21,22,24,26,29,30,32,34,35,36}. Here rules are labeled as
   follows:
   
     DPs:
       { 1: isLNat^#(n__afterNth(V1, V2)) ->
            c_5(U41^#(isNatural(activate(V1)), activate(V2)))
       , 2: isLNat^#(n__cons(V1, V2)) ->
            c_6(U51^#(isNatural(activate(V1)), activate(V2)))
       , 3: isLNat^#(n__take(V1, V2)) ->
            c_10(U101^#(isNatural(activate(V1)), activate(V2)))
       , 4: activate^#(X) -> c_11(X)
       , 5: activate^#(n__natsFrom(X)) -> c_12(natsFrom^#(X))
       , 6: activate^#(n__afterNth(X1, X2)) -> c_14(afterNth^#(X1, X2))
       , 7: activate^#(n__cons(X1, X2)) -> c_15(cons^#(X1, X2))
       , 8: activate^#(n__fst(X)) -> c_16(fst^#(X))
       , 9: activate^#(n__snd(X)) -> c_17(snd^#(X))
       , 10: activate^#(n__tail(X)) -> c_18(tail^#(X))
       , 11: activate^#(n__take(X1, X2)) -> c_19(take^#(X1, X2))
       , 12: activate^#(n__head(X)) -> c_21(head^#(X))
       , 13: activate^#(n__s(X)) -> c_22(s^#(X))
       , 14: activate^#(n__sel(X1, X2)) -> c_23(sel^#(X1, X2))
       , 15: activate^#(n__pair(X1, X2)) -> c_24(pair^#(X1, X2))
       , 16: activate^#(n__splitAt(X1, X2)) -> c_25(splitAt^#(X1, X2))
       , 17: natsFrom^#(N) -> c_83(U161^#(isNatural(N), N))
       , 18: natsFrom^#(X) -> c_84(X)
       , 19: afterNth^#(N, XS) -> c_48(U11^#(isNatural(N), N, XS))
       , 20: afterNth^#(X1, X2) -> c_49(X1, X2)
       , 21: cons^#(X1, X2) -> c_42(X1, X2)
       , 22: fst^#(X) -> c_69(X)
       , 23: fst^#(pair(X, Y)) -> c_70(U21^#(isLNat(X), X, Y))
       , 24: snd^#(X) -> c_29(X)
       , 25: snd^#(pair(X, Y)) -> c_30(U181^#(isLNat(X), Y))
       , 26: tail^#(X) -> c_88(X)
       , 27: tail^#(cons(N, XS)) ->
             c_89(U211^#(isNatural(N), activate(XS)))
       , 28: take^#(N, XS) -> c_90(U221^#(isNatural(N), N, XS))
       , 29: take^#(X1, X2) -> c_91(X1, X2)
       , 30: head^#(X) -> c_46(X)
       , 31: head^#(cons(N, XS)) ->
             c_47(U31^#(isNatural(N), N, activate(XS)))
       , 32: s^#(X) -> c_43(X)
       , 33: sel^#(N, XS) -> c_85(U171^#(isNatural(N), N, XS))
       , 34: sel^#(X1, X2) -> c_86(X1, X2)
       , 35: pair^#(X1, X2) -> c_53(X1, X2)
       , 36: splitAt^#(X1, X2) -> c_31(X1, X2)
       , 37: splitAt^#(s(N), cons(X, XS)) ->
             c_32(U201^#(isNatural(N), N, X, activate(XS)))
       , 38: splitAt^#(0(), XS) -> c_33(U191^#(isLNat(XS), XS))
       , 39: U11^#(tt(), N, XS) ->
             c_26(U12^#(isLNat(activate(XS)), activate(N), activate(XS)))
       , 40: U12^#(tt(), N, XS) ->
             c_27(snd^#(splitAt(activate(N), activate(XS))))
       , 41: U181^#(tt(), Y) ->
             c_50(U182^#(isLNat(activate(Y)), activate(Y)))
       , 42: U201^#(tt(), N, X, XS) ->
             c_55(U202^#(isNatural(activate(X)),
                         activate(N),
                         activate(X),
                         activate(XS)))
       , 43: U191^#(tt(), XS) -> c_52(pair^#(nil(), activate(XS)))
       , 44: U161^#(tt(), N) ->
             c_41(cons^#(activate(N), n__natsFrom(s(activate(N)))))
       , 45: U171^#(tt(), N, XS) ->
             c_44(U172^#(isLNat(activate(XS)), activate(N), activate(XS)))
       , 46: U172^#(tt(), N, XS) ->
             c_45(head^#(afterNth(activate(N), activate(XS))))
       , 47: U31^#(tt(), N, XS) ->
             c_71(U32^#(isLNat(activate(XS)), activate(N)))
       , 48: U182^#(tt(), Y) -> c_51(activate^#(Y))
       , 49: U202^#(tt(), N, X, XS) ->
             c_56(U203^#(isLNat(activate(XS)),
                         activate(N),
                         activate(X),
                         activate(XS)))
       , 50: U203^#(tt(), N, X, XS) ->
             c_61(U204^#(splitAt(activate(N), activate(XS)), activate(X)))
       , 51: isNatural^#(n__sel(V1, V2)) ->
             c_60(U131^#(isNatural(activate(V1)), activate(V2)))
       , 52: U204^#(pair(YS, ZS), X) ->
             c_62(pair^#(cons(activate(X), YS), ZS))
       , 53: U21^#(tt(), X, Y) ->
             c_63(U22^#(isLNat(activate(Y)), activate(X)))
       , 54: U22^#(tt(), X) -> c_64(activate^#(X))
       , 55: U211^#(tt(), XS) ->
             c_65(U212^#(isLNat(activate(XS)), activate(XS)))
       , 56: U212^#(tt(), XS) -> c_66(activate^#(XS))
       , 57: U221^#(tt(), N, XS) ->
             c_67(U222^#(isLNat(activate(XS)), activate(N), activate(XS)))
       , 58: U222^#(tt(), N, XS) ->
             c_68(fst^#(splitAt(activate(N), activate(XS))))
       , 59: U32^#(tt(), N) -> c_72(activate^#(N))
       , 60: isPLNat^#(n__pair(V1, V2)) ->
             c_81(U141^#(isLNat(activate(V1)), activate(V2)))
       , 61: isPLNat^#(n__splitAt(V1, V2)) ->
             c_82(U151^#(isNatural(activate(V1)), activate(V2)))
       , 62: U101^#(tt(), V2) -> c_1(U102^#(isLNat(activate(V2))))
       , 63: U102^#(tt()) -> c_2()
       , 64: isLNat^#(n__natsFrom(V1)) ->
             c_3(U71^#(isNatural(activate(V1))))
       , 65: isLNat^#(n__nil()) -> c_4()
       , 66: isLNat^#(n__fst(V1)) -> c_7(U61^#(isPLNat(activate(V1))))
       , 67: isLNat^#(n__snd(V1)) -> c_8(U81^#(isPLNat(activate(V1))))
       , 68: isLNat^#(n__tail(V1)) -> c_9(U91^#(isLNat(activate(V1))))
       , 69: U71^#(tt()) -> c_78()
       , 70: U41^#(tt(), V2) -> c_73(U42^#(isLNat(activate(V2))))
       , 71: U51^#(tt(), V2) -> c_75(U52^#(isLNat(activate(V2))))
       , 72: U61^#(tt()) -> c_77()
       , 73: U81^#(tt()) -> c_79()
       , 74: U91^#(tt()) -> c_80()
       , 75: activate^#(n__nil()) -> c_13(nil^#())
       , 76: activate^#(n__0()) -> c_20(0^#())
       , 77: nil^#() -> c_54()
       , 78: 0^#() -> c_87()
       , 79: U111^#(tt()) -> c_28()
       , 80: U121^#(tt()) -> c_34()
       , 81: U131^#(tt(), V2) -> c_35(U132^#(isLNat(activate(V2))))
       , 82: U132^#(tt()) -> c_36()
       , 83: U141^#(tt(), V2) -> c_37(U142^#(isLNat(activate(V2))))
       , 84: U142^#(tt()) -> c_38()
       , 85: U151^#(tt(), V2) -> c_39(U152^#(isLNat(activate(V2))))
       , 86: U152^#(tt()) -> c_40()
       , 87: isNatural^#(n__0()) -> c_57()
       , 88: isNatural^#(n__head(V1)) ->
             c_58(U111^#(isLNat(activate(V1))))
       , 89: isNatural^#(n__s(V1)) ->
             c_59(U121^#(isNatural(activate(V1))))
       , 90: U42^#(tt()) -> c_74()
       , 91: U52^#(tt()) -> c_76() }
   
   We are left with following problem, upon which TcT provides the
   certificate MAYBE.
   
   Strict DPs:
     { activate^#(X) -> c_11(X)
     , activate^#(n__natsFrom(X)) -> c_12(natsFrom^#(X))
     , activate^#(n__afterNth(X1, X2)) -> c_14(afterNth^#(X1, X2))
     , activate^#(n__cons(X1, X2)) -> c_15(cons^#(X1, X2))
     , activate^#(n__fst(X)) -> c_16(fst^#(X))
     , activate^#(n__snd(X)) -> c_17(snd^#(X))
     , activate^#(n__tail(X)) -> c_18(tail^#(X))
     , activate^#(n__take(X1, X2)) -> c_19(take^#(X1, X2))
     , activate^#(n__head(X)) -> c_21(head^#(X))
     , activate^#(n__s(X)) -> c_22(s^#(X))
     , activate^#(n__sel(X1, X2)) -> c_23(sel^#(X1, X2))
     , activate^#(n__pair(X1, X2)) -> c_24(pair^#(X1, X2))
     , activate^#(n__splitAt(X1, X2)) -> c_25(splitAt^#(X1, X2))
     , natsFrom^#(N) -> c_83(U161^#(isNatural(N), N))
     , natsFrom^#(X) -> c_84(X)
     , afterNth^#(N, XS) -> c_48(U11^#(isNatural(N), N, XS))
     , afterNth^#(X1, X2) -> c_49(X1, X2)
     , cons^#(X1, X2) -> c_42(X1, X2)
     , fst^#(X) -> c_69(X)
     , fst^#(pair(X, Y)) -> c_70(U21^#(isLNat(X), X, Y))
     , snd^#(X) -> c_29(X)
     , snd^#(pair(X, Y)) -> c_30(U181^#(isLNat(X), Y))
     , tail^#(X) -> c_88(X)
     , tail^#(cons(N, XS)) -> c_89(U211^#(isNatural(N), activate(XS)))
     , take^#(N, XS) -> c_90(U221^#(isNatural(N), N, XS))
     , take^#(X1, X2) -> c_91(X1, X2)
     , head^#(X) -> c_46(X)
     , head^#(cons(N, XS)) -> c_47(U31^#(isNatural(N), N, activate(XS)))
     , s^#(X) -> c_43(X)
     , sel^#(N, XS) -> c_85(U171^#(isNatural(N), N, XS))
     , sel^#(X1, X2) -> c_86(X1, X2)
     , pair^#(X1, X2) -> c_53(X1, X2)
     , splitAt^#(X1, X2) -> c_31(X1, X2)
     , splitAt^#(s(N), cons(X, XS)) ->
       c_32(U201^#(isNatural(N), N, X, activate(XS)))
     , splitAt^#(0(), XS) -> c_33(U191^#(isLNat(XS), XS))
     , U11^#(tt(), N, XS) ->
       c_26(U12^#(isLNat(activate(XS)), activate(N), activate(XS)))
     , U12^#(tt(), N, XS) ->
       c_27(snd^#(splitAt(activate(N), activate(XS))))
     , U181^#(tt(), Y) -> c_50(U182^#(isLNat(activate(Y)), activate(Y)))
     , U201^#(tt(), N, X, XS) ->
       c_55(U202^#(isNatural(activate(X)),
                   activate(N),
                   activate(X),
                   activate(XS)))
     , U191^#(tt(), XS) -> c_52(pair^#(nil(), activate(XS)))
     , U161^#(tt(), N) ->
       c_41(cons^#(activate(N), n__natsFrom(s(activate(N)))))
     , U171^#(tt(), N, XS) ->
       c_44(U172^#(isLNat(activate(XS)), activate(N), activate(XS)))
     , U172^#(tt(), N, XS) ->
       c_45(head^#(afterNth(activate(N), activate(XS))))
     , U31^#(tt(), N, XS) ->
       c_71(U32^#(isLNat(activate(XS)), activate(N)))
     , U182^#(tt(), Y) -> c_51(activate^#(Y))
     , U202^#(tt(), N, X, XS) ->
       c_56(U203^#(isLNat(activate(XS)),
                   activate(N),
                   activate(X),
                   activate(XS)))
     , U203^#(tt(), N, X, XS) ->
       c_61(U204^#(splitAt(activate(N), activate(XS)), activate(X)))
     , U204^#(pair(YS, ZS), X) ->
       c_62(pair^#(cons(activate(X), YS), ZS))
     , U21^#(tt(), X, Y) ->
       c_63(U22^#(isLNat(activate(Y)), activate(X)))
     , U22^#(tt(), X) -> c_64(activate^#(X))
     , U211^#(tt(), XS) ->
       c_65(U212^#(isLNat(activate(XS)), activate(XS)))
     , U212^#(tt(), XS) -> c_66(activate^#(XS))
     , U221^#(tt(), N, XS) ->
       c_67(U222^#(isLNat(activate(XS)), activate(N), activate(XS)))
     , U222^#(tt(), N, XS) ->
       c_68(fst^#(splitAt(activate(N), activate(XS))))
     , U32^#(tt(), N) -> c_72(activate^#(N)) }
   Strict Trs:
     { U101(tt(), V2) -> U102(isLNat(activate(V2)))
     , U102(tt()) -> tt()
     , isLNat(n__natsFrom(V1)) -> U71(isNatural(activate(V1)))
     , 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__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))
     , activate(X) -> X
     , 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)
     , U11(tt(), N, XS) ->
       U12(isLNat(activate(XS)), activate(N), activate(XS))
     , U12(tt(), N, XS) -> snd(splitAt(activate(N), activate(XS)))
     , U111(tt()) -> tt()
     , snd(X) -> n__snd(X)
     , snd(pair(X, Y)) -> U181(isLNat(X), Y)
     , splitAt(X1, X2) -> n__splitAt(X1, X2)
     , splitAt(s(N), cons(X, XS)) ->
       U201(isNatural(N), N, X, activate(XS))
     , splitAt(0(), XS) -> U191(isLNat(XS), 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(s(activate(N))))
     , cons(X1, X2) -> n__cons(X1, X2)
     , s(X) -> n__s(X)
     , U171(tt(), N, XS) ->
       U172(isLNat(activate(XS)), activate(N), activate(XS))
     , U172(tt(), N, XS) -> head(afterNth(activate(N), activate(XS)))
     , head(X) -> n__head(X)
     , head(cons(N, XS)) -> U31(isNatural(N), N, activate(XS))
     , afterNth(N, XS) -> U11(isNatural(N), N, XS)
     , afterNth(X1, X2) -> n__afterNth(X1, X2)
     , U181(tt(), Y) -> U182(isLNat(activate(Y)), activate(Y))
     , U182(tt(), Y) -> activate(Y)
     , U191(tt(), XS) -> pair(nil(), activate(XS))
     , pair(X1, X2) -> n__pair(X1, X2)
     , nil() -> n__nil()
     , 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))
     , 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))
     , 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))
     , U22(tt(), X) -> activate(X)
     , U211(tt(), XS) -> U212(isLNat(activate(XS)), activate(XS))
     , U212(tt(), XS) -> activate(XS)
     , U221(tt(), N, XS) ->
       U222(isLNat(activate(XS)), activate(N), activate(XS))
     , U222(tt(), N, XS) -> fst(splitAt(activate(N), activate(XS)))
     , fst(X) -> n__fst(X)
     , fst(pair(X, Y)) -> U21(isLNat(X), X, Y)
     , 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()
     , 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)
     , natsFrom(X) -> n__natsFrom(X)
     , sel(N, XS) -> U171(isNatural(N), N, XS)
     , sel(X1, X2) -> n__sel(X1, X2)
     , 0() -> n__0()
     , tail(X) -> n__tail(X)
     , tail(cons(N, XS)) -> U211(isNatural(N), activate(XS))
     , take(N, XS) -> U221(isNatural(N), N, XS)
     , take(X1, X2) -> n__take(X1, X2) }
   Weak DPs:
     { U101^#(tt(), V2) -> c_1(U102^#(isLNat(activate(V2))))
     , U102^#(tt()) -> c_2()
     , isLNat^#(n__natsFrom(V1)) -> c_3(U71^#(isNatural(activate(V1))))
     , isLNat^#(n__nil()) -> c_4()
     , isLNat^#(n__afterNth(V1, V2)) ->
       c_5(U41^#(isNatural(activate(V1)), activate(V2)))
     , isLNat^#(n__cons(V1, V2)) ->
       c_6(U51^#(isNatural(activate(V1)), activate(V2)))
     , isLNat^#(n__fst(V1)) -> c_7(U61^#(isPLNat(activate(V1))))
     , isLNat^#(n__snd(V1)) -> c_8(U81^#(isPLNat(activate(V1))))
     , isLNat^#(n__tail(V1)) -> c_9(U91^#(isLNat(activate(V1))))
     , isLNat^#(n__take(V1, V2)) ->
       c_10(U101^#(isNatural(activate(V1)), activate(V2)))
     , U71^#(tt()) -> c_78()
     , U41^#(tt(), V2) -> c_73(U42^#(isLNat(activate(V2))))
     , U51^#(tt(), V2) -> c_75(U52^#(isLNat(activate(V2))))
     , U61^#(tt()) -> c_77()
     , U81^#(tt()) -> c_79()
     , U91^#(tt()) -> c_80()
     , activate^#(n__nil()) -> c_13(nil^#())
     , activate^#(n__0()) -> c_20(0^#())
     , nil^#() -> c_54()
     , 0^#() -> c_87()
     , U111^#(tt()) -> c_28()
     , U121^#(tt()) -> c_34()
     , U131^#(tt(), V2) -> c_35(U132^#(isLNat(activate(V2))))
     , U132^#(tt()) -> c_36()
     , U141^#(tt(), V2) -> c_37(U142^#(isLNat(activate(V2))))
     , U142^#(tt()) -> c_38()
     , U151^#(tt(), V2) -> c_39(U152^#(isLNat(activate(V2))))
     , U152^#(tt()) -> c_40()
     , isNatural^#(n__0()) -> c_57()
     , isNatural^#(n__head(V1)) -> c_58(U111^#(isLNat(activate(V1))))
     , isNatural^#(n__s(V1)) -> c_59(U121^#(isNatural(activate(V1))))
     , isNatural^#(n__sel(V1, V2)) ->
       c_60(U131^#(isNatural(activate(V1)), activate(V2)))
     , U42^#(tt()) -> c_74()
     , U52^#(tt()) -> c_76()
     , isPLNat^#(n__pair(V1, V2)) ->
       c_81(U141^#(isLNat(activate(V1)), activate(V2)))
     , isPLNat^#(n__splitAt(V1, V2)) ->
       c_82(U151^#(isNatural(activate(V1)), activate(V2))) }
   Obligation:
     runtime complexity
   Answer:
     MAYBE
   
   Empty strict component of the problem is NOT empty.


Arrrr..