The TRS could not be proven terminating. The proof attempt took 60001 ms.
Problem 1 remains open; application of the following processors failed [DependencyGraph (81ms), SubtermCriterion (2ms), DependencyGraph (42ms), PolynomialLinearRange4iUR (2636ms), DependencyGraph (41ms), PolynomialLinearRange8NegiUR (28020ms), DependencyGraph (32ms), ReductionPairSAT (1142ms), DependencyGraph (36ms), SizeChangePrinciple (timeout)].
| a__from#(X) | → | mark#(X) | a__2nd#(cons(X, X1)) | → | mark#(X1) | |
| mark#(from(X)) | → | a__from#(mark(X)) | a__2nd#(cons(X, X1)) | → | mark#(X) | |
| mark#(from(X)) | → | mark#(X) | mark#(cons(X1, X2)) | → | mark#(X1) | |
| a__2nd#(cons(X, X1)) | → | a__2nd#(cons1(mark(X), mark(X1))) | mark#(cons1(X1, X2)) | → | mark#(X2) | |
| mark#(cons1(X1, X2)) | → | mark#(X1) | mark#(2nd(X)) | → | a__2nd#(mark(X)) | |
| a__2nd#(cons1(X, cons(Y, Z))) | → | mark#(Y) | mark#(s(X)) | → | mark#(X) | |
| mark#(2nd(X)) | → | mark#(X) |
| a__2nd(cons1(X, cons(Y, Z))) | → | mark(Y) | a__2nd(cons(X, X1)) | → | a__2nd(cons1(mark(X), mark(X1))) | |
| a__from(X) | → | cons(mark(X), from(s(X))) | mark(2nd(X)) | → | a__2nd(mark(X)) | |
| mark(from(X)) | → | a__from(mark(X)) | mark(cons(X1, X2)) | → | cons(mark(X1), X2) | |
| mark(s(X)) | → | s(mark(X)) | mark(cons1(X1, X2)) | → | cons1(mark(X1), mark(X2)) | |
| a__2nd(X) | → | 2nd(X) | a__from(X) | → | from(X) |
Termination of terms over the following signature is verified: 2nd, cons1, s, mark, from, a__2nd, a__from, cons