TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (104ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (2ms), PolynomialLinearRange4iUR (0ms), DependencyGraph (1ms), PolynomialOrderingProcessor (0ms), DependencyGraph (4ms), PolynomialLinearRange4 (190ms), DependencyGraph (1ms), PolynomialLinearRange4 (102ms), DependencyGraph (4ms), PolynomialLinearRange4 (97ms), DependencyGraph (5ms), ReductionPairSAT (234ms), DependencyGraph (0ms), SizeChangePrinciple (timeout)].
 | – Problem 3 was processed with processor PolynomialLinearRange4 (105ms).
 |    | – Problem 4 was processed with processor PolynomialLinearRange4 (86ms).

The following open problems remain:

Open Dependency Pair Problem 2

Dependency Pairs

splitAt#(s(N), cons(X, XS)) → splitAt#(N, XS)

Rewrite Rules

natsFrom(N) → cons(N, natsFrom(s(N)))fst(pair(XS, YS)) → XS
snd(pair(XS, YS)) → YSsplitAt(0, XS) → pair(nil, XS)
splitAt(s(N), cons(X, XS)) → u(splitAt(N, XS), N, X, XS)u(pair(YS, ZS), N, X, XS) → pair(cons(X, YS), ZS)
head(cons(N, XS)) → Ntail(cons(N, XS)) → XS
sel(N, XS) → head(afterNth(N, XS))take(N, XS) → fst(splitAt(N, XS))
afterNth(N, XS) → snd(splitAt(N, XS))

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, tail, splitAt, fst, u, 0, s, take, afterNth, head, sel, cons, snd, nil

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

T(natsFrom(x_1)) → T(x_1)splitAt#(s(N), cons(X, XS)) → T(XS)
afterNth#(N, XS) → snd#(splitAt(N, XS))splitAt#(s(N), cons(X, XS)) → splitAt#(N, XS)
sel#(N, XS) → afterNth#(N, XS)T(natsFrom(s(N))) → natsFrom#(s(N))
sel#(N, XS) → head#(afterNth(N, XS))take#(N, XS) → splitAt#(N, XS)
take#(N, XS) → fst#(splitAt(N, XS))afterNth#(N, XS) → splitAt#(N, XS)
u#(pair(YS, ZS), N, X, XS) → T(X)splitAt#(s(N), cons(X, XS)) → u#(splitAt(N, XS), N, X, XS)
tail#(cons(N, XS)) → T(XS)T(s(x_1)) → T(x_1)

Rewrite Rules

natsFrom(N) → cons(N, natsFrom(s(N)))fst(pair(XS, YS)) → XS
snd(pair(XS, YS)) → YSsplitAt(0, XS) → pair(nil, XS)
splitAt(s(N), cons(X, XS)) → u(splitAt(N, XS), N, X, XS)u(pair(YS, ZS), N, X, XS) → pair(cons(X, YS), ZS)
head(cons(N, XS)) → Ntail(cons(N, XS)) → XS
sel(N, XS) → head(afterNth(N, XS))take(N, XS) → fst(splitAt(N, XS))
afterNth(N, XS) → snd(splitAt(N, XS))

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, tail, splitAt, fst, u, 0, s, take, afterNth, head, sel, nil, snd, cons

Strategy

Context-sensitive strategy:
μ(T) = μ(0) = μ(nil) = ∅
μ(natsFrom#) = μ(fst#) = μ(natsFrom) = μ(tail#) = μ(fst) = μ(snd#) = μ(head) = μ(snd) = μ(cons) = μ(tail) = μ(u) = μ(s) = μ(u#) = μ(head#) = {1}
μ(pair) = μ(sel#) = μ(take#) = μ(splitAt) = μ(afterNth#) = μ(splitAt#) = μ(take) = μ(afterNth) = μ(sel) = {1, 2}

The following SCCs where found

splitAt#(s(N), cons(X, XS)) → splitAt#(N, 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

natsFrom(N) → cons(N, natsFrom(s(N)))fst(pair(XS, YS)) → XS
snd(pair(XS, YS)) → YSsplitAt(0, XS) → pair(nil, XS)
splitAt(s(N), cons(X, XS)) → u(splitAt(N, XS), N, X, XS)u(pair(YS, ZS), N, X, XS) → pair(cons(X, YS), ZS)
head(cons(N, XS)) → Ntail(cons(N, XS)) → XS
sel(N, XS) → head(afterNth(N, XS))take(N, XS) → fst(splitAt(N, XS))
afterNth(N, XS) → snd(splitAt(N, XS))

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, tail, splitAt, fst, u, 0, s, take, afterNth, head, sel, nil, snd, cons

Strategy

Context-sensitive strategy:
μ(T) = μ(0) = μ(nil) = ∅
μ(natsFrom#) = μ(fst#) = μ(natsFrom) = μ(tail#) = μ(fst) = μ(snd#) = μ(head) = μ(cons) = μ(snd) = μ(tail) = μ(u) = μ(s) = μ(u#) = μ(head#) = {1}
μ(pair) = μ(sel#) = μ(take#) = μ(splitAt) = μ(afterNth#) = μ(splitAt#) = μ(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)

Problem 4: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

natsFrom(N) → cons(N, natsFrom(s(N)))fst(pair(XS, YS)) → XS
snd(pair(XS, YS)) → YSsplitAt(0, XS) → pair(nil, XS)
splitAt(s(N), cons(X, XS)) → u(splitAt(N, XS), N, X, XS)u(pair(YS, ZS), N, X, XS) → pair(cons(X, YS), ZS)
head(cons(N, XS)) → Ntail(cons(N, XS)) → XS
sel(N, XS) → head(afterNth(N, XS))take(N, XS) → fst(splitAt(N, XS))
afterNth(N, XS) → snd(splitAt(N, XS))

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, tail, splitAt, fst, u, 0, s, take, afterNth, head, sel, cons, snd, nil

Strategy

Context-sensitive strategy:
μ(T) = μ(0) = μ(nil) = ∅
μ(natsFrom#) = μ(fst#) = μ(natsFrom) = μ(tail#) = μ(fst) = μ(snd#) = μ(head) = μ(snd) = μ(cons) = μ(tail) = μ(u) = μ(s) = μ(u#) = μ(head#) = {1}
μ(pair) = μ(sel#) = μ(take#) = μ(splitAt) = μ(afterNth#) = μ(splitAt#) = μ(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)