MAYBE

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

Strict Trs:
  { U11(tt(), N, XS) -> U12(tt(), N, XS)
  , U12(tt(), N, XS) -> snd(splitAt(N, XS))
  , snd(pair(X, Y)) -> U51(tt(), Y)
  , splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, XS)
  , splitAt(0(), XS) -> pair(nil(), XS)
  , U21(tt(), X) -> U22(tt(), X)
  , U22(tt(), X) -> X
  , U31(tt(), N) -> U32(tt(), N)
  , U32(tt(), N) -> N
  , U41(tt(), N, XS) -> U42(tt(), N, XS)
  , U42(tt(), N, XS) -> head(afterNth(N, XS))
  , head(cons(N, XS)) -> U31(tt(), N)
  , afterNth(N, XS) -> U11(tt(), N, XS)
  , U51(tt(), Y) -> U52(tt(), Y)
  , U52(tt(), Y) -> Y
  , U61(tt(), N, X, XS) -> U62(tt(), N, X, XS)
  , U62(tt(), N, X, XS) -> U63(tt(), N, X, XS)
  , U63(tt(), N, X, XS) -> U64(splitAt(N, XS), X)
  , U64(pair(YS, ZS), X) -> pair(cons(X, YS), ZS)
  , U71(tt(), XS) -> U72(tt(), XS)
  , U72(tt(), XS) -> XS
  , U81(tt(), N, XS) -> U82(tt(), N, XS)
  , U82(tt(), N, XS) -> fst(splitAt(N, XS))
  , fst(pair(X, Y)) -> U21(tt(), X)
  , natsFrom(N) -> cons(N, natsFrom(s(N)))
  , sel(N, XS) -> U41(tt(), N, XS)
  , tail(cons(N, XS)) -> U71(tt(), XS)
  , take(N, XS) -> U81(tt(), N, XS) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We add following dependency tuples:

