YES(?,O(n^1))

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).

Strict Trs:
  { U11(tt(), N, X, XS) ->
    U12(splitAt(activate(N), activate(XS)), activate(X))
  , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS)
  , splitAt(s(N), cons(X, XS)) -> U11(tt(), N, X, activate(XS))
  , splitAt(0(), XS) -> pair(nil(), XS)
  , activate(X) -> X
  , activate(n__natsFrom(X)) -> natsFrom(X)
  , afterNth(N, XS) -> snd(splitAt(N, XS))
  , snd(pair(X, Y)) -> Y
  , and(tt(), X) -> activate(X)
  , fst(pair(X, Y)) -> X
  , head(cons(N, XS)) -> N
  , natsFrom(N) -> cons(N, n__natsFrom(s(N)))
  , natsFrom(X) -> n__natsFrom(X)
  , sel(N, XS) -> head(afterNth(N, XS))
  , tail(cons(N, XS)) -> activate(XS)
  , take(N, XS) -> fst(splitAt(N, XS)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

We add following dependency tuples:

Strict DPs:
  { U11^#(tt(), N, X, XS) ->
    c_1(U12^#(splitAt(activate(N), activate(XS)), activate(X)),
        splitAt^#(activate(N), activate(XS)),
        activate^#(N),
        activate^#(XS),
        activate^#(X))
  , U12^#(pair(YS, ZS), X) -> c_2(activate^#(X))
  , splitAt^#(s(N), cons(X, XS)) ->
    c_3(U11^#(tt(), N, X, activate(XS)), activate^#(XS))
  , splitAt^#(0(), XS) -> c_4()
  , activate^#(X) -> c_5()
  , activate^#(n__natsFrom(X)) -> c_6(natsFrom^#(X))
  , natsFrom^#(N) -> c_12()
  , natsFrom^#(X) -> c_13()
  , afterNth^#(N, XS) -> c_7(snd^#(splitAt(N, XS)), splitAt^#(N, XS))
  , snd^#(pair(X, Y)) -> c_8()
  , and^#(tt(), X) -> c_9(activate^#(X))
  , fst^#(pair(X, Y)) -> c_10()
  , head^#(cons(N, XS)) -> c_11()
  , sel^#(N, XS) -> c_14(head^#(afterNth(N, XS)), afterNth^#(N, XS))
  , tail^#(cons(N, XS)) -> c_15(activate^#(XS))
  , take^#(N, XS) -> c_16(fst^#(splitAt(N, XS)), splitAt^#(N, XS)) }

and mark the set of starting terms.

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).

Strict DPs:
  { U11^#(tt(), N, X, XS) ->
    c_1(U12^#(splitAt(activate(N), activate(XS)), activate(X)),
        splitAt^#(activate(N), activate(XS)),
        activate^#(N),
        activate^#(XS),
        activate^#(X))
  , U12^#(pair(YS, ZS), X) -> c_2(activate^#(X))
  , splitAt^#(s(N), cons(X, XS)) ->
    c_3(U11^#(tt(), N, X, activate(XS)), activate^#(XS))
  , splitAt^#(0(), XS) -> c_4()
  , activate^#(X) -> c_5()
  , activate^#(n__natsFrom(X)) -> c_6(natsFrom^#(X))
  , natsFrom^#(N) -> c_12()
  , natsFrom^#(X) -> c_13()
  , afterNth^#(N, XS) -> c_7(snd^#(splitAt(N, XS)), splitAt^#(N, XS))
  , snd^#(pair(X, Y)) -> c_8()
  , and^#(tt(), X) -> c_9(activate^#(X))
  , fst^#(pair(X, Y)) -> c_10()
  , head^#(cons(N, XS)) -> c_11()
  , sel^#(N, XS) -> c_14(head^#(afterNth(N, XS)), afterNth^#(N, XS))
  , tail^#(cons(N, XS)) -> c_15(activate^#(XS))
  , take^#(N, XS) -> c_16(fst^#(splitAt(N, XS)), splitAt^#(N, XS)) }
Weak Trs:
  { U11(tt(), N, X, XS) ->
    U12(splitAt(activate(N), activate(XS)), activate(X))
  , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS)
  , splitAt(s(N), cons(X, XS)) -> U11(tt(), N, X, activate(XS))
  , splitAt(0(), XS) -> pair(nil(), XS)
  , activate(X) -> X
  , activate(n__natsFrom(X)) -> natsFrom(X)
  , afterNth(N, XS) -> snd(splitAt(N, XS))
  , snd(pair(X, Y)) -> Y
  , and(tt(), X) -> activate(X)
  , fst(pair(X, Y)) -> X
  , head(cons(N, XS)) -> N
  , natsFrom(N) -> cons(N, n__natsFrom(s(N)))
  , natsFrom(X) -> n__natsFrom(X)
  , sel(N, XS) -> head(afterNth(N, XS))
  , tail(cons(N, XS)) -> activate(XS)
  , take(N, XS) -> fst(splitAt(N, XS)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

We estimate the number of application of {4,5,7,8,10,12,13} by
applications of Pre({4,5,7,8,10,12,13}) = {1,2,3,6,9,11,14,15,16}.
Here rules are labeled as follows:

  DPs:
    { 1: U11^#(tt(), N, X, XS) ->
         c_1(U12^#(splitAt(activate(N), activate(XS)), activate(X)),
             splitAt^#(activate(N), activate(XS)),
             activate^#(N),
             activate^#(XS),
             activate^#(X))
    , 2: U12^#(pair(YS, ZS), X) -> c_2(activate^#(X))
    , 3: splitAt^#(s(N), cons(X, XS)) ->
         c_3(U11^#(tt(), N, X, activate(XS)), activate^#(XS))
    , 4: splitAt^#(0(), XS) -> c_4()
    , 5: activate^#(X) -> c_5()
    , 6: activate^#(n__natsFrom(X)) -> c_6(natsFrom^#(X))
    , 7: natsFrom^#(N) -> c_12()
    , 8: natsFrom^#(X) -> c_13()
    , 9: afterNth^#(N, XS) ->
         c_7(snd^#(splitAt(N, XS)), splitAt^#(N, XS))
    , 10: snd^#(pair(X, Y)) -> c_8()
    , 11: and^#(tt(), X) -> c_9(activate^#(X))
    , 12: fst^#(pair(X, Y)) -> c_10()
    , 13: head^#(cons(N, XS)) -> c_11()
    , 14: sel^#(N, XS) ->
          c_14(head^#(afterNth(N, XS)), afterNth^#(N, XS))
    , 15: tail^#(cons(N, XS)) -> c_15(activate^#(XS))
    , 16: take^#(N, XS) ->
          c_16(fst^#(splitAt(N, XS)), splitAt^#(N, XS)) }

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).

Strict DPs:
  { U11^#(tt(), N, X, XS) ->
    c_1(U12^#(splitAt(activate(N), activate(XS)), activate(X)),
        splitAt^#(activate(N), activate(XS)),
        activate^#(N),
        activate^#(XS),
        activate^#(X))
  , U12^#(pair(YS, ZS), X) -> c_2(activate^#(X))
  , splitAt^#(s(N), cons(X, XS)) ->
    c_3(U11^#(tt(), N, X, activate(XS)), activate^#(XS))
  , activate^#(n__natsFrom(X)) -> c_6(natsFrom^#(X))
  , afterNth^#(N, XS) -> c_7(snd^#(splitAt(N, XS)), splitAt^#(N, XS))
  , and^#(tt(), X) -> c_9(activate^#(X))
  , sel^#(N, XS) -> c_14(head^#(afterNth(N, XS)), afterNth^#(N, XS))
  , tail^#(cons(N, XS)) -> c_15(activate^#(XS))
  , take^#(N, XS) -> c_16(fst^#(splitAt(N, XS)), splitAt^#(N, XS)) }
Weak DPs:
  { splitAt^#(0(), XS) -> c_4()
  , activate^#(X) -> c_5()
  , natsFrom^#(N) -> c_12()
  , natsFrom^#(X) -> c_13()
  , snd^#(pair(X, Y)) -> c_8()
  , fst^#(pair(X, Y)) -> c_10()
  , head^#(cons(N, XS)) -> c_11() }
Weak Trs:
  { U11(tt(), N, X, XS) ->
    U12(splitAt(activate(N), activate(XS)), activate(X))
  , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS)
  , splitAt(s(N), cons(X, XS)) -> U11(tt(), N, X, activate(XS))
  , splitAt(0(), XS) -> pair(nil(), XS)
  , activate(X) -> X
  , activate(n__natsFrom(X)) -> natsFrom(X)
  , afterNth(N, XS) -> snd(splitAt(N, XS))
  , snd(pair(X, Y)) -> Y
  , and(tt(), X) -> activate(X)
  , fst(pair(X, Y)) -> X
  , head(cons(N, XS)) -> N
  , natsFrom(N) -> cons(N, n__natsFrom(s(N)))
  , natsFrom(X) -> n__natsFrom(X)
  , sel(N, XS) -> head(afterNth(N, XS))
  , tail(cons(N, XS)) -> activate(XS)
  , take(N, XS) -> fst(splitAt(N, XS)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

We estimate the number of application of {4} by applications of
Pre({4}) = {1,2,3,6,8}. Here rules are labeled as follows:

  DPs:
    { 1: U11^#(tt(), N, X, XS) ->
         c_1(U12^#(splitAt(activate(N), activate(XS)), activate(X)),
             splitAt^#(activate(N), activate(XS)),
             activate^#(N),
             activate^#(XS),
             activate^#(X))
    , 2: U12^#(pair(YS, ZS), X) -> c_2(activate^#(X))
    , 3: splitAt^#(s(N), cons(X, XS)) ->
         c_3(U11^#(tt(), N, X, activate(XS)), activate^#(XS))
    , 4: activate^#(n__natsFrom(X)) -> c_6(natsFrom^#(X))
    , 5: afterNth^#(N, XS) ->
         c_7(snd^#(splitAt(N, XS)), splitAt^#(N, XS))
    , 6: and^#(tt(), X) -> c_9(activate^#(X))
    , 7: sel^#(N, XS) ->
         c_14(head^#(afterNth(N, XS)), afterNth^#(N, XS))
    , 8: tail^#(cons(N, XS)) -> c_15(activate^#(XS))
    , 9: take^#(N, XS) -> c_16(fst^#(splitAt(N, XS)), splitAt^#(N, XS))
    , 10: splitAt^#(0(), XS) -> c_4()
    , 11: activate^#(X) -> c_5()
    , 12: natsFrom^#(N) -> c_12()
    , 13: natsFrom^#(X) -> c_13()
    , 14: snd^#(pair(X, Y)) -> c_8()
    , 15: fst^#(pair(X, Y)) -> c_10()
    , 16: head^#(cons(N, XS)) -> c_11() }

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).

Strict DPs:
  { U11^#(tt(), N, X, XS) ->
    c_1(U12^#(splitAt(activate(N), activate(XS)), activate(X)),
        splitAt^#(activate(N), activate(XS)),
        activate^#(N),
        activate^#(XS),
        activate^#(X))
  , U12^#(pair(YS, ZS), X) -> c_2(activate^#(X))
  , splitAt^#(s(N), cons(X, XS)) ->
    c_3(U11^#(tt(), N, X, activate(XS)), activate^#(XS))
  , afterNth^#(N, XS) -> c_7(snd^#(splitAt(N, XS)), splitAt^#(N, XS))
  , and^#(tt(), X) -> c_9(activate^#(X))
  , sel^#(N, XS) -> c_14(head^#(afterNth(N, XS)), afterNth^#(N, XS))
  , tail^#(cons(N, XS)) -> c_15(activate^#(XS))
  , take^#(N, XS) -> c_16(fst^#(splitAt(N, XS)), splitAt^#(N, XS)) }
Weak DPs:
  { splitAt^#(0(), XS) -> c_4()
  , activate^#(X) -> c_5()
  , activate^#(n__natsFrom(X)) -> c_6(natsFrom^#(X))
  , natsFrom^#(N) -> c_12()
  , natsFrom^#(X) -> c_13()
  , snd^#(pair(X, Y)) -> c_8()
  , fst^#(pair(X, Y)) -> c_10()
  , head^#(cons(N, XS)) -> c_11() }
Weak Trs:
  { U11(tt(), N, X, XS) ->
    U12(splitAt(activate(N), activate(XS)), activate(X))
  , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS)
  , splitAt(s(N), cons(X, XS)) -> U11(tt(), N, X, activate(XS))
  , splitAt(0(), XS) -> pair(nil(), XS)
  , activate(X) -> X
  , activate(n__natsFrom(X)) -> natsFrom(X)
  , afterNth(N, XS) -> snd(splitAt(N, XS))
  , snd(pair(X, Y)) -> Y
  , and(tt(), X) -> activate(X)
  , fst(pair(X, Y)) -> X
  , head(cons(N, XS)) -> N
  , natsFrom(N) -> cons(N, n__natsFrom(s(N)))
  , natsFrom(X) -> n__natsFrom(X)
  , sel(N, XS) -> head(afterNth(N, XS))
  , tail(cons(N, XS)) -> activate(XS)
  , take(N, XS) -> fst(splitAt(N, XS)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

We estimate the number of application of {2,5,7} by applications of
Pre({2,5,7}) = {1}. Here rules are labeled as follows:

  DPs:
    { 1: U11^#(tt(), N, X, XS) ->
         c_1(U12^#(splitAt(activate(N), activate(XS)), activate(X)),
             splitAt^#(activate(N), activate(XS)),
             activate^#(N),
             activate^#(XS),
             activate^#(X))
    , 2: U12^#(pair(YS, ZS), X) -> c_2(activate^#(X))
    , 3: splitAt^#(s(N), cons(X, XS)) ->
         c_3(U11^#(tt(), N, X, activate(XS)), activate^#(XS))
    , 4: afterNth^#(N, XS) ->
         c_7(snd^#(splitAt(N, XS)), splitAt^#(N, XS))
    , 5: and^#(tt(), X) -> c_9(activate^#(X))
    , 6: sel^#(N, XS) ->
         c_14(head^#(afterNth(N, XS)), afterNth^#(N, XS))
    , 7: tail^#(cons(N, XS)) -> c_15(activate^#(XS))
    , 8: take^#(N, XS) -> c_16(fst^#(splitAt(N, XS)), splitAt^#(N, XS))
    , 9: splitAt^#(0(), XS) -> c_4()
    , 10: activate^#(X) -> c_5()
    , 11: activate^#(n__natsFrom(X)) -> c_6(natsFrom^#(X))
    , 12: natsFrom^#(N) -> c_12()
    , 13: natsFrom^#(X) -> c_13()
    , 14: snd^#(pair(X, Y)) -> c_8()
    , 15: fst^#(pair(X, Y)) -> c_10()
    , 16: head^#(cons(N, XS)) -> c_11() }

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).

Strict DPs:
  { U11^#(tt(), N, X, XS) ->
    c_1(U12^#(splitAt(activate(N), activate(XS)), activate(X)),
        splitAt^#(activate(N), activate(XS)),
        activate^#(N),
        activate^#(XS),
        activate^#(X))
  , splitAt^#(s(N), cons(X, XS)) ->
    c_3(U11^#(tt(), N, X, activate(XS)), activate^#(XS))
  , afterNth^#(N, XS) -> c_7(snd^#(splitAt(N, XS)), splitAt^#(N, XS))
  , sel^#(N, XS) -> c_14(head^#(afterNth(N, XS)), afterNth^#(N, XS))
  , take^#(N, XS) -> c_16(fst^#(splitAt(N, XS)), splitAt^#(N, XS)) }
Weak DPs:
  { U12^#(pair(YS, ZS), X) -> c_2(activate^#(X))
  , splitAt^#(0(), XS) -> c_4()
  , activate^#(X) -> c_5()
  , activate^#(n__natsFrom(X)) -> c_6(natsFrom^#(X))
  , natsFrom^#(N) -> c_12()
  , natsFrom^#(X) -> c_13()
  , snd^#(pair(X, Y)) -> c_8()
  , and^#(tt(), X) -> c_9(activate^#(X))
  , fst^#(pair(X, Y)) -> c_10()
  , head^#(cons(N, XS)) -> c_11()
  , tail^#(cons(N, XS)) -> c_15(activate^#(XS)) }
Weak Trs:
  { U11(tt(), N, X, XS) ->
    U12(splitAt(activate(N), activate(XS)), activate(X))
  , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS)
  , splitAt(s(N), cons(X, XS)) -> U11(tt(), N, X, activate(XS))
  , splitAt(0(), XS) -> pair(nil(), XS)
  , activate(X) -> X
  , activate(n__natsFrom(X)) -> natsFrom(X)
  , afterNth(N, XS) -> snd(splitAt(N, XS))
  , snd(pair(X, Y)) -> Y
  , and(tt(), X) -> activate(X)
  , fst(pair(X, Y)) -> X
  , head(cons(N, XS)) -> N
  , natsFrom(N) -> cons(N, n__natsFrom(s(N)))
  , natsFrom(X) -> n__natsFrom(X)
  , sel(N, XS) -> head(afterNth(N, XS))
  , tail(cons(N, XS)) -> activate(XS)
  , take(N, XS) -> fst(splitAt(N, XS)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.

{ U12^#(pair(YS, ZS), X) -> c_2(activate^#(X))
, splitAt^#(0(), XS) -> c_4()
, activate^#(X) -> c_5()
, activate^#(n__natsFrom(X)) -> c_6(natsFrom^#(X))
, natsFrom^#(N) -> c_12()
, natsFrom^#(X) -> c_13()
, snd^#(pair(X, Y)) -> c_8()
, and^#(tt(), X) -> c_9(activate^#(X))
, fst^#(pair(X, Y)) -> c_10()
, head^#(cons(N, XS)) -> c_11()
, tail^#(cons(N, XS)) -> c_15(activate^#(XS)) }

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).

Strict DPs:
  { U11^#(tt(), N, X, XS) ->
    c_1(U12^#(splitAt(activate(N), activate(XS)), activate(X)),
        splitAt^#(activate(N), activate(XS)),
        activate^#(N),
        activate^#(XS),
        activate^#(X))
  , splitAt^#(s(N), cons(X, XS)) ->
    c_3(U11^#(tt(), N, X, activate(XS)), activate^#(XS))
  , afterNth^#(N, XS) -> c_7(snd^#(splitAt(N, XS)), splitAt^#(N, XS))
  , sel^#(N, XS) -> c_14(head^#(afterNth(N, XS)), afterNth^#(N, XS))
  , take^#(N, XS) -> c_16(fst^#(splitAt(N, XS)), splitAt^#(N, XS)) }
Weak Trs:
  { U11(tt(), N, X, XS) ->
    U12(splitAt(activate(N), activate(XS)), activate(X))
  , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS)
  , splitAt(s(N), cons(X, XS)) -> U11(tt(), N, X, activate(XS))
  , splitAt(0(), XS) -> pair(nil(), XS)
  , activate(X) -> X
  , activate(n__natsFrom(X)) -> natsFrom(X)
  , afterNth(N, XS) -> snd(splitAt(N, XS))
  , snd(pair(X, Y)) -> Y
  , and(tt(), X) -> activate(X)
  , fst(pair(X, Y)) -> X
  , head(cons(N, XS)) -> N
  , natsFrom(N) -> cons(N, n__natsFrom(s(N)))
  , natsFrom(X) -> n__natsFrom(X)
  , sel(N, XS) -> head(afterNth(N, XS))
  , tail(cons(N, XS)) -> activate(XS)
  , take(N, XS) -> fst(splitAt(N, XS)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:

  { U11^#(tt(), N, X, XS) ->
    c_1(U12^#(splitAt(activate(N), activate(XS)), activate(X)),
        splitAt^#(activate(N), activate(XS)),
        activate^#(N),
        activate^#(XS),
        activate^#(X))
  , splitAt^#(s(N), cons(X, XS)) ->
    c_3(U11^#(tt(), N, X, activate(XS)), activate^#(XS))
  , afterNth^#(N, XS) -> c_7(snd^#(splitAt(N, XS)), splitAt^#(N, XS))
  , sel^#(N, XS) -> c_14(head^#(afterNth(N, XS)), afterNth^#(N, XS))
  , take^#(N, XS) -> c_16(fst^#(splitAt(N, XS)), splitAt^#(N, XS)) }

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).

Strict DPs:
  { U11^#(tt(), N, X, XS) ->
    c_1(splitAt^#(activate(N), activate(XS)))
  , splitAt^#(s(N), cons(X, XS)) ->
    c_2(U11^#(tt(), N, X, activate(XS)))
  , afterNth^#(N, XS) -> c_3(splitAt^#(N, XS))
  , sel^#(N, XS) -> c_4(afterNth^#(N, XS))
  , take^#(N, XS) -> c_5(splitAt^#(N, XS)) }
Weak Trs:
  { U11(tt(), N, X, XS) ->
    U12(splitAt(activate(N), activate(XS)), activate(X))
  , U12(pair(YS, ZS), X) -> pair(cons(activate(X), YS), ZS)
  , splitAt(s(N), cons(X, XS)) -> U11(tt(), N, X, activate(XS))
  , splitAt(0(), XS) -> pair(nil(), XS)
  , activate(X) -> X
  , activate(n__natsFrom(X)) -> natsFrom(X)
  , afterNth(N, XS) -> snd(splitAt(N, XS))
  , snd(pair(X, Y)) -> Y
  , and(tt(), X) -> activate(X)
  , fst(pair(X, Y)) -> X
  , head(cons(N, XS)) -> N
  , natsFrom(N) -> cons(N, n__natsFrom(s(N)))
  , natsFrom(X) -> n__natsFrom(X)
  , sel(N, XS) -> head(afterNth(N, XS))
  , tail(cons(N, XS)) -> activate(XS)
  , take(N, XS) -> fst(splitAt(N, XS)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

We replace rewrite rules by usable rules:

  Weak Usable Rules:
    { activate(X) -> X
    , activate(n__natsFrom(X)) -> natsFrom(X)
    , natsFrom(N) -> cons(N, n__natsFrom(s(N)))
    , natsFrom(X) -> n__natsFrom(X) }

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).

Strict DPs:
  { U11^#(tt(), N, X, XS) ->
    c_1(splitAt^#(activate(N), activate(XS)))
  , splitAt^#(s(N), cons(X, XS)) ->
    c_2(U11^#(tt(), N, X, activate(XS)))
  , afterNth^#(N, XS) -> c_3(splitAt^#(N, XS))
  , sel^#(N, XS) -> c_4(afterNth^#(N, XS))
  , take^#(N, XS) -> c_5(splitAt^#(N, XS)) }
Weak Trs:
  { activate(X) -> X
  , activate(n__natsFrom(X)) -> natsFrom(X)
  , natsFrom(N) -> cons(N, n__natsFrom(s(N)))
  , natsFrom(X) -> n__natsFrom(X) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

Consider the dependency graph

  1: U11^#(tt(), N, X, XS) ->
     c_1(splitAt^#(activate(N), activate(XS)))
     -->_1 splitAt^#(s(N), cons(X, XS)) ->
           c_2(U11^#(tt(), N, X, activate(XS))) :2
  
  2: splitAt^#(s(N), cons(X, XS)) ->
     c_2(U11^#(tt(), N, X, activate(XS)))
     -->_1 U11^#(tt(), N, X, XS) ->
           c_1(splitAt^#(activate(N), activate(XS))) :1
  
  3: afterNth^#(N, XS) -> c_3(splitAt^#(N, XS))
     -->_1 splitAt^#(s(N), cons(X, XS)) ->
           c_2(U11^#(tt(), N, X, activate(XS))) :2
  
  4: sel^#(N, XS) -> c_4(afterNth^#(N, XS))
     -->_1 afterNth^#(N, XS) -> c_3(splitAt^#(N, XS)) :3
  
  5: take^#(N, XS) -> c_5(splitAt^#(N, XS))
     -->_1 splitAt^#(s(N), cons(X, XS)) ->
           c_2(U11^#(tt(), N, X, activate(XS))) :2
  

Following roots of the dependency graph are removed, as the
considered set of starting terms is closed under reduction with
respect to these rules (modulo compound contexts).

  { sel^#(N, XS) -> c_4(afterNth^#(N, XS))
  , take^#(N, XS) -> c_5(splitAt^#(N, XS)) }


We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).

Strict DPs:
  { U11^#(tt(), N, X, XS) ->
    c_1(splitAt^#(activate(N), activate(XS)))
  , splitAt^#(s(N), cons(X, XS)) ->
    c_2(U11^#(tt(), N, X, activate(XS)))
  , afterNth^#(N, XS) -> c_3(splitAt^#(N, XS)) }
Weak Trs:
  { activate(X) -> X
  , activate(n__natsFrom(X)) -> natsFrom(X)
  , natsFrom(N) -> cons(N, n__natsFrom(s(N)))
  , natsFrom(X) -> n__natsFrom(X) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

Consider the dependency graph

  1: U11^#(tt(), N, X, XS) ->
     c_1(splitAt^#(activate(N), activate(XS)))
     -->_1 splitAt^#(s(N), cons(X, XS)) ->
           c_2(U11^#(tt(), N, X, activate(XS))) :2
  
  2: splitAt^#(s(N), cons(X, XS)) ->
     c_2(U11^#(tt(), N, X, activate(XS)))
     -->_1 U11^#(tt(), N, X, XS) ->
           c_1(splitAt^#(activate(N), activate(XS))) :1
  
  3: afterNth^#(N, XS) -> c_3(splitAt^#(N, XS))
     -->_1 splitAt^#(s(N), cons(X, XS)) ->
           c_2(U11^#(tt(), N, X, activate(XS))) :2
  

Following roots of the dependency graph are removed, as the
considered set of starting terms is closed under reduction with
respect to these rules (modulo compound contexts).

  { afterNth^#(N, XS) -> c_3(splitAt^#(N, XS)) }


We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).

Strict DPs:
  { U11^#(tt(), N, X, XS) ->
    c_1(splitAt^#(activate(N), activate(XS)))
  , splitAt^#(s(N), cons(X, XS)) ->
    c_2(U11^#(tt(), N, X, activate(XS))) }
Weak Trs:
  { activate(X) -> X
  , activate(n__natsFrom(X)) -> natsFrom(X)
  , natsFrom(N) -> cons(N, n__natsFrom(s(N)))
  , natsFrom(X) -> n__natsFrom(X) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

The following argument positions are usable:
  Uargs(c_1) = {1}, Uargs(c_2) = {1}

TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).

                     [tt] = [1]                  
                                                 
           [activate](x1) = [1] x1 + [0]         
                                                 
           [cons](x1, x2) = [1] x1 + [0]         
                                                 
           [natsFrom](x1) = [1] x1 + [0]         
                                                 
        [n__natsFrom](x1) = [1] x1 + [0]         
                                                 
                  [s](x1) = [1] x1 + [1]         
                                                 
  [U11^#](x1, x2, x3, x4) = [1] x1 + [2] x2 + [0]
                                                 
      [splitAt^#](x1, x2) = [2] x1 + [0]         
                                                 
                [c_1](x1) = [1] x1 + [0]         
                                                 
                [c_2](x1) = [1] x1 + [0]         

This order satisfies following ordering constraints:

                   [activate(X)] =  [1] X + [0]                                
                                 >= [1] X + [0]                                
                                 =  [X]                                        
                                                                               
      [activate(n__natsFrom(X))] =  [1] X + [0]                                
                                 >= [1] X + [0]                                
                                 =  [natsFrom(X)]                              
                                                                               
                   [natsFrom(N)] =  [1] N + [0]                                
                                 >= [1] N + [0]                                
                                 =  [cons(N, n__natsFrom(s(N)))]               
                                                                               
                   [natsFrom(X)] =  [1] X + [0]                                
                                 >= [1] X + [0]                                
                                 =  [n__natsFrom(X)]                           
                                                                               
         [U11^#(tt(), N, X, XS)] =  [2] N + [1]                                
                                 >  [2] N + [0]                                
                                 =  [c_1(splitAt^#(activate(N), activate(XS)))]
                                                                               
  [splitAt^#(s(N), cons(X, XS))] =  [2] N + [2]                                
                                 >  [2] N + [1]                                
                                 =  [c_2(U11^#(tt(), N, X, activate(XS)))]     
                                                                               

Hurray, we answered YES(?,O(n^1))