TIMEOUT

The TRS could not be proven terminating. The proof attempt took 60000 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (419ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (3ms), PolynomialLinearRange4iUR (0ms), DependencyGraph (35ms), PolynomialOrderingProcessor (0ms), DependencyGraph (3ms), PolynomialLinearRange4 (220ms), DependencyGraph (3ms), PolynomialLinearRange4 (190ms), DependencyGraph (2ms), PolynomialLinearRange4 (120ms), DependencyGraph (3ms), ReductionPairSAT (7920ms), DependencyGraph (2ms), SizeChangePrinciple (timeout)].
 | – Problem 3 was processed with processor PolynomialLinearRange4 (86ms).
 |    | – Problem 4 was processed with processor PolynomialLinearRange4 (22ms).

The following open problems remain:

Open Dependency Pair Problem 2

Dependency Pairs

U63#(tt, N, X, XS) → splitAt#(N, XS)U62#(tt, N, X, XS) → U63#(tt, N, X, XS)
splitAt#(s(N), cons(X, XS)) → U61#(tt, N, X, XS)U61#(tt, N, X, XS) → U62#(tt, N, X, XS)

Rewrite Rules

U11(tt, N, XS) → U12(tt, N, XS)U12(tt, N, XS) → snd(splitAt(N, XS))
U21(tt, X) → U22(tt, X)U22(tt, X) → X
U31(tt, N) → U32(tt, N)U32(tt, N) → N
U41(tt, N, XS) → U42(tt, N, XS)U42(tt, N, XS) → head(afterNth(N, XS))
U51(tt, Y) → U52(tt, Y)U52(tt, Y) → Y
U61(tt, N, X, XS) → U62(tt, N, X, XS)U62(tt, N, X, XS) → U63(tt, N, X, XS)
U63(tt, N, X, XS) → U64(splitAt(N, XS), X)U64(pair(YS, ZS), X) → pair(cons(X, YS), ZS)
U71(tt, XS) → U72(tt, XS)U72(tt, XS) → XS
U81(tt, N, XS) → U82(tt, N, XS)U82(tt, N, XS) → fst(splitAt(N, XS))
afterNth(N, XS) → U11(tt, N, XS)fst(pair(X, Y)) → U21(tt, X)
head(cons(N, XS)) → U31(tt, N)natsFrom(N) → cons(N, natsFrom(s(N)))
sel(N, XS) → U41(tt, N, XS)snd(pair(X, Y)) → U51(tt, Y)
splitAt(0, XS) → pair(nil, XS)splitAt(s(N), cons(X, XS)) → U61(tt, N, X, XS)
tail(cons(N, XS)) → U71(tt, XS)take(N, XS) → U81(tt, N, XS)

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, fst, U64, U63, U62, U61, U42, U41, head, U21, U22, snd, cons, tail, splitAt, U71, U72, 0, s, U51, tt, take, U82, U52, U81, U11, U12, afterNth, U31, U32, sel, nil

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

U63#(tt, N, X, XS) → T(N)U63#(tt, N, X, XS) → U64#(splitAt(N, XS), X)
U22#(tt, X) → T(X)U63#(tt, N, X, XS) → T(XS)
U21#(tt, X) → U22#(tt, X)U64#(pair(YS, ZS), X) → T(X)
U11#(tt, N, XS) → U12#(tt, N, XS)U82#(tt, N, XS) → T(N)
U63#(tt, N, X, XS) → splitAt#(N, XS)U42#(tt, N, XS) → T(N)
U41#(tt, N, XS) → U42#(tt, N, XS)U82#(tt, N, XS) → fst#(splitAt(N, XS))
U62#(tt, N, X, XS) → U63#(tt, N, X, XS)U42#(tt, N, XS) → head#(afterNth(N, XS))
head#(cons(N, XS)) → U31#(tt, N)U51#(tt, Y) → U52#(tt, Y)
T(s(x_1)) → T(x_1)U12#(tt, N, XS) → splitAt#(N, XS)
fst#(pair(X, Y)) → U21#(tt, X)afterNth#(N, XS) → U11#(tt, N, XS)
snd#(pair(X, Y)) → U51#(tt, Y)U61#(tt, N, X, XS) → U62#(tt, N, X, XS)
T(natsFrom(x_1)) → T(x_1)U12#(tt, N, XS) → T(XS)
U72#(tt, XS) → T(XS)U12#(tt, N, XS) → snd#(splitAt(N, XS))
U12#(tt, N, XS) → T(N)T(natsFrom(s(N))) → natsFrom#(s(N))
U32#(tt, N) → T(N)U42#(tt, N, XS) → T(XS)
U82#(tt, N, XS) → splitAt#(N, XS)splitAt#(s(N), cons(X, XS)) → U61#(tt, N, X, XS)
U31#(tt, N) → U32#(tt, N)U81#(tt, N, XS) → U82#(tt, N, XS)
U42#(tt, N, XS) → afterNth#(N, XS)U52#(tt, Y) → T(Y)
take#(N, XS) → U81#(tt, N, XS)U71#(tt, XS) → U72#(tt, XS)
tail#(cons(N, XS)) → U71#(tt, XS)U82#(tt, N, XS) → T(XS)
sel#(N, XS) → U41#(tt, N, XS)

Rewrite Rules

U11(tt, N, XS) → U12(tt, N, XS)U12(tt, N, XS) → snd(splitAt(N, XS))
U21(tt, X) → U22(tt, X)U22(tt, X) → X
U31(tt, N) → U32(tt, N)U32(tt, N) → N
U41(tt, N, XS) → U42(tt, N, XS)U42(tt, N, XS) → head(afterNth(N, XS))
U51(tt, Y) → U52(tt, Y)U52(tt, Y) → Y
U61(tt, N, X, XS) → U62(tt, N, X, XS)U62(tt, N, X, XS) → U63(tt, N, X, XS)
U63(tt, N, X, XS) → U64(splitAt(N, XS), X)U64(pair(YS, ZS), X) → pair(cons(X, YS), ZS)
U71(tt, XS) → U72(tt, XS)U72(tt, XS) → XS
U81(tt, N, XS) → U82(tt, N, XS)U82(tt, N, XS) → fst(splitAt(N, XS))
afterNth(N, XS) → U11(tt, N, XS)fst(pair(X, Y)) → U21(tt, X)
head(cons(N, XS)) → U31(tt, N)natsFrom(N) → cons(N, natsFrom(s(N)))
sel(N, XS) → U41(tt, N, XS)snd(pair(X, Y)) → U51(tt, Y)
splitAt(0, XS) → pair(nil, XS)splitAt(s(N), cons(X, XS)) → U61(tt, N, X, XS)
tail(cons(N, XS)) → U71(tt, XS)take(N, XS) → U81(tt, N, XS)

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, U64, fst, U63, U62, U61, U42, U41, head, U21, snd, U22, cons, tail, splitAt, U71, U72, 0, s, U51, tt, take, U82, U81, U52, U11, U12, U31, afterNth, U32, sel, nil

Strategy

Context-sensitive strategy:
μ(0) = μ(T) = μ(tt) = μ(nil) = ∅
μ(natsFrom#) = μ(U11#) = μ(fst#) = μ(U31#) = μ(natsFrom) = μ(U21#) = μ(U62#) = μ(tail#) = μ(U52#) = μ(U64) = μ(fst) = μ(U63) = μ(U62) = μ(U41#) = μ(U61) = μ(U72#) = μ(snd#) = μ(head) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U61#) = μ(U51#) = μ(tail) = μ(U71) = μ(U72) = μ(U42#) = μ(U71#) = μ(U32#) = μ(U31) = μ(U32) = μ(U64#) = μ(U81#) = μ(U42) = μ(U41) = μ(cons) = μ(snd) = μ(U63#) = μ(U82#) = μ(U51) = μ(s) = μ(U82) = μ(U81) = μ(U52) = μ(U11) = μ(U12) = μ(head#) = {1}
μ(sel#) = μ(take#) = μ(splitAt#) = μ(pair) = μ(splitAt) = μ(afterNth#) = μ(take) = μ(afterNth) = μ(sel) = {1, 2}

The following SCCs where found

U63#(tt, N, X, XS) → splitAt#(N, XS)U62#(tt, N, X, XS) → U63#(tt, N, X, XS)
splitAt#(s(N), cons(X, XS)) → U61#(tt, N, X, XS)U61#(tt, N, X, XS) → U62#(tt, N, X, XS)
T(natsFrom(x_1)) → T(x_1)T(s(x_1)) → T(x_1)

Problem 3: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(natsFrom(x_1)) → T(x_1)T(s(x_1)) → T(x_1)

Rewrite Rules

U11(tt, N, XS) → U12(tt, N, XS)U12(tt, N, XS) → snd(splitAt(N, XS))
U21(tt, X) → U22(tt, X)U22(tt, X) → X
U31(tt, N) → U32(tt, N)U32(tt, N) → N
U41(tt, N, XS) → U42(tt, N, XS)U42(tt, N, XS) → head(afterNth(N, XS))
U51(tt, Y) → U52(tt, Y)U52(tt, Y) → Y
U61(tt, N, X, XS) → U62(tt, N, X, XS)U62(tt, N, X, XS) → U63(tt, N, X, XS)
U63(tt, N, X, XS) → U64(splitAt(N, XS), X)U64(pair(YS, ZS), X) → pair(cons(X, YS), ZS)
U71(tt, XS) → U72(tt, XS)U72(tt, XS) → XS
U81(tt, N, XS) → U82(tt, N, XS)U82(tt, N, XS) → fst(splitAt(N, XS))
afterNth(N, XS) → U11(tt, N, XS)fst(pair(X, Y)) → U21(tt, X)
head(cons(N, XS)) → U31(tt, N)natsFrom(N) → cons(N, natsFrom(s(N)))
sel(N, XS) → U41(tt, N, XS)snd(pair(X, Y)) → U51(tt, Y)
splitAt(0, XS) → pair(nil, XS)splitAt(s(N), cons(X, XS)) → U61(tt, N, X, XS)
tail(cons(N, XS)) → U71(tt, XS)take(N, XS) → U81(tt, N, XS)

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, U64, fst, U63, U62, U61, U42, U41, head, U21, snd, U22, cons, tail, splitAt, U71, U72, 0, s, U51, tt, take, U82, U81, U52, U11, U12, U31, afterNth, U32, sel, nil

Strategy

Context-sensitive strategy:
μ(0) = μ(T) = μ(tt) = μ(nil) = ∅
μ(natsFrom#) = μ(U11#) = μ(fst#) = μ(U31#) = μ(natsFrom) = μ(U21#) = μ(U62#) = μ(tail#) = μ(U52#) = μ(U64) = μ(fst) = μ(U63) = μ(U41#) = μ(U62) = μ(U61) = μ(snd#) = μ(U72#) = μ(head) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U61#) = μ(U51#) = μ(tail) = μ(U71) = μ(U72) = μ(U42#) = μ(U71#) = μ(U32#) = μ(U31) = μ(U32) = μ(U64#) = μ(U81#) = μ(U42) = μ(U41) = μ(cons) = μ(snd) = μ(U63#) = μ(U82#) = μ(s) = μ(U51) = μ(U82) = μ(U52) = μ(U81) = μ(U11) = μ(U12) = μ(head#) = {1}
μ(sel#) = μ(take#) = μ(splitAt#) = μ(pair) = μ(splitAt) = μ(afterNth#) = μ(take) = μ(afterNth) = μ(sel) = {1, 2}

Polynomial Interpretation

There are no usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

T(s(x_1)) → T(x_1)

Problem 4: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(natsFrom(x_1)) → T(x_1)

Rewrite Rules

U11(tt, N, XS) → U12(tt, N, XS)U12(tt, N, XS) → snd(splitAt(N, XS))
U21(tt, X) → U22(tt, X)U22(tt, X) → X
U31(tt, N) → U32(tt, N)U32(tt, N) → N
U41(tt, N, XS) → U42(tt, N, XS)U42(tt, N, XS) → head(afterNth(N, XS))
U51(tt, Y) → U52(tt, Y)U52(tt, Y) → Y
U61(tt, N, X, XS) → U62(tt, N, X, XS)U62(tt, N, X, XS) → U63(tt, N, X, XS)
U63(tt, N, X, XS) → U64(splitAt(N, XS), X)U64(pair(YS, ZS), X) → pair(cons(X, YS), ZS)
U71(tt, XS) → U72(tt, XS)U72(tt, XS) → XS
U81(tt, N, XS) → U82(tt, N, XS)U82(tt, N, XS) → fst(splitAt(N, XS))
afterNth(N, XS) → U11(tt, N, XS)fst(pair(X, Y)) → U21(tt, X)
head(cons(N, XS)) → U31(tt, N)natsFrom(N) → cons(N, natsFrom(s(N)))
sel(N, XS) → U41(tt, N, XS)snd(pair(X, Y)) → U51(tt, Y)
splitAt(0, XS) → pair(nil, XS)splitAt(s(N), cons(X, XS)) → U61(tt, N, X, XS)
tail(cons(N, XS)) → U71(tt, XS)take(N, XS) → U81(tt, N, XS)

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, fst, U64, U63, U62, U61, U42, U41, head, U21, U22, snd, cons, tail, splitAt, U71, U72, 0, s, U51, tt, take, U82, U52, U81, U11, U12, afterNth, U31, U32, sel, nil

Strategy

Context-sensitive strategy:
μ(0) = μ(T) = μ(tt) = μ(nil) = ∅
μ(natsFrom#) = μ(U11#) = μ(fst#) = μ(U31#) = μ(natsFrom) = μ(U21#) = μ(U62#) = μ(tail#) = μ(U52#) = μ(U64) = μ(fst) = μ(U63) = μ(U62) = μ(U41#) = μ(U61) = μ(U72#) = μ(snd#) = μ(head) = μ(U21) = μ(U22) = μ(U12#) = μ(U22#) = μ(U61#) = μ(U51#) = μ(tail) = μ(U71) = μ(U72) = μ(U42#) = μ(U71#) = μ(U32#) = μ(U31) = μ(U32) = μ(U64#) = μ(U81#) = μ(U42) = μ(U41) = μ(cons) = μ(snd) = μ(U63#) = μ(U82#) = μ(U51) = μ(s) = μ(U82) = μ(U81) = μ(U52) = μ(U11) = μ(U12) = μ(head#) = {1}
μ(sel#) = μ(take#) = μ(splitAt#) = μ(pair) = μ(splitAt) = μ(afterNth#) = μ(take) = μ(afterNth) = μ(sel) = {1, 2}

Polynomial Interpretation

There are no usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

T(natsFrom(x_1)) → T(x_1)