Strict DPs:
  { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), N, XS))
  , U12^#(tt(), N, XS) ->
    c_2(snd^#(splitAt(N, XS)), splitAt^#(N, XS))
  , snd^#(pair(X, Y)) -> c_3(U51^#(tt(), Y))
  , splitAt^#(s(N), cons(X, XS)) -> c_4(U61^#(tt(), N, X, XS))
  , splitAt^#(0(), XS) -> c_5()
  , U51^#(tt(), Y) -> c_14(U52^#(tt(), Y))
  , U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), N, X, XS))
  , U21^#(tt(), X) -> c_6(U22^#(tt(), X))
  , U22^#(tt(), X) -> c_7()
  , U31^#(tt(), N) -> c_8(U32^#(tt(), N))
  , U32^#(tt(), N) -> c_9()
  , U41^#(tt(), N, XS) -> c_10(U42^#(tt(), N, XS))
  , U42^#(tt(), N, XS) ->
    c_11(head^#(afterNth(N, XS)), afterNth^#(N, XS))
  , head^#(cons(N, XS)) -> c_12(U31^#(tt(), N))
  , afterNth^#(N, XS) -> c_13(U11^#(tt(), N, XS))
  , U52^#(tt(), Y) -> c_15()
  , U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), N, X, XS))
  , U63^#(tt(), N, X, XS) ->
    c_18(U64^#(splitAt(N, XS), X), splitAt^#(N, XS))
  , U64^#(pair(YS, ZS), X) -> c_19()
  , U71^#(tt(), XS) -> c_20(U72^#(tt(), XS))
  , U72^#(tt(), XS) -> c_21()
  , U81^#(tt(), N, XS) -> c_22(U82^#(tt(), N, XS))
  , U82^#(tt(), N, XS) ->
    c_23(fst^#(splitAt(N, XS)), splitAt^#(N, XS))
  , fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
  , natsFrom^#(N) -> c_25(natsFrom^#(s(N)))
  , sel^#(N, XS) -> c_26(U41^#(tt(), N, XS))
  , tail^#(cons(N, XS)) -> c_27(U71^#(tt(), XS))
  , take^#(N, XS) -> c_28(U81^#(tt(), N, XS)) }

and mark the set of starting terms.

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

Strict DPs:
  { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), N, XS))
  , U12^#(tt(), N, XS) ->
    c_2(snd^#(splitAt(N, XS)), splitAt^#(N, XS))
  , snd^#(pair(X, Y)) -> c_3(U51^#(tt(), Y))
  , splitAt^#(s(N), cons(X, XS)) -> c_4(U61^#(tt(), N, X, XS))
  , splitAt^#(0(), XS) -> c_5()
  , U51^#(tt(), Y) -> c_14(U52^#(tt(), Y))
  , U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), N, X, XS))
  , U21^#(tt(), X) -> c_6(U22^#(tt(), X))
  , U22^#(tt(), X) -> c_7()
  , U31^#(tt(), N) -> c_8(U32^#(tt(), N))
  , U32^#(tt(), N) -> c_9()
  , U41^#(tt(), N, XS) -> c_10(U42^#(tt(), N, XS))
  , U42^#(tt(), N, XS) ->
    c_11(head^#(afterNth(N, XS)), afterNth^#(N, XS))
  , head^#(cons(N, XS)) -> c_12(U31^#(tt(), N))
  , afterNth^#(N, XS) -> c_13(U11^#(tt(), N, XS))
  , U52^#(tt(), Y) -> c_15()
  , U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), N, X, XS))
  , U63^#(tt(), N, X, XS) ->
    c_18(U64^#(splitAt(N, XS), X), splitAt^#(N, XS))
  , U64^#(pair(YS, ZS), X) -> c_19()
  , U71^#(tt(), XS) -> c_20(U72^#(tt(), XS))
  , U72^#(tt(), XS) -> c_21()
  , U81^#(tt(), N, XS) -> c_22(U82^#(tt(), N, XS))
  , U82^#(tt(), N, XS) ->
    c_23(fst^#(splitAt(N, XS)), splitAt^#(N, XS))
  , fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
  , natsFrom^#(N) -> c_25(natsFrom^#(s(N)))
  , sel^#(N, XS) -> c_26(U41^#(tt(), N, XS))
  , tail^#(cons(N, XS)) -> c_27(U71^#(tt(), XS))
  , take^#(N, XS) -> c_28(U81^#(tt(), N, XS)) }
Weak Trs:
  { U11(tt(), N, XS) -> U12(tt(), N, XS)
  , U12(tt(), N, XS) -> snd(splitAt(N, XS))
  , snd(pair(X, Y)) -> U51(tt(), Y)
  , splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, XS)
  , splitAt(0(), XS) -> pair(nil(), XS)
  , U21(tt(), X) -> U22(tt(), X)
  , U22(tt(), X) -> X
  , U31(tt(), N) -> U32(tt(), N)
  , U32(tt(), N) -> N
  , U41(tt(), N, XS) -> U42(tt(), N, XS)
  , U42(tt(), N, XS) -> head(afterNth(N, XS))
  , head(cons(N, XS)) -> U31(tt(), N)
  , afterNth(N, XS) -> U11(tt(), N, XS)
  , U51(tt(), Y) -> U52(tt(), Y)
  , U52(tt(), Y) -> Y
  , U61(tt(), N, X, XS) -> U62(tt(), N, X, XS)
  , U62(tt(), N, X, XS) -> U63(tt(), N, X, XS)
  , U63(tt(), N, X, XS) -> U64(splitAt(N, XS), X)
  , U64(pair(YS, ZS), X) -> pair(cons(X, YS), ZS)
  , U71(tt(), XS) -> U72(tt(), XS)
  , U72(tt(), XS) -> XS
  , U81(tt(), N, XS) -> U82(tt(), N, XS)
  , U82(tt(), N, XS) -> fst(splitAt(N, XS))
  , fst(pair(X, Y)) -> U21(tt(), X)
  , natsFrom(N) -> cons(N, natsFrom(s(N)))
  , sel(N, XS) -> U41(tt(), N, XS)
  , tail(cons(N, XS)) -> U71(tt(), XS)
  , take(N, XS) -> U81(tt(), N, XS) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We estimate the number of application of {5,9,11,16,19,21} by
applications of Pre({5,9,11,16,19,21}) = {2,6,8,10,18,20,23}. Here
rules are labeled as follows:

  DPs:
    { 1: U11^#(tt(), N, XS) -> c_1(U12^#(tt(), N, XS))
    , 2: U12^#(tt(), N, XS) ->
         c_2(snd^#(splitAt(N, XS)), splitAt^#(N, XS))
    , 3: snd^#(pair(X, Y)) -> c_3(U51^#(tt(), Y))
    , 4: splitAt^#(s(N), cons(X, XS)) -> c_4(U61^#(tt(), N, X, XS))
    , 5: splitAt^#(0(), XS) -> c_5()
    , 6: U51^#(tt(), Y) -> c_14(U52^#(tt(), Y))
    , 7: U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), N, X, XS))
    , 8: U21^#(tt(), X) -> c_6(U22^#(tt(), X))
    , 9: U22^#(tt(), X) -> c_7()
    , 10: U31^#(tt(), N) -> c_8(U32^#(tt(), N))
    , 11: U32^#(tt(), N) -> c_9()
    , 12: U41^#(tt(), N, XS) -> c_10(U42^#(tt(), N, XS))
    , 13: U42^#(tt(), N, XS) ->
          c_11(head^#(afterNth(N, XS)), afterNth^#(N, XS))
    , 14: head^#(cons(N, XS)) -> c_12(U31^#(tt(), N))
    , 15: afterNth^#(N, XS) -> c_13(U11^#(tt(), N, XS))
    , 16: U52^#(tt(), Y) -> c_15()
    , 17: U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), N, X, XS))
    , 18: U63^#(tt(), N, X, XS) ->
          c_18(U64^#(splitAt(N, XS), X), splitAt^#(N, XS))
    , 19: U64^#(pair(YS, ZS), X) -> c_19()
    , 20: U71^#(tt(), XS) -> c_20(U72^#(tt(), XS))
    , 21: U72^#(tt(), XS) -> c_21()
    , 22: U81^#(tt(), N, XS) -> c_22(U82^#(tt(), N, XS))
    , 23: U82^#(tt(), N, XS) ->
          c_23(fst^#(splitAt(N, XS)), splitAt^#(N, XS))
    , 24: fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
    , 25: natsFrom^#(N) -> c_25(natsFrom^#(s(N)))
    , 26: sel^#(N, XS) -> c_26(U41^#(tt(), N, XS))
    , 27: tail^#(cons(N, XS)) -> c_27(U71^#(tt(), XS))
    , 28: take^#(N, XS) -> c_28(U81^#(tt(), N, XS)) }

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

Strict DPs:
  { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), N, XS))
  , U12^#(tt(), N, XS) ->
    c_2(snd^#(splitAt(N, XS)), splitAt^#(N, XS))
  , snd^#(pair(X, Y)) -> c_3(U51^#(tt(), Y))
  , splitAt^#(s(N), cons(X, XS)) -> c_4(U61^#(tt(), N, X, XS))
  , U51^#(tt(), Y) -> c_14(U52^#(tt(), Y))
  , U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), N, X, XS))
  , U21^#(tt(), X) -> c_6(U22^#(tt(), X))
  , U31^#(tt(), N) -> c_8(U32^#(tt(), N))
  , U41^#(tt(), N, XS) -> c_10(U42^#(tt(), N, XS))
  , U42^#(tt(), N, XS) ->
    c_11(head^#(afterNth(N, XS)), afterNth^#(N, XS))
  , head^#(cons(N, XS)) -> c_12(U31^#(tt(), N))
  , afterNth^#(N, XS) -> c_13(U11^#(tt(), N, XS))
  , U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), N, X, XS))
  , U63^#(tt(), N, X, XS) ->
    c_18(U64^#(splitAt(N, XS), X), splitAt^#(N, XS))
  , U71^#(tt(), XS) -> c_20(U72^#(tt(), XS))
  , U81^#(tt(), N, XS) -> c_22(U82^#(tt(), N, XS))
  , U82^#(tt(), N, XS) ->
    c_23(fst^#(splitAt(N, XS)), splitAt^#(N, XS))
  , fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
  , natsFrom^#(N) -> c_25(natsFrom^#(s(N)))
  , sel^#(N, XS) -> c_26(U41^#(tt(), N, XS))
  , tail^#(cons(N, XS)) -> c_27(U71^#(tt(), XS))
  , take^#(N, XS) -> c_28(U81^#(tt(), N, XS)) }
Weak DPs:
  { splitAt^#(0(), XS) -> c_5()
  , U22^#(tt(), X) -> c_7()
  , U32^#(tt(), N) -> c_9()
  , U52^#(tt(), Y) -> c_15()
  , U64^#(pair(YS, ZS), X) -> c_19()
  , U72^#(tt(), XS) -> c_21() }
Weak Trs:
  { U11(tt(), N, XS) -> U12(tt(), N, XS)
  , U12(tt(), N, XS) -> snd(splitAt(N, XS))
  , snd(pair(X, Y)) -> U51(tt(), Y)
  , splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, XS)
  , splitAt(0(), XS) -> pair(nil(), XS)
  , U21(tt(), X) -> U22(tt(), X)
  , U22(tt(), X) -> X
  , U31(tt(), N) -> U32(tt(), N)
  , U32(tt(), N) -> N
  , U41(tt(), N, XS) -> U42(tt(), N, XS)
  , U42(tt(), N, XS) -> head(afterNth(N, XS))
  , head(cons(N, XS)) -> U31(tt(), N)
  , afterNth(N, XS) -> U11(tt(), N, XS)
  , U51(tt(), Y) -> U52(tt(), Y)
  , U52(tt(), Y) -> Y
  , U61(tt(), N, X, XS) -> U62(tt(), N, X, XS)
  , U62(tt(), N, X, XS) -> U63(tt(), N, X, XS)
  , U63(tt(), N, X, XS) -> U64(splitAt(N, XS), X)
  , U64(pair(YS, ZS), X) -> pair(cons(X, YS), ZS)
  , U71(tt(), XS) -> U72(tt(), XS)
  , U72(tt(), XS) -> XS
  , U81(tt(), N, XS) -> U82(tt(), N, XS)
  , U82(tt(), N, XS) -> fst(splitAt(N, XS))
  , fst(pair(X, Y)) -> U21(tt(), X)
  , natsFrom(N) -> cons(N, natsFrom(s(N)))
  , sel(N, XS) -> U41(tt(), N, XS)
  , tail(cons(N, XS)) -> U71(tt(), XS)
  , take(N, XS) -> U81(tt(), N, XS) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We estimate the number of application of {5,7,8,15} by applications
of Pre({5,7,8,15}) = {3,11,18,21}. Here rules are labeled as
follows:

  DPs:
    { 1: U11^#(tt(), N, XS) -> c_1(U12^#(tt(), N, XS))
    , 2: U12^#(tt(), N, XS) ->
         c_2(snd^#(splitAt(N, XS)), splitAt^#(N, XS))
    , 3: snd^#(pair(X, Y)) -> c_3(U51^#(tt(), Y))
    , 4: splitAt^#(s(N), cons(X, XS)) -> c_4(U61^#(tt(), N, X, XS))
    , 5: U51^#(tt(), Y) -> c_14(U52^#(tt(), Y))
    , 6: U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), N, X, XS))
    , 7: U21^#(tt(), X) -> c_6(U22^#(tt(), X))
    , 8: U31^#(tt(), N) -> c_8(U32^#(tt(), N))
    , 9: U41^#(tt(), N, XS) -> c_10(U42^#(tt(), N, XS))
    , 10: U42^#(tt(), N, XS) ->
          c_11(head^#(afterNth(N, XS)), afterNth^#(N, XS))
    , 11: head^#(cons(N, XS)) -> c_12(U31^#(tt(), N))
    , 12: afterNth^#(N, XS) -> c_13(U11^#(tt(), N, XS))
    , 13: U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), N, X, XS))
    , 14: U63^#(tt(), N, X, XS) ->
          c_18(U64^#(splitAt(N, XS), X), splitAt^#(N, XS))
    , 15: U71^#(tt(), XS) -> c_20(U72^#(tt(), XS))
    , 16: U81^#(tt(), N, XS) -> c_22(U82^#(tt(), N, XS))
    , 17: U82^#(tt(), N, XS) ->
          c_23(fst^#(splitAt(N, XS)), splitAt^#(N, XS))
    , 18: fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
    , 19: natsFrom^#(N) -> c_25(natsFrom^#(s(N)))
    , 20: sel^#(N, XS) -> c_26(U41^#(tt(), N, XS))
    , 21: tail^#(cons(N, XS)) -> c_27(U71^#(tt(), XS))
    , 22: take^#(N, XS) -> c_28(U81^#(tt(), N, XS))
    , 23: splitAt^#(0(), XS) -> c_5()
    , 24: U22^#(tt(), X) -> c_7()
    , 25: U32^#(tt(), N) -> c_9()
    , 26: U52^#(tt(), Y) -> c_15()
    , 27: U64^#(pair(YS, ZS), X) -> c_19()
    , 28: U72^#(tt(), XS) -> c_21() }

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

Strict DPs:
  { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), N, XS))
  , U12^#(tt(), N, XS) ->
    c_2(snd^#(splitAt(N, XS)), splitAt^#(N, XS))
  , snd^#(pair(X, Y)) -> c_3(U51^#(tt(), Y))
  , splitAt^#(s(N), cons(X, XS)) -> c_4(U61^#(tt(), N, X, XS))
  , U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), N, X, XS))
  , U41^#(tt(), N, XS) -> c_10(U42^#(tt(), N, XS))
  , U42^#(tt(), N, XS) ->
    c_11(head^#(afterNth(N, XS)), afterNth^#(N, XS))
  , head^#(cons(N, XS)) -> c_12(U31^#(tt(), N))
  , afterNth^#(N, XS) -> c_13(U11^#(tt(), N, XS))
  , U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), N, X, XS))
  , U63^#(tt(), N, X, XS) ->
    c_18(U64^#(splitAt(N, XS), X), splitAt^#(N, XS))
  , U81^#(tt(), N, XS) -> c_22(U82^#(tt(), N, XS))
  , U82^#(tt(), N, XS) ->
    c_23(fst^#(splitAt(N, XS)), splitAt^#(N, XS))
  , fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
  , natsFrom^#(N) -> c_25(natsFrom^#(s(N)))
  , sel^#(N, XS) -> c_26(U41^#(tt(), N, XS))
  , tail^#(cons(N, XS)) -> c_27(U71^#(tt(), XS))
  , take^#(N, XS) -> c_28(U81^#(tt(), N, XS)) }
Weak DPs:
  { splitAt^#(0(), XS) -> c_5()
  , U51^#(tt(), Y) -> c_14(U52^#(tt(), Y))
  , U21^#(tt(), X) -> c_6(U22^#(tt(), X))
  , U22^#(tt(), X) -> c_7()
  , U31^#(tt(), N) -> c_8(U32^#(tt(), N))
  , U32^#(tt(), N) -> c_9()
  , U52^#(tt(), Y) -> c_15()
  , U64^#(pair(YS, ZS), X) -> c_19()
  , U71^#(tt(), XS) -> c_20(U72^#(tt(), XS))
  , U72^#(tt(), XS) -> c_21() }
Weak Trs:
  { U11(tt(), N, XS) -> U12(tt(), N, XS)
  , U12(tt(), N, XS) -> snd(splitAt(N, XS))
  , snd(pair(X, Y)) -> U51(tt(), Y)
  , splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, XS)
  , splitAt(0(), XS) -> pair(nil(), XS)
  , U21(tt(), X) -> U22(tt(), X)
  , U22(tt(), X) -> X
  , U31(tt(), N) -> U32(tt(), N)
  , U32(tt(), N) -> N
  , U41(tt(), N, XS) -> U42(tt(), N, XS)
  , U42(tt(), N, XS) -> head(afterNth(N, XS))
  , head(cons(N, XS)) -> U31(tt(), N)
  , afterNth(N, XS) -> U11(tt(), N, XS)
  , U51(tt(), Y) -> U52(tt(), Y)
  , U52(tt(), Y) -> Y
  , U61(tt(), N, X, XS) -> U62(tt(), N, X, XS)
  , U62(tt(), N, X, XS) -> U63(tt(), N, X, XS)
  , U63(tt(), N, X, XS) -> U64(splitAt(N, XS), X)
  , U64(pair(YS, ZS), X) -> pair(cons(X, YS), ZS)
  , U71(tt(), XS) -> U72(tt(), XS)
  , U72(tt(), XS) -> XS
  , U81(tt(), N, XS) -> U82(tt(), N, XS)
  , U82(tt(), N, XS) -> fst(splitAt(N, XS))
  , fst(pair(X, Y)) -> U21(tt(), X)
  , natsFrom(N) -> cons(N, natsFrom(s(N)))
  , sel(N, XS) -> U41(tt(), N, XS)
  , tail(cons(N, XS)) -> U71(tt(), XS)
  , take(N, XS) -> U81(tt(), N, XS) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

We estimate the number of application of {3,8,14,17} by
applications of Pre({3,8,14,17}) = {2,7,13}. Here rules are labeled
as follows:

  DPs:
    { 1: U11^#(tt(), N, XS) -> c_1(U12^#(tt(), N, XS))
    , 2: U12^#(tt(), N, XS) ->
         c_2(snd^#(splitAt(N, XS)), splitAt^#(N, XS))
    , 3: snd^#(pair(X, Y)) -> c_3(U51^#(tt(), Y))
    , 4: splitAt^#(s(N), cons(X, XS)) -> c_4(U61^#(tt(), N, X, XS))
    , 5: U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), N, X, XS))
    , 6: U41^#(tt(), N, XS) -> c_10(U42^#(tt(), N, XS))
    , 7: U42^#(tt(), N, XS) ->
         c_11(head^#(afterNth(N, XS)), afterNth^#(N, XS))
    , 8: head^#(cons(N, XS)) -> c_12(U31^#(tt(), N))
    , 9: afterNth^#(N, XS) -> c_13(U11^#(tt(), N, XS))
    , 10: U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), N, X, XS))
    , 11: U63^#(tt(), N, X, XS) ->
          c_18(U64^#(splitAt(N, XS), X), splitAt^#(N, XS))
    , 12: U81^#(tt(), N, XS) -> c_22(U82^#(tt(), N, XS))
    , 13: U82^#(tt(), N, XS) ->
          c_23(fst^#(splitAt(N, XS)), splitAt^#(N, XS))
    , 14: fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
    , 15: natsFrom^#(N) -> c_25(natsFrom^#(s(N)))
    , 16: sel^#(N, XS) -> c_26(U41^#(tt(), N, XS))
    , 17: tail^#(cons(N, XS)) -> c_27(U71^#(tt(), XS))
    , 18: take^#(N, XS) -> c_28(U81^#(tt(), N, XS))
    , 19: splitAt^#(0(), XS) -> c_5()
    , 20: U51^#(tt(), Y) -> c_14(U52^#(tt(), Y))
    , 21: U21^#(tt(), X) -> c_6(U22^#(tt(), X))
    , 22: U22^#(tt(), X) -> c_7()
    , 23: U31^#(tt(), N) -> c_8(U32^#(tt(), N))
    , 24: U32^#(tt(), N) -> c_9()
    , 25: U52^#(tt(), Y) -> c_15()
    , 26: U64^#(pair(YS, ZS), X) -> c_19()
    , 27: U71^#(tt(), XS) -> c_20(U72^#(tt(), XS))
    , 28: U72^#(tt(), XS) -> c_21() }

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

Strict DPs:
  { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), N, XS))
  , U12^#(tt(), N, XS) ->
    c_2(snd^#(splitAt(N, XS)), splitAt^#(N, XS))
  , splitAt^#(s(N), cons(X, XS)) -> c_4(U61^#(tt(), N, X, XS))
  , U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), N, X, XS))
  , U41^#(tt(), N, XS) -> c_10(U42^#(tt(), N, XS))
  , U42^#(tt(), N, XS) ->
    c_11(head^#(afterNth(N, XS)), afterNth^#(N, XS))
  , afterNth^#(N, XS) -> c_13(U11^#(tt(), N, XS))
  , U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), N, X, XS))
  , U63^#(tt(), N, X, XS) ->
    c_18(U64^#(splitAt(N, XS), X), splitAt^#(N, XS))
  , U81^#(tt(), N, XS) -> c_22(U82^#(tt(), N, XS))
  , U82^#(tt(), N, XS) ->
    c_23(fst^#(splitAt(N, XS)), splitAt^#(N, XS))
  , natsFrom^#(N) -> c_25(natsFrom^#(s(N)))
  , sel^#(N, XS) -> c_26(U41^#(tt(), N, XS))
  , take^#(N, XS) -> c_28(U81^#(tt(), N, XS)) }
Weak DPs:
  { snd^#(pair(X, Y)) -> c_3(U51^#(tt(), Y))
  , splitAt^#(0(), XS) -> c_5()
  , U51^#(tt(), Y) -> c_14(U52^#(tt(), Y))
  , U21^#(tt(), X) -> c_6(U22^#(tt(), X))
  , U22^#(tt(), X) -> c_7()
  , U31^#(tt(), N) -> c_8(U32^#(tt(), N))
  , U32^#(tt(), N) -> c_9()
  , head^#(cons(N, XS)) -> c_12(U31^#(tt(), N))
  , U52^#(tt(), Y) -> c_15()
  , U64^#(pair(YS, ZS), X) -> c_19()
  , U71^#(tt(), XS) -> c_20(U72^#(tt(), XS))
  , U72^#(tt(), XS) -> c_21()
  , fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
  , tail^#(cons(N, XS)) -> c_27(U71^#(tt(), XS)) }
Weak Trs:
  { U11(tt(), N, XS) -> U12(tt(), N, XS)
  , U12(tt(), N, XS) -> snd(splitAt(N, XS))
  , snd(pair(X, Y)) -> U51(tt(), Y)
  , splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, XS)
  , splitAt(0(), XS) -> pair(nil(), XS)
  , U21(tt(), X) -> U22(tt(), X)
  , U22(tt(), X) -> X
  , U31(tt(), N) -> U32(tt(), N)
  , U32(tt(), N) -> N
  , U41(tt(), N, XS) -> U42(tt(), N, XS)
  , U42(tt(), N, XS) -> head(afterNth(N, XS))
  , head(cons(N, XS)) -> U31(tt(), N)
  , afterNth(N, XS) -> U11(tt(), N, XS)
  , U51(tt(), Y) -> U52(tt(), Y)
  , U52(tt(), Y) -> Y
  , U61(tt(), N, X, XS) -> U62(tt(), N, X, XS)
  , U62(tt(), N, X, XS) -> U63(tt(), N, X, XS)
  , U63(tt(), N, X, XS) -> U64(splitAt(N, XS), X)
  , U64(pair(YS, ZS), X) -> pair(cons(X, YS), ZS)
  , U71(tt(), XS) -> U72(tt(), XS)
  , U72(tt(), XS) -> XS
  , U81(tt(), N, XS) -> U82(tt(), N, XS)
  , U82(tt(), N, XS) -> fst(splitAt(N, XS))
  , fst(pair(X, Y)) -> U21(tt(), X)
  , natsFrom(N) -> cons(N, natsFrom(s(N)))
  , sel(N, XS) -> U41(tt(), N, XS)
  , tail(cons(N, XS)) -> U71(tt(), XS)
  , take(N, XS) -> U81(tt(), N, XS) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

{ snd^#(pair(X, Y)) -> c_3(U51^#(tt(), Y))
, splitAt^#(0(), XS) -> c_5()
, U51^#(tt(), Y) -> c_14(U52^#(tt(), Y))
, U21^#(tt(), X) -> c_6(U22^#(tt(), X))
, U22^#(tt(), X) -> c_7()
, U31^#(tt(), N) -> c_8(U32^#(tt(), N))
, U32^#(tt(), N) -> c_9()
, head^#(cons(N, XS)) -> c_12(U31^#(tt(), N))
, U52^#(tt(), Y) -> c_15()
, U64^#(pair(YS, ZS), X) -> c_19()
, U71^#(tt(), XS) -> c_20(U72^#(tt(), XS))
, U72^#(tt(), XS) -> c_21()
, fst^#(pair(X, Y)) -> c_24(U21^#(tt(), X))
, tail^#(cons(N, XS)) -> c_27(U71^#(tt(), XS)) }

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

Strict DPs:
  { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), N, XS))
  , U12^#(tt(), N, XS) ->
    c_2(snd^#(splitAt(N, XS)), splitAt^#(N, XS))
  , splitAt^#(s(N), cons(X, XS)) -> c_4(U61^#(tt(), N, X, XS))
  , U61^#(tt(), N, X, XS) -> c_16(U62^#(tt(), N, X, XS))
  , U41^#(tt(), N, XS) -> c_10(U42^#(tt(), N, XS))
  , U42^#(tt(), N, XS) ->
    c_11(head^#(afterNth(N, XS)), afterNth^#(N, XS))
  , afterNth^#(N, XS) -> c_13(U11^#(tt(), N, XS))
  , U62^#(tt(), N, X, XS) -> c_17(U63^#(tt(), N, X, XS))
  , U63^#(tt(), N, X, XS) ->
    c_18(U64^#(splitAt(N, XS), X), splitAt^#(N, XS))
  , U81^#(tt(), N, XS) -> c_22(U82^#(tt(), N, XS))
  , U82^#(tt(), N, XS) ->
    c_23(fst^#(splitAt(N, XS)), splitAt^#(N, XS))
  , natsFrom^#(N) -> c_25(natsFrom^#(s(N)))
  , sel^#(N, XS) -> c_26(U41^#(tt(), N, XS))
  , take^#(N, XS) -> c_28(U81^#(tt(), N, XS)) }
Weak Trs:
  { U11(tt(), N, XS) -> U12(tt(), N, XS)
  , U12(tt(), N, XS) -> snd(splitAt(N, XS))
  , snd(pair(X, Y)) -> U51(tt(), Y)
  , splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, XS)
  , splitAt(0(), XS) -> pair(nil(), XS)
  , U21(tt(), X) -> U22(tt(), X)
  , U22(tt(), X) -> X
  , U31(tt(), N) -> U32(tt(), N)
  , U32(tt(), N) -> N
  , U41(tt(), N, XS) -> U42(tt(), N, XS)
  , U42(tt(), N, XS) -> head(afterNth(N, XS))
  , head(cons(N, XS)) -> U31(tt(), N)
  , afterNth(N, XS) -> U11(tt(), N, XS)
  , U51(tt(), Y) -> U52(tt(), Y)
  , U52(tt(), Y) -> Y
  , U61(tt(), N, X, XS) -> U62(tt(), N, X, XS)
  , U62(tt(), N, X, XS) -> U63(tt(), N, X, XS)
  , U63(tt(), N, X, XS) -> U64(splitAt(N, XS), X)
  , U64(pair(YS, ZS), X) -> pair(cons(X, YS), ZS)
  , U71(tt(), XS) -> U72(tt(), XS)
  , U72(tt(), XS) -> XS
  , U81(tt(), N, XS) -> U82(tt(), N, XS)
  , U82(tt(), N, XS) -> fst(splitAt(N, XS))
  , fst(pair(X, Y)) -> U21(tt(), X)
  , natsFrom(N) -> cons(N, natsFrom(s(N)))
  , sel(N, XS) -> U41(tt(), N, XS)
  , tail(cons(N, XS)) -> U71(tt(), XS)
  , take(N, XS) -> U81(tt(), N, XS) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

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

  { U12^#(tt(), N, XS) ->
    c_2(snd^#(splitAt(N, XS)), splitAt^#(N, XS))
  , U42^#(tt(), N, XS) ->
    c_11(head^#(afterNth(N, XS)), afterNth^#(N, XS))
  , U63^#(tt(), N, X, XS) ->
    c_18(U64^#(splitAt(N, XS), X), splitAt^#(N, XS))
  , U82^#(tt(), N, XS) ->
    c_23(fst^#(splitAt(N, XS)), splitAt^#(N, XS)) }

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

Strict DPs:
  { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), N, XS))
  , U12^#(tt(), N, XS) -> c_2(splitAt^#(N, XS))
  , splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, XS))
  , U61^#(tt(), N, X, XS) -> c_4(U62^#(tt(), N, X, XS))
  , U41^#(tt(), N, XS) -> c_5(U42^#(tt(), N, XS))
  , U42^#(tt(), N, XS) -> c_6(afterNth^#(N, XS))
  , afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS))
  , U62^#(tt(), N, X, XS) -> c_8(U63^#(tt(), N, X, XS))
  , U63^#(tt(), N, X, XS) -> c_9(splitAt^#(N, XS))
  , U81^#(tt(), N, XS) -> c_10(U82^#(tt(), N, XS))
  , U82^#(tt(), N, XS) -> c_11(splitAt^#(N, XS))
  , natsFrom^#(N) -> c_12(natsFrom^#(s(N)))
  , sel^#(N, XS) -> c_13(U41^#(tt(), N, XS))
  , take^#(N, XS) -> c_14(U81^#(tt(), N, XS)) }
Weak Trs:
  { U11(tt(), N, XS) -> U12(tt(), N, XS)
  , U12(tt(), N, XS) -> snd(splitAt(N, XS))
  , snd(pair(X, Y)) -> U51(tt(), Y)
  , splitAt(s(N), cons(X, XS)) -> U61(tt(), N, X, XS)
  , splitAt(0(), XS) -> pair(nil(), XS)
  , U21(tt(), X) -> U22(tt(), X)
  , U22(tt(), X) -> X
  , U31(tt(), N) -> U32(tt(), N)
  , U32(tt(), N) -> N
  , U41(tt(), N, XS) -> U42(tt(), N, XS)
  , U42(tt(), N, XS) -> head(afterNth(N, XS))
  , head(cons(N, XS)) -> U31(tt(), N)
  , afterNth(N, XS) -> U11(tt(), N, XS)
  , U51(tt(), Y) -> U52(tt(), Y)
  , U52(tt(), Y) -> Y
  , U61(tt(), N, X, XS) -> U62(tt(), N, X, XS)
  , U62(tt(), N, X, XS) -> U63(tt(), N, X, XS)
  , U63(tt(), N, X, XS) -> U64(splitAt(N, XS), X)
  , U64(pair(YS, ZS), X) -> pair(cons(X, YS), ZS)
  , U71(tt(), XS) -> U72(tt(), XS)
  , U72(tt(), XS) -> XS
  , U81(tt(), N, XS) -> U82(tt(), N, XS)
  , U82(tt(), N, XS) -> fst(splitAt(N, XS))
  , fst(pair(X, Y)) -> U21(tt(), X)
  , natsFrom(N) -> cons(N, natsFrom(s(N)))
  , sel(N, XS) -> U41(tt(), N, XS)
  , tail(cons(N, XS)) -> U71(tt(), XS)
  , take(N, XS) -> U81(tt(), N, XS) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

No rule is usable, rules are removed from the input problem.

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

Strict DPs:
  { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), N, XS))
  , U12^#(tt(), N, XS) -> c_2(splitAt^#(N, XS))
  , splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, XS))
  , U61^#(tt(), N, X, XS) -> c_4(U62^#(tt(), N, X, XS))
  , U41^#(tt(), N, XS) -> c_5(U42^#(tt(), N, XS))
  , U42^#(tt(), N, XS) -> c_6(afterNth^#(N, XS))
  , afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS))
  , U62^#(tt(), N, X, XS) -> c_8(U63^#(tt(), N, X, XS))
  , U63^#(tt(), N, X, XS) -> c_9(splitAt^#(N, XS))
  , U81^#(tt(), N, XS) -> c_10(U82^#(tt(), N, XS))
  , U82^#(tt(), N, XS) -> c_11(splitAt^#(N, XS))
  , natsFrom^#(N) -> c_12(natsFrom^#(s(N)))
  , sel^#(N, XS) -> c_13(U41^#(tt(), N, XS))
  , take^#(N, XS) -> c_14(U81^#(tt(), N, XS)) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

