The TRS could not be proven terminating. The proof attempt took 60000 ms.
Problem 1 remains open; application of the following processors failed [DependencyGraph (120ms), SubtermCriterion (1ms), DependencyGraph (85ms), PolynomialLinearRange4iUR (5468ms), DependencyGraph (70ms), PolynomialLinearRange8NegiUR (timeout), DependencyGraph (84ms), ReductionPairSAT (2907ms), DependencyGraph (70ms), SizeChangePrinciple (timeout)].
| a__from#(X) | → | mark#(X) | mark#(first(X1, X2)) | → | mark#(X2) | |
| mark#(from(X)) | → | a__from#(mark(X)) | mark#(first(X1, X2)) | → | a__first#(mark(X1), mark(X2)) | |
| a__sel#(s(X), cons(Y, Z)) | → | mark#(Z) | a__sel#(s(X), cons(Y, Z)) | → | a__sel#(mark(X), mark(Z)) | |
| mark#(from(X)) | → | mark#(X) | mark#(cons(X1, X2)) | → | mark#(X1) | |
| a__first#(s(X), cons(Y, Z)) | → | mark#(Y) | mark#(sel(X1, X2)) | → | a__sel#(mark(X1), mark(X2)) | |
| mark#(sel(X1, X2)) | → | mark#(X2) | mark#(first(X1, X2)) | → | mark#(X1) | |
| mark#(s(X)) | → | mark#(X) | mark#(sel(X1, X2)) | → | mark#(X1) | |
| a__sel#(s(X), cons(Y, Z)) | → | mark#(X) | a__sel#(0, cons(X, Z)) | → | mark#(X) |
| a__from(X) | → | cons(mark(X), from(s(X))) | a__first(0, Z) | → | nil | |
| a__first(s(X), cons(Y, Z)) | → | cons(mark(Y), first(X, Z)) | a__sel(0, cons(X, Z)) | → | mark(X) | |
| a__sel(s(X), cons(Y, Z)) | → | a__sel(mark(X), mark(Z)) | mark(from(X)) | → | a__from(mark(X)) | |
| mark(first(X1, X2)) | → | a__first(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__first(X1, X2) | → | first(X1, X2) | |
| a__sel(X1, X2) | → | sel(X1, X2) |
Termination of terms over the following signature is verified: 0, s, a__sel, mark, from, sel, first, a__first, a__from, nil, cons