The TRS could not be proven terminating. The proof attempt took 60001 ms.
Problem 1 remains open; application of the following processors failed [DependencyGraph (277ms), SubtermCriterion (1ms), DependencyGraph (239ms), PolynomialLinearRange4iUR (timeout), PolynomialLinearRange4iUR (-2ms), PolynomialLinearRange8NegiUR (30007ms), ReductionPairSAT (4499ms), DependencyGraph (186ms), SizeChangePrinciple (timeout)].
| mark#(fib1(X1, X2)) | → | a__fib1#(mark(X1), mark(X2)) | a__sel#(s(N), cons(X, XS)) | → | mark#(N) | |
| a__fib#(N) | → | a__fib1#(s(0), s(0)) | mark#(sel(X1, X2)) | → | mark#(X2) | |
| a__fib#(N) | → | a__sel#(mark(N), a__fib1(s(0), s(0))) | mark#(add(X1, X2)) | → | mark#(X2) | |
| mark#(s(X)) | → | mark#(X) | a__add#(s(X), Y) | → | mark#(Y) | |
| mark#(sel(X1, X2)) | → | mark#(X1) | mark#(add(X1, X2)) | → | mark#(X1) | |
| a__add#(s(X), Y) | → | mark#(X) | mark#(add(X1, X2)) | → | a__add#(mark(X1), mark(X2)) | |
| mark#(cons(X1, X2)) | → | mark#(X1) | a__sel#(s(N), cons(X, XS)) | → | mark#(XS) | |
| mark#(fib1(X1, X2)) | → | mark#(X1) | a__add#(0, X) | → | mark#(X) | |
| mark#(fib(X)) | → | a__fib#(mark(X)) | mark#(fib1(X1, X2)) | → | mark#(X2) | |
| a__sel#(s(N), cons(X, XS)) | → | a__sel#(mark(N), mark(XS)) | a__sel#(0, cons(X, XS)) | → | mark#(X) | |
| mark#(sel(X1, X2)) | → | a__sel#(mark(X1), mark(X2)) | mark#(fib(X)) | → | mark#(X) | |
| a__fib1#(X, Y) | → | mark#(X) | a__add#(s(X), Y) | → | a__add#(mark(X), mark(Y)) | |
| a__fib#(N) | → | mark#(N) |
| a__fib(N) | → | a__sel(mark(N), a__fib1(s(0), s(0))) | a__fib1(X, Y) | → | cons(mark(X), fib1(Y, add(X, Y))) | |
| a__add(0, X) | → | mark(X) | a__add(s(X), Y) | → | s(a__add(mark(X), mark(Y))) | |
| a__sel(0, cons(X, XS)) | → | mark(X) | a__sel(s(N), cons(X, XS)) | → | a__sel(mark(N), mark(XS)) | |
| mark(fib(X)) | → | a__fib(mark(X)) | mark(sel(X1, X2)) | → | a__sel(mark(X1), mark(X2)) | |
| mark(fib1(X1, X2)) | → | a__fib1(mark(X1), mark(X2)) | mark(add(X1, X2)) | → | a__add(mark(X1), mark(X2)) | |
| mark(s(X)) | → | s(mark(X)) | mark(0) | → | 0 | |
| mark(cons(X1, X2)) | → | cons(mark(X1), X2) | a__fib(X) | → | fib(X) | |
| a__sel(X1, X2) | → | sel(X1, X2) | a__fib1(X1, X2) | → | fib1(X1, X2) | |
| a__add(X1, X2) | → | add(X1, X2) |
Termination of terms over the following signature is verified: a__fib, 0, s, a__fib1, a__sel, mark, a__add, fib1, add, sel, fib, cons