Consider the dependency graph

  1: U11^#(tt(), N, XS) -> c_1(U12^#(tt(), N, XS))
     -->_1 U12^#(tt(), N, XS) -> c_2(splitAt^#(N, XS)) :2
  
  2: U12^#(tt(), N, XS) -> c_2(splitAt^#(N, XS))
     -->_1 splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, XS)) :3
  
  3: splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, XS))
     -->_1 U61^#(tt(), N, X, XS) -> c_4(U62^#(tt(), N, X, XS)) :4
  
  4: U61^#(tt(), N, X, XS) -> c_4(U62^#(tt(), N, X, XS))
     -->_1 U62^#(tt(), N, X, XS) -> c_8(U63^#(tt(), N, X, XS)) :8
  
  5: U41^#(tt(), N, XS) -> c_5(U42^#(tt(), N, XS))
     -->_1 U42^#(tt(), N, XS) -> c_6(afterNth^#(N, XS)) :6
  
  6: U42^#(tt(), N, XS) -> c_6(afterNth^#(N, XS))
     -->_1 afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS)) :7
  
  7: afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS))
     -->_1 U11^#(tt(), N, XS) -> c_1(U12^#(tt(), N, XS)) :1
  
  8: U62^#(tt(), N, X, XS) -> c_8(U63^#(tt(), N, X, XS))
     -->_1 U63^#(tt(), N, X, XS) -> c_9(splitAt^#(N, XS)) :9
  
  9: U63^#(tt(), N, X, XS) -> c_9(splitAt^#(N, XS))
     -->_1 splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, XS)) :3
  
  10: U81^#(tt(), N, XS) -> c_10(U82^#(tt(), N, XS))
     -->_1 U82^#(tt(), N, XS) -> c_11(splitAt^#(N, XS)) :11
  
  11: U82^#(tt(), N, XS) -> c_11(splitAt^#(N, XS))
     -->_1 splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, XS)) :3
  
  12: natsFrom^#(N) -> c_12(natsFrom^#(s(N)))
     -->_1 natsFrom^#(N) -> c_12(natsFrom^#(s(N))) :12
  
  13: sel^#(N, XS) -> c_13(U41^#(tt(), N, XS))
     -->_1 U41^#(tt(), N, XS) -> c_5(U42^#(tt(), N, XS)) :5
  
  14: take^#(N, XS) -> c_14(U81^#(tt(), N, XS))
     -->_1 U81^#(tt(), N, XS) -> c_10(U82^#(tt(), N, XS)) :10
  

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_13(U41^#(tt(), N, XS))
  , take^#(N, XS) -> c_14(U81^#(tt(), N, XS)) }


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

Strict DPs:
  { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), N, XS))
  , U12^#(tt(), N, XS) -> c_2(splitAt^#(N, XS))
  , splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, XS))
  , U61^#(tt(), N, X, XS) -> c_4(U62^#(tt(), N, X, XS))
  , U41^#(tt(), N, XS) -> c_5(U42^#(tt(), N, XS))
  , U42^#(tt(), N, XS) -> c_6(afterNth^#(N, XS))
  , afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS))
  , U62^#(tt(), N, X, XS) -> c_8(U63^#(tt(), N, X, XS))
  , U63^#(tt(), N, X, XS) -> c_9(splitAt^#(N, XS))
  , U81^#(tt(), N, XS) -> c_10(U82^#(tt(), N, XS))
  , U82^#(tt(), N, XS) -> c_11(splitAt^#(N, XS))
  , natsFrom^#(N) -> c_12(natsFrom^#(s(N))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

