MAYBE
Time: 0.003841
TRS:
 {               natsFrom N -> cons(N, n__natsFrom s N),
                 natsFrom X -> n__natsFrom X,
           fst pair(XS, YS) -> XS,
           snd pair(XS, YS) -> YS,
  splitAt(s N, cons(X, XS)) -> u(splitAt(N, activate XS), N, X, activate XS),
           splitAt(0(), XS) -> pair(nil(), XS),
  u(pair(YS, ZS), N, X, XS) -> pair(cons(activate X, YS), ZS),
                 activate X -> X,
     activate n__natsFrom X -> natsFrom X,
           head cons(N, XS) -> N,
           tail cons(N, XS) -> activate XS,
            afterNth(N, XS) -> snd splitAt(N, XS),
                 sel(N, XS) -> head afterNth(N, XS),
                take(N, XS) -> fst splitAt(N, XS)}
 DP:
  DP:
   {splitAt#(s N, cons(X, XS)) -> splitAt#(N, activate XS),
    splitAt#(s N, cons(X, XS)) -> u#(splitAt(N, activate XS), N, X, activate XS),
    splitAt#(s N, cons(X, XS)) -> activate# XS,
    u#(pair(YS, ZS), N, X, XS) -> activate# X,
       activate# n__natsFrom X -> natsFrom# X,
             tail# cons(N, XS) -> activate# XS,
              afterNth#(N, XS) -> snd# splitAt(N, XS),
              afterNth#(N, XS) -> splitAt#(N, XS),
                   sel#(N, XS) -> head# afterNth(N, XS),
                   sel#(N, XS) -> afterNth#(N, XS),
                  take#(N, XS) -> fst# splitAt(N, XS),
                  take#(N, XS) -> splitAt#(N, XS)}
  TRS:
  {               natsFrom N -> cons(N, n__natsFrom s N),
                  natsFrom X -> n__natsFrom X,
            fst pair(XS, YS) -> XS,
            snd pair(XS, YS) -> YS,
   splitAt(s N, cons(X, XS)) -> u(splitAt(N, activate XS), N, X, activate XS),
            splitAt(0(), XS) -> pair(nil(), XS),
   u(pair(YS, ZS), N, X, XS) -> pair(cons(activate X, YS), ZS),
                  activate X -> X,
      activate n__natsFrom X -> natsFrom X,
            head cons(N, XS) -> N,
            tail cons(N, XS) -> activate XS,
             afterNth(N, XS) -> snd splitAt(N, XS),
                  sel(N, XS) -> head afterNth(N, XS),
                 take(N, XS) -> fst splitAt(N, XS)}
  EDG:
   {(splitAt#(s N, cons(X, XS)) -> u#(splitAt(N, activate XS), N, X, activate XS), u#(pair(YS, ZS), N, X, XS) -> activate# X)
    (splitAt#(s N, cons(X, XS)) -> activate# XS, activate# n__natsFrom X -> natsFrom# X)
    (afterNth#(N, XS) -> splitAt#(N, XS), splitAt#(s N, cons(X, XS)) -> activate# XS)
    (afterNth#(N, XS) -> splitAt#(N, XS), splitAt#(s N, cons(X, XS)) -> u#(splitAt(N, activate XS), N, X, activate XS))
    (afterNth#(N, XS) -> splitAt#(N, XS), splitAt#(s N, cons(X, XS)) -> splitAt#(N, activate XS))
    (take#(N, XS) -> splitAt#(N, XS), splitAt#(s N, cons(X, XS)) -> activate# XS)
    (take#(N, XS) -> splitAt#(N, XS), splitAt#(s N, cons(X, XS)) -> u#(splitAt(N, activate XS), N, X, activate XS))
    (take#(N, XS) -> splitAt#(N, XS), splitAt#(s N, cons(X, XS)) -> splitAt#(N, activate XS))
    (u#(pair(YS, ZS), N, X, XS) -> activate# X, activate# n__natsFrom X -> natsFrom# X)
    (sel#(N, XS) -> afterNth#(N, XS), afterNth#(N, XS) -> snd# splitAt(N, XS))
    (sel#(N, XS) -> afterNth#(N, XS), afterNth#(N, XS) -> splitAt#(N, XS))
    (tail# cons(N, XS) -> activate# XS, activate# n__natsFrom X -> natsFrom# X)
    (splitAt#(s N, cons(X, XS)) -> splitAt#(N, activate XS), splitAt#(s N, cons(X, XS)) -> splitAt#(N, activate XS))
    (splitAt#(s N, cons(X, XS)) -> splitAt#(N, activate XS), splitAt#(s N, cons(X, XS)) -> u#(splitAt(N, activate XS), N, X, activate XS))
    (splitAt#(s N, cons(X, XS)) -> splitAt#(N, activate XS), splitAt#(s N, cons(X, XS)) -> activate# XS)}
   STATUS:
    arrows: 0.895833
    SCCS (1):
     Scc:
      {splitAt#(s N, cons(X, XS)) -> splitAt#(N, activate XS)}
     
     
     
     
     
     
     
     
     SCC (1):
      Strict:
       {splitAt#(s N, cons(X, XS)) -> splitAt#(N, activate XS)}
      Weak:
      {               natsFrom N -> cons(N, n__natsFrom s N),
                      natsFrom X -> n__natsFrom X,
                fst pair(XS, YS) -> XS,
                snd pair(XS, YS) -> YS,
       splitAt(s N, cons(X, XS)) -> u(splitAt(N, activate XS), N, X, activate XS),
                splitAt(0(), XS) -> pair(nil(), XS),
       u(pair(YS, ZS), N, X, XS) -> pair(cons(activate X, YS), ZS),
                      activate X -> X,
          activate n__natsFrom X -> natsFrom X,
                head cons(N, XS) -> N,
                tail cons(N, XS) -> activate XS,
                 afterNth(N, XS) -> snd splitAt(N, XS),
                      sel(N, XS) -> head afterNth(N, XS),
                     take(N, XS) -> fst splitAt(N, XS)}
      Open