MAYBE
Time: 0.002231
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)}
  UR:
   {               natsFrom N -> cons(N, n__natsFrom s N),
                   natsFrom X -> n__natsFrom X,
             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,
              afterNth(N, XS) -> snd splitAt(N, XS),
                      a(x, y) -> x,
                      a(x, y) -> y}
   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