Consider the dependency graph

  1: U11^#(tt(), N, XS) -> c_1(U12^#(tt(), N, XS))
     -->_1 U12^#(tt(), N, XS) -> c_2(splitAt^#(N, XS)) :2
  
  2: U12^#(tt(), N, XS) -> c_2(splitAt^#(N, XS))
     -->_1 splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, XS)) :3
  
  3: splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, XS))
     -->_1 U61^#(tt(), N, X, XS) -> c_4(U62^#(tt(), N, X, XS)) :4
  
  4: U61^#(tt(), N, X, XS) -> c_4(U62^#(tt(), N, X, XS))
     -->_1 U62^#(tt(), N, X, XS) -> c_8(U63^#(tt(), N, X, XS)) :8
  
  5: U41^#(tt(), N, XS) -> c_5(U42^#(tt(), N, XS))
     -->_1 U42^#(tt(), N, XS) -> c_6(afterNth^#(N, XS)) :6
  
  6: U42^#(tt(), N, XS) -> c_6(afterNth^#(N, XS))
     -->_1 afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS)) :7
  
  7: afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS))
     -->_1 U11^#(tt(), N, XS) -> c_1(U12^#(tt(), N, XS)) :1
  
  8: U62^#(tt(), N, X, XS) -> c_8(U63^#(tt(), N, X, XS))
     -->_1 U63^#(tt(), N, X, XS) -> c_9(splitAt^#(N, XS)) :9
  
  9: U63^#(tt(), N, X, XS) -> c_9(splitAt^#(N, XS))
     -->_1 splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, XS)) :3
  
  10: U81^#(tt(), N, XS) -> c_10(U82^#(tt(), N, XS))
     -->_1 U82^#(tt(), N, XS) -> c_11(splitAt^#(N, XS)) :11
  
  11: U82^#(tt(), N, XS) -> c_11(splitAt^#(N, XS))
     -->_1 splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, XS)) :3
  
  12: natsFrom^#(N) -> c_12(natsFrom^#(s(N)))
     -->_1 natsFrom^#(N) -> c_12(natsFrom^#(s(N))) :12
  

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).

  { U41^#(tt(), N, XS) -> c_5(U42^#(tt(), N, XS))
  , U81^#(tt(), N, XS) -> c_10(U82^#(tt(), N, XS)) }


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

Strict DPs:
  { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), N, XS))
  , U12^#(tt(), N, XS) -> c_2(splitAt^#(N, XS))
  , splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, XS))
  , U61^#(tt(), N, X, XS) -> c_4(U62^#(tt(), N, X, XS))
  , U42^#(tt(), N, XS) -> c_6(afterNth^#(N, XS))
  , afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS))
  , U62^#(tt(), N, X, XS) -> c_8(U63^#(tt(), N, X, XS))
  , U63^#(tt(), N, X, XS) -> c_9(splitAt^#(N, XS))
  , U82^#(tt(), N, XS) -> c_11(splitAt^#(N, XS))
  , natsFrom^#(N) -> c_12(natsFrom^#(s(N))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

