We consider the system h33.

  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 
    isLNat : [] --> A -> A 
    isNatural : [] --> A -> A 
    isPLNat : [] --> 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 
    u101 : [] --> A -> A -> A -> A 
    u11 : [] --> A -> A -> A -> A 
    u21 : [] --> A -> A -> A 
    u31 : [] --> A -> A -> A 
    u41 : [] --> A -> A -> A 
    u51 : [] --> A -> A -> A -> A 
    u61 : [] --> A -> A -> A 
    u71 : [] --> A -> A -> A 
    u81 : [] --> A -> A -> A -> A -> A 
    u82 : [] --> A -> A -> A 
    u91 : [] --> A -> A -> A 

  Rules:

    active (u101 tt x y) => mark (fst (splitAt x y)) 
    active (u11 tt x y) => mark (snd (splitAt x y)) 
    active (u21 tt x) => mark x 
    active (u31 tt x) => mark x 
    active (u41 tt x) => mark (cons x (natsFrom (s x))) 
    active (u51 tt x y) => mark (head (afterNth x y)) 
    active (u61 tt x) => mark x 
    active (u71 tt x) => mark (pair nil x) 
    active (u81 tt x y z) => mark (u82 (splitAt x z) y) 
    active (u82 (pair x y) z) => mark (pair (cons z x) y) 
    active (u91 tt x) => mark x 
    active (afterNth x y) => mark (u11 (and (isNatural x) (isLNat y)) x y) 
    active (and tt x) => mark x 
    active (fst (pair x y)) => mark (u21 (and (isLNat x) (isLNat y)) x) 
    active (head (cons x y)) => mark (u31 (and (isNatural x) (isLNat y)) x) 
    active (isLNat nil) => mark tt 
    active (isLNat (afterNth x y)) => mark (and (isNatural x) (isLNat y)) 
    active (isLNat (cons x y)) => mark (and (isNatural x) (isLNat y)) 
    active (isLNat (fst x)) => mark (isPLNat x) 
    active (isLNat (natsFrom x)) => mark (isNatural x) 
    active (isLNat (snd x)) => mark (isPLNat x) 
    active (isLNat (tail x)) => mark (isLNat x) 
    active (isLNat (take x y)) => mark (and (isNatural x) (isLNat y)) 
    active (isNatural 0) => mark tt 
    active (isNatural (head x)) => mark (isLNat x) 
    active (isNatural (s x)) => mark (isNatural x) 
    active (isNatural (sel x y)) => mark (and (isNatural x) (isLNat y)) 
    active (isPLNat (pair x y)) => mark (and (isLNat x) (isLNat y)) 
    active (isPLNat (splitAt x y)) => mark (and (isNatural x) (isLNat y)) 
    active (natsFrom x) => mark (u41 (isNatural x) x) 
    active (sel x y) => mark (u51 (and (isNatural x) (isLNat y)) x y) 
    active (snd (pair x y)) => mark (u61 (and (isLNat x) (isLNat y)) y) 
    active (splitAt 0 x) => mark (u71 (isLNat x) x) 
    active (splitAt (s x) (cons y z)) => mark (u81 (and (isNatural x) (and (isNatural y) (isLNat z))) x y z) 
    active (tail (cons x y)) => mark (u91 (and (isNatural x) (isLNat y)) y) 
    active (take x y) => mark (u101 (and (isNatural x) (isLNat y)) x y) 
    mark (u101 x y z) => active (u101 (mark x) y z) 
    mark tt => active tt 
    mark (fst x) => active (fst (mark x)) 
    mark (splitAt x y) => active (splitAt (mark x) (mark y)) 
    mark (u11 x y z) => active (u11 (mark x) y z) 
    mark (snd x) => active (snd (mark x)) 
    mark (u21 x y) => active (u21 (mark x) y) 
    mark (u31 x y) => active (u31 (mark x) y) 
    mark (u41 x y) => active (u41 (mark x) y) 
    mark (cons x y) => active (cons (mark x) y) 
    mark (natsFrom x) => active (natsFrom (mark x)) 
    mark (s x) => active (s (mark x)) 
    mark (u51 x y z) => active (u51 (mark x) y z) 
    mark (head x) => active (head (mark x)) 
    mark (afterNth x y) => active (afterNth (mark x) (mark y)) 
    mark (u61 x y) => active (u61 (mark x) y) 
    mark (u71 x y) => active (u71 (mark x) y) 
    mark (pair x y) => active (pair (mark x) (mark y)) 
    mark nil => active nil 
    mark (u81 x y z u) => active (u81 (mark x) y z u) 
    mark (u82 x y) => active (u82 (mark x) y) 
    mark (u91 x y) => active (u91 (mark x) y) 
    mark (and x y) => active (and (mark x) y) 
    mark (isNatural x) => active (isNatural x) 
    mark (isLNat x) => active (isLNat x) 
    mark (isPLNat x) => active (isPLNat x) 
    mark (tail x) => active (tail (mark x)) 
    mark (take x y) => active (take (mark x) (mark y)) 
    mark 0 => active 0 
    mark (sel x y) => active (sel (mark x) (mark y)) 
    u101 (mark x) y z => u101 x y z 
    u101 x (mark y) z => u101 x y z 
    u101 x y (mark z) => u101 x y z 
    u101 (active x) y z => u101 x y z 
    u101 x (active y) z => u101 x y z 
    u101 x y (active z) => u101 x y z 
    fst (mark x) => fst x 
    fst (active x) => fst x 
    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 
    u11 (mark x) y z => u11 x y z 
    u11 x (mark y) z => u11 x y z 
    u11 x y (mark z) => u11 x y z 
    u11 (active x) y z => u11 x y z 
    u11 x (active y) z => u11 x y z 
    u11 x y (active z) => u11 x y z 
    snd (mark x) => snd x 
    snd (active x) => snd x 
    u21 (mark x) y => u21 x y 
    u21 x (mark y) => u21 x y 
    u21 (active x) y => u21 x y 
    u21 x (active y) => u21 x y 
    u31 (mark x) y => u31 x y 
    u31 x (mark y) => u31 x y 
    u31 (active x) y => u31 x y 
    u31 x (active y) => u31 x y 
    u41 (mark x) y => u41 x y 
    u41 x (mark y) => u41 x y 
    u41 (active x) y => u41 x y 
    u41 x (active y) => u41 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 
    natsFrom (mark x) => natsFrom x 
    natsFrom (active x) => natsFrom x 
    s (mark x) => s x 
    s (active x) => s x 
    u51 (mark x) y z => u51 x y z 
    u51 x (mark y) z => u51 x y z 
    u51 x y (mark z) => u51 x y z 
    u51 (active x) y z => u51 x y z 
    u51 x (active y) z => u51 x y z 
    u51 x y (active z) => u51 x y z 
    head (mark x) => head x 
    head (active x) => head x 
    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 
    u61 (mark x) y => u61 x y 
    u61 x (mark y) => u61 x y 
    u61 (active x) y => u61 x y 
    u61 x (active y) => u61 x y 
    u71 (mark x) y => u71 x y 
    u71 x (mark y) => u71 x y 
    u71 (active x) y => u71 x y 
    u71 x (active y) => u71 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 
    u81 (mark x) y z u => u81 x y z u 
    u81 x (mark y) z u => u81 x y z u 
    u81 x y (mark z) u => u81 x y z u 
    u81 x y z (mark u) => u81 x y z u 
    u81 (active x) y z u => u81 x y z u 
    u81 x (active y) z u => u81 x y z u 
    u81 x y (active z) u => u81 x y z u 
    u81 x y z (active u) => u81 x y z u 
    u82 (mark x) y => u82 x y 
    u82 x (mark y) => u82 x y 
    u82 (active x) y => u82 x y 
    u82 x (active y) => u82 x y 
    u91 (mark x) y => u91 x y 
    u91 x (mark y) => u91 x y 
    u91 (active x) y => u91 x y 
    u91 x (active y) => u91 x y 
    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 
    isNatural (mark x) => isNatural x 
    isNatural (active x) => isNatural x 
    isLNat (mark x) => isLNat x 
    isLNat (active x) => isLNat x 
    isPLNat (mark x) => isPLNat x 
    isPLNat (active x) => isPLNat x 
    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 
    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 
    map (/\x.f x) nil => nil 
    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 
    isLNat : [A] --> A 
    isNatural : [A] --> A 
    isPLNat : [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 
    u101 : [A * A * A] --> A 
    u11 : [A * A * A] --> A 
    u21 : [A * A] --> A 
    u31 : [A * A] --> A 
    u41 : [A * A] --> A 
    u51 : [A * A * A] --> A 
    u61 : [A * A] --> A 
    u71 : [A * A] --> A 
    u81 : [A * A * A * A] --> A 
    u82 : [A * A] --> A 
    u91 : [A * A] --> A 
    ~AP1 : [A -> A * A] --> A 

  Rules:

    active(u101(tt, X, Y)) => mark(fst(splitAt(X, Y))) 
    active(u11(tt, X, Y)) => mark(snd(splitAt(X, Y))) 
    active(u21(tt, X)) => mark(X) 
    active(u31(tt, X)) => mark(X) 
    active(u41(tt, X)) => mark(cons(X, natsFrom(s(X)))) 
    active(u51(tt, X, Y)) => mark(head(afterNth(X, Y))) 
    active(u61(tt, X)) => mark(X) 
    active(u71(tt, X)) => mark(pair(nil, X)) 
    active(u81(tt, X, Y, Z)) => mark(u82(splitAt(X, Z), Y)) 
    active(u82(pair(X, Y), Z)) => mark(pair(cons(Z, X), Y)) 
    active(u91(tt, X)) => mark(X) 
    active(afterNth(X, Y)) => mark(u11(and(isNatural(X), isLNat(Y)), X, Y)) 
    active(and(tt, X)) => mark(X) 
    active(fst(pair(X, Y))) => mark(u21(and(isLNat(X), isLNat(Y)), X)) 
    active(head(cons(X, Y))) => mark(u31(and(isNatural(X), isLNat(Y)), X)) 
    active(isLNat(nil)) => mark(tt) 
    active(isLNat(afterNth(X, Y))) => mark(and(isNatural(X), isLNat(Y))) 
    active(isLNat(cons(X, Y))) => mark(and(isNatural(X), isLNat(Y))) 
    active(isLNat(fst(X))) => mark(isPLNat(X)) 
    active(isLNat(natsFrom(X))) => mark(isNatural(X)) 
    active(isLNat(snd(X))) => mark(isPLNat(X)) 
    active(isLNat(tail(X))) => mark(isLNat(X)) 
    active(isLNat(take(X, Y))) => mark(and(isNatural(X), isLNat(Y))) 
    active(isNatural(0)) => mark(tt) 
    active(isNatural(head(X))) => mark(isLNat(X)) 
    active(isNatural(s(X))) => mark(isNatural(X)) 
    active(isNatural(sel(X, Y))) => mark(and(isNatural(X), isLNat(Y))) 
    active(isPLNat(pair(X, Y))) => mark(and(isLNat(X), isLNat(Y))) 
    active(isPLNat(splitAt(X, Y))) => mark(and(isNatural(X), isLNat(Y))) 
    active(natsFrom(X)) => mark(u41(isNatural(X), X)) 
    active(sel(X, Y)) => mark(u51(and(isNatural(X), isLNat(Y)), X, Y)) 
    active(snd(pair(X, Y))) => mark(u61(and(isLNat(X), isLNat(Y)), Y)) 
    active(splitAt(0, X)) => mark(u71(isLNat(X), X)) 
    active(splitAt(s(X), cons(Y, Z))) => mark(u81(and(isNatural(X), and(isNatural(Y), isLNat(Z))), X, Y, Z)) 
    active(tail(cons(X, Y))) => mark(u91(and(isNatural(X), isLNat(Y)), Y)) 
    active(take(X, Y)) => mark(u101(and(isNatural(X), isLNat(Y)), X, Y)) 
    mark(u101(X, Y, Z)) => active(u101(mark(X), Y, Z)) 
    mark(tt) => active(tt) 
    mark(fst(X)) => active(fst(mark(X))) 
    mark(splitAt(X, Y)) => active(splitAt(mark(X), mark(Y))) 
    mark(u11(X, Y, Z)) => active(u11(mark(X), Y, Z)) 
    mark(snd(X)) => active(snd(mark(X))) 
    mark(u21(X, Y)) => active(u21(mark(X), Y)) 
    mark(u31(X, Y)) => active(u31(mark(X), Y)) 
    mark(u41(X, Y)) => active(u41(mark(X), Y)) 
    mark(cons(X, Y)) => active(cons(mark(X), Y)) 
    mark(natsFrom(X)) => active(natsFrom(mark(X))) 
    mark(s(X)) => active(s(mark(X))) 
    mark(u51(X, Y, Z)) => active(u51(mark(X), Y, Z)) 
    mark(head(X)) => active(head(mark(X))) 
    mark(afterNth(X, Y)) => active(afterNth(mark(X), mark(Y))) 
    mark(u61(X, Y)) => active(u61(mark(X), Y)) 
    mark(u71(X, Y)) => active(u71(mark(X), Y)) 
    mark(pair(X, Y)) => active(pair(mark(X), mark(Y))) 
    mark(nil) => active(nil) 
    mark(u81(X, Y, Z, U)) => active(u81(mark(X), Y, Z, U)) 
    mark(u82(X, Y)) => active(u82(mark(X), Y)) 
    mark(u91(X, Y)) => active(u91(mark(X), Y)) 
    mark(and(X, Y)) => active(and(mark(X), Y)) 
    mark(isNatural(X)) => active(isNatural(X)) 
    mark(isLNat(X)) => active(isLNat(X)) 
    mark(isPLNat(X)) => active(isPLNat(X)) 
    mark(tail(X)) => active(tail(mark(X))) 
    mark(take(X, Y)) => active(take(mark(X), mark(Y))) 
    mark(0) => active(0) 
    mark(sel(X, Y)) => active(sel(mark(X), mark(Y))) 
    u101(mark(X), Y, Z) => u101(X, Y, Z) 
    u101(X, mark(Y), Z) => u101(X, Y, Z) 
    u101(X, Y, mark(Z)) => u101(X, Y, Z) 
    u101(active(X), Y, Z) => u101(X, Y, Z) 
    u101(X, active(Y), Z) => u101(X, Y, Z) 
    u101(X, Y, active(Z)) => u101(X, Y, Z) 
    fst(mark(X)) => fst(X) 
    fst(active(X)) => fst(X) 
    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) 
    u11(mark(X), Y, Z) => u11(X, Y, Z) 
    u11(X, mark(Y), Z) => u11(X, Y, Z) 
    u11(X, Y, mark(Z)) => u11(X, Y, Z) 
    u11(active(X), Y, Z) => u11(X, Y, Z) 
    u11(X, active(Y), Z) => u11(X, Y, Z) 
    u11(X, Y, active(Z)) => u11(X, Y, Z) 
    snd(mark(X)) => snd(X) 
    snd(active(X)) => snd(X) 
    u21(mark(X), Y) => u21(X, Y) 
    u21(X, mark(Y)) => u21(X, Y) 
    u21(active(X), Y) => u21(X, Y) 
    u21(X, active(Y)) => u21(X, Y) 
    u31(mark(X), Y) => u31(X, Y) 
    u31(X, mark(Y)) => u31(X, Y) 
    u31(active(X), Y) => u31(X, Y) 
    u31(X, active(Y)) => u31(X, Y) 
    u41(mark(X), Y) => u41(X, Y) 
    u41(X, mark(Y)) => u41(X, Y) 
    u41(active(X), Y) => u41(X, Y) 
    u41(X, active(Y)) => u41(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) 
    natsFrom(mark(X)) => natsFrom(X) 
    natsFrom(active(X)) => natsFrom(X) 
    s(mark(X)) => s(X) 
    s(active(X)) => s(X) 
    u51(mark(X), Y, Z) => u51(X, Y, Z) 
    u51(X, mark(Y), Z) => u51(X, Y, Z) 
    u51(X, Y, mark(Z)) => u51(X, Y, Z) 
    u51(active(X), Y, Z) => u51(X, Y, Z) 
    u51(X, active(Y), Z) => u51(X, Y, Z) 
    u51(X, Y, active(Z)) => u51(X, Y, Z) 
    head(mark(X)) => head(X) 
    head(active(X)) => head(X) 
    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) 
    u61(mark(X), Y) => u61(X, Y) 
    u61(X, mark(Y)) => u61(X, Y) 
    u61(active(X), Y) => u61(X, Y) 
    u61(X, active(Y)) => u61(X, Y) 
    u71(mark(X), Y) => u71(X, Y) 
    u71(X, mark(Y)) => u71(X, Y) 
    u71(active(X), Y) => u71(X, Y) 
    u71(X, active(Y)) => u71(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) 
    u81(mark(X), Y, Z, U) => u81(X, Y, Z, U) 
    u81(X, mark(Y), Z, U) => u81(X, Y, Z, U) 
    u81(X, Y, mark(Z), U) => u81(X, Y, Z, U) 
    u81(X, Y, Z, mark(U)) => u81(X, Y, Z, U) 
    u81(active(X), Y, Z, U) => u81(X, Y, Z, U) 
    u81(X, active(Y), Z, U) => u81(X, Y, Z, U) 
    u81(X, Y, active(Z), U) => u81(X, Y, Z, U) 
    u81(X, Y, Z, active(U)) => u81(X, Y, Z, U) 
    u82(mark(X), Y) => u82(X, Y) 
    u82(X, mark(Y)) => u82(X, Y) 
    u82(active(X), Y) => u82(X, Y) 
    u82(X, active(Y)) => u82(X, Y) 
    u91(mark(X), Y) => u91(X, Y) 
    u91(X, mark(Y)) => u91(X, Y) 
    u91(active(X), Y) => u91(X, Y) 
    u91(X, active(Y)) => u91(X, Y) 
    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) 
    isNatural(mark(X)) => isNatural(X) 
    isNatural(active(X)) => isNatural(X) 
    isLNat(mark(X)) => isLNat(X) 
    isLNat(active(X)) => isLNat(X) 
    isPLNat(mark(X)) => isPLNat(X) 
    isPLNat(active(X)) => isPLNat(X) 
    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) 
    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) 
    map(/\x.~AP1(F, x), nil) => nil 
    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.isLNat(x), nil) => nil 
    map(/\x.isNatural(x), nil) => nil 
    map(/\x.isPLNat(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.u101(X, Y, x), nil) => nil 
    map(/\x.u11(X, Y, x), nil) => nil 
    map(/\x.u21(X, x), nil) => nil 
    map(/\x.u31(X, x), nil) => nil 
    map(/\x.u41(X, x), nil) => nil 
    map(/\x.u51(X, Y, x), nil) => nil 
    map(/\x.u61(X, x), nil) => nil 
    map(/\x.u71(X, x), nil) => nil 
    map(/\x.u81(X, Y, Z, x), nil) => nil 
    map(/\x.u82(X, x), nil) => nil 
    map(/\x.u91(X, x), nil) => nil 
    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.isLNat(x), X) => isLNat(X) 
    app(/\x.isNatural(x), X) => isNatural(X) 
    app(/\x.isPLNat(x), X) => isPLNat(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.u101(X, Y, x), Z) => u101(X, Y, Z) 
    app(/\x.u11(X, Y, x), Z) => u11(X, Y, Z) 
    app(/\x.u21(X, x), Y) => u21(X, Y) 
    app(/\x.u31(X, x), Y) => u31(X, Y) 
    app(/\x.u41(X, x), Y) => u41(X, Y) 
    app(/\x.u51(X, Y, x), Z) => u51(X, Y, Z) 
    app(/\x.u61(X, x), Y) => u61(X, Y) 
    app(/\x.u71(X, x), Y) => u71(X, Y) 
    app(/\x.u81(X, Y, Z, x), U) => u81(X, Y, Z, U) 
    app(/\x.u82(X, x), Y) => u82(X, Y) 
    app(/\x.u91(X, x), Y) => u91(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 
    isLNat : [A] --> A 
    isNatural : [A] --> A 
    isPLNat : [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 
    u101 : [A * A * A] --> A 
    u11 : [A * A * A] --> A 
    u21 : [A * A] --> A 
    u31 : [A * A] --> A 
    u41 : [A * A] --> A 
    u51 : [A * A * A] --> A 
    u61 : [A * A] --> A 
    u71 : [A * A] --> A 
    u81 : [A * A * A * A] --> A 
    u82 : [A * A] --> A 
    u91 : [A * A] --> A 

  Rules:

    active(u101(tt, X, Y)) => mark(fst(splitAt(X, Y))) 
    active(u11(tt, X, Y)) => mark(snd(splitAt(X, Y))) 
    active(u21(tt, X)) => mark(X) 
    active(u31(tt, X)) => mark(X) 
    active(u41(tt, X)) => mark(cons(X, natsFrom(s(X)))) 
    active(u51(tt, X, Y)) => mark(head(afterNth(X, Y))) 
    active(u61(tt, X)) => mark(X) 
    active(u71(tt, X)) => mark(pair(nil, X)) 
    active(u81(tt, X, Y, Z)) => mark(u82(splitAt(X, Z), Y)) 
    active(u82(pair(X, Y), Z)) => mark(pair(cons(Z, X), Y)) 
    active(u91(tt, X)) => mark(X) 
    active(afterNth(X, Y)) => mark(u11(and(isNatural(X), isLNat(Y)), X, Y)) 
    active(and(tt, X)) => mark(X) 
    active(fst(pair(X, Y))) => mark(u21(and(isLNat(X), isLNat(Y)), X)) 
    active(head(cons(X, Y))) => mark(u31(and(isNatural(X), isLNat(Y)), X)) 
    active(isLNat(nil)) => mark(tt) 
    active(isLNat(afterNth(X, Y))) => mark(and(isNatural(X), isLNat(Y))) 
    active(isLNat(cons(X, Y))) => mark(and(isNatural(X), isLNat(Y))) 
    active(isLNat(fst(X))) => mark(isPLNat(X)) 
    active(isLNat(natsFrom(X))) => mark(isNatural(X)) 
    active(isLNat(snd(X))) => mark(isPLNat(X)) 
    active(isLNat(tail(X))) => mark(isLNat(X)) 
    active(isLNat(take(X, Y))) => mark(and(isNatural(X), isLNat(Y))) 
    active(isNatural(0)) => mark(tt) 
    active(isNatural(head(X))) => mark(isLNat(X)) 
    active(isNatural(s(X))) => mark(isNatural(X)) 
    active(isNatural(sel(X, Y))) => mark(and(isNatural(X), isLNat(Y))) 
    active(isPLNat(pair(X, Y))) => mark(and(isLNat(X), isLNat(Y))) 
    active(isPLNat(splitAt(X, Y))) => mark(and(isNatural(X), isLNat(Y))) 
    active(natsFrom(X)) => mark(u41(isNatural(X), X)) 
    active(sel(X, Y)) => mark(u51(and(isNatural(X), isLNat(Y)), X, Y)) 
    active(snd(pair(X, Y))) => mark(u61(and(isLNat(X), isLNat(Y)), Y)) 
    active(splitAt(0, X)) => mark(u71(isLNat(X), X)) 
    active(splitAt(s(X), cons(Y, Z))) => mark(u81(and(isNatural(X), and(isNatural(Y), isLNat(Z))), X, Y, Z)) 
    active(tail(cons(X, Y))) => mark(u91(and(isNatural(X), isLNat(Y)), Y)) 
    active(take(X, Y)) => mark(u101(and(isNatural(X), isLNat(Y)), X, Y)) 
    mark(u101(X, Y, Z)) => active(u101(mark(X), Y, Z)) 
    mark(tt) => active(tt) 
    mark(fst(X)) => active(fst(mark(X))) 
    mark(splitAt(X, Y)) => active(splitAt(mark(X), mark(Y))) 
    mark(u11(X, Y, Z)) => active(u11(mark(X), Y, Z)) 
    mark(snd(X)) => active(snd(mark(X))) 
    mark(u21(X, Y)) => active(u21(mark(X), Y)) 
    mark(u31(X, Y)) => active(u31(mark(X), Y)) 
    mark(u41(X, Y)) => active(u41(mark(X), Y)) 
    mark(cons(X, Y)) => active(cons(mark(X), Y)) 
    mark(natsFrom(X)) => active(natsFrom(mark(X))) 
    mark(s(X)) => active(s(mark(X))) 
    mark(u51(X, Y, Z)) => active(u51(mark(X), Y, Z)) 
    mark(head(X)) => active(head(mark(X))) 
    mark(afterNth(X, Y)) => active(afterNth(mark(X), mark(Y))) 
    mark(u61(X, Y)) => active(u61(mark(X), Y)) 
    mark(u71(X, Y)) => active(u71(mark(X), Y)) 
    mark(pair(X, Y)) => active(pair(mark(X), mark(Y))) 
    mark(nil) => active(nil) 
    mark(u81(X, Y, Z, U)) => active(u81(mark(X), Y, Z, U)) 
    mark(u82(X, Y)) => active(u82(mark(X), Y)) 
    mark(u91(X, Y)) => active(u91(mark(X), Y)) 
    mark(and(X, Y)) => active(and(mark(X), Y)) 
    mark(isNatural(X)) => active(isNatural(X)) 
    mark(isLNat(X)) => active(isLNat(X)) 
    mark(isPLNat(X)) => active(isPLNat(X)) 
    mark(tail(X)) => active(tail(mark(X))) 
    mark(take(X, Y)) => active(take(mark(X), mark(Y))) 
    mark(0) => active(0) 
    mark(sel(X, Y)) => active(sel(mark(X), mark(Y))) 
    u101(mark(X), Y, Z) => u101(X, Y, Z) 
    u101(X, mark(Y), Z) => u101(X, Y, Z) 
    u101(X, Y, mark(Z)) => u101(X, Y, Z) 
    u101(active(X), Y, Z) => u101(X, Y, Z) 
    u101(X, active(Y), Z) => u101(X, Y, Z) 
    u101(X, Y, active(Z)) => u101(X, Y, Z) 
    fst(mark(X)) => fst(X) 
    fst(active(X)) => fst(X) 
    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) 
    u11(mark(X), Y, Z) => u11(X, Y, Z) 
    u11(X, mark(Y), Z) => u11(X, Y, Z) 
    u11(X, Y, mark(Z)) => u11(X, Y, Z) 
    u11(active(X), Y, Z) => u11(X, Y, Z) 
    u11(X, active(Y), Z) => u11(X, Y, Z) 
    u11(X, Y, active(Z)) => u11(X, Y, Z) 
    snd(mark(X)) => snd(X) 
    snd(active(X)) => snd(X) 
    u21(mark(X), Y) => u21(X, Y) 
    u21(X, mark(Y)) => u21(X, Y) 
    u21(active(X), Y) => u21(X, Y) 
    u21(X, active(Y)) => u21(X, Y) 
    u31(mark(X), Y) => u31(X, Y) 
    u31(X, mark(Y)) => u31(X, Y) 
    u31(active(X), Y) => u31(X, Y) 
    u31(X, active(Y)) => u31(X, Y) 
    u41(mark(X), Y) => u41(X, Y) 
    u41(X, mark(Y)) => u41(X, Y) 
    u41(active(X), Y) => u41(X, Y) 
    u41(X, active(Y)) => u41(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) 
    natsFrom(mark(X)) => natsFrom(X) 
    natsFrom(active(X)) => natsFrom(X) 
    s(mark(X)) => s(X) 
    s(active(X)) => s(X) 
    u51(mark(X), Y, Z) => u51(X, Y, Z) 
    u51(X, mark(Y), Z) => u51(X, Y, Z) 
    u51(X, Y, mark(Z)) => u51(X, Y, Z) 
    u51(active(X), Y, Z) => u51(X, Y, Z) 
    u51(X, active(Y), Z) => u51(X, Y, Z) 
    u51(X, Y, active(Z)) => u51(X, Y, Z) 
    head(mark(X)) => head(X) 
    head(active(X)) => head(X) 
    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) 
    u61(mark(X), Y) => u61(X, Y) 
    u61(X, mark(Y)) => u61(X, Y) 
    u61(active(X), Y) => u61(X, Y) 
    u61(X, active(Y)) => u61(X, Y) 
    u71(mark(X), Y) => u71(X, Y) 
    u71(X, mark(Y)) => u71(X, Y) 
    u71(active(X), Y) => u71(X, Y) 
    u71(X, active(Y)) => u71(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) 
    u81(mark(X), Y, Z, U) => u81(X, Y, Z, U) 
    u81(X, mark(Y), Z, U) => u81(X, Y, Z, U) 
    u81(X, Y, mark(Z), U) => u81(X, Y, Z, U) 
    u81(X, Y, Z, mark(U)) => u81(X, Y, Z, U) 
    u81(active(X), Y, Z, U) => u81(X, Y, Z, U) 
    u81(X, active(Y), Z, U) => u81(X, Y, Z, U) 
    u81(X, Y, active(Z), U) => u81(X, Y, Z, U) 
    u81(X, Y, Z, active(U)) => u81(X, Y, Z, U) 
    u82(mark(X), Y) => u82(X, Y) 
    u82(X, mark(Y)) => u82(X, Y) 
    u82(active(X), Y) => u82(X, Y) 
    u82(X, active(Y)) => u82(X, Y) 
    u91(mark(X), Y) => u91(X, Y) 
    u91(X, mark(Y)) => u91(X, Y) 
    u91(active(X), Y) => u91(X, Y) 
    u91(X, active(Y)) => u91(X, Y) 
    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) 
    isNatural(mark(X)) => isNatural(X) 
    isNatural(active(X)) => isNatural(X) 
    isLNat(mark(X)) => isLNat(X) 
    isLNat(active(X)) => isLNat(X) 
    isPLNat(mark(X)) => isPLNat(X) 
    isPLNat(active(X)) => isPLNat(X) 
    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) 
    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) 
    map(/\x.X(x), nil) => nil 
    app(/\x.X(x), Y) => X(Y) 

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

  active(u101(tt, X, Y)) => mark(fst(splitAt(X, Y))) 
  active(u11(tt, X, Y)) => mark(snd(splitAt(X, Y))) 
  active(u21(tt, X)) => mark(X) 
  active(u31(tt, X)) => mark(X) 
  active(u41(tt, X)) => mark(cons(X, natsFrom(s(X)))) 
  active(u51(tt, X, Y)) => mark(head(afterNth(X, Y))) 
  active(u61(tt, X)) => mark(X) 
  active(u71(tt, X)) => mark(pair(nil, X)) 
  active(u81(tt, X, Y, Z)) => mark(u82(splitAt(X, Z), Y)) 
  active(u82(pair(X, Y), Z)) => mark(pair(cons(Z, X), Y)) 
  active(u91(tt, X)) => mark(X) 
  active(afterNth(X, Y)) => mark(u11(and(isNatural(X), isLNat(Y)), X, Y)) 
  active(and(tt, X)) => mark(X) 
  active(fst(pair(X, Y))) => mark(u21(and(isLNat(X), isLNat(Y)), X)) 
  active(head(cons(X, Y))) => mark(u31(and(isNatural(X), isLNat(Y)), X)) 
  active(isLNat(nil)) => mark(tt) 
  active(isLNat(afterNth(X, Y))) => mark(and(isNatural(X), isLNat(Y))) 
  active(isLNat(cons(X, Y))) => mark(and(isNatural(X), isLNat(Y))) 
  active(isLNat(fst(X))) => mark(isPLNat(X)) 
  active(isLNat(natsFrom(X))) => mark(isNatural(X)) 
  active(isLNat(snd(X))) => mark(isPLNat(X)) 
  active(isLNat(tail(X))) => mark(isLNat(X)) 
  active(isLNat(take(X, Y))) => mark(and(isNatural(X), isLNat(Y))) 
  active(isNatural(0)) => mark(tt) 
  active(isNatural(head(X))) => mark(isLNat(X)) 
  active(isNatural(s(X))) => mark(isNatural(X)) 
  active(isNatural(sel(X, Y))) => mark(and(isNatural(X), isLNat(Y))) 
  active(isPLNat(pair(X, Y))) => mark(and(isLNat(X), isLNat(Y))) 
  active(isPLNat(splitAt(X, Y))) => mark(and(isNatural(X), isLNat(Y))) 
  active(natsFrom(X)) => mark(u41(isNatural(X), X)) 
  active(sel(X, Y)) => mark(u51(and(isNatural(X), isLNat(Y)), X, Y)) 
  active(snd(pair(X, Y))) => mark(u61(and(isLNat(X), isLNat(Y)), Y)) 
  active(splitAt(0, X)) => mark(u71(isLNat(X), X)) 
  active(splitAt(s(X), cons(Y, Z))) => mark(u81(and(isNatural(X), and(isNatural(Y), isLNat(Z))), X, Y, Z)) 
  active(tail(cons(X, Y))) => mark(u91(and(isNatural(X), isLNat(Y)), Y)) 
  active(take(X, Y)) => mark(u101(and(isNatural(X), isLNat(Y)), X, Y)) 
  mark(u101(X, Y, Z)) => active(u101(mark(X), Y, Z)) 
  mark(tt) => active(tt) 
  mark(fst(X)) => active(fst(mark(X))) 
  mark(splitAt(X, Y)) => active(splitAt(mark(X), mark(Y))) 
  mark(u11(X, Y, Z)) => active(u11(mark(X), Y, Z)) 
  mark(snd(X)) => active(snd(mark(X))) 
  mark(u21(X, Y)) => active(u21(mark(X), Y)) 
  mark(u31(X, Y)) => active(u31(mark(X), Y)) 
  mark(u41(X, Y)) => active(u41(mark(X), Y)) 
  mark(cons(X, Y)) => active(cons(mark(X), Y)) 
  mark(natsFrom(X)) => active(natsFrom(mark(X))) 
  mark(s(X)) => active(s(mark(X))) 
  mark(u51(X, Y, Z)) => active(u51(mark(X), Y, Z)) 
  mark(head(X)) => active(head(mark(X))) 
  mark(afterNth(X, Y)) => active(afterNth(mark(X), mark(Y))) 
  mark(u61(X, Y)) => active(u61(mark(X), Y)) 
  mark(u71(X, Y)) => active(u71(mark(X), Y)) 
  mark(pair(X, Y)) => active(pair(mark(X), mark(Y))) 
  mark(nil) => active(nil) 
  mark(u81(X, Y, Z, U)) => active(u81(mark(X), Y, Z, U)) 
  mark(u82(X, Y)) => active(u82(mark(X), Y)) 
  mark(u91(X, Y)) => active(u91(mark(X), Y)) 
  mark(and(X, Y)) => active(and(mark(X), Y)) 
  mark(isNatural(X)) => active(isNatural(X)) 
  mark(isLNat(X)) => active(isLNat(X)) 
  mark(isPLNat(X)) => active(isPLNat(X)) 
  mark(tail(X)) => active(tail(mark(X))) 
  mark(take(X, Y)) => active(take(mark(X), mark(Y))) 
  mark(0) => active(0) 
  mark(sel(X, Y)) => active(sel(mark(X), mark(Y))) 
  u101(mark(X), Y, Z) => u101(X, Y, Z) 
  u101(X, mark(Y), Z) => u101(X, Y, Z) 
  u101(X, Y, mark(Z)) => u101(X, Y, Z) 
  u101(active(X), Y, Z) => u101(X, Y, Z) 
  u101(X, active(Y), Z) => u101(X, Y, Z) 
  u101(X, Y, active(Z)) => u101(X, Y, Z) 
  fst(mark(X)) => fst(X) 
  fst(active(X)) => fst(X) 
  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) 
  u11(mark(X), Y, Z) => u11(X, Y, Z) 
  u11(X, mark(Y), Z) => u11(X, Y, Z) 
  u11(X, Y, mark(Z)) => u11(X, Y, Z) 
  u11(active(X), Y, Z) => u11(X, Y, Z) 
  u11(X, active(Y), Z) => u11(X, Y, Z) 
  u11(X, Y, active(Z)) => u11(X, Y, Z) 
  snd(mark(X)) => snd(X) 
  snd(active(X)) => snd(X) 
  u21(mark(X), Y) => u21(X, Y) 
  u21(X, mark(Y)) => u21(X, Y) 
  u21(active(X), Y) => u21(X, Y) 
  u21(X, active(Y)) => u21(X, Y) 
  u31(mark(X), Y) => u31(X, Y) 
  u31(X, mark(Y)) => u31(X, Y) 
  u31(active(X), Y) => u31(X, Y) 
  u31(X, active(Y)) => u31(X, Y) 
  u41(mark(X), Y) => u41(X, Y) 
  u41(X, mark(Y)) => u41(X, Y) 
  u41(active(X), Y) => u41(X, Y) 
  u41(X, active(Y)) => u41(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) 
  natsFrom(mark(X)) => natsFrom(X) 
  natsFrom(active(X)) => natsFrom(X) 
  s(mark(X)) => s(X) 
  s(active(X)) => s(X) 
  u51(mark(X), Y, Z) => u51(X, Y, Z) 
  u51(X, mark(Y), Z) => u51(X, Y, Z) 
  u51(X, Y, mark(Z)) => u51(X, Y, Z) 
  u51(active(X), Y, Z) => u51(X, Y, Z) 
  u51(X, active(Y), Z) => u51(X, Y, Z) 
  u51(X, Y, active(Z)) => u51(X, Y, Z) 
  head(mark(X)) => head(X) 
  head(active(X)) => head(X) 
  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) 
  u61(mark(X), Y) => u61(X, Y) 
  u61(X, mark(Y)) => u61(X, Y) 
  u61(active(X), Y) => u61(X, Y) 
  u61(X, active(Y)) => u61(X, Y) 
  u71(mark(X), Y) => u71(X, Y) 
  u71(X, mark(Y)) => u71(X, Y) 
  u71(active(X), Y) => u71(X, Y) 
  u71(X, active(Y)) => u71(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) 
  u81(mark(X), Y, Z, U) => u81(X, Y, Z, U) 
  u81(X, mark(Y), Z, U) => u81(X, Y, Z, U) 
  u81(X, Y, mark(Z), U) => u81(X, Y, Z, U) 
  u81(X, Y, Z, mark(U)) => u81(X, Y, Z, U) 
  u81(active(X), Y, Z, U) => u81(X, Y, Z, U) 
  u81(X, active(Y), Z, U) => u81(X, Y, Z, U) 
  u81(X, Y, active(Z), U) => u81(X, Y, Z, U) 
  u81(X, Y, Z, active(U)) => u81(X, Y, Z, U) 
  u82(mark(X), Y) => u82(X, Y) 
  u82(X, mark(Y)) => u82(X, Y) 
  u82(active(X), Y) => u82(X, Y) 
  u82(X, active(Y)) => u82(X, Y) 
  u91(mark(X), Y) => u91(X, Y) 
  u91(X, mark(Y)) => u91(X, Y) 
  u91(active(X), Y) => u91(X, Y) 
  u91(X, active(Y)) => u91(X, Y) 
  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) 
  isNatural(mark(X)) => isNatural(X) 
  isNatural(active(X)) => isNatural(X) 
  isLNat(mark(X)) => isLNat(X) 
  isLNat(active(X)) => isLNat(X) 
  isPLNat(mark(X)) => isPLNat(X) 
  isPLNat(active(X)) => isPLNat(X) 
  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) 
  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) 

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(u101(tt(),PeRCenTX,PeRCenTY)) -> mark(fst(splitAt(PeRCenTX,PeRCenTY)))
 ||     2: active(u11(tt(),PeRCenTX,PeRCenTY)) -> mark(snd(splitAt(PeRCenTX,PeRCenTY)))
 ||     3: active(u21(tt(),PeRCenTX)) -> mark(PeRCenTX)
 ||     4: active(u31(tt(),PeRCenTX)) -> mark(PeRCenTX)
 ||     5: active(u41(tt(),PeRCenTX)) -> mark(cons(PeRCenTX,natsFrom(s(PeRCenTX))))
 ||     6: active(u51(tt(),PeRCenTX,PeRCenTY)) -> mark(head(afterNth(PeRCenTX,PeRCenTY)))
 ||     7: active(u61(tt(),PeRCenTX)) -> mark(PeRCenTX)
 ||     8: active(u71(tt(),PeRCenTX)) -> mark(pair(nil(),PeRCenTX))
 ||     9: active(u81(tt(),PeRCenTX,PeRCenTY,PeRCenTZ)) -> mark(u82(splitAt(PeRCenTX,PeRCenTZ),PeRCenTY))
 ||     10: active(u82(pair(PeRCenTX,PeRCenTY),PeRCenTZ)) -> mark(pair(cons(PeRCenTZ,PeRCenTX),PeRCenTY))
 ||     11: active(u91(tt(),PeRCenTX)) -> mark(PeRCenTX)
 ||     12: active(afterNth(PeRCenTX,PeRCenTY)) -> mark(u11(and(isNatural(PeRCenTX),isLNat(PeRCenTY)),PeRCenTX,PeRCenTY))
 ||     13: active(and(tt(),PeRCenTX)) -> mark(PeRCenTX)
 ||     14: active(fst(pair(PeRCenTX,PeRCenTY))) -> mark(u21(and(isLNat(PeRCenTX),isLNat(PeRCenTY)),PeRCenTX))
 ||     15: active(head(cons(PeRCenTX,PeRCenTY))) -> mark(u31(and(isNatural(PeRCenTX),isLNat(PeRCenTY)),PeRCenTX))
 ||     16: active(isLNat(nil())) -> mark(tt())
 ||     17: active(isLNat(afterNth(PeRCenTX,PeRCenTY))) -> mark(and(isNatural(PeRCenTX),isLNat(PeRCenTY)))
 ||     18: active(isLNat(cons(PeRCenTX,PeRCenTY))) -> mark(and(isNatural(PeRCenTX),isLNat(PeRCenTY)))
 ||     19: active(isLNat(fst(PeRCenTX))) -> mark(isPLNat(PeRCenTX))
 ||     20: active(isLNat(natsFrom(PeRCenTX))) -> mark(isNatural(PeRCenTX))
 ||     21: active(isLNat(snd(PeRCenTX))) -> mark(isPLNat(PeRCenTX))
 ||     22: active(isLNat(tail(PeRCenTX))) -> mark(isLNat(PeRCenTX))
 ||     23: active(isLNat(take(PeRCenTX,PeRCenTY))) -> mark(and(isNatural(PeRCenTX),isLNat(PeRCenTY)))
 ||     24: active(isNatural(0())) -> mark(tt())
 ||     25: active(isNatural(head(PeRCenTX))) -> mark(isLNat(PeRCenTX))
 ||     26: active(isNatural(s(PeRCenTX))) -> mark(isNatural(PeRCenTX))
 ||     27: active(isNatural(sel(PeRCenTX,PeRCenTY))) -> mark(and(isNatural(PeRCenTX),isLNat(PeRCenTY)))
 ||     28: active(isPLNat(pair(PeRCenTX,PeRCenTY))) -> mark(and(isLNat(PeRCenTX),isLNat(PeRCenTY)))
 ||     29: active(isPLNat(splitAt(PeRCenTX,PeRCenTY))) -> mark(and(isNatural(PeRCenTX),isLNat(PeRCenTY)))
 ||     30: active(natsFrom(PeRCenTX)) -> mark(u41(isNatural(PeRCenTX),PeRCenTX))
 ||     31: active(sel(PeRCenTX,PeRCenTY)) -> mark(u51(and(isNatural(PeRCenTX),isLNat(PeRCenTY)),PeRCenTX,PeRCenTY))
 ||     32: active(snd(pair(PeRCenTX,PeRCenTY))) -> mark(u61(and(isLNat(PeRCenTX),isLNat(PeRCenTY)),PeRCenTY))
 ||     33: active(splitAt(0(),PeRCenTX)) -> mark(u71(isLNat(PeRCenTX),PeRCenTX))
 ||     34: active(splitAt(s(PeRCenTX),cons(PeRCenTY,PeRCenTZ))) -> mark(u81(and(isNatural(PeRCenTX),and(isNatural(PeRCenTY),isLNat(PeRCenTZ))),PeRCenTX,PeRCenTY,PeRCenTZ))
 ||     35: active(tail(cons(PeRCenTX,PeRCenTY))) -> mark(u91(and(isNatural(PeRCenTX),isLNat(PeRCenTY)),PeRCenTY))
 ||     36: active(take(PeRCenTX,PeRCenTY)) -> mark(u101(and(isNatural(PeRCenTX),isLNat(PeRCenTY)),PeRCenTX,PeRCenTY))
 ||     37: mark(u101(PeRCenTX,PeRCenTY,PeRCenTZ)) -> active(u101(mark(PeRCenTX),PeRCenTY,PeRCenTZ))
 ||     38: mark(tt()) -> active(tt())
 ||     39: mark(fst(PeRCenTX)) -> active(fst(mark(PeRCenTX)))
 ||     40: mark(splitAt(PeRCenTX,PeRCenTY)) -> active(splitAt(mark(PeRCenTX),mark(PeRCenTY)))
 ||     41: mark(u11(PeRCenTX,PeRCenTY,PeRCenTZ)) -> active(u11(mark(PeRCenTX),PeRCenTY,PeRCenTZ))
 ||     42: mark(snd(PeRCenTX)) -> active(snd(mark(PeRCenTX)))
 ||     43: mark(u21(PeRCenTX,PeRCenTY)) -> active(u21(mark(PeRCenTX),PeRCenTY))
 ||     44: mark(u31(PeRCenTX,PeRCenTY)) -> active(u31(mark(PeRCenTX),PeRCenTY))
 ||     45: mark(u41(PeRCenTX,PeRCenTY)) -> active(u41(mark(PeRCenTX),PeRCenTY))
 ||     46: mark(cons(PeRCenTX,PeRCenTY)) -> active(cons(mark(PeRCenTX),PeRCenTY))
 ||     47: mark(natsFrom(PeRCenTX)) -> active(natsFrom(mark(PeRCenTX)))
 ||     48: mark(s(PeRCenTX)) -> active(s(mark(PeRCenTX)))
 ||     49: mark(u51(PeRCenTX,PeRCenTY,PeRCenTZ)) -> active(u51(mark(PeRCenTX),PeRCenTY,PeRCenTZ))
 ||     50: mark(head(PeRCenTX)) -> active(head(mark(PeRCenTX)))
 ||     51: mark(afterNth(PeRCenTX,PeRCenTY)) -> active(afterNth(mark(PeRCenTX),mark(PeRCenTY)))
 ||     52: mark(u61(PeRCenTX,PeRCenTY)) -> active(u61(mark(PeRCenTX),PeRCenTY))
 ||     53: mark(u71(PeRCenTX,PeRCenTY)) -> active(u71(mark(PeRCenTX),PeRCenTY))
 ||     54: mark(pair(PeRCenTX,PeRCenTY)) -> active(pair(mark(PeRCenTX),mark(PeRCenTY)))
 ||     55: mark(nil()) -> active(nil())
 ||     56: mark(u81(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> active(u81(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU))
 ||     57: mark(u82(PeRCenTX,PeRCenTY)) -> active(u82(mark(PeRCenTX),PeRCenTY))
 ||     58: mark(u91(PeRCenTX,PeRCenTY)) -> active(u91(mark(PeRCenTX),PeRCenTY))
 ||     59: mark(and(PeRCenTX,PeRCenTY)) -> active(and(mark(PeRCenTX),PeRCenTY))
 ||     60: mark(isNatural(PeRCenTX)) -> active(isNatural(PeRCenTX))
 ||     61: mark(isLNat(PeRCenTX)) -> active(isLNat(PeRCenTX))
 ||     62: mark(isPLNat(PeRCenTX)) -> active(isPLNat(PeRCenTX))
 ||     63: mark(tail(PeRCenTX)) -> active(tail(mark(PeRCenTX)))
 ||     64: mark(take(PeRCenTX,PeRCenTY)) -> active(take(mark(PeRCenTX),mark(PeRCenTY)))
 ||     65: mark(0()) -> active(0())
 ||     66: mark(sel(PeRCenTX,PeRCenTY)) -> active(sel(mark(PeRCenTX),mark(PeRCenTY)))
 ||     67: u101(mark(PeRCenTX),PeRCenTY,PeRCenTZ) -> u101(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||     68: u101(PeRCenTX,mark(PeRCenTY),PeRCenTZ) -> u101(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||     69: u101(PeRCenTX,PeRCenTY,mark(PeRCenTZ)) -> u101(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||     70: u101(active(PeRCenTX),PeRCenTY,PeRCenTZ) -> u101(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||     71: u101(PeRCenTX,active(PeRCenTY),PeRCenTZ) -> u101(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||     72: u101(PeRCenTX,PeRCenTY,active(PeRCenTZ)) -> u101(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||     73: fst(mark(PeRCenTX)) -> fst(PeRCenTX)
 ||     74: fst(active(PeRCenTX)) -> fst(PeRCenTX)
 ||     75: splitAt(mark(PeRCenTX),PeRCenTY) -> splitAt(PeRCenTX,PeRCenTY)
 ||     76: splitAt(PeRCenTX,mark(PeRCenTY)) -> splitAt(PeRCenTX,PeRCenTY)
 ||     77: splitAt(active(PeRCenTX),PeRCenTY) -> splitAt(PeRCenTX,PeRCenTY)
 ||     78: splitAt(PeRCenTX,active(PeRCenTY)) -> splitAt(PeRCenTX,PeRCenTY)
 ||     79: u11(mark(PeRCenTX),PeRCenTY,PeRCenTZ) -> u11(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||     80: u11(PeRCenTX,mark(PeRCenTY),PeRCenTZ) -> u11(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||     81: u11(PeRCenTX,PeRCenTY,mark(PeRCenTZ)) -> u11(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||     82: u11(active(PeRCenTX),PeRCenTY,PeRCenTZ) -> u11(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||     83: u11(PeRCenTX,active(PeRCenTY),PeRCenTZ) -> u11(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||     84: u11(PeRCenTX,PeRCenTY,active(PeRCenTZ)) -> u11(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||     85: snd(mark(PeRCenTX)) -> snd(PeRCenTX)
 ||     86: snd(active(PeRCenTX)) -> snd(PeRCenTX)
 ||     87: u21(mark(PeRCenTX),PeRCenTY) -> u21(PeRCenTX,PeRCenTY)
 ||     88: u21(PeRCenTX,mark(PeRCenTY)) -> u21(PeRCenTX,PeRCenTY)
 ||     89: u21(active(PeRCenTX),PeRCenTY) -> u21(PeRCenTX,PeRCenTY)
 ||     90: u21(PeRCenTX,active(PeRCenTY)) -> u21(PeRCenTX,PeRCenTY)
 ||     91: u31(mark(PeRCenTX),PeRCenTY) -> u31(PeRCenTX,PeRCenTY)
 ||     92: u31(PeRCenTX,mark(PeRCenTY)) -> u31(PeRCenTX,PeRCenTY)
 ||     93: u31(active(PeRCenTX),PeRCenTY) -> u31(PeRCenTX,PeRCenTY)
 ||     94: u31(PeRCenTX,active(PeRCenTY)) -> u31(PeRCenTX,PeRCenTY)
 ||     95: u41(mark(PeRCenTX),PeRCenTY) -> u41(PeRCenTX,PeRCenTY)
 ||     96: u41(PeRCenTX,mark(PeRCenTY)) -> u41(PeRCenTX,PeRCenTY)
 ||     97: u41(active(PeRCenTX),PeRCenTY) -> u41(PeRCenTX,PeRCenTY)
 ||     98: u41(PeRCenTX,active(PeRCenTY)) -> u41(PeRCenTX,PeRCenTY)
 ||     99: cons(mark(PeRCenTX),PeRCenTY) -> cons(PeRCenTX,PeRCenTY)
 ||     100: cons(PeRCenTX,mark(PeRCenTY)) -> cons(PeRCenTX,PeRCenTY)
 ||     101: cons(active(PeRCenTX),PeRCenTY) -> cons(PeRCenTX,PeRCenTY)
 ||     102: cons(PeRCenTX,active(PeRCenTY)) -> cons(PeRCenTX,PeRCenTY)
 ||     103: natsFrom(mark(PeRCenTX)) -> natsFrom(PeRCenTX)
 ||     104: natsFrom(active(PeRCenTX)) -> natsFrom(PeRCenTX)
 ||     105: s(mark(PeRCenTX)) -> s(PeRCenTX)
 ||     106: s(active(PeRCenTX)) -> s(PeRCenTX)
 ||     107: u51(mark(PeRCenTX),PeRCenTY,PeRCenTZ) -> u51(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||     108: u51(PeRCenTX,mark(PeRCenTY),PeRCenTZ) -> u51(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||     109: u51(PeRCenTX,PeRCenTY,mark(PeRCenTZ)) -> u51(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||     110: u51(active(PeRCenTX),PeRCenTY,PeRCenTZ) -> u51(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||     111: u51(PeRCenTX,active(PeRCenTY),PeRCenTZ) -> u51(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||     112: u51(PeRCenTX,PeRCenTY,active(PeRCenTZ)) -> u51(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||     113: head(mark(PeRCenTX)) -> head(PeRCenTX)
 ||     114: head(active(PeRCenTX)) -> head(PeRCenTX)
 ||     115: afterNth(mark(PeRCenTX),PeRCenTY) -> afterNth(PeRCenTX,PeRCenTY)
 ||     116: afterNth(PeRCenTX,mark(PeRCenTY)) -> afterNth(PeRCenTX,PeRCenTY)
 ||     117: afterNth(active(PeRCenTX),PeRCenTY) -> afterNth(PeRCenTX,PeRCenTY)
 ||     118: afterNth(PeRCenTX,active(PeRCenTY)) -> afterNth(PeRCenTX,PeRCenTY)
 ||     119: u61(mark(PeRCenTX),PeRCenTY) -> u61(PeRCenTX,PeRCenTY)
 ||     120: u61(PeRCenTX,mark(PeRCenTY)) -> u61(PeRCenTX,PeRCenTY)
 ||     121: u61(active(PeRCenTX),PeRCenTY) -> u61(PeRCenTX,PeRCenTY)
 ||     122: u61(PeRCenTX,active(PeRCenTY)) -> u61(PeRCenTX,PeRCenTY)
 ||     123: u71(mark(PeRCenTX),PeRCenTY) -> u71(PeRCenTX,PeRCenTY)
 ||     124: u71(PeRCenTX,mark(PeRCenTY)) -> u71(PeRCenTX,PeRCenTY)
 ||     125: u71(active(PeRCenTX),PeRCenTY) -> u71(PeRCenTX,PeRCenTY)
 ||     126: u71(PeRCenTX,active(PeRCenTY)) -> u71(PeRCenTX,PeRCenTY)
 ||     127: pair(mark(PeRCenTX),PeRCenTY) -> pair(PeRCenTX,PeRCenTY)
 ||     128: pair(PeRCenTX,mark(PeRCenTY)) -> pair(PeRCenTX,PeRCenTY)
 ||     129: pair(active(PeRCenTX),PeRCenTY) -> pair(PeRCenTX,PeRCenTY)
 ||     130: pair(PeRCenTX,active(PeRCenTY)) -> pair(PeRCenTX,PeRCenTY)
 ||     131: u81(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU) -> u81(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||     132: u81(PeRCenTX,mark(PeRCenTY),PeRCenTZ,PeRCenTU) -> u81(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||     133: u81(PeRCenTX,PeRCenTY,mark(PeRCenTZ),PeRCenTU) -> u81(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||     134: u81(PeRCenTX,PeRCenTY,PeRCenTZ,mark(PeRCenTU)) -> u81(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||     135: u81(active(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU) -> u81(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||     136: u81(PeRCenTX,active(PeRCenTY),PeRCenTZ,PeRCenTU) -> u81(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||     137: u81(PeRCenTX,PeRCenTY,active(PeRCenTZ),PeRCenTU) -> u81(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||     138: u81(PeRCenTX,PeRCenTY,PeRCenTZ,active(PeRCenTU)) -> u81(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||     139: u82(mark(PeRCenTX),PeRCenTY) -> u82(PeRCenTX,PeRCenTY)
 ||     140: u82(PeRCenTX,mark(PeRCenTY)) -> u82(PeRCenTX,PeRCenTY)
 ||     141: u82(active(PeRCenTX),PeRCenTY) -> u82(PeRCenTX,PeRCenTY)
 ||     142: u82(PeRCenTX,active(PeRCenTY)) -> u82(PeRCenTX,PeRCenTY)
 ||     143: u91(mark(PeRCenTX),PeRCenTY) -> u91(PeRCenTX,PeRCenTY)
 ||     144: u91(PeRCenTX,mark(PeRCenTY)) -> u91(PeRCenTX,PeRCenTY)
 ||     145: u91(active(PeRCenTX),PeRCenTY) -> u91(PeRCenTX,PeRCenTY)
 ||     146: u91(PeRCenTX,active(PeRCenTY)) -> u91(PeRCenTX,PeRCenTY)
 ||     147: and(mark(PeRCenTX),PeRCenTY) -> and(PeRCenTX,PeRCenTY)
 ||     148: and(PeRCenTX,mark(PeRCenTY)) -> and(PeRCenTX,PeRCenTY)
 ||     149: and(active(PeRCenTX),PeRCenTY) -> and(PeRCenTX,PeRCenTY)
 ||     150: and(PeRCenTX,active(PeRCenTY)) -> and(PeRCenTX,PeRCenTY)
 ||     151: isNatural(mark(PeRCenTX)) -> isNatural(PeRCenTX)
 ||     152: isNatural(active(PeRCenTX)) -> isNatural(PeRCenTX)
 ||     153: isLNat(mark(PeRCenTX)) -> isLNat(PeRCenTX)
 ||     154: isLNat(active(PeRCenTX)) -> isLNat(PeRCenTX)
 ||     155: isPLNat(mark(PeRCenTX)) -> isPLNat(PeRCenTX)
 ||     156: isPLNat(active(PeRCenTX)) -> isPLNat(PeRCenTX)
 ||     157: tail(mark(PeRCenTX)) -> tail(PeRCenTX)
 ||     158: tail(active(PeRCenTX)) -> tail(PeRCenTX)
 ||     159: take(mark(PeRCenTX),PeRCenTY) -> take(PeRCenTX,PeRCenTY)
 ||     160: take(PeRCenTX,mark(PeRCenTY)) -> take(PeRCenTX,PeRCenTY)
 ||     161: take(active(PeRCenTX),PeRCenTY) -> take(PeRCenTX,PeRCenTY)
 ||     162: take(PeRCenTX,active(PeRCenTY)) -> take(PeRCenTX,PeRCenTY)
 ||     163: sel(mark(PeRCenTX),PeRCenTY) -> sel(PeRCenTX,PeRCenTY)
 ||     164: sel(PeRCenTX,mark(PeRCenTY)) -> sel(PeRCenTX,PeRCenTY)
 ||     165: sel(active(PeRCenTX),PeRCenTY) -> sel(PeRCenTX,PeRCenTY)
 ||     166: sel(PeRCenTX,active(PeRCenTY)) -> sel(PeRCenTX,PeRCenTY)
 ||     167: TIlDePAIR(PeRCenTX,PeRCenTY) -> PeRCenTX
 ||     168: TIlDePAIR(PeRCenTX,PeRCenTY) -> PeRCenTY
 || Number of strict rules: 168
 || Direct POLO(bPol) ... failed.
 || Uncurrying ... failed.
 || Dependency Pairs:
 ||    #1: #active(u11(tt(),PeRCenTX,PeRCenTY)) -> #mark(snd(splitAt(PeRCenTX,PeRCenTY)))
 ||    #2: #active(u11(tt(),PeRCenTX,PeRCenTY)) -> #snd(splitAt(PeRCenTX,PeRCenTY))
 ||    #3: #active(u11(tt(),PeRCenTX,PeRCenTY)) -> #splitAt(PeRCenTX,PeRCenTY)
 ||    #4: #snd(active(PeRCenTX)) -> #snd(PeRCenTX)
 ||    #5: #mark(u21(PeRCenTX,PeRCenTY)) -> #active(u21(mark(PeRCenTX),PeRCenTY))
 ||    #6: #mark(u21(PeRCenTX,PeRCenTY)) -> #u21(mark(PeRCenTX),PeRCenTY)
 ||    #7: #mark(u21(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #8: #active(isPLNat(splitAt(PeRCenTX,PeRCenTY))) -> #mark(and(isNatural(PeRCenTX),isLNat(PeRCenTY)))
 ||    #9: #active(isPLNat(splitAt(PeRCenTX,PeRCenTY))) -> #and(isNatural(PeRCenTX),isLNat(PeRCenTY))
 ||    #10: #active(isPLNat(splitAt(PeRCenTX,PeRCenTY))) -> #isNatural(PeRCenTX)
 ||    #11: #active(isPLNat(splitAt(PeRCenTX,PeRCenTY))) -> #isLNat(PeRCenTY)
 ||    #12: #active(tail(cons(PeRCenTX,PeRCenTY))) -> #mark(u91(and(isNatural(PeRCenTX),isLNat(PeRCenTY)),PeRCenTY))
 ||    #13: #active(tail(cons(PeRCenTX,PeRCenTY))) -> #u91(and(isNatural(PeRCenTX),isLNat(PeRCenTY)),PeRCenTY)
 ||    #14: #active(tail(cons(PeRCenTX,PeRCenTY))) -> #and(isNatural(PeRCenTX),isLNat(PeRCenTY))
 ||    #15: #active(tail(cons(PeRCenTX,PeRCenTY))) -> #isNatural(PeRCenTX)
 ||    #16: #active(tail(cons(PeRCenTX,PeRCenTY))) -> #isLNat(PeRCenTY)
 ||    #17: #u11(PeRCenTX,active(PeRCenTY),PeRCenTZ) -> #u11(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||    #18: #mark(sel(PeRCenTX,PeRCenTY)) -> #active(sel(mark(PeRCenTX),mark(PeRCenTY)))
 ||    #19: #mark(sel(PeRCenTX,PeRCenTY)) -> #sel(mark(PeRCenTX),mark(PeRCenTY))
 ||    #20: #mark(sel(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #21: #mark(sel(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY)
 ||    #22: #mark(cons(PeRCenTX,PeRCenTY)) -> #active(cons(mark(PeRCenTX),PeRCenTY))
 ||    #23: #mark(cons(PeRCenTX,PeRCenTY)) -> #cons(mark(PeRCenTX),PeRCenTY)
 ||    #24: #mark(cons(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #25: #mark(snd(PeRCenTX)) -> #active(snd(mark(PeRCenTX)))
 ||    #26: #mark(snd(PeRCenTX)) -> #snd(mark(PeRCenTX))
 ||    #27: #mark(snd(PeRCenTX)) -> #mark(PeRCenTX)
 ||    #28: #afterNth(mark(PeRCenTX),PeRCenTY) -> #afterNth(PeRCenTX,PeRCenTY)
 ||    #29: #and(active(PeRCenTX),PeRCenTY) -> #and(PeRCenTX,PeRCenTY)
 ||    #30: #u41(mark(PeRCenTX),PeRCenTY) -> #u41(PeRCenTX,PeRCenTY)
 ||    #31: #mark(u11(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #active(u11(mark(PeRCenTX),PeRCenTY,PeRCenTZ))
 ||    #32: #mark(u11(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #u11(mark(PeRCenTX),PeRCenTY,PeRCenTZ)
 ||    #33: #mark(u11(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #mark(PeRCenTX)
 ||    #34: #mark(u101(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #active(u101(mark(PeRCenTX),PeRCenTY,PeRCenTZ))
 ||    #35: #mark(u101(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #u101(mark(PeRCenTX),PeRCenTY,PeRCenTZ)
 ||    #36: #mark(u101(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #mark(PeRCenTX)
 ||    #37: #head(active(PeRCenTX)) -> #head(PeRCenTX)
 ||    #38: #cons(mark(PeRCenTX),PeRCenTY) -> #cons(PeRCenTX,PeRCenTY)
 ||    #39: #sel(mark(PeRCenTX),PeRCenTY) -> #sel(PeRCenTX,PeRCenTY)
 ||    #40: #u41(active(PeRCenTX),PeRCenTY) -> #u41(PeRCenTX,PeRCenTY)
 ||    #41: #u31(mark(PeRCenTX),PeRCenTY) -> #u31(PeRCenTX,PeRCenTY)
 ||    #42: #fst(mark(PeRCenTX)) -> #fst(PeRCenTX)
 ||    #43: #mark(natsFrom(PeRCenTX)) -> #active(natsFrom(mark(PeRCenTX)))
 ||    #44: #mark(natsFrom(PeRCenTX)) -> #natsFrom(mark(PeRCenTX))
 ||    #45: #mark(natsFrom(PeRCenTX)) -> #mark(PeRCenTX)
 ||    #46: #mark(u71(PeRCenTX,PeRCenTY)) -> #active(u71(mark(PeRCenTX),PeRCenTY))
 ||    #47: #mark(u71(PeRCenTX,PeRCenTY)) -> #u71(mark(PeRCenTX),PeRCenTY)
 ||    #48: #mark(u71(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #49: #u101(PeRCenTX,active(PeRCenTY),PeRCenTZ) -> #u101(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||    #50: #and(mark(PeRCenTX),PeRCenTY) -> #and(PeRCenTX,PeRCenTY)
 ||    #51: #u82(mark(PeRCenTX),PeRCenTY) -> #u82(PeRCenTX,PeRCenTY)
 ||    #52: #mark(s(PeRCenTX)) -> #active(s(mark(PeRCenTX)))
 ||    #53: #mark(s(PeRCenTX)) -> #s(mark(PeRCenTX))
 ||    #54: #mark(s(PeRCenTX)) -> #mark(PeRCenTX)
 ||    #55: #u71(mark(PeRCenTX),PeRCenTY) -> #u71(PeRCenTX,PeRCenTY)
 ||    #56: #splitAt(mark(PeRCenTX),PeRCenTY) -> #splitAt(PeRCenTX,PeRCenTY)
 ||    #57: #u51(PeRCenTX,PeRCenTY,active(PeRCenTZ)) -> #u51(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||    #58: #fst(active(PeRCenTX)) -> #fst(PeRCenTX)
 ||    #59: #mark(u91(PeRCenTX,PeRCenTY)) -> #active(u91(mark(PeRCenTX),PeRCenTY))
 ||    #60: #mark(u91(PeRCenTX,PeRCenTY)) -> #u91(mark(PeRCenTX),PeRCenTY)
 ||    #61: #mark(u91(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #62: #u81(PeRCenTX,PeRCenTY,PeRCenTZ,active(PeRCenTU)) -> #u81(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||    #63: #head(mark(PeRCenTX)) -> #head(PeRCenTX)
 ||    #64: #tail(active(PeRCenTX)) -> #tail(PeRCenTX)
 ||    #65: #mark(isLNat(PeRCenTX)) -> #active(isLNat(PeRCenTX))
 ||    #66: #mark(tt()) -> #active(tt())
 ||    #67: #isNatural(mark(PeRCenTX)) -> #isNatural(PeRCenTX)
 ||    #68: #isLNat(active(PeRCenTX)) -> #isLNat(PeRCenTX)
 ||    #69: #afterNth(PeRCenTX,mark(PeRCenTY)) -> #afterNth(PeRCenTX,PeRCenTY)
 ||    #70: #isPLNat(mark(PeRCenTX)) -> #isPLNat(PeRCenTX)
 ||    #71: #active(u51(tt(),PeRCenTX,PeRCenTY)) -> #mark(head(afterNth(PeRCenTX,PeRCenTY)))
 ||    #72: #active(u51(tt(),PeRCenTX,PeRCenTY)) -> #head(afterNth(PeRCenTX,PeRCenTY))
 ||    #73: #active(u51(tt(),PeRCenTX,PeRCenTY)) -> #afterNth(PeRCenTX,PeRCenTY)
 ||    #74: #sel(active(PeRCenTX),PeRCenTY) -> #sel(PeRCenTX,PeRCenTY)
 ||    #75: #mark(and(PeRCenTX,PeRCenTY)) -> #active(and(mark(PeRCenTX),PeRCenTY))
 ||    #76: #mark(and(PeRCenTX,PeRCenTY)) -> #and(mark(PeRCenTX),PeRCenTY)
 ||    #77: #mark(and(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #78: #u51(active(PeRCenTX),PeRCenTY,PeRCenTZ) -> #u51(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||    #79: #u81(PeRCenTX,mark(PeRCenTY),PeRCenTZ,PeRCenTU) -> #u81(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||    #80: #mark(nil()) -> #active(nil())
 ||    #81: #u101(mark(PeRCenTX),PeRCenTY,PeRCenTZ) -> #u101(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||    #82: #mark(splitAt(PeRCenTX,PeRCenTY)) -> #active(splitAt(mark(PeRCenTX),mark(PeRCenTY)))
 ||    #83: #mark(splitAt(PeRCenTX,PeRCenTY)) -> #splitAt(mark(PeRCenTX),mark(PeRCenTY))
 ||    #84: #mark(splitAt(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #85: #mark(splitAt(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY)
 ||    #86: #u21(PeRCenTX,active(PeRCenTY)) -> #u21(PeRCenTX,PeRCenTY)
 ||    #87: #u91(PeRCenTX,active(PeRCenTY)) -> #u91(PeRCenTX,PeRCenTY)
 ||    #88: #u51(mark(PeRCenTX),PeRCenTY,PeRCenTZ) -> #u51(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||    #89: #mark(afterNth(PeRCenTX,PeRCenTY)) -> #active(afterNth(mark(PeRCenTX),mark(PeRCenTY)))
 ||    #90: #mark(afterNth(PeRCenTX,PeRCenTY)) -> #afterNth(mark(PeRCenTX),mark(PeRCenTY))
 ||    #91: #mark(afterNth(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #92: #mark(afterNth(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY)
 ||    #93: #active(and(tt(),PeRCenTX)) -> #mark(PeRCenTX)
 ||    #94: #active(u81(tt(),PeRCenTX,PeRCenTY,PeRCenTZ)) -> #mark(u82(splitAt(PeRCenTX,PeRCenTZ),PeRCenTY))
 ||    #95: #active(u81(tt(),PeRCenTX,PeRCenTY,PeRCenTZ)) -> #u82(splitAt(PeRCenTX,PeRCenTZ),PeRCenTY)
 ||    #96: #active(u81(tt(),PeRCenTX,PeRCenTY,PeRCenTZ)) -> #splitAt(PeRCenTX,PeRCenTZ)
 ||    #97: #active(u91(tt(),PeRCenTX)) -> #mark(PeRCenTX)
 ||    #98: #u41(PeRCenTX,active(PeRCenTY)) -> #u41(PeRCenTX,PeRCenTY)
 ||    #99: #isPLNat(active(PeRCenTX)) -> #isPLNat(PeRCenTX)
 ||    #100: #mark(u82(PeRCenTX,PeRCenTY)) -> #active(u82(mark(PeRCenTX),PeRCenTY))
 ||    #101: #mark(u82(PeRCenTX,PeRCenTY)) -> #u82(mark(PeRCenTX),PeRCenTY)
 ||    #102: #mark(u82(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #103: #splitAt(PeRCenTX,mark(PeRCenTY)) -> #splitAt(PeRCenTX,PeRCenTY)
 ||    #104: #u51(PeRCenTX,PeRCenTY,mark(PeRCenTZ)) -> #u51(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||    #105: #u31(PeRCenTX,active(PeRCenTY)) -> #u31(PeRCenTX,PeRCenTY)
 ||    #106: #active(isNatural(0())) -> #mark(tt())
 ||    #107: #u81(PeRCenTX,PeRCenTY,PeRCenTZ,mark(PeRCenTU)) -> #u81(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||    #108: #u101(active(PeRCenTX),PeRCenTY,PeRCenTZ) -> #u101(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||    #109: #active(isLNat(take(PeRCenTX,PeRCenTY))) -> #mark(and(isNatural(PeRCenTX),isLNat(PeRCenTY)))
 ||    #110: #active(isLNat(take(PeRCenTX,PeRCenTY))) -> #and(isNatural(PeRCenTX),isLNat(PeRCenTY))
 ||    #111: #active(isLNat(take(PeRCenTX,PeRCenTY))) -> #isNatural(PeRCenTX)
 ||    #112: #active(isLNat(take(PeRCenTX,PeRCenTY))) -> #isLNat(PeRCenTY)
 ||    #113: #pair(PeRCenTX,mark(PeRCenTY)) -> #pair(PeRCenTX,PeRCenTY)
 ||    #114: #u11(PeRCenTX,PeRCenTY,mark(PeRCenTZ)) -> #u11(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||    #115: #afterNth(PeRCenTX,active(PeRCenTY)) -> #afterNth(PeRCenTX,PeRCenTY)
 ||    #116: #splitAt(PeRCenTX,active(PeRCenTY)) -> #splitAt(PeRCenTX,PeRCenTY)
 ||    #117: #mark(u41(PeRCenTX,PeRCenTY)) -> #active(u41(mark(PeRCenTX),PeRCenTY))
 ||    #118: #mark(u41(PeRCenTX,PeRCenTY)) -> #u41(mark(PeRCenTX),PeRCenTY)
 ||    #119: #mark(u41(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #120: #u41(PeRCenTX,mark(PeRCenTY)) -> #u41(PeRCenTX,PeRCenTY)
 ||    #121: #u101(PeRCenTX,PeRCenTY,mark(PeRCenTZ)) -> #u101(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||    #122: #cons(active(PeRCenTX),PeRCenTY) -> #cons(PeRCenTX,PeRCenTY)
 ||    #123: #active(afterNth(PeRCenTX,PeRCenTY)) -> #mark(u11(and(isNatural(PeRCenTX),isLNat(PeRCenTY)),PeRCenTX,PeRCenTY))
 ||    #124: #active(afterNth(PeRCenTX,PeRCenTY)) -> #u11(and(isNatural(PeRCenTX),isLNat(PeRCenTY)),PeRCenTX,PeRCenTY)
 ||    #125: #active(afterNth(PeRCenTX,PeRCenTY)) -> #and(isNatural(PeRCenTX),isLNat(PeRCenTY))
 ||    #126: #active(afterNth(PeRCenTX,PeRCenTY)) -> #isNatural(PeRCenTX)
 ||    #127: #active(afterNth(PeRCenTX,PeRCenTY)) -> #isLNat(PeRCenTY)
 ||    #128: #active(sel(PeRCenTX,PeRCenTY)) -> #mark(u51(and(isNatural(PeRCenTX),isLNat(PeRCenTY)),PeRCenTX,PeRCenTY))
 ||    #129: #active(sel(PeRCenTX,PeRCenTY)) -> #u51(and(isNatural(PeRCenTX),isLNat(PeRCenTY)),PeRCenTX,PeRCenTY)
 ||    #130: #active(sel(PeRCenTX,PeRCenTY)) -> #and(isNatural(PeRCenTX),isLNat(PeRCenTY))
 ||    #131: #active(sel(PeRCenTX,PeRCenTY)) -> #isNatural(PeRCenTX)
 ||    #132: #active(sel(PeRCenTX,PeRCenTY)) -> #isLNat(PeRCenTY)
 ||    #133: #sel(PeRCenTX,mark(PeRCenTY)) -> #sel(PeRCenTX,PeRCenTY)
 ||    #134: #u11(mark(PeRCenTX),PeRCenTY,PeRCenTZ) -> #u11(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||    #135: #mark(u81(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> #active(u81(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU))
 ||    #136: #mark(u81(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> #u81(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU)
 ||    #137: #mark(u81(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> #mark(PeRCenTX)
 ||    #138: #u21(active(PeRCenTX),PeRCenTY) -> #u21(PeRCenTX,PeRCenTY)
 ||    #139: #u81(PeRCenTX,PeRCenTY,mark(PeRCenTZ),PeRCenTU) -> #u81(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||    #140: #u11(active(PeRCenTX),PeRCenTY,PeRCenTZ) -> #u11(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||    #141: #u51(PeRCenTX,active(PeRCenTY),PeRCenTZ) -> #u51(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||    #142: #active(fst(pair(PeRCenTX,PeRCenTY))) -> #mark(u21(and(isLNat(PeRCenTX),isLNat(PeRCenTY)),PeRCenTX))
 ||    #143: #active(fst(pair(PeRCenTX,PeRCenTY))) -> #u21(and(isLNat(PeRCenTX),isLNat(PeRCenTY)),PeRCenTX)
 ||    #144: #active(fst(pair(PeRCenTX,PeRCenTY))) -> #and(isLNat(PeRCenTX),isLNat(PeRCenTY))
 ||    #145: #active(fst(pair(PeRCenTX,PeRCenTY))) -> #isLNat(PeRCenTX)
 ||    #146: #active(fst(pair(PeRCenTX,PeRCenTY))) -> #isLNat(PeRCenTY)
 ||    #147: #s(active(PeRCenTX)) -> #s(PeRCenTX)
 ||    #148: #mark(isPLNat(PeRCenTX)) -> #active(isPLNat(PeRCenTX))
 ||    #149: #active(natsFrom(PeRCenTX)) -> #mark(u41(isNatural(PeRCenTX),PeRCenTX))
 ||    #150: #active(natsFrom(PeRCenTX)) -> #u41(isNatural(PeRCenTX),PeRCenTX)
 ||    #151: #active(natsFrom(PeRCenTX)) -> #isNatural(PeRCenTX)
 ||    #152: #mark(u61(PeRCenTX,PeRCenTY)) -> #active(u61(mark(PeRCenTX),PeRCenTY))
 ||    #153: #mark(u61(PeRCenTX,PeRCenTY)) -> #u61(mark(PeRCenTX),PeRCenTY)
 ||    #154: #mark(u61(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #155: #mark(u51(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #active(u51(mark(PeRCenTX),PeRCenTY,PeRCenTZ))
 ||    #156: #mark(u51(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #u51(mark(PeRCenTX),PeRCenTY,PeRCenTZ)
 ||    #157: #mark(u51(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #mark(PeRCenTX)
 ||    #158: #active(isNatural(head(PeRCenTX))) -> #mark(isLNat(PeRCenTX))
 ||    #159: #active(isNatural(head(PeRCenTX))) -> #isLNat(PeRCenTX)
 ||    #160: #pair(PeRCenTX,active(PeRCenTY)) -> #pair(PeRCenTX,PeRCenTY)
 ||    #161: #sel(PeRCenTX,active(PeRCenTY)) -> #sel(PeRCenTX,PeRCenTY)
 ||    #162: #u51(PeRCenTX,mark(PeRCenTY),PeRCenTZ) -> #u51(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||    #163: #pair(active(PeRCenTX),PeRCenTY) -> #pair(PeRCenTX,PeRCenTY)
 ||    #164: #active(isLNat(natsFrom(PeRCenTX))) -> #mark(isNatural(PeRCenTX))
 ||    #165: #active(isLNat(natsFrom(PeRCenTX))) -> #isNatural(PeRCenTX)
 ||    #166: #u71(PeRCenTX,active(PeRCenTY)) -> #u71(PeRCenTX,PeRCenTY)
 ||    #167: #u21(PeRCenTX,mark(PeRCenTY)) -> #u21(PeRCenTX,PeRCenTY)
 ||    #168: #active(u61(tt(),PeRCenTX)) -> #mark(PeRCenTX)
 ||    #169: #mark(fst(PeRCenTX)) -> #active(fst(mark(PeRCenTX)))
 ||    #170: #mark(fst(PeRCenTX)) -> #fst(mark(PeRCenTX))
 ||    #171: #mark(fst(PeRCenTX)) -> #mark(PeRCenTX)
 ||    #172: #isLNat(mark(PeRCenTX)) -> #isLNat(PeRCenTX)
 ||    #173: #u81(PeRCenTX,active(PeRCenTY),PeRCenTZ,PeRCenTU) -> #u81(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||    #174: #active(u82(pair(PeRCenTX,PeRCenTY),PeRCenTZ)) -> #mark(pair(cons(PeRCenTZ,PeRCenTX),PeRCenTY))
 ||    #175: #active(u82(pair(PeRCenTX,PeRCenTY),PeRCenTZ)) -> #pair(cons(PeRCenTZ,PeRCenTX),PeRCenTY)
 ||    #176: #active(u82(pair(PeRCenTX,PeRCenTY),PeRCenTZ)) -> #cons(PeRCenTZ,PeRCenTX)
 ||    #177: #u31(PeRCenTX,mark(PeRCenTY)) -> #u31(PeRCenTX,PeRCenTY)
 ||    #178: #u61(mark(PeRCenTX),PeRCenTY) -> #u61(PeRCenTX,PeRCenTY)
 ||    #179: #u31(active(PeRCenTX),PeRCenTY) -> #u31(PeRCenTX,PeRCenTY)
 ||    #180: #mark(take(PeRCenTX,PeRCenTY)) -> #active(take(mark(PeRCenTX),mark(PeRCenTY)))
 ||    #181: #mark(take(PeRCenTX,PeRCenTY)) -> #take(mark(PeRCenTX),mark(PeRCenTY))
 ||    #182: #mark(take(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #183: #mark(take(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY)
 ||    #184: #active(splitAt(0(),PeRCenTX)) -> #mark(u71(isLNat(PeRCenTX),PeRCenTX))
 ||    #185: #active(splitAt(0(),PeRCenTX)) -> #u71(isLNat(PeRCenTX),PeRCenTX)
 ||    #186: #active(splitAt(0(),PeRCenTX)) -> #isLNat(PeRCenTX)
 ||    #187: #u101(PeRCenTX,PeRCenTY,active(PeRCenTZ)) -> #u101(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||    #188: #take(PeRCenTX,active(PeRCenTY)) -> #take(PeRCenTX,PeRCenTY)
 ||    #189: #u61(PeRCenTX,mark(PeRCenTY)) -> #u61(PeRCenTX,PeRCenTY)
 ||    #190: #active(u41(tt(),PeRCenTX)) -> #mark(cons(PeRCenTX,natsFrom(s(PeRCenTX))))
 ||    #191: #active(u41(tt(),PeRCenTX)) -> #cons(PeRCenTX,natsFrom(s(PeRCenTX)))
 ||    #192: #active(u41(tt(),PeRCenTX)) -> #natsFrom(s(PeRCenTX))
 ||    #193: #active(u41(tt(),PeRCenTX)) -> #s(PeRCenTX)
 ||    #194: #mark(u31(PeRCenTX,PeRCenTY)) -> #active(u31(mark(PeRCenTX),PeRCenTY))
 ||    #195: #mark(u31(PeRCenTX,PeRCenTY)) -> #u31(mark(PeRCenTX),PeRCenTY)
 ||    #196: #mark(u31(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #197: #mark(0()) -> #active(0())
 ||    #198: #and(PeRCenTX,mark(PeRCenTY)) -> #and(PeRCenTX,PeRCenTY)
 ||    #199: #active(isPLNat(pair(PeRCenTX,PeRCenTY))) -> #mark(and(isLNat(PeRCenTX),isLNat(PeRCenTY)))
 ||    #200: #active(isPLNat(pair(PeRCenTX,PeRCenTY))) -> #and(isLNat(PeRCenTX),isLNat(PeRCenTY))
 ||    #201: #active(isPLNat(pair(PeRCenTX,PeRCenTY))) -> #isLNat(PeRCenTX)
 ||    #202: #active(isPLNat(pair(PeRCenTX,PeRCenTY))) -> #isLNat(PeRCenTY)
 ||    #203: #active(isLNat(tail(PeRCenTX))) -> #mark(isLNat(PeRCenTX))
 ||    #204: #active(isLNat(tail(PeRCenTX))) -> #isLNat(PeRCenTX)
 ||    #205: #pair(mark(PeRCenTX),PeRCenTY) -> #pair(PeRCenTX,PeRCenTY)
 ||    #206: #active(splitAt(s(PeRCenTX),cons(PeRCenTY,PeRCenTZ))) -> #mark(u81(and(isNatural(PeRCenTX),and(isNatural(PeRCenTY),isLNat(PeRCenTZ))),PeRCenTX,PeRCenTY,PeRCenTZ))
 ||    #207: #active(splitAt(s(PeRCenTX),cons(PeRCenTY,PeRCenTZ))) -> #u81(and(isNatural(PeRCenTX),and(isNatural(PeRCenTY),isLNat(PeRCenTZ))),PeRCenTX,PeRCenTY,PeRCenTZ)
 ||    #208: #active(splitAt(s(PeRCenTX),cons(PeRCenTY,PeRCenTZ))) -> #and(isNatural(PeRCenTX),and(isNatural(PeRCenTY),isLNat(PeRCenTZ)))
 ||    #209: #active(splitAt(s(PeRCenTX),cons(PeRCenTY,PeRCenTZ))) -> #isNatural(PeRCenTX)
 ||    #210: #active(splitAt(s(PeRCenTX),cons(PeRCenTY,PeRCenTZ))) -> #and(isNatural(PeRCenTY),isLNat(PeRCenTZ))
 ||    #211: #active(splitAt(s(PeRCenTX),cons(PeRCenTY,PeRCenTZ))) -> #isNatural(PeRCenTY)
 ||    #212: #active(splitAt(s(PeRCenTX),cons(PeRCenTY,PeRCenTZ))) -> #isLNat(PeRCenTZ)
 ||    #213: #u11(PeRCenTX,PeRCenTY,active(PeRCenTZ)) -> #u11(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||    #214: #u21(mark(PeRCenTX),PeRCenTY) -> #u21(PeRCenTX,PeRCenTY)
 ||    #215: #tail(mark(PeRCenTX)) -> #tail(PeRCenTX)
 ||    #216: #active(isNatural(sel(PeRCenTX,PeRCenTY))) -> #mark(and(isNatural(PeRCenTX),isLNat(PeRCenTY)))
 ||    #217: #active(isNatural(sel(PeRCenTX,PeRCenTY))) -> #and(isNatural(PeRCenTX),isLNat(PeRCenTY))
 ||    #218: #active(isNatural(sel(PeRCenTX,PeRCenTY))) -> #isNatural(PeRCenTX)
 ||    #219: #active(isNatural(sel(PeRCenTX,PeRCenTY))) -> #isLNat(PeRCenTY)
 ||    #220: #u81(PeRCenTX,PeRCenTY,active(PeRCenTZ),PeRCenTU) -> #u81(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||    #221: #u91(PeRCenTX,mark(PeRCenTY)) -> #u91(PeRCenTX,PeRCenTY)
 ||    #222: #u82(PeRCenTX,active(PeRCenTY)) -> #u82(PeRCenTX,PeRCenTY)
 ||    #223: #take(active(PeRCenTX),PeRCenTY) -> #take(PeRCenTX,PeRCenTY)
 ||    #224: #and(PeRCenTX,active(PeRCenTY)) -> #and(PeRCenTX,PeRCenTY)
 ||    #225: #mark(isNatural(PeRCenTX)) -> #active(isNatural(PeRCenTX))
 ||    #226: #afterNth(active(PeRCenTX),PeRCenTY) -> #afterNth(PeRCenTX,PeRCenTY)
 ||    #227: #active(isLNat(afterNth(PeRCenTX,PeRCenTY))) -> #mark(and(isNatural(PeRCenTX),isLNat(PeRCenTY)))
 ||    #228: #active(isLNat(afterNth(PeRCenTX,PeRCenTY))) -> #and(isNatural(PeRCenTX),isLNat(PeRCenTY))
 ||    #229: #active(isLNat(afterNth(PeRCenTX,PeRCenTY))) -> #isNatural(PeRCenTX)
 ||    #230: #active(isLNat(afterNth(PeRCenTX,PeRCenTY))) -> #isLNat(PeRCenTY)
 ||    #231: #active(snd(pair(PeRCenTX,PeRCenTY))) -> #mark(u61(and(isLNat(PeRCenTX),isLNat(PeRCenTY)),PeRCenTY))
 ||    #232: #active(snd(pair(PeRCenTX,PeRCenTY))) -> #u61(and(isLNat(PeRCenTX),isLNat(PeRCenTY)),PeRCenTY)
 ||    #233: #active(snd(pair(PeRCenTX,PeRCenTY))) -> #and(isLNat(PeRCenTX),isLNat(PeRCenTY))
 ||    #234: #active(snd(pair(PeRCenTX,PeRCenTY))) -> #isLNat(PeRCenTX)
 ||    #235: #active(snd(pair(PeRCenTX,PeRCenTY))) -> #isLNat(PeRCenTY)
 ||    #236: #active(isLNat(fst(PeRCenTX))) -> #mark(isPLNat(PeRCenTX))
 ||    #237: #active(isLNat(fst(PeRCenTX))) -> #isPLNat(PeRCenTX)
 ||    #238: #u91(mark(PeRCenTX),PeRCenTY) -> #u91(PeRCenTX,PeRCenTY)
 ||    #239: #u71(active(PeRCenTX),PeRCenTY) -> #u71(PeRCenTX,PeRCenTY)
 ||    #240: #mark(tail(PeRCenTX)) -> #active(tail(mark(PeRCenTX)))
 ||    #241: #mark(tail(PeRCenTX)) -> #tail(mark(PeRCenTX))
 ||    #242: #mark(tail(PeRCenTX)) -> #mark(PeRCenTX)
 ||    #243: #u81(active(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU) -> #u81(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||    #244: #s(mark(PeRCenTX)) -> #s(PeRCenTX)
 ||    #245: #active(isNatural(s(PeRCenTX))) -> #mark(isNatural(PeRCenTX))
 ||    #246: #active(isNatural(s(PeRCenTX))) -> #isNatural(PeRCenTX)
 ||    #247: #cons(PeRCenTX,mark(PeRCenTY)) -> #cons(PeRCenTX,PeRCenTY)
 ||    #248: #snd(mark(PeRCenTX)) -> #snd(PeRCenTX)
 ||    #249: #u61(PeRCenTX,active(PeRCenTY)) -> #u61(PeRCenTX,PeRCenTY)
 ||    #250: #u101(PeRCenTX,mark(PeRCenTY),PeRCenTZ) -> #u101(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||    #251: #u81(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU) -> #u81(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)
 ||    #252: #active(take(PeRCenTX,PeRCenTY)) -> #mark(u101(and(isNatural(PeRCenTX),isLNat(PeRCenTY)),PeRCenTX,PeRCenTY))
 ||    #253: #active(take(PeRCenTX,PeRCenTY)) -> #u101(and(isNatural(PeRCenTX),isLNat(PeRCenTY)),PeRCenTX,PeRCenTY)
 ||    #254: #active(take(PeRCenTX,PeRCenTY)) -> #and(isNatural(PeRCenTX),isLNat(PeRCenTY))
 ||    #255: #active(take(PeRCenTX,PeRCenTY)) -> #isNatural(PeRCenTX)
 ||    #256: #active(take(PeRCenTX,PeRCenTY)) -> #isLNat(PeRCenTY)
 ||    #257: #active(isLNat(snd(PeRCenTX))) -> #mark(isPLNat(PeRCenTX))
 ||    #258: #active(isLNat(snd(PeRCenTX))) -> #isPLNat(PeRCenTX)
 ||    #259: #active(isLNat(nil())) -> #mark(tt())
 ||    #260: #active(u21(tt(),PeRCenTX)) -> #mark(PeRCenTX)
 ||    #261: #take(mark(PeRCenTX),PeRCenTY) -> #take(PeRCenTX,PeRCenTY)
 ||    #262: #splitAt(active(PeRCenTX),PeRCenTY) -> #splitAt(PeRCenTX,PeRCenTY)
 ||    #263: #active(u101(tt(),PeRCenTX,PeRCenTY)) -> #mark(fst(splitAt(PeRCenTX,PeRCenTY)))
 ||    #264: #active(u101(tt(),PeRCenTX,PeRCenTY)) -> #fst(splitAt(PeRCenTX,PeRCenTY))
 ||    #265: #active(u101(tt(),PeRCenTX,PeRCenTY)) -> #splitAt(PeRCenTX,PeRCenTY)
 ||    #266: #u82(PeRCenTX,mark(PeRCenTY)) -> #u82(PeRCenTX,PeRCenTY)
 ||    #267: #u71(PeRCenTX,mark(PeRCenTY)) -> #u71(PeRCenTX,PeRCenTY)
 ||    #268: #mark(pair(PeRCenTX,PeRCenTY)) -> #active(pair(mark(PeRCenTX),mark(PeRCenTY)))
 ||    #269: #mark(pair(PeRCenTX,PeRCenTY)) -> #pair(mark(PeRCenTX),mark(PeRCenTY))
 ||    #270: #mark(pair(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX)
 ||    #271: #mark(pair(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY)
 ||    #272: #take(PeRCenTX,mark(PeRCenTY)) -> #take(PeRCenTX,PeRCenTY)
 ||    #273: #active(u71(tt(),PeRCenTX)) -> #mark(pair(nil(),PeRCenTX))
 ||    #274: #active(u71(tt(),PeRCenTX)) -> #pair(nil(),PeRCenTX)
 ||    #275: #isNatural(active(PeRCenTX)) -> #isNatural(PeRCenTX)
 ||    #276: #u82(active(PeRCenTX),PeRCenTY) -> #u82(PeRCenTX,PeRCenTY)
 ||    #277: #u61(active(PeRCenTX),PeRCenTY) -> #u61(PeRCenTX,PeRCenTY)
 ||    #278: #active(head(cons(PeRCenTX,PeRCenTY))) -> #mark(u31(and(isNatural(PeRCenTX),isLNat(PeRCenTY)),PeRCenTX))
 ||    #279: #active(head(cons(PeRCenTX,PeRCenTY))) -> #u31(and(isNatural(PeRCenTX),isLNat(PeRCenTY)),PeRCenTX)
 ||    #280: #active(head(cons(PeRCenTX,PeRCenTY))) -> #and(isNatural(PeRCenTX),isLNat(PeRCenTY))
 ||    #281: #active(head(cons(PeRCenTX,PeRCenTY))) -> #isNatural(PeRCenTX)
 ||    #282: #active(head(cons(PeRCenTX,PeRCenTY))) -> #isLNat(PeRCenTY)
 ||    #283: #u91(active(PeRCenTX),PeRCenTY) -> #u91(PeRCenTX,PeRCenTY)
 ||    #284: #cons(PeRCenTX,active(PeRCenTY)) -> #cons(PeRCenTX,PeRCenTY)
 ||    #285: #natsFrom(mark(PeRCenTX)) -> #natsFrom(PeRCenTX)
 ||    #286: #active(u31(tt(),PeRCenTX)) -> #mark(PeRCenTX)
 ||    #287: #natsFrom(active(PeRCenTX)) -> #natsFrom(PeRCenTX)
 ||    #288: #u11(PeRCenTX,mark(PeRCenTY),PeRCenTZ) -> #u11(PeRCenTX,PeRCenTY,PeRCenTZ)
 ||    #289: #mark(head(PeRCenTX)) -> #active(head(mark(PeRCenTX)))
 ||    #290: #mark(head(PeRCenTX)) -> #head(mark(PeRCenTX))
 ||    #291: #mark(head(PeRCenTX)) -> #mark(PeRCenTX)
 ||    #292: #active(isLNat(cons(PeRCenTX,PeRCenTY))) -> #mark(and(isNatural(PeRCenTX),isLNat(PeRCenTY)))
 ||    #293: #active(isLNat(cons(PeRCenTX,PeRCenTY))) -> #and(isNatural(PeRCenTX),isLNat(PeRCenTY))
 ||    #294: #active(isLNat(cons(PeRCenTX,PeRCenTY))) -> #isNatural(PeRCenTX)
 ||    #295: #active(isLNat(cons(PeRCenTX,PeRCenTY))) -> #isLNat(PeRCenTY)
 || Number of SCCs: 28, DPs: 187
 ||   SCC { #4 #248 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: x1
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #4 #248
 || Number of SCCs: 27, DPs: 185
 ||   SCC { #285 #287 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: x1
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #285 #287
 || Number of SCCs: 26, DPs: 183
 ||   SCC { #70 #99 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: x1
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #70 #99
 || Number of SCCs: 25, DPs: 181
 ||   SCC { #147 #244 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: x1
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #147 #244
 || Number of SCCs: 24, DPs: 179
 ||   SCC { #42 #58 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: x1
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #42 #58
 || Number of SCCs: 23, DPs: 177
 ||   SCC { #64 #215 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: x1
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #64 #215
 || Number of SCCs: 22, DPs: 175
 ||   SCC { #68 #172 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: x1
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #68 #172
 || Number of SCCs: 21, DPs: 173
 ||   SCC { #37 #63 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: x1
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #37 #63
 || Number of SCCs: 20, DPs: 171
 ||   SCC { #67 #275 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: x1
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #67 #275
 || Number of SCCs: 19, DPs: 169
 ||   SCC { #39 #74 #133 #161 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: x2
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #133 #161
 || Number of SCCs: 19, DPs: 167
 ||   SCC { #39 #74 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: x1
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #39 #74
 || Number of SCCs: 18, DPs: 165
 ||   SCC { #55 #166 #239 #267 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: x1
 ||     USABLE RULES: { }
 ||     Removed DPs: #55 #239
 || Number of SCCs: 18, DPs: 163
 ||   SCC { #166 #267 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: x2
 ||     USABLE RULES: { }
 ||     Removed DPs: #166 #267
 || Number of SCCs: 17, DPs: 161
 ||   SCC { #38 #122 #247 #284 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: x2
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #247 #284
 || Number of SCCs: 17, DPs: 159
 ||   SCC { #38 #122 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: x1
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #38 #122
 || Number of SCCs: 16, DPs: 157
 ||   SCC { #51 #222 #266 #276 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: x2
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #222 #266
 || Number of SCCs: 16, DPs: 155
 ||   SCC { #51 #276 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: x1
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #51 #276
 || Number of SCCs: 15, DPs: 153
 ||   SCC { #56 #103 #116 #262 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: x1
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #56 #262
 || Number of SCCs: 15, DPs: 151
 ||   SCC { #103 #116 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: x2
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #103 #116
 || Number of SCCs: 14, DPs: 149
 ||   SCC { #29 #50 #198 #224 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: x2
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #198 #224
 || Number of SCCs: 14, DPs: 147
 ||   SCC { #29 #50 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: x1
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #29 #50
 || Number of SCCs: 13, DPs: 145
 ||   SCC { #178 #189 #249 #277 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: x2
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #189 #249
 || Number of SCCs: 13, DPs: 143
 ||   SCC { #178 #277 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: x1
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #178 #277
 || Number of SCCs: 12, DPs: 141
 ||   SCC { #28 #69 #115 #226 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: x1
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #28 #226
 || Number of SCCs: 12, DPs: 139
 ||   SCC { #69 #115 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: x2
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #69 #115
 || Number of SCCs: 11, DPs: 137
 ||   SCC { #86 #138 #167 #214 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: x1
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #138 #214
 || Number of SCCs: 11, DPs: 135
 ||   SCC { #86 #167 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: x2
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #86 #167
 || Number of SCCs: 10, DPs: 133
 ||   SCC { #188 #223 #261 #272 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: x2
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #188 #272
 || Number of SCCs: 10, DPs: 131
 ||   SCC { #223 #261 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: x1
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #223 #261
 || Number of SCCs: 9, DPs: 129
 ||   SCC { #87 #221 #238 #283 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: x2
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #87 #221
 || Number of SCCs: 9, DPs: 127
 ||   SCC { #238 #283 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: x1
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #238 #283
 || Number of SCCs: 8, DPs: 125
 ||   SCC { #113 #160 #163 #205 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: x2
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #113 #160
 || Number of SCCs: 8, DPs: 123
 ||   SCC { #163 #205 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: x1
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #163 #205
 || Number of SCCs: 7, DPs: 121
 ||   SCC { #41 #105 #177 #179 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: x1
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #41 #179
 || Number of SCCs: 7, DPs: 119
 ||   SCC { #105 #177 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: x2
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #105 #177
 || Number of SCCs: 6, DPs: 117
 ||   SCC { #30 #40 #98 #120 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: x2
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #98 #120
 || Number of SCCs: 6, DPs: 115
 ||   SCC { #30 #40 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: x1
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #30 #40
 || Number of SCCs: 5, DPs: 113
 ||   SCC { #17 #114 #134 #140 #213 #288 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: x1 + x2
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #17 #134 #140 #288
 || Number of SCCs: 5, DPs: 109
 ||   SCC { #114 #213 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: x3
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #114 #213
 || Number of SCCs: 4, DPs: 107
 ||   SCC { #57 #78 #88 #104 #141 #162 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: x1 + x2
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #78 #88 #141 #162
 || Number of SCCs: 4, DPs: 103
 ||   SCC { #57 #104 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: x3
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #57 #104
 || Number of SCCs: 3, DPs: 101
 ||   SCC { #49 #81 #108 #121 #187 #250 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: x2 + x3
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #49 #121 #187 #250
 || Number of SCCs: 3, DPs: 97
 ||   SCC { #81 #108 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: x1
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #81 #108
 || Number of SCCs: 2, DPs: 95
 ||   SCC { #62 #79 #107 #139 #173 #220 #243 #251 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: x1 + x3 + x4
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #62 #107 #139 #220 #243 #251
 || Number of SCCs: 2, DPs: 89
 ||   SCC { #79 #173 }
 || POLO(Sum)... succeeded.
 ||       u81	w: 0
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: 0
 ||       u91	w: 0
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: 0
 ||       #u21	w: 0
 ||       and	w: 0
 ||       pair	w: 0
 ||       fst	w: 0
 ||       natsFrom	w: 0
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 0
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: 0
 ||       #u81	w: x2
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: 0
 ||       u51	w: 0
 ||       tail	w: 0
 ||       #mark	w: 0
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: 0
 ||       #isLNat	w: 0
 ||       sel	w: 0
 ||       #s 	w: 0
 ||       afterNth	w: 0
 ||       #isPLNat	w: 0
 ||       nil	w: 0
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: 0
 ||       #afterNth	w: 0
 ||       u21	w: 0
 ||       #u41	w: 0
 ||       u82	w: 0
 ||       active	w: x1 + 1
 ||       head	w: 0
 ||       #snd	w: 0
 ||       cons	w: 0
 ||       #natsFrom	w: 0
 ||       #active	w: 0
 ||       #u31	w: 0
 ||       snd	w: 0
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: 0
 ||       u31	w: 0
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { }
 ||     Removed DPs: #79 #173
 || Number of SCCs: 1, DPs: 87
 ||   SCC { #1 #5 #7 #8 #12 #18 #20 #21 #24 #25 #27 #31 #33 #34 #36 #43 #45 #46 #48 #54 #59 #61 #65 #71 #75 #77 #82 #84 #85 #89 #91..94 #97 #100 #102 #109 #117 #119 #123 #128 #135 #137 #142 #148 #149 #152 #154 #155 #157 #158 #164 #168 #169 #171 #174 #180 #182..184 #190 #194 #196 #199 #203 #206 #216 #225 #227 #231 #236 #240 #242 #245 #252 #257 #260 #263 #270 #271 #273 #278 #286 #289 #291 #292 }
 || POLO(Sum)... POLO(max)... succeeded.
 ||       u81	w: max(x1 + 1, x2 + 3, x3 + 2, x4)
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: x1
 ||       u91	w: max(x1 + 1, x2 + 2)
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: max(x1 + 6, x2)
 ||       #u21	w: 0
 ||       and	w: max(x1, x2)
 ||       pair	w: max(x1, x2)
 ||       fst	w: x1
 ||       natsFrom	w: x1 + 4
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: max(x1 + 3, x2)
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: max(x1 + 1, x2 + 2)
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: max(x1 + 3, x2 + 4)
 ||       u51	w: max(x1 + 12, x2 + 13, x3 + 14)
 ||       tail	w: x1 + 3
 ||       #mark	w: x1
 ||       0 	w: 1
 ||       #sel	w: 0
 ||       u11	w: max(x1 + 2, x2 + 7, x3 + 3)
 ||       #isLNat	w: 0
 ||       sel	w: max(x1 + 15, x2 + 16)
 ||       #s 	w: 0
 ||       afterNth	w: max(x1 + 8, x2 + 9)
 ||       #isPLNat	w: 0
 ||       nil	w: 1
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1
 ||       u101	w: max(x1 + 4, x2 + 5, x3)
 ||       #afterNth	w: 0
 ||       u21	w: max(x1, x2)
 ||       #u41	w: 0
 ||       u82	w: max(x1, x2 + 2)
 ||       active	w: x1
 ||       head	w: x1 + 2
 ||       #snd	w: 0
 ||       cons	w: max(x1 + 2, x2)
 ||       #natsFrom	w: 0
 ||       #active	w: x1
 ||       #u31	w: 0
 ||       snd	w: x1 + 3
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: max(x1 + 1, x2)
 ||       u31	w: max(x1 + 3, x2 + 1)
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { 1..166 }
 ||     Removed DPs: #12 #20 #21 #24 #27 #33 #36 #45 #48 #61 #71 #84 #91 #92 #97 #119 #123 #128 #137 #154 #157 #168 #182 #196 #231 #242 #278 #286 #291
 || Number of SCCs: 1, DPs: 43
 ||   SCC { #5 #7 #8 #34 #46 #54 #65 #75 #77 #82 #85 #93 #94 #100 #102 #109 #135 #142 #148 #158 #164 #169 #171 #174 #180 #183 #184 #199 #203 #206 #216 #225 #227 #236 #245 #252 #257 #260 #263 #270 #271 #273 #292 }
 || POLO(Sum)... POLO(max)... succeeded.
 ||       u81	w: max(x1 + 1, x2 + 2, x3 + 3, x4)
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: x1
 ||       u91	w: max(x1 + 1, x2 + 2)
 ||       #take	w: 0
 ||       isPLNat	w: 0
 ||       #u51	w: 0
 ||       take	w: max(x1 + 6, x2 + 4)
 ||       #u21	w: 0
 ||       and	w: max(x1, x2)
 ||       pair	w: max(x1, x2)
 ||       fst	w: x1
 ||       natsFrom	w: x1 + 4
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: max(x1 + 2, x2)
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: max(x1 + 1, x2 + 2)
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 0
 ||       u41	w: max(x1 + 3, x2 + 4)
 ||       u51	w: max(x1 + 12, x2 + 13, x3 + 14)
 ||       tail	w: x1 + 3
 ||       #mark	w: x1
 ||       0 	w: 2
 ||       #sel	w: 0
 ||       u11	w: max(x1 + 2, x2 + 5, x3 + 3)
 ||       #isLNat	w: 0
 ||       sel	w: max(x1 + 15, x2 + 16)
 ||       #s 	w: 0
 ||       afterNth	w: max(x1 + 8, x2 + 9)
 ||       #isPLNat	w: 0
 ||       nil	w: 4
 ||       isLNat	w: 0
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1
 ||       u101	w: max(x1 + 5, x2 + 6, x3 + 3)
 ||       #afterNth	w: 0
 ||       u21	w: max(x1, x2)
 ||       #u41	w: 0
 ||       u82	w: max(x1, x2 + 3)
 ||       active	w: x1
 ||       head	w: x1 + 2
 ||       #snd	w: 0
 ||       cons	w: max(x1 + 3, x2)
 ||       #natsFrom	w: 0
 ||       #active	w: x1
 ||       #u31	w: 0
 ||       snd	w: x1 + 3
 ||       tt	w: 0
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: max(x1 + 4, x2)
 ||       u31	w: max(x1 + 3, x2 + 1)
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { 1..166 }
 ||     Removed DPs: #183 #263
 || Number of SCCs: 1, DPs: 38
 ||   SCC { #5 #7 #8 #46 #54 #65 #75 #77 #82 #85 #93 #94 #100 #102 #109 #135 #142 #148 #158 #164 #169 #171 #174 #184 #199 #203 #206 #216 #225 #227 #236 #245 #257 #260 #270 #271 #273 #292 }
 || POLO(Sum)... POLO(max)... succeeded.
 ||       u81	w: max(x3 + 7, x4 + 6)
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: x1
 ||       u91	w: max(x2 + 1)
 ||       #take	w: 0
 ||       isPLNat	w: 1
 ||       #u51	w: 0
 ||       take	w: max(x1 + 11, x2 + 9)
 ||       #u21	w: 0
 ||       and	w: max(x1, x2)
 ||       pair	w: max(x1 + 2, x2 + 1)
 ||       fst	w: x1 + 3
 ||       natsFrom	w: x1 + 3
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: max(x2 + 6)
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: max(x2 + 1)
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: 1
 ||       u41	w: max(x1 + 1, x2 + 3)
 ||       u51	w: max(x2 + 9, x3 + 10)
 ||       tail	w: x1 + 1
 ||       #mark	w: x1
 ||       0 	w: 0
 ||       #sel	w: 0
 ||       u11	w: max(x2 + 8, x3 + 7)
 ||       #isLNat	w: 0
 ||       sel	w: max(x1 + 10, x2 + 11)
 ||       #s 	w: 0
 ||       afterNth	w: max(x1 + 8, x2 + 9)
 ||       #isPLNat	w: 0
 ||       nil	w: 1
 ||       isLNat	w: 1
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1
 ||       u101	w: max(x1 + 10, x2 + 11, x3 + 9)
 ||       #afterNth	w: 0
 ||       u21	w: max(x1 + 2, x2 + 1)
 ||       #u41	w: 0
 ||       u82	w: max(x1, x2 + 5)
 ||       active	w: x1
 ||       head	w: x1
 ||       #snd	w: 0
 ||       cons	w: max(x1 + 2, x2)
 ||       #natsFrom	w: 0
 ||       #active	w: x1
 ||       #u31	w: 0
 ||       snd	w: x1 + 1
 ||       tt	w: 1
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: max(x2 + 4)
 ||       u31	w: max(x1 + 1, x2)
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { 1..166 }
 ||     Removed DPs: #7 #85 #142 #171 #184 #260 #270 #271 #273
 || Number of SCCs: 1, DPs: 24
 ||   SCC { #8 #54 #65 #75 #77 #82 #93 #94 #102 #109 #135 #148 #158 #164 #199 #203 #206 #216 #225 #227 #236 #245 #257 #292 }
 || POLO(Sum)... POLO(max)... succeeded.
 ||       u81	w: max(x1 + 2, x2 + 8, x3 + 7, x4 + 6)
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: x1
 ||       u91	w: max(x2 + 1)
 ||       #take	w: 0
 ||       isPLNat	w: x1 + 4
 ||       #u51	w: 0
 ||       take	w: max(x1 + 15, x2 + 14)
 ||       #u21	w: 0
 ||       and	w: max(x1 + 1, x2)
 ||       pair	w: max(x1 + 2, x2 + 1)
 ||       fst	w: x1 + 3
 ||       natsFrom	w: x1 + 3
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: max(x1 + 8, x2 + 6)
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: max(x2)
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: x1 + 1
 ||       u41	w: max(x1 + 1, x2 + 3)
 ||       u51	w: max(x2 + 15, x3 + 16)
 ||       tail	w: x1 + 1
 ||       #mark	w: x1
 ||       0 	w: 6
 ||       #sel	w: 0
 ||       u11	w: max(x2 + 10, x3 + 11)
 ||       #isLNat	w: 0
 ||       sel	w: max(x1 + 17, x2 + 16)
 ||       #s 	w: 0
 ||       afterNth	w: max(x1 + 10, x2 + 11)
 ||       #isPLNat	w: 0
 ||       nil	w: 4
 ||       isLNat	w: x1 + 3
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1
 ||       u101	w: max(x1 + 11, x2 + 12, x3 + 11)
 ||       #afterNth	w: 0
 ||       u21	w: max(x2)
 ||       #u41	w: 0
 ||       u82	w: max(x1, x2 + 5)
 ||       active	w: x1
 ||       head	w: x1 + 4
 ||       #snd	w: 0
 ||       cons	w: max(x1 + 3, x2)
 ||       #natsFrom	w: 0
 ||       #active	w: x1
 ||       #u31	w: 0
 ||       snd	w: x1 + 2
 ||       tt	w: 7
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: max(x2 + 6)
 ||       u31	w: max(x1 + 1, x2 + 2)
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { 1..166 }
 ||     Removed DPs: #8 #77 #109 #158 #164 #199 #203 #216 #227 #236 #257
 || Number of SCCs: 2, DPs: 12
 ||   SCC { #225 #245 }
 || POLO(Sum)... succeeded.
 ||       u81	w: x3 + 3
 ||       #u101	w: 0
 ||       TIlDePAIR	w: 0
 ||       #u82	w: 0
 ||       #cons	w: 0
 ||       s 	w: x1 + 2
 ||       u91	w: x2 + 3
 ||       #take	w: 0
 ||       isPLNat	w: 21
 ||       #u51	w: 0
 ||       take	w: 1
 ||       #u21	w: 0
 ||       and	w: 23
 ||       pair	w: x1 + 1
 ||       fst	w: 5
 ||       natsFrom	w: 1
 ||       #head	w: 0
 ||       #u61	w: 0
 ||       splitAt	w: 1
 ||       #fst	w: 0
 ||       #u11	w: 0
 ||       u61	w: x2 + 7
 ||       #u81	w: 0
 ||       #u91	w: 0
 ||       isNatural	w: x1 + 2
 ||       u41	w: x2 + 5
 ||       u51	w: x2 + x3 + 8
 ||       tail	w: 1
 ||       #mark	w: x1 + 1
 ||       0 	w: 1
 ||       #sel	w: 0
 ||       u11	w: 3
 ||       #isLNat	w: 0
 ||       sel	w: 6
 ||       #s 	w: 0
 ||       afterNth	w: 1
 ||       #isPLNat	w: 0
 ||       nil	w: 4
 ||       isLNat	w: x1 + 14
 ||       #TIlDePAIR	w: 0
 ||       #tail	w: 0
 ||       #splitAt	w: 0
 ||       mark	w: x1 + 1
 ||       u101	w: x2 + x3 + 3
 ||       #afterNth	w: 0
 ||       u21	w: x2 + 7
 ||       #u41	w: 0
 ||       u82	w: 5
 ||       active	w: x1 + 2
 ||       head	w: 10
 ||       #snd	w: 0
 ||       cons	w: 6
 ||       #natsFrom	w: 0
 ||       #active	w: x1
 ||       #u31	w: 0
 ||       snd	w: 5
 ||       tt	w: 20
 ||       #isNatural	w: 0
 ||       #pair	w: 0
 ||       u71	w: x2 + 3
 ||       u31	w: x2 + 12
 ||       #and	w: 0
 ||       #u71	w: 0
 ||     USABLE RULES: { 67..104 107..166 }
 ||     Removed DPs: #225 #245
 || Number of SCCs: 1, DPs: 10
 ||   SCC { #54 #65 #75 #82 #93 #94 #102 #135 #206 #292 }
 || POLO(Sum)... POLO(max)... QLPOS... succeeded.
 ||       u81	s: []	p: 10
 ||       #u101	s: [3]	p: 0
 ||       TIlDePAIR	s: [2]	p: 0
 ||       #u82	s: [1,2]	p: 0
 ||       #cons	s: []	p: 0
 ||       s 	s: [1]	p: 1
 ||       u91	s: []	p: 9
 ||       #take	s: [2]	p: 0
 ||       isPLNat	s: []	p: 3
 ||       #u51	s: [1,3]	p: 0
 ||       take	s: [2,1]	p: 10
 ||       #u21	s: [1]	p: 0
 ||       and	s: 2
 ||       pair	s: []	p: 8
 ||       fst	s: []	p: 8
 ||       natsFrom	s: []	p: 0
 ||       #head	s: []	p: 0
 ||       #u61	s: []	p: 0
 ||       splitAt	s: []	p: 10
 ||       #fst	s: []	p: 0
 ||       #u11	s: [1]	p: 0
 ||       u61	s: [1]	p: 1
 ||       #u81	s: [1,2,4,3]	p: 0
 ||       #u91	s: [2]	p: 0
 ||       isNatural	s: []	p: 2
 ||       u41	s: []	p: 0
 ||       u51	s: [1,2,3]	p: 10
 ||       tail	s: [1]	p: 4
 ||       #mark	s: 1
 ||       0 	s: []	p: 2
 ||       #sel	s: []	p: 0
 ||       u11	s: []	p: 9
 ||       #isLNat	s: []	p: 0
 ||       sel	s: []	p: 2
 ||       #s 	s: []	p: 0
 ||       afterNth	s: [1,2]	p: 9
 ||       #isPLNat	s: []	p: 0
 ||       nil	s: []	p: 2
 ||       isLNat	s: []	p: 4
 ||       #TIlDePAIR	s: []	p: 0
 ||       #tail	s: []	p: 0
 ||       #splitAt	s: [1,2]	p: 0
 ||       mark	s: [1]	p: 2
 ||       u101	s: [2,3,1]	p: 8
 ||       #afterNth	s: [1]	p: 0
 ||       u21	s: [1]	p: 2
 ||       #u41	s: [1,2]	p: 0
 ||       u82	s: 1
 ||       active	s: [1]	p: 9
 ||       head	s: [1]	p: 9
 ||       #snd	s: []	p: 0
 ||       cons	s: [1,2]	p: 2
 ||       #natsFrom	s: []	p: 0
 ||       #active	s: 1
 ||       #u31	s: [1,2]	p: 0
 ||       snd	s: []	p: 8
 ||       tt	s: []	p: 7
 ||       #isNatural	s: []	p: 0
 ||       #pair	s: []	p: 0
 ||       u71	s: [2,1]	p: 11
 ||       u31	s: [2]	p: 2
 ||       #and	s: [1,2]	p: 0
 ||       #u71	s: [1,2]	p: 0
 ||     USABLE RULES: { 67..78 95..102 105..112 115..122 131..142 147..150 153 154 }
 ||     Removed DPs: #54
 || Number of SCCs: 1, DPs: 9
 ||   SCC { #65 #75 #82 #93 #94 #102 #135 #206 #292 }
 || POLO(Sum)... POLO(max)... QLPOS... succeeded.
 ||       u81	s: []	p: 10
 ||       #u101	s: [3]	p: 0
 ||       TIlDePAIR	s: [2]	p: 0
 ||       #u82	s: [1,2]	p: 0
 ||       #cons	s: []	p: 0
 ||       s 	s: [1]	p: 1
 ||       u91	s: []	p: 9
 ||       #take	s: [2]	p: 0
 ||       isPLNat	s: []	p: 3
 ||       #u51	s: [1,3]	p: 0
 ||       take	s: [2,1]	p: 10
 ||       #u21	s: [1]	p: 0
 ||       and	s: 2
 ||       pair	s: []	p: 6
 ||       fst	s: []	p: 8
 ||       natsFrom	s: [1]	p: 0
 ||       #head	s: []	p: 0
 ||       #u61	s: []	p: 0
 ||       splitAt	s: []	p: 10
 ||       #fst	s: []	p: 0
 ||       #u11	s: [1]	p: 0
 ||       u61	s: []	p: 2
 ||       #u81	s: [1,2,4,3]	p: 0
 ||       #u91	s: [2]	p: 0
 ||       isNatural	s: []	p: 2
 ||       u41	s: []	p: 0
 ||       u51	s: [3,2]	p: 10
 ||       tail	s: []	p: 4
 ||       #mark	s: 1
 ||       0 	s: []	p: 2
 ||       #sel	s: []	p: 0
 ||       u11	s: []	p: 9
 ||       #isLNat	s: []	p: 0
 ||       sel	s: []	p: 2
 ||       #s 	s: []	p: 0
 ||       afterNth	s: [1]	p: 9
 ||       #isPLNat	s: []	p: 0
 ||       nil	s: []	p: 5
 ||       isLNat	s: [1]	p: 4
 ||       #TIlDePAIR	s: []	p: 0
 ||       #tail	s: []	p: 0
 ||       #splitAt	s: [1,2]	p: 0
 ||       mark	s: [1]	p: 2
 ||       u101	s: [2,3,1]	p: 8
 ||       #afterNth	s: [1]	p: 0
 ||       u21	s: []	p: 1
 ||       #u41	s: [1,2]	p: 0
 ||       u82	s: 1
 ||       active	s: [1]	p: 9
 ||       head	s: [1]	p: 9
 ||       #snd	s: []	p: 0
 ||       cons	s: [1,2]	p: 2
 ||       #natsFrom	s: []	p: 0
 ||       #active	s: 1
 ||       #u31	s: [1,2]	p: 0
 ||       snd	s: []	p: 6
 ||       tt	s: []	p: 4
 ||       #isNatural	s: []	p: 0
 ||       #pair	s: []	p: 0
 ||       u71	s: [2,1]	p: 11
 ||       u31	s: [2]	p: 2
 ||       #and	s: [1,2]	p: 0
 ||       #u71	s: [1,2]	p: 0
 ||     USABLE RULES: { 67..78 95..102 105..112 115..118 131..142 147..150 153 154 }
 ||     Removed DPs: #292
 || Number of SCCs: 1, DPs: 7
 ||   SCC { #75 #82 #93 #94 #102 #135 #206 }
 || POLO(Sum)... POLO(max)... QLPOS... succeeded.
 ||       u81	s: []	p: 6
 ||       #u101	s: []	p: 0
 ||       TIlDePAIR	s: [2]	p: 0
 ||       #u82	s: [1,2]	p: 0
 ||       #cons	s: []	p: 0
 ||       s 	s: [1]	p: 3
 ||       u91	s: [1]	p: 11
 ||       #take	s: [2]	p: 0
 ||       isPLNat	s: []	p: 12
 ||       #u51	s: [1,3]	p: 0
 ||       take	s: [1,2]	p: 11
 ||       #u21	s: [1]	p: 0
 ||       and	s: [2]	p: 2
 ||       pair	s: []	p: 10
 ||       fst	s: [1]	p: 9
 ||       natsFrom	s: [1]	p: 11
 ||       #head	s: []	p: 0
 ||       #u61	s: []	p: 0
 ||       splitAt	s: []	p: 6
 ||       #fst	s: []	p: 0
 ||       #u11	s: [1]	p: 0
 ||       u61	s: []	p: 0
 ||       #u81	s: [1,2,4,3]	p: 0
 ||       #u91	s: [2]	p: 0
 ||       isNatural	s: []	p: 4
 ||       u41	s: []	p: 11
 ||       u51	s: 2
 ||       tail	s: [1]	p: 11
 ||       #mark	s: [1]	p: 2
 ||       0 	s: []	p: 1
 ||       #sel	s: []	p: 0
 ||       u11	s: [2,1,3]	p: 0
 ||       #isLNat	s: []	p: 0
 ||       sel	s: [1]	p: 6
 ||       #s 	s: []	p: 0
 ||       afterNth	s: [2]	p: 1
 ||       #isPLNat	s: []	p: 0
 ||       nil	s: []	p: 4
 ||       isLNat	s: []	p: 8
 ||       #TIlDePAIR	s: []	p: 0
 ||       #tail	s: []	p: 0
 ||       #splitAt	s: [1,2]	p: 0
 ||       mark	s: [1]	p: 6
 ||       u101	s: [2,3]	p: 11
 ||       #afterNth	s: [1]	p: 0
 ||       u21	s: [1]	p: 9
 ||       #u41	s: [1,2]	p: 0
 ||       u82	s: 1
 ||       active	s: [1]	p: 11
 ||       head	s: []	p: 7
 ||       #snd	s: []	p: 0
 ||       cons	s: []	p: 9
 ||       #natsFrom	s: []	p: 0
 ||       #active	s: [1]	p: 2
 ||       #u31	s: [1,2]	p: 0
 ||       snd	s: [1]	p: 12
 ||       tt	s: []	p: 4
 ||       #isNatural	s: []	p: 0
 ||       #pair	s: []	p: 0
 ||       u71	s: [2,1]	p: 5
 ||       u31	s: []	p: 2
 ||       #and	s: [1,2]	p: 0
 ||       #u71	s: [1,2]	p: 0
 ||     USABLE RULES: { 75..78 87..94 99..102 105..114 119..126 131..154 }
 ||     Removed DPs: #93
 || Number of SCCs: 1, DPs: 5
 ||   SCC { #82 #94 #102 #135 #206 }
 || POLO(Sum)... POLO(max)... QLPOS... POLO(mSum)... QWPOpS(mSum)... succeeded.
 ||       u81	s: [2,4]	p: 1	w: max(x2 + 19, x3 + 14, x4 + 15)
 ||       #u101	s: [3]	p: 0	w: max(x1, x3)
 ||       TIlDePAIR	s: []	p: 0	w: x2
 ||       #u82	s: [1,2]	p: 0	w: max(x1 + 1, x2 + 1)
 ||       #cons	s: [1,2]	p: 0	w: max(x1 + 1, x2 + 1)
 ||       s 	s: [1]	p: 5	w: x1
 ||       u91	s: []	p: 4	w: max(x2 + 1)
 ||       #take	s: [1]	p: 0	w: x1 + 1
 ||       isPLNat	s: []	p: 5	w: 0
 ||       #u51	s: [2]	p: 0	w: max(x2, x3 + 1)
 ||       take	s: [2]	p: 6	w: x1 + x2 + 26
 ||       #u21	s: [1]	p: 0	w: max(x1 + 1)
 ||       and	s: 2
 ||       pair	s: []	p: 0	w: max(x1 + 3, x2)
 ||       fst	s: []	p: 5	w: x1 + 3
 ||       natsFrom	s: []	p: 7	w: x1
 ||       #head	s: []	p: 0	w: 0
 ||       #u61	s: [2,1]	p: 0	w: max(x1 + 1, x2 + 1)
 ||       splitAt	s: [1]	p: 1	w: max(x1 + 19, x2 + 15)
 ||       #fst	s: []	p: 0	w: 0
 ||       #u11	s: [2,3,1]	p: 0	w: max(x1, x2 + 1, x3 + 1)
 ||       u61	s: []	p: 6	w: max(x2 + 1)
 ||       #u81	s: []	p: 0	w: max(x1 + 1, x2 + 1)
 ||       #u91	s: []	p: 0	w: 0
 ||       isNatural	s: []	p: 5	w: 0
 ||       u41	s: []	p: 6	w: max(x2)
 ||       u51	s: [2,3]	p: 7	w: max(x1 + 26, x2 + 25, x3 + 25)
 ||       tail	s: []	p: 4	w: x1 + 1
 ||       #mark	s: [1]	p: 0	w: x1 + 6
 ||       0 	s: []	p: 0	w: 4
 ||       #sel	s: [2,1]	p: 0	w: x1 + x2 + 1
 ||       u11	s: []	p: 0	w: max(x1 + 19, x2 + 22, x3 + 18)
 ||       #isLNat	s: []	p: 0	w: 1
 ||       sel	s: []	p: 8	w: x1 + x2 + 27
 ||       #s 	s: []	p: 0	w: 0
 ||       afterNth	s: [2]	p: 6	w: max(x1 + 23, x2 + 19)
 ||       #isPLNat	s: []	p: 0	w: 0
 ||       nil	s: []	p: 6	w: 0
 ||       isLNat	s: []	p: 5	w: 0
 ||       #TIlDePAIR	s: []	p: 0	w: x1
 ||       #tail	s: []	p: 0	w: 0
 ||       #splitAt	s: [2]	p: 0	w: max(x2 + 1)
 ||       mark	s: 1
 ||       u101	s: []	p: 7	w: max(x1 + 23, x2 + 25, x3 + 24)
 ||       #afterNth	s: [1]	p: 0	w: max(x1)
 ||       u21	s: [1]	p: 5	w: max(x1 + 5, x2 + 4)
 ||       #u41	s: [1,2]	p: 0	w: max(x1 + 1, x2)
 ||       u82	s: [2,1]	p: 0	w: max(x1, x2 + 7)
 ||       active	s: 1
 ||       head	s: []	p: 6	w: x1 + 1
 ||       #snd	s: []	p: 0	w: 1
 ||       cons	s: []	p: 5	w: max(x1, x2)
 ||       #natsFrom	s: []	p: 0	w: 1
 ||       #active	s: [1]	p: 0	w: x1 + 6
 ||       #u31	s: [2,1]	p: 0	w: max(x1 + 1, x2)
 ||       snd	s: []	p: 0	w: x1 + 2
 ||       tt	s: []	p: 2	w: 0
 ||       #isNatural	s: []	p: 0	w: 1
 ||       #pair	s: [2,1]	p: 0	w: max(x1, x2)
 ||       u71	s: []	p: 1	w: max(x1 + 3, x2)
 ||       u31	s: []	p: 0	w: max(x2 + 1)
 ||       #and	s: [1]	p: 0	w: max(x1)
 ||       #u71	s: [2,1]	p: 0	w: max(x1, x2 + 1)
 ||     USABLE RULES: { 1..166 }
 ||     Removed DPs: #94 #102
 || 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:


  Rules R_0:

    active(u101(tt, X, Y)) => mark(fst(splitAt(X, Y))) 
    active(u11(tt, X, Y)) => mark(snd(splitAt(X, Y))) 
    active(u21(tt, X)) => mark(X) 
    active(u31(tt, X)) => mark(X) 
    active(u41(tt, X)) => mark(cons(X, natsFrom(s(X)))) 
    active(u51(tt, X, Y)) => mark(head(afterNth(X, Y))) 
    active(u61(tt, X)) => mark(X) 
    active(u71(tt, X)) => mark(pair(nil, X)) 
    active(u81(tt, X, Y, Z)) => mark(u82(splitAt(X, Z), Y)) 
    active(u82(pair(X, Y), Z)) => mark(pair(cons(Z, X), Y)) 
    active(u91(tt, X)) => mark(X) 
    active(afterNth(X, Y)) => mark(u11(and(isNatural(X), isLNat(Y)), X, Y)) 
    active(and(tt, X)) => mark(X) 
    active(fst(pair(X, Y))) => mark(u21(and(isLNat(X), isLNat(Y)), X)) 
    active(head(cons(X, Y))) => mark(u31(and(isNatural(X), isLNat(Y)), X)) 
    active(isLNat(nil)) => mark(tt) 
    active(isLNat(afterNth(X, Y))) => mark(and(isNatural(X), isLNat(Y))) 
    active(isLNat(cons(X, Y))) => mark(and(isNatural(X), isLNat(Y))) 
    active(isLNat(fst(X))) => mark(isPLNat(X)) 
    active(isLNat(natsFrom(X))) => mark(isNatural(X)) 
    active(isLNat(snd(X))) => mark(isPLNat(X)) 
    active(isLNat(tail(X))) => mark(isLNat(X)) 
    active(isLNat(take(X, Y))) => mark(and(isNatural(X), isLNat(Y))) 
    active(isNatural(0)) => mark(tt) 
    active(isNatural(head(X))) => mark(isLNat(X)) 
    active(isNatural(s(X))) => mark(isNatural(X)) 
    active(isNatural(sel(X, Y))) => mark(and(isNatural(X), isLNat(Y))) 
    active(isPLNat(pair(X, Y))) => mark(and(isLNat(X), isLNat(Y))) 
    active(isPLNat(splitAt(X, Y))) => mark(and(isNatural(X), isLNat(Y))) 
    active(natsFrom(X)) => mark(u41(isNatural(X), X)) 
    active(sel(X, Y)) => mark(u51(and(isNatural(X), isLNat(Y)), X, Y)) 
    active(snd(pair(X, Y))) => mark(u61(and(isLNat(X), isLNat(Y)), Y)) 
    active(splitAt(0, X)) => mark(u71(isLNat(X), X)) 
    active(splitAt(s(X), cons(Y, Z))) => mark(u81(and(isNatural(X), and(isNatural(Y), isLNat(Z))), X, Y, Z)) 
    active(tail(cons(X, Y))) => mark(u91(and(isNatural(X), isLNat(Y)), Y)) 
    active(take(X, Y)) => mark(u101(and(isNatural(X), isLNat(Y)), X, Y)) 
    mark(u101(X, Y, Z)) => active(u101(mark(X), Y, Z)) 
    mark(tt) => active(tt) 
    mark(fst(X)) => active(fst(mark(X))) 
    mark(splitAt(X, Y)) => active(splitAt(mark(X), mark(Y))) 
    mark(u11(X, Y, Z)) => active(u11(mark(X), Y, Z)) 
    mark(snd(X)) => active(snd(mark(X))) 
    mark(u21(X, Y)) => active(u21(mark(X), Y)) 
    mark(u31(X, Y)) => active(u31(mark(X), Y)) 
    mark(u41(X, Y)) => active(u41(mark(X), Y)) 
    mark(cons(X, Y)) => active(cons(mark(X), Y)) 
    mark(natsFrom(X)) => active(natsFrom(mark(X))) 
    mark(s(X)) => active(s(mark(X))) 
    mark(u51(X, Y, Z)) => active(u51(mark(X), Y, Z)) 
    mark(head(X)) => active(head(mark(X))) 
    mark(afterNth(X, Y)) => active(afterNth(mark(X), mark(Y))) 
    mark(u61(X, Y)) => active(u61(mark(X), Y)) 
    mark(u71(X, Y)) => active(u71(mark(X), Y)) 
    mark(pair(X, Y)) => active(pair(mark(X), mark(Y))) 
    mark(nil) => active(nil) 
    mark(u81(X, Y, Z, U)) => active(u81(mark(X), Y, Z, U)) 
    mark(u82(X, Y)) => active(u82(mark(X), Y)) 
    mark(u91(X, Y)) => active(u91(mark(X), Y)) 
    mark(and(X, Y)) => active(and(mark(X), Y)) 
    mark(isNatural(X)) => active(isNatural(X)) 
    mark(isLNat(X)) => active(isLNat(X)) 
    mark(isPLNat(X)) => active(isPLNat(X)) 
    mark(tail(X)) => active(tail(mark(X))) 
    mark(take(X, Y)) => active(take(mark(X), mark(Y))) 
    mark(0) => active(0) 
    mark(sel(X, Y)) => active(sel(mark(X), mark(Y))) 
    u101(mark(X), Y, Z) => u101(X, Y, Z) 
    u101(X, mark(Y), Z) => u101(X, Y, Z) 
    u101(X, Y, mark(Z)) => u101(X, Y, Z) 
    u101(active(X), Y, Z) => u101(X, Y, Z) 
    u101(X, active(Y), Z) => u101(X, Y, Z) 
    u101(X, Y, active(Z)) => u101(X, Y, Z) 
    fst(mark(X)) => fst(X) 
    fst(active(X)) => fst(X) 
    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) 
    u11(mark(X), Y, Z) => u11(X, Y, Z) 
    u11(X, mark(Y), Z) => u11(X, Y, Z) 
    u11(X, Y, mark(Z)) => u11(X, Y, Z) 
    u11(active(X), Y, Z) => u11(X, Y, Z) 
    u11(X, active(Y), Z) => u11(X, Y, Z) 
    u11(X, Y, active(Z)) => u11(X, Y, Z) 
    snd(mark(X)) => snd(X) 
    snd(active(X)) => snd(X) 
    u21(mark(X), Y) => u21(X, Y) 
    u21(X, mark(Y)) => u21(X, Y) 
    u21(active(X), Y) => u21(X, Y) 
    u21(X, active(Y)) => u21(X, Y) 
    u31(mark(X), Y) => u31(X, Y) 
    u31(X, mark(Y)) => u31(X, Y) 
    u31(active(X), Y) => u31(X, Y) 
    u31(X, active(Y)) => u31(X, Y) 
    u41(mark(X), Y) => u41(X, Y) 
    u41(X, mark(Y)) => u41(X, Y) 
    u41(active(X), Y) => u41(X, Y) 
    u41(X, active(Y)) => u41(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) 
    natsFrom(mark(X)) => natsFrom(X) 
    natsFrom(active(X)) => natsFrom(X) 
    s(mark(X)) => s(X) 
    s(active(X)) => s(X) 
    u51(mark(X), Y, Z) => u51(X, Y, Z) 
    u51(X, mark(Y), Z) => u51(X, Y, Z) 
    u51(X, Y, mark(Z)) => u51(X, Y, Z) 
    u51(active(X), Y, Z) => u51(X, Y, Z) 
    u51(X, active(Y), Z) => u51(X, Y, Z) 
    u51(X, Y, active(Z)) => u51(X, Y, Z) 
    head(mark(X)) => head(X) 
    head(active(X)) => head(X) 
    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) 
    u61(mark(X), Y) => u61(X, Y) 
    u61(X, mark(Y)) => u61(X, Y) 
    u61(active(X), Y) => u61(X, Y) 
    u61(X, active(Y)) => u61(X, Y) 
    u71(mark(X), Y) => u71(X, Y) 
    u71(X, mark(Y)) => u71(X, Y) 
    u71(active(X), Y) => u71(X, Y) 
    u71(X, active(Y)) => u71(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) 
    u81(mark(X), Y, Z, U) => u81(X, Y, Z, U) 
    u81(X, mark(Y), Z, U) => u81(X, Y, Z, U) 
    u81(X, Y, mark(Z), U) => u81(X, Y, Z, U) 
    u81(X, Y, Z, mark(U)) => u81(X, Y, Z, U) 
    u81(active(X), Y, Z, U) => u81(X, Y, Z, U) 
    u81(X, active(Y), Z, U) => u81(X, Y, Z, U) 
    u81(X, Y, active(Z), U) => u81(X, Y, Z, U) 
    u81(X, Y, Z, active(U)) => u81(X, Y, Z, U) 
    u82(mark(X), Y) => u82(X, Y) 
    u82(X, mark(Y)) => u82(X, Y) 
    u82(active(X), Y) => u82(X, Y) 
    u82(X, active(Y)) => u82(X, Y) 
    u91(mark(X), Y) => u91(X, Y) 
    u91(X, mark(Y)) => u91(X, Y) 
    u91(active(X), Y) => u91(X, Y) 
    u91(X, active(Y)) => u91(X, Y) 
    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) 
    isNatural(mark(X)) => isNatural(X) 
    isNatural(active(X)) => isNatural(X) 
    isLNat(mark(X)) => isLNat(X) 
    isLNat(active(X)) => isLNat(X) 
    isPLNat(mark(X)) => isPLNat(X) 
    isPLNat(active(X)) => isPLNat(X) 
    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) 
    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) 
    map(/\x.X(x), nil) => nil 
    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:


This graph has no strongly connected components.  By [Kop12, Thm. 7.31], this implies finiteness of the dependency pair problem.

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.