The TRS could not be proven terminating. The proof attempt took 60000 ms.
Problem 1 remains open; application of the following processors failed [DependencyGraph (114ms), SubtermCriterion (1ms), DependencyGraph (72ms), PolynomialLinearRange4iUR (3296ms), DependencyGraph (73ms), PolynomialLinearRange8NegiUR (timeout), PolynomialLinearRange8NegiUR (-2ms), ReductionPairSAT (2207ms), DependencyGraph (60ms), SizeChangePrinciple (timeout)].
| a__sel#(0, cons(X, Y)) | → | mark#(X) | mark#(g(X)) | → | mark#(X) | |
| a__sel#(s(X), cons(Y, Z)) | → | mark#(Z) | a__sel#(s(X), cons(Y, Z)) | → | a__sel#(mark(X), mark(Z)) | |
| mark#(cons(X1, X2)) | → | mark#(X1) | mark#(f(X)) | → | a__f#(mark(X)) | |
| a__g#(s(X)) | → | mark#(X) | mark#(f(X)) | → | mark#(X) | |
| mark#(g(X)) | → | a__g#(mark(X)) | a__g#(s(X)) | → | a__g#(mark(X)) | |
| mark#(sel(X1, X2)) | → | a__sel#(mark(X1), mark(X2)) | mark#(sel(X1, X2)) | → | mark#(X2) | |
| a__f#(X) | → | mark#(X) | mark#(s(X)) | → | mark#(X) | |
| mark#(sel(X1, X2)) | → | mark#(X1) | a__sel#(s(X), cons(Y, Z)) | → | mark#(X) |
| a__f(X) | → | cons(mark(X), f(g(X))) | a__g(0) | → | s(0) | |
| a__g(s(X)) | → | s(s(a__g(mark(X)))) | a__sel(0, cons(X, Y)) | → | mark(X) | |
| a__sel(s(X), cons(Y, Z)) | → | a__sel(mark(X), mark(Z)) | mark(f(X)) | → | a__f(mark(X)) | |
| mark(g(X)) | → | a__g(mark(X)) | mark(sel(X1, X2)) | → | a__sel(mark(X1), mark(X2)) | |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | mark(0) | → | 0 | |
| mark(s(X)) | → | s(mark(X)) | a__f(X) | → | f(X) | |
| a__g(X) | → | g(X) | a__sel(X1, X2) | → | sel(X1, X2) |
Termination of terms over the following signature is verified: f, g, 0, s, a__sel, mark, sel, a__g, a__f, cons