Consider the dependency graph

  1: U11^#(tt(), N, XS) -> c_1(U12^#(tt(), N, XS))
     -->_1 U12^#(tt(), N, XS) -> c_2(splitAt^#(N, XS)) :2
  
  2: U12^#(tt(), N, XS) -> c_2(splitAt^#(N, XS))
     -->_1 splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, XS)) :3
  
  3: splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, XS))
     -->_1 U61^#(tt(), N, X, XS) -> c_4(U62^#(tt(), N, X, XS)) :4
  
  4: U61^#(tt(), N, X, XS) -> c_4(U62^#(tt(), N, X, XS))
     -->_1 U62^#(tt(), N, X, XS) -> c_8(U63^#(tt(), N, X, XS)) :7
  
  5: U42^#(tt(), N, XS) -> c_6(afterNth^#(N, XS))
     -->_1 afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS)) :6
  
  6: afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS))
     -->_1 U11^#(tt(), N, XS) -> c_1(U12^#(tt(), N, XS)) :1
  
  7: U62^#(tt(), N, X, XS) -> c_8(U63^#(tt(), N, X, XS))
     -->_1 U63^#(tt(), N, X, XS) -> c_9(splitAt^#(N, XS)) :8
  
  8: U63^#(tt(), N, X, XS) -> c_9(splitAt^#(N, XS))
     -->_1 splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, XS)) :3
  
  9: U82^#(tt(), N, XS) -> c_11(splitAt^#(N, XS))
     -->_1 splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, XS)) :3
  
  10: natsFrom^#(N) -> c_12(natsFrom^#(s(N)))
     -->_1 natsFrom^#(N) -> c_12(natsFrom^#(s(N))) :10
  

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).

  { U42^#(tt(), N, XS) -> c_6(afterNth^#(N, XS))
  , U82^#(tt(), N, XS) -> c_11(splitAt^#(N, XS)) }


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

Strict DPs:
  { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), N, XS))
  , U12^#(tt(), N, XS) -> c_2(splitAt^#(N, XS))
  , splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, XS))
  , U61^#(tt(), N, X, XS) -> c_4(U62^#(tt(), N, X, XS))
  , afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS))
  , U62^#(tt(), N, X, XS) -> c_8(U63^#(tt(), N, X, XS))
  , U63^#(tt(), N, X, XS) -> c_9(splitAt^#(N, XS))
  , natsFrom^#(N) -> c_12(natsFrom^#(s(N))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

