We consider universal computability of the STRS with no additional rule schemes:

  Signature: 0           :: A
             afterNth    :: A -> A -> A
             and         :: A -> A -> A
             axxafterNth :: A -> A -> A
             axxand      :: A -> A -> A
             axxfst      :: A -> A
             axxhead     :: A -> A
             axxnatsFrom :: A -> A
             axxsel      :: A -> A -> A
             axxsnd      :: A -> A
             axxsplitAt  :: A -> A -> A
             axxtail     :: A -> A
             axxtake     :: A -> A -> A
             axxu11      :: A -> A -> A -> A -> A
             axxu12      :: A -> A -> A
             cons        :: A -> A -> A
             fst         :: A -> A
             head        :: A -> A
             mark        :: A -> A
             natsFrom    :: A -> A
             nil         :: A
             pair        :: A -> A -> A
             s           :: A -> A
             sel         :: A -> A -> A
             snd         :: A -> A
             splitAt     :: A -> A -> A
             tail        :: A -> A
             take        :: A -> A -> A
             tt          :: A
             u11         :: A -> A -> A -> A -> A
             u12         :: A -> A -> A

  Rules: axxu11(tt, X, Y, U) -> axxu12(axxsplitAt(mark(X), mark(U)), Y)
         axxu12(pair(V, W), P) -> pair(cons(mark(P), V), mark(W))
         axxafterNth(X1, Y1) -> axxsnd(axxsplitAt(mark(X1), mark(Y1)))
         axxand(tt, U1) -> mark(U1)
         axxfst(pair(V1, W1)) -> mark(V1)
         axxhead(cons(P1, X2)) -> mark(P1)
         axxnatsFrom(Y2) -> cons(mark(Y2), natsFrom(s(Y2)))
         axxsel(U2, V2) -> axxhead(axxafterNth(mark(U2), mark(V2)))
         axxsnd(pair(W2, P2)) -> mark(P2)
         axxsplitAt(0, X3) -> pair(nil, mark(X3))
         axxsplitAt(s(Y3), cons(U3, V3)) -> axxu11(tt, Y3, U3, V3)
         axxtail(cons(W3, P3)) -> mark(P3)
         axxtake(X4, Y4) -> axxfst(axxsplitAt(mark(X4), mark(Y4)))
         mark(u11(U4, V4, W4, P4)) -> axxu11(mark(U4), V4, W4, P4)
         mark(u12(X5, Y5)) -> axxu12(mark(X5), Y5)
         mark(splitAt(U5, V5)) -> axxsplitAt(mark(U5), mark(V5))
         mark(afterNth(W5, P5)) -> axxafterNth(mark(W5), mark(P5))
         mark(snd(X6)) -> axxsnd(mark(X6))
         mark(and(Y6, U6)) -> axxand(mark(Y6), U6)
         mark(fst(V6)) -> axxfst(mark(V6))
         mark(head(W6)) -> axxhead(mark(W6))
         mark(natsFrom(P6)) -> axxnatsFrom(mark(P6))
         mark(sel(X7, Y7)) -> axxsel(mark(X7), mark(Y7))
         mark(tail(U7)) -> axxtail(mark(U7))
         mark(take(V7, W7)) -> axxtake(mark(V7), mark(W7))
         mark(tt) -> tt
         mark(pair(P7, X8)) -> pair(mark(P7), mark(X8))
         mark(cons(Y8, U8)) -> cons(mark(Y8), U8)
         mark(s(V8)) -> s(mark(V8))
         mark(0) -> 0
         mark(nil) -> nil
         axxu11(W8, P8, X9, Y9) -> u11(W8, P8, X9, Y9)
         axxu12(U9, V9) -> u12(U9, V9)
         axxsplitAt(W9, P9) -> splitAt(W9, P9)
         axxafterNth(X10, Y10) -> afterNth(X10, Y10)
         axxsnd(U10) -> snd(U10)
         axxand(V10, W10) -> and(V10, W10)
         axxfst(P10) -> fst(P10)
         axxhead(X11) -> head(X11)
         axxnatsFrom(Y11) -> natsFrom(Y11)
         axxsel(U11, V11) -> sel(U11, V11)
         axxtail(W11) -> tail(W11)
         axxtake(P11, X12) -> take(P11, X12)

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

We start by computing the initial DP problem D1 = (P1, R UNION R_?, f, c), where:

  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 D1 = (P1, R UNION R_?, f, c).