The system is accessible function passing by a sort ordering that equates all sorts.

We start by computing the following initial DP problem:

  P1. (1)  axxu11#(tt, X, Y, U) => mark#(X)
      (2)  axxu11#(tt, X, Y, U) => mark#(U)
      (3)  axxu11#(tt, X, Y, U) => axxsplitAt#(mark(X), mark(U))
      (4)  axxu11#(tt, X, Y, U) => axxu12#(axxsplitAt(mark(X), mark(U)), Y)
      (5)  axxu12#(pair(V, W), P) => mark#(P)
      (6)  axxu12#(pair(V, W), P) => mark#(W)
      (7)  axxafterNth#(X1, Y1) => mark#(X1)
      (8)  axxafterNth#(X1, Y1) => mark#(Y1)
      (9)  axxafterNth#(X1, Y1) => axxsplitAt#(mark(X1), mark(Y1))
      (10) axxafterNth#(X1, Y1) => axxsnd#(axxsplitAt(mark(X1), mark(Y1)))
      (11) axxand#(tt, U1) => mark#(U1)
      (12) axxfst#(pair(V1, W1)) => mark#(V1)
      (13) axxhead#(cons(P1, X2)) => mark#(P1)
      (14) axxnatsFrom#(Y2) => mark#(Y2)
      (15) axxsel#(U2, V2) => mark#(U2)
      (16) axxsel#(U2, V2) => mark#(V2)
      (17) axxsel#(U2, V2) => axxafterNth#(mark(U2), mark(V2))
      (18) axxsel#(U2, V2) => axxhead#(axxafterNth(mark(U2), mark(V2)))
      (19) axxsnd#(pair(W2, P2)) => mark#(P2)
      (20) axxsplitAt#(0, X3) => mark#(X3)
      (21) axxsplitAt#(s(Y3), cons(U3, V3)) => axxu11#(tt, Y3, U3, V3)
      (22) axxtail#(cons(W3, P3)) => mark#(P3)
      (23) axxtake#(X4, Y4) => mark#(X4)
      (24) axxtake#(X4, Y4) => mark#(Y4)
      (25) axxtake#(X4, Y4) => axxsplitAt#(mark(X4), mark(Y4))
      (26) axxtake#(X4, Y4) => axxfst#(axxsplitAt(mark(X4), mark(Y4)))
      (27) mark#(u11(U4, V4, W4, P4)) => mark#(U4)
      (28) mark#(u11(U4, V4, W4, P4)) => axxu11#(mark(U4), V4, W4, P4)
      (29) mark#(u12(X5, Y5)) => mark#(X5)
      (30) mark#(u12(X5, Y5)) => axxu12#(mark(X5), Y5)
      (31) mark#(splitAt(U5, V5)) => mark#(U5)
      (32) mark#(splitAt(U5, V5)) => mark#(V5)
      (33) mark#(splitAt(U5, V5)) => axxsplitAt#(mark(U5), mark(V5))
      (34) mark#(afterNth(W5, P5)) => mark#(W5)
      (35) mark#(afterNth(W5, P5)) => mark#(P5)
      (36) mark#(afterNth(W5, P5)) => axxafterNth#(mark(W5), mark(P5))
      (37) mark#(snd(X6)) => mark#(X6)
      (38) mark#(snd(X6)) => axxsnd#(mark(X6))
      (39) mark#(and(Y6, U6)) => mark#(Y6)
      (40) mark#(and(Y6, U6)) => axxand#(mark(Y6), U6)
      (41) mark#(fst(V6)) => mark#(V6)
      (42) mark#(fst(V6)) => axxfst#(mark(V6))
      (43) mark#(head(W6)) => mark#(W6)
      (44) mark#(head(W6)) => axxhead#(mark(W6))
      (45) mark#(natsFrom(P6)) => mark#(P6)
      (46) mark#(natsFrom(P6)) => axxnatsFrom#(mark(P6))
      (47) mark#(sel(X7, Y7)) => mark#(X7)
      (48) mark#(sel(X7, Y7)) => mark#(Y7)
      (49) mark#(sel(X7, Y7)) => axxsel#(mark(X7), mark(Y7))
      (50) mark#(tail(U7)) => mark#(U7)
      (51) mark#(tail(U7)) => axxtail#(mark(U7))
      (52) mark#(take(V7, W7)) => mark#(V7)
      (53) mark#(take(V7, W7)) => mark#(W7)
      (54) mark#(take(V7, W7)) => axxtake#(mark(V7), mark(W7))
      (55) mark#(pair(P7, X8)) => mark#(P7)
      (56) mark#(pair(P7, X8)) => mark#(X8)
      (57) mark#(cons(Y8, U8)) => mark#(Y8)
      (58) mark#(s(V8)) => mark#(V8)

***** No progress could be made on DP problem P1.