Consider the dependency graph

  1: U11^#(tt(), N, XS) -> c_1(U12^#(tt(), N, XS))
     -->_1 U12^#(tt(), N, XS) -> c_2(splitAt^#(N, XS)) :2
  
  2: U12^#(tt(), N, XS) -> c_2(splitAt^#(N, XS))
     -->_1 splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, XS)) :3
  
  3: splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, XS))
     -->_1 U61^#(tt(), N, X, XS) -> c_4(U62^#(tt(), N, X, XS)) :4
  
  4: U61^#(tt(), N, X, XS) -> c_4(U62^#(tt(), N, X, XS))
     -->_1 U62^#(tt(), N, X, XS) -> c_8(U63^#(tt(), N, X, XS)) :6
  
  5: afterNth^#(N, XS) -> c_7(U11^#(tt(), N, XS))
     -->_1 U11^#(tt(), N, XS) -> c_1(U12^#(tt(), N, XS)) :1
  
  6: U62^#(tt(), N, X, XS) -> c_8(U63^#(tt(), N, X, XS))
     -->_1 U63^#(tt(), N, X, XS) -> c_9(splitAt^#(N, XS)) :7
  
  7: U63^#(tt(), N, X, XS) -> c_9(splitAt^#(N, XS))
     -->_1 splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, XS)) :3
  
  8: natsFrom^#(N) -> c_12(natsFrom^#(s(N)))
     -->_1 natsFrom^#(N) -> c_12(natsFrom^#(s(N))) :8
  

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_7(U11^#(tt(), N, XS)) }


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

Strict DPs:
  { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), N, XS))
  , U12^#(tt(), N, XS) -> c_2(splitAt^#(N, XS))
  , splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, XS))
  , U61^#(tt(), N, X, XS) -> c_4(U62^#(tt(), N, X, XS))
  , U62^#(tt(), N, X, XS) -> c_8(U63^#(tt(), N, X, XS))
  , U63^#(tt(), N, X, XS) -> c_9(splitAt^#(N, XS))
  , natsFrom^#(N) -> c_12(natsFrom^#(s(N))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

