MAYBE
Time: 0.011825
TRS:
 {     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,
        U11(tt(), N, X, XS) -> U12(splitAt(activate N, activate XS), activate X),
             snd pair(X, Y) -> Y,
            afterNth(N, XS) -> snd splitAt(N, XS),
               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)}
 DP:
  DP:
   {     U12#(pair(YS, ZS), X) -> activate# X,
    splitAt#(s N, cons(X, XS)) -> activate# XS,
    splitAt#(s N, cons(X, XS)) -> U11#(tt(), N, X, activate XS),
       activate# n__natsFrom X -> natsFrom# X,
          U11#(tt(), N, X, XS) -> U12#(splitAt(activate N, activate XS), activate X),
          U11#(tt(), N, X, XS) -> splitAt#(activate N, activate XS),
          U11#(tt(), N, X, XS) -> activate# N,
          U11#(tt(), N, X, XS) -> activate# XS,
          U11#(tt(), N, X, XS) -> activate# X,
              afterNth#(N, XS) -> splitAt#(N, XS),
              afterNth#(N, XS) -> snd# splitAt(N, XS),
                 and#(tt(), X) -> activate# X,
                   sel#(N, XS) -> afterNth#(N, XS),
                   sel#(N, XS) -> head# afterNth(N, XS),
             tail# cons(N, XS) -> activate# XS,
                  take#(N, XS) -> splitAt#(N, XS),
                  take#(N, XS) -> fst# splitAt(N, XS)}
  TRS:
  {     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,
         U11(tt(), N, X, XS) -> U12(splitAt(activate N, activate XS), activate X),
              snd pair(X, Y) -> Y,
             afterNth(N, XS) -> snd splitAt(N, XS),
                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)}
  EDG:
   {(U11#(tt(), N, X, XS) -> splitAt#(activate N, activate XS), splitAt#(s N, cons(X, XS)) -> U11#(tt(), N, X, activate XS))
    (U11#(tt(), N, X, XS) -> splitAt#(activate N, activate XS), splitAt#(s N, cons(X, XS)) -> activate# XS)
    (U12#(pair(YS, ZS), X) -> activate# X, activate# n__natsFrom X -> natsFrom# X)
    (U11#(tt(), N, X, XS) -> activate# X, activate# n__natsFrom X -> natsFrom# X)
    (splitAt#(s N, cons(X, XS)) -> activate# XS, activate# n__natsFrom X -> natsFrom# X)
    (tail# cons(N, XS) -> activate# XS, 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))
    (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)) -> U11#(tt(), N, X, activate XS))
    (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)) -> U11#(tt(), N, X, activate XS))
    (U11#(tt(), N, X, XS) -> activate# N, activate# n__natsFrom X -> natsFrom# X)
    (U11#(tt(), N, X, XS) -> activate# XS, activate# n__natsFrom X -> natsFrom# X)
    (and#(tt(), X) -> activate# X, activate# n__natsFrom X -> natsFrom# X)
    (splitAt#(s N, cons(X, XS)) -> U11#(tt(), N, X, activate XS), U11#(tt(), N, X, XS) -> U12#(splitAt(activate N, activate XS), activate X))
    (splitAt#(s N, cons(X, XS)) -> U11#(tt(), N, X, activate XS), U11#(tt(), N, X, XS) -> splitAt#(activate N, activate XS))
    (splitAt#(s N, cons(X, XS)) -> U11#(tt(), N, X, activate XS), U11#(tt(), N, X, XS) -> activate# N)
    (splitAt#(s N, cons(X, XS)) -> U11#(tt(), N, X, activate XS), U11#(tt(), N, X, XS) -> activate# XS)
    (splitAt#(s N, cons(X, XS)) -> U11#(tt(), N, X, activate XS), U11#(tt(), N, X, XS) -> activate# X)
    (U11#(tt(), N, X, XS) -> U12#(splitAt(activate N, activate XS), activate X), U12#(pair(YS, ZS), X) -> activate# X)}
   STATUS:
    arrows: 0.927336
    SCCS (1):
     Scc:
      {splitAt#(s N, cons(X, XS)) -> U11#(tt(), N, X, activate XS),
             U11#(tt(), N, X, XS) -> splitAt#(activate N, activate XS)}
     
     
     
     
     
     
     
     
     
     SCC (2):
      Strict:
       {splitAt#(s N, cons(X, XS)) -> U11#(tt(), N, X, activate XS),
              U11#(tt(), N, X, XS) -> splitAt#(activate N, activate XS)}
      Weak:
      {     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,
             U11(tt(), N, X, XS) -> U12(splitAt(activate N, activate XS), activate X),
                  snd pair(X, Y) -> Y,
                 afterNth(N, XS) -> snd splitAt(N, XS),
                    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)}
      Open