The TRS could not be proven terminating. The proof attempt took 60005 ms.
Problem 1 remains open; application of the following processors failed [DependencyGraph (3652ms), SubtermCriterion (1ms), DependencyGraph (2988ms), PolynomialLinearRange4iUR (timeout), DependencyGraph (2905ms), PolynomialLinearRange8NegiUR (timeout), DependencyGraph (2948ms), ReductionPairSAT (timeout)].
| mark#(from(X)) | → | a__from#(mark(X)) | a__sel#(s(X), cons(Y, Z)) | → | mark#(Z) | |
| a__quote1#(cons(X, Z)) | → | a__quote#(X) | mark#(cons1(X1, X2)) | → | mark#(X1) | |
| a__unquote1#(cons1(X, Z)) | → | mark#(Z) | a__unquote1#(cons1(X, Z)) | → | a__fcons#(a__unquote(mark(X)), a__unquote1(mark(Z))) | |
| a__first1#(s(X), cons(Y, Z)) | → | mark#(Z) | a__first#(s(X), cons(Y, Z)) | → | mark#(Y) | |
| mark#(unquote(X)) | → | mark#(X) | mark#(quote1(X)) | → | a__quote1#(X) | |
| mark#(s(X)) | → | mark#(X) | a__unquote1#(cons1(X, Z)) | → | mark#(X) | |
| mark#(sel(X1, X2)) | → | mark#(X1) | mark#(sel1(X1, X2)) | → | a__sel1#(mark(X1), mark(X2)) | |
| a__sel1#(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__sel1#(s(X), cons(Y, Z)) | → | mark#(X) | mark#(unquote1(X)) | → | a__unquote1#(mark(X)) | |
| a__unquote1#(cons1(X, Z)) | → | a__unquote#(mark(X)) | a__quote#(s(X)) | → | a__quote#(X) | |
| mark#(first(X1, X2)) | → | mark#(X1) | mark#(unquote(X)) | → | a__unquote#(mark(X)) | |
| a__fcons#(X, Z) | → | mark#(X) | a__sel#(0, cons(X, Z)) | → | mark#(X) | |
| a__first1#(s(X), cons(Y, Z)) | → | mark#(X) | a__from#(X) | → | mark#(X) | |
| mark#(first(X1, X2)) | → | a__first#(mark(X1), mark(X2)) | mark#(unquote1(X)) | → | mark#(X) | |
| a__unquote1#(cons1(X, Z)) | → | a__unquote1#(mark(Z)) | mark#(first1(X1, X2)) | → | mark#(X1) | |
| a__quote#(sel(X, Z)) | → | mark#(Z) | a__sel1#(0, cons(X, Z)) | → | a__quote#(X) | |
| a__first1#(s(X), cons(Y, Z)) | → | a__quote#(Y) | a__first1#(s(X), cons(Y, Z)) | → | a__first1#(mark(X), mark(Z)) | |
| a__quote1#(cons(X, Z)) | → | a__quote1#(Z) | mark#(sel(X1, X2)) | → | mark#(X2) | |
| mark#(first1(X1, X2)) | → | mark#(X2) | mark#(first(X1, X2)) | → | mark#(X2) | |
| mark#(fcons(X1, X2)) | → | mark#(X2) | mark#(fcons(X1, X2)) | → | mark#(X1) | |
| a__quote#(sel(X, Z)) | → | mark#(X) | mark#(sel1(X1, X2)) | → | mark#(X2) | |
| mark#(fcons(X1, X2)) | → | a__fcons#(mark(X1), mark(X2)) | a__quote1#(first(X, Z)) | → | a__first1#(mark(X), mark(Z)) | |
| mark#(cons1(X1, X2)) | → | mark#(X2) | mark#(quote(X)) | → | a__quote#(X) | |
| mark#(s1(X)) | → | mark#(X) | a__sel1#(s(X), cons(Y, Z)) | → | a__sel1#(mark(X), mark(Z)) | |
| mark#(first1(X1, X2)) | → | a__first1#(mark(X1), mark(X2)) | a__unquote#(s1(X)) | → | mark#(X) | |
| mark#(sel(X1, X2)) | → | a__sel#(mark(X1), mark(X2)) | a__quote1#(first(X, Z)) | → | mark#(Z) | |
| a__quote1#(first(X, Z)) | → | mark#(X) | a__quote#(sel(X, Z)) | → | a__sel1#(mark(X), mark(Z)) | |
| a__unquote#(s1(X)) | → | a__unquote#(mark(X)) | a__sel#(s(X), cons(Y, Z)) | → | mark#(X) | |
| mark#(sel1(X1, X2)) | → | mark#(X1) |
| a__sel(s(X), cons(Y, Z)) | → | a__sel(mark(X), mark(Z)) | a__sel(0, cons(X, Z)) | → | mark(X) | |
| a__first(0, Z) | → | nil | a__first(s(X), cons(Y, Z)) | → | cons(mark(Y), first(X, Z)) | |
| a__from(X) | → | cons(mark(X), from(s(X))) | a__sel1(s(X), cons(Y, Z)) | → | a__sel1(mark(X), mark(Z)) | |
| a__sel1(0, cons(X, Z)) | → | a__quote(X) | a__first1(0, Z) | → | nil1 | |
| a__first1(s(X), cons(Y, Z)) | → | cons1(a__quote(Y), a__first1(mark(X), mark(Z))) | a__quote(0) | → | 01 | |
| a__quote1(cons(X, Z)) | → | cons1(a__quote(X), a__quote1(Z)) | a__quote1(nil) | → | nil1 | |
| a__quote(s(X)) | → | s1(a__quote(X)) | a__quote(sel(X, Z)) | → | a__sel1(mark(X), mark(Z)) | |
| a__quote1(first(X, Z)) | → | a__first1(mark(X), mark(Z)) | a__unquote(01) | → | 0 | |
| a__unquote(s1(X)) | → | s(a__unquote(mark(X))) | a__unquote1(nil1) | → | nil | |
| a__unquote1(cons1(X, Z)) | → | a__fcons(a__unquote(mark(X)), a__unquote1(mark(Z))) | a__fcons(X, Z) | → | cons(mark(X), Z) | |
| mark(sel(X1, X2)) | → | a__sel(mark(X1), mark(X2)) | mark(first(X1, X2)) | → | a__first(mark(X1), mark(X2)) | |
| mark(from(X)) | → | a__from(mark(X)) | mark(sel1(X1, X2)) | → | a__sel1(mark(X1), mark(X2)) | |
| mark(quote(X)) | → | a__quote(X) | mark(first1(X1, X2)) | → | a__first1(mark(X1), mark(X2)) | |
| mark(quote1(X)) | → | a__quote1(X) | mark(unquote(X)) | → | a__unquote(mark(X)) | |
| mark(unquote1(X)) | → | a__unquote1(mark(X)) | mark(fcons(X1, X2)) | → | a__fcons(mark(X1), mark(X2)) | |
| mark(s(X)) | → | s(mark(X)) | mark(cons(X1, X2)) | → | cons(mark(X1), X2) | |
| mark(0) | → | 0 | mark(nil) | → | nil | |
| mark(nil1) | → | nil1 | mark(cons1(X1, X2)) | → | cons1(mark(X1), mark(X2)) | |
| mark(01) | → | 01 | mark(s1(X)) | → | s1(mark(X)) | |
| a__sel(X1, X2) | → | sel(X1, X2) | a__first(X1, X2) | → | first(X1, X2) | |
| a__from(X) | → | from(X) | a__sel1(X1, X2) | → | sel1(X1, X2) | |
| a__quote(X) | → | quote(X) | a__first1(X1, X2) | → | first1(X1, X2) | |
| a__quote1(X) | → | quote1(X) | a__unquote(X) | → | unquote(X) | |
| a__unquote1(X) | → | unquote1(X) | a__fcons(X1, X2) | → | fcons(X1, X2) |
Termination of terms over the following signature is verified: a__sel1, cons1, a__quote1, from, unquote, sel1, unquote1, quote, a__quote, cons, s1, a__first1, mark, fcons, 01, a__fcons, first1, quote1, 0, s, a__sel, nil1, first, a__first, sel, a__from, a__unquote, a__unquote1, nil