We consider the system h41. Alphabet: 0 : [] --> A active : [] --> A -> A afterNth : [] --> A -> A -> A app : [] --> (A -> A) -> A -> A cons : [] --> A -> A -> A fst : [] --> A -> A head : [] --> A -> A map : [] --> (A -> A) -> A -> A mark : [] --> A -> A natsFrom : [] --> A -> A nil : [] --> A pair : [] --> A -> A -> A s : [] --> A -> A sel : [] --> A -> A -> A snd : [] --> A -> A splitAt : [] --> A -> A -> A tail : [] --> A -> A take : [] --> A -> A -> A tt : [] --> A u11 : [] --> A -> A -> A -> A u12 : [] --> A -> A -> A -> A u21 : [] --> A -> A -> A u22 : [] --> A -> A -> A u31 : [] --> A -> A -> A u32 : [] --> A -> A -> A u41 : [] --> A -> A -> A -> A u42 : [] --> A -> A -> A -> A u51 : [] --> A -> A -> A u52 : [] --> A -> A -> A u61 : [] --> A -> A -> A -> A -> A u62 : [] --> A -> A -> A -> A -> A u63 : [] --> A -> A -> A -> A -> A u64 : [] --> A -> A -> A u71 : [] --> A -> A -> A u72 : [] --> A -> A -> A u81 : [] --> A -> A -> A -> A u82 : [] --> A -> A -> A -> A Rules: active (u11 tt x y) => mark (u12 tt x y) active (u12 tt x y) => mark (snd (splitAt x y)) active (u21 tt x) => mark (u22 tt x) active (u22 tt x) => mark x active (u31 tt x) => mark (u32 tt x) active (u32 tt x) => mark x active (u41 tt x y) => mark (u42 tt x y) active (u42 tt x y) => mark (head (afterNth x y)) active (u51 tt x) => mark (u52 tt x) active (u52 tt x) => mark x active (u61 tt x y z) => mark (u62 tt x y z) active (u62 tt x y z) => mark (u63 tt x y z) active (u63 tt x y z) => mark (u64 (splitAt x z) y) active (u64 (pair x y) z) => mark (pair (cons z x) y) active (u71 tt x) => mark (u72 tt x) active (u72 tt x) => mark x active (u81 tt x y) => mark (u82 tt x y) active (u82 tt x y) => mark (fst (splitAt x y)) active (afterNth x y) => mark (u11 tt x y) active (fst (pair x y)) => mark (u21 tt x) active (head (cons x y)) => mark (u31 tt x) active (natsFrom x) => mark (cons x (natsFrom (s x))) active (sel x y) => mark (u41 tt x y) active (snd (pair x y)) => mark (u51 tt y) active (splitAt 0 x) => mark (pair nil x) active (splitAt (s x) (cons y z)) => mark (u61 tt x y z) active (tail (cons x y)) => mark (u71 tt y) active (take x y) => mark (u81 tt x y) mark (u11 x y z) => active (u11 (mark x) y z) mark tt => active tt mark (u12 x y z) => active (u12 (mark x) y z) mark (snd x) => active (snd (mark x)) mark (splitAt x y) => active (splitAt (mark x) (mark y)) mark (u21 x y) => active (u21 (mark x) y) mark (u22 x y) => active (u22 (mark x) y) mark (u31 x y) => active (u31 (mark x) y) mark (u32 x y) => active (u32 (mark x) y) mark (u41 x y z) => active (u41 (mark x) y z) mark (u42 x y z) => active (u42 (mark x) y z) mark (head x) => active (head (mark x)) mark (afterNth x y) => active (afterNth (mark x) (mark y)) mark (u51 x y) => active (u51 (mark x) y) mark (u52 x y) => active (u52 (mark x) y) mark (u61 x y z u) => active (u61 (mark x) y z u) mark (u62 x y z u) => active (u62 (mark x) y z u) mark (u63 x y z u) => active (u63 (mark x) y z u) mark (u64 x y) => active (u64 (mark x) y) mark (pair x y) => active (pair (mark x) (mark y)) mark (cons x y) => active (cons (mark x) y) mark (u71 x y) => active (u71 (mark x) y) mark (u72 x y) => active (u72 (mark x) y) mark (u81 x y z) => active (u81 (mark x) y z) mark (u82 x y z) => active (u82 (mark x) y z) mark (fst x) => active (fst (mark x)) mark (natsFrom x) => active (natsFrom (mark x)) mark (s x) => active (s (mark x)) mark (sel x y) => active (sel (mark x) (mark y)) mark 0 => active 0 mark nil => active nil mark (tail x) => active (tail (mark x)) mark (take x y) => active (take (mark x) (mark y)) u11 (mark x) y z => 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 u12 (mark x) y z => u12 x y z u12 x (mark y) z => u12 x y z u12 x y (mark z) => u12 x y z u12 (active x) y z => u12 x y z u12 x (active y) z => u12 x y z u12 x y (active z) => u12 x y z snd (mark x) => snd x snd (active x) => snd 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 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 u22 (mark x) y => u22 x y u22 x (mark y) => u22 x y u22 (active x) y => u22 x y u22 x (active y) => u22 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 u32 (mark x) y => u32 x y u32 x (mark y) => u32 x y u32 (active x) y => u32 x y u32 x (active y) => u32 x y u41 (mark x) y z => u41 x y z u41 x (mark y) z => u41 x y z u41 x y (mark z) => u41 x y z u41 (active x) y z => u41 x y z u41 x (active y) z => u41 x y z u41 x y (active z) => u41 x y z u42 (mark x) y z => u42 x y z u42 x (mark y) z => u42 x y z u42 x y (mark z) => u42 x y z u42 (active x) y z => u42 x y z u42 x (active y) z => u42 x y z u42 x y (active z) => u42 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 u51 (mark x) y => u51 x y u51 x (mark y) => u51 x y u51 (active x) y => u51 x y u51 x (active y) => u51 x y u52 (mark x) y => u52 x y u52 x (mark y) => u52 x y u52 (active x) y => u52 x y u52 x (active y) => u52 x y u61 (mark x) y z u => u61 x y z u u61 x (mark y) z u => u61 x y z u u61 x y (mark z) u => u61 x y z u u61 x y z (mark u) => u61 x y z u u61 (active x) y z u => u61 x y z u u61 x (active y) z u => u61 x y z u u61 x y (active z) u => u61 x y z u u61 x y z (active u) => u61 x y z u u62 (mark x) y z u => u62 x y z u u62 x (mark y) z u => u62 x y z u u62 x y (mark z) u => u62 x y z u u62 x y z (mark u) => u62 x y z u u62 (active x) y z u => u62 x y z u u62 x (active y) z u => u62 x y z u u62 x y (active z) u => u62 x y z u u62 x y z (active u) => u62 x y z u u63 (mark x) y z u => u63 x y z u u63 x (mark y) z u => u63 x y z u u63 x y (mark z) u => u63 x y z u u63 x y z (mark u) => u63 x y z u u63 (active x) y z u => u63 x y z u u63 x (active y) z u => u63 x y z u u63 x y (active z) u => u63 x y z u u63 x y z (active u) => u63 x y z u u64 (mark x) y => u64 x y u64 x (mark y) => u64 x y u64 (active x) y => u64 x y u64 x (active y) => u64 x y pair (mark x) y => pair x y pair x (mark y) => pair x y pair (active x) y => pair x y pair x (active y) => pair x y cons (mark x) y => cons x y cons x (mark y) => cons x y cons (active x) y => cons x y cons x (active y) => cons x y 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 u72 (mark x) y => u72 x y u72 x (mark y) => u72 x y u72 (active x) y => u72 x y u72 x (active y) => u72 x y u81 (mark x) y z => u81 x y z u81 x (mark y) z => u81 x y z u81 x y (mark z) => u81 x y z u81 (active x) y z => u81 x y z u81 x (active y) z => u81 x y z u81 x y (active z) => u81 x y z u82 (mark x) y z => u82 x y z u82 x (mark y) z => u82 x y z u82 x y (mark z) => u82 x y z u82 (active x) y z => u82 x y z u82 x (active y) z => u82 x y z u82 x y (active z) => u82 x y z fst (mark x) => fst x fst (active x) => fst x natsFrom (mark x) => natsFrom x natsFrom (active x) => natsFrom x s (mark x) => s x s (active x) => s x sel (mark x) y => sel x y sel x (mark y) => sel x y sel (active x) y => sel x y sel x (active y) => sel x y tail (mark x) => tail x tail (active x) => tail x take (mark x) y => take x y take x (mark y) => take x y take (active x) y => take x y take x (active y) => take x y map (/\x.f x) nil => nil map (/\x.f x) (cons y z) => cons (f y) (map (/\u.f u) z) app (/\x.f x) y => f y Using the transformations described in [Kop11], this system can be brought in a form without leading free variables in the left-hand side, and where the left-hand side of a variable is always a functional term or application headed by a functional term. We now transform the resulting AFS into an AFSM by replacing all free variables by meta-variables (with arity 0). This leads to the following AFSM: Alphabet: 0 : [] --> A active : [A] --> A afterNth : [A * A] --> A app : [A -> A * A] --> A cons : [A * A] --> A fst : [A] --> A head : [A] --> A map : [A -> A * A] --> A mark : [A] --> A natsFrom : [A] --> A nil : [] --> A pair : [A * A] --> A s : [A] --> A sel : [A * A] --> A snd : [A] --> A splitAt : [A * A] --> A tail : [A] --> A take : [A * A] --> A tt : [] --> A u11 : [A * A * A] --> A u12 : [A * A * A] --> A u21 : [A * A] --> A u22 : [A * A] --> A u31 : [A * A] --> A u32 : [A * A] --> A u41 : [A * A * A] --> A u42 : [A * A * A] --> A u51 : [A * A] --> A u52 : [A * A] --> A u61 : [A * A * A * A] --> A u62 : [A * A * A * A] --> A u63 : [A * A * A * A] --> A u64 : [A * A] --> A u71 : [A * A] --> A u72 : [A * A] --> A u81 : [A * A * A] --> A u82 : [A * A * A] --> A ~AP1 : [A -> A * A] --> A Rules: active(u11(tt, X, Y)) => mark(u12(tt, X, Y)) active(u12(tt, X, Y)) => mark(snd(splitAt(X, Y))) active(u21(tt, X)) => mark(u22(tt, X)) active(u22(tt, X)) => mark(X) active(u31(tt, X)) => mark(u32(tt, X)) active(u32(tt, X)) => mark(X) active(u41(tt, X, Y)) => mark(u42(tt, X, Y)) active(u42(tt, X, Y)) => mark(head(afterNth(X, Y))) active(u51(tt, X)) => mark(u52(tt, X)) active(u52(tt, X)) => mark(X) active(u61(tt, X, Y, Z)) => mark(u62(tt, X, Y, Z)) active(u62(tt, X, Y, Z)) => mark(u63(tt, X, Y, Z)) active(u63(tt, X, Y, Z)) => mark(u64(splitAt(X, Z), Y)) active(u64(pair(X, Y), Z)) => mark(pair(cons(Z, X), Y)) active(u71(tt, X)) => mark(u72(tt, X)) active(u72(tt, X)) => mark(X) active(u81(tt, X, Y)) => mark(u82(tt, X, Y)) active(u82(tt, X, Y)) => mark(fst(splitAt(X, Y))) active(afterNth(X, Y)) => mark(u11(tt, X, Y)) active(fst(pair(X, Y))) => mark(u21(tt, X)) active(head(cons(X, Y))) => mark(u31(tt, X)) active(natsFrom(X)) => mark(cons(X, natsFrom(s(X)))) active(sel(X, Y)) => mark(u41(tt, X, Y)) active(snd(pair(X, Y))) => mark(u51(tt, Y)) active(splitAt(0, X)) => mark(pair(nil, X)) active(splitAt(s(X), cons(Y, Z))) => mark(u61(tt, X, Y, Z)) active(tail(cons(X, Y))) => mark(u71(tt, Y)) active(take(X, Y)) => mark(u81(tt, X, Y)) mark(u11(X, Y, Z)) => active(u11(mark(X), Y, Z)) mark(tt) => active(tt) mark(u12(X, Y, Z)) => active(u12(mark(X), Y, Z)) mark(snd(X)) => active(snd(mark(X))) mark(splitAt(X, Y)) => active(splitAt(mark(X), mark(Y))) mark(u21(X, Y)) => active(u21(mark(X), Y)) mark(u22(X, Y)) => active(u22(mark(X), Y)) mark(u31(X, Y)) => active(u31(mark(X), Y)) mark(u32(X, Y)) => active(u32(mark(X), Y)) mark(u41(X, Y, Z)) => active(u41(mark(X), Y, Z)) mark(u42(X, Y, Z)) => active(u42(mark(X), Y, Z)) mark(head(X)) => active(head(mark(X))) mark(afterNth(X, Y)) => active(afterNth(mark(X), mark(Y))) mark(u51(X, Y)) => active(u51(mark(X), Y)) mark(u52(X, Y)) => active(u52(mark(X), Y)) mark(u61(X, Y, Z, U)) => active(u61(mark(X), Y, Z, U)) mark(u62(X, Y, Z, U)) => active(u62(mark(X), Y, Z, U)) mark(u63(X, Y, Z, U)) => active(u63(mark(X), Y, Z, U)) mark(u64(X, Y)) => active(u64(mark(X), Y)) mark(pair(X, Y)) => active(pair(mark(X), mark(Y))) mark(cons(X, Y)) => active(cons(mark(X), Y)) mark(u71(X, Y)) => active(u71(mark(X), Y)) mark(u72(X, Y)) => active(u72(mark(X), Y)) mark(u81(X, Y, Z)) => active(u81(mark(X), Y, Z)) mark(u82(X, Y, Z)) => active(u82(mark(X), Y, Z)) mark(fst(X)) => active(fst(mark(X))) mark(natsFrom(X)) => active(natsFrom(mark(X))) mark(s(X)) => active(s(mark(X))) mark(sel(X, Y)) => active(sel(mark(X), mark(Y))) mark(0) => active(0) mark(nil) => active(nil) mark(tail(X)) => active(tail(mark(X))) mark(take(X, Y)) => active(take(mark(X), mark(Y))) u11(mark(X), Y, Z) => 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) u12(mark(X), Y, Z) => u12(X, Y, Z) u12(X, mark(Y), Z) => u12(X, Y, Z) u12(X, Y, mark(Z)) => u12(X, Y, Z) u12(active(X), Y, Z) => u12(X, Y, Z) u12(X, active(Y), Z) => u12(X, Y, Z) u12(X, Y, active(Z)) => u12(X, Y, Z) snd(mark(X)) => snd(X) snd(active(X)) => snd(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) 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) u22(mark(X), Y) => u22(X, Y) u22(X, mark(Y)) => u22(X, Y) u22(active(X), Y) => u22(X, Y) u22(X, active(Y)) => u22(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) u32(mark(X), Y) => u32(X, Y) u32(X, mark(Y)) => u32(X, Y) u32(active(X), Y) => u32(X, Y) u32(X, active(Y)) => u32(X, Y) u41(mark(X), Y, Z) => u41(X, Y, Z) u41(X, mark(Y), Z) => u41(X, Y, Z) u41(X, Y, mark(Z)) => u41(X, Y, Z) u41(active(X), Y, Z) => u41(X, Y, Z) u41(X, active(Y), Z) => u41(X, Y, Z) u41(X, Y, active(Z)) => u41(X, Y, Z) u42(mark(X), Y, Z) => u42(X, Y, Z) u42(X, mark(Y), Z) => u42(X, Y, Z) u42(X, Y, mark(Z)) => u42(X, Y, Z) u42(active(X), Y, Z) => u42(X, Y, Z) u42(X, active(Y), Z) => u42(X, Y, Z) u42(X, Y, active(Z)) => u42(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) u51(mark(X), Y) => u51(X, Y) u51(X, mark(Y)) => u51(X, Y) u51(active(X), Y) => u51(X, Y) u51(X, active(Y)) => u51(X, Y) u52(mark(X), Y) => u52(X, Y) u52(X, mark(Y)) => u52(X, Y) u52(active(X), Y) => u52(X, Y) u52(X, active(Y)) => u52(X, Y) u61(mark(X), Y, Z, U) => u61(X, Y, Z, U) u61(X, mark(Y), Z, U) => u61(X, Y, Z, U) u61(X, Y, mark(Z), U) => u61(X, Y, Z, U) u61(X, Y, Z, mark(U)) => u61(X, Y, Z, U) u61(active(X), Y, Z, U) => u61(X, Y, Z, U) u61(X, active(Y), Z, U) => u61(X, Y, Z, U) u61(X, Y, active(Z), U) => u61(X, Y, Z, U) u61(X, Y, Z, active(U)) => u61(X, Y, Z, U) u62(mark(X), Y, Z, U) => u62(X, Y, Z, U) u62(X, mark(Y), Z, U) => u62(X, Y, Z, U) u62(X, Y, mark(Z), U) => u62(X, Y, Z, U) u62(X, Y, Z, mark(U)) => u62(X, Y, Z, U) u62(active(X), Y, Z, U) => u62(X, Y, Z, U) u62(X, active(Y), Z, U) => u62(X, Y, Z, U) u62(X, Y, active(Z), U) => u62(X, Y, Z, U) u62(X, Y, Z, active(U)) => u62(X, Y, Z, U) u63(mark(X), Y, Z, U) => u63(X, Y, Z, U) u63(X, mark(Y), Z, U) => u63(X, Y, Z, U) u63(X, Y, mark(Z), U) => u63(X, Y, Z, U) u63(X, Y, Z, mark(U)) => u63(X, Y, Z, U) u63(active(X), Y, Z, U) => u63(X, Y, Z, U) u63(X, active(Y), Z, U) => u63(X, Y, Z, U) u63(X, Y, active(Z), U) => u63(X, Y, Z, U) u63(X, Y, Z, active(U)) => u63(X, Y, Z, U) u64(mark(X), Y) => u64(X, Y) u64(X, mark(Y)) => u64(X, Y) u64(active(X), Y) => u64(X, Y) u64(X, active(Y)) => u64(X, Y) pair(mark(X), Y) => pair(X, Y) pair(X, mark(Y)) => pair(X, Y) pair(active(X), Y) => pair(X, Y) pair(X, active(Y)) => pair(X, Y) cons(mark(X), Y) => cons(X, Y) cons(X, mark(Y)) => cons(X, Y) cons(active(X), Y) => cons(X, Y) cons(X, active(Y)) => cons(X, Y) 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) u72(mark(X), Y) => u72(X, Y) u72(X, mark(Y)) => u72(X, Y) u72(active(X), Y) => u72(X, Y) u72(X, active(Y)) => u72(X, Y) u81(mark(X), Y, Z) => u81(X, Y, Z) u81(X, mark(Y), Z) => u81(X, Y, Z) u81(X, Y, mark(Z)) => u81(X, Y, Z) u81(active(X), Y, Z) => u81(X, Y, Z) u81(X, active(Y), Z) => u81(X, Y, Z) u81(X, Y, active(Z)) => u81(X, Y, Z) u82(mark(X), Y, Z) => u82(X, Y, Z) u82(X, mark(Y), Z) => u82(X, Y, Z) u82(X, Y, mark(Z)) => u82(X, Y, Z) u82(active(X), Y, Z) => u82(X, Y, Z) u82(X, active(Y), Z) => u82(X, Y, Z) u82(X, Y, active(Z)) => u82(X, Y, Z) fst(mark(X)) => fst(X) fst(active(X)) => fst(X) natsFrom(mark(X)) => natsFrom(X) natsFrom(active(X)) => natsFrom(X) s(mark(X)) => s(X) s(active(X)) => s(X) sel(mark(X), Y) => sel(X, Y) sel(X, mark(Y)) => sel(X, Y) sel(active(X), Y) => sel(X, Y) sel(X, active(Y)) => sel(X, Y) tail(mark(X)) => tail(X) tail(active(X)) => tail(X) take(mark(X), Y) => take(X, Y) take(X, mark(Y)) => take(X, Y) take(active(X), Y) => take(X, Y) take(X, active(Y)) => take(X, Y) map(/\x.~AP1(F, x), nil) => nil map(/\x.~AP1(F, x), cons(X, Y)) => cons(~AP1(F, X), map(/\y.~AP1(F, y), Y)) app(/\x.~AP1(F, x), X) => ~AP1(F, X) map(/\x.active(x), nil) => nil map(/\x.afterNth(X, x), nil) => nil map(/\x.app(F, x), nil) => nil map(/\x.cons(X, x), nil) => nil map(/\x.fst(x), nil) => nil map(/\x.head(x), nil) => nil map(/\x.map(F, x), nil) => nil map(/\x.mark(x), nil) => nil map(/\x.natsFrom(x), nil) => nil map(/\x.pair(X, x), nil) => nil map(/\x.s(x), nil) => nil map(/\x.sel(X, x), nil) => nil map(/\x.snd(x), nil) => nil map(/\x.splitAt(X, x), nil) => nil map(/\x.tail(x), nil) => nil map(/\x.take(X, x), nil) => nil map(/\x.u11(X, Y, x), nil) => nil map(/\x.u12(X, Y, x), nil) => nil map(/\x.u21(X, x), nil) => nil map(/\x.u22(X, x), nil) => nil map(/\x.u31(X, x), nil) => nil map(/\x.u32(X, x), nil) => nil map(/\x.u41(X, Y, x), nil) => nil map(/\x.u42(X, Y, x), nil) => nil map(/\x.u51(X, x), nil) => nil map(/\x.u52(X, x), nil) => nil map(/\x.u61(X, Y, Z, x), nil) => nil map(/\x.u62(X, Y, Z, x), nil) => nil map(/\x.u63(X, Y, Z, x), nil) => nil map(/\x.u64(X, x), nil) => nil map(/\x.u71(X, x), nil) => nil map(/\x.u72(X, x), nil) => nil map(/\x.u81(X, Y, x), nil) => nil map(/\x.u82(X, Y, x), nil) => nil map(/\x.active(x), cons(X, Y)) => cons(active(X), map(/\y.active(y), Y)) map(/\x.afterNth(X, x), cons(Y, Z)) => cons(afterNth(X, Y), map(/\y.afterNth(X, y), Z)) map(/\x.app(F, x), cons(X, Y)) => cons(app(F, X), map(/\y.app(F, y), Y)) map(/\x.cons(X, x), cons(Y, Z)) => cons(cons(X, Y), map(/\y.cons(X, y), Z)) map(/\x.fst(x), cons(X, Y)) => cons(fst(X), map(/\y.fst(y), Y)) map(/\x.head(x), cons(X, Y)) => cons(head(X), map(/\y.head(y), Y)) map(/\x.map(F, x), cons(X, Y)) => cons(map(F, X), map(/\y.map(F, y), Y)) map(/\x.mark(x), cons(X, Y)) => cons(mark(X), map(/\y.mark(y), Y)) map(/\x.natsFrom(x), cons(X, Y)) => cons(natsFrom(X), map(/\y.natsFrom(y), Y)) map(/\x.pair(X, x), cons(Y, Z)) => cons(pair(X, Y), map(/\y.pair(X, y), Z)) map(/\x.s(x), cons(X, Y)) => cons(s(X), map(/\y.s(y), Y)) map(/\x.sel(X, x), cons(Y, Z)) => cons(sel(X, Y), map(/\y.sel(X, y), Z)) map(/\x.snd(x), cons(X, Y)) => cons(snd(X), map(/\y.snd(y), Y)) map(/\x.splitAt(X, x), cons(Y, Z)) => cons(splitAt(X, Y), map(/\y.splitAt(X, y), Z)) map(/\x.tail(x), cons(X, Y)) => cons(tail(X), map(/\y.tail(y), Y)) map(/\x.take(X, x), cons(Y, Z)) => cons(take(X, Y), map(/\y.take(X, y), Z)) map(/\x.u11(X, Y, x), cons(Z, U)) => cons(u11(X, Y, Z), map(/\y.u11(X, Y, y), U)) map(/\x.u12(X, Y, x), cons(Z, U)) => cons(u12(X, Y, Z), map(/\y.u12(X, Y, y), U)) map(/\x.u21(X, x), cons(Y, Z)) => cons(u21(X, Y), map(/\y.u21(X, y), Z)) map(/\x.u22(X, x), cons(Y, Z)) => cons(u22(X, Y), map(/\y.u22(X, y), Z)) map(/\x.u31(X, x), cons(Y, Z)) => cons(u31(X, Y), map(/\y.u31(X, y), Z)) map(/\x.u32(X, x), cons(Y, Z)) => cons(u32(X, Y), map(/\y.u32(X, y), Z)) map(/\x.u41(X, Y, x), cons(Z, U)) => cons(u41(X, Y, Z), map(/\y.u41(X, Y, y), U)) map(/\x.u42(X, Y, x), cons(Z, U)) => cons(u42(X, Y, Z), map(/\y.u42(X, Y, y), U)) map(/\x.u51(X, x), cons(Y, Z)) => cons(u51(X, Y), map(/\y.u51(X, y), Z)) map(/\x.u52(X, x), cons(Y, Z)) => cons(u52(X, Y), map(/\y.u52(X, y), Z)) map(/\x.u61(X, Y, Z, x), cons(U, V)) => cons(u61(X, Y, Z, U), map(/\y.u61(X, Y, Z, y), V)) map(/\x.u62(X, Y, Z, x), cons(U, V)) => cons(u62(X, Y, Z, U), map(/\y.u62(X, Y, Z, y), V)) map(/\x.u63(X, Y, Z, x), cons(U, V)) => cons(u63(X, Y, Z, U), map(/\y.u63(X, Y, Z, y), V)) map(/\x.u64(X, x), cons(Y, Z)) => cons(u64(X, Y), map(/\y.u64(X, y), Z)) map(/\x.u71(X, x), cons(Y, Z)) => cons(u71(X, Y), map(/\y.u71(X, y), Z)) map(/\x.u72(X, x), cons(Y, Z)) => cons(u72(X, Y), map(/\y.u72(X, y), Z)) map(/\x.u81(X, Y, x), cons(Z, U)) => cons(u81(X, Y, Z), map(/\y.u81(X, Y, y), U)) map(/\x.u82(X, Y, x), cons(Z, U)) => cons(u82(X, Y, Z), map(/\y.u82(X, Y, y), U)) app(/\x.active(x), X) => active(X) app(/\x.afterNth(X, x), Y) => afterNth(X, Y) app(/\x.app(F, x), X) => app(F, X) app(/\x.cons(X, x), Y) => cons(X, Y) app(/\x.fst(x), X) => fst(X) app(/\x.head(x), X) => head(X) app(/\x.map(F, x), X) => map(F, X) app(/\x.mark(x), X) => mark(X) app(/\x.natsFrom(x), X) => natsFrom(X) app(/\x.pair(X, x), Y) => pair(X, Y) app(/\x.s(x), X) => s(X) app(/\x.sel(X, x), Y) => sel(X, Y) app(/\x.snd(x), X) => snd(X) app(/\x.splitAt(X, x), Y) => splitAt(X, Y) app(/\x.tail(x), X) => tail(X) app(/\x.take(X, x), Y) => take(X, Y) app(/\x.u11(X, Y, x), Z) => u11(X, Y, Z) app(/\x.u12(X, Y, x), Z) => u12(X, Y, Z) app(/\x.u21(X, x), Y) => u21(X, Y) app(/\x.u22(X, x), Y) => u22(X, Y) app(/\x.u31(X, x), Y) => u31(X, Y) app(/\x.u32(X, x), Y) => u32(X, Y) app(/\x.u41(X, Y, x), Z) => u41(X, Y, Z) app(/\x.u42(X, Y, x), Z) => u42(X, Y, Z) app(/\x.u51(X, x), Y) => u51(X, Y) app(/\x.u52(X, x), Y) => u52(X, Y) app(/\x.u61(X, Y, Z, x), U) => u61(X, Y, Z, U) app(/\x.u62(X, Y, Z, x), U) => u62(X, Y, Z, U) app(/\x.u63(X, Y, Z, x), U) => u63(X, Y, Z, U) app(/\x.u64(X, x), Y) => u64(X, Y) app(/\x.u71(X, x), Y) => u71(X, Y) app(/\x.u72(X, x), Y) => u72(X, Y) app(/\x.u81(X, Y, x), Z) => u81(X, Y, Z) app(/\x.u82(X, Y, x), Z) => u82(X, Y, Z) ~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 app : [A -> A * A] --> A cons : [A * A] --> A fst : [A] --> A head : [A] --> A map : [A -> A * A] --> A mark : [A] --> A natsFrom : [A] --> A nil : [] --> A pair : [A * A] --> A s : [A] --> A sel : [A * A] --> A snd : [A] --> A splitAt : [A * A] --> A tail : [A] --> A take : [A * A] --> A tt : [] --> A u11 : [A * A * A] --> A u12 : [A * A * A] --> A u21 : [A * A] --> A u22 : [A * A] --> A u31 : [A * A] --> A u32 : [A * A] --> A u41 : [A * A * A] --> A u42 : [A * A * A] --> A u51 : [A * A] --> A u52 : [A * A] --> A u61 : [A * A * A * A] --> A u62 : [A * A * A * A] --> A u63 : [A * A * A * A] --> A u64 : [A * A] --> A u71 : [A * A] --> A u72 : [A * A] --> A u81 : [A * A * A] --> A u82 : [A * A * A] --> A Rules: active(u11(tt, X, Y)) => mark(u12(tt, X, Y)) active(u12(tt, X, Y)) => mark(snd(splitAt(X, Y))) active(u21(tt, X)) => mark(u22(tt, X)) active(u22(tt, X)) => mark(X) active(u31(tt, X)) => mark(u32(tt, X)) active(u32(tt, X)) => mark(X) active(u41(tt, X, Y)) => mark(u42(tt, X, Y)) active(u42(tt, X, Y)) => mark(head(afterNth(X, Y))) active(u51(tt, X)) => mark(u52(tt, X)) active(u52(tt, X)) => mark(X) active(u61(tt, X, Y, Z)) => mark(u62(tt, X, Y, Z)) active(u62(tt, X, Y, Z)) => mark(u63(tt, X, Y, Z)) active(u63(tt, X, Y, Z)) => mark(u64(splitAt(X, Z), Y)) active(u64(pair(X, Y), Z)) => mark(pair(cons(Z, X), Y)) active(u71(tt, X)) => mark(u72(tt, X)) active(u72(tt, X)) => mark(X) active(u81(tt, X, Y)) => mark(u82(tt, X, Y)) active(u82(tt, X, Y)) => mark(fst(splitAt(X, Y))) active(afterNth(X, Y)) => mark(u11(tt, X, Y)) active(fst(pair(X, Y))) => mark(u21(tt, X)) active(head(cons(X, Y))) => mark(u31(tt, X)) active(natsFrom(X)) => mark(cons(X, natsFrom(s(X)))) active(sel(X, Y)) => mark(u41(tt, X, Y)) active(snd(pair(X, Y))) => mark(u51(tt, Y)) active(splitAt(0, X)) => mark(pair(nil, X)) active(splitAt(s(X), cons(Y, Z))) => mark(u61(tt, X, Y, Z)) active(tail(cons(X, Y))) => mark(u71(tt, Y)) active(take(X, Y)) => mark(u81(tt, X, Y)) mark(u11(X, Y, Z)) => active(u11(mark(X), Y, Z)) mark(tt) => active(tt) mark(u12(X, Y, Z)) => active(u12(mark(X), Y, Z)) mark(snd(X)) => active(snd(mark(X))) mark(splitAt(X, Y)) => active(splitAt(mark(X), mark(Y))) mark(u21(X, Y)) => active(u21(mark(X), Y)) mark(u22(X, Y)) => active(u22(mark(X), Y)) mark(u31(X, Y)) => active(u31(mark(X), Y)) mark(u32(X, Y)) => active(u32(mark(X), Y)) mark(u41(X, Y, Z)) => active(u41(mark(X), Y, Z)) mark(u42(X, Y, Z)) => active(u42(mark(X), Y, Z)) mark(head(X)) => active(head(mark(X))) mark(afterNth(X, Y)) => active(afterNth(mark(X), mark(Y))) mark(u51(X, Y)) => active(u51(mark(X), Y)) mark(u52(X, Y)) => active(u52(mark(X), Y)) mark(u61(X, Y, Z, U)) => active(u61(mark(X), Y, Z, U)) mark(u62(X, Y, Z, U)) => active(u62(mark(X), Y, Z, U)) mark(u63(X, Y, Z, U)) => active(u63(mark(X), Y, Z, U)) mark(u64(X, Y)) => active(u64(mark(X), Y)) mark(pair(X, Y)) => active(pair(mark(X), mark(Y))) mark(cons(X, Y)) => active(cons(mark(X), Y)) mark(u71(X, Y)) => active(u71(mark(X), Y)) mark(u72(X, Y)) => active(u72(mark(X), Y)) mark(u81(X, Y, Z)) => active(u81(mark(X), Y, Z)) mark(u82(X, Y, Z)) => active(u82(mark(X), Y, Z)) mark(fst(X)) => active(fst(mark(X))) mark(natsFrom(X)) => active(natsFrom(mark(X))) mark(s(X)) => active(s(mark(X))) mark(sel(X, Y)) => active(sel(mark(X), mark(Y))) mark(0) => active(0) mark(nil) => active(nil) mark(tail(X)) => active(tail(mark(X))) mark(take(X, Y)) => active(take(mark(X), mark(Y))) u11(mark(X), Y, Z) => 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) u12(mark(X), Y, Z) => u12(X, Y, Z) u12(X, mark(Y), Z) => u12(X, Y, Z) u12(X, Y, mark(Z)) => u12(X, Y, Z) u12(active(X), Y, Z) => u12(X, Y, Z) u12(X, active(Y), Z) => u12(X, Y, Z) u12(X, Y, active(Z)) => u12(X, Y, Z) snd(mark(X)) => snd(X) snd(active(X)) => snd(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) 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) u22(mark(X), Y) => u22(X, Y) u22(X, mark(Y)) => u22(X, Y) u22(active(X), Y) => u22(X, Y) u22(X, active(Y)) => u22(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) u32(mark(X), Y) => u32(X, Y) u32(X, mark(Y)) => u32(X, Y) u32(active(X), Y) => u32(X, Y) u32(X, active(Y)) => u32(X, Y) u41(mark(X), Y, Z) => u41(X, Y, Z) u41(X, mark(Y), Z) => u41(X, Y, Z) u41(X, Y, mark(Z)) => u41(X, Y, Z) u41(active(X), Y, Z) => u41(X, Y, Z) u41(X, active(Y), Z) => u41(X, Y, Z) u41(X, Y, active(Z)) => u41(X, Y, Z) u42(mark(X), Y, Z) => u42(X, Y, Z) u42(X, mark(Y), Z) => u42(X, Y, Z) u42(X, Y, mark(Z)) => u42(X, Y, Z) u42(active(X), Y, Z) => u42(X, Y, Z) u42(X, active(Y), Z) => u42(X, Y, Z) u42(X, Y, active(Z)) => u42(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) u51(mark(X), Y) => u51(X, Y) u51(X, mark(Y)) => u51(X, Y) u51(active(X), Y) => u51(X, Y) u51(X, active(Y)) => u51(X, Y) u52(mark(X), Y) => u52(X, Y) u52(X, mark(Y)) => u52(X, Y) u52(active(X), Y) => u52(X, Y) u52(X, active(Y)) => u52(X, Y) u61(mark(X), Y, Z, U) => u61(X, Y, Z, U) u61(X, mark(Y), Z, U) => u61(X, Y, Z, U) u61(X, Y, mark(Z), U) => u61(X, Y, Z, U) u61(X, Y, Z, mark(U)) => u61(X, Y, Z, U) u61(active(X), Y, Z, U) => u61(X, Y, Z, U) u61(X, active(Y), Z, U) => u61(X, Y, Z, U) u61(X, Y, active(Z), U) => u61(X, Y, Z, U) u61(X, Y, Z, active(U)) => u61(X, Y, Z, U) u62(mark(X), Y, Z, U) => u62(X, Y, Z, U) u62(X, mark(Y), Z, U) => u62(X, Y, Z, U) u62(X, Y, mark(Z), U) => u62(X, Y, Z, U) u62(X, Y, Z, mark(U)) => u62(X, Y, Z, U) u62(active(X), Y, Z, U) => u62(X, Y, Z, U) u62(X, active(Y), Z, U) => u62(X, Y, Z, U) u62(X, Y, active(Z), U) => u62(X, Y, Z, U) u62(X, Y, Z, active(U)) => u62(X, Y, Z, U) u63(mark(X), Y, Z, U) => u63(X, Y, Z, U) u63(X, mark(Y), Z, U) => u63(X, Y, Z, U) u63(X, Y, mark(Z), U) => u63(X, Y, Z, U) u63(X, Y, Z, mark(U)) => u63(X, Y, Z, U) u63(active(X), Y, Z, U) => u63(X, Y, Z, U) u63(X, active(Y), Z, U) => u63(X, Y, Z, U) u63(X, Y, active(Z), U) => u63(X, Y, Z, U) u63(X, Y, Z, active(U)) => u63(X, Y, Z, U) u64(mark(X), Y) => u64(X, Y) u64(X, mark(Y)) => u64(X, Y) u64(active(X), Y) => u64(X, Y) u64(X, active(Y)) => u64(X, Y) pair(mark(X), Y) => pair(X, Y) pair(X, mark(Y)) => pair(X, Y) pair(active(X), Y) => pair(X, Y) pair(X, active(Y)) => pair(X, Y) cons(mark(X), Y) => cons(X, Y) cons(X, mark(Y)) => cons(X, Y) cons(active(X), Y) => cons(X, Y) cons(X, active(Y)) => cons(X, Y) 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) u72(mark(X), Y) => u72(X, Y) u72(X, mark(Y)) => u72(X, Y) u72(active(X), Y) => u72(X, Y) u72(X, active(Y)) => u72(X, Y) u81(mark(X), Y, Z) => u81(X, Y, Z) u81(X, mark(Y), Z) => u81(X, Y, Z) u81(X, Y, mark(Z)) => u81(X, Y, Z) u81(active(X), Y, Z) => u81(X, Y, Z) u81(X, active(Y), Z) => u81(X, Y, Z) u81(X, Y, active(Z)) => u81(X, Y, Z) u82(mark(X), Y, Z) => u82(X, Y, Z) u82(X, mark(Y), Z) => u82(X, Y, Z) u82(X, Y, mark(Z)) => u82(X, Y, Z) u82(active(X), Y, Z) => u82(X, Y, Z) u82(X, active(Y), Z) => u82(X, Y, Z) u82(X, Y, active(Z)) => u82(X, Y, Z) fst(mark(X)) => fst(X) fst(active(X)) => fst(X) natsFrom(mark(X)) => natsFrom(X) natsFrom(active(X)) => natsFrom(X) s(mark(X)) => s(X) s(active(X)) => s(X) sel(mark(X), Y) => sel(X, Y) sel(X, mark(Y)) => sel(X, Y) sel(active(X), Y) => sel(X, Y) sel(X, active(Y)) => sel(X, Y) tail(mark(X)) => tail(X) tail(active(X)) => tail(X) take(mark(X), Y) => take(X, Y) take(X, mark(Y)) => take(X, Y) take(active(X), Y) => take(X, Y) take(X, active(Y)) => take(X, Y) map(/\x.X(x), nil) => nil map(/\x.X(x), cons(Y, Z)) => cons(X(Y), map(/\y.X(y), Z)) app(/\x.X(x), Y) => X(Y) We observe that the rules contain a first-order subset: active(u11(tt, X, Y)) => mark(u12(tt, X, Y)) active(u12(tt, X, Y)) => mark(snd(splitAt(X, Y))) active(u21(tt, X)) => mark(u22(tt, X)) active(u22(tt, X)) => mark(X) active(u31(tt, X)) => mark(u32(tt, X)) active(u32(tt, X)) => mark(X) active(u41(tt, X, Y)) => mark(u42(tt, X, Y)) active(u42(tt, X, Y)) => mark(head(afterNth(X, Y))) active(u51(tt, X)) => mark(u52(tt, X)) active(u52(tt, X)) => mark(X) active(u61(tt, X, Y, Z)) => mark(u62(tt, X, Y, Z)) active(u62(tt, X, Y, Z)) => mark(u63(tt, X, Y, Z)) active(u63(tt, X, Y, Z)) => mark(u64(splitAt(X, Z), Y)) active(u64(pair(X, Y), Z)) => mark(pair(cons(Z, X), Y)) active(u71(tt, X)) => mark(u72(tt, X)) active(u72(tt, X)) => mark(X) active(u81(tt, X, Y)) => mark(u82(tt, X, Y)) active(u82(tt, X, Y)) => mark(fst(splitAt(X, Y))) active(afterNth(X, Y)) => mark(u11(tt, X, Y)) active(fst(pair(X, Y))) => mark(u21(tt, X)) active(head(cons(X, Y))) => mark(u31(tt, X)) active(natsFrom(X)) => mark(cons(X, natsFrom(s(X)))) active(sel(X, Y)) => mark(u41(tt, X, Y)) active(snd(pair(X, Y))) => mark(u51(tt, Y)) active(splitAt(0, X)) => mark(pair(nil, X)) active(splitAt(s(X), cons(Y, Z))) => mark(u61(tt, X, Y, Z)) active(tail(cons(X, Y))) => mark(u71(tt, Y)) active(take(X, Y)) => mark(u81(tt, X, Y)) mark(u11(X, Y, Z)) => active(u11(mark(X), Y, Z)) mark(tt) => active(tt) mark(u12(X, Y, Z)) => active(u12(mark(X), Y, Z)) mark(snd(X)) => active(snd(mark(X))) mark(splitAt(X, Y)) => active(splitAt(mark(X), mark(Y))) mark(u21(X, Y)) => active(u21(mark(X), Y)) mark(u22(X, Y)) => active(u22(mark(X), Y)) mark(u31(X, Y)) => active(u31(mark(X), Y)) mark(u32(X, Y)) => active(u32(mark(X), Y)) mark(u41(X, Y, Z)) => active(u41(mark(X), Y, Z)) mark(u42(X, Y, Z)) => active(u42(mark(X), Y, Z)) mark(head(X)) => active(head(mark(X))) mark(afterNth(X, Y)) => active(afterNth(mark(X), mark(Y))) mark(u51(X, Y)) => active(u51(mark(X), Y)) mark(u52(X, Y)) => active(u52(mark(X), Y)) mark(u61(X, Y, Z, U)) => active(u61(mark(X), Y, Z, U)) mark(u62(X, Y, Z, U)) => active(u62(mark(X), Y, Z, U)) mark(u63(X, Y, Z, U)) => active(u63(mark(X), Y, Z, U)) mark(u64(X, Y)) => active(u64(mark(X), Y)) mark(pair(X, Y)) => active(pair(mark(X), mark(Y))) mark(cons(X, Y)) => active(cons(mark(X), Y)) mark(u71(X, Y)) => active(u71(mark(X), Y)) mark(u72(X, Y)) => active(u72(mark(X), Y)) mark(u81(X, Y, Z)) => active(u81(mark(X), Y, Z)) mark(u82(X, Y, Z)) => active(u82(mark(X), Y, Z)) mark(fst(X)) => active(fst(mark(X))) mark(natsFrom(X)) => active(natsFrom(mark(X))) mark(s(X)) => active(s(mark(X))) mark(sel(X, Y)) => active(sel(mark(X), mark(Y))) mark(0) => active(0) mark(nil) => active(nil) mark(tail(X)) => active(tail(mark(X))) mark(take(X, Y)) => active(take(mark(X), mark(Y))) u11(mark(X), Y, Z) => 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) u12(mark(X), Y, Z) => u12(X, Y, Z) u12(X, mark(Y), Z) => u12(X, Y, Z) u12(X, Y, mark(Z)) => u12(X, Y, Z) u12(active(X), Y, Z) => u12(X, Y, Z) u12(X, active(Y), Z) => u12(X, Y, Z) u12(X, Y, active(Z)) => u12(X, Y, Z) snd(mark(X)) => snd(X) snd(active(X)) => snd(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) 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) u22(mark(X), Y) => u22(X, Y) u22(X, mark(Y)) => u22(X, Y) u22(active(X), Y) => u22(X, Y) u22(X, active(Y)) => u22(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) u32(mark(X), Y) => u32(X, Y) u32(X, mark(Y)) => u32(X, Y) u32(active(X), Y) => u32(X, Y) u32(X, active(Y)) => u32(X, Y) u41(mark(X), Y, Z) => u41(X, Y, Z) u41(X, mark(Y), Z) => u41(X, Y, Z) u41(X, Y, mark(Z)) => u41(X, Y, Z) u41(active(X), Y, Z) => u41(X, Y, Z) u41(X, active(Y), Z) => u41(X, Y, Z) u41(X, Y, active(Z)) => u41(X, Y, Z) u42(mark(X), Y, Z) => u42(X, Y, Z) u42(X, mark(Y), Z) => u42(X, Y, Z) u42(X, Y, mark(Z)) => u42(X, Y, Z) u42(active(X), Y, Z) => u42(X, Y, Z) u42(X, active(Y), Z) => u42(X, Y, Z) u42(X, Y, active(Z)) => u42(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) u51(mark(X), Y) => u51(X, Y) u51(X, mark(Y)) => u51(X, Y) u51(active(X), Y) => u51(X, Y) u51(X, active(Y)) => u51(X, Y) u52(mark(X), Y) => u52(X, Y) u52(X, mark(Y)) => u52(X, Y) u52(active(X), Y) => u52(X, Y) u52(X, active(Y)) => u52(X, Y) u61(mark(X), Y, Z, U) => u61(X, Y, Z, U) u61(X, mark(Y), Z, U) => u61(X, Y, Z, U) u61(X, Y, mark(Z), U) => u61(X, Y, Z, U) u61(X, Y, Z, mark(U)) => u61(X, Y, Z, U) u61(active(X), Y, Z, U) => u61(X, Y, Z, U) u61(X, active(Y), Z, U) => u61(X, Y, Z, U) u61(X, Y, active(Z), U) => u61(X, Y, Z, U) u61(X, Y, Z, active(U)) => u61(X, Y, Z, U) u62(mark(X), Y, Z, U) => u62(X, Y, Z, U) u62(X, mark(Y), Z, U) => u62(X, Y, Z, U) u62(X, Y, mark(Z), U) => u62(X, Y, Z, U) u62(X, Y, Z, mark(U)) => u62(X, Y, Z, U) u62(active(X), Y, Z, U) => u62(X, Y, Z, U) u62(X, active(Y), Z, U) => u62(X, Y, Z, U) u62(X, Y, active(Z), U) => u62(X, Y, Z, U) u62(X, Y, Z, active(U)) => u62(X, Y, Z, U) u63(mark(X), Y, Z, U) => u63(X, Y, Z, U) u63(X, mark(Y), Z, U) => u63(X, Y, Z, U) u63(X, Y, mark(Z), U) => u63(X, Y, Z, U) u63(X, Y, Z, mark(U)) => u63(X, Y, Z, U) u63(active(X), Y, Z, U) => u63(X, Y, Z, U) u63(X, active(Y), Z, U) => u63(X, Y, Z, U) u63(X, Y, active(Z), U) => u63(X, Y, Z, U) u63(X, Y, Z, active(U)) => u63(X, Y, Z, U) u64(mark(X), Y) => u64(X, Y) u64(X, mark(Y)) => u64(X, Y) u64(active(X), Y) => u64(X, Y) u64(X, active(Y)) => u64(X, Y) pair(mark(X), Y) => pair(X, Y) pair(X, mark(Y)) => pair(X, Y) pair(active(X), Y) => pair(X, Y) pair(X, active(Y)) => pair(X, Y) cons(mark(X), Y) => cons(X, Y) cons(X, mark(Y)) => cons(X, Y) cons(active(X), Y) => cons(X, Y) cons(X, active(Y)) => cons(X, Y) 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) u72(mark(X), Y) => u72(X, Y) u72(X, mark(Y)) => u72(X, Y) u72(active(X), Y) => u72(X, Y) u72(X, active(Y)) => u72(X, Y) u81(mark(X), Y, Z) => u81(X, Y, Z) u81(X, mark(Y), Z) => u81(X, Y, Z) u81(X, Y, mark(Z)) => u81(X, Y, Z) u81(active(X), Y, Z) => u81(X, Y, Z) u81(X, active(Y), Z) => u81(X, Y, Z) u81(X, Y, active(Z)) => u81(X, Y, Z) u82(mark(X), Y, Z) => u82(X, Y, Z) u82(X, mark(Y), Z) => u82(X, Y, Z) u82(X, Y, mark(Z)) => u82(X, Y, Z) u82(active(X), Y, Z) => u82(X, Y, Z) u82(X, active(Y), Z) => u82(X, Y, Z) u82(X, Y, active(Z)) => u82(X, Y, Z) fst(mark(X)) => fst(X) fst(active(X)) => fst(X) natsFrom(mark(X)) => natsFrom(X) natsFrom(active(X)) => natsFrom(X) s(mark(X)) => s(X) s(active(X)) => s(X) sel(mark(X), Y) => sel(X, Y) sel(X, mark(Y)) => sel(X, Y) sel(active(X), Y) => sel(X, Y) sel(X, active(Y)) => sel(X, Y) tail(mark(X)) => tail(X) tail(active(X)) => tail(X) take(mark(X), Y) => take(X, Y) take(X, mark(Y)) => take(X, Y) take(active(X), Y) => take(X, Y) take(X, active(Y)) => take(X, Y) Moreover, the system is finitely branching. Thus, by [Kop12, Thm. 7.55], we may omit all first-order dependency pairs from the dependency pair problem (DP(R), R) if this first-order part is Ce-terminating when seen as a many-sorted first-order TRS. According to nattprover, this system is indeed Ce-terminating: || Input TRS: || 1: active(u11(tt(),PeRCenTX,PeRCenTY)) -> mark(u12(tt(),PeRCenTX,PeRCenTY)) || 2: active(u12(tt(),PeRCenTX,PeRCenTY)) -> mark(snd(splitAt(PeRCenTX,PeRCenTY))) || 3: active(u21(tt(),PeRCenTX)) -> mark(u22(tt(),PeRCenTX)) || 4: active(u22(tt(),PeRCenTX)) -> mark(PeRCenTX) || 5: active(u31(tt(),PeRCenTX)) -> mark(u32(tt(),PeRCenTX)) || 6: active(u32(tt(),PeRCenTX)) -> mark(PeRCenTX) || 7: active(u41(tt(),PeRCenTX,PeRCenTY)) -> mark(u42(tt(),PeRCenTX,PeRCenTY)) || 8: active(u42(tt(),PeRCenTX,PeRCenTY)) -> mark(head(afterNth(PeRCenTX,PeRCenTY))) || 9: active(u51(tt(),PeRCenTX)) -> mark(u52(tt(),PeRCenTX)) || 10: active(u52(tt(),PeRCenTX)) -> mark(PeRCenTX) || 11: active(u61(tt(),PeRCenTX,PeRCenTY,PeRCenTZ)) -> mark(u62(tt(),PeRCenTX,PeRCenTY,PeRCenTZ)) || 12: active(u62(tt(),PeRCenTX,PeRCenTY,PeRCenTZ)) -> mark(u63(tt(),PeRCenTX,PeRCenTY,PeRCenTZ)) || 13: active(u63(tt(),PeRCenTX,PeRCenTY,PeRCenTZ)) -> mark(u64(splitAt(PeRCenTX,PeRCenTZ),PeRCenTY)) || 14: active(u64(pair(PeRCenTX,PeRCenTY),PeRCenTZ)) -> mark(pair(cons(PeRCenTZ,PeRCenTX),PeRCenTY)) || 15: active(u71(tt(),PeRCenTX)) -> mark(u72(tt(),PeRCenTX)) || 16: active(u72(tt(),PeRCenTX)) -> mark(PeRCenTX) || 17: active(u81(tt(),PeRCenTX,PeRCenTY)) -> mark(u82(tt(),PeRCenTX,PeRCenTY)) || 18: active(u82(tt(),PeRCenTX,PeRCenTY)) -> mark(fst(splitAt(PeRCenTX,PeRCenTY))) || 19: active(afterNth(PeRCenTX,PeRCenTY)) -> mark(u11(tt(),PeRCenTX,PeRCenTY)) || 20: active(fst(pair(PeRCenTX,PeRCenTY))) -> mark(u21(tt(),PeRCenTX)) || 21: active(head(cons(PeRCenTX,PeRCenTY))) -> mark(u31(tt(),PeRCenTX)) || 22: active(natsFrom(PeRCenTX)) -> mark(cons(PeRCenTX,natsFrom(s(PeRCenTX)))) || 23: active(sel(PeRCenTX,PeRCenTY)) -> mark(u41(tt(),PeRCenTX,PeRCenTY)) || 24: active(snd(pair(PeRCenTX,PeRCenTY))) -> mark(u51(tt(),PeRCenTY)) || 25: active(splitAt(0(),PeRCenTX)) -> mark(pair(nil(),PeRCenTX)) || 26: active(splitAt(s(PeRCenTX),cons(PeRCenTY,PeRCenTZ))) -> mark(u61(tt(),PeRCenTX,PeRCenTY,PeRCenTZ)) || 27: active(tail(cons(PeRCenTX,PeRCenTY))) -> mark(u71(tt(),PeRCenTY)) || 28: active(take(PeRCenTX,PeRCenTY)) -> mark(u81(tt(),PeRCenTX,PeRCenTY)) || 29: mark(u11(PeRCenTX,PeRCenTY,PeRCenTZ)) -> active(u11(mark(PeRCenTX),PeRCenTY,PeRCenTZ)) || 30: mark(tt()) -> active(tt()) || 31: mark(u12(PeRCenTX,PeRCenTY,PeRCenTZ)) -> active(u12(mark(PeRCenTX),PeRCenTY,PeRCenTZ)) || 32: mark(snd(PeRCenTX)) -> active(snd(mark(PeRCenTX))) || 33: mark(splitAt(PeRCenTX,PeRCenTY)) -> active(splitAt(mark(PeRCenTX),mark(PeRCenTY))) || 34: mark(u21(PeRCenTX,PeRCenTY)) -> active(u21(mark(PeRCenTX),PeRCenTY)) || 35: mark(u22(PeRCenTX,PeRCenTY)) -> active(u22(mark(PeRCenTX),PeRCenTY)) || 36: mark(u31(PeRCenTX,PeRCenTY)) -> active(u31(mark(PeRCenTX),PeRCenTY)) || 37: mark(u32(PeRCenTX,PeRCenTY)) -> active(u32(mark(PeRCenTX),PeRCenTY)) || 38: mark(u41(PeRCenTX,PeRCenTY,PeRCenTZ)) -> active(u41(mark(PeRCenTX),PeRCenTY,PeRCenTZ)) || 39: mark(u42(PeRCenTX,PeRCenTY,PeRCenTZ)) -> active(u42(mark(PeRCenTX),PeRCenTY,PeRCenTZ)) || 40: mark(head(PeRCenTX)) -> active(head(mark(PeRCenTX))) || 41: mark(afterNth(PeRCenTX,PeRCenTY)) -> active(afterNth(mark(PeRCenTX),mark(PeRCenTY))) || 42: mark(u51(PeRCenTX,PeRCenTY)) -> active(u51(mark(PeRCenTX),PeRCenTY)) || 43: mark(u52(PeRCenTX,PeRCenTY)) -> active(u52(mark(PeRCenTX),PeRCenTY)) || 44: mark(u61(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> active(u61(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU)) || 45: mark(u62(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> active(u62(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU)) || 46: mark(u63(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> active(u63(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU)) || 47: mark(u64(PeRCenTX,PeRCenTY)) -> active(u64(mark(PeRCenTX),PeRCenTY)) || 48: mark(pair(PeRCenTX,PeRCenTY)) -> active(pair(mark(PeRCenTX),mark(PeRCenTY))) || 49: mark(cons(PeRCenTX,PeRCenTY)) -> active(cons(mark(PeRCenTX),PeRCenTY)) || 50: mark(u71(PeRCenTX,PeRCenTY)) -> active(u71(mark(PeRCenTX),PeRCenTY)) || 51: mark(u72(PeRCenTX,PeRCenTY)) -> active(u72(mark(PeRCenTX),PeRCenTY)) || 52: mark(u81(PeRCenTX,PeRCenTY,PeRCenTZ)) -> active(u81(mark(PeRCenTX),PeRCenTY,PeRCenTZ)) || 53: mark(u82(PeRCenTX,PeRCenTY,PeRCenTZ)) -> active(u82(mark(PeRCenTX),PeRCenTY,PeRCenTZ)) || 54: mark(fst(PeRCenTX)) -> active(fst(mark(PeRCenTX))) || 55: mark(natsFrom(PeRCenTX)) -> active(natsFrom(mark(PeRCenTX))) || 56: mark(s(PeRCenTX)) -> active(s(mark(PeRCenTX))) || 57: mark(sel(PeRCenTX,PeRCenTY)) -> active(sel(mark(PeRCenTX),mark(PeRCenTY))) || 58: mark(0()) -> active(0()) || 59: mark(nil()) -> active(nil()) || 60: mark(tail(PeRCenTX)) -> active(tail(mark(PeRCenTX))) || 61: mark(take(PeRCenTX,PeRCenTY)) -> active(take(mark(PeRCenTX),mark(PeRCenTY))) || 62: u11(mark(PeRCenTX),PeRCenTY,PeRCenTZ) -> u11(PeRCenTX,PeRCenTY,PeRCenTZ) || 63: u11(PeRCenTX,mark(PeRCenTY),PeRCenTZ) -> u11(PeRCenTX,PeRCenTY,PeRCenTZ) || 64: u11(PeRCenTX,PeRCenTY,mark(PeRCenTZ)) -> u11(PeRCenTX,PeRCenTY,PeRCenTZ) || 65: u11(active(PeRCenTX),PeRCenTY,PeRCenTZ) -> u11(PeRCenTX,PeRCenTY,PeRCenTZ) || 66: u11(PeRCenTX,active(PeRCenTY),PeRCenTZ) -> u11(PeRCenTX,PeRCenTY,PeRCenTZ) || 67: u11(PeRCenTX,PeRCenTY,active(PeRCenTZ)) -> u11(PeRCenTX,PeRCenTY,PeRCenTZ) || 68: u12(mark(PeRCenTX),PeRCenTY,PeRCenTZ) -> u12(PeRCenTX,PeRCenTY,PeRCenTZ) || 69: u12(PeRCenTX,mark(PeRCenTY),PeRCenTZ) -> u12(PeRCenTX,PeRCenTY,PeRCenTZ) || 70: u12(PeRCenTX,PeRCenTY,mark(PeRCenTZ)) -> u12(PeRCenTX,PeRCenTY,PeRCenTZ) || 71: u12(active(PeRCenTX),PeRCenTY,PeRCenTZ) -> u12(PeRCenTX,PeRCenTY,PeRCenTZ) || 72: u12(PeRCenTX,active(PeRCenTY),PeRCenTZ) -> u12(PeRCenTX,PeRCenTY,PeRCenTZ) || 73: u12(PeRCenTX,PeRCenTY,active(PeRCenTZ)) -> u12(PeRCenTX,PeRCenTY,PeRCenTZ) || 74: snd(mark(PeRCenTX)) -> snd(PeRCenTX) || 75: snd(active(PeRCenTX)) -> snd(PeRCenTX) || 76: splitAt(mark(PeRCenTX),PeRCenTY) -> splitAt(PeRCenTX,PeRCenTY) || 77: splitAt(PeRCenTX,mark(PeRCenTY)) -> splitAt(PeRCenTX,PeRCenTY) || 78: splitAt(active(PeRCenTX),PeRCenTY) -> splitAt(PeRCenTX,PeRCenTY) || 79: splitAt(PeRCenTX,active(PeRCenTY)) -> splitAt(PeRCenTX,PeRCenTY) || 80: u21(mark(PeRCenTX),PeRCenTY) -> u21(PeRCenTX,PeRCenTY) || 81: u21(PeRCenTX,mark(PeRCenTY)) -> u21(PeRCenTX,PeRCenTY) || 82: u21(active(PeRCenTX),PeRCenTY) -> u21(PeRCenTX,PeRCenTY) || 83: u21(PeRCenTX,active(PeRCenTY)) -> u21(PeRCenTX,PeRCenTY) || 84: u22(mark(PeRCenTX),PeRCenTY) -> u22(PeRCenTX,PeRCenTY) || 85: u22(PeRCenTX,mark(PeRCenTY)) -> u22(PeRCenTX,PeRCenTY) || 86: u22(active(PeRCenTX),PeRCenTY) -> u22(PeRCenTX,PeRCenTY) || 87: u22(PeRCenTX,active(PeRCenTY)) -> u22(PeRCenTX,PeRCenTY) || 88: u31(mark(PeRCenTX),PeRCenTY) -> u31(PeRCenTX,PeRCenTY) || 89: u31(PeRCenTX,mark(PeRCenTY)) -> u31(PeRCenTX,PeRCenTY) || 90: u31(active(PeRCenTX),PeRCenTY) -> u31(PeRCenTX,PeRCenTY) || 91: u31(PeRCenTX,active(PeRCenTY)) -> u31(PeRCenTX,PeRCenTY) || 92: u32(mark(PeRCenTX),PeRCenTY) -> u32(PeRCenTX,PeRCenTY) || 93: u32(PeRCenTX,mark(PeRCenTY)) -> u32(PeRCenTX,PeRCenTY) || 94: u32(active(PeRCenTX),PeRCenTY) -> u32(PeRCenTX,PeRCenTY) || 95: u32(PeRCenTX,active(PeRCenTY)) -> u32(PeRCenTX,PeRCenTY) || 96: u41(mark(PeRCenTX),PeRCenTY,PeRCenTZ) -> u41(PeRCenTX,PeRCenTY,PeRCenTZ) || 97: u41(PeRCenTX,mark(PeRCenTY),PeRCenTZ) -> u41(PeRCenTX,PeRCenTY,PeRCenTZ) || 98: u41(PeRCenTX,PeRCenTY,mark(PeRCenTZ)) -> u41(PeRCenTX,PeRCenTY,PeRCenTZ) || 99: u41(active(PeRCenTX),PeRCenTY,PeRCenTZ) -> u41(PeRCenTX,PeRCenTY,PeRCenTZ) || 100: u41(PeRCenTX,active(PeRCenTY),PeRCenTZ) -> u41(PeRCenTX,PeRCenTY,PeRCenTZ) || 101: u41(PeRCenTX,PeRCenTY,active(PeRCenTZ)) -> u41(PeRCenTX,PeRCenTY,PeRCenTZ) || 102: u42(mark(PeRCenTX),PeRCenTY,PeRCenTZ) -> u42(PeRCenTX,PeRCenTY,PeRCenTZ) || 103: u42(PeRCenTX,mark(PeRCenTY),PeRCenTZ) -> u42(PeRCenTX,PeRCenTY,PeRCenTZ) || 104: u42(PeRCenTX,PeRCenTY,mark(PeRCenTZ)) -> u42(PeRCenTX,PeRCenTY,PeRCenTZ) || 105: u42(active(PeRCenTX),PeRCenTY,PeRCenTZ) -> u42(PeRCenTX,PeRCenTY,PeRCenTZ) || 106: u42(PeRCenTX,active(PeRCenTY),PeRCenTZ) -> u42(PeRCenTX,PeRCenTY,PeRCenTZ) || 107: u42(PeRCenTX,PeRCenTY,active(PeRCenTZ)) -> u42(PeRCenTX,PeRCenTY,PeRCenTZ) || 108: head(mark(PeRCenTX)) -> head(PeRCenTX) || 109: head(active(PeRCenTX)) -> head(PeRCenTX) || 110: afterNth(mark(PeRCenTX),PeRCenTY) -> afterNth(PeRCenTX,PeRCenTY) || 111: afterNth(PeRCenTX,mark(PeRCenTY)) -> afterNth(PeRCenTX,PeRCenTY) || 112: afterNth(active(PeRCenTX),PeRCenTY) -> afterNth(PeRCenTX,PeRCenTY) || 113: afterNth(PeRCenTX,active(PeRCenTY)) -> afterNth(PeRCenTX,PeRCenTY) || 114: u51(mark(PeRCenTX),PeRCenTY) -> u51(PeRCenTX,PeRCenTY) || 115: u51(PeRCenTX,mark(PeRCenTY)) -> u51(PeRCenTX,PeRCenTY) || 116: u51(active(PeRCenTX),PeRCenTY) -> u51(PeRCenTX,PeRCenTY) || 117: u51(PeRCenTX,active(PeRCenTY)) -> u51(PeRCenTX,PeRCenTY) || 118: u52(mark(PeRCenTX),PeRCenTY) -> u52(PeRCenTX,PeRCenTY) || 119: u52(PeRCenTX,mark(PeRCenTY)) -> u52(PeRCenTX,PeRCenTY) || 120: u52(active(PeRCenTX),PeRCenTY) -> u52(PeRCenTX,PeRCenTY) || 121: u52(PeRCenTX,active(PeRCenTY)) -> u52(PeRCenTX,PeRCenTY) || 122: u61(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU) -> u61(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || 123: u61(PeRCenTX,mark(PeRCenTY),PeRCenTZ,PeRCenTU) -> u61(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || 124: u61(PeRCenTX,PeRCenTY,mark(PeRCenTZ),PeRCenTU) -> u61(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || 125: u61(PeRCenTX,PeRCenTY,PeRCenTZ,mark(PeRCenTU)) -> u61(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || 126: u61(active(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU) -> u61(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || 127: u61(PeRCenTX,active(PeRCenTY),PeRCenTZ,PeRCenTU) -> u61(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || 128: u61(PeRCenTX,PeRCenTY,active(PeRCenTZ),PeRCenTU) -> u61(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || 129: u61(PeRCenTX,PeRCenTY,PeRCenTZ,active(PeRCenTU)) -> u61(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || 130: u62(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU) -> u62(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || 131: u62(PeRCenTX,mark(PeRCenTY),PeRCenTZ,PeRCenTU) -> u62(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || 132: u62(PeRCenTX,PeRCenTY,mark(PeRCenTZ),PeRCenTU) -> u62(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || 133: u62(PeRCenTX,PeRCenTY,PeRCenTZ,mark(PeRCenTU)) -> u62(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || 134: u62(active(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU) -> u62(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || 135: u62(PeRCenTX,active(PeRCenTY),PeRCenTZ,PeRCenTU) -> u62(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || 136: u62(PeRCenTX,PeRCenTY,active(PeRCenTZ),PeRCenTU) -> u62(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || 137: u62(PeRCenTX,PeRCenTY,PeRCenTZ,active(PeRCenTU)) -> u62(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || 138: u63(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU) -> u63(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || 139: u63(PeRCenTX,mark(PeRCenTY),PeRCenTZ,PeRCenTU) -> u63(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || 140: u63(PeRCenTX,PeRCenTY,mark(PeRCenTZ),PeRCenTU) -> u63(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || 141: u63(PeRCenTX,PeRCenTY,PeRCenTZ,mark(PeRCenTU)) -> u63(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || 142: u63(active(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU) -> u63(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || 143: u63(PeRCenTX,active(PeRCenTY),PeRCenTZ,PeRCenTU) -> u63(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || 144: u63(PeRCenTX,PeRCenTY,active(PeRCenTZ),PeRCenTU) -> u63(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || 145: u63(PeRCenTX,PeRCenTY,PeRCenTZ,active(PeRCenTU)) -> u63(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || 146: u64(mark(PeRCenTX),PeRCenTY) -> u64(PeRCenTX,PeRCenTY) || 147: u64(PeRCenTX,mark(PeRCenTY)) -> u64(PeRCenTX,PeRCenTY) || 148: u64(active(PeRCenTX),PeRCenTY) -> u64(PeRCenTX,PeRCenTY) || 149: u64(PeRCenTX,active(PeRCenTY)) -> u64(PeRCenTX,PeRCenTY) || 150: pair(mark(PeRCenTX),PeRCenTY) -> pair(PeRCenTX,PeRCenTY) || 151: pair(PeRCenTX,mark(PeRCenTY)) -> pair(PeRCenTX,PeRCenTY) || 152: pair(active(PeRCenTX),PeRCenTY) -> pair(PeRCenTX,PeRCenTY) || 153: pair(PeRCenTX,active(PeRCenTY)) -> pair(PeRCenTX,PeRCenTY) || 154: cons(mark(PeRCenTX),PeRCenTY) -> cons(PeRCenTX,PeRCenTY) || 155: cons(PeRCenTX,mark(PeRCenTY)) -> cons(PeRCenTX,PeRCenTY) || 156: cons(active(PeRCenTX),PeRCenTY) -> cons(PeRCenTX,PeRCenTY) || 157: cons(PeRCenTX,active(PeRCenTY)) -> cons(PeRCenTX,PeRCenTY) || 158: u71(mark(PeRCenTX),PeRCenTY) -> u71(PeRCenTX,PeRCenTY) || 159: u71(PeRCenTX,mark(PeRCenTY)) -> u71(PeRCenTX,PeRCenTY) || 160: u71(active(PeRCenTX),PeRCenTY) -> u71(PeRCenTX,PeRCenTY) || 161: u71(PeRCenTX,active(PeRCenTY)) -> u71(PeRCenTX,PeRCenTY) || 162: u72(mark(PeRCenTX),PeRCenTY) -> u72(PeRCenTX,PeRCenTY) || 163: u72(PeRCenTX,mark(PeRCenTY)) -> u72(PeRCenTX,PeRCenTY) || 164: u72(active(PeRCenTX),PeRCenTY) -> u72(PeRCenTX,PeRCenTY) || 165: u72(PeRCenTX,active(PeRCenTY)) -> u72(PeRCenTX,PeRCenTY) || 166: u81(mark(PeRCenTX),PeRCenTY,PeRCenTZ) -> u81(PeRCenTX,PeRCenTY,PeRCenTZ) || 167: u81(PeRCenTX,mark(PeRCenTY),PeRCenTZ) -> u81(PeRCenTX,PeRCenTY,PeRCenTZ) || 168: u81(PeRCenTX,PeRCenTY,mark(PeRCenTZ)) -> u81(PeRCenTX,PeRCenTY,PeRCenTZ) || 169: u81(active(PeRCenTX),PeRCenTY,PeRCenTZ) -> u81(PeRCenTX,PeRCenTY,PeRCenTZ) || 170: u81(PeRCenTX,active(PeRCenTY),PeRCenTZ) -> u81(PeRCenTX,PeRCenTY,PeRCenTZ) || 171: u81(PeRCenTX,PeRCenTY,active(PeRCenTZ)) -> u81(PeRCenTX,PeRCenTY,PeRCenTZ) || 172: u82(mark(PeRCenTX),PeRCenTY,PeRCenTZ) -> u82(PeRCenTX,PeRCenTY,PeRCenTZ) || 173: u82(PeRCenTX,mark(PeRCenTY),PeRCenTZ) -> u82(PeRCenTX,PeRCenTY,PeRCenTZ) || 174: u82(PeRCenTX,PeRCenTY,mark(PeRCenTZ)) -> u82(PeRCenTX,PeRCenTY,PeRCenTZ) || 175: u82(active(PeRCenTX),PeRCenTY,PeRCenTZ) -> u82(PeRCenTX,PeRCenTY,PeRCenTZ) || 176: u82(PeRCenTX,active(PeRCenTY),PeRCenTZ) -> u82(PeRCenTX,PeRCenTY,PeRCenTZ) || 177: u82(PeRCenTX,PeRCenTY,active(PeRCenTZ)) -> u82(PeRCenTX,PeRCenTY,PeRCenTZ) || 178: fst(mark(PeRCenTX)) -> fst(PeRCenTX) || 179: fst(active(PeRCenTX)) -> fst(PeRCenTX) || 180: natsFrom(mark(PeRCenTX)) -> natsFrom(PeRCenTX) || 181: natsFrom(active(PeRCenTX)) -> natsFrom(PeRCenTX) || 182: s(mark(PeRCenTX)) -> s(PeRCenTX) || 183: s(active(PeRCenTX)) -> s(PeRCenTX) || 184: sel(mark(PeRCenTX),PeRCenTY) -> sel(PeRCenTX,PeRCenTY) || 185: sel(PeRCenTX,mark(PeRCenTY)) -> sel(PeRCenTX,PeRCenTY) || 186: sel(active(PeRCenTX),PeRCenTY) -> sel(PeRCenTX,PeRCenTY) || 187: sel(PeRCenTX,active(PeRCenTY)) -> sel(PeRCenTX,PeRCenTY) || 188: tail(mark(PeRCenTX)) -> tail(PeRCenTX) || 189: tail(active(PeRCenTX)) -> tail(PeRCenTX) || 190: take(mark(PeRCenTX),PeRCenTY) -> take(PeRCenTX,PeRCenTY) || 191: take(PeRCenTX,mark(PeRCenTY)) -> take(PeRCenTX,PeRCenTY) || 192: take(active(PeRCenTX),PeRCenTY) -> take(PeRCenTX,PeRCenTY) || 193: take(PeRCenTX,active(PeRCenTY)) -> take(PeRCenTX,PeRCenTY) || 194: TIlDePAIR(PeRCenTX,PeRCenTY) -> PeRCenTX || 195: TIlDePAIR(PeRCenTX,PeRCenTY) -> PeRCenTY || Number of strict rules: 195 || Direct POLO(bPol) ... failed. || Uncurrying ... failed. || Dependency Pairs: || #1: #active(u12(tt(),PeRCenTX,PeRCenTY)) -> #mark(snd(splitAt(PeRCenTX,PeRCenTY))) || #2: #active(u12(tt(),PeRCenTX,PeRCenTY)) -> #snd(splitAt(PeRCenTX,PeRCenTY)) || #3: #active(u12(tt(),PeRCenTX,PeRCenTY)) -> #splitAt(PeRCenTX,PeRCenTY) || #4: #u22(active(PeRCenTX),PeRCenTY) -> #u22(PeRCenTX,PeRCenTY) || #5: #mark(u52(PeRCenTX,PeRCenTY)) -> #active(u52(mark(PeRCenTX),PeRCenTY)) || #6: #mark(u52(PeRCenTX,PeRCenTY)) -> #u52(mark(PeRCenTX),PeRCenTY) || #7: #mark(u52(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #8: #mark(u11(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #active(u11(mark(PeRCenTX),PeRCenTY,PeRCenTZ)) || #9: #mark(u11(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #u11(mark(PeRCenTX),PeRCenTY,PeRCenTZ) || #10: #mark(u11(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #mark(PeRCenTX) || #11: #mark(u22(PeRCenTX,PeRCenTY)) -> #active(u22(mark(PeRCenTX),PeRCenTY)) || #12: #mark(u22(PeRCenTX,PeRCenTY)) -> #u22(mark(PeRCenTX),PeRCenTY) || #13: #mark(u22(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #14: #u21(PeRCenTX,active(PeRCenTY)) -> #u21(PeRCenTX,PeRCenTY) || #15: #u11(PeRCenTX,active(PeRCenTY),PeRCenTZ) -> #u11(PeRCenTX,PeRCenTY,PeRCenTZ) || #16: #u82(PeRCenTX,PeRCenTY,active(PeRCenTZ)) -> #u82(PeRCenTX,PeRCenTY,PeRCenTZ) || #17: #mark(u63(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> #active(u63(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU)) || #18: #mark(u63(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> #u63(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU) || #19: #mark(u63(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> #mark(PeRCenTX) || #20: #mark(u51(PeRCenTX,PeRCenTY)) -> #active(u51(mark(PeRCenTX),PeRCenTY)) || #21: #mark(u51(PeRCenTX,PeRCenTY)) -> #u51(mark(PeRCenTX),PeRCenTY) || #22: #mark(u51(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #23: #u51(PeRCenTX,mark(PeRCenTY)) -> #u51(PeRCenTX,PeRCenTY) || #24: #u64(PeRCenTX,active(PeRCenTY)) -> #u64(PeRCenTX,PeRCenTY) || #25: #u32(PeRCenTX,active(PeRCenTY)) -> #u32(PeRCenTX,PeRCenTY) || #26: #mark(afterNth(PeRCenTX,PeRCenTY)) -> #active(afterNth(mark(PeRCenTX),mark(PeRCenTY))) || #27: #mark(afterNth(PeRCenTX,PeRCenTY)) -> #afterNth(mark(PeRCenTX),mark(PeRCenTY)) || #28: #mark(afterNth(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #29: #mark(afterNth(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY) || #30: #mark(u32(PeRCenTX,PeRCenTY)) -> #active(u32(mark(PeRCenTX),PeRCenTY)) || #31: #mark(u32(PeRCenTX,PeRCenTY)) -> #u32(mark(PeRCenTX),PeRCenTY) || #32: #mark(u32(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #33: #u51(mark(PeRCenTX),PeRCenTY) -> #u51(PeRCenTX,PeRCenTY) || #34: #u41(active(PeRCenTX),PeRCenTY,PeRCenTZ) -> #u41(PeRCenTX,PeRCenTY,PeRCenTZ) || #35: #u72(PeRCenTX,mark(PeRCenTY)) -> #u72(PeRCenTX,PeRCenTY) || #36: #u41(PeRCenTX,mark(PeRCenTY),PeRCenTZ) -> #u41(PeRCenTX,PeRCenTY,PeRCenTZ) || #37: #u31(PeRCenTX,active(PeRCenTY)) -> #u31(PeRCenTX,PeRCenTY) || #38: #u12(PeRCenTX,PeRCenTY,active(PeRCenTZ)) -> #u12(PeRCenTX,PeRCenTY,PeRCenTZ) || #39: #mark(u64(PeRCenTX,PeRCenTY)) -> #active(u64(mark(PeRCenTX),PeRCenTY)) || #40: #mark(u64(PeRCenTX,PeRCenTY)) -> #u64(mark(PeRCenTX),PeRCenTY) || #41: #mark(u64(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #42: #take(PeRCenTX,mark(PeRCenTY)) -> #take(PeRCenTX,PeRCenTY) || #43: #mark(u82(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #active(u82(mark(PeRCenTX),PeRCenTY,PeRCenTZ)) || #44: #mark(u82(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #u82(mark(PeRCenTX),PeRCenTY,PeRCenTZ) || #45: #mark(u82(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #mark(PeRCenTX) || #46: #u82(PeRCenTX,mark(PeRCenTY),PeRCenTZ) -> #u82(PeRCenTX,PeRCenTY,PeRCenTZ) || #47: #u12(active(PeRCenTX),PeRCenTY,PeRCenTZ) -> #u12(PeRCenTX,PeRCenTY,PeRCenTZ) || #48: #u64(PeRCenTX,mark(PeRCenTY)) -> #u64(PeRCenTX,PeRCenTY) || #49: #u63(PeRCenTX,mark(PeRCenTY),PeRCenTZ,PeRCenTU) -> #u63(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || #50: #mark(pair(PeRCenTX,PeRCenTY)) -> #active(pair(mark(PeRCenTX),mark(PeRCenTY))) || #51: #mark(pair(PeRCenTX,PeRCenTY)) -> #pair(mark(PeRCenTX),mark(PeRCenTY)) || #52: #mark(pair(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #53: #mark(pair(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY) || #54: #u61(PeRCenTX,mark(PeRCenTY),PeRCenTZ,PeRCenTU) -> #u61(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || #55: #snd(active(PeRCenTX)) -> #snd(PeRCenTX) || #56: #fst(mark(PeRCenTX)) -> #fst(PeRCenTX) || #57: #afterNth(active(PeRCenTX),PeRCenTY) -> #afterNth(PeRCenTX,PeRCenTY) || #58: #snd(mark(PeRCenTX)) -> #snd(PeRCenTX) || #59: #u81(PeRCenTX,active(PeRCenTY),PeRCenTZ) -> #u81(PeRCenTX,PeRCenTY,PeRCenTZ) || #60: #mark(0()) -> #active(0()) || #61: #u63(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU) -> #u63(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || #62: #afterNth(PeRCenTX,active(PeRCenTY)) -> #afterNth(PeRCenTX,PeRCenTY) || #63: #u71(mark(PeRCenTX),PeRCenTY) -> #u71(PeRCenTX,PeRCenTY) || #64: #mark(take(PeRCenTX,PeRCenTY)) -> #active(take(mark(PeRCenTX),mark(PeRCenTY))) || #65: #mark(take(PeRCenTX,PeRCenTY)) -> #take(mark(PeRCenTX),mark(PeRCenTY)) || #66: #mark(take(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #67: #mark(take(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY) || #68: #mark(u41(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #active(u41(mark(PeRCenTX),PeRCenTY,PeRCenTZ)) || #69: #mark(u41(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #u41(mark(PeRCenTX),PeRCenTY,PeRCenTZ) || #70: #mark(u41(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #mark(PeRCenTX) || #71: #pair(PeRCenTX,mark(PeRCenTY)) -> #pair(PeRCenTX,PeRCenTY) || #72: #cons(mark(PeRCenTX),PeRCenTY) -> #cons(PeRCenTX,PeRCenTY) || #73: #u51(active(PeRCenTX),PeRCenTY) -> #u51(PeRCenTX,PeRCenTY) || #74: #cons(PeRCenTX,mark(PeRCenTY)) -> #cons(PeRCenTX,PeRCenTY) || #75: #active(u32(tt(),PeRCenTX)) -> #mark(PeRCenTX) || #76: #u72(PeRCenTX,active(PeRCenTY)) -> #u72(PeRCenTX,PeRCenTY) || #77: #mark(nil()) -> #active(nil()) || #78: #take(PeRCenTX,active(PeRCenTY)) -> #take(PeRCenTX,PeRCenTY) || #79: #afterNth(mark(PeRCenTX),PeRCenTY) -> #afterNth(PeRCenTX,PeRCenTY) || #80: #u62(PeRCenTX,PeRCenTY,mark(PeRCenTZ),PeRCenTU) -> #u62(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || #81: #mark(natsFrom(PeRCenTX)) -> #active(natsFrom(mark(PeRCenTX))) || #82: #mark(natsFrom(PeRCenTX)) -> #natsFrom(mark(PeRCenTX)) || #83: #mark(natsFrom(PeRCenTX)) -> #mark(PeRCenTX) || #84: #u11(PeRCenTX,PeRCenTY,active(PeRCenTZ)) -> #u11(PeRCenTX,PeRCenTY,PeRCenTZ) || #85: #mark(head(PeRCenTX)) -> #active(head(mark(PeRCenTX))) || #86: #mark(head(PeRCenTX)) -> #head(mark(PeRCenTX)) || #87: #mark(head(PeRCenTX)) -> #mark(PeRCenTX) || #88: #u31(active(PeRCenTX),PeRCenTY) -> #u31(PeRCenTX,PeRCenTY) || #89: #u64(mark(PeRCenTX),PeRCenTY) -> #u64(PeRCenTX,PeRCenTY) || #90: #u42(PeRCenTX,PeRCenTY,active(PeRCenTZ)) -> #u42(PeRCenTX,PeRCenTY,PeRCenTZ) || #91: #mark(u72(PeRCenTX,PeRCenTY)) -> #active(u72(mark(PeRCenTX),PeRCenTY)) || #92: #mark(u72(PeRCenTX,PeRCenTY)) -> #u72(mark(PeRCenTX),PeRCenTY) || #93: #mark(u72(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #94: #active(u63(tt(),PeRCenTX,PeRCenTY,PeRCenTZ)) -> #mark(u64(splitAt(PeRCenTX,PeRCenTZ),PeRCenTY)) || #95: #active(u63(tt(),PeRCenTX,PeRCenTY,PeRCenTZ)) -> #u64(splitAt(PeRCenTX,PeRCenTZ),PeRCenTY) || #96: #active(u63(tt(),PeRCenTX,PeRCenTY,PeRCenTZ)) -> #splitAt(PeRCenTX,PeRCenTZ) || #97: #active(u51(tt(),PeRCenTX)) -> #mark(u52(tt(),PeRCenTX)) || #98: #active(u51(tt(),PeRCenTX)) -> #u52(tt(),PeRCenTX) || #99: #active(u61(tt(),PeRCenTX,PeRCenTY,PeRCenTZ)) -> #mark(u62(tt(),PeRCenTX,PeRCenTY,PeRCenTZ)) || #100: #active(u61(tt(),PeRCenTX,PeRCenTY,PeRCenTZ)) -> #u62(tt(),PeRCenTX,PeRCenTY,PeRCenTZ) || #101: #u41(PeRCenTX,PeRCenTY,mark(PeRCenTZ)) -> #u41(PeRCenTX,PeRCenTY,PeRCenTZ) || #102: #cons(active(PeRCenTX),PeRCenTY) -> #cons(PeRCenTX,PeRCenTY) || #103: #mark(sel(PeRCenTX,PeRCenTY)) -> #active(sel(mark(PeRCenTX),mark(PeRCenTY))) || #104: #mark(sel(PeRCenTX,PeRCenTY)) -> #sel(mark(PeRCenTX),mark(PeRCenTY)) || #105: #mark(sel(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #106: #mark(sel(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY) || #107: #splitAt(mark(PeRCenTX),PeRCenTY) -> #splitAt(PeRCenTX,PeRCenTY) || #108: #u81(PeRCenTX,mark(PeRCenTY),PeRCenTZ) -> #u81(PeRCenTX,PeRCenTY,PeRCenTZ) || #109: #take(mark(PeRCenTX),PeRCenTY) -> #take(PeRCenTX,PeRCenTY) || #110: #head(active(PeRCenTX)) -> #head(PeRCenTX) || #111: #u32(active(PeRCenTX),PeRCenTY) -> #u32(PeRCenTX,PeRCenTY) || #112: #active(snd(pair(PeRCenTX,PeRCenTY))) -> #mark(u51(tt(),PeRCenTY)) || #113: #active(snd(pair(PeRCenTX,PeRCenTY))) -> #u51(tt(),PeRCenTY) || #114: #u62(active(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU) -> #u62(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || #115: #u12(PeRCenTX,PeRCenTY,mark(PeRCenTZ)) -> #u12(PeRCenTX,PeRCenTY,PeRCenTZ) || #116: #active(sel(PeRCenTX,PeRCenTY)) -> #mark(u41(tt(),PeRCenTX,PeRCenTY)) || #117: #active(sel(PeRCenTX,PeRCenTY)) -> #u41(tt(),PeRCenTX,PeRCenTY) || #118: #u61(PeRCenTX,PeRCenTY,active(PeRCenTZ),PeRCenTU) -> #u61(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || #119: #u21(PeRCenTX,mark(PeRCenTY)) -> #u21(PeRCenTX,PeRCenTY) || #120: #u52(mark(PeRCenTX),PeRCenTY) -> #u52(PeRCenTX,PeRCenTY) || #121: #splitAt(active(PeRCenTX),PeRCenTY) -> #splitAt(PeRCenTX,PeRCenTY) || #122: #mark(u62(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> #active(u62(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU)) || #123: #mark(u62(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> #u62(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU) || #124: #mark(u62(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> #mark(PeRCenTX) || #125: #u41(mark(PeRCenTX),PeRCenTY,PeRCenTZ) -> #u41(PeRCenTX,PeRCenTY,PeRCenTZ) || #126: #u12(PeRCenTX,mark(PeRCenTY),PeRCenTZ) -> #u12(PeRCenTX,PeRCenTY,PeRCenTZ) || #127: #u41(PeRCenTX,PeRCenTY,active(PeRCenTZ)) -> #u41(PeRCenTX,PeRCenTY,PeRCenTZ) || #128: #active(u62(tt(),PeRCenTX,PeRCenTY,PeRCenTZ)) -> #mark(u63(tt(),PeRCenTX,PeRCenTY,PeRCenTZ)) || #129: #active(u62(tt(),PeRCenTX,PeRCenTY,PeRCenTZ)) -> #u63(tt(),PeRCenTX,PeRCenTY,PeRCenTZ) || #130: #mark(u12(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #active(u12(mark(PeRCenTX),PeRCenTY,PeRCenTZ)) || #131: #mark(u12(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #u12(mark(PeRCenTX),PeRCenTY,PeRCenTZ) || #132: #mark(u12(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #mark(PeRCenTX) || #133: #u72(active(PeRCenTX),PeRCenTY) -> #u72(PeRCenTX,PeRCenTY) || #134: #splitAt(PeRCenTX,active(PeRCenTY)) -> #splitAt(PeRCenTX,PeRCenTY) || #135: #mark(s(PeRCenTX)) -> #active(s(mark(PeRCenTX))) || #136: #mark(s(PeRCenTX)) -> #s(mark(PeRCenTX)) || #137: #mark(s(PeRCenTX)) -> #mark(PeRCenTX) || #138: #u31(PeRCenTX,mark(PeRCenTY)) -> #u31(PeRCenTX,PeRCenTY) || #139: #u62(PeRCenTX,PeRCenTY,PeRCenTZ,mark(PeRCenTU)) -> #u62(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || #140: #u21(active(PeRCenTX),PeRCenTY) -> #u21(PeRCenTX,PeRCenTY) || #141: #afterNth(PeRCenTX,mark(PeRCenTY)) -> #afterNth(PeRCenTX,PeRCenTY) || #142: #active(u64(pair(PeRCenTX,PeRCenTY),PeRCenTZ)) -> #mark(pair(cons(PeRCenTZ,PeRCenTX),PeRCenTY)) || #143: #active(u64(pair(PeRCenTX,PeRCenTY),PeRCenTZ)) -> #pair(cons(PeRCenTZ,PeRCenTX),PeRCenTY) || #144: #active(u64(pair(PeRCenTX,PeRCenTY),PeRCenTZ)) -> #cons(PeRCenTZ,PeRCenTX) || #145: #u42(PeRCenTX,active(PeRCenTY),PeRCenTZ) -> #u42(PeRCenTX,PeRCenTY,PeRCenTZ) || #146: #sel(PeRCenTX,mark(PeRCenTY)) -> #sel(PeRCenTX,PeRCenTY) || #147: #u11(mark(PeRCenTX),PeRCenTY,PeRCenTZ) -> #u11(PeRCenTX,PeRCenTY,PeRCenTZ) || #148: #mark(tt()) -> #active(tt()) || #149: #mark(u81(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #active(u81(mark(PeRCenTX),PeRCenTY,PeRCenTZ)) || #150: #mark(u81(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #u81(mark(PeRCenTX),PeRCenTY,PeRCenTZ) || #151: #mark(u81(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #mark(PeRCenTX) || #152: #mark(cons(PeRCenTX,PeRCenTY)) -> #active(cons(mark(PeRCenTX),PeRCenTY)) || #153: #mark(cons(PeRCenTX,PeRCenTY)) -> #cons(mark(PeRCenTX),PeRCenTY) || #154: #mark(cons(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #155: #active(splitAt(0(),PeRCenTX)) -> #mark(pair(nil(),PeRCenTX)) || #156: #active(splitAt(0(),PeRCenTX)) -> #pair(nil(),PeRCenTX) || #157: #u62(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU) -> #u62(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || #158: #u81(mark(PeRCenTX),PeRCenTY,PeRCenTZ) -> #u81(PeRCenTX,PeRCenTY,PeRCenTZ) || #159: #head(mark(PeRCenTX)) -> #head(PeRCenTX) || #160: #u61(PeRCenTX,PeRCenTY,PeRCenTZ,active(PeRCenTU)) -> #u61(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || #161: #active(fst(pair(PeRCenTX,PeRCenTY))) -> #mark(u21(tt(),PeRCenTX)) || #162: #active(fst(pair(PeRCenTX,PeRCenTY))) -> #u21(tt(),PeRCenTX) || #163: #fst(active(PeRCenTX)) -> #fst(PeRCenTX) || #164: #u61(active(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU) -> #u61(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || #165: #u82(PeRCenTX,PeRCenTY,mark(PeRCenTZ)) -> #u82(PeRCenTX,PeRCenTY,PeRCenTZ) || #166: #u31(mark(PeRCenTX),PeRCenTY) -> #u31(PeRCenTX,PeRCenTY) || #167: #active(u41(tt(),PeRCenTX,PeRCenTY)) -> #mark(u42(tt(),PeRCenTX,PeRCenTY)) || #168: #active(u41(tt(),PeRCenTX,PeRCenTY)) -> #u42(tt(),PeRCenTX,PeRCenTY) || #169: #mark(u42(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #active(u42(mark(PeRCenTX),PeRCenTY,PeRCenTZ)) || #170: #mark(u42(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #u42(mark(PeRCenTX),PeRCenTY,PeRCenTZ) || #171: #mark(u42(PeRCenTX,PeRCenTY,PeRCenTZ)) -> #mark(PeRCenTX) || #172: #pair(PeRCenTX,active(PeRCenTY)) -> #pair(PeRCenTX,PeRCenTY) || #173: #u62(PeRCenTX,PeRCenTY,active(PeRCenTZ),PeRCenTU) -> #u62(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || #174: #active(u52(tt(),PeRCenTX)) -> #mark(PeRCenTX) || #175: #u32(mark(PeRCenTX),PeRCenTY) -> #u32(PeRCenTX,PeRCenTY) || #176: #u82(active(PeRCenTX),PeRCenTY,PeRCenTZ) -> #u82(PeRCenTX,PeRCenTY,PeRCenTZ) || #177: #u52(PeRCenTX,mark(PeRCenTY)) -> #u52(PeRCenTX,PeRCenTY) || #178: #u32(PeRCenTX,mark(PeRCenTY)) -> #u32(PeRCenTX,PeRCenTY) || #179: #u11(PeRCenTX,PeRCenTY,mark(PeRCenTZ)) -> #u11(PeRCenTX,PeRCenTY,PeRCenTZ) || #180: #mark(splitAt(PeRCenTX,PeRCenTY)) -> #active(splitAt(mark(PeRCenTX),mark(PeRCenTY))) || #181: #mark(splitAt(PeRCenTX,PeRCenTY)) -> #splitAt(mark(PeRCenTX),mark(PeRCenTY)) || #182: #mark(splitAt(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #183: #mark(splitAt(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTY) || #184: #u12(PeRCenTX,active(PeRCenTY),PeRCenTZ) -> #u12(PeRCenTX,PeRCenTY,PeRCenTZ) || #185: #u72(mark(PeRCenTX),PeRCenTY) -> #u72(PeRCenTX,PeRCenTY) || #186: #sel(mark(PeRCenTX),PeRCenTY) -> #sel(PeRCenTX,PeRCenTY) || #187: #u52(active(PeRCenTX),PeRCenTY) -> #u52(PeRCenTX,PeRCenTY) || #188: #active(u31(tt(),PeRCenTX)) -> #mark(u32(tt(),PeRCenTX)) || #189: #active(u31(tt(),PeRCenTX)) -> #u32(tt(),PeRCenTX) || #190: #mark(u61(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> #active(u61(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU)) || #191: #mark(u61(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> #u61(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU) || #192: #mark(u61(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU)) -> #mark(PeRCenTX) || #193: #u11(active(PeRCenTX),PeRCenTY,PeRCenTZ) -> #u11(PeRCenTX,PeRCenTY,PeRCenTZ) || #194: #u64(active(PeRCenTX),PeRCenTY) -> #u64(PeRCenTX,PeRCenTY) || #195: #active(take(PeRCenTX,PeRCenTY)) -> #mark(u81(tt(),PeRCenTX,PeRCenTY)) || #196: #active(take(PeRCenTX,PeRCenTY)) -> #u81(tt(),PeRCenTX,PeRCenTY) || #197: #active(natsFrom(PeRCenTX)) -> #mark(cons(PeRCenTX,natsFrom(s(PeRCenTX)))) || #198: #active(natsFrom(PeRCenTX)) -> #cons(PeRCenTX,natsFrom(s(PeRCenTX))) || #199: #active(natsFrom(PeRCenTX)) -> #natsFrom(s(PeRCenTX)) || #200: #active(natsFrom(PeRCenTX)) -> #s(PeRCenTX) || #201: #u61(PeRCenTX,active(PeRCenTY),PeRCenTZ,PeRCenTU) -> #u61(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || #202: #u81(active(PeRCenTX),PeRCenTY,PeRCenTZ) -> #u81(PeRCenTX,PeRCenTY,PeRCenTZ) || #203: #mark(u21(PeRCenTX,PeRCenTY)) -> #active(u21(mark(PeRCenTX),PeRCenTY)) || #204: #mark(u21(PeRCenTX,PeRCenTY)) -> #u21(mark(PeRCenTX),PeRCenTY) || #205: #mark(u21(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #206: #u81(PeRCenTX,PeRCenTY,active(PeRCenTZ)) -> #u81(PeRCenTX,PeRCenTY,PeRCenTZ) || #207: #s(active(PeRCenTX)) -> #s(PeRCenTX) || #208: #u22(mark(PeRCenTX),PeRCenTY) -> #u22(PeRCenTX,PeRCenTY) || #209: #u22(PeRCenTX,active(PeRCenTY)) -> #u22(PeRCenTX,PeRCenTY) || #210: #cons(PeRCenTX,active(PeRCenTY)) -> #cons(PeRCenTX,PeRCenTY) || #211: #active(tail(cons(PeRCenTX,PeRCenTY))) -> #mark(u71(tt(),PeRCenTY)) || #212: #active(tail(cons(PeRCenTX,PeRCenTY))) -> #u71(tt(),PeRCenTY) || #213: #u62(PeRCenTX,PeRCenTY,PeRCenTZ,active(PeRCenTU)) -> #u62(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || #214: #u63(PeRCenTX,PeRCenTY,active(PeRCenTZ),PeRCenTU) -> #u63(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || #215: #u63(active(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU) -> #u63(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || #216: #u71(PeRCenTX,active(PeRCenTY)) -> #u71(PeRCenTX,PeRCenTY) || #217: #sel(PeRCenTX,active(PeRCenTY)) -> #sel(PeRCenTX,PeRCenTY) || #218: #pair(mark(PeRCenTX),PeRCenTY) -> #pair(PeRCenTX,PeRCenTY) || #219: #mark(tail(PeRCenTX)) -> #active(tail(mark(PeRCenTX))) || #220: #mark(tail(PeRCenTX)) -> #tail(mark(PeRCenTX)) || #221: #mark(tail(PeRCenTX)) -> #mark(PeRCenTX) || #222: #u51(PeRCenTX,active(PeRCenTY)) -> #u51(PeRCenTX,PeRCenTY) || #223: #u82(mark(PeRCenTX),PeRCenTY,PeRCenTZ) -> #u82(PeRCenTX,PeRCenTY,PeRCenTZ) || #224: #active(u81(tt(),PeRCenTX,PeRCenTY)) -> #mark(u82(tt(),PeRCenTX,PeRCenTY)) || #225: #active(u81(tt(),PeRCenTX,PeRCenTY)) -> #u82(tt(),PeRCenTX,PeRCenTY) || #226: #mark(snd(PeRCenTX)) -> #active(snd(mark(PeRCenTX))) || #227: #mark(snd(PeRCenTX)) -> #snd(mark(PeRCenTX)) || #228: #mark(snd(PeRCenTX)) -> #mark(PeRCenTX) || #229: #active(afterNth(PeRCenTX,PeRCenTY)) -> #mark(u11(tt(),PeRCenTX,PeRCenTY)) || #230: #active(afterNth(PeRCenTX,PeRCenTY)) -> #u11(tt(),PeRCenTX,PeRCenTY) || #231: #u63(PeRCenTX,active(PeRCenTY),PeRCenTZ,PeRCenTU) -> #u63(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || #232: #u61(PeRCenTX,PeRCenTY,PeRCenTZ,mark(PeRCenTU)) -> #u61(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || #233: #take(active(PeRCenTX),PeRCenTY) -> #take(PeRCenTX,PeRCenTY) || #234: #sel(active(PeRCenTX),PeRCenTY) -> #sel(PeRCenTX,PeRCenTY) || #235: #u82(PeRCenTX,active(PeRCenTY),PeRCenTZ) -> #u82(PeRCenTX,PeRCenTY,PeRCenTZ) || #236: #u11(PeRCenTX,mark(PeRCenTY),PeRCenTZ) -> #u11(PeRCenTX,PeRCenTY,PeRCenTZ) || #237: #u62(PeRCenTX,active(PeRCenTY),PeRCenTZ,PeRCenTU) -> #u62(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || #238: #u42(active(PeRCenTX),PeRCenTY,PeRCenTZ) -> #u42(PeRCenTX,PeRCenTY,PeRCenTZ) || #239: #active(splitAt(s(PeRCenTX),cons(PeRCenTY,PeRCenTZ))) -> #mark(u61(tt(),PeRCenTX,PeRCenTY,PeRCenTZ)) || #240: #active(splitAt(s(PeRCenTX),cons(PeRCenTY,PeRCenTZ))) -> #u61(tt(),PeRCenTX,PeRCenTY,PeRCenTZ) || #241: #u41(PeRCenTX,active(PeRCenTY),PeRCenTZ) -> #u41(PeRCenTX,PeRCenTY,PeRCenTZ) || #242: #u22(PeRCenTX,mark(PeRCenTY)) -> #u22(PeRCenTX,PeRCenTY) || #243: #natsFrom(active(PeRCenTX)) -> #natsFrom(PeRCenTX) || #244: #u61(mark(PeRCenTX),PeRCenTY,PeRCenTZ,PeRCenTU) -> #u61(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || #245: #u12(mark(PeRCenTX),PeRCenTY,PeRCenTZ) -> #u12(PeRCenTX,PeRCenTY,PeRCenTZ) || #246: #u62(PeRCenTX,mark(PeRCenTY),PeRCenTZ,PeRCenTU) -> #u62(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || #247: #mark(u31(PeRCenTX,PeRCenTY)) -> #active(u31(mark(PeRCenTX),PeRCenTY)) || #248: #mark(u31(PeRCenTX,PeRCenTY)) -> #u31(mark(PeRCenTX),PeRCenTY) || #249: #mark(u31(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #250: #active(head(cons(PeRCenTX,PeRCenTY))) -> #mark(u31(tt(),PeRCenTX)) || #251: #active(head(cons(PeRCenTX,PeRCenTY))) -> #u31(tt(),PeRCenTX) || #252: #active(u72(tt(),PeRCenTX)) -> #mark(PeRCenTX) || #253: #active(u21(tt(),PeRCenTX)) -> #mark(u22(tt(),PeRCenTX)) || #254: #active(u21(tt(),PeRCenTX)) -> #u22(tt(),PeRCenTX) || #255: #u71(PeRCenTX,mark(PeRCenTY)) -> #u71(PeRCenTX,PeRCenTY) || #256: #splitAt(PeRCenTX,mark(PeRCenTY)) -> #splitAt(PeRCenTX,PeRCenTY) || #257: #active(u11(tt(),PeRCenTX,PeRCenTY)) -> #mark(u12(tt(),PeRCenTX,PeRCenTY)) || #258: #active(u11(tt(),PeRCenTX,PeRCenTY)) -> #u12(tt(),PeRCenTX,PeRCenTY) || #259: #u63(PeRCenTX,PeRCenTY,mark(PeRCenTZ),PeRCenTU) -> #u63(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || #260: #u61(PeRCenTX,PeRCenTY,mark(PeRCenTZ),PeRCenTU) -> #u61(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || #261: #mark(fst(PeRCenTX)) -> #active(fst(mark(PeRCenTX))) || #262: #mark(fst(PeRCenTX)) -> #fst(mark(PeRCenTX)) || #263: #mark(fst(PeRCenTX)) -> #mark(PeRCenTX) || #264: #u71(active(PeRCenTX),PeRCenTY) -> #u71(PeRCenTX,PeRCenTY) || #265: #active(u42(tt(),PeRCenTX,PeRCenTY)) -> #mark(head(afterNth(PeRCenTX,PeRCenTY))) || #266: #active(u42(tt(),PeRCenTX,PeRCenTY)) -> #head(afterNth(PeRCenTX,PeRCenTY)) || #267: #active(u42(tt(),PeRCenTX,PeRCenTY)) -> #afterNth(PeRCenTX,PeRCenTY) || #268: #pair(active(PeRCenTX),PeRCenTY) -> #pair(PeRCenTX,PeRCenTY) || #269: #u81(PeRCenTX,PeRCenTY,mark(PeRCenTZ)) -> #u81(PeRCenTX,PeRCenTY,PeRCenTZ) || #270: #u63(PeRCenTX,PeRCenTY,PeRCenTZ,mark(PeRCenTU)) -> #u63(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || #271: #u52(PeRCenTX,active(PeRCenTY)) -> #u52(PeRCenTX,PeRCenTY) || #272: #natsFrom(mark(PeRCenTX)) -> #natsFrom(PeRCenTX) || #273: #active(u71(tt(),PeRCenTX)) -> #mark(u72(tt(),PeRCenTX)) || #274: #active(u71(tt(),PeRCenTX)) -> #u72(tt(),PeRCenTX) || #275: #u63(PeRCenTX,PeRCenTY,PeRCenTZ,active(PeRCenTU)) -> #u63(PeRCenTX,PeRCenTY,PeRCenTZ,PeRCenTU) || #276: #u42(mark(PeRCenTX),PeRCenTY,PeRCenTZ) -> #u42(PeRCenTX,PeRCenTY,PeRCenTZ) || #277: #tail(active(PeRCenTX)) -> #tail(PeRCenTX) || #278: #u42(PeRCenTX,mark(PeRCenTY),PeRCenTZ) -> #u42(PeRCenTX,PeRCenTY,PeRCenTZ) || #279: #active(u22(tt(),PeRCenTX)) -> #mark(PeRCenTX) || #280: #tail(mark(PeRCenTX)) -> #tail(PeRCenTX) || #281: #u42(PeRCenTX,PeRCenTY,mark(PeRCenTZ)) -> #u42(PeRCenTX,PeRCenTY,PeRCenTZ) || #282: #u21(mark(PeRCenTX),PeRCenTY) -> #u21(PeRCenTX,PeRCenTY) || #283: #mark(u71(PeRCenTX,PeRCenTY)) -> #active(u71(mark(PeRCenTX),PeRCenTY)) || #284: #mark(u71(PeRCenTX,PeRCenTY)) -> #u71(mark(PeRCenTX),PeRCenTY) || #285: #mark(u71(PeRCenTX,PeRCenTY)) -> #mark(PeRCenTX) || #286: #active(u82(tt(),PeRCenTX,PeRCenTY)) -> #mark(fst(splitAt(PeRCenTX,PeRCenTY))) || #287: #active(u82(tt(),PeRCenTX,PeRCenTY)) -> #fst(splitAt(PeRCenTX,PeRCenTY)) || #288: #active(u82(tt(),PeRCenTX,PeRCenTY)) -> #splitAt(PeRCenTX,PeRCenTY) || #289: #s(mark(PeRCenTX)) -> #s(PeRCenTX) || Number of SCCs: 31, DPs: 222 || SCC { #243 #272 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: x1 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #243 #272 || Number of SCCs: 30, DPs: 220 || SCC { #110 #159 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: x1 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #110 #159 || Number of SCCs: 29, DPs: 218 || SCC { #207 #289 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: x1 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #207 #289 || Number of SCCs: 28, DPs: 216 || SCC { #277 #280 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: x1 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #277 #280 || Number of SCCs: 27, DPs: 214 || SCC { #55 #58 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: x1 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #55 #58 || Number of SCCs: 26, DPs: 212 || SCC { #56 #163 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: x1 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #56 #163 || Number of SCCs: 25, DPs: 210 || SCC { #120 #177 #187 #271 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: x1 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #120 #187 || Number of SCCs: 25, DPs: 208 || SCC { #177 #271 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: x2 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #177 #271 || Number of SCCs: 24, DPs: 206 || SCC { #24 #48 #89 #194 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: x1 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #89 #194 || Number of SCCs: 24, DPs: 204 || SCC { #24 #48 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: x2 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #24 #48 || Number of SCCs: 23, DPs: 202 || SCC { #42 #78 #109 #233 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: x1 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #109 #233 || Number of SCCs: 23, DPs: 200 || SCC { #42 #78 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: x2 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #42 #78 || Number of SCCs: 22, DPs: 198 || SCC { #146 #186 #217 #234 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: x2 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #146 #217 || Number of SCCs: 22, DPs: 196 || SCC { #186 #234 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: x1 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #186 #234 || Number of SCCs: 21, DPs: 194 || SCC { #72 #74 #102 #210 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: x1 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #72 #102 || Number of SCCs: 21, DPs: 192 || SCC { #74 #210 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: x2 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #74 #210 || Number of SCCs: 20, DPs: 190 || SCC { #57 #62 #79 #141 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: x2 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #62 #141 || Number of SCCs: 20, DPs: 188 || SCC { #57 #79 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: x1 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #57 #79 || Number of SCCs: 19, DPs: 186 || SCC { #71 #172 #218 #268 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: x2 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #71 #172 || Number of SCCs: 19, DPs: 184 || SCC { #218 #268 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: x1 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #218 #268 || Number of SCCs: 18, DPs: 182 || SCC { #4 #208 #209 #242 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: x1 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #4 #208 || Number of SCCs: 18, DPs: 180 || SCC { #209 #242 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: x2 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #209 #242 || Number of SCCs: 17, DPs: 178 || SCC { #23 #33 #73 #222 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: x2 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #23 #222 || Number of SCCs: 17, DPs: 176 || SCC { #33 #73 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: x1 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #33 #73 || Number of SCCs: 16, DPs: 174 || SCC { #25 #111 #175 #178 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: x1 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #111 #175 || Number of SCCs: 16, DPs: 172 || SCC { #25 #178 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: x2 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #25 #178 || Number of SCCs: 15, DPs: 170 || SCC { #37 #88 #138 #166 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: x1 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #88 #166 || Number of SCCs: 15, DPs: 168 || SCC { #37 #138 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: x2 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #37 #138 || Number of SCCs: 14, DPs: 166 || SCC { #14 #119 #140 #282 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: x2 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #14 #119 || Number of SCCs: 14, DPs: 164 || SCC { #140 #282 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: x1 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #140 #282 || Number of SCCs: 13, DPs: 162 || SCC { #35 #76 #133 #185 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: x1 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #133 #185 || Number of SCCs: 13, DPs: 160 || SCC { #35 #76 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: x2 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #35 #76 || Number of SCCs: 12, DPs: 158 || SCC { #63 #216 #255 #264 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: x1 || USABLE RULES: { } || Removed DPs: #63 #264 || Number of SCCs: 12, DPs: 156 || SCC { #216 #255 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: x2 || USABLE RULES: { } || Removed DPs: #216 #255 || Number of SCCs: 11, DPs: 154 || SCC { #107 #121 #134 #256 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: x1 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #107 #121 || Number of SCCs: 11, DPs: 152 || SCC { #134 #256 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: x2 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #134 #256 || Number of SCCs: 10, DPs: 150 || SCC { #15 #84 #147 #179 #193 #236 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: x2 + x3 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #15 #84 #179 #236 || Number of SCCs: 10, DPs: 146 || SCC { #147 #193 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: x1 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #147 #193 || Number of SCCs: 9, DPs: 144 || SCC { #34 #36 #101 #125 #127 #241 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: x1 + x2 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #34 #36 #125 #241 || Number of SCCs: 9, DPs: 140 || SCC { #101 #127 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: x3 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #101 #127 || Number of SCCs: 8, DPs: 138 || SCC { #38 #47 #115 #126 #184 #245 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: x1 + x2 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #47 #126 #184 #245 || Number of SCCs: 8, DPs: 134 || SCC { #38 #115 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: x3 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #38 #115 || Number of SCCs: 7, DPs: 132 || SCC { #16 #46 #165 #176 #223 #235 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: x1 + x3 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #16 #165 #176 #223 || Number of SCCs: 7, DPs: 128 || SCC { #46 #235 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: x2 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #46 #235 || Number of SCCs: 6, DPs: 126 || SCC { #59 #108 #158 #202 #206 #269 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: x2 + x3 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #59 #108 #206 #269 || Number of SCCs: 6, DPs: 122 || SCC { #158 #202 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: x1 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #158 #202 || Number of SCCs: 5, DPs: 120 || SCC { #90 #145 #238 #276 #278 #281 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: x2 + x3 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #90 #145 #278 #281 || Number of SCCs: 5, DPs: 116 || SCC { #238 #276 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: x1 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #238 #276 || Number of SCCs: 4, DPs: 114 || SCC { #49 #61 #214 #215 #231 #259 #270 #275 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: x2 + x3 + x4 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #49 #214 #231 #259 #270 #275 || Number of SCCs: 4, DPs: 108 || SCC { #61 #215 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: x1 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #61 #215 || Number of SCCs: 3, DPs: 106 || SCC { #80 #114 #139 #157 #173 #213 #237 #246 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: x2 + x3 + x4 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #80 #139 #173 #213 #237 #246 || Number of SCCs: 3, DPs: 100 || SCC { #114 #157 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: x1 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #114 #157 || Number of SCCs: 2, DPs: 98 || SCC { #54 #118 #160 #164 #201 #232 #244 #260 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: x1 + x2 + x3 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #54 #118 #164 #201 #244 #260 || Number of SCCs: 2, DPs: 92 || SCC { #160 #232 } || POLO(Sum)... succeeded. || u81 w: 0 || #u22 w: 0 || u62 w: 0 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: 0 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 0 || #u21 w: 0 || pair w: 0 || fst w: 0 || #u64 w: 0 || natsFrom w: 0 || #u12 w: 0 || #head w: 0 || #u61 w: x4 || splitAt w: 0 || u52 w: 0 || #fst w: 0 || #u11 w: 0 || u61 w: 0 || #u81 w: 0 || u41 w: 0 || #u72 w: 0 || u63 w: 0 || u51 w: 0 || tail w: 0 || #mark w: 0 || 0 w: 0 || #sel w: 0 || u11 w: 0 || sel w: 0 || u32 w: 0 || #u63 w: 0 || u64 w: 0 || #s w: 0 || afterNth w: 0 || nil w: 0 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: 0 || #afterNth w: 0 || u72 w: 0 || u21 w: 0 || #u41 w: 0 || u82 w: 0 || active w: x1 + 1 || head w: 0 || #u42 w: 0 || #snd w: 0 || cons w: 0 || #natsFrom w: 0 || #active w: 0 || #u31 w: 0 || snd w: 0 || u22 w: 0 || u42 w: 0 || tt w: 0 || #pair w: 0 || u71 w: 0 || #u32 w: 0 || u31 w: 0 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { } || Removed DPs: #160 #232 || Number of SCCs: 1, DPs: 90 || SCC { #1 #5 #7 #8 #10 #11 #13 #17 #19 #20 #22 #26 #28..30 #32 #39 #41 #43 #45 #52 #53 #64 #66..68 #70 #75 #81 #83 #85 #87 #91 #93 #94 #97 #99 #103 #105 #106 #112 #116 #122 #124 #128 #130 #132 #137 #142 #149 #151 #154 #155 #161 #167 #169 #171 #174 #180 #182 #183 #188 #190 #192 #195 #197 #203 #205 #211 #219 #221 #224 #226 #228 #229 #239 #247 #249 #250 #252 #253 #257 #261 #263 #265 #273 #279 #283 #285 #286 } || POLO(Sum)... POLO(max)... succeeded. || u81 w: max(x1 + 26, x2 + 24, x3 + 23) || #u22 w: 0 || u62 w: max(x1 + 12, x2 + 10, x3 + 9, x4 + 8) || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: x1 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: max(x1 + 29, x2 + 28) || #u21 w: 0 || pair w: max(x1 + 2, x2 + 1) || fst w: x1 + 8 || #u64 w: 0 || natsFrom w: x1 + 6 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: max(x1 + 10, x2 + 8) || u52 w: max(x1 + 2, x2 + 1) || #fst w: 0 || #u11 w: 0 || u61 w: max(x1 + 12, x2 + 10, x3 + 9, x4 + 8) || #u81 w: 0 || u41 w: max(x1 + 45, x2 + 44, x3 + 43) || #u72 w: 0 || u63 w: max(x1 + 12, x2 + 10, x3 + 7, x4 + 8) || u51 w: max(x1 + 5, x2 + 4) || tail w: x1 + 9 || #mark w: x1 || 0 w: 1 || #sel w: 0 || u11 w: max(x1 + 26, x2 + 23, x3 + 25) || sel w: max(x1 + 49, x2 + 48) || u32 w: max(x1 + 3, x2 + 1) || #u63 w: 0 || u64 w: max(x1, x2 + 7) || #s w: 0 || afterNth w: max(x1 + 24, x2 + 28) || nil w: 1 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 || u12 w: max(x1 + 21, x2 + 20, x3 + 19) || #afterNth w: 0 || u72 w: max(x1 + 2, x2 + 1) || u21 w: max(x1 + 6, x2 + 5) || #u41 w: 0 || u82 w: max(x1 + 20, x2 + 19, x3 + 22) || active w: x1 || head w: x1 + 7 || #u42 w: 0 || #snd w: 0 || cons w: max(x1 + 5, x2) || #natsFrom w: 0 || #active w: x1 || #u31 w: 0 || snd w: x1 + 8 || u22 w: max(x1 + 2, x2 + 1) || u42 w: max(x1 + 40, x2 + 39, x3 + 38) || tt w: 1 || #pair w: 0 || u71 w: max(x1 + 5, x2 + 4) || #u32 w: 0 || u31 w: max(x1 + 7, x2 + 5) || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { 1..193 } || Removed DPs: #1 #7 #10 #13 #19 #22 #28 #29 #32 #45 #52 #53 #66 #67 #70 #75 #83 #87 #93 #97 #105 #106 #112 #116 #124 #132 #151 #154 #155 #161 #167 #171 #174 #182 #183 #188 #192 #195 #205 #211 #221 #224 #228 #229 #249 #250 #252 #253 #257 #263 #265 #273 #279 #285 #286 || Number of SCCs: 1, DPs: 10 || SCC { #17 #41 #94 #99 #122 #128 #137 #180 #190 #239 } || POLO(Sum)... succeeded. || u81 w: x2 + 3 || #u22 w: 0 || u62 w: 7 || TIlDePAIR w: 0 || #u82 w: 0 || #cons w: 0 || s w: x1 + 1 || #u52 w: 0 || #take w: 0 || #u51 w: 0 || take w: 1 || #u21 w: 0 || pair w: x1 + x2 + 1 || fst w: x1 || #u64 w: 0 || natsFrom w: 1 || #u12 w: 0 || #head w: 0 || #u61 w: 0 || splitAt w: 7 || u52 w: x2 + 3 || #fst w: 0 || #u11 w: 0 || u61 w: 7 || #u81 w: 0 || u41 w: x1 + x2 + x3 || #u72 w: 0 || u63 w: 7 || u51 w: x2 + 1 || tail w: 4 || #mark w: x1 + 1 || 0 w: 0 || #sel w: 0 || u11 w: x2 + x3 + 4 || sel w: x1 + x2 + 3 || u32 w: x1 + x2 || #u63 w: 0 || u64 w: x1 || #s w: 0 || afterNth w: 1 || nil w: 8 || #TIlDePAIR w: 0 || #tail w: 0 || #splitAt w: 0 || mark w: x1 + 1 || u12 w: x1 + x2 + x3 || #afterNth w: 0 || u72 w: 1 || u21 w: x1 + x2 || #u41 w: 0 || u82 w: x1 + x2 + x3 || active w: x1 + 2 || head w: x1 || #u42 w: 0 || #snd w: 0 || cons w: x1 + 4 || #natsFrom w: 0 || #active w: 8 || #u31 w: 0 || snd w: 1 || u22 w: x1 + x2 || u42 w: x2 || tt w: 5 || #pair w: 0 || u71 w: x1 || #u32 w: 0 || u31 w: x1 || #u62 w: 0 || #u71 w: 0 || USABLE RULES: { 62..107 110..177 180..183 190..193 } || Removed DPs: #137 || Number of SCCs: 1, DPs: 9 || SCC { #17 #41 #94 #99 #122 #128 #180 #190 #239 } || POLO(Sum)... POLO(max)... QLPOS... POLO(mSum)... QWPOpS(mSum)... succeeded. || u81 s: [2] p: 0 w: x1 + x2 + x3 + 41 || #u22 s: [1] p: 0 w: x1 || u62 s: [2,1] p: 5 w: max(x1 + 38, x2 + 47, x3 + 41, x4 + 34) || TIlDePAIR s: [1,2] p: 0 w: x1 + x2 + 1 || #u82 s: [1,3] p: 0 w: x1 + x3 || #cons s: [] p: 0 w: max(x2 + 1) || s s: [1] p: 0 w: x1 || #u52 s: [] p: 0 w: x2 + 1 || #take s: [1] p: 0 w: x1 + 1 || #u51 s: [] p: 0 w: x2 || take s: [2] p: 1 w: x1 + x2 + 49 || #u21 s: [1,2] p: 0 w: x1 + x2 + 1 || pair s: [] p: 2 w: max(x1 + 10, x2 + 21) || fst s: [1] p: 2 w: x1 || #u64 s: [] p: 0 w: max(x1 + 1) || natsFrom s: [1] p: 4 w: x1 + 46 || #u12 s: [1,3] p: 0 w: x1 + x3 + 1 || #head s: [] p: 0 w: 1 || #u61 s: [2] p: 0 w: max(x2) || splitAt s: [1] p: 5 w: max(x1 + 47, x2 + 34) || u52 s: [2] p: 1 w: x2 || #fst s: [] p: 0 w: 0 || #u11 s: [3,2,1] p: 0 w: x1 + x2 + x3 || u61 s: [2,1,3] p: 5 w: max(x1 + 37, x2 + 47, x3 + 42, x4 + 34) || #u81 s: [] p: 0 w: 1 || u41 s: [] p: 6 w: x2 + x3 + 51 || #u72 s: [] p: 0 w: 0 || u63 s: [2,1] p: 5 w: max(x1 + 39, x2 + 47, x3 + 40, x4 + 34) || u51 s: [1] p: 1 w: x1 + x2 + 4 || tail s: [] p: 4 w: x1 + 10 || #mark s: 1 || 0 s: [] p: 2 w: 22 || #sel s: [2,1] p: 0 w: x1 + x2 || u11 s: [] p: 1 w: x2 + x3 + 48 || sel s: [2] p: 1 w: x1 + x2 + 52 || u32 s: [] p: 0 w: x1 + x2 + 1 || #u63 s: [3,2,4,1] p: 0 w: max(x1, x2, x3 + 1, x4) || u64 s: [2,1] p: 2 w: max(x1, x2 + 20) || #s s: [] p: 0 w: 0 || afterNth s: [] p: 1 w: x1 + x2 + 49 || nil s: [] p: 6 w: 23 || #TIlDePAIR s: [2,1] p: 0 w: x1 + x2 + 1 || #tail s: [] p: 0 w: 1 || #splitAt s: [] p: 0 w: max(x1) || mark s: 1 || u12 s: [2,1] p: 6 w: x1 + x2 + x3 + 40 || #afterNth s: [1,2] p: 0 w: x1 + x2 + 1 || u72 s: [2] p: 2 w: x1 + x2 + 1 || u21 s: [] p: 2 w: x2 + 10 || #u41 s: [2] p: 0 w: x1 + x2 + 1 || u82 s: [1,3] p: 6 w: x1 + x2 + x3 + 40 || active s: 1 || head s: [] p: 1 w: x1 + 1 || #u42 s: [] p: 0 w: x2 + 1 || #snd s: [] p: 0 w: 1 || cons s: [] p: 4 w: max(x1 + 9, x2) || #natsFrom s: [] p: 0 w: 0 || #active s: 1 || #u31 s: [1] p: 0 w: x1 + 1 || snd s: 1 || u22 s: [2] p: 5 w: x2 + 1 || u42 s: [] p: 2 w: x2 + x3 + 50 || tt s: [] p: 3 w: 7 || #pair s: [] p: 0 w: 0 || u71 s: [2] p: 3 w: x2 + 10 || #u32 s: [] p: 0 w: x2 || u31 s: [] p: 1 w: x2 + 8 || #u62 s: [3,1] p: 0 w: max(x1, x2 + 1, x3) || #u71 s: [1] p: 0 w: x1 || USABLE RULES: { 1..193 } || Removed DPs: #41 #94 #99 #239 || Number of SCCs: 0, DPs: 0 || We use the dependency pair framework as described in [Kop12, Ch. 6/7], with static dependency pairs (see [KusIsoSakBla09] and the adaptation for AFSMs and accessible arguments in [FuhKop19]). We thus obtain the following dependency pair problem (P_0, R_0, computable, formative): Dependency Pairs P_0: 0] map#(/\x.X(x), cons(Y, Z)) =#> cons#(X(Y), map(/\y.X(y), Z)) 1] map#(/\x.X(x), cons(Y, Z)) =#> map#(/\y.X(y), Z) Rules R_0: active(u11(tt, X, Y)) => mark(u12(tt, X, Y)) active(u12(tt, X, Y)) => mark(snd(splitAt(X, Y))) active(u21(tt, X)) => mark(u22(tt, X)) active(u22(tt, X)) => mark(X) active(u31(tt, X)) => mark(u32(tt, X)) active(u32(tt, X)) => mark(X) active(u41(tt, X, Y)) => mark(u42(tt, X, Y)) active(u42(tt, X, Y)) => mark(head(afterNth(X, Y))) active(u51(tt, X)) => mark(u52(tt, X)) active(u52(tt, X)) => mark(X) active(u61(tt, X, Y, Z)) => mark(u62(tt, X, Y, Z)) active(u62(tt, X, Y, Z)) => mark(u63(tt, X, Y, Z)) active(u63(tt, X, Y, Z)) => mark(u64(splitAt(X, Z), Y)) active(u64(pair(X, Y), Z)) => mark(pair(cons(Z, X), Y)) active(u71(tt, X)) => mark(u72(tt, X)) active(u72(tt, X)) => mark(X) active(u81(tt, X, Y)) => mark(u82(tt, X, Y)) active(u82(tt, X, Y)) => mark(fst(splitAt(X, Y))) active(afterNth(X, Y)) => mark(u11(tt, X, Y)) active(fst(pair(X, Y))) => mark(u21(tt, X)) active(head(cons(X, Y))) => mark(u31(tt, X)) active(natsFrom(X)) => mark(cons(X, natsFrom(s(X)))) active(sel(X, Y)) => mark(u41(tt, X, Y)) active(snd(pair(X, Y))) => mark(u51(tt, Y)) active(splitAt(0, X)) => mark(pair(nil, X)) active(splitAt(s(X), cons(Y, Z))) => mark(u61(tt, X, Y, Z)) active(tail(cons(X, Y))) => mark(u71(tt, Y)) active(take(X, Y)) => mark(u81(tt, X, Y)) mark(u11(X, Y, Z)) => active(u11(mark(X), Y, Z)) mark(tt) => active(tt) mark(u12(X, Y, Z)) => active(u12(mark(X), Y, Z)) mark(snd(X)) => active(snd(mark(X))) mark(splitAt(X, Y)) => active(splitAt(mark(X), mark(Y))) mark(u21(X, Y)) => active(u21(mark(X), Y)) mark(u22(X, Y)) => active(u22(mark(X), Y)) mark(u31(X, Y)) => active(u31(mark(X), Y)) mark(u32(X, Y)) => active(u32(mark(X), Y)) mark(u41(X, Y, Z)) => active(u41(mark(X), Y, Z)) mark(u42(X, Y, Z)) => active(u42(mark(X), Y, Z)) mark(head(X)) => active(head(mark(X))) mark(afterNth(X, Y)) => active(afterNth(mark(X), mark(Y))) mark(u51(X, Y)) => active(u51(mark(X), Y)) mark(u52(X, Y)) => active(u52(mark(X), Y)) mark(u61(X, Y, Z, U)) => active(u61(mark(X), Y, Z, U)) mark(u62(X, Y, Z, U)) => active(u62(mark(X), Y, Z, U)) mark(u63(X, Y, Z, U)) => active(u63(mark(X), Y, Z, U)) mark(u64(X, Y)) => active(u64(mark(X), Y)) mark(pair(X, Y)) => active(pair(mark(X), mark(Y))) mark(cons(X, Y)) => active(cons(mark(X), Y)) mark(u71(X, Y)) => active(u71(mark(X), Y)) mark(u72(X, Y)) => active(u72(mark(X), Y)) mark(u81(X, Y, Z)) => active(u81(mark(X), Y, Z)) mark(u82(X, Y, Z)) => active(u82(mark(X), Y, Z)) mark(fst(X)) => active(fst(mark(X))) mark(natsFrom(X)) => active(natsFrom(mark(X))) mark(s(X)) => active(s(mark(X))) mark(sel(X, Y)) => active(sel(mark(X), mark(Y))) mark(0) => active(0) mark(nil) => active(nil) mark(tail(X)) => active(tail(mark(X))) mark(take(X, Y)) => active(take(mark(X), mark(Y))) u11(mark(X), Y, Z) => 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) u12(mark(X), Y, Z) => u12(X, Y, Z) u12(X, mark(Y), Z) => u12(X, Y, Z) u12(X, Y, mark(Z)) => u12(X, Y, Z) u12(active(X), Y, Z) => u12(X, Y, Z) u12(X, active(Y), Z) => u12(X, Y, Z) u12(X, Y, active(Z)) => u12(X, Y, Z) snd(mark(X)) => snd(X) snd(active(X)) => snd(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) 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) u22(mark(X), Y) => u22(X, Y) u22(X, mark(Y)) => u22(X, Y) u22(active(X), Y) => u22(X, Y) u22(X, active(Y)) => u22(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) u32(mark(X), Y) => u32(X, Y) u32(X, mark(Y)) => u32(X, Y) u32(active(X), Y) => u32(X, Y) u32(X, active(Y)) => u32(X, Y) u41(mark(X), Y, Z) => u41(X, Y, Z) u41(X, mark(Y), Z) => u41(X, Y, Z) u41(X, Y, mark(Z)) => u41(X, Y, Z) u41(active(X), Y, Z) => u41(X, Y, Z) u41(X, active(Y), Z) => u41(X, Y, Z) u41(X, Y, active(Z)) => u41(X, Y, Z) u42(mark(X), Y, Z) => u42(X, Y, Z) u42(X, mark(Y), Z) => u42(X, Y, Z) u42(X, Y, mark(Z)) => u42(X, Y, Z) u42(active(X), Y, Z) => u42(X, Y, Z) u42(X, active(Y), Z) => u42(X, Y, Z) u42(X, Y, active(Z)) => u42(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) u51(mark(X), Y) => u51(X, Y) u51(X, mark(Y)) => u51(X, Y) u51(active(X), Y) => u51(X, Y) u51(X, active(Y)) => u51(X, Y) u52(mark(X), Y) => u52(X, Y) u52(X, mark(Y)) => u52(X, Y) u52(active(X), Y) => u52(X, Y) u52(X, active(Y)) => u52(X, Y) u61(mark(X), Y, Z, U) => u61(X, Y, Z, U) u61(X, mark(Y), Z, U) => u61(X, Y, Z, U) u61(X, Y, mark(Z), U) => u61(X, Y, Z, U) u61(X, Y, Z, mark(U)) => u61(X, Y, Z, U) u61(active(X), Y, Z, U) => u61(X, Y, Z, U) u61(X, active(Y), Z, U) => u61(X, Y, Z, U) u61(X, Y, active(Z), U) => u61(X, Y, Z, U) u61(X, Y, Z, active(U)) => u61(X, Y, Z, U) u62(mark(X), Y, Z, U) => u62(X, Y, Z, U) u62(X, mark(Y), Z, U) => u62(X, Y, Z, U) u62(X, Y, mark(Z), U) => u62(X, Y, Z, U) u62(X, Y, Z, mark(U)) => u62(X, Y, Z, U) u62(active(X), Y, Z, U) => u62(X, Y, Z, U) u62(X, active(Y), Z, U) => u62(X, Y, Z, U) u62(X, Y, active(Z), U) => u62(X, Y, Z, U) u62(X, Y, Z, active(U)) => u62(X, Y, Z, U) u63(mark(X), Y, Z, U) => u63(X, Y, Z, U) u63(X, mark(Y), Z, U) => u63(X, Y, Z, U) u63(X, Y, mark(Z), U) => u63(X, Y, Z, U) u63(X, Y, Z, mark(U)) => u63(X, Y, Z, U) u63(active(X), Y, Z, U) => u63(X, Y, Z, U) u63(X, active(Y), Z, U) => u63(X, Y, Z, U) u63(X, Y, active(Z), U) => u63(X, Y, Z, U) u63(X, Y, Z, active(U)) => u63(X, Y, Z, U) u64(mark(X), Y) => u64(X, Y) u64(X, mark(Y)) => u64(X, Y) u64(active(X), Y) => u64(X, Y) u64(X, active(Y)) => u64(X, Y) pair(mark(X), Y) => pair(X, Y) pair(X, mark(Y)) => pair(X, Y) pair(active(X), Y) => pair(X, Y) pair(X, active(Y)) => pair(X, Y) cons(mark(X), Y) => cons(X, Y) cons(X, mark(Y)) => cons(X, Y) cons(active(X), Y) => cons(X, Y) cons(X, active(Y)) => cons(X, Y) 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) u72(mark(X), Y) => u72(X, Y) u72(X, mark(Y)) => u72(X, Y) u72(active(X), Y) => u72(X, Y) u72(X, active(Y)) => u72(X, Y) u81(mark(X), Y, Z) => u81(X, Y, Z) u81(X, mark(Y), Z) => u81(X, Y, Z) u81(X, Y, mark(Z)) => u81(X, Y, Z) u81(active(X), Y, Z) => u81(X, Y, Z) u81(X, active(Y), Z) => u81(X, Y, Z) u81(X, Y, active(Z)) => u81(X, Y, Z) u82(mark(X), Y, Z) => u82(X, Y, Z) u82(X, mark(Y), Z) => u82(X, Y, Z) u82(X, Y, mark(Z)) => u82(X, Y, Z) u82(active(X), Y, Z) => u82(X, Y, Z) u82(X, active(Y), Z) => u82(X, Y, Z) u82(X, Y, active(Z)) => u82(X, Y, Z) fst(mark(X)) => fst(X) fst(active(X)) => fst(X) natsFrom(mark(X)) => natsFrom(X) natsFrom(active(X)) => natsFrom(X) s(mark(X)) => s(X) s(active(X)) => s(X) sel(mark(X), Y) => sel(X, Y) sel(X, mark(Y)) => sel(X, Y) sel(active(X), Y) => sel(X, Y) sel(X, active(Y)) => sel(X, Y) tail(mark(X)) => tail(X) tail(active(X)) => tail(X) take(mark(X), Y) => take(X, Y) take(X, mark(Y)) => take(X, Y) take(active(X), Y) => take(X, Y) take(X, active(Y)) => take(X, Y) map(/\x.X(x), nil) => nil map(/\x.X(x), cons(Y, Z)) => cons(X(Y), map(/\y.X(y), Z)) app(/\x.X(x), Y) => X(Y) Thus, the original system is terminating if (P_0, R_0, computable, formative) is finite. We consider the dependency pair problem (P_0, R_0, computable, formative). We place the elements of P in a dependency graph approximation G (see e.g. [Kop12, Thm. 7.27, 7.29], as follows: * 0 : * 1 : 0, 1 This graph has the following strongly connected components: P_1: map#(/\x.X(x), cons(Y, Z)) =#> map#(/\y.X(y), Z) By [Kop12, Thm. 7.31], we may replace any dependency pair problem (P_0, R_0, m, f) by (P_1, R_0, m, f). Thus, the original system is terminating if (P_1, R_0, computable, formative) is finite. We consider the dependency pair problem (P_1, R_0, computable, formative). We apply the subterm criterion with the following projection function: nu(map#) = 2 Thus, we can orient the dependency pairs as follows: nu(map#(/\x.X(x), cons(Y, Z))) = cons(Y, Z) |> Z = nu(map#(/\y.X(y), Z)) By [FuhKop19, Thm. 61], we may replace a dependency pair problem (P_1, R_0, computable, f) by ({}, R_0, computable, f). By the empty set processor [Kop12, Thm. 7.15] this problem may be immediately removed. As all dependency pair problems were succesfully simplified with sound (and complete) processors until nothing remained, we conclude termination. +++ Citations +++ [FuhKop19] C. Fuhs, and C. Kop. A static higher-order dependency pair framework. In Proceedings of ESOP 2019, 2019. [Kop11] C. Kop. Simplifying Algebraic Functional Systems. In Proceedings of CAI 2011, volume 6742 of LNCS. 201--215, Springer, 2011. [Kop12] C. Kop. Higher Order Termination. PhD Thesis, 2012. [KusIsoSakBla09] K. Kusakari, Y. Isogai, M. Sakai, and F. Blanqui. Static Dependency Pair Method Based On Strong Computability for Higher-Order Rewrite Systems. In volume 92(10) of IEICE Transactions on Information and Systems. 2007--2015, 2009.