Consider the dependency graph

  1: U11^#(tt(), N, XS) -> c_1(U12^#(tt(), N, XS))
     -->_1 U12^#(tt(), N, XS) -> c_2(splitAt^#(N, XS)) :2
  
  2: U12^#(tt(), N, XS) -> c_2(splitAt^#(N, XS))
     -->_1 splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, XS)) :3
  
  3: splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, XS))
     -->_1 U61^#(tt(), N, X, XS) -> c_4(U62^#(tt(), N, X, XS)) :4
  
  4: U61^#(tt(), N, X, XS) -> c_4(U62^#(tt(), N, X, XS))
     -->_1 U62^#(tt(), N, X, XS) -> c_8(U63^#(tt(), N, X, XS)) :5
  
  5: U62^#(tt(), N, X, XS) -> c_8(U63^#(tt(), N, X, XS))
     -->_1 U63^#(tt(), N, X, XS) -> c_9(splitAt^#(N, XS)) :6
  
  6: U63^#(tt(), N, X, XS) -> c_9(splitAt^#(N, XS))
     -->_1 splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, XS)) :3
  
  7: natsFrom^#(N) -> c_12(natsFrom^#(s(N)))
     -->_1 natsFrom^#(N) -> c_12(natsFrom^#(s(N))) :7
  

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).

  { U11^#(tt(), N, XS) -> c_1(U12^#(tt(), N, XS)) }


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

Strict DPs:
  { U12^#(tt(), N, XS) -> c_2(splitAt^#(N, XS))
  , splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, XS))
  , U61^#(tt(), N, X, XS) -> c_4(U62^#(tt(), N, X, XS))
  , U62^#(tt(), N, X, XS) -> c_8(U63^#(tt(), N, X, XS))
  , U63^#(tt(), N, X, XS) -> c_9(splitAt^#(N, XS))
  , natsFrom^#(N) -> c_12(natsFrom^#(s(N))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

Consider the dependency graph

  1: U12^#(tt(), N, XS) -> c_2(splitAt^#(N, XS))
     -->_1 splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, XS)) :2
  
  2: splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, XS))
     -->_1 U61^#(tt(), N, X, XS) -> c_4(U62^#(tt(), N, X, XS)) :3
  
  3: U61^#(tt(), N, X, XS) -> c_4(U62^#(tt(), N, X, XS))
     -->_1 U62^#(tt(), N, X, XS) -> c_8(U63^#(tt(), N, X, XS)) :4
  
  4: U62^#(tt(), N, X, XS) -> c_8(U63^#(tt(), N, X, XS))
     -->_1 U63^#(tt(), N, X, XS) -> c_9(splitAt^#(N, XS)) :5
  
  5: U63^#(tt(), N, X, XS) -> c_9(splitAt^#(N, XS))
     -->_1 splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, XS)) :2
  
  6: natsFrom^#(N) -> c_12(natsFrom^#(s(N)))
     -->_1 natsFrom^#(N) -> c_12(natsFrom^#(s(N))) :6
  

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).

  { U12^#(tt(), N, XS) -> c_2(splitAt^#(N, XS)) }


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

Strict DPs:
  { splitAt^#(s(N), cons(X, XS)) -> c_3(U61^#(tt(), N, X, XS))
  , U61^#(tt(), N, X, XS) -> c_4(U62^#(tt(), N, X, XS))
  , U62^#(tt(), N, X, XS) -> c_8(U63^#(tt(), N, X, XS))
  , U63^#(tt(), N, X, XS) -> c_9(splitAt^#(N, XS))
  , natsFrom^#(N) -> c_12(natsFrom^#(s(N))) }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

None of the processors succeeded.

Details of failed attempt(s):
-----------------------------
1) 'matrices' failed due to the following reason:
   
   None of the processors succeeded.
   
   Details of failed attempt(s):
   -----------------------------
   1) 'matrix interpretation of dimension 4' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   2) 'matrix interpretation of dimension 3' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   3) 'matrix interpretation of dimension 3' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   4) 'matrix interpretation of dimension 2' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   5) 'matrix interpretation of dimension 2' failed due to the
      following reason:
      
      The input cannot be shown compatible
   
   6) 'matrix interpretation of dimension 1' failed due to the
      following reason:
      
      The input cannot be shown compatible
   

2) 'empty' failed due to the following reason:
   
   Empty strict component of the problem is NOT empty.


Arrrr..