MAYBE
Time: 0.343043
TRS:
 {              a__U12(X1, X2) -> U12(X1, X2),
       a__U12(pair(YS, ZS), X) -> pair(cons(mark X, YS), mark ZS),
            a__splitAt(X1, X2) -> splitAt(X1, X2),
  a__splitAt(s N, cons(X, XS)) -> a__U11(tt(), N, X, XS),
           a__splitAt(0(), XS) -> pair(nil(), mark XS),
                     mark tt() -> tt(),
             mark pair(X1, X2) -> pair(mark X1, mark X2),
             mark cons(X1, X2) -> cons(mark X1, X2),
               mark natsFrom X -> a__natsFrom mark X,
                      mark s X -> s mark X,
                    mark nil() -> nil(),
                      mark 0() -> 0(),
      mark U11(X1, X2, X3, X4) -> a__U11(mark X1, X2, X3, X4),
              mark U12(X1, X2) -> a__U12(mark X1, X2),
          mark splitAt(X1, X2) -> a__splitAt(mark X1, mark X2),
         mark afterNth(X1, X2) -> a__afterNth(mark X1, mark X2),
                    mark snd X -> a__snd mark X,
              mark and(X1, X2) -> a__and(mark X1, X2),
                    mark fst X -> a__fst mark X,
                   mark head X -> a__head mark X,
              mark sel(X1, X2) -> a__sel(mark X1, mark X2),
                   mark tail X -> a__tail mark X,
             mark take(X1, X2) -> a__take(mark X1, mark X2),
        a__U11(X1, X2, X3, X4) -> U11(X1, X2, X3, X4),
        a__U11(tt(), N, X, XS) -> a__U12(a__splitAt(mark N, mark XS), X),
                      a__snd X -> snd X,
             a__snd pair(X, Y) -> mark Y,
            a__afterNth(N, XS) -> a__snd a__splitAt(mark N, mark XS),
           a__afterNth(X1, X2) -> afterNth(X1, X2),
                a__and(X1, X2) -> and(X1, X2),
               a__and(tt(), X) -> mark X,
                      a__fst X -> fst X,
             a__fst pair(X, Y) -> mark X,
                     a__head X -> head X,
           a__head cons(N, XS) -> mark N,
                 a__natsFrom N -> cons(mark N, natsFrom s N),
                 a__natsFrom X -> natsFrom X,
                 a__sel(N, XS) -> a__head a__afterNth(mark N, mark XS),
                a__sel(X1, X2) -> sel(X1, X2),
                     a__tail X -> tail X,
           a__tail cons(N, XS) -> mark XS,
                a__take(N, XS) -> a__fst a__splitAt(mark N, mark XS),
               a__take(X1, X2) -> take(X1, X2)}
 DP:
  DP:
   {     a__U12#(pair(YS, ZS), X) -> mark# X,
         a__U12#(pair(YS, ZS), X) -> mark# ZS,
    a__splitAt#(s N, cons(X, XS)) -> a__U11#(tt(), N, X, XS),
             a__splitAt#(0(), XS) -> mark# XS,
               mark# pair(X1, X2) -> mark# X1,
               mark# pair(X1, X2) -> mark# X2,
               mark# cons(X1, X2) -> mark# X1,
                 mark# natsFrom X -> mark# X,
                 mark# natsFrom X -> a__natsFrom# mark X,
                        mark# s X -> mark# X,
        mark# U11(X1, X2, X3, X4) -> mark# X1,
        mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4),
                mark# U12(X1, X2) -> a__U12#(mark X1, X2),
                mark# U12(X1, X2) -> mark# X1,
            mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2),
            mark# splitAt(X1, X2) -> mark# X1,
            mark# splitAt(X1, X2) -> mark# X2,
           mark# afterNth(X1, X2) -> mark# X1,
           mark# afterNth(X1, X2) -> mark# X2,
           mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2),
                      mark# snd X -> mark# X,
                      mark# snd X -> a__snd# mark X,
                mark# and(X1, X2) -> mark# X1,
                mark# and(X1, X2) -> a__and#(mark X1, X2),
                      mark# fst X -> mark# X,
                      mark# fst X -> a__fst# mark X,
                     mark# head X -> mark# X,
                     mark# head X -> a__head# mark X,
                mark# sel(X1, X2) -> mark# X1,
                mark# sel(X1, X2) -> mark# X2,
                mark# sel(X1, X2) -> a__sel#(mark X1, mark X2),
                     mark# tail X -> mark# X,
                     mark# tail X -> a__tail# mark X,
               mark# take(X1, X2) -> mark# X1,
               mark# take(X1, X2) -> mark# X2,
               mark# take(X1, X2) -> a__take#(mark X1, mark X2),
          a__U11#(tt(), N, X, XS) -> a__U12#(a__splitAt(mark N, mark XS), X),
          a__U11#(tt(), N, X, XS) -> a__splitAt#(mark N, mark XS),
          a__U11#(tt(), N, X, XS) -> mark# N,
          a__U11#(tt(), N, X, XS) -> mark# XS,
               a__snd# pair(X, Y) -> mark# Y,
              a__afterNth#(N, XS) -> a__splitAt#(mark N, mark XS),
              a__afterNth#(N, XS) -> mark# N,
              a__afterNth#(N, XS) -> mark# XS,
              a__afterNth#(N, XS) -> a__snd# a__splitAt(mark N, mark XS),
                 a__and#(tt(), X) -> mark# X,
               a__fst# pair(X, Y) -> mark# X,
             a__head# cons(N, XS) -> mark# N,
                   a__natsFrom# N -> mark# N,
                   a__sel#(N, XS) -> mark# N,
                   a__sel#(N, XS) -> mark# XS,
                   a__sel#(N, XS) -> a__afterNth#(mark N, mark XS),
                   a__sel#(N, XS) -> a__head# a__afterNth(mark N, mark XS),
             a__tail# cons(N, XS) -> mark# XS,
                  a__take#(N, XS) -> a__splitAt#(mark N, mark XS),
                  a__take#(N, XS) -> mark# N,
                  a__take#(N, XS) -> mark# XS,
                  a__take#(N, XS) -> a__fst# a__splitAt(mark N, mark XS)}
  TRS:
  {              a__U12(X1, X2) -> U12(X1, X2),
        a__U12(pair(YS, ZS), X) -> pair(cons(mark X, YS), mark ZS),
             a__splitAt(X1, X2) -> splitAt(X1, X2),
   a__splitAt(s N, cons(X, XS)) -> a__U11(tt(), N, X, XS),
            a__splitAt(0(), XS) -> pair(nil(), mark XS),
                      mark tt() -> tt(),
              mark pair(X1, X2) -> pair(mark X1, mark X2),
              mark cons(X1, X2) -> cons(mark X1, X2),
                mark natsFrom X -> a__natsFrom mark X,
                       mark s X -> s mark X,
                     mark nil() -> nil(),
                       mark 0() -> 0(),
       mark U11(X1, X2, X3, X4) -> a__U11(mark X1, X2, X3, X4),
               mark U12(X1, X2) -> a__U12(mark X1, X2),
           mark splitAt(X1, X2) -> a__splitAt(mark X1, mark X2),
          mark afterNth(X1, X2) -> a__afterNth(mark X1, mark X2),
                     mark snd X -> a__snd mark X,
               mark and(X1, X2) -> a__and(mark X1, X2),
                     mark fst X -> a__fst mark X,
                    mark head X -> a__head mark X,
               mark sel(X1, X2) -> a__sel(mark X1, mark X2),
                    mark tail X -> a__tail mark X,
              mark take(X1, X2) -> a__take(mark X1, mark X2),
         a__U11(X1, X2, X3, X4) -> U11(X1, X2, X3, X4),
         a__U11(tt(), N, X, XS) -> a__U12(a__splitAt(mark N, mark XS), X),
                       a__snd X -> snd X,
              a__snd pair(X, Y) -> mark Y,
             a__afterNth(N, XS) -> a__snd a__splitAt(mark N, mark XS),
            a__afterNth(X1, X2) -> afterNth(X1, X2),
                 a__and(X1, X2) -> and(X1, X2),
                a__and(tt(), X) -> mark X,
                       a__fst X -> fst X,
              a__fst pair(X, Y) -> mark X,
                      a__head X -> head X,
            a__head cons(N, XS) -> mark N,
                  a__natsFrom N -> cons(mark N, natsFrom s N),
                  a__natsFrom X -> natsFrom X,
                  a__sel(N, XS) -> a__head a__afterNth(mark N, mark XS),
                 a__sel(X1, X2) -> sel(X1, X2),
                      a__tail X -> tail X,
            a__tail cons(N, XS) -> mark XS,
                 a__take(N, XS) -> a__fst a__splitAt(mark N, mark XS),
                a__take(X1, X2) -> take(X1, X2)}
  UR:
   {              a__U12(X1, X2) -> U12(X1, X2),
         a__U12(pair(YS, ZS), X) -> pair(cons(mark X, YS), mark ZS),
              a__splitAt(X1, X2) -> splitAt(X1, X2),
    a__splitAt(s N, cons(X, XS)) -> a__U11(tt(), N, X, XS),
             a__splitAt(0(), XS) -> pair(nil(), mark XS),
                       mark tt() -> tt(),
               mark pair(X1, X2) -> pair(mark X1, mark X2),
               mark cons(X1, X2) -> cons(mark X1, X2),
                 mark natsFrom X -> a__natsFrom mark X,
                        mark s X -> s mark X,
                      mark nil() -> nil(),
                        mark 0() -> 0(),
        mark U11(X1, X2, X3, X4) -> a__U11(mark X1, X2, X3, X4),
                mark U12(X1, X2) -> a__U12(mark X1, X2),
            mark splitAt(X1, X2) -> a__splitAt(mark X1, mark X2),
           mark afterNth(X1, X2) -> a__afterNth(mark X1, mark X2),
                      mark snd X -> a__snd mark X,
                mark and(X1, X2) -> a__and(mark X1, X2),
                      mark fst X -> a__fst mark X,
                     mark head X -> a__head mark X,
                mark sel(X1, X2) -> a__sel(mark X1, mark X2),
                     mark tail X -> a__tail mark X,
               mark take(X1, X2) -> a__take(mark X1, mark X2),
          a__U11(X1, X2, X3, X4) -> U11(X1, X2, X3, X4),
          a__U11(tt(), N, X, XS) -> a__U12(a__splitAt(mark N, mark XS), X),
                        a__snd X -> snd X,
               a__snd pair(X, Y) -> mark Y,
              a__afterNth(N, XS) -> a__snd a__splitAt(mark N, mark XS),
             a__afterNth(X1, X2) -> afterNth(X1, X2),
                  a__and(X1, X2) -> and(X1, X2),
                 a__and(tt(), X) -> mark X,
                        a__fst X -> fst X,
               a__fst pair(X, Y) -> mark X,
                       a__head X -> head X,
             a__head cons(N, XS) -> mark N,
                   a__natsFrom N -> cons(mark N, natsFrom s N),
                   a__natsFrom X -> natsFrom X,
                   a__sel(N, XS) -> a__head a__afterNth(mark N, mark XS),
                  a__sel(X1, X2) -> sel(X1, X2),
                       a__tail X -> tail X,
             a__tail cons(N, XS) -> mark XS,
                  a__take(N, XS) -> a__fst a__splitAt(mark N, mark XS),
                 a__take(X1, X2) -> take(X1, X2)}
   EDG:
    {
     (a__U11#(tt(), N, X, XS) -> mark# N, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (a__U11#(tt(), N, X, XS) -> mark# N, mark# take(X1, X2) -> mark# X2)
     (a__U11#(tt(), N, X, XS) -> mark# N, mark# take(X1, X2) -> mark# X1)
     (a__U11#(tt(), N, X, XS) -> mark# N, mark# tail X -> a__tail# mark X)
     (a__U11#(tt(), N, X, XS) -> mark# N, mark# tail X -> mark# X)
     (a__U11#(tt(), N, X, XS) -> mark# N, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (a__U11#(tt(), N, X, XS) -> mark# N, mark# sel(X1, X2) -> mark# X2)
     (a__U11#(tt(), N, X, XS) -> mark# N, mark# sel(X1, X2) -> mark# X1)
     (a__U11#(tt(), N, X, XS) -> mark# N, mark# head X -> a__head# mark X)
     (a__U11#(tt(), N, X, XS) -> mark# N, mark# head X -> mark# X)
     (a__U11#(tt(), N, X, XS) -> mark# N, mark# fst X -> a__fst# mark X)
     (a__U11#(tt(), N, X, XS) -> mark# N, mark# fst X -> mark# X)
     (a__U11#(tt(), N, X, XS) -> mark# N, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (a__U11#(tt(), N, X, XS) -> mark# N, mark# and(X1, X2) -> mark# X1)
     (a__U11#(tt(), N, X, XS) -> mark# N, mark# snd X -> a__snd# mark X)
     (a__U11#(tt(), N, X, XS) -> mark# N, mark# snd X -> mark# X)
     (a__U11#(tt(), N, X, XS) -> mark# N, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (a__U11#(tt(), N, X, XS) -> mark# N, mark# afterNth(X1, X2) -> mark# X2)
     (a__U11#(tt(), N, X, XS) -> mark# N, mark# afterNth(X1, X2) -> mark# X1)
     (a__U11#(tt(), N, X, XS) -> mark# N, mark# splitAt(X1, X2) -> mark# X2)
     (a__U11#(tt(), N, X, XS) -> mark# N, mark# splitAt(X1, X2) -> mark# X1)
     (a__U11#(tt(), N, X, XS) -> mark# N, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (a__U11#(tt(), N, X, XS) -> mark# N, mark# U12(X1, X2) -> mark# X1)
     (a__U11#(tt(), N, X, XS) -> mark# N, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (a__U11#(tt(), N, X, XS) -> mark# N, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (a__U11#(tt(), N, X, XS) -> mark# N, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (a__U11#(tt(), N, X, XS) -> mark# N, mark# s X -> mark# X)
     (a__U11#(tt(), N, X, XS) -> mark# N, mark# natsFrom X -> a__natsFrom# mark X)
     (a__U11#(tt(), N, X, XS) -> mark# N, mark# natsFrom X -> mark# X)
     (a__U11#(tt(), N, X, XS) -> mark# N, mark# cons(X1, X2) -> mark# X1)
     (a__U11#(tt(), N, X, XS) -> mark# N, mark# pair(X1, X2) -> mark# X2)
     (a__U11#(tt(), N, X, XS) -> mark# N, mark# pair(X1, X2) -> mark# X1)
     (a__head# cons(N, XS) -> mark# N, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (a__head# cons(N, XS) -> mark# N, mark# take(X1, X2) -> mark# X2)
     (a__head# cons(N, XS) -> mark# N, mark# take(X1, X2) -> mark# X1)
     (a__head# cons(N, XS) -> mark# N, mark# tail X -> a__tail# mark X)
     (a__head# cons(N, XS) -> mark# N, mark# tail X -> mark# X)
     (a__head# cons(N, XS) -> mark# N, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (a__head# cons(N, XS) -> mark# N, mark# sel(X1, X2) -> mark# X2)
     (a__head# cons(N, XS) -> mark# N, mark# sel(X1, X2) -> mark# X1)
     (a__head# cons(N, XS) -> mark# N, mark# head X -> a__head# mark X)
     (a__head# cons(N, XS) -> mark# N, mark# head X -> mark# X)
     (a__head# cons(N, XS) -> mark# N, mark# fst X -> a__fst# mark X)
     (a__head# cons(N, XS) -> mark# N, mark# fst X -> mark# X)
     (a__head# cons(N, XS) -> mark# N, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (a__head# cons(N, XS) -> mark# N, mark# and(X1, X2) -> mark# X1)
     (a__head# cons(N, XS) -> mark# N, mark# snd X -> a__snd# mark X)
     (a__head# cons(N, XS) -> mark# N, mark# snd X -> mark# X)
     (a__head# cons(N, XS) -> mark# N, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (a__head# cons(N, XS) -> mark# N, mark# afterNth(X1, X2) -> mark# X2)
     (a__head# cons(N, XS) -> mark# N, mark# afterNth(X1, X2) -> mark# X1)
     (a__head# cons(N, XS) -> mark# N, mark# splitAt(X1, X2) -> mark# X2)
     (a__head# cons(N, XS) -> mark# N, mark# splitAt(X1, X2) -> mark# X1)
     (a__head# cons(N, XS) -> mark# N, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (a__head# cons(N, XS) -> mark# N, mark# U12(X1, X2) -> mark# X1)
     (a__head# cons(N, XS) -> mark# N, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (a__head# cons(N, XS) -> mark# N, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (a__head# cons(N, XS) -> mark# N, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (a__head# cons(N, XS) -> mark# N, mark# s X -> mark# X)
     (a__head# cons(N, XS) -> mark# N, mark# natsFrom X -> a__natsFrom# mark X)
     (a__head# cons(N, XS) -> mark# N, mark# natsFrom X -> mark# X)
     (a__head# cons(N, XS) -> mark# N, mark# cons(X1, X2) -> mark# X1)
     (a__head# cons(N, XS) -> mark# N, mark# pair(X1, X2) -> mark# X2)
     (a__head# cons(N, XS) -> mark# N, mark# pair(X1, X2) -> mark# X1)
     (a__sel#(N, XS) -> mark# N, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (a__sel#(N, XS) -> mark# N, mark# take(X1, X2) -> mark# X2)
     (a__sel#(N, XS) -> mark# N, mark# take(X1, X2) -> mark# X1)
     (a__sel#(N, XS) -> mark# N, mark# tail X -> a__tail# mark X)
     (a__sel#(N, XS) -> mark# N, mark# tail X -> mark# X)
     (a__sel#(N, XS) -> mark# N, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (a__sel#(N, XS) -> mark# N, mark# sel(X1, X2) -> mark# X2)
     (a__sel#(N, XS) -> mark# N, mark# sel(X1, X2) -> mark# X1)
     (a__sel#(N, XS) -> mark# N, mark# head X -> a__head# mark X)
     (a__sel#(N, XS) -> mark# N, mark# head X -> mark# X)
     (a__sel#(N, XS) -> mark# N, mark# fst X -> a__fst# mark X)
     (a__sel#(N, XS) -> mark# N, mark# fst X -> mark# X)
     (a__sel#(N, XS) -> mark# N, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (a__sel#(N, XS) -> mark# N, mark# and(X1, X2) -> mark# X1)
     (a__sel#(N, XS) -> mark# N, mark# snd X -> a__snd# mark X)
     (a__sel#(N, XS) -> mark# N, mark# snd X -> mark# X)
     (a__sel#(N, XS) -> mark# N, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (a__sel#(N, XS) -> mark# N, mark# afterNth(X1, X2) -> mark# X2)
     (a__sel#(N, XS) -> mark# N, mark# afterNth(X1, X2) -> mark# X1)
     (a__sel#(N, XS) -> mark# N, mark# splitAt(X1, X2) -> mark# X2)
     (a__sel#(N, XS) -> mark# N, mark# splitAt(X1, X2) -> mark# X1)
     (a__sel#(N, XS) -> mark# N, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (a__sel#(N, XS) -> mark# N, mark# U12(X1, X2) -> mark# X1)
     (a__sel#(N, XS) -> mark# N, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (a__sel#(N, XS) -> mark# N, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (a__sel#(N, XS) -> mark# N, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (a__sel#(N, XS) -> mark# N, mark# s X -> mark# X)
     (a__sel#(N, XS) -> mark# N, mark# natsFrom X -> a__natsFrom# mark X)
     (a__sel#(N, XS) -> mark# N, mark# natsFrom X -> mark# X)
     (a__sel#(N, XS) -> mark# N, mark# cons(X1, X2) -> mark# X1)
     (a__sel#(N, XS) -> mark# N, mark# pair(X1, X2) -> mark# X2)
     (a__sel#(N, XS) -> mark# N, mark# pair(X1, X2) -> mark# X1)
     (a__U11#(tt(), N, X, XS) -> a__U12#(a__splitAt(mark N, mark XS), X), a__U12#(pair(YS, ZS), X) -> mark# ZS)
     (a__U11#(tt(), N, X, XS) -> a__U12#(a__splitAt(mark N, mark XS), X), a__U12#(pair(YS, ZS), X) -> mark# X)
     (mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2), a__afterNth#(N, XS) -> a__snd# a__splitAt(mark N, mark XS))
     (mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2), a__afterNth#(N, XS) -> mark# XS)
     (mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2), a__afterNth#(N, XS) -> mark# N)
     (mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2), a__afterNth#(N, XS) -> a__splitAt#(mark N, mark XS))
     (mark# take(X1, X2) -> a__take#(mark X1, mark X2), a__take#(N, XS) -> a__fst# a__splitAt(mark N, mark XS))
     (mark# take(X1, X2) -> a__take#(mark X1, mark X2), a__take#(N, XS) -> mark# XS)
     (mark# take(X1, X2) -> a__take#(mark X1, mark X2), a__take#(N, XS) -> mark# N)
     (mark# take(X1, X2) -> a__take#(mark X1, mark X2), a__take#(N, XS) -> a__splitAt#(mark N, mark XS))
     (a__afterNth#(N, XS) -> a__splitAt#(mark N, mark XS), a__splitAt#(0(), XS) -> mark# XS)
     (a__afterNth#(N, XS) -> a__splitAt#(mark N, mark XS), a__splitAt#(s N, cons(X, XS)) -> a__U11#(tt(), N, X, XS))
     (a__take#(N, XS) -> a__splitAt#(mark N, mark XS), a__splitAt#(0(), XS) -> mark# XS)
     (a__take#(N, XS) -> a__splitAt#(mark N, mark XS), a__splitAt#(s N, cons(X, XS)) -> a__U11#(tt(), N, X, XS))
     (a__sel#(N, XS) -> a__head# a__afterNth(mark N, mark XS), a__head# cons(N, XS) -> mark# N)
     (mark# pair(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (mark# pair(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2)
     (mark# pair(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1)
     (mark# pair(X1, X2) -> mark# X1, mark# tail X -> a__tail# mark X)
     (mark# pair(X1, X2) -> mark# X1, mark# tail X -> mark# X)
     (mark# pair(X1, X2) -> mark# X1, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (mark# pair(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2)
     (mark# pair(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1)
     (mark# pair(X1, X2) -> mark# X1, mark# head X -> a__head# mark X)
     (mark# pair(X1, X2) -> mark# X1, mark# head X -> mark# X)
     (mark# pair(X1, X2) -> mark# X1, mark# fst X -> a__fst# mark X)
     (mark# pair(X1, X2) -> mark# X1, mark# fst X -> mark# X)
     (mark# pair(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# pair(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
     (mark# pair(X1, X2) -> mark# X1, mark# snd X -> a__snd# mark X)
     (mark# pair(X1, X2) -> mark# X1, mark# snd X -> mark# X)
     (mark# pair(X1, X2) -> mark# X1, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (mark# pair(X1, X2) -> mark# X1, mark# afterNth(X1, X2) -> mark# X2)
     (mark# pair(X1, X2) -> mark# X1, mark# afterNth(X1, X2) -> mark# X1)
     (mark# pair(X1, X2) -> mark# X1, mark# splitAt(X1, X2) -> mark# X2)
     (mark# pair(X1, X2) -> mark# X1, mark# splitAt(X1, X2) -> mark# X1)
     (mark# pair(X1, X2) -> mark# X1, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (mark# pair(X1, X2) -> mark# X1, mark# U12(X1, X2) -> mark# X1)
     (mark# pair(X1, X2) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (mark# pair(X1, X2) -> mark# X1, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (mark# pair(X1, X2) -> mark# X1, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (mark# pair(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# pair(X1, X2) -> mark# X1, mark# natsFrom X -> a__natsFrom# mark X)
     (mark# pair(X1, X2) -> mark# X1, mark# natsFrom X -> mark# X)
     (mark# pair(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (mark# pair(X1, X2) -> mark# X1, mark# pair(X1, X2) -> mark# X2)
     (mark# pair(X1, X2) -> mark# X1, mark# pair(X1, X2) -> mark# X1)
     (mark# U11(X1, X2, X3, X4) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (mark# U11(X1, X2, X3, X4) -> mark# X1, mark# take(X1, X2) -> mark# X2)
     (mark# U11(X1, X2, X3, X4) -> mark# X1, mark# take(X1, X2) -> mark# X1)
     (mark# U11(X1, X2, X3, X4) -> mark# X1, mark# tail X -> a__tail# mark X)
     (mark# U11(X1, X2, X3, X4) -> mark# X1, mark# tail X -> mark# X)
     (mark# U11(X1, X2, X3, X4) -> mark# X1, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (mark# U11(X1, X2, X3, X4) -> mark# X1, mark# sel(X1, X2) -> mark# X2)
     (mark# U11(X1, X2, X3, X4) -> mark# X1, mark# sel(X1, X2) -> mark# X1)
     (mark# U11(X1, X2, X3, X4) -> mark# X1, mark# head X -> a__head# mark X)
     (mark# U11(X1, X2, X3, X4) -> mark# X1, mark# head X -> mark# X)
     (mark# U11(X1, X2, X3, X4) -> mark# X1, mark# fst X -> a__fst# mark X)
     (mark# U11(X1, X2, X3, X4) -> mark# X1, mark# fst X -> mark# X)
     (mark# U11(X1, X2, X3, X4) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# U11(X1, X2, X3, X4) -> mark# X1, mark# and(X1, X2) -> mark# X1)
     (mark# U11(X1, X2, X3, X4) -> mark# X1, mark# snd X -> a__snd# mark X)
     (mark# U11(X1, X2, X3, X4) -> mark# X1, mark# snd X -> mark# X)
     (mark# U11(X1, X2, X3, X4) -> mark# X1, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (mark# U11(X1, X2, X3, X4) -> mark# X1, mark# afterNth(X1, X2) -> mark# X2)
     (mark# U11(X1, X2, X3, X4) -> mark# X1, mark# afterNth(X1, X2) -> mark# X1)
     (mark# U11(X1, X2, X3, X4) -> mark# X1, mark# splitAt(X1, X2) -> mark# X2)
     (mark# U11(X1, X2, X3, X4) -> mark# X1, mark# splitAt(X1, X2) -> mark# X1)
     (mark# U11(X1, X2, X3, X4) -> mark# X1, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (mark# U11(X1, X2, X3, X4) -> mark# X1, mark# U12(X1, X2) -> mark# X1)
     (mark# U11(X1, X2, X3, X4) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (mark# U11(X1, X2, X3, X4) -> mark# X1, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (mark# U11(X1, X2, X3, X4) -> mark# X1, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (mark# U11(X1, X2, X3, X4) -> mark# X1, mark# s X -> mark# X)
     (mark# U11(X1, X2, X3, X4) -> mark# X1, mark# natsFrom X -> a__natsFrom# mark X)
     (mark# U11(X1, X2, X3, X4) -> mark# X1, mark# natsFrom X -> mark# X)
     (mark# U11(X1, X2, X3, X4) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (mark# U11(X1, X2, X3, X4) -> mark# X1, mark# pair(X1, X2) -> mark# X2)
     (mark# U11(X1, X2, X3, X4) -> mark# X1, mark# pair(X1, X2) -> mark# X1)
     (mark# splitAt(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (mark# splitAt(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2)
     (mark# splitAt(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1)
     (mark# splitAt(X1, X2) -> mark# X1, mark# tail X -> a__tail# mark X)
     (mark# splitAt(X1, X2) -> mark# X1, mark# tail X -> mark# X)
     (mark# splitAt(X1, X2) -> mark# X1, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (mark# splitAt(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2)
     (mark# splitAt(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1)
     (mark# splitAt(X1, X2) -> mark# X1, mark# head X -> a__head# mark X)
     (mark# splitAt(X1, X2) -> mark# X1, mark# head X -> mark# X)
     (mark# splitAt(X1, X2) -> mark# X1, mark# fst X -> a__fst# mark X)
     (mark# splitAt(X1, X2) -> mark# X1, mark# fst X -> mark# X)
     (mark# splitAt(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# splitAt(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
     (mark# splitAt(X1, X2) -> mark# X1, mark# snd X -> a__snd# mark X)
     (mark# splitAt(X1, X2) -> mark# X1, mark# snd X -> mark# X)
     (mark# splitAt(X1, X2) -> mark# X1, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (mark# splitAt(X1, X2) -> mark# X1, mark# afterNth(X1, X2) -> mark# X2)
     (mark# splitAt(X1, X2) -> mark# X1, mark# afterNth(X1, X2) -> mark# X1)
     (mark# splitAt(X1, X2) -> mark# X1, mark# splitAt(X1, X2) -> mark# X2)
     (mark# splitAt(X1, X2) -> mark# X1, mark# splitAt(X1, X2) -> mark# X1)
     (mark# splitAt(X1, X2) -> mark# X1, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (mark# splitAt(X1, X2) -> mark# X1, mark# U12(X1, X2) -> mark# X1)
     (mark# splitAt(X1, X2) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (mark# splitAt(X1, X2) -> mark# X1, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (mark# splitAt(X1, X2) -> mark# X1, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (mark# splitAt(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# splitAt(X1, X2) -> mark# X1, mark# natsFrom X -> a__natsFrom# mark X)
     (mark# splitAt(X1, X2) -> mark# X1, mark# natsFrom X -> mark# X)
     (mark# splitAt(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (mark# splitAt(X1, X2) -> mark# X1, mark# pair(X1, X2) -> mark# X2)
     (mark# splitAt(X1, X2) -> mark# X1, mark# pair(X1, X2) -> mark# X1)
     (mark# and(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (mark# and(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2)
     (mark# and(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1)
     (mark# and(X1, X2) -> mark# X1, mark# tail X -> a__tail# mark X)
     (mark# and(X1, X2) -> mark# X1, mark# tail X -> mark# X)
     (mark# and(X1, X2) -> mark# X1, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (mark# and(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2)
     (mark# and(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1)
     (mark# and(X1, X2) -> mark# X1, mark# head X -> a__head# mark X)
     (mark# and(X1, X2) -> mark# X1, mark# head X -> mark# X)
     (mark# and(X1, X2) -> mark# X1, mark# fst X -> a__fst# mark X)
     (mark# and(X1, X2) -> mark# X1, mark# fst X -> mark# X)
     (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
     (mark# and(X1, X2) -> mark# X1, mark# snd X -> a__snd# mark X)
     (mark# and(X1, X2) -> mark# X1, mark# snd X -> mark# X)
     (mark# and(X1, X2) -> mark# X1, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (mark# and(X1, X2) -> mark# X1, mark# afterNth(X1, X2) -> mark# X2)
     (mark# and(X1, X2) -> mark# X1, mark# afterNth(X1, X2) -> mark# X1)
     (mark# and(X1, X2) -> mark# X1, mark# splitAt(X1, X2) -> mark# X2)
     (mark# and(X1, X2) -> mark# X1, mark# splitAt(X1, X2) -> mark# X1)
     (mark# and(X1, X2) -> mark# X1, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (mark# and(X1, X2) -> mark# X1, mark# U12(X1, X2) -> mark# X1)
     (mark# and(X1, X2) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (mark# and(X1, X2) -> mark# X1, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (mark# and(X1, X2) -> mark# X1, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (mark# and(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# and(X1, X2) -> mark# X1, mark# natsFrom X -> a__natsFrom# mark X)
     (mark# and(X1, X2) -> mark# X1, mark# natsFrom X -> mark# X)
     (mark# and(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (mark# and(X1, X2) -> mark# X1, mark# pair(X1, X2) -> mark# X2)
     (mark# and(X1, X2) -> mark# X1, mark# pair(X1, X2) -> mark# X1)
     (mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2)
     (mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1)
     (mark# take(X1, X2) -> mark# X1, mark# tail X -> a__tail# mark X)
     (mark# take(X1, X2) -> mark# X1, mark# tail X -> mark# X)
     (mark# take(X1, X2) -> mark# X1, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (mark# take(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2)
     (mark# take(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1)
     (mark# take(X1, X2) -> mark# X1, mark# head X -> a__head# mark X)
     (mark# take(X1, X2) -> mark# X1, mark# head X -> mark# X)
     (mark# take(X1, X2) -> mark# X1, mark# fst X -> a__fst# mark X)
     (mark# take(X1, X2) -> mark# X1, mark# fst X -> mark# X)
     (mark# take(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# take(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
     (mark# take(X1, X2) -> mark# X1, mark# snd X -> a__snd# mark X)
     (mark# take(X1, X2) -> mark# X1, mark# snd X -> mark# X)
     (mark# take(X1, X2) -> mark# X1, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (mark# take(X1, X2) -> mark# X1, mark# afterNth(X1, X2) -> mark# X2)
     (mark# take(X1, X2) -> mark# X1, mark# afterNth(X1, X2) -> mark# X1)
     (mark# take(X1, X2) -> mark# X1, mark# splitAt(X1, X2) -> mark# X2)
     (mark# take(X1, X2) -> mark# X1, mark# splitAt(X1, X2) -> mark# X1)
     (mark# take(X1, X2) -> mark# X1, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (mark# take(X1, X2) -> mark# X1, mark# U12(X1, X2) -> mark# X1)
     (mark# take(X1, X2) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (mark# take(X1, X2) -> mark# X1, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (mark# take(X1, X2) -> mark# X1, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (mark# take(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# take(X1, X2) -> mark# X1, mark# natsFrom X -> a__natsFrom# mark X)
     (mark# take(X1, X2) -> mark# X1, mark# natsFrom X -> mark# X)
     (mark# take(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (mark# take(X1, X2) -> mark# X1, mark# pair(X1, X2) -> mark# X2)
     (mark# take(X1, X2) -> mark# X1, mark# pair(X1, X2) -> mark# X1)
     (a__U11#(tt(), N, X, XS) -> mark# XS, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (a__U11#(tt(), N, X, XS) -> mark# XS, mark# take(X1, X2) -> mark# X2)
     (a__U11#(tt(), N, X, XS) -> mark# XS, mark# take(X1, X2) -> mark# X1)
     (a__U11#(tt(), N, X, XS) -> mark# XS, mark# tail X -> a__tail# mark X)
     (a__U11#(tt(), N, X, XS) -> mark# XS, mark# tail X -> mark# X)
     (a__U11#(tt(), N, X, XS) -> mark# XS, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (a__U11#(tt(), N, X, XS) -> mark# XS, mark# sel(X1, X2) -> mark# X2)
     (a__U11#(tt(), N, X, XS) -> mark# XS, mark# sel(X1, X2) -> mark# X1)
     (a__U11#(tt(), N, X, XS) -> mark# XS, mark# head X -> a__head# mark X)
     (a__U11#(tt(), N, X, XS) -> mark# XS, mark# head X -> mark# X)
     (a__U11#(tt(), N, X, XS) -> mark# XS, mark# fst X -> a__fst# mark X)
     (a__U11#(tt(), N, X, XS) -> mark# XS, mark# fst X -> mark# X)
     (a__U11#(tt(), N, X, XS) -> mark# XS, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (a__U11#(tt(), N, X, XS) -> mark# XS, mark# and(X1, X2) -> mark# X1)
     (a__U11#(tt(), N, X, XS) -> mark# XS, mark# snd X -> a__snd# mark X)
     (a__U11#(tt(), N, X, XS) -> mark# XS, mark# snd X -> mark# X)
     (a__U11#(tt(), N, X, XS) -> mark# XS, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (a__U11#(tt(), N, X, XS) -> mark# XS, mark# afterNth(X1, X2) -> mark# X2)
     (a__U11#(tt(), N, X, XS) -> mark# XS, mark# afterNth(X1, X2) -> mark# X1)
     (a__U11#(tt(), N, X, XS) -> mark# XS, mark# splitAt(X1, X2) -> mark# X2)
     (a__U11#(tt(), N, X, XS) -> mark# XS, mark# splitAt(X1, X2) -> mark# X1)
     (a__U11#(tt(), N, X, XS) -> mark# XS, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (a__U11#(tt(), N, X, XS) -> mark# XS, mark# U12(X1, X2) -> mark# X1)
     (a__U11#(tt(), N, X, XS) -> mark# XS, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (a__U11#(tt(), N, X, XS) -> mark# XS, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (a__U11#(tt(), N, X, XS) -> mark# XS, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (a__U11#(tt(), N, X, XS) -> mark# XS, mark# s X -> mark# X)
     (a__U11#(tt(), N, X, XS) -> mark# XS, mark# natsFrom X -> a__natsFrom# mark X)
     (a__U11#(tt(), N, X, XS) -> mark# XS, mark# natsFrom X -> mark# X)
     (a__U11#(tt(), N, X, XS) -> mark# XS, mark# cons(X1, X2) -> mark# X1)
     (a__U11#(tt(), N, X, XS) -> mark# XS, mark# pair(X1, X2) -> mark# X2)
     (a__U11#(tt(), N, X, XS) -> mark# XS, mark# pair(X1, X2) -> mark# X1)
     (a__sel#(N, XS) -> mark# XS, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (a__sel#(N, XS) -> mark# XS, mark# take(X1, X2) -> mark# X2)
     (a__sel#(N, XS) -> mark# XS, mark# take(X1, X2) -> mark# X1)
     (a__sel#(N, XS) -> mark# XS, mark# tail X -> a__tail# mark X)
     (a__sel#(N, XS) -> mark# XS, mark# tail X -> mark# X)
     (a__sel#(N, XS) -> mark# XS, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (a__sel#(N, XS) -> mark# XS, mark# sel(X1, X2) -> mark# X2)
     (a__sel#(N, XS) -> mark# XS, mark# sel(X1, X2) -> mark# X1)
     (a__sel#(N, XS) -> mark# XS, mark# head X -> a__head# mark X)
     (a__sel#(N, XS) -> mark# XS, mark# head X -> mark# X)
     (a__sel#(N, XS) -> mark# XS, mark# fst X -> a__fst# mark X)
     (a__sel#(N, XS) -> mark# XS, mark# fst X -> mark# X)
     (a__sel#(N, XS) -> mark# XS, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (a__sel#(N, XS) -> mark# XS, mark# and(X1, X2) -> mark# X1)
     (a__sel#(N, XS) -> mark# XS, mark# snd X -> a__snd# mark X)
     (a__sel#(N, XS) -> mark# XS, mark# snd X -> mark# X)
     (a__sel#(N, XS) -> mark# XS, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (a__sel#(N, XS) -> mark# XS, mark# afterNth(X1, X2) -> mark# X2)
     (a__sel#(N, XS) -> mark# XS, mark# afterNth(X1, X2) -> mark# X1)
     (a__sel#(N, XS) -> mark# XS, mark# splitAt(X1, X2) -> mark# X2)
     (a__sel#(N, XS) -> mark# XS, mark# splitAt(X1, X2) -> mark# X1)
     (a__sel#(N, XS) -> mark# XS, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (a__sel#(N, XS) -> mark# XS, mark# U12(X1, X2) -> mark# X1)
     (a__sel#(N, XS) -> mark# XS, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (a__sel#(N, XS) -> mark# XS, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (a__sel#(N, XS) -> mark# XS, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (a__sel#(N, XS) -> mark# XS, mark# s X -> mark# X)
     (a__sel#(N, XS) -> mark# XS, mark# natsFrom X -> a__natsFrom# mark X)
     (a__sel#(N, XS) -> mark# XS, mark# natsFrom X -> mark# X)
     (a__sel#(N, XS) -> mark# XS, mark# cons(X1, X2) -> mark# X1)
     (a__sel#(N, XS) -> mark# XS, mark# pair(X1, X2) -> mark# X2)
     (a__sel#(N, XS) -> mark# XS, mark# pair(X1, X2) -> mark# X1)
     (a__take#(N, XS) -> mark# XS, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (a__take#(N, XS) -> mark# XS, mark# take(X1, X2) -> mark# X2)
     (a__take#(N, XS) -> mark# XS, mark# take(X1, X2) -> mark# X1)
     (a__take#(N, XS) -> mark# XS, mark# tail X -> a__tail# mark X)
     (a__take#(N, XS) -> mark# XS, mark# tail X -> mark# X)
     (a__take#(N, XS) -> mark# XS, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (a__take#(N, XS) -> mark# XS, mark# sel(X1, X2) -> mark# X2)
     (a__take#(N, XS) -> mark# XS, mark# sel(X1, X2) -> mark# X1)
     (a__take#(N, XS) -> mark# XS, mark# head X -> a__head# mark X)
     (a__take#(N, XS) -> mark# XS, mark# head X -> mark# X)
     (a__take#(N, XS) -> mark# XS, mark# fst X -> a__fst# mark X)
     (a__take#(N, XS) -> mark# XS, mark# fst X -> mark# X)
     (a__take#(N, XS) -> mark# XS, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (a__take#(N, XS) -> mark# XS, mark# and(X1, X2) -> mark# X1)
     (a__take#(N, XS) -> mark# XS, mark# snd X -> a__snd# mark X)
     (a__take#(N, XS) -> mark# XS, mark# snd X -> mark# X)
     (a__take#(N, XS) -> mark# XS, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (a__take#(N, XS) -> mark# XS, mark# afterNth(X1, X2) -> mark# X2)
     (a__take#(N, XS) -> mark# XS, mark# afterNth(X1, X2) -> mark# X1)
     (a__take#(N, XS) -> mark# XS, mark# splitAt(X1, X2) -> mark# X2)
     (a__take#(N, XS) -> mark# XS, mark# splitAt(X1, X2) -> mark# X1)
     (a__take#(N, XS) -> mark# XS, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (a__take#(N, XS) -> mark# XS, mark# U12(X1, X2) -> mark# X1)
     (a__take#(N, XS) -> mark# XS, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (a__take#(N, XS) -> mark# XS, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (a__take#(N, XS) -> mark# XS, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (a__take#(N, XS) -> mark# XS, mark# s X -> mark# X)
     (a__take#(N, XS) -> mark# XS, mark# natsFrom X -> a__natsFrom# mark X)
     (a__take#(N, XS) -> mark# XS, mark# natsFrom X -> mark# X)
     (a__take#(N, XS) -> mark# XS, mark# cons(X1, X2) -> mark# X1)
     (a__take#(N, XS) -> mark# XS, mark# pair(X1, X2) -> mark# X2)
     (a__take#(N, XS) -> mark# XS, mark# pair(X1, X2) -> mark# X1)
     (mark# U12(X1, X2) -> a__U12#(mark X1, X2), a__U12#(pair(YS, ZS), X) -> mark# ZS)
     (mark# U12(X1, X2) -> a__U12#(mark X1, X2), a__U12#(pair(YS, ZS), X) -> mark# X)
     (a__splitAt#(s N, cons(X, XS)) -> a__U11#(tt(), N, X, XS), a__U11#(tt(), N, X, XS) -> mark# XS)
     (a__splitAt#(s N, cons(X, XS)) -> a__U11#(tt(), N, X, XS), a__U11#(tt(), N, X, XS) -> mark# N)
     (a__splitAt#(s N, cons(X, XS)) -> a__U11#(tt(), N, X, XS), a__U11#(tt(), N, X, XS) -> a__splitAt#(mark N, mark XS))
     (a__splitAt#(s N, cons(X, XS)) -> a__U11#(tt(), N, X, XS), a__U11#(tt(), N, X, XS) -> a__U12#(a__splitAt(mark N, mark XS), X))
     (mark# natsFrom X -> a__natsFrom# mark X, a__natsFrom# N -> mark# N)
     (mark# fst X -> a__fst# mark X, a__fst# pair(X, Y) -> mark# X)
     (mark# tail X -> a__tail# mark X, a__tail# cons(N, XS) -> mark# XS)
     (mark# splitAt(X1, X2) -> mark# X2, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (mark# splitAt(X1, X2) -> mark# X2, mark# take(X1, X2) -> mark# X2)
     (mark# splitAt(X1, X2) -> mark# X2, mark# take(X1, X2) -> mark# X1)
     (mark# splitAt(X1, X2) -> mark# X2, mark# tail X -> a__tail# mark X)
     (mark# splitAt(X1, X2) -> mark# X2, mark# tail X -> mark# X)
     (mark# splitAt(X1, X2) -> mark# X2, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (mark# splitAt(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X2)
     (mark# splitAt(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X1)
     (mark# splitAt(X1, X2) -> mark# X2, mark# head X -> a__head# mark X)
     (mark# splitAt(X1, X2) -> mark# X2, mark# head X -> mark# X)
     (mark# splitAt(X1, X2) -> mark# X2, mark# fst X -> a__fst# mark X)
     (mark# splitAt(X1, X2) -> mark# X2, mark# fst X -> mark# X)
     (mark# splitAt(X1, X2) -> mark# X2, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# splitAt(X1, X2) -> mark# X2, mark# and(X1, X2) -> mark# X1)
     (mark# splitAt(X1, X2) -> mark# X2, mark# snd X -> a__snd# mark X)
     (mark# splitAt(X1, X2) -> mark# X2, mark# snd X -> mark# X)
     (mark# splitAt(X1, X2) -> mark# X2, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (mark# splitAt(X1, X2) -> mark# X2, mark# afterNth(X1, X2) -> mark# X2)
     (mark# splitAt(X1, X2) -> mark# X2, mark# afterNth(X1, X2) -> mark# X1)
     (mark# splitAt(X1, X2) -> mark# X2, mark# splitAt(X1, X2) -> mark# X2)
     (mark# splitAt(X1, X2) -> mark# X2, mark# splitAt(X1, X2) -> mark# X1)
     (mark# splitAt(X1, X2) -> mark# X2, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (mark# splitAt(X1, X2) -> mark# X2, mark# U12(X1, X2) -> mark# X1)
     (mark# splitAt(X1, X2) -> mark# X2, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (mark# splitAt(X1, X2) -> mark# X2, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (mark# splitAt(X1, X2) -> mark# X2, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (mark# splitAt(X1, X2) -> mark# X2, mark# s X -> mark# X)
     (mark# splitAt(X1, X2) -> mark# X2, mark# natsFrom X -> a__natsFrom# mark X)
     (mark# splitAt(X1, X2) -> mark# X2, mark# natsFrom X -> mark# X)
     (mark# splitAt(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
     (mark# splitAt(X1, X2) -> mark# X2, mark# pair(X1, X2) -> mark# X2)
     (mark# splitAt(X1, X2) -> mark# X2, mark# pair(X1, X2) -> mark# X1)
     (mark# sel(X1, X2) -> mark# X2, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (mark# sel(X1, X2) -> mark# X2, mark# take(X1, X2) -> mark# X2)
     (mark# sel(X1, X2) -> mark# X2, mark# take(X1, X2) -> mark# X1)
     (mark# sel(X1, X2) -> mark# X2, mark# tail X -> a__tail# mark X)
     (mark# sel(X1, X2) -> mark# X2, mark# tail X -> mark# X)
     (mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X2)
     (mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X1)
     (mark# sel(X1, X2) -> mark# X2, mark# head X -> a__head# mark X)
     (mark# sel(X1, X2) -> mark# X2, mark# head X -> mark# X)
     (mark# sel(X1, X2) -> mark# X2, mark# fst X -> a__fst# mark X)
     (mark# sel(X1, X2) -> mark# X2, mark# fst X -> mark# X)
     (mark# sel(X1, X2) -> mark# X2, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# sel(X1, X2) -> mark# X2, mark# and(X1, X2) -> mark# X1)
     (mark# sel(X1, X2) -> mark# X2, mark# snd X -> a__snd# mark X)
     (mark# sel(X1, X2) -> mark# X2, mark# snd X -> mark# X)
     (mark# sel(X1, X2) -> mark# X2, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (mark# sel(X1, X2) -> mark# X2, mark# afterNth(X1, X2) -> mark# X2)
     (mark# sel(X1, X2) -> mark# X2, mark# afterNth(X1, X2) -> mark# X1)
     (mark# sel(X1, X2) -> mark# X2, mark# splitAt(X1, X2) -> mark# X2)
     (mark# sel(X1, X2) -> mark# X2, mark# splitAt(X1, X2) -> mark# X1)
     (mark# sel(X1, X2) -> mark# X2, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (mark# sel(X1, X2) -> mark# X2, mark# U12(X1, X2) -> mark# X1)
     (mark# sel(X1, X2) -> mark# X2, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (mark# sel(X1, X2) -> mark# X2, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (mark# sel(X1, X2) -> mark# X2, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (mark# sel(X1, X2) -> mark# X2, mark# s X -> mark# X)
     (mark# sel(X1, X2) -> mark# X2, mark# natsFrom X -> a__natsFrom# mark X)
     (mark# sel(X1, X2) -> mark# X2, mark# natsFrom X -> mark# X)
     (mark# sel(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
     (mark# sel(X1, X2) -> mark# X2, mark# pair(X1, X2) -> mark# X2)
     (mark# sel(X1, X2) -> mark# X2, mark# pair(X1, X2) -> mark# X1)
     (a__U12#(pair(YS, ZS), X) -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (a__U12#(pair(YS, ZS), X) -> mark# X, mark# take(X1, X2) -> mark# X2)
     (a__U12#(pair(YS, ZS), X) -> mark# X, mark# take(X1, X2) -> mark# X1)
     (a__U12#(pair(YS, ZS), X) -> mark# X, mark# tail X -> a__tail# mark X)
     (a__U12#(pair(YS, ZS), X) -> mark# X, mark# tail X -> mark# X)
     (a__U12#(pair(YS, ZS), X) -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (a__U12#(pair(YS, ZS), X) -> mark# X, mark# sel(X1, X2) -> mark# X2)
     (a__U12#(pair(YS, ZS), X) -> mark# X, mark# sel(X1, X2) -> mark# X1)
     (a__U12#(pair(YS, ZS), X) -> mark# X, mark# head X -> a__head# mark X)
     (a__U12#(pair(YS, ZS), X) -> mark# X, mark# head X -> mark# X)
     (a__U12#(pair(YS, ZS), X) -> mark# X, mark# fst X -> a__fst# mark X)
     (a__U12#(pair(YS, ZS), X) -> mark# X, mark# fst X -> mark# X)
     (a__U12#(pair(YS, ZS), X) -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (a__U12#(pair(YS, ZS), X) -> mark# X, mark# and(X1, X2) -> mark# X1)
     (a__U12#(pair(YS, ZS), X) -> mark# X, mark# snd X -> a__snd# mark X)
     (a__U12#(pair(YS, ZS), X) -> mark# X, mark# snd X -> mark# X)
     (a__U12#(pair(YS, ZS), X) -> mark# X, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (a__U12#(pair(YS, ZS), X) -> mark# X, mark# afterNth(X1, X2) -> mark# X2)
     (a__U12#(pair(YS, ZS), X) -> mark# X, mark# afterNth(X1, X2) -> mark# X1)
     (a__U12#(pair(YS, ZS), X) -> mark# X, mark# splitAt(X1, X2) -> mark# X2)
     (a__U12#(pair(YS, ZS), X) -> mark# X, mark# splitAt(X1, X2) -> mark# X1)
     (a__U12#(pair(YS, ZS), X) -> mark# X, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (a__U12#(pair(YS, ZS), X) -> mark# X, mark# U12(X1, X2) -> mark# X1)
     (a__U12#(pair(YS, ZS), X) -> mark# X, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (a__U12#(pair(YS, ZS), X) -> mark# X, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (a__U12#(pair(YS, ZS), X) -> mark# X, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (a__U12#(pair(YS, ZS), X) -> mark# X, mark# s X -> mark# X)
     (a__U12#(pair(YS, ZS), X) -> mark# X, mark# natsFrom X -> a__natsFrom# mark X)
     (a__U12#(pair(YS, ZS), X) -> mark# X, mark# natsFrom X -> mark# X)
     (a__U12#(pair(YS, ZS), X) -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (a__U12#(pair(YS, ZS), X) -> mark# X, mark# pair(X1, X2) -> mark# X2)
     (a__U12#(pair(YS, ZS), X) -> mark# X, mark# pair(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (mark# s X -> mark# X, mark# take(X1, X2) -> mark# X2)
     (mark# s X -> mark# X, mark# take(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# tail X -> a__tail# mark X)
     (mark# s X -> mark# X, mark# tail X -> mark# X)
     (mark# s X -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (mark# s X -> mark# X, mark# sel(X1, X2) -> mark# X2)
     (mark# s X -> mark# X, mark# sel(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# head X -> a__head# mark X)
     (mark# s X -> mark# X, mark# head X -> mark# X)
     (mark# s X -> mark# X, mark# fst X -> a__fst# mark X)
     (mark# s X -> mark# X, mark# fst X -> mark# X)
     (mark# s X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# s X -> mark# X, mark# and(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# snd X -> a__snd# mark X)
     (mark# s X -> mark# X, mark# snd X -> mark# X)
     (mark# s X -> mark# X, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (mark# s X -> mark# X, mark# afterNth(X1, X2) -> mark# X2)
     (mark# s X -> mark# X, mark# afterNth(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# splitAt(X1, X2) -> mark# X2)
     (mark# s X -> mark# X, mark# splitAt(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (mark# s X -> mark# X, mark# U12(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (mark# s X -> mark# X, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (mark# s X -> mark# X, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (mark# s X -> mark# X, mark# s X -> mark# X)
     (mark# s X -> mark# X, mark# natsFrom X -> a__natsFrom# mark X)
     (mark# s X -> mark# X, mark# natsFrom X -> mark# X)
     (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# s X -> mark# X, mark# pair(X1, X2) -> mark# X2)
     (mark# s X -> mark# X, mark# pair(X1, X2) -> mark# X1)
     (mark# fst X -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (mark# fst X -> mark# X, mark# take(X1, X2) -> mark# X2)
     (mark# fst X -> mark# X, mark# take(X1, X2) -> mark# X1)
     (mark# fst X -> mark# X, mark# tail X -> a__tail# mark X)
     (mark# fst X -> mark# X, mark# tail X -> mark# X)
     (mark# fst X -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (mark# fst X -> mark# X, mark# sel(X1, X2) -> mark# X2)
     (mark# fst X -> mark# X, mark# sel(X1, X2) -> mark# X1)
     (mark# fst X -> mark# X, mark# head X -> a__head# mark X)
     (mark# fst X -> mark# X, mark# head X -> mark# X)
     (mark# fst X -> mark# X, mark# fst X -> a__fst# mark X)
     (mark# fst X -> mark# X, mark# fst X -> mark# X)
     (mark# fst X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# fst X -> mark# X, mark# and(X1, X2) -> mark# X1)
     (mark# fst X -> mark# X, mark# snd X -> a__snd# mark X)
     (mark# fst X -> mark# X, mark# snd X -> mark# X)
     (mark# fst X -> mark# X, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (mark# fst X -> mark# X, mark# afterNth(X1, X2) -> mark# X2)
     (mark# fst X -> mark# X, mark# afterNth(X1, X2) -> mark# X1)
     (mark# fst X -> mark# X, mark# splitAt(X1, X2) -> mark# X2)
     (mark# fst X -> mark# X, mark# splitAt(X1, X2) -> mark# X1)
     (mark# fst X -> mark# X, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (mark# fst X -> mark# X, mark# U12(X1, X2) -> mark# X1)
     (mark# fst X -> mark# X, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (mark# fst X -> mark# X, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (mark# fst X -> mark# X, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (mark# fst X -> mark# X, mark# s X -> mark# X)
     (mark# fst X -> mark# X, mark# natsFrom X -> a__natsFrom# mark X)
     (mark# fst X -> mark# X, mark# natsFrom X -> mark# X)
     (mark# fst X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# fst X -> mark# X, mark# pair(X1, X2) -> mark# X2)
     (mark# fst X -> mark# X, mark# pair(X1, X2) -> mark# X1)
     (mark# tail X -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (mark# tail X -> mark# X, mark# take(X1, X2) -> mark# X2)
     (mark# tail X -> mark# X, mark# take(X1, X2) -> mark# X1)
     (mark# tail X -> mark# X, mark# tail X -> a__tail# mark X)
     (mark# tail X -> mark# X, mark# tail X -> mark# X)
     (mark# tail X -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (mark# tail X -> mark# X, mark# sel(X1, X2) -> mark# X2)
     (mark# tail X -> mark# X, mark# sel(X1, X2) -> mark# X1)
     (mark# tail X -> mark# X, mark# head X -> a__head# mark X)
     (mark# tail X -> mark# X, mark# head X -> mark# X)
     (mark# tail X -> mark# X, mark# fst X -> a__fst# mark X)
     (mark# tail X -> mark# X, mark# fst X -> mark# X)
     (mark# tail X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# tail X -> mark# X, mark# and(X1, X2) -> mark# X1)
     (mark# tail X -> mark# X, mark# snd X -> a__snd# mark X)
     (mark# tail X -> mark# X, mark# snd X -> mark# X)
     (mark# tail X -> mark# X, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (mark# tail X -> mark# X, mark# afterNth(X1, X2) -> mark# X2)
     (mark# tail X -> mark# X, mark# afterNth(X1, X2) -> mark# X1)
     (mark# tail X -> mark# X, mark# splitAt(X1, X2) -> mark# X2)
     (mark# tail X -> mark# X, mark# splitAt(X1, X2) -> mark# X1)
     (mark# tail X -> mark# X, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (mark# tail X -> mark# X, mark# U12(X1, X2) -> mark# X1)
     (mark# tail X -> mark# X, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (mark# tail X -> mark# X, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (mark# tail X -> mark# X, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (mark# tail X -> mark# X, mark# s X -> mark# X)
     (mark# tail X -> mark# X, mark# natsFrom X -> a__natsFrom# mark X)
     (mark# tail X -> mark# X, mark# natsFrom X -> mark# X)
     (mark# tail X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# tail X -> mark# X, mark# pair(X1, X2) -> mark# X2)
     (mark# tail X -> mark# X, mark# pair(X1, X2) -> mark# X1)
     (a__fst# pair(X, Y) -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (a__fst# pair(X, Y) -> mark# X, mark# take(X1, X2) -> mark# X2)
     (a__fst# pair(X, Y) -> mark# X, mark# take(X1, X2) -> mark# X1)
     (a__fst# pair(X, Y) -> mark# X, mark# tail X -> a__tail# mark X)
     (a__fst# pair(X, Y) -> mark# X, mark# tail X -> mark# X)
     (a__fst# pair(X, Y) -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (a__fst# pair(X, Y) -> mark# X, mark# sel(X1, X2) -> mark# X2)
     (a__fst# pair(X, Y) -> mark# X, mark# sel(X1, X2) -> mark# X1)
     (a__fst# pair(X, Y) -> mark# X, mark# head X -> a__head# mark X)
     (a__fst# pair(X, Y) -> mark# X, mark# head X -> mark# X)
     (a__fst# pair(X, Y) -> mark# X, mark# fst X -> a__fst# mark X)
     (a__fst# pair(X, Y) -> mark# X, mark# fst X -> mark# X)
     (a__fst# pair(X, Y) -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (a__fst# pair(X, Y) -> mark# X, mark# and(X1, X2) -> mark# X1)
     (a__fst# pair(X, Y) -> mark# X, mark# snd X -> a__snd# mark X)
     (a__fst# pair(X, Y) -> mark# X, mark# snd X -> mark# X)
     (a__fst# pair(X, Y) -> mark# X, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (a__fst# pair(X, Y) -> mark# X, mark# afterNth(X1, X2) -> mark# X2)
     (a__fst# pair(X, Y) -> mark# X, mark# afterNth(X1, X2) -> mark# X1)
     (a__fst# pair(X, Y) -> mark# X, mark# splitAt(X1, X2) -> mark# X2)
     (a__fst# pair(X, Y) -> mark# X, mark# splitAt(X1, X2) -> mark# X1)
     (a__fst# pair(X, Y) -> mark# X, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (a__fst# pair(X, Y) -> mark# X, mark# U12(X1, X2) -> mark# X1)
     (a__fst# pair(X, Y) -> mark# X, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (a__fst# pair(X, Y) -> mark# X, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (a__fst# pair(X, Y) -> mark# X, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (a__fst# pair(X, Y) -> mark# X, mark# s X -> mark# X)
     (a__fst# pair(X, Y) -> mark# X, mark# natsFrom X -> a__natsFrom# mark X)
     (a__fst# pair(X, Y) -> mark# X, mark# natsFrom X -> mark# X)
     (a__fst# pair(X, Y) -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (a__fst# pair(X, Y) -> mark# X, mark# pair(X1, X2) -> mark# X2)
     (a__fst# pair(X, Y) -> mark# X, mark# pair(X1, X2) -> mark# X1)
     (a__and#(tt(), X) -> mark# X, mark# pair(X1, X2) -> mark# X1)
     (a__and#(tt(), X) -> mark# X, mark# pair(X1, X2) -> mark# X2)
     (a__and#(tt(), X) -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (a__and#(tt(), X) -> mark# X, mark# natsFrom X -> mark# X)
     (a__and#(tt(), X) -> mark# X, mark# natsFrom X -> a__natsFrom# mark X)
     (a__and#(tt(), X) -> mark# X, mark# s X -> mark# X)
     (a__and#(tt(), X) -> mark# X, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (a__and#(tt(), X) -> mark# X, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (a__and#(tt(), X) -> mark# X, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (a__and#(tt(), X) -> mark# X, mark# U12(X1, X2) -> mark# X1)
     (a__and#(tt(), X) -> mark# X, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (a__and#(tt(), X) -> mark# X, mark# splitAt(X1, X2) -> mark# X1)
     (a__and#(tt(), X) -> mark# X, mark# splitAt(X1, X2) -> mark# X2)
     (a__and#(tt(), X) -> mark# X, mark# afterNth(X1, X2) -> mark# X1)
     (a__and#(tt(), X) -> mark# X, mark# afterNth(X1, X2) -> mark# X2)
     (a__and#(tt(), X) -> mark# X, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (a__and#(tt(), X) -> mark# X, mark# snd X -> mark# X)
     (a__and#(tt(), X) -> mark# X, mark# snd X -> a__snd# mark X)
     (a__and#(tt(), X) -> mark# X, mark# and(X1, X2) -> mark# X1)
     (a__and#(tt(), X) -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (a__and#(tt(), X) -> mark# X, mark# fst X -> mark# X)
     (a__and#(tt(), X) -> mark# X, mark# fst X -> a__fst# mark X)
     (a__and#(tt(), X) -> mark# X, mark# head X -> mark# X)
     (a__and#(tt(), X) -> mark# X, mark# head X -> a__head# mark X)
     (a__and#(tt(), X) -> mark# X, mark# sel(X1, X2) -> mark# X1)
     (a__and#(tt(), X) -> mark# X, mark# sel(X1, X2) -> mark# X2)
     (a__and#(tt(), X) -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (a__and#(tt(), X) -> mark# X, mark# tail X -> mark# X)
     (a__and#(tt(), X) -> mark# X, mark# tail X -> a__tail# mark X)
     (a__and#(tt(), X) -> mark# X, mark# take(X1, X2) -> mark# X1)
     (a__and#(tt(), X) -> mark# X, mark# take(X1, X2) -> mark# X2)
     (a__and#(tt(), X) -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (mark# head X -> mark# X, mark# pair(X1, X2) -> mark# X1)
     (mark# head X -> mark# X, mark# pair(X1, X2) -> mark# X2)
     (mark# head X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# head X -> mark# X, mark# natsFrom X -> mark# X)
     (mark# head X -> mark# X, mark# natsFrom X -> a__natsFrom# mark X)
     (mark# head X -> mark# X, mark# s X -> mark# X)
     (mark# head X -> mark# X, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (mark# head X -> mark# X, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (mark# head X -> mark# X, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (mark# head X -> mark# X, mark# U12(X1, X2) -> mark# X1)
     (mark# head X -> mark# X, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (mark# head X -> mark# X, mark# splitAt(X1, X2) -> mark# X1)
     (mark# head X -> mark# X, mark# splitAt(X1, X2) -> mark# X2)
     (mark# head X -> mark# X, mark# afterNth(X1, X2) -> mark# X1)
     (mark# head X -> mark# X, mark# afterNth(X1, X2) -> mark# X2)
     (mark# head X -> mark# X, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (mark# head X -> mark# X, mark# snd X -> mark# X)
     (mark# head X -> mark# X, mark# snd X -> a__snd# mark X)
     (mark# head X -> mark# X, mark# and(X1, X2) -> mark# X1)
     (mark# head X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# head X -> mark# X, mark# fst X -> mark# X)
     (mark# head X -> mark# X, mark# fst X -> a__fst# mark X)
     (mark# head X -> mark# X, mark# head X -> mark# X)
     (mark# head X -> mark# X, mark# head X -> a__head# mark X)
     (mark# head X -> mark# X, mark# sel(X1, X2) -> mark# X1)
     (mark# head X -> mark# X, mark# sel(X1, X2) -> mark# X2)
     (mark# head X -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (mark# head X -> mark# X, mark# tail X -> mark# X)
     (mark# head X -> mark# X, mark# tail X -> a__tail# mark X)
     (mark# head X -> mark# X, mark# take(X1, X2) -> mark# X1)
     (mark# head X -> mark# X, mark# take(X1, X2) -> mark# X2)
     (mark# head X -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (mark# snd X -> mark# X, mark# pair(X1, X2) -> mark# X1)
     (mark# snd X -> mark# X, mark# pair(X1, X2) -> mark# X2)
     (mark# snd X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# snd X -> mark# X, mark# natsFrom X -> mark# X)
     (mark# snd X -> mark# X, mark# natsFrom X -> a__natsFrom# mark X)
     (mark# snd X -> mark# X, mark# s X -> mark# X)
     (mark# snd X -> mark# X, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (mark# snd X -> mark# X, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (mark# snd X -> mark# X, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (mark# snd X -> mark# X, mark# U12(X1, X2) -> mark# X1)
     (mark# snd X -> mark# X, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (mark# snd X -> mark# X, mark# splitAt(X1, X2) -> mark# X1)
     (mark# snd X -> mark# X, mark# splitAt(X1, X2) -> mark# X2)
     (mark# snd X -> mark# X, mark# afterNth(X1, X2) -> mark# X1)
     (mark# snd X -> mark# X, mark# afterNth(X1, X2) -> mark# X2)
     (mark# snd X -> mark# X, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (mark# snd X -> mark# X, mark# snd X -> mark# X)
     (mark# snd X -> mark# X, mark# snd X -> a__snd# mark X)
     (mark# snd X -> mark# X, mark# and(X1, X2) -> mark# X1)
     (mark# snd X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# snd X -> mark# X, mark# fst X -> mark# X)
     (mark# snd X -> mark# X, mark# fst X -> a__fst# mark X)
     (mark# snd X -> mark# X, mark# head X -> mark# X)
     (mark# snd X -> mark# X, mark# head X -> a__head# mark X)
     (mark# snd X -> mark# X, mark# sel(X1, X2) -> mark# X1)
     (mark# snd X -> mark# X, mark# sel(X1, X2) -> mark# X2)
     (mark# snd X -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (mark# snd X -> mark# X, mark# tail X -> mark# X)
     (mark# snd X -> mark# X, mark# tail X -> a__tail# mark X)
     (mark# snd X -> mark# X, mark# take(X1, X2) -> mark# X1)
     (mark# snd X -> mark# X, mark# take(X1, X2) -> mark# X2)
     (mark# snd X -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (mark# natsFrom X -> mark# X, mark# pair(X1, X2) -> mark# X1)
     (mark# natsFrom X -> mark# X, mark# pair(X1, X2) -> mark# X2)
     (mark# natsFrom X -> mark# X, mark# cons(X1, X2) -> mark# X1)
     (mark# natsFrom X -> mark# X, mark# natsFrom X -> mark# X)
     (mark# natsFrom X -> mark# X, mark# natsFrom X -> a__natsFrom# mark X)
     (mark# natsFrom X -> mark# X, mark# s X -> mark# X)
     (mark# natsFrom X -> mark# X, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (mark# natsFrom X -> mark# X, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (mark# natsFrom X -> mark# X, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (mark# natsFrom X -> mark# X, mark# U12(X1, X2) -> mark# X1)
     (mark# natsFrom X -> mark# X, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (mark# natsFrom X -> mark# X, mark# splitAt(X1, X2) -> mark# X1)
     (mark# natsFrom X -> mark# X, mark# splitAt(X1, X2) -> mark# X2)
     (mark# natsFrom X -> mark# X, mark# afterNth(X1, X2) -> mark# X1)
     (mark# natsFrom X -> mark# X, mark# afterNth(X1, X2) -> mark# X2)
     (mark# natsFrom X -> mark# X, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (mark# natsFrom X -> mark# X, mark# snd X -> mark# X)
     (mark# natsFrom X -> mark# X, mark# snd X -> a__snd# mark X)
     (mark# natsFrom X -> mark# X, mark# and(X1, X2) -> mark# X1)
     (mark# natsFrom X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# natsFrom X -> mark# X, mark# fst X -> mark# X)
     (mark# natsFrom X -> mark# X, mark# fst X -> a__fst# mark X)
     (mark# natsFrom X -> mark# X, mark# head X -> mark# X)
     (mark# natsFrom X -> mark# X, mark# head X -> a__head# mark X)
     (mark# natsFrom X -> mark# X, mark# sel(X1, X2) -> mark# X1)
     (mark# natsFrom X -> mark# X, mark# sel(X1, X2) -> mark# X2)
     (mark# natsFrom X -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (mark# natsFrom X -> mark# X, mark# tail X -> mark# X)
     (mark# natsFrom X -> mark# X, mark# tail X -> a__tail# mark X)
     (mark# natsFrom X -> mark# X, mark# take(X1, X2) -> mark# X1)
     (mark# natsFrom X -> mark# X, mark# take(X1, X2) -> mark# X2)
     (mark# natsFrom X -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (mark# take(X1, X2) -> mark# X2, mark# pair(X1, X2) -> mark# X1)
     (mark# take(X1, X2) -> mark# X2, mark# pair(X1, X2) -> mark# X2)
     (mark# take(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
     (mark# take(X1, X2) -> mark# X2, mark# natsFrom X -> mark# X)
     (mark# take(X1, X2) -> mark# X2, mark# natsFrom X -> a__natsFrom# mark X)
     (mark# take(X1, X2) -> mark# X2, mark# s X -> mark# X)
     (mark# take(X1, X2) -> mark# X2, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (mark# take(X1, X2) -> mark# X2, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (mark# take(X1, X2) -> mark# X2, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (mark# take(X1, X2) -> mark# X2, mark# U12(X1, X2) -> mark# X1)
     (mark# take(X1, X2) -> mark# X2, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (mark# take(X1, X2) -> mark# X2, mark# splitAt(X1, X2) -> mark# X1)
     (mark# take(X1, X2) -> mark# X2, mark# splitAt(X1, X2) -> mark# X2)
     (mark# take(X1, X2) -> mark# X2, mark# afterNth(X1, X2) -> mark# X1)
     (mark# take(X1, X2) -> mark# X2, mark# afterNth(X1, X2) -> mark# X2)
     (mark# take(X1, X2) -> mark# X2, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (mark# take(X1, X2) -> mark# X2, mark# snd X -> mark# X)
     (mark# take(X1, X2) -> mark# X2, mark# snd X -> a__snd# mark X)
     (mark# take(X1, X2) -> mark# X2, mark# and(X1, X2) -> mark# X1)
     (mark# take(X1, X2) -> mark# X2, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# take(X1, X2) -> mark# X2, mark# fst X -> mark# X)
     (mark# take(X1, X2) -> mark# X2, mark# fst X -> a__fst# mark X)
     (mark# take(X1, X2) -> mark# X2, mark# head X -> mark# X)
     (mark# take(X1, X2) -> mark# X2, mark# head X -> a__head# mark X)
     (mark# take(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X1)
     (mark# take(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X2)
     (mark# take(X1, X2) -> mark# X2, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (mark# take(X1, X2) -> mark# X2, mark# tail X -> mark# X)
     (mark# take(X1, X2) -> mark# X2, mark# tail X -> a__tail# mark X)
     (mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> mark# X1)
     (mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> mark# X2)
     (mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (mark# afterNth(X1, X2) -> mark# X2, mark# pair(X1, X2) -> mark# X1)
     (mark# afterNth(X1, X2) -> mark# X2, mark# pair(X1, X2) -> mark# X2)
     (mark# afterNth(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
     (mark# afterNth(X1, X2) -> mark# X2, mark# natsFrom X -> mark# X)
     (mark# afterNth(X1, X2) -> mark# X2, mark# natsFrom X -> a__natsFrom# mark X)
     (mark# afterNth(X1, X2) -> mark# X2, mark# s X -> mark# X)
     (mark# afterNth(X1, X2) -> mark# X2, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (mark# afterNth(X1, X2) -> mark# X2, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (mark# afterNth(X1, X2) -> mark# X2, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (mark# afterNth(X1, X2) -> mark# X2, mark# U12(X1, X2) -> mark# X1)
     (mark# afterNth(X1, X2) -> mark# X2, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (mark# afterNth(X1, X2) -> mark# X2, mark# splitAt(X1, X2) -> mark# X1)
     (mark# afterNth(X1, X2) -> mark# X2, mark# splitAt(X1, X2) -> mark# X2)
     (mark# afterNth(X1, X2) -> mark# X2, mark# afterNth(X1, X2) -> mark# X1)
     (mark# afterNth(X1, X2) -> mark# X2, mark# afterNth(X1, X2) -> mark# X2)
     (mark# afterNth(X1, X2) -> mark# X2, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (mark# afterNth(X1, X2) -> mark# X2, mark# snd X -> mark# X)
     (mark# afterNth(X1, X2) -> mark# X2, mark# snd X -> a__snd# mark X)
     (mark# afterNth(X1, X2) -> mark# X2, mark# and(X1, X2) -> mark# X1)
     (mark# afterNth(X1, X2) -> mark# X2, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# afterNth(X1, X2) -> mark# X2, mark# fst X -> mark# X)
     (mark# afterNth(X1, X2) -> mark# X2, mark# fst X -> a__fst# mark X)
     (mark# afterNth(X1, X2) -> mark# X2, mark# head X -> mark# X)
     (mark# afterNth(X1, X2) -> mark# X2, mark# head X -> a__head# mark X)
     (mark# afterNth(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X1)
     (mark# afterNth(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X2)
     (mark# afterNth(X1, X2) -> mark# X2, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (mark# afterNth(X1, X2) -> mark# X2, mark# tail X -> mark# X)
     (mark# afterNth(X1, X2) -> mark# X2, mark# tail X -> a__tail# mark X)
     (mark# afterNth(X1, X2) -> mark# X2, mark# take(X1, X2) -> mark# X1)
     (mark# afterNth(X1, X2) -> mark# X2, mark# take(X1, X2) -> mark# X2)
     (mark# afterNth(X1, X2) -> mark# X2, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (mark# pair(X1, X2) -> mark# X2, mark# pair(X1, X2) -> mark# X1)
     (mark# pair(X1, X2) -> mark# X2, mark# pair(X1, X2) -> mark# X2)
     (mark# pair(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1)
     (mark# pair(X1, X2) -> mark# X2, mark# natsFrom X -> mark# X)
     (mark# pair(X1, X2) -> mark# X2, mark# natsFrom X -> a__natsFrom# mark X)
     (mark# pair(X1, X2) -> mark# X2, mark# s X -> mark# X)
     (mark# pair(X1, X2) -> mark# X2, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (mark# pair(X1, X2) -> mark# X2, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (mark# pair(X1, X2) -> mark# X2, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (mark# pair(X1, X2) -> mark# X2, mark# U12(X1, X2) -> mark# X1)
     (mark# pair(X1, X2) -> mark# X2, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (mark# pair(X1, X2) -> mark# X2, mark# splitAt(X1, X2) -> mark# X1)
     (mark# pair(X1, X2) -> mark# X2, mark# splitAt(X1, X2) -> mark# X2)
     (mark# pair(X1, X2) -> mark# X2, mark# afterNth(X1, X2) -> mark# X1)
     (mark# pair(X1, X2) -> mark# X2, mark# afterNth(X1, X2) -> mark# X2)
     (mark# pair(X1, X2) -> mark# X2, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (mark# pair(X1, X2) -> mark# X2, mark# snd X -> mark# X)
     (mark# pair(X1, X2) -> mark# X2, mark# snd X -> a__snd# mark X)
     (mark# pair(X1, X2) -> mark# X2, mark# and(X1, X2) -> mark# X1)
     (mark# pair(X1, X2) -> mark# X2, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# pair(X1, X2) -> mark# X2, mark# fst X -> mark# X)
     (mark# pair(X1, X2) -> mark# X2, mark# fst X -> a__fst# mark X)
     (mark# pair(X1, X2) -> mark# X2, mark# head X -> mark# X)
     (mark# pair(X1, X2) -> mark# X2, mark# head X -> a__head# mark X)
     (mark# pair(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X1)
     (mark# pair(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X2)
     (mark# pair(X1, X2) -> mark# X2, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (mark# pair(X1, X2) -> mark# X2, mark# tail X -> mark# X)
     (mark# pair(X1, X2) -> mark# X2, mark# tail X -> a__tail# mark X)
     (mark# pair(X1, X2) -> mark# X2, mark# take(X1, X2) -> mark# X1)
     (mark# pair(X1, X2) -> mark# X2, mark# take(X1, X2) -> mark# X2)
     (mark# pair(X1, X2) -> mark# X2, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (mark# head X -> a__head# mark X, a__head# cons(N, XS) -> mark# N)
     (mark# snd X -> a__snd# mark X, a__snd# pair(X, Y) -> mark# Y)
     (a__U12#(pair(YS, ZS), X) -> mark# ZS, mark# pair(X1, X2) -> mark# X1)
     (a__U12#(pair(YS, ZS), X) -> mark# ZS, mark# pair(X1, X2) -> mark# X2)
     (a__U12#(pair(YS, ZS), X) -> mark# ZS, mark# cons(X1, X2) -> mark# X1)
     (a__U12#(pair(YS, ZS), X) -> mark# ZS, mark# natsFrom X -> mark# X)
     (a__U12#(pair(YS, ZS), X) -> mark# ZS, mark# natsFrom X -> a__natsFrom# mark X)
     (a__U12#(pair(YS, ZS), X) -> mark# ZS, mark# s X -> mark# X)
     (a__U12#(pair(YS, ZS), X) -> mark# ZS, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (a__U12#(pair(YS, ZS), X) -> mark# ZS, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (a__U12#(pair(YS, ZS), X) -> mark# ZS, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (a__U12#(pair(YS, ZS), X) -> mark# ZS, mark# U12(X1, X2) -> mark# X1)
     (a__U12#(pair(YS, ZS), X) -> mark# ZS, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (a__U12#(pair(YS, ZS), X) -> mark# ZS, mark# splitAt(X1, X2) -> mark# X1)
     (a__U12#(pair(YS, ZS), X) -> mark# ZS, mark# splitAt(X1, X2) -> mark# X2)
     (a__U12#(pair(YS, ZS), X) -> mark# ZS, mark# afterNth(X1, X2) -> mark# X1)
     (a__U12#(pair(YS, ZS), X) -> mark# ZS, mark# afterNth(X1, X2) -> mark# X2)
     (a__U12#(pair(YS, ZS), X) -> mark# ZS, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (a__U12#(pair(YS, ZS), X) -> mark# ZS, mark# snd X -> mark# X)
     (a__U12#(pair(YS, ZS), X) -> mark# ZS, mark# snd X -> a__snd# mark X)
     (a__U12#(pair(YS, ZS), X) -> mark# ZS, mark# and(X1, X2) -> mark# X1)
     (a__U12#(pair(YS, ZS), X) -> mark# ZS, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (a__U12#(pair(YS, ZS), X) -> mark# ZS, mark# fst X -> mark# X)
     (a__U12#(pair(YS, ZS), X) -> mark# ZS, mark# fst X -> a__fst# mark X)
     (a__U12#(pair(YS, ZS), X) -> mark# ZS, mark# head X -> mark# X)
     (a__U12#(pair(YS, ZS), X) -> mark# ZS, mark# head X -> a__head# mark X)
     (a__U12#(pair(YS, ZS), X) -> mark# ZS, mark# sel(X1, X2) -> mark# X1)
     (a__U12#(pair(YS, ZS), X) -> mark# ZS, mark# sel(X1, X2) -> mark# X2)
     (a__U12#(pair(YS, ZS), X) -> mark# ZS, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (a__U12#(pair(YS, ZS), X) -> mark# ZS, mark# tail X -> mark# X)
     (a__U12#(pair(YS, ZS), X) -> mark# ZS, mark# tail X -> a__tail# mark X)
     (a__U12#(pair(YS, ZS), X) -> mark# ZS, mark# take(X1, X2) -> mark# X1)
     (a__U12#(pair(YS, ZS), X) -> mark# ZS, mark# take(X1, X2) -> mark# X2)
     (a__U12#(pair(YS, ZS), X) -> mark# ZS, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (mark# and(X1, X2) -> a__and#(mark X1, X2), a__and#(tt(), X) -> mark# X)
     (mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4), a__U11#(tt(), N, X, XS) -> a__U12#(a__splitAt(mark N, mark XS), X))
     (mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4), a__U11#(tt(), N, X, XS) -> a__splitAt#(mark N, mark XS))
     (mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4), a__U11#(tt(), N, X, XS) -> mark# N)
     (mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4), a__U11#(tt(), N, X, XS) -> mark# XS)
     (a__tail# cons(N, XS) -> mark# XS, mark# pair(X1, X2) -> mark# X1)
     (a__tail# cons(N, XS) -> mark# XS, mark# pair(X1, X2) -> mark# X2)
     (a__tail# cons(N, XS) -> mark# XS, mark# cons(X1, X2) -> mark# X1)
     (a__tail# cons(N, XS) -> mark# XS, mark# natsFrom X -> mark# X)
     (a__tail# cons(N, XS) -> mark# XS, mark# natsFrom X -> a__natsFrom# mark X)
     (a__tail# cons(N, XS) -> mark# XS, mark# s X -> mark# X)
     (a__tail# cons(N, XS) -> mark# XS, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (a__tail# cons(N, XS) -> mark# XS, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (a__tail# cons(N, XS) -> mark# XS, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (a__tail# cons(N, XS) -> mark# XS, mark# U12(X1, X2) -> mark# X1)
     (a__tail# cons(N, XS) -> mark# XS, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (a__tail# cons(N, XS) -> mark# XS, mark# splitAt(X1, X2) -> mark# X1)
     (a__tail# cons(N, XS) -> mark# XS, mark# splitAt(X1, X2) -> mark# X2)
     (a__tail# cons(N, XS) -> mark# XS, mark# afterNth(X1, X2) -> mark# X1)
     (a__tail# cons(N, XS) -> mark# XS, mark# afterNth(X1, X2) -> mark# X2)
     (a__tail# cons(N, XS) -> mark# XS, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (a__tail# cons(N, XS) -> mark# XS, mark# snd X -> mark# X)
     (a__tail# cons(N, XS) -> mark# XS, mark# snd X -> a__snd# mark X)
     (a__tail# cons(N, XS) -> mark# XS, mark# and(X1, X2) -> mark# X1)
     (a__tail# cons(N, XS) -> mark# XS, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (a__tail# cons(N, XS) -> mark# XS, mark# fst X -> mark# X)
     (a__tail# cons(N, XS) -> mark# XS, mark# fst X -> a__fst# mark X)
     (a__tail# cons(N, XS) -> mark# XS, mark# head X -> mark# X)
     (a__tail# cons(N, XS) -> mark# XS, mark# head X -> a__head# mark X)
     (a__tail# cons(N, XS) -> mark# XS, mark# sel(X1, X2) -> mark# X1)
     (a__tail# cons(N, XS) -> mark# XS, mark# sel(X1, X2) -> mark# X2)
     (a__tail# cons(N, XS) -> mark# XS, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (a__tail# cons(N, XS) -> mark# XS, mark# tail X -> mark# X)
     (a__tail# cons(N, XS) -> mark# XS, mark# tail X -> a__tail# mark X)
     (a__tail# cons(N, XS) -> mark# XS, mark# take(X1, X2) -> mark# X1)
     (a__tail# cons(N, XS) -> mark# XS, mark# take(X1, X2) -> mark# X2)
     (a__tail# cons(N, XS) -> mark# XS, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (a__afterNth#(N, XS) -> mark# XS, mark# pair(X1, X2) -> mark# X1)
     (a__afterNth#(N, XS) -> mark# XS, mark# pair(X1, X2) -> mark# X2)
     (a__afterNth#(N, XS) -> mark# XS, mark# cons(X1, X2) -> mark# X1)
     (a__afterNth#(N, XS) -> mark# XS, mark# natsFrom X -> mark# X)
     (a__afterNth#(N, XS) -> mark# XS, mark# natsFrom X -> a__natsFrom# mark X)
     (a__afterNth#(N, XS) -> mark# XS, mark# s X -> mark# X)
     (a__afterNth#(N, XS) -> mark# XS, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (a__afterNth#(N, XS) -> mark# XS, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (a__afterNth#(N, XS) -> mark# XS, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (a__afterNth#(N, XS) -> mark# XS, mark# U12(X1, X2) -> mark# X1)
     (a__afterNth#(N, XS) -> mark# XS, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (a__afterNth#(N, XS) -> mark# XS, mark# splitAt(X1, X2) -> mark# X1)
     (a__afterNth#(N, XS) -> mark# XS, mark# splitAt(X1, X2) -> mark# X2)
     (a__afterNth#(N, XS) -> mark# XS, mark# afterNth(X1, X2) -> mark# X1)
     (a__afterNth#(N, XS) -> mark# XS, mark# afterNth(X1, X2) -> mark# X2)
     (a__afterNth#(N, XS) -> mark# XS, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (a__afterNth#(N, XS) -> mark# XS, mark# snd X -> mark# X)
     (a__afterNth#(N, XS) -> mark# XS, mark# snd X -> a__snd# mark X)
     (a__afterNth#(N, XS) -> mark# XS, mark# and(X1, X2) -> mark# X1)
     (a__afterNth#(N, XS) -> mark# XS, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (a__afterNth#(N, XS) -> mark# XS, mark# fst X -> mark# X)
     (a__afterNth#(N, XS) -> mark# XS, mark# fst X -> a__fst# mark X)
     (a__afterNth#(N, XS) -> mark# XS, mark# head X -> mark# X)
     (a__afterNth#(N, XS) -> mark# XS, mark# head X -> a__head# mark X)
     (a__afterNth#(N, XS) -> mark# XS, mark# sel(X1, X2) -> mark# X1)
     (a__afterNth#(N, XS) -> mark# XS, mark# sel(X1, X2) -> mark# X2)
     (a__afterNth#(N, XS) -> mark# XS, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (a__afterNth#(N, XS) -> mark# XS, mark# tail X -> mark# X)
     (a__afterNth#(N, XS) -> mark# XS, mark# tail X -> a__tail# mark X)
     (a__afterNth#(N, XS) -> mark# XS, mark# take(X1, X2) -> mark# X1)
     (a__afterNth#(N, XS) -> mark# XS, mark# take(X1, X2) -> mark# X2)
     (a__afterNth#(N, XS) -> mark# XS, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (a__splitAt#(0(), XS) -> mark# XS, mark# pair(X1, X2) -> mark# X1)
     (a__splitAt#(0(), XS) -> mark# XS, mark# pair(X1, X2) -> mark# X2)
     (a__splitAt#(0(), XS) -> mark# XS, mark# cons(X1, X2) -> mark# X1)
     (a__splitAt#(0(), XS) -> mark# XS, mark# natsFrom X -> mark# X)
     (a__splitAt#(0(), XS) -> mark# XS, mark# natsFrom X -> a__natsFrom# mark X)
     (a__splitAt#(0(), XS) -> mark# XS, mark# s X -> mark# X)
     (a__splitAt#(0(), XS) -> mark# XS, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (a__splitAt#(0(), XS) -> mark# XS, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (a__splitAt#(0(), XS) -> mark# XS, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (a__splitAt#(0(), XS) -> mark# XS, mark# U12(X1, X2) -> mark# X1)
     (a__splitAt#(0(), XS) -> mark# XS, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (a__splitAt#(0(), XS) -> mark# XS, mark# splitAt(X1, X2) -> mark# X1)
     (a__splitAt#(0(), XS) -> mark# XS, mark# splitAt(X1, X2) -> mark# X2)
     (a__splitAt#(0(), XS) -> mark# XS, mark# afterNth(X1, X2) -> mark# X1)
     (a__splitAt#(0(), XS) -> mark# XS, mark# afterNth(X1, X2) -> mark# X2)
     (a__splitAt#(0(), XS) -> mark# XS, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (a__splitAt#(0(), XS) -> mark# XS, mark# snd X -> mark# X)
     (a__splitAt#(0(), XS) -> mark# XS, mark# snd X -> a__snd# mark X)
     (a__splitAt#(0(), XS) -> mark# XS, mark# and(X1, X2) -> mark# X1)
     (a__splitAt#(0(), XS) -> mark# XS, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (a__splitAt#(0(), XS) -> mark# XS, mark# fst X -> mark# X)
     (a__splitAt#(0(), XS) -> mark# XS, mark# fst X -> a__fst# mark X)
     (a__splitAt#(0(), XS) -> mark# XS, mark# head X -> mark# X)
     (a__splitAt#(0(), XS) -> mark# XS, mark# head X -> a__head# mark X)
     (a__splitAt#(0(), XS) -> mark# XS, mark# sel(X1, X2) -> mark# X1)
     (a__splitAt#(0(), XS) -> mark# XS, mark# sel(X1, X2) -> mark# X2)
     (a__splitAt#(0(), XS) -> mark# XS, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (a__splitAt#(0(), XS) -> mark# XS, mark# tail X -> mark# X)
     (a__splitAt#(0(), XS) -> mark# XS, mark# tail X -> a__tail# mark X)
     (a__splitAt#(0(), XS) -> mark# XS, mark# take(X1, X2) -> mark# X1)
     (a__splitAt#(0(), XS) -> mark# XS, mark# take(X1, X2) -> mark# X2)
     (a__splitAt#(0(), XS) -> mark# XS, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (mark# sel(X1, X2) -> mark# X1, mark# pair(X1, X2) -> mark# X1)
     (mark# sel(X1, X2) -> mark# X1, mark# pair(X1, X2) -> mark# X2)
     (mark# sel(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (mark# sel(X1, X2) -> mark# X1, mark# natsFrom X -> mark# X)
     (mark# sel(X1, X2) -> mark# X1, mark# natsFrom X -> a__natsFrom# mark X)
     (mark# sel(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# sel(X1, X2) -> mark# X1, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (mark# sel(X1, X2) -> mark# X1, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (mark# sel(X1, X2) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (mark# sel(X1, X2) -> mark# X1, mark# U12(X1, X2) -> mark# X1)
     (mark# sel(X1, X2) -> mark# X1, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (mark# sel(X1, X2) -> mark# X1, mark# splitAt(X1, X2) -> mark# X1)
     (mark# sel(X1, X2) -> mark# X1, mark# splitAt(X1, X2) -> mark# X2)
     (mark# sel(X1, X2) -> mark# X1, mark# afterNth(X1, X2) -> mark# X1)
     (mark# sel(X1, X2) -> mark# X1, mark# afterNth(X1, X2) -> mark# X2)
     (mark# sel(X1, X2) -> mark# X1, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (mark# sel(X1, X2) -> mark# X1, mark# snd X -> mark# X)
     (mark# sel(X1, X2) -> mark# X1, mark# snd X -> a__snd# mark X)
     (mark# sel(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
     (mark# sel(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# sel(X1, X2) -> mark# X1, mark# fst X -> mark# X)
     (mark# sel(X1, X2) -> mark# X1, mark# fst X -> a__fst# mark X)
     (mark# sel(X1, X2) -> mark# X1, mark# head X -> mark# X)
     (mark# sel(X1, X2) -> mark# X1, mark# head X -> a__head# mark X)
     (mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1)
     (mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2)
     (mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (mark# sel(X1, X2) -> mark# X1, mark# tail X -> mark# X)
     (mark# sel(X1, X2) -> mark# X1, mark# tail X -> a__tail# mark X)
     (mark# sel(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1)
     (mark# sel(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2)
     (mark# sel(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (mark# afterNth(X1, X2) -> mark# X1, mark# pair(X1, X2) -> mark# X1)
     (mark# afterNth(X1, X2) -> mark# X1, mark# pair(X1, X2) -> mark# X2)
     (mark# afterNth(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (mark# afterNth(X1, X2) -> mark# X1, mark# natsFrom X -> mark# X)
     (mark# afterNth(X1, X2) -> mark# X1, mark# natsFrom X -> a__natsFrom# mark X)
     (mark# afterNth(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# afterNth(X1, X2) -> mark# X1, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (mark# afterNth(X1, X2) -> mark# X1, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (mark# afterNth(X1, X2) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (mark# afterNth(X1, X2) -> mark# X1, mark# U12(X1, X2) -> mark# X1)
     (mark# afterNth(X1, X2) -> mark# X1, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (mark# afterNth(X1, X2) -> mark# X1, mark# splitAt(X1, X2) -> mark# X1)
     (mark# afterNth(X1, X2) -> mark# X1, mark# splitAt(X1, X2) -> mark# X2)
     (mark# afterNth(X1, X2) -> mark# X1, mark# afterNth(X1, X2) -> mark# X1)
     (mark# afterNth(X1, X2) -> mark# X1, mark# afterNth(X1, X2) -> mark# X2)
     (mark# afterNth(X1, X2) -> mark# X1, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (mark# afterNth(X1, X2) -> mark# X1, mark# snd X -> mark# X)
     (mark# afterNth(X1, X2) -> mark# X1, mark# snd X -> a__snd# mark X)
     (mark# afterNth(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
     (mark# afterNth(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# afterNth(X1, X2) -> mark# X1, mark# fst X -> mark# X)
     (mark# afterNth(X1, X2) -> mark# X1, mark# fst X -> a__fst# mark X)
     (mark# afterNth(X1, X2) -> mark# X1, mark# head X -> mark# X)
     (mark# afterNth(X1, X2) -> mark# X1, mark# head X -> a__head# mark X)
     (mark# afterNth(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1)
     (mark# afterNth(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2)
     (mark# afterNth(X1, X2) -> mark# X1, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (mark# afterNth(X1, X2) -> mark# X1, mark# tail X -> mark# X)
     (mark# afterNth(X1, X2) -> mark# X1, mark# tail X -> a__tail# mark X)
     (mark# afterNth(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1)
     (mark# afterNth(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2)
     (mark# afterNth(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (mark# U12(X1, X2) -> mark# X1, mark# pair(X1, X2) -> mark# X1)
     (mark# U12(X1, X2) -> mark# X1, mark# pair(X1, X2) -> mark# X2)
     (mark# U12(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (mark# U12(X1, X2) -> mark# X1, mark# natsFrom X -> mark# X)
     (mark# U12(X1, X2) -> mark# X1, mark# natsFrom X -> a__natsFrom# mark X)
     (mark# U12(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# U12(X1, X2) -> mark# X1, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (mark# U12(X1, X2) -> mark# X1, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (mark# U12(X1, X2) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (mark# U12(X1, X2) -> mark# X1, mark# U12(X1, X2) -> mark# X1)
     (mark# U12(X1, X2) -> mark# X1, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (mark# U12(X1, X2) -> mark# X1, mark# splitAt(X1, X2) -> mark# X1)
     (mark# U12(X1, X2) -> mark# X1, mark# splitAt(X1, X2) -> mark# X2)
     (mark# U12(X1, X2) -> mark# X1, mark# afterNth(X1, X2) -> mark# X1)
     (mark# U12(X1, X2) -> mark# X1, mark# afterNth(X1, X2) -> mark# X2)
     (mark# U12(X1, X2) -> mark# X1, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (mark# U12(X1, X2) -> mark# X1, mark# snd X -> mark# X)
     (mark# U12(X1, X2) -> mark# X1, mark# snd X -> a__snd# mark X)
     (mark# U12(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
     (mark# U12(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# U12(X1, X2) -> mark# X1, mark# fst X -> mark# X)
     (mark# U12(X1, X2) -> mark# X1, mark# fst X -> a__fst# mark X)
     (mark# U12(X1, X2) -> mark# X1, mark# head X -> mark# X)
     (mark# U12(X1, X2) -> mark# X1, mark# head X -> a__head# mark X)
     (mark# U12(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1)
     (mark# U12(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2)
     (mark# U12(X1, X2) -> mark# X1, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (mark# U12(X1, X2) -> mark# X1, mark# tail X -> mark# X)
     (mark# U12(X1, X2) -> mark# X1, mark# tail X -> a__tail# mark X)
     (mark# U12(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1)
     (mark# U12(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2)
     (mark# U12(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (mark# cons(X1, X2) -> mark# X1, mark# pair(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# pair(X1, X2) -> mark# X2)
     (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# natsFrom X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# natsFrom X -> a__natsFrom# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (mark# cons(X1, X2) -> mark# X1, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (mark# cons(X1, X2) -> mark# X1, mark# U12(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (mark# cons(X1, X2) -> mark# X1, mark# splitAt(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# splitAt(X1, X2) -> mark# X2)
     (mark# cons(X1, X2) -> mark# X1, mark# afterNth(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# afterNth(X1, X2) -> mark# X2)
     (mark# cons(X1, X2) -> mark# X1, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (mark# cons(X1, X2) -> mark# X1, mark# snd X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# snd X -> a__snd# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# cons(X1, X2) -> mark# X1, mark# fst X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# fst X -> a__fst# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# head X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# head X -> a__head# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2)
     (mark# cons(X1, X2) -> mark# X1, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (mark# cons(X1, X2) -> mark# X1, mark# tail X -> mark# X)
     (mark# cons(X1, X2) -> mark# X1, mark# tail X -> a__tail# mark X)
     (mark# cons(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1)
     (mark# cons(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2)
     (mark# cons(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (a__take#(N, XS) -> a__fst# a__splitAt(mark N, mark XS), a__fst# pair(X, Y) -> mark# X)
     (a__afterNth#(N, XS) -> a__snd# a__splitAt(mark N, mark XS), a__snd# pair(X, Y) -> mark# Y)
     (a__sel#(N, XS) -> a__afterNth#(mark N, mark XS), a__afterNth#(N, XS) -> a__splitAt#(mark N, mark XS))
     (a__sel#(N, XS) -> a__afterNth#(mark N, mark XS), a__afterNth#(N, XS) -> mark# N)
     (a__sel#(N, XS) -> a__afterNth#(mark N, mark XS), a__afterNth#(N, XS) -> mark# XS)
     (a__sel#(N, XS) -> a__afterNth#(mark N, mark XS), a__afterNth#(N, XS) -> a__snd# a__splitAt(mark N, mark XS))
     (a__U11#(tt(), N, X, XS) -> a__splitAt#(mark N, mark XS), a__splitAt#(s N, cons(X, XS)) -> a__U11#(tt(), N, X, XS))
     (a__U11#(tt(), N, X, XS) -> a__splitAt#(mark N, mark XS), a__splitAt#(0(), XS) -> mark# XS)
     (mark# sel(X1, X2) -> a__sel#(mark X1, mark X2), a__sel#(N, XS) -> mark# N)
     (mark# sel(X1, X2) -> a__sel#(mark X1, mark X2), a__sel#(N, XS) -> mark# XS)
     (mark# sel(X1, X2) -> a__sel#(mark X1, mark X2), a__sel#(N, XS) -> a__afterNth#(mark N, mark XS))
     (mark# sel(X1, X2) -> a__sel#(mark X1, mark X2), a__sel#(N, XS) -> a__head# a__afterNth(mark N, mark XS))
     (mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2), a__splitAt#(s N, cons(X, XS)) -> a__U11#(tt(), N, X, XS))
     (mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2), a__splitAt#(0(), XS) -> mark# XS)
     (a__take#(N, XS) -> mark# N, mark# pair(X1, X2) -> mark# X1)
     (a__take#(N, XS) -> mark# N, mark# pair(X1, X2) -> mark# X2)
     (a__take#(N, XS) -> mark# N, mark# cons(X1, X2) -> mark# X1)
     (a__take#(N, XS) -> mark# N, mark# natsFrom X -> mark# X)
     (a__take#(N, XS) -> mark# N, mark# natsFrom X -> a__natsFrom# mark X)
     (a__take#(N, XS) -> mark# N, mark# s X -> mark# X)
     (a__take#(N, XS) -> mark# N, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (a__take#(N, XS) -> mark# N, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (a__take#(N, XS) -> mark# N, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (a__take#(N, XS) -> mark# N, mark# U12(X1, X2) -> mark# X1)
     (a__take#(N, XS) -> mark# N, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (a__take#(N, XS) -> mark# N, mark# splitAt(X1, X2) -> mark# X1)
     (a__take#(N, XS) -> mark# N, mark# splitAt(X1, X2) -> mark# X2)
     (a__take#(N, XS) -> mark# N, mark# afterNth(X1, X2) -> mark# X1)
     (a__take#(N, XS) -> mark# N, mark# afterNth(X1, X2) -> mark# X2)
     (a__take#(N, XS) -> mark# N, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (a__take#(N, XS) -> mark# N, mark# snd X -> mark# X)
     (a__take#(N, XS) -> mark# N, mark# snd X -> a__snd# mark X)
     (a__take#(N, XS) -> mark# N, mark# and(X1, X2) -> mark# X1)
     (a__take#(N, XS) -> mark# N, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (a__take#(N, XS) -> mark# N, mark# fst X -> mark# X)
     (a__take#(N, XS) -> mark# N, mark# fst X -> a__fst# mark X)
     (a__take#(N, XS) -> mark# N, mark# head X -> mark# X)
     (a__take#(N, XS) -> mark# N, mark# head X -> a__head# mark X)
     (a__take#(N, XS) -> mark# N, mark# sel(X1, X2) -> mark# X1)
     (a__take#(N, XS) -> mark# N, mark# sel(X1, X2) -> mark# X2)
     (a__take#(N, XS) -> mark# N, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (a__take#(N, XS) -> mark# N, mark# tail X -> mark# X)
     (a__take#(N, XS) -> mark# N, mark# tail X -> a__tail# mark X)
     (a__take#(N, XS) -> mark# N, mark# take(X1, X2) -> mark# X1)
     (a__take#(N, XS) -> mark# N, mark# take(X1, X2) -> mark# X2)
     (a__take#(N, XS) -> mark# N, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (a__natsFrom# N -> mark# N, mark# pair(X1, X2) -> mark# X1)
     (a__natsFrom# N -> mark# N, mark# pair(X1, X2) -> mark# X2)
     (a__natsFrom# N -> mark# N, mark# cons(X1, X2) -> mark# X1)
     (a__natsFrom# N -> mark# N, mark# natsFrom X -> mark# X)
     (a__natsFrom# N -> mark# N, mark# natsFrom X -> a__natsFrom# mark X)
     (a__natsFrom# N -> mark# N, mark# s X -> mark# X)
     (a__natsFrom# N -> mark# N, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (a__natsFrom# N -> mark# N, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (a__natsFrom# N -> mark# N, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (a__natsFrom# N -> mark# N, mark# U12(X1, X2) -> mark# X1)
     (a__natsFrom# N -> mark# N, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (a__natsFrom# N -> mark# N, mark# splitAt(X1, X2) -> mark# X1)
     (a__natsFrom# N -> mark# N, mark# splitAt(X1, X2) -> mark# X2)
     (a__natsFrom# N -> mark# N, mark# afterNth(X1, X2) -> mark# X1)
     (a__natsFrom# N -> mark# N, mark# afterNth(X1, X2) -> mark# X2)
     (a__natsFrom# N -> mark# N, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (a__natsFrom# N -> mark# N, mark# snd X -> mark# X)
     (a__natsFrom# N -> mark# N, mark# snd X -> a__snd# mark X)
     (a__natsFrom# N -> mark# N, mark# and(X1, X2) -> mark# X1)
     (a__natsFrom# N -> mark# N, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (a__natsFrom# N -> mark# N, mark# fst X -> mark# X)
     (a__natsFrom# N -> mark# N, mark# fst X -> a__fst# mark X)
     (a__natsFrom# N -> mark# N, mark# head X -> mark# X)
     (a__natsFrom# N -> mark# N, mark# head X -> a__head# mark X)
     (a__natsFrom# N -> mark# N, mark# sel(X1, X2) -> mark# X1)
     (a__natsFrom# N -> mark# N, mark# sel(X1, X2) -> mark# X2)
     (a__natsFrom# N -> mark# N, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (a__natsFrom# N -> mark# N, mark# tail X -> mark# X)
     (a__natsFrom# N -> mark# N, mark# tail X -> a__tail# mark X)
     (a__natsFrom# N -> mark# N, mark# take(X1, X2) -> mark# X1)
     (a__natsFrom# N -> mark# N, mark# take(X1, X2) -> mark# X2)
     (a__natsFrom# N -> mark# N, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (a__afterNth#(N, XS) -> mark# N, mark# pair(X1, X2) -> mark# X1)
     (a__afterNth#(N, XS) -> mark# N, mark# pair(X1, X2) -> mark# X2)
     (a__afterNth#(N, XS) -> mark# N, mark# cons(X1, X2) -> mark# X1)
     (a__afterNth#(N, XS) -> mark# N, mark# natsFrom X -> mark# X)
     (a__afterNth#(N, XS) -> mark# N, mark# natsFrom X -> a__natsFrom# mark X)
     (a__afterNth#(N, XS) -> mark# N, mark# s X -> mark# X)
     (a__afterNth#(N, XS) -> mark# N, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (a__afterNth#(N, XS) -> mark# N, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (a__afterNth#(N, XS) -> mark# N, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (a__afterNth#(N, XS) -> mark# N, mark# U12(X1, X2) -> mark# X1)
     (a__afterNth#(N, XS) -> mark# N, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (a__afterNth#(N, XS) -> mark# N, mark# splitAt(X1, X2) -> mark# X1)
     (a__afterNth#(N, XS) -> mark# N, mark# splitAt(X1, X2) -> mark# X2)
     (a__afterNth#(N, XS) -> mark# N, mark# afterNth(X1, X2) -> mark# X1)
     (a__afterNth#(N, XS) -> mark# N, mark# afterNth(X1, X2) -> mark# X2)
     (a__afterNth#(N, XS) -> mark# N, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (a__afterNth#(N, XS) -> mark# N, mark# snd X -> mark# X)
     (a__afterNth#(N, XS) -> mark# N, mark# snd X -> a__snd# mark X)
     (a__afterNth#(N, XS) -> mark# N, mark# and(X1, X2) -> mark# X1)
     (a__afterNth#(N, XS) -> mark# N, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (a__afterNth#(N, XS) -> mark# N, mark# fst X -> mark# X)
     (a__afterNth#(N, XS) -> mark# N, mark# fst X -> a__fst# mark X)
     (a__afterNth#(N, XS) -> mark# N, mark# head X -> mark# X)
     (a__afterNth#(N, XS) -> mark# N, mark# head X -> a__head# mark X)
     (a__afterNth#(N, XS) -> mark# N, mark# sel(X1, X2) -> mark# X1)
     (a__afterNth#(N, XS) -> mark# N, mark# sel(X1, X2) -> mark# X2)
     (a__afterNth#(N, XS) -> mark# N, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (a__afterNth#(N, XS) -> mark# N, mark# tail X -> mark# X)
     (a__afterNth#(N, XS) -> mark# N, mark# tail X -> a__tail# mark X)
     (a__afterNth#(N, XS) -> mark# N, mark# take(X1, X2) -> mark# X1)
     (a__afterNth#(N, XS) -> mark# N, mark# take(X1, X2) -> mark# X2)
     (a__afterNth#(N, XS) -> mark# N, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
     (a__snd# pair(X, Y) -> mark# Y, mark# pair(X1, X2) -> mark# X1)
     (a__snd# pair(X, Y) -> mark# Y, mark# pair(X1, X2) -> mark# X2)
     (a__snd# pair(X, Y) -> mark# Y, mark# cons(X1, X2) -> mark# X1)
     (a__snd# pair(X, Y) -> mark# Y, mark# natsFrom X -> mark# X)
     (a__snd# pair(X, Y) -> mark# Y, mark# natsFrom X -> a__natsFrom# mark X)
     (a__snd# pair(X, Y) -> mark# Y, mark# s X -> mark# X)
     (a__snd# pair(X, Y) -> mark# Y, mark# U11(X1, X2, X3, X4) -> mark# X1)
     (a__snd# pair(X, Y) -> mark# Y, mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4))
     (a__snd# pair(X, Y) -> mark# Y, mark# U12(X1, X2) -> a__U12#(mark X1, X2))
     (a__snd# pair(X, Y) -> mark# Y, mark# U12(X1, X2) -> mark# X1)
     (a__snd# pair(X, Y) -> mark# Y, mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2))
     (a__snd# pair(X, Y) -> mark# Y, mark# splitAt(X1, X2) -> mark# X1)
     (a__snd# pair(X, Y) -> mark# Y, mark# splitAt(X1, X2) -> mark# X2)
     (a__snd# pair(X, Y) -> mark# Y, mark# afterNth(X1, X2) -> mark# X1)
     (a__snd# pair(X, Y) -> mark# Y, mark# afterNth(X1, X2) -> mark# X2)
     (a__snd# pair(X, Y) -> mark# Y, mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2))
     (a__snd# pair(X, Y) -> mark# Y, mark# snd X -> mark# X)
     (a__snd# pair(X, Y) -> mark# Y, mark# snd X -> a__snd# mark X)
     (a__snd# pair(X, Y) -> mark# Y, mark# and(X1, X2) -> mark# X1)
     (a__snd# pair(X, Y) -> mark# Y, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (a__snd# pair(X, Y) -> mark# Y, mark# fst X -> mark# X)
     (a__snd# pair(X, Y) -> mark# Y, mark# fst X -> a__fst# mark X)
     (a__snd# pair(X, Y) -> mark# Y, mark# head X -> mark# X)
     (a__snd# pair(X, Y) -> mark# Y, mark# head X -> a__head# mark X)
     (a__snd# pair(X, Y) -> mark# Y, mark# sel(X1, X2) -> mark# X1)
     (a__snd# pair(X, Y) -> mark# Y, mark# sel(X1, X2) -> mark# X2)
     (a__snd# pair(X, Y) -> mark# Y, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2))
     (a__snd# pair(X, Y) -> mark# Y, mark# tail X -> mark# X)
     (a__snd# pair(X, Y) -> mark# Y, mark# tail X -> a__tail# mark X)
     (a__snd# pair(X, Y) -> mark# Y, mark# take(X1, X2) -> mark# X1)
     (a__snd# pair(X, Y) -> mark# Y, mark# take(X1, X2) -> mark# X2)
     (a__snd# pair(X, Y) -> mark# Y, mark# take(X1, X2) -> a__take#(mark X1, mark X2))
    }
    STATUS:
     arrows: 0.634661
     SCCS (1):
      Scc:
       {     a__U12#(pair(YS, ZS), X) -> mark# X,
             a__U12#(pair(YS, ZS), X) -> mark# ZS,
        a__splitAt#(s N, cons(X, XS)) -> a__U11#(tt(), N, X, XS),
                 a__splitAt#(0(), XS) -> mark# XS,
                   mark# pair(X1, X2) -> mark# X1,
                   mark# pair(X1, X2) -> mark# X2,
                   mark# cons(X1, X2) -> mark# X1,
                     mark# natsFrom X -> mark# X,
                     mark# natsFrom X -> a__natsFrom# mark X,
                            mark# s X -> mark# X,
            mark# U11(X1, X2, X3, X4) -> mark# X1,
            mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4),
                    mark# U12(X1, X2) -> a__U12#(mark X1, X2),
                    mark# U12(X1, X2) -> mark# X1,
                mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2),
                mark# splitAt(X1, X2) -> mark# X1,
                mark# splitAt(X1, X2) -> mark# X2,
               mark# afterNth(X1, X2) -> mark# X1,
               mark# afterNth(X1, X2) -> mark# X2,
               mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2),
                          mark# snd X -> mark# X,
                          mark# snd X -> a__snd# mark X,
                    mark# and(X1, X2) -> mark# X1,
                    mark# and(X1, X2) -> a__and#(mark X1, X2),
                          mark# fst X -> mark# X,
                          mark# fst X -> a__fst# mark X,
                         mark# head X -> mark# X,
                         mark# head X -> a__head# mark X,
                    mark# sel(X1, X2) -> mark# X1,
                    mark# sel(X1, X2) -> mark# X2,
                    mark# sel(X1, X2) -> a__sel#(mark X1, mark X2),
                         mark# tail X -> mark# X,
                         mark# tail X -> a__tail# mark X,
                   mark# take(X1, X2) -> mark# X1,
                   mark# take(X1, X2) -> mark# X2,
                   mark# take(X1, X2) -> a__take#(mark X1, mark X2),
              a__U11#(tt(), N, X, XS) -> a__U12#(a__splitAt(mark N, mark XS), X),
              a__U11#(tt(), N, X, XS) -> a__splitAt#(mark N, mark XS),
              a__U11#(tt(), N, X, XS) -> mark# N,
              a__U11#(tt(), N, X, XS) -> mark# XS,
                   a__snd# pair(X, Y) -> mark# Y,
                  a__afterNth#(N, XS) -> a__splitAt#(mark N, mark XS),
                  a__afterNth#(N, XS) -> mark# N,
                  a__afterNth#(N, XS) -> mark# XS,
                  a__afterNth#(N, XS) -> a__snd# a__splitAt(mark N, mark XS),
                     a__and#(tt(), X) -> mark# X,
                   a__fst# pair(X, Y) -> mark# X,
                 a__head# cons(N, XS) -> mark# N,
                       a__natsFrom# N -> mark# N,
                       a__sel#(N, XS) -> mark# N,
                       a__sel#(N, XS) -> mark# XS,
                       a__sel#(N, XS) -> a__afterNth#(mark N, mark XS),
                       a__sel#(N, XS) -> a__head# a__afterNth(mark N, mark XS),
                 a__tail# cons(N, XS) -> mark# XS,
                      a__take#(N, XS) -> a__splitAt#(mark N, mark XS),
                      a__take#(N, XS) -> mark# N,
                      a__take#(N, XS) -> mark# XS,
                      a__take#(N, XS) -> a__fst# a__splitAt(mark N, mark XS)}
      
      SCC (58):
       Strict:
        {     a__U12#(pair(YS, ZS), X) -> mark# X,
              a__U12#(pair(YS, ZS), X) -> mark# ZS,
         a__splitAt#(s N, cons(X, XS)) -> a__U11#(tt(), N, X, XS),
                  a__splitAt#(0(), XS) -> mark# XS,
                    mark# pair(X1, X2) -> mark# X1,
                    mark# pair(X1, X2) -> mark# X2,
                    mark# cons(X1, X2) -> mark# X1,
                      mark# natsFrom X -> mark# X,
                      mark# natsFrom X -> a__natsFrom# mark X,
                             mark# s X -> mark# X,
             mark# U11(X1, X2, X3, X4) -> mark# X1,
             mark# U11(X1, X2, X3, X4) -> a__U11#(mark X1, X2, X3, X4),
                     mark# U12(X1, X2) -> a__U12#(mark X1, X2),
                     mark# U12(X1, X2) -> mark# X1,
                 mark# splitAt(X1, X2) -> a__splitAt#(mark X1, mark X2),
                 mark# splitAt(X1, X2) -> mark# X1,
                 mark# splitAt(X1, X2) -> mark# X2,
                mark# afterNth(X1, X2) -> mark# X1,
                mark# afterNth(X1, X2) -> mark# X2,
                mark# afterNth(X1, X2) -> a__afterNth#(mark X1, mark X2),
                           mark# snd X -> mark# X,
                           mark# snd X -> a__snd# mark X,
                     mark# and(X1, X2) -> mark# X1,
                     mark# and(X1, X2) -> a__and#(mark X1, X2),
                           mark# fst X -> mark# X,
                           mark# fst X -> a__fst# mark X,
                          mark# head X -> mark# X,
                          mark# head X -> a__head# mark X,
                     mark# sel(X1, X2) -> mark# X1,
                     mark# sel(X1, X2) -> mark# X2,
                     mark# sel(X1, X2) -> a__sel#(mark X1, mark X2),
                          mark# tail X -> mark# X,
                          mark# tail X -> a__tail# mark X,
                    mark# take(X1, X2) -> mark# X1,
                    mark# take(X1, X2) -> mark# X2,
                    mark# take(X1, X2) -> a__take#(mark X1, mark X2),
               a__U11#(tt(), N, X, XS) -> a__U12#(a__splitAt(mark N, mark XS), X),
               a__U11#(tt(), N, X, XS) -> a__splitAt#(mark N, mark XS),
               a__U11#(tt(), N, X, XS) -> mark# N,
               a__U11#(tt(), N, X, XS) -> mark# XS,
                    a__snd# pair(X, Y) -> mark# Y,
                   a__afterNth#(N, XS) -> a__splitAt#(mark N, mark XS),
                   a__afterNth#(N, XS) -> mark# N,
                   a__afterNth#(N, XS) -> mark# XS,
                   a__afterNth#(N, XS) -> a__snd# a__splitAt(mark N, mark XS),
                      a__and#(tt(), X) -> mark# X,
                    a__fst# pair(X, Y) -> mark# X,
                  a__head# cons(N, XS) -> mark# N,
                        a__natsFrom# N -> mark# N,
                        a__sel#(N, XS) -> mark# N,
                        a__sel#(N, XS) -> mark# XS,
                        a__sel#(N, XS) -> a__afterNth#(mark N, mark XS),
                        a__sel#(N, XS) -> a__head# a__afterNth(mark N, mark XS),
                  a__tail# cons(N, XS) -> mark# XS,
                       a__take#(N, XS) -> a__splitAt#(mark N, mark XS),
                       a__take#(N, XS) -> mark# N,
                       a__take#(N, XS) -> mark# XS,
                       a__take#(N, XS) -> a__fst# a__splitAt(mark N, mark XS)}
       Weak:
       {              a__U12(X1, X2) -> U12(X1, X2),
             a__U12(pair(YS, ZS), X) -> pair(cons(mark X, YS), mark ZS),
                  a__splitAt(X1, X2) -> splitAt(X1, X2),
        a__splitAt(s N, cons(X, XS)) -> a__U11(tt(), N, X, XS),
                 a__splitAt(0(), XS) -> pair(nil(), mark XS),
                           mark tt() -> tt(),
                   mark pair(X1, X2) -> pair(mark X1, mark X2),
                   mark cons(X1, X2) -> cons(mark X1, X2),
                     mark natsFrom X -> a__natsFrom mark X,
                            mark s X -> s mark X,
                          mark nil() -> nil(),
                            mark 0() -> 0(),
            mark U11(X1, X2, X3, X4) -> a__U11(mark X1, X2, X3, X4),
                    mark U12(X1, X2) -> a__U12(mark X1, X2),
                mark splitAt(X1, X2) -> a__splitAt(mark X1, mark X2),
               mark afterNth(X1, X2) -> a__afterNth(mark X1, mark X2),
                          mark snd X -> a__snd mark X,
                    mark and(X1, X2) -> a__and(mark X1, X2),
                          mark fst X -> a__fst mark X,
                         mark head X -> a__head mark X,
                    mark sel(X1, X2) -> a__sel(mark X1, mark X2),
                         mark tail X -> a__tail mark X,
                   mark take(X1, X2) -> a__take(mark X1, mark X2),
              a__U11(X1, X2, X3, X4) -> U11(X1, X2, X3, X4),
              a__U11(tt(), N, X, XS) -> a__U12(a__splitAt(mark N, mark XS), X),
                            a__snd X -> snd X,
                   a__snd pair(X, Y) -> mark Y,
                  a__afterNth(N, XS) -> a__snd a__splitAt(mark N, mark XS),
                 a__afterNth(X1, X2) -> afterNth(X1, X2),
                      a__and(X1, X2) -> and(X1, X2),
                     a__and(tt(), X) -> mark X,
                            a__fst X -> fst X,
                   a__fst pair(X, Y) -> mark X,
                           a__head X -> head X,
                 a__head cons(N, XS) -> mark N,
                       a__natsFrom N -> cons(mark N, natsFrom s N),
                       a__natsFrom X -> natsFrom X,
                       a__sel(N, XS) -> a__head a__afterNth(mark N, mark XS),
                      a__sel(X1, X2) -> sel(X1, X2),
                           a__tail X -> tail X,
                 a__tail cons(N, XS) -> mark XS,
                      a__take(N, XS) -> a__fst a__splitAt(mark N, mark XS),
                     a__take(X1, X2) -> take(X1, X2)}
       Open