The TRS could not be proven terminating. The proof attempt took 60000 ms.
Problem 1 remains open; application of the following processors failed [DependencyGraph (288ms), SubtermCriterion (1ms), DependencyGraph (236ms), PolynomialLinearRange4iUR (timeout), DependencyGraph (175ms), PolynomialLinearRange8NegiUR (30000ms), ReductionPairSAT (7605ms), DependencyGraph (223ms), SizeChangePrinciple (timeout)].
| a__from#(X) | → | mark#(X) | mark#(take(X1, X2)) | → | mark#(X1) | |
| mark#(from(X)) | → | a__from#(mark(X)) | a__sel#(s(N), cons(X, XS)) | → | mark#(N) | |
| mark#(from(X)) | → | mark#(X) | mark#(cons(X1, X2)) | → | mark#(X1) | |
| a__2nd#(cons(X, XS)) | → | a__head#(mark(XS)) | a__sel#(s(N), cons(X, XS)) | → | mark#(XS) | |
| a__take#(s(N), cons(X, XS)) | → | mark#(X) | a__2nd#(cons(X, XS)) | → | mark#(XS) | |
| a__sel#(s(N), cons(X, XS)) | → | a__sel#(mark(N), mark(XS)) | a__sel#(0, cons(X, XS)) | → | mark#(X) | |
| mark#(head(X)) | → | mark#(X) | mark#(sel(X1, X2)) | → | a__sel#(mark(X1), mark(X2)) | |
| mark#(2nd(X)) | → | a__2nd#(mark(X)) | mark#(take(X1, X2)) | → | a__take#(mark(X1), mark(X2)) | |
| mark#(sel(X1, X2)) | → | mark#(X2) | mark#(head(X)) | → | a__head#(mark(X)) | |
| mark#(take(X1, X2)) | → | mark#(X2) | mark#(s(X)) | → | mark#(X) | |
| mark#(sel(X1, X2)) | → | mark#(X1) | mark#(2nd(X)) | → | mark#(X) | |
| a__head#(cons(X, XS)) | → | mark#(X) |
| a__from(X) | → | cons(mark(X), from(s(X))) | a__head(cons(X, XS)) | → | mark(X) | |
| a__2nd(cons(X, XS)) | → | a__head(mark(XS)) | a__take(0, XS) | → | nil | |
| a__take(s(N), cons(X, XS)) | → | cons(mark(X), take(N, XS)) | a__sel(0, cons(X, XS)) | → | mark(X) | |
| a__sel(s(N), cons(X, XS)) | → | a__sel(mark(N), mark(XS)) | mark(from(X)) | → | a__from(mark(X)) | |
| mark(head(X)) | → | a__head(mark(X)) | mark(2nd(X)) | → | a__2nd(mark(X)) | |
| mark(take(X1, X2)) | → | a__take(mark(X1), mark(X2)) | mark(sel(X1, X2)) | → | a__sel(mark(X1), mark(X2)) | |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | mark(s(X)) | → | s(mark(X)) | |
| mark(0) | → | 0 | mark(nil) | → | nil | |
| a__from(X) | → | from(X) | a__head(X) | → | head(X) | |
| a__2nd(X) | → | 2nd(X) | a__take(X1, X2) | → | take(X1, X2) | |
| a__sel(X1, X2) | → | sel(X1, X2) |
Termination of terms over the following signature is verified: 2nd, a__take, mark, from, 0, s, take, a__sel, a__head, a__2nd, head, sel, a__from, cons, nil