We consider the system h38.

  Alphabet:

    0 : [] --> A 
    active : [] --> A -> A 
    afterNth : [] --> A -> A -> A 
    and : [] --> A -> A -> A 
    app : [] --> (A -> A) -> A -> A 
    cons : [] --> A -> A -> A 
    fst : [] --> A -> A 
    head : [] --> A -> A 
    map : [] --> (A -> A) -> 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:

    active (u11 tt x y z) => mark (u12 (splitAt x z) y) 
    active (u12 (pair x y) z) => mark (pair (cons z x) y) 
    active (afterNth x y) => mark (snd (splitAt x y)) 
    active (and tt x) => mark x 
    active (fst (pair x y)) => mark x 
    active (head (cons x y)) => mark x 
    active (natsFrom x) => mark (cons x (natsFrom (s x))) 
    active (sel x y) => mark (head (afterNth x y)) 
    active (snd (pair x y)) => mark y 
    active (splitAt 0 x) => mark (pair nil x) 
    active (splitAt (s x) (cons y z)) => mark (u11 tt x y z) 
    active (tail (cons x y)) => mark y 
    active (take x y) => mark (fst (splitAt x y)) 
    mark (u11 x y z u) => active (u11 (mark x) y z u) 
    mark tt => active tt 
    mark (u12 x y) => active (u12 (mark x) y) 
    mark (splitAt x y) => active (splitAt (mark x) (mark y)) 
    mark (pair x y) => active (pair (mark x) (mark y)) 
    mark (cons x y) => active (cons (mark x) y) 
    mark (afterNth x y) => active (afterNth (mark x) (mark y)) 
    mark (snd x) => active (snd (mark x)) 
    mark (and x y) => active (and (mark x) y) 
    mark (fst x) => active (fst (mark x)) 
    mark (head x) => active (head (mark x)) 
    mark (natsFrom x) => active (natsFrom (mark x)) 
    mark (s x) => active (s (mark x)) 
    mark (sel x y) => active (sel (mark x) (mark y)) 
    mark 0 => active 0 
    mark nil => active nil 
    mark (tail x) => active (tail (mark x)) 
    mark (take x y) => active (take (mark x) (mark y)) 
    u11 (mark x) y z u => u11 x y z u 
    u11 x (mark y) z u => u11 x y z u 
    u11 x y (mark z) u => u11 x y z u 
    u11 x y z (mark u) => u11 x y z u 
    u11 (active x) y z u => u11 x y z u 
    u11 x (active y) z u => u11 x y z u 
    u11 x y (active z) u => u11 x y z u 
    u11 x y z (active u) => u11 x y z u 
    u12 (mark x) y => u12 x y 
    u12 x (mark y) => u12 x y 
    u12 (active x) y => u12 x y 
    u12 x (active y) => u12 x y 
    splitAt (mark x) y => splitAt x y 
    splitAt x (mark y) => splitAt x y 
    splitAt (active x) y => splitAt x y 
    splitAt x (active y) => splitAt x y 
    pair (mark x) y => pair x y 
    pair x (mark y) => pair x y 
    pair (active x) y => pair x y 
    pair x (active y) => pair x y 
    cons (mark x) y => cons x y 
    cons x (mark y) => cons x y 
    cons (active x) y => cons x y 
    cons x (active y) => cons x y 
    afterNth (mark x) y => afterNth x y 
    afterNth x (mark y) => afterNth x y 
    afterNth (active x) y => afterNth x y 
    afterNth x (active y) => afterNth x y 
    snd (mark x) => snd x 
    snd (active x) => snd x 
    and (mark x) y => and x y 
    and x (mark y) => and x y 
    and (active x) y => and x y 
    and x (active y) => and x y 
    fst (mark x) => fst x 
    fst (active x) => fst x 
    head (mark x) => head x 
    head (active x) => head x 
    natsFrom (mark x) => natsFrom x 
    natsFrom (active x) => natsFrom x 
    s (mark x) => s x 
    s (active x) => s x 
    sel (mark x) y => sel x y 
    sel x (mark y) => sel x y 
    sel (active x) y => sel x y 
    sel x (active y) => sel x y 
    tail (mark x) => tail x 
    tail (active x) => tail x 
    take (mark x) y => take x y 
    take x (mark y) => take x y 
    take (active x) y => take x y 
    take x (active y) => take x y 
    map (/\x.f x) nil => nil 
    map (/\x.f x) (cons y z) => cons (f y) (map (/\u.f u) z) 
    app (/\x.f x) y => f y 

Using the transformations described in [Kop11], this system can be brought in a form without leading free variables in the left-hand side, and where the left-hand side of a variable is always a functional term or application headed by a functional term.

We now transform the resulting AFS into an AFSM by replacing all free variables by meta-variables (with arity 0).  This leads to the following AFSM:

  Alphabet:

    0 : [] --> A 
    active : [A] --> A 
    afterNth : [A * A] --> A 
    and : [A * A] --> A 
    app : [A -> A * A] --> A 
    cons : [A * A] --> A 
    fst : [A] --> A 
    head : [A] --> A 
    map : [A -> A * 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 
    ~AP1 : [A -> A * A] --> A 

  Rules:

    active(u11(tt, X, Y, Z)) => mark(u12(splitAt(X, Z), Y)) 
    active(u12(pair(X, Y), Z)) => mark(pair(cons(Z, X), Y)) 
    active(afterNth(X, Y)) => mark(snd(splitAt(X, Y))) 
    active(and(tt, X)) => mark(X) 
    active(fst(pair(X, Y))) => mark(X) 
    active(head(cons(X, Y))) => mark(X) 
    active(natsFrom(X)) => mark(cons(X, natsFrom(s(X)))) 
    active(sel(X, Y)) => mark(head(afterNth(X, Y))) 
    active(snd(pair(X, Y))) => mark(Y) 
    active(splitAt(0, X)) => mark(pair(nil, X)) 
    active(splitAt(s(X), cons(Y, Z))) => mark(u11(tt, X, Y, Z)) 
    active(tail(cons(X, Y))) => mark(Y) 
    active(take(X, Y)) => mark(fst(splitAt(X, Y))) 
    mark(u11(X, Y, Z, U)) => active(u11(mark(X), Y, Z, U)) 
    mark(tt) => active(tt) 
    mark(u12(X, Y)) => active(u12(mark(X), Y)) 
    mark(splitAt(X, Y)) => active(splitAt(mark(X), mark(Y))) 
    mark(pair(X, Y)) => active(pair(mark(X), mark(Y))) 
    mark(cons(X, Y)) => active(cons(mark(X), Y)) 
    mark(afterNth(X, Y)) => active(afterNth(mark(X), mark(Y))) 
    mark(snd(X)) => active(snd(mark(X))) 
    mark(and(X, Y)) => active(and(mark(X), Y)) 
    mark(fst(X)) => active(fst(mark(X))) 
    mark(head(X)) => active(head(mark(X))) 
    mark(natsFrom(X)) => active(natsFrom(mark(X))) 
    mark(s(X)) => active(s(mark(X))) 
    mark(sel(X, Y)) => active(sel(mark(X), mark(Y))) 
    mark(0) => active(0) 
    mark(nil) => active(nil) 
    mark(tail(X)) => active(tail(mark(X))) 
    mark(take(X, Y)) => active(take(mark(X), mark(Y))) 
    u11(mark(X), Y, Z, U) => u11(X, Y, Z, U) 
    u11(X, mark(Y), Z, U) => u11(X, Y, Z, U) 
    u11(X, Y, mark(Z), U) => u11(X, Y, Z, U) 
    u11(X, Y, Z, mark(U)) => u11(X, Y, Z, U) 
    u11(active(X), Y, Z, U) => u11(X, Y, Z, U) 
    u11(X, active(Y), Z, U) => u11(X, Y, Z, U) 
    u11(X, Y, active(Z), U) => u11(X, Y, Z, U) 
    u11(X, Y, Z, active(U)) => u11(X, Y, Z, U) 
    u12(mark(X), Y) => u12(X, Y) 
    u12(X, mark(Y)) => u12(X, Y) 
    u12(active(X), Y) => u12(X, Y) 
    u12(X, active(Y)) => u12(X, Y) 
    splitAt(mark(X), Y) => splitAt(X, Y) 
    splitAt(X, mark(Y)) => splitAt(X, Y) 
    splitAt(active(X), Y) => splitAt(X, Y) 
    splitAt(X, active(Y)) => splitAt(X, Y) 
    pair(mark(X), Y) => pair(X, Y) 
    pair(X, mark(Y)) => pair(X, Y) 
    pair(active(X), Y) => pair(X, Y) 
    pair(X, active(Y)) => pair(X, Y) 
    cons(mark(X), Y) => cons(X, Y) 
    cons(X, mark(Y)) => cons(X, Y) 
    cons(active(X), Y) => cons(X, Y) 
    cons(X, active(Y)) => cons(X, Y) 
    afterNth(mark(X), Y) => afterNth(X, Y) 
    afterNth(X, mark(Y)) => afterNth(X, Y) 
    afterNth(active(X), Y) => afterNth(X, Y) 
    afterNth(X, active(Y)) => afterNth(X, Y) 
    snd(mark(X)) => snd(X) 
    snd(active(X)) => snd(X) 
    and(mark(X), Y) => and(X, Y) 
    and(X, mark(Y)) => and(X, Y) 
    and(active(X), Y) => and(X, Y) 
    and(X, active(Y)) => and(X, Y) 
    fst(mark(X)) => fst(X) 
    fst(active(X)) => fst(X) 
    head(mark(X)) => head(X) 
    head(active(X)) => head(X) 
    natsFrom(mark(X)) => natsFrom(X) 
    natsFrom(active(X)) => natsFrom(X) 
    s(mark(X)) => s(X) 
    s(active(X)) => s(X) 
    sel(mark(X), Y) => sel(X, Y) 
    sel(X, mark(Y)) => sel(X, Y) 
    sel(active(X), Y) => sel(X, Y) 
    sel(X, active(Y)) => sel(X, Y) 
    tail(mark(X)) => tail(X) 
    tail(active(X)) => tail(X) 
    take(mark(X), Y) => take(X, Y) 
    take(X, mark(Y)) => take(X, Y) 
    take(active(X), Y) => take(X, Y) 
    take(X, active(Y)) => take(X, Y) 
    map(/\x.~AP1(F, x), nil) => nil 
    map(/\x.~AP1(F, x), cons(X, Y)) => cons(~AP1(F, X), map(/\y.~AP1(F, y), Y)) 
    app(/\x.~AP1(F, x), X) => ~AP1(F, X) 
    map(/\x.active(x), nil) => nil 
    map(/\x.afterNth(X, x), nil) => nil 
    map(/\x.and(X, x), nil) => nil 
    map(/\x.app(F, x), nil) => nil 
    map(/\x.cons(X, x), nil) => nil 
    map(/\x.fst(x), nil) => nil 
    map(/\x.head(x), nil) => nil 
    map(/\x.map(F, x), nil) => nil 
    map(/\x.mark(x), nil) => nil 
    map(/\x.natsFrom(x), nil) => nil 
    map(/\x.pair(X, x), nil) => nil 
    map(/\x.s(x), nil) => nil 
    map(/\x.sel(X, x), nil) => nil 
    map(/\x.snd(x), nil) => nil 
    map(/\x.splitAt(X, x), nil) => nil 
    map(/\x.tail(x), nil) => nil 
    map(/\x.take(X, x), nil) => nil 
    map(/\x.u11(X, Y, Z, x), nil) => nil 
    map(/\x.u12(X, x), nil) => nil 
    map(/\x.active(x), cons(X, Y)) => cons(active(X), map(/\y.active(y), Y)) 
    map(/\x.afterNth(X, x), cons(Y, Z)) => cons(afterNth(X, Y), map(/\y.afterNth(X, y), Z)) 
    map(/\x.and(X, x), cons(Y, Z)) => cons(and(X, Y), map(/\y.and(X, y), Z)) 
    map(/\x.app(F, x), cons(X, Y)) => cons(app(F, X), map(/\y.app(F, y), Y)) 
    map(/\x.cons(X, x), cons(Y, Z)) => cons(cons(X, Y), map(/\y.cons(X, y), Z)) 
    map(/\x.fst(x), cons(X, Y)) => cons(fst(X), map(/\y.fst(y), Y)) 
    map(/\x.head(x), cons(X, Y)) => cons(head(X), map(/\y.head(y), Y)) 
    map(/\x.map(F, x), cons(X, Y)) => cons(map(F, X), map(/\y.map(F, y), Y)) 
    map(/\x.mark(x), cons(X, Y)) => cons(mark(X), map(/\y.mark(y), Y)) 
    map(/\x.natsFrom(x), cons(X, Y)) => cons(natsFrom(X), map(/\y.natsFrom(y), Y)) 
    map(/\x.pair(X, x), cons(Y, Z)) => cons(pair(X, Y), map(/\y.pair(X, y), Z)) 
    map(/\x.s(x), cons(X, Y)) => cons(s(X), map(/\y.s(y), Y)) 
    map(/\x.sel(X, x), cons(Y, Z)) => cons(sel(X, Y), map(/\y.sel(X, y), Z)) 
    map(/\x.snd(x), cons(X, Y)) => cons(snd(X), map(/\y.snd(y), Y)) 
    map(/\x.splitAt(X, x), cons(Y, Z)) => cons(splitAt(X, Y), map(/\y.splitAt(X, y), Z)) 
    map(/\x.tail(x), cons(X, Y)) => cons(tail(X), map(/\y.tail(y), Y)) 
    map(/\x.take(X, x), cons(Y, Z)) => cons(take(X, Y), map(/\y.take(X, y), Z)) 
    map(/\x.u11(X, Y, Z, x), cons(U, V)) => cons(u11(X, Y, Z, U), map(/\y.u11(X, Y, Z, y), V)) 
    map(/\x.u12(X, x), cons(Y, Z)) => cons(u12(X, Y), map(/\y.u12(X, y), Z)) 
    app(/\x.active(x), X) => active(X) 
    app(/\x.afterNth(X, x), Y) => afterNth(X, Y) 
    app(/\x.and(X, x), Y) => and(X, Y) 
    app(/\x.app(F, x), X) => app(F, X) 
    app(/\x.cons(X, x), Y) => cons(X, Y) 
    app(/\x.fst(x), X) => fst(X) 
    app(/\x.head(x), X) => head(X) 
    app(/\x.map(F, x), X) => map(F, X) 
    app(/\x.mark(x), X) => mark(X) 
    app(/\x.natsFrom(x), X) => natsFrom(X) 
    app(/\x.pair(X, x), Y) => pair(X, Y) 
    app(/\x.s(x), X) => s(X) 
    app(/\x.sel(X, x), Y) => sel(X, Y) 
    app(/\x.snd(x), X) => snd(X) 
    app(/\x.splitAt(X, x), Y) => splitAt(X, Y) 
    app(/\x.tail(x), X) => tail(X) 
    app(/\x.take(X, x), Y) => take(X, Y) 
    app(/\x.u11(X, Y, Z, x), U) => u11(X, Y, Z, U) 
    app(/\x.u12(X, x), Y) => u12(X, Y) 
    ~AP1(F, X) => F X 

Symbol ~AP1 is an encoding for application that is only used in innocuous ways.  We can simplify the program (without losing non-termination) by removing it.  Additionally, we can remove some (now-)redundant rules.  This gives:

  Alphabet:

    0 : [] --> A 
    active : [A] --> A 
    afterNth : [A * A] --> A 
    and : [A * A] --> A 
    app : [A -> A * A] --> A 
    cons : [A * A] --> A 
    fst : [A] --> A 
    head : [A] --> A 
    map : [A -> A * 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:

    active(u11(tt, X, Y, Z)) => mark(u12(splitAt(X, Z), Y)) 
    active(u12(pair(X, Y), Z)) => mark(pair(cons(Z, X), Y)) 
    active(afterNth(X, Y)) => mark(snd(splitAt(X, Y))) 
    active(and(tt, X)) => mark(X) 
    active(fst(pair(X, Y))) => mark(X) 
    active(head(cons(X, Y))) => mark(X) 
    active(natsFrom(X)) => mark(cons(X, natsFrom(s(X)))) 
    active(sel(X, Y)) => mark(head(afterNth(X, Y))) 
    active(snd(pair(X, Y))) => mark(Y) 
    active(splitAt(0, X)) => mark(pair(nil, X)) 
    active(splitAt(s(X), cons(Y, Z))) => mark(u11(tt, X, Y, Z)) 
    active(tail(cons(X, Y))) => mark(Y) 
    active(take(X, Y)) => mark(fst(splitAt(X, Y))) 
    mark(u11(X, Y, Z, U)) => active(u11(mark(X), Y, Z, U)) 
    mark(tt) => active(tt) 
    mark(u12(X, Y)) => active(u12(mark(X), Y)) 
    mark(splitAt(X, Y)) => active(splitAt(mark(X), mark(Y))) 
    mark(pair(X, Y)) => active(pair(mark(X), mark(Y))) 
    mark(cons(X, Y)) => active(cons(mark(X), Y)) 
    mark(afterNth(X, Y)) => active(afterNth(mark(X), mark(Y))) 
    mark(snd(X)) => active(snd(mark(X))) 
    mark(and(X, Y)) => active(and(mark(X), Y)) 
    mark(fst(X)) => active(fst(mark(X))) 
    mark(head(X)) => active(head(mark(X))) 
    mark(natsFrom(X)) => active(natsFrom(mark(X))) 
    mark(s(X)) => active(s(mark(X))) 
    mark(sel(X, Y)) => active(sel(mark(X), mark(Y))) 
    mark(0) => active(0) 
    mark(nil) => active(nil) 
    mark(tail(X)) => active(tail(mark(X))) 
    mark(take(X, Y)) => active(take(mark(X), mark(Y))) 
    u11(mark(X), Y, Z, U) => u11(X, Y, Z, U) 
    u11(X, mark(Y), Z, U) => u11(X, Y, Z, U) 
    u11(X, Y, mark(Z), U) => u11(X, Y, Z, U) 
    u11(X, Y, Z, mark(U)) => u11(X, Y, Z, U) 
    u11(active(X), Y, Z, U) => u11(X, Y, Z, U) 
    u11(X, active(Y), Z, U) => u11(X, Y, Z, U) 
    u11(X, Y, active(Z), U) => u11(X, Y, Z, U) 
    u11(X, Y, Z, active(U)) => u11(X, Y, Z, U) 
    u12(mark(X), Y) => u12(X, Y) 
    u12(X, mark(Y)) => u12(X, Y) 
    u12(active(X), Y) => u12(X, Y) 
    u12(X, active(Y)) => u12(X, Y) 
    splitAt(mark(X), Y) => splitAt(X, Y) 
    splitAt(X, mark(Y)) => splitAt(X, Y) 
    splitAt(active(X), Y) => splitAt(X, Y) 
    splitAt(X, active(Y)) => splitAt(X, Y) 
    pair(mark(X), Y) => pair(X, Y) 
    pair(X, mark(Y)) => pair(X, Y) 
    pair(active(X), Y) => pair(X, Y) 
    pair(X, active(Y)) => pair(X, Y) 
    cons(mark(X), Y) => cons(X, Y) 
    cons(X, mark(Y)) => cons(X, Y) 
    cons(active(X), Y) => cons(X, Y) 
    cons(X, active(Y)) => cons(X, Y) 
    afterNth(mark(X), Y) => afterNth(X, Y) 
    afterNth(X, mark(Y)) => afterNth(X, Y) 
    afterNth(active(X), Y) => afterNth(X, Y) 
    afterNth(X, active(Y)) => afterNth(X, Y) 
    snd(mark(X)) => snd(X) 
    snd(active(X)) => snd(X) 
    and(mark(X), Y) => and(X, Y) 
    and(X, mark(Y)) => and(X, Y) 
    and(active(X), Y) => and(X, Y) 
    and(X, active(Y)) => and(X, Y) 
    fst(mark(X)) => fst(X) 
    fst(active(X)) => fst(X) 
    head(mark(X)) => head(X) 
    head(active(X)) => head(X) 
    natsFrom(mark(X)) => natsFrom(X) 
    natsFrom(active(X)) => natsFrom(X) 
    s(mark(X)) => s(X) 
    s(active(X)) => s(X) 
    sel(mark(X), Y) => sel(X, Y) 
    sel(X, mark(Y)) => sel(X, Y) 
    sel(active(X), Y) => sel(X, Y) 
    sel(X, active(Y)) => sel(X, Y) 
    tail(mark(X)) => tail(X) 
    tail(active(X)) => tail(X) 
    take(mark(X), Y) => take(X, Y) 
    take(X, mark(Y)) => take(X, Y) 
    take(active(X), Y) => take(X, Y) 
    take(X, active(Y)) => take(X, Y) 
    map(/\x.X(x), nil) => nil 
    map(/\x.X(x), cons(Y, Z)) => cons(X(Y), map(/\y.X(y), Z)) 
    app(/\x.X(x), Y) => X(Y) 

We observe that the rules contain a first-order subset:

  active(u11(tt, X, Y, Z)) => mark(u12(splitAt(X, Z), Y)) 
  active(u12(pair(X, Y), Z)) => mark(pair(cons(Z, X), Y)) 
  active(afterNth(X, Y)) => mark(snd(splitAt(X, Y))) 
  active(and(tt, X)) => mark(X) 
  active(fst(pair(X, Y))) => mark(X) 
  active(head(cons(X, Y))) => mark(X) 
  active(natsFrom(X)) => mark(cons(X, natsFrom(s(X)))) 
  active(sel(X, Y)) => mark(head(afterNth(X, Y))) 
  active(snd(pair(X, Y))) => mark(Y) 
  active(splitAt(0, X)) => mark(pair(nil, X)) 
  active(splitAt(s(X), cons(Y, Z))) => mark(u11(tt, X, Y, Z)) 
  active(tail(cons(X, Y))) => mark(Y) 
  active(take(X, Y)) => mark(fst(splitAt(X, Y))) 
  mark(u11(X, Y, Z, U)) => active(u11(mark(X), Y, Z, U)) 
  mark(tt) => active(tt) 
  mark(u12(X, Y)) => active(u12(mark(X), Y)) 
  mark(splitAt(X, Y)) => active(splitAt(mark(X), mark(Y))) 
  mark(pair(X, Y)) => active(pair(mark(X), mark(Y))) 
  mark(cons(X, Y)) => active(cons(mark(X), Y)) 
  mark(afterNth(X, Y)) => active(afterNth(mark(X), mark(Y))) 
  mark(snd(X)) => active(snd(mark(X))) 
  mark(and(X, Y)) => active(and(mark(X), Y)) 
  mark(fst(X)) => active(fst(mark(X))) 
  mark(head(X)) => active(head(mark(X))) 
  mark(natsFrom(X)) => active(natsFrom(mark(X))) 
  mark(s(X)) => active(s(mark(X))) 
  mark(sel(X, Y)) => active(sel(mark(X), mark(Y))) 
  mark(0) => active(0) 
  mark(nil) => active(nil) 
  mark(tail(X)) => active(tail(mark(X))) 
  mark(take(X, Y)) => active(take(mark(X), mark(Y))) 
  u11(mark(X), Y, Z, U) => u11(X, Y, Z, U) 
  u11(X, mark(Y), Z, U) => u11(X, Y, Z, U) 
  u11(X, Y, mark(Z), U) => u11(X, Y, Z, U) 
  u11(X, Y, Z, mark(U)) => u11(X, Y, Z, U) 
  u11(active(X), Y, Z, U) => u11(X, Y, Z, U) 
  u11(X, active(Y), Z, U) => u11(X, Y, Z, U) 
  u11(X, Y, active(Z), U) => u11(X, Y, Z, U) 
  u11(X, Y, Z, active(U)) => u11(X, Y, Z, U) 
  u12(mark(X), Y) => u12(X, Y) 
  u12(X, mark(Y)) => u12(X, Y) 
  u12(active(X), Y) => u12(X, Y) 
  u12(X, active(Y)) => u12(X, Y) 
  splitAt(mark(X), Y) => splitAt(X, Y) 
  splitAt(X, mark(Y)) => splitAt(X, Y) 
  splitAt(active(X), Y) => splitAt(X, Y) 
  splitAt(X, active(Y)) => splitAt(X, Y) 
  pair(mark(X), Y) => pair(X, Y) 
  pair(X, mark(Y)) => pair(X, Y) 
  pair(active(X), Y) => pair(X, Y) 
  pair(X, active(Y)) => pair(X, Y) 
  cons(mark(X), Y) => cons(X, Y) 
  cons(X, mark(Y)) => cons(X, Y) 
  cons(active(X), Y) => cons(X, Y) 
  cons(X, active(Y)) => cons(X, Y) 
  afterNth(mark(X), Y) => afterNth(X, Y) 
  afterNth(X, mark(Y)) => afterNth(X, Y) 
  afterNth(active(X), Y) => afterNth(X, Y) 
  afterNth(X, active(Y)) => afterNth(X, Y) 
  snd(mark(X)) => snd(X) 
  snd(active(X)) => snd(X) 
  and(mark(X), Y) => and(X, Y) 
  and(X, mark(Y)) => and(X, Y) 
  and(active(X), Y) => and(X, Y) 
  and(X, active(Y)) => and(X, Y) 
  fst(mark(X)) => fst(X) 
  fst(active(X)) => fst(X) 
  head(mark(X)) => head(X) 
  head(active(X)) => head(X) 
  natsFrom(mark(X)) => natsFrom(X) 
  natsFrom(active(X)) => natsFrom(X) 
  s(mark(X)) => s(X) 
  s(active(X)) => s(X) 
  sel(mark(X), Y) => sel(X, Y) 
  sel(X, mark(Y)) => sel(X, Y) 
  sel(active(X), Y) => sel(X, Y) 
  sel(X, active(Y)) => sel(X, Y) 
  tail(mark(X)) => tail(X) 
  tail(active(X)) => tail(X) 
  take(mark(X), Y) => take(X, Y) 
  take(X, mark(Y)) => take(X, Y) 
  take(active(X), Y) => take(X, Y) 
  take(X, active(Y)) => take(X, Y) 

Moreover, the system is finitely branching.  Thus, by [Kop12, Thm. 7.55], we may omit all first-order dependency pairs from the dependency pair problem (DP(R), R) if this first-order part is Ce-terminating when seen as a many-sorted first-order TRS.

According to nattprover, this system is indeed Ce-terminating:

 || Input TRS:
 ||     1: active(u11(tt(),PeRCenTX,PeRCenTY,PeRCenTZ)) -> mark(u12(splitAt(PeRCenTX,PeRCenTZ),PeRCenTY))
 ||     2: active(u12(pair(PeRCenTX,PeRCenTY),PeRCenTZ)) -> mark(pair(cons(PeRCenTZ,PeRCenTX),PeRCenTY))
 ||     3: active(afterNth(PeRCenTX,PeRCenTY)) -> mark(snd(splitAt(PeRCenTX,PeRCenTY)))
 ||     4: active(and(tt(),PeRCenTX)) -> mark(PeRCenTX)
 ||     5: active(fst(pair(PeRCenTX,PeRCenTY))) -> mark(PeRCenTX)
 ||     6: active(head(cons(PeRCenTX,PeRCenTY))) -> mark(PeRCenTX)
 ||     7: active(natsFrom(PeRCenTX)) -> mark(cons(PeRCenTX,natsFrom(s(PeRCenTX))))
 ||     8: active(sel(PeRCenTX,PeRCenTY)) -> mark(head(afterNth(PeRCenTX,PeRCenTY)))
 ||     9: active(snd(pair(PeRCenTX,PeRCenTY))) -> mark(PeRCenTY)
 ||     10: active(splitAt(0(),PeRCenTX)) -> mark(pair(nil(),PeRCenTX))
 ||     11: active(splitAt(s(PeRCenTX),cons(PeRCenTY,PeRCenTZ))) -> mark(u11(tt(),PeRCenTX,PeRCenTY,PeRCenTZ))
 ||     12: active(tail(cons(PeRCenTX,PeRCenTY))) -> mark(PeRCenTY)
 ||     13: active(take(PeRCenTX,PeRCenTY)) -> mark(fst(splitAt(PeRCenTX,PeRCenTY)))
 ||     14: mark(u11(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> active(u11(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU))
 ||     15: mark(tt()) -> active(tt())
 ||     16: mark(u12(PeRCenTX,PeRCenTY)) -> active(u12(mark(PeRCenTX),PeRCenTY))
 ||     17: mark(splitAt(PeRCenTX,PeRCenTY)) -> active(splitAt(mark(PeRCenTX),mark(PeRCenTY)))
 ||     18: mark(pair(PeRCenTX,PeRCenTY)) -> active(pair(mark(PeRCenTX),mark(PeRCenTY)))
 ||     19: mark(cons(PeRCenTX,PeRCenTY)) -> active(cons(mark(PeRCenTX),PeRCenTY))
 ||     20: mark(afterNth(PeRCenTX,PeRCenTY)) -> active(afterNth(mark(PeRCenTX),mark(PeRCenTY)))
 ||     21: mark(snd(PeRCenTX)) -> active(snd(mark(PeRCenTX)))
 ||     22: mark(and(PeRCenTX,PeRCenTY)) -> active(and(mark(PeRCenTX),PeRCenTY))
 ||     23: mark(fst(PeRCenTX)) -> active(fst(mark(PeRCenTX)))
 ||     24: mark(head(PeRCenTX)) -> active(head(mark(PeRCenTX)))
 ||     25: mark(natsFrom(PeRCenTX)) -> active(natsFrom(mark(PeRCenTX)))
 ||     26: mark(s(PeRCenTX)) -> active(s(mark(PeRCenTX)))
 ||     27: mark(sel(PeRCenTX,PeRCenTY)) -> active(sel(mark(PeRCenTX),mark(PeRCenTY)))
 ||     28: mark(0()) -> active(0())
 ||     29: mark(nil()) -> active(nil())
 ||     30: mark(tail(PeRCenTX)) -> active(tail(mark(PeRCenTX)))
 ||     31: mark(take(PeRCenTX,PeRCenTY)) -> active(take(mark(PeRCenTX),mark(PeRCenTY)))
 ||     32: u11(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU) -> u11(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||     33: u11(PeRCenTX,mark(PeRCenTY),PeRCenTZ,PeRCenTU) -> u11(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||     34: u11(PeRCenTX,PeRCenTY,mark(PeRCenTZ),PeRCenTU) -> u11(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||     35: u11(PeRCenTX,PeRCenTY,PeRCenTZ,mark(PeRCenTU)) -> u11(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||     36: u11(active(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU) -> u11(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||     37: u11(PeRCenTX,active(PeRCenTY),PeRCenTZ,PeRCenTU) -> u11(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||     38: u11(PeRCenTX,PeRCenTY,active(PeRCenTZ),PeRCenTU) -> u11(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||     39: u11(PeRCenTX,PeRCenTY,PeRCenTZ,active(PeRCenTU)) -> u11(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||     40: u12(mark(PeRCenTX),PeRCenTY) -> u12(PeRCenTX,PeRCenTY)
 ||     41: u12(PeRCenTX,mark(PeRCenTY)) -> u12(PeRCenTX,PeRCenTY)
 ||     42: u12(active(PeRCenTX),PeRCenTY) -> u12(PeRCenTX,PeRCenTY)
 ||     43: u12(PeRCenTX,active(PeRCenTY)) -> u12(PeRCenTX,PeRCenTY)
 ||     44: splitAt(mark(PeRCenTX),PeRCenTY) -> splitAt(PeRCenTX,PeRCenTY)
 ||     45: splitAt(PeRCenTX,mark(PeRCenTY)) -> splitAt(PeRCenTX,PeRCenTY)
 ||     46: splitAt(active(PeRCenTX),PeRCenTY) -> splitAt(PeRCenTX,PeRCenTY)
 ||     47: splitAt(PeRCenTX,active(PeRCenTY)) -> splitAt(PeRCenTX,PeRCenTY)
 ||     48: pair(mark(PeRCenTX),PeRCenTY) -> pair(PeRCenTX,PeRCenTY)
 ||     49: pair(PeRCenTX,mark(PeRCenTY)) -> pair(PeRCenTX,PeRCenTY)
 ||     50: pair(active(PeRCenTX),PeRCenTY) -> pair(PeRCenTX,PeRCenTY)
 ||     51: pair(PeRCenTX,active(PeRCenTY)) -> pair(PeRCenTX,PeRCenTY)
 ||     52: cons(mark(PeRCenTX),PeRCenTY) -> cons(PeRCenTX,PeRCenTY)
 ||     53: cons(PeRCenTX,mark(PeRCenTY)) -> cons(PeRCenTX,PeRCenTY)
 ||     54: cons(active(PeRCenTX),PeRCenTY) -> cons(PeRCenTX,PeRCenTY)
 ||     55: cons(PeRCenTX,active(PeRCenTY)) -> cons(PeRCenTX,PeRCenTY)
 ||     56: afterNth(mark(PeRCenTX),PeRCenTY) -> afterNth(PeRCenTX,PeRCenTY)
 ||     57: afterNth(PeRCenTX,mark(PeRCenTY)) -> afterNth(PeRCenTX,PeRCenTY)
 ||     58: afterNth(active(PeRCenTX),PeRCenTY) -> afterNth(PeRCenTX,PeRCenTY)
 ||     59: afterNth(PeRCenTX,active(PeRCenTY)) -> afterNth(PeRCenTX,PeRCenTY)
 ||     60: snd(mark(PeRCenTX)) -> snd(PeRCenTX)
 ||     61: snd(active(PeRCenTX)) -> snd(PeRCenTX)
 ||     62: and(mark(PeRCenTX),PeRCenTY) -> and(PeRCenTX,PeRCenTY)
 ||     63: and(PeRCenTX,mark(PeRCenTY)) -> and(PeRCenTX,PeRCenTY)
 ||     64: and(active(PeRCenTX),PeRCenTY) -> and(PeRCenTX,PeRCenTY)
 ||     65: and(PeRCenTX,active(PeRCenTY)) -> and(PeRCenTX,PeRCenTY)
 ||     66: fst(mark(PeRCenTX)) -> fst(PeRCenTX)
 ||     67: fst(active(PeRCenTX)) -> fst(PeRCenTX)
 ||     68: head(mark(PeRCenTX)) -> head(PeRCenTX)
 ||     69: head(active(PeRCenTX)) -> head(PeRCenTX)
 ||     70: natsFrom(mark(PeRCenTX)) -> natsFrom(PeRCenTX)
 ||     71: natsFrom(active(PeRCenTX)) -> natsFrom(PeRCenTX)
 ||     72: s(mark(PeRCenTX)) -> s(PeRCenTX)
 ||     73: s(active(PeRCenTX)) -> s(PeRCenTX)
 ||     74: sel(mark(PeRCenTX),PeRCenTY) -> sel(PeRCenTX,PeRCenTY)
 ||     75: sel(PeRCenTX,mark(PeRCenTY)) -> sel(PeRCenTX,PeRCenTY)
 ||     76: sel(active(PeRCenTX),PeRCenTY) -> sel(PeRCenTX,PeRCenTY)
 ||     77: sel(PeRCenTX,active(PeRCenTY)) -> sel(PeRCenTX,PeRCenTY)
 ||     78: tail(mark(PeRCenTX)) -> tail(PeRCenTX)
 ||     79: tail(active(PeRCenTX)) -> tail(PeRCenTX)
 ||     80: take(mark(PeRCenTX),PeRCenTY) -> take(PeRCenTX,PeRCenTY)
 ||     81: take(PeRCenTX,mark(PeRCenTY)) -> take(PeRCenTX,PeRCenTY)
 ||     82: take(active(PeRCenTX),PeRCenTY) -> take(PeRCenTX,PeRCenTY)
 ||     83: take(PeRCenTX,active(PeRCenTY)) -> take(PeRCenTX,PeRCenTY)
 ||     84: TIlDePAIR(PeRCenTX,PeRCenTY) -> PeRCenTX
 ||     85: TIlDePAIR(PeRCenTX,PeRCenTY) -> PeRCenTY
 || Number of strict rules: 85
 || Direct POLO(bPol) ... failed.
 || Uncurrying ... failed.
 || Dependency Pairs:
 ||    #1: #active(u12(pair(PeRCenTX,PeRCenTY),PeRCenTZ)) -> #mark(pair(cons(PeRCenTZ,PeRCenTX),PeRCenTY))
 ||    #2: #active(u12(pair(PeRCenTX,PeRCenTY),PeRCenTZ)) -> #pair(cons(PeRCenTZ,PeRCenTX),PeRCenTY)
 ||    #3: #active(u12(pair(PeRCenTX,PeRCenTY),PeRCenTZ)) -> #cons(PeRCenTZ,PeRCenTX)
 ||    #4: #u12(PeRCenTX,active(PeRCenTY)) -> #u12(PeRCenTX,PeRCenTY)
 ||    #5: #mark(nil()) -> #active(nil())
 ||    #6: #u11(PeRCenTX,PeRCenTY,PeRCenTZ,mark(PeRCenTU)) -> #u11(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||    #7: #take(PeRCenTX,active(PeRCenTY)) -> #take(PeRCenTX,PeRCenTY)
 ||    #8: #fst(mark(PeRCenTX)) -> #fst(PeRCenTX)
 ||    #9: #splitAt(active(PeRCenTX),PeRCenTY) -> #splitAt(PeRCenTX,PeRCenTY)
 ||    #10: #u12(active(PeRCenTX),PeRCenTY) -> #u12(PeRCenTX,PeRCenTY)
 ||    #11: #u12(PeRCenTX,mark(PeRCenTY)) -> #u12(PeRCenTX,PeRCenTY)
 ||    #12: #u11(PeRCenTX,active(PeRCenTY),PeRCenTZ,PeRCenTU) -> #u11(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||    #13: #s(active(PeRCenTX)) -> #s(PeRCenTX)
 ||    #14: #splitAt(PeRCenTX,active(PeRCenTY)) -> #splitAt(PeRCenTX,PeRCenTY)
 ||    #15: #cons(PeRCenTX,mark(PeRCenTY)) -> #cons(PeRCenTX,PeRCenTY)
 ||    #16: #natsFrom(active(PeRCenTX)) -> #natsFrom(PeRCenTX)
 ||    #17: #pair(mark(PeRCenTX),PeRCenTY) -> #pair(PeRCenTX,PeRCenTY)
 ||    #18: #sel(PeRCenTX,mark(PeRCenTY)) -> #sel(PeRCenTX,PeRCenTY)
 ||    #19: #sel(mark(PeRCenTX),PeRCenTY) -> #sel(PeRCenTX,PeRCenTY)
 ||    #20: #afterNth(active(PeRCenTX),PeRCenTY) -> #afterNth(PeRCenTX,PeRCenTY)
 ||    #21: #snd(active(PeRCenTX)) -> #snd(PeRCenTX)
 ||    #22: #u11(PeRCenTX,PeRCenTY,active(PeRCenTZ),PeRCenTU) -> #u11(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||    #23: #active(head(cons(PeRCenTX,PeRCenTY))) -> #mark(PeRCenTX)
 ||    #24: #afterNth(PeRCenTX,active(PeRCenTY)) -> #afterNth(PeRCenTX,PeRCenTY)
 ||    #25: #cons(PeRCenTX,active(PeRCenTY)) -> #cons(PeRCenTX,PeRCenTY)
 ||    #26: #fst(active(PeRCenTX)) -> #fst(PeRCenTX)
 ||    #27: #u12(mark(PeRCenTX),PeRCenTY) -> #u12(PeRCenTX,PeRCenTY)
 ||    #28: #pair(PeRCenTX,active(PeRCenTY)) -> #pair(PeRCenTX,PeRCenTY)
 ||    #29: #active(take(PeRCenTX,PeRCenTY)) -> #mark(fst(splitAt(PeRCenTX,PeRCenTY)))
 ||    #30: #active(take(PeRCenTX,PeRCenTY)) -> #fst(splitAt(PeRCenTX,PeRCenTY))
 ||    #31: #active(take(PeRCenTX,PeRCenTY)) -> #splitAt(PeRCenTX,PeRCenTY)
 ||    #32: #active(snd(pair(PeRCenTX,PeRCenTY))) -> #mark(PeRCenTY)
 ||    #33: #active(splitAt(s(PeRCenTX),cons(PeRCenTY,PeRCenTZ))) -> #mark(u11(tt(),PeRCenTX,PeRCenTY,PeRCenTZ))
 ||    #34: #active(splitAt(s(PeRCenTX),cons(PeRCenTY,PeRCenTZ))) -> #u11(tt(),PeRCenTX,PeRCenTY,PeRCenTZ)
 ||    #35: #afterNth(PeRCenTX,mark(PeRCenTY)) -> #afterNth(PeRCenTX,PeRCenTY)
 ||    #36: #sel(active(PeRCenTX),PeRCenTY) -> #sel(PeRCenTX,PeRCenTY)
 ||    #37: #mark(head(PeRCenTX)) -> #active(head(mark(PeRCenTX)))
 ||    #38: #mark(head(PeRCenTX)) -> #head(mark(PeRCenTX))
 ||    #39: #mark(head(PeRCenTX)) -> #mark(PeRCenTX)
 ||    #40: #natsFrom(mark(PeRCenTX)) -> #natsFrom(PeRCenTX)
 ||    #41: #mark(fst(PeRCenTX)) -> #active(fst(mark(PeRCenTX)))
 ||    #42: #mark(fst(PeRCenTX)) -> #fst(mark(PeRCenTX))
 ||    #43: #mark(fst(PeRCenTX)) -> #mark(PeRCenTX)
 ||    #44: #take(PeRCenTX,mark(PeRCenTY)) -> #take(PeRCenTX,PeRCenTY)
 ||    #45: #tail(mark(PeRCenTX)) -> #tail(PeRCenTX)
 ||    #46: #splitAt(PeRCenTX,mark(PeRCenTY)) -> #splitAt(PeRCenTX,PeRCenTY)
 ||    #47: #head(active(PeRCenTX)) -> #head(PeRCenTX)
 ||    #48: #active(tail(cons(PeRCenTX,PeRCenTY))) -> #mark(PeRCenTY)
 ||    #49: #mark(take(PeRCenTX,PeRCenTY)) -> #active(take(mark(PeRCenTX),mark(PeRCenTY)))
 ||    #50: #mark(take(PeRCenTX,PeRCenTY)) -> #take(mark(PeRCenTX),mark(PeRCenTY))
 ||    #51: #mark(take(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #52: #mark(take(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY)
 ||    #53: #tail(active(PeRCenTX)) -> #tail(PeRCenTX)
 ||    #54: #afterNth(mark(PeRCenTX),PeRCenTY) -> #afterNth(PeRCenTX,PeRCenTY)
 ||    #55: #take(active(PeRCenTX),PeRCenTY) -> #take(PeRCenTX,PeRCenTY)
 ||    #56: #mark(u11(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> #active(u11(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU))
 ||    #57: #mark(u11(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> #u11(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU)
 ||    #58: #mark(u11(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> #mark(PeRCenTX)
 ||    #59: #and(mark(PeRCenTX),PeRCenTY) -> #and(PeRCenTX,PeRCenTY)
 ||    #60: #mark(tail(PeRCenTX)) -> #active(tail(mark(PeRCenTX)))
 ||    #61: #mark(tail(PeRCenTX)) -> #tail(mark(PeRCenTX))
 ||    #62: #mark(tail(PeRCenTX)) -> #mark(PeRCenTX)
 ||    #63: #cons(mark(PeRCenTX),PeRCenTY) -> #cons(PeRCenTX,PeRCenTY)
 ||    #64: #pair(PeRCenTX,mark(PeRCenTY)) -> #pair(PeRCenTX,PeRCenTY)
 ||    #65: #mark(natsFrom(PeRCenTX)) -> #active(natsFrom(mark(PeRCenTX)))
 ||    #66: #mark(natsFrom(PeRCenTX)) -> #natsFrom(mark(PeRCenTX))
 ||    #67: #mark(natsFrom(PeRCenTX)) -> #mark(PeRCenTX)
 ||    #68: #mark(afterNth(PeRCenTX,PeRCenTY)) -> #active(afterNth(mark(PeRCenTX),mark(PeRCenTY)))
 ||    #69: #mark(afterNth(PeRCenTX,PeRCenTY)) -> #afterNth(mark(PeRCenTX),mark(PeRCenTY))
 ||    #70: #mark(afterNth(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #71: #mark(afterNth(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY)
 ||    #72: #active(natsFrom(PeRCenTX)) -> #mark(cons(PeRCenTX,natsFrom(s(PeRCenTX))))
 ||    #73: #active(natsFrom(PeRCenTX)) -> #cons(PeRCenTX,natsFrom(s(PeRCenTX)))
 ||    #74: #active(natsFrom(PeRCenTX)) -> #natsFrom(s(PeRCenTX))
 ||    #75: #active(natsFrom(PeRCenTX)) -> #s(PeRCenTX)
 ||    #76: #u11(PeRCenTX,PeRCenTY,PeRCenTZ,active(PeRCenTU)) -> #u11(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||    #77: #active(splitAt(0(),PeRCenTX)) -> #mark(pair(nil(),PeRCenTX))
 ||    #78: #active(splitAt(0(),PeRCenTX)) -> #pair(nil(),PeRCenTX)
 ||    #79: #and(active(PeRCenTX),PeRCenTY) -> #and(PeRCenTX,PeRCenTY)
 ||    #80: #u11(PeRCenTX,mark(PeRCenTY),PeRCenTZ,PeRCenTU) -> #u11(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||    #81: #s(mark(PeRCenTX)) -> #s(PeRCenTX)
 ||    #82: #active(fst(pair(PeRCenTX,PeRCenTY))) -> #mark(PeRCenTX)
 ||    #83: #splitAt(mark(PeRCenTX),PeRCenTY) -> #splitAt(PeRCenTX,PeRCenTY)
 ||    #84: #and(PeRCenTX,active(PeRCenTY)) -> #and(PeRCenTX,PeRCenTY)
 ||    #85: #mark(0()) -> #active(0())
 ||    #86: #mark(and(PeRCenTX,PeRCenTY)) -> #active(and(mark(PeRCenTX),PeRCenTY))
 ||    #87: #mark(and(PeRCenTX,PeRCenTY)) -> #and(mark(PeRCenTX),PeRCenTY)
 ||    #88: #mark(and(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #89: #u11(PeRCenTX,PeRCenTY,mark(PeRCenTZ),PeRCenTU) -> #u11(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||    #90: #mark(sel(PeRCenTX,PeRCenTY)) -> #active(sel(mark(PeRCenTX),mark(PeRCenTY)))
 ||    #91: #mark(sel(PeRCenTX,PeRCenTY)) -> #sel(mark(PeRCenTX),mark(PeRCenTY))
 ||    #92: #mark(sel(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #93: #mark(sel(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY)
 ||    #94: #snd(mark(PeRCenTX)) -> #snd(PeRCenTX)
 ||    #95: #mark(splitAt(PeRCenTX,PeRCenTY)) -> #active(splitAt(mark(PeRCenTX),mark(PeRCenTY)))
 ||    #96: #mark(splitAt(PeRCenTX,PeRCenTY)) -> #splitAt(mark(PeRCenTX),mark(PeRCenTY))
 ||    #97: #mark(splitAt(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #98: #mark(splitAt(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY)
 ||    #99: #u11(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU) -> #u11(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||    #100: #mark(cons(PeRCenTX,PeRCenTY)) -> #active(cons(mark(PeRCenTX),PeRCenTY))
 ||    #101: #mark(cons(PeRCenTX,PeRCenTY)) -> #cons(mark(PeRCenTX),PeRCenTY)
 ||    #102: #mark(cons(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #103: #and(PeRCenTX,mark(PeRCenTY)) -> #and(PeRCenTX,PeRCenTY)
 ||    #104: #mark(s(PeRCenTX)) -> #active(s(mark(PeRCenTX)))
 ||    #105: #mark(s(PeRCenTX)) -> #s(mark(PeRCenTX))
 ||    #106: #mark(s(PeRCenTX)) -> #mark(PeRCenTX)
 ||    #107: #head(mark(PeRCenTX)) -> #head(PeRCenTX)
 ||    #108: #u11(active(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU) -> #u11(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||    #109: #mark(snd(PeRCenTX)) -> #active(snd(mark(PeRCenTX)))
 ||    #110: #mark(snd(PeRCenTX)) -> #snd(mark(PeRCenTX))
 ||    #111: #mark(snd(PeRCenTX)) -> #mark(PeRCenTX)
 ||    #112: #mark(u12(PeRCenTX,PeRCenTY)) -> #active(u12(mark(PeRCenTX),PeRCenTY))
 ||    #113: #mark(u12(PeRCenTX,PeRCenTY)) -> #u12(mark(PeRCenTX),PeRCenTY)
 ||    #114: #mark(u12(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #115: #active(afterNth(PeRCenTX,PeRCenTY)) -> #mark(snd(splitAt(PeRCenTX,PeRCenTY)))
 ||    #116: #active(afterNth(PeRCenTX,PeRCenTY)) -> #snd(splitAt(PeRCenTX,PeRCenTY))
 ||    #117: #active(afterNth(PeRCenTX,PeRCenTY)) -> #splitAt(PeRCenTX,PeRCenTY)
 ||    #118: #sel(PeRCenTX,active(PeRCenTY)) -> #sel(PeRCenTX,PeRCenTY)
 ||    #119: #active(u11(tt(),PeRCenTX,PeRCenTY,PeRCenTZ)) -> #mark(u12(splitAt(PeRCenTX,PeRCenTZ),PeRCenTY))
 ||    #120: #active(u11(tt(),PeRCenTX,PeRCenTY,PeRCenTZ)) -> #u12(splitAt(PeRCenTX,PeRCenTZ),PeRCenTY)
 ||    #121: #active(u11(tt(),PeRCenTX,PeRCenTY,PeRCenTZ)) -> #splitAt(PeRCenTX,PeRCenTZ)
 ||    #122: #cons(active(PeRCenTX),PeRCenTY) -> #cons(PeRCenTX,PeRCenTY)
 ||    #123: #active(sel(PeRCenTX,PeRCenTY)) -> #mark(head(afterNth(PeRCenTX,PeRCenTY)))
 ||    #124: #active(sel(PeRCenTX,PeRCenTY)) -> #head(afterNth(PeRCenTX,PeRCenTY))
 ||    #125: #active(sel(PeRCenTX,PeRCenTY)) -> #afterNth(PeRCenTX,PeRCenTY)
 ||    #126: #mark(tt()) -> #active(tt())
 ||    #127: #active(and(tt(),PeRCenTX)) -> #mark(PeRCenTX)
 ||    #128: #take(mark(PeRCenTX),PeRCenTY) -> #take(PeRCenTX,PeRCenTY)
 ||    #129: #pair(active(PeRCenTX),PeRCenTY) -> #pair(PeRCenTX,PeRCenTY)
 ||    #130: #mark(pair(PeRCenTX,PeRCenTY)) -> #active(pair(mark(PeRCenTX),mark(PeRCenTY)))
 ||    #131: #mark(pair(PeRCenTX,PeRCenTY)) -> #pair(mark(PeRCenTX),mark(PeRCenTY))
 ||    #132: #mark(pair(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #133: #mark(pair(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY)
 || Number of SCCs: 16, DPs: 97
 ||   SCC { #47 #107 }
 || POLO(Sum)... succeeded.
 ||       TIlDePAIR	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       #take	w: 0
 ||       take	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #u12	w: 0
 ||       #head	w: x1
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       nil	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u12	w: 0
 ||       #afterNth	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #pair	w: 0
 ||       #and	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #47 #107
 || Number of SCCs: 15, DPs: 95
 ||   SCC { #8 #26 }
 || POLO(Sum)... succeeded.
 ||       TIlDePAIR	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       #take	w: 0
 ||       take	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #u12	w: 0
 ||       #head	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: x1
 ||       #u11	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       nil	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u12	w: 0
 ||       #afterNth	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #pair	w: 0
 ||       #and	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #8 #26
 || Number of SCCs: 14, DPs: 93
 ||   SCC { #45 #53 }
 || POLO(Sum)... succeeded.
 ||       TIlDePAIR	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       #take	w: 0
 ||       take	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #u12	w: 0
 ||       #head	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       nil	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: x1
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u12	w: 0
 ||       #afterNth	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #pair	w: 0
 ||       #and	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #45 #53
 || Number of SCCs: 13, DPs: 91
 ||   SCC { #16 #40 }
 || POLO(Sum)... succeeded.
 ||       TIlDePAIR	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       #take	w: 0
 ||       take	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #u12	w: 0
 ||       #head	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       nil	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u12	w: 0
 ||       #afterNth	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: x1
 ||       #active	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #pair	w: 0
 ||       #and	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #16 #40
 || Number of SCCs: 12, DPs: 89
 ||   SCC { #13 #81 }
 || POLO(Sum)... succeeded.
 ||       TIlDePAIR	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       #take	w: 0
 ||       take	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #u12	w: 0
 ||       #head	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       sel	w: 0
 ||       #s 	w: x1
 ||       afterNth	w: 0
 ||       nil	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u12	w: 0
 ||       #afterNth	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #pair	w: 0
 ||       #and	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #13 #81
 || Number of SCCs: 11, DPs: 87
 ||   SCC { #21 #94 }
 || POLO(Sum)... succeeded.
 ||       TIlDePAIR	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       #take	w: 0
 ||       take	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #u12	w: 0
 ||       #head	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       nil	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u12	w: 0
 ||       #afterNth	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: x1
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #pair	w: 0
 ||       #and	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #21 #94
 || Number of SCCs: 10, DPs: 85
 ||   SCC { #7 #44 #55 #128 }
 || POLO(Sum)... succeeded.
 ||       TIlDePAIR	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       #take	w: x1
 ||       take	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #u12	w: 0
 ||       #head	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       nil	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u12	w: 0
 ||       #afterNth	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #pair	w: 0
 ||       #and	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #55 #128
 || Number of SCCs: 10, DPs: 83
 ||   SCC { #7 #44 }
 || POLO(Sum)... succeeded.
 ||       TIlDePAIR	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       #take	w: x2
 ||       take	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #u12	w: 0
 ||       #head	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       nil	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u12	w: 0
 ||       #afterNth	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #pair	w: 0
 ||       #and	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #7 #44
 || Number of SCCs: 9, DPs: 81
 ||   SCC { #59 #79 #84 #103 }
 || POLO(Sum)... succeeded.
 ||       TIlDePAIR	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       #take	w: 0
 ||       take	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #u12	w: 0
 ||       #head	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       nil	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u12	w: 0
 ||       #afterNth	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #pair	w: 0
 ||       #and	w: x1
 ||     USABLE RULES: { }
 ||     Removed DPs: #59 #79
 || Number of SCCs: 9, DPs: 79
 ||   SCC { #84 #103 }
 || POLO(Sum)... succeeded.
 ||       TIlDePAIR	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       #take	w: 0
 ||       take	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #u12	w: 0
 ||       #head	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       nil	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u12	w: 0
 ||       #afterNth	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #pair	w: 0
 ||       #and	w: x2
 ||     USABLE RULES: { }
 ||     Removed DPs: #84 #103
 || Number of SCCs: 8, DPs: 77
 ||   SCC { #18 #19 #36 #118 }
 || POLO(Sum)... succeeded.
 ||       TIlDePAIR	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       #take	w: 0
 ||       take	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #u12	w: 0
 ||       #head	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: x2
 ||       u11	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       nil	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u12	w: 0
 ||       #afterNth	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #pair	w: 0
 ||       #and	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #18 #118
 || Number of SCCs: 8, DPs: 75
 ||   SCC { #19 #36 }
 || POLO(Sum)... succeeded.
 ||       TIlDePAIR	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       #take	w: 0
 ||       take	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #u12	w: 0
 ||       #head	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: x1
 ||       u11	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       nil	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u12	w: 0
 ||       #afterNth	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #pair	w: 0
 ||       #and	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #19 #36
 || Number of SCCs: 7, DPs: 73
 ||   SCC { #9 #14 #46 #83 }
 || POLO(Sum)... succeeded.
 ||       TIlDePAIR	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       #take	w: 0
 ||       take	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #u12	w: 0
 ||       #head	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       nil	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: x2
 ||       mark	w: x1 + 1
 ||       u12	w: 0
 ||       #afterNth	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #pair	w: 0
 ||       #and	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #14 #46
 || Number of SCCs: 7, DPs: 71
 ||   SCC { #9 #83 }
 || POLO(Sum)... succeeded.
 ||       TIlDePAIR	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       #take	w: 0
 ||       take	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #u12	w: 0
 ||       #head	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       nil	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: x1
 ||       mark	w: x1 + 1
 ||       u12	w: 0
 ||       #afterNth	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #pair	w: 0
 ||       #and	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #9 #83
 || Number of SCCs: 6, DPs: 69
 ||   SCC { #15 #25 #63 #122 }
 || POLO(Sum)... succeeded.
 ||       TIlDePAIR	w: 0
 ||       #cons	w: x2
 ||       s 	w: 0
 ||       #take	w: 0
 ||       take	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #u12	w: 0
 ||       #head	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       nil	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u12	w: 0
 ||       #afterNth	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #pair	w: 0
 ||       #and	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #15 #25
 || Number of SCCs: 6, DPs: 67
 ||   SCC { #63 #122 }
 || POLO(Sum)... succeeded.
 ||       TIlDePAIR	w: 0
 ||       #cons	w: x1
 ||       s 	w: 0
 ||       #take	w: 0
 ||       take	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #u12	w: 0
 ||       #head	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       nil	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u12	w: 0
 ||       #afterNth	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #pair	w: 0
 ||       #and	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #63 #122
 || Number of SCCs: 5, DPs: 65
 ||   SCC { #4 #10 #11 #27 }
 || POLO(Sum)... succeeded.
 ||       TIlDePAIR	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       #take	w: 0
 ||       take	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #u12	w: x2
 ||       #head	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       nil	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u12	w: 0
 ||       #afterNth	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #pair	w: 0
 ||       #and	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #4 #11
 || Number of SCCs: 5, DPs: 63
 ||   SCC { #10 #27 }
 || POLO(Sum)... succeeded.
 ||       TIlDePAIR	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       #take	w: 0
 ||       take	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #u12	w: x1
 ||       #head	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       nil	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u12	w: 0
 ||       #afterNth	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #pair	w: 0
 ||       #and	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #10 #27
 || Number of SCCs: 4, DPs: 61
 ||   SCC { #17 #28 #64 #129 }
 || POLO(Sum)... succeeded.
 ||       TIlDePAIR	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       #take	w: 0
 ||       take	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #u12	w: 0
 ||       #head	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       nil	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u12	w: 0
 ||       #afterNth	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #pair	w: x1
 ||       #and	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #17 #129
 || Number of SCCs: 4, DPs: 59
 ||   SCC { #28 #64 }
 || POLO(Sum)... succeeded.
 ||       TIlDePAIR	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       #take	w: 0
 ||       take	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #u12	w: 0
 ||       #head	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       nil	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u12	w: 0
 ||       #afterNth	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #pair	w: x2
 ||       #and	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #28 #64
 || Number of SCCs: 3, DPs: 57
 ||   SCC { #20 #24 #35 #54 }
 || POLO(Sum)... succeeded.
 ||       TIlDePAIR	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       #take	w: 0
 ||       take	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #u12	w: 0
 ||       #head	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       nil	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u12	w: 0
 ||       #afterNth	w: x2
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #pair	w: 0
 ||       #and	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #24 #35
 || Number of SCCs: 3, DPs: 55
 ||   SCC { #20 #54 }
 || POLO(Sum)... succeeded.
 ||       TIlDePAIR	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       #take	w: 0
 ||       take	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #u12	w: 0
 ||       #head	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       nil	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u12	w: 0
 ||       #afterNth	w: x1
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #pair	w: 0
 ||       #and	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #20 #54
 || Number of SCCs: 2, DPs: 53
 ||   SCC { #6 #12 #22 #76 #80 #89 #99 #108 }
 || POLO(Sum)... succeeded.
 ||       TIlDePAIR	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       #take	w: 0
 ||       take	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #u12	w: 0
 ||       #head	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: x2 + x3 + x4
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       nil	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u12	w: 0
 ||       #afterNth	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #pair	w: 0
 ||       #and	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #6 #12 #22 #76 #80 #89
 || Number of SCCs: 2, DPs: 47
 ||   SCC { #99 #108 }
 || POLO(Sum)... succeeded.
 ||       TIlDePAIR	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       #take	w: 0
 ||       take	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #u12	w: 0
 ||       #head	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: x1
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       nil	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u12	w: 0
 ||       #afterNth	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #pair	w: 0
 ||       #and	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #99 #108
 || Number of SCCs: 1, DPs: 45
 ||   SCC { #1 #23 #29 #32 #33 #37 #39 #41 #43 #48 #49 #51 #52 #56 #58 #60 #62 #65 #67 #68 #70..72 #77 #82 #86 #88 #90 #92 #93 #95 #97 #98 #102 #106 #109 #111 #112 #114 #115 #119 #123 #127 #132 #133 }
 || POLO(Sum)... POLO(max)... succeeded.
 ||       TIlDePAIR	w: 0
 ||       #cons	w: 0
 ||       s 	w: x1
 ||       #take	w: 0
 ||       take	w: max(x1 + 8, x2 + 9)
 ||       and	w: max(x1 + 1, x2 + 2)
 ||       pair	w: max(x1 + 1, x2 + 2)
 ||       fst	w: x1 + 1
 ||       natsFrom	w: x1 + 5
 ||       #u12	w: 0
 ||       #head	w: 0
 ||       splitAt	w: max(x1 + 6, x2 + 4)
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       tail	w: x1 + 1
 ||       #mark	w: x1
 ||       0 	w: 1
 ||       #sel	w: 0
 ||       u11	w: max(x1 + 1, x2 + 6, x3 + 7, x4 + 4)
 ||       sel	w: max(x1 + 9, x2 + 10)
 ||       #s 	w: 0
 ||       afterNth	w: max(x1 + 7, x2 + 5)
 ||       nil	w: 4
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1
 ||       u12	w: max(x1, x2 + 5)
 ||       #afterNth	w: 0
 ||       active	w: x1
 ||       head	w: x1 + 1
 ||       #snd	w: 0
 ||       cons	w: max(x1 + 4, x2)
 ||       #natsFrom	w: 0
 ||       #active	w: x1
 ||       snd	w: x1 + 1
 ||       tt	w: 7
 ||       #pair	w: 0
 ||       #and	w: 0
 ||     USABLE RULES: { 1..83 }
 ||     Removed DPs: #23 #29 #32 #39 #43 #48 #51 #52 #58 #62 #67 #70 #71 #77 #82 #88 #92 #93 #97 #98 #102 #111 #123 #127 #132 #133
 || Number of SCCs: 1, DPs: 6
 ||   SCC { #33 #56 #95 #106 #114 #119 }
 || POLO(Sum)... succeeded.
 ||       TIlDePAIR	w: 0
 ||       #cons	w: 0
 ||       s 	w: x1 + 1
 ||       #take	w: 0
 ||       take	w: x1 + x2 + 1
 ||       and	w: x2 + 1
 ||       pair	w: x1 + x2 + 1
 ||       fst	w: x1 + 1
 ||       natsFrom	w: x1 + 1
 ||       #u12	w: 0
 ||       #head	w: 0
 ||       splitAt	w: 1
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       tail	w: 1
 ||       #mark	w: x1
 ||       0 	w: 1
 ||       #sel	w: 0
 ||       u11	w: 1
 ||       sel	w: x1 + 1
 ||       #s 	w: 0
 ||       afterNth	w: 1
 ||       nil	w: 3
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u12	w: x1
 ||       #afterNth	w: 0
 ||       active	w: x1 + 3
 ||       head	w: x1 + 1
 ||       #snd	w: 0
 ||       cons	w: x2 + 3
 ||       #natsFrom	w: 0
 ||       #active	w: 1
 ||       snd	w: x1 + 1
 ||       tt	w: 2
 ||       #pair	w: 0
 ||       #and	w: 0
 ||     USABLE RULES: { 32..59 62..65 72 73 }
 ||     Removed DPs: #106
 || Number of SCCs: 1, DPs: 5
 ||   SCC { #33 #56 #95 #114 #119 }
 || POLO(Sum)... POLO(max)... QLPOS... POLO(mSum)... QWPOpS(mSum)... succeeded.
 ||       TIlDePAIR	s: []	p: 0	w: x2
 ||       #cons	s: [1]	p: 0	w: max(x1 + 1)
 ||       s 	s: [1]	p: 4	w: x1
 ||       #take	s: []	p: 0	w: 1
 ||       take	s: [1,2]	p: 1	w: x1 + x2 + 12
 ||       and	s: [1]	p: 0	w: x1 + x2 + 1
 ||       pair	s: [2]	p: 0	w: max(x1, x2 + 1)
 ||       fst	s: []	p: 3	w: x1 + 1
 ||       natsFrom	s: []	p: 1	w: x1 + 7
 ||       #u12	s: []	p: 0	w: max(x1)
 ||       #head	s: []	p: 0	w: 1
 ||       splitAt	s: [1,2]	p: 3	w: max(x1 + 8, x2 + 10)
 ||       #fst	s: []	p: 0	w: 1
 ||       #u11	s: []	p: 0	w: max(x2)
 ||       tail	s: []	p: 3	w: x1 + 1
 ||       #mark	s: [1]	p: 4	w: x1
 ||       0 	s: []	p: 2	w: 0
 ||       #sel	s: []	p: 0	w: 0
 ||       u11	s: [2,4,1]	p: 3	w: max(x1 + 5, x2 + 8, x3 + 4, x4 + 10)
 ||       sel	s: [2]	p: 5	w: x1 + x2 + 13
 ||       #s 	s: []	p: 0	w: 1
 ||       afterNth	s: [2]	p: 5	w: x1 + x2 + 12
 ||       nil	s: []	p: 4	w: 9
 ||       #TIlDePAIR	s: [1]	p: 0	w: x1
 ||       #tail	s: []	p: 0	w: 0
 ||       #splitAt	s: [2,1]	p: 0	w: max(x1, x2)
 ||       mark	s: 1
 ||       u12	s: [2,1]	p: 2	w: max(x1, x2 + 3)
 ||       #afterNth	s: []	p: 0	w: x1 + 1
 ||       active	s: 1
 ||       head	s: 1
 ||       #snd	s: []	p: 0	w: 1
 ||       cons	s: []	p: 1	w: max(x1 + 2, x2)
 ||       #natsFrom	s: []	p: 0	w: 1
 ||       #active	s: [1]	p: 4	w: x1
 ||       snd	s: [1]	p: 3	w: x1 + 1
 ||       tt	s: []	p: 3	w: 2
 ||       #pair	s: [1,2]	p: 0	w: max(x1, x2)
 ||       #and	s: []	p: 0	w: x2
 ||     USABLE RULES: { 1..83 }
 ||     Removed DPs: #114
 || Number of SCCs: 0, DPs: 0
 || 
We use the dependency pair framework as described in [Kop12, Ch. 6/7], with static dependency pairs (see [KusIsoSakBla09] and the adaptation for AFSMs and accessible arguments in [FuhKop19]).

We thus obtain the following dependency pair problem (P_0, R_0, computable, formative):

  Dependency Pairs P_0:

    0] map#(/\x.X(x), cons(Y, Z)) =#> cons#(X(Y), map(/\y.X(y), Z))   
    1] map#(/\x.X(x), cons(Y, Z)) =#> map#(/\y.X(y), Z)   

  Rules R_0:

    active(u11(tt, X, Y, Z)) => mark(u12(splitAt(X, Z), Y)) 
    active(u12(pair(X, Y), Z)) => mark(pair(cons(Z, X), Y)) 
    active(afterNth(X, Y)) => mark(snd(splitAt(X, Y))) 
    active(and(tt, X)) => mark(X) 
    active(fst(pair(X, Y))) => mark(X) 
    active(head(cons(X, Y))) => mark(X) 
    active(natsFrom(X)) => mark(cons(X, natsFrom(s(X)))) 
    active(sel(X, Y)) => mark(head(afterNth(X, Y))) 
    active(snd(pair(X, Y))) => mark(Y) 
    active(splitAt(0, X)) => mark(pair(nil, X)) 
    active(splitAt(s(X), cons(Y, Z))) => mark(u11(tt, X, Y, Z)) 
    active(tail(cons(X, Y))) => mark(Y) 
    active(take(X, Y)) => mark(fst(splitAt(X, Y))) 
    mark(u11(X, Y, Z, U)) => active(u11(mark(X), Y, Z, U)) 
    mark(tt) => active(tt) 
    mark(u12(X, Y)) => active(u12(mark(X), Y)) 
    mark(splitAt(X, Y)) => active(splitAt(mark(X), mark(Y))) 
    mark(pair(X, Y)) => active(pair(mark(X), mark(Y))) 
    mark(cons(X, Y)) => active(cons(mark(X), Y)) 
    mark(afterNth(X, Y)) => active(afterNth(mark(X), mark(Y))) 
    mark(snd(X)) => active(snd(mark(X))) 
    mark(and(X, Y)) => active(and(mark(X), Y)) 
    mark(fst(X)) => active(fst(mark(X))) 
    mark(head(X)) => active(head(mark(X))) 
    mark(natsFrom(X)) => active(natsFrom(mark(X))) 
    mark(s(X)) => active(s(mark(X))) 
    mark(sel(X, Y)) => active(sel(mark(X), mark(Y))) 
    mark(0) => active(0) 
    mark(nil) => active(nil) 
    mark(tail(X)) => active(tail(mark(X))) 
    mark(take(X, Y)) => active(take(mark(X), mark(Y))) 
    u11(mark(X), Y, Z, U) => u11(X, Y, Z, U) 
    u11(X, mark(Y), Z, U) => u11(X, Y, Z, U) 
    u11(X, Y, mark(Z), U) => u11(X, Y, Z, U) 
    u11(X, Y, Z, mark(U)) => u11(X, Y, Z, U) 
    u11(active(X), Y, Z, U) => u11(X, Y, Z, U) 
    u11(X, active(Y), Z, U) => u11(X, Y, Z, U) 
    u11(X, Y, active(Z), U) => u11(X, Y, Z, U) 
    u11(X, Y, Z, active(U)) => u11(X, Y, Z, U) 
    u12(mark(X), Y) => u12(X, Y) 
    u12(X, mark(Y)) => u12(X, Y) 
    u12(active(X), Y) => u12(X, Y) 
    u12(X, active(Y)) => u12(X, Y) 
    splitAt(mark(X), Y) => splitAt(X, Y) 
    splitAt(X, mark(Y)) => splitAt(X, Y) 
    splitAt(active(X), Y) => splitAt(X, Y) 
    splitAt(X, active(Y)) => splitAt(X, Y) 
    pair(mark(X), Y) => pair(X, Y) 
    pair(X, mark(Y)) => pair(X, Y) 
    pair(active(X), Y) => pair(X, Y) 
    pair(X, active(Y)) => pair(X, Y) 
    cons(mark(X), Y) => cons(X, Y) 
    cons(X, mark(Y)) => cons(X, Y) 
    cons(active(X), Y) => cons(X, Y) 
    cons(X, active(Y)) => cons(X, Y) 
    afterNth(mark(X), Y) => afterNth(X, Y) 
    afterNth(X, mark(Y)) => afterNth(X, Y) 
    afterNth(active(X), Y) => afterNth(X, Y) 
    afterNth(X, active(Y)) => afterNth(X, Y) 
    snd(mark(X)) => snd(X) 
    snd(active(X)) => snd(X) 
    and(mark(X), Y) => and(X, Y) 
    and(X, mark(Y)) => and(X, Y) 
    and(active(X), Y) => and(X, Y) 
    and(X, active(Y)) => and(X, Y) 
    fst(mark(X)) => fst(X) 
    fst(active(X)) => fst(X) 
    head(mark(X)) => head(X) 
    head(active(X)) => head(X) 
    natsFrom(mark(X)) => natsFrom(X) 
    natsFrom(active(X)) => natsFrom(X) 
    s(mark(X)) => s(X) 
    s(active(X)) => s(X) 
    sel(mark(X), Y) => sel(X, Y) 
    sel(X, mark(Y)) => sel(X, Y) 
    sel(active(X), Y) => sel(X, Y) 
    sel(X, active(Y)) => sel(X, Y) 
    tail(mark(X)) => tail(X) 
    tail(active(X)) => tail(X) 
    take(mark(X), Y) => take(X, Y) 
    take(X, mark(Y)) => take(X, Y) 
    take(active(X), Y) => take(X, Y) 
    take(X, active(Y)) => take(X, Y) 
    map(/\x.X(x), nil) => nil 
    map(/\x.X(x), cons(Y, Z)) => cons(X(Y), map(/\y.X(y), Z)) 
    app(/\x.X(x), Y) => X(Y) 

Thus, the original system is terminating if (P_0, R_0, computable, formative) is finite.

We consider the dependency pair problem (P_0, R_0, computable, formative).

We place the elements of P in a dependency graph approximation G (see e.g. [Kop12, Thm. 7.27, 7.29], as follows:

    * 0 :  
    * 1 : 0, 1 

This graph has the following strongly connected components:

  P_1:

    map#(/\x.X(x), cons(Y, Z)) =#> map#(/\y.X(y), Z)   

By [Kop12, Thm. 7.31], we may replace any dependency pair problem (P_0, R_0, m, f) by (P_1, R_0, m, f).

Thus, the original system is terminating if (P_1, R_0, computable, formative) is finite.

We consider the dependency pair problem (P_1, R_0, computable, formative).

We apply the subterm criterion with the following projection function:

  nu(map#) = 2 

Thus, we can orient the dependency pairs as follows:

  nu(map#(/\x.X(x), cons(Y, Z))) = cons(Y, Z) |> Z = nu(map#(/\y.X(y), Z)) 

By [FuhKop19, Thm. 61], we may replace a dependency pair problem (P_1, R_0, computable, f) by ({}, R_0, computable, f).  By the empty set processor [Kop12, Thm. 7.15] this problem may be immediately removed.

As all dependency pair problems were succesfully simplified with sound (and complete) processors until nothing remained, we conclude termination.


+++ Citations +++

[FuhKop19]  C. Fuhs, and C. Kop.  A static higher-order dependency pair framework.  In Proceedings of ESOP 2019, 2019.
[Kop11]  C. Kop.  Simplifying Algebraic Functional Systems.  In Proceedings of CAI 2011, volume 6742 of LNCS.  201--215, Springer, 2011.
[Kop12]  C. Kop.  Higher Order Termination.  PhD Thesis, 2012.
[KusIsoSakBla09]  K. Kusakari, Y. Isogai, M. Sakai, and F. Blanqui.  Static Dependency Pair Method Based On Strong Computability for Higher-Order Rewrite Systems.  In volume 92(10) of IEICE Transactions on Information and Systems.  2007--2015, 2009.