The TRS could not be proven terminating. The proof attempt took 60017 ms.
Problem 1 remains open; application of the following processors failed [DependencyGraph (2582ms), SubtermCriterion (2ms), DependencyGraph (2398ms), PolynomialLinearRange4iUR (timeout), DependencyGraph (2089ms), PolynomialLinearRange8NegiUR (timeout), DependencyGraph (2050ms), ReductionPairSAT (timeout)].
| a__pi#(X) | → | a__2ndspos#(mark(X), a__from(0)) | a__2ndsneg#(s(N), cons2(X, cons(Y, Z))) | → | a__2ndspos#(mark(N), mark(Z)) | |
| mark#(from(X)) | → | a__from#(mark(X)) | mark#(2ndspos(X1, X2)) | → | mark#(X2) | |
| mark#(square(X)) | → | mark#(X) | a__2ndsneg#(s(N), cons2(X, cons(Y, Z))) | → | mark#(Z) | |
| a__2ndspos#(s(N), cons2(X, cons(Y, Z))) | → | a__2ndsneg#(mark(N), mark(Z)) | mark#(pi(X)) | → | mark#(X) | |
| a__2ndsneg#(s(N), cons(X, Z)) | → | mark#(Z) | mark#(cons2(X1, X2)) | → | mark#(X2) | |
| mark#(pi(X)) | → | a__pi#(mark(X)) | mark#(times(X1, X2)) | → | mark#(X2) | |
| mark#(negrecip(X)) | → | mark#(X) | mark#(2ndsneg(X1, X2)) | → | mark#(X1) | |
| a__times#(s(X), Y) | → | a__plus#(mark(Y), a__times(mark(X), mark(Y))) | mark#(times(X1, X2)) | → | mark#(X1) | |
| mark#(2ndsneg(X1, X2)) | → | mark#(X2) | mark#(2ndsneg(X1, X2)) | → | a__2ndsneg#(mark(X1), mark(X2)) | |
| mark#(s(X)) | → | mark#(X) | a__2ndspos#(s(N), cons2(X, cons(Y, Z))) | → | mark#(Y) | |
| a__pi#(X) | → | mark#(X) | a__2ndsneg#(s(N), cons2(X, cons(Y, Z))) | → | mark#(N) | |
| a__2ndspos#(s(N), cons(X, Z)) | → | mark#(Z) | mark#(rcons(X1, X2)) | → | mark#(X2) | |
| mark#(plus(X1, X2)) | → | a__plus#(mark(X1), mark(X2)) | a__2ndspos#(s(N), cons2(X, cons(Y, Z))) | → | mark#(N) | |
| mark#(from(X)) | → | mark#(X) | mark#(cons(X1, X2)) | → | mark#(X1) | |
| mark#(plus(X1, X2)) | → | mark#(X1) | a__plus#(s(X), Y) | → | mark#(Y) | |
| a__2ndsneg#(s(N), cons(X, Z)) | → | a__2ndsneg#(s(mark(N)), cons2(X, mark(Z))) | mark#(posrecip(X)) | → | mark#(X) | |
| a__2ndsneg#(s(N), cons(X, Z)) | → | mark#(N) | mark#(times(X1, X2)) | → | a__times#(mark(X1), mark(X2)) | |
| a__2ndspos#(s(N), cons(X, Z)) | → | mark#(N) | a__from#(X) | → | mark#(X) | |
| a__2ndspos#(s(N), cons2(X, cons(Y, Z))) | → | mark#(Z) | mark#(square(X)) | → | a__square#(mark(X)) | |
| a__times#(s(X), Y) | → | mark#(X) | mark#(plus(X1, X2)) | → | mark#(X2) | |
| mark#(2ndspos(X1, X2)) | → | a__2ndspos#(mark(X1), mark(X2)) | a__plus#(0, Y) | → | mark#(Y) | |
| a__square#(X) | → | mark#(X) | a__2ndspos#(s(N), cons(X, Z)) | → | a__2ndspos#(s(mark(N)), cons2(X, mark(Z))) | |
| a__times#(s(X), Y) | → | a__times#(mark(X), mark(Y)) | a__2ndsneg#(s(N), cons2(X, cons(Y, Z))) | → | mark#(Y) | |
| a__pi#(X) | → | a__from#(0) | a__times#(s(X), Y) | → | mark#(Y) | |
| a__plus#(s(X), Y) | → | mark#(X) | a__plus#(s(X), Y) | → | a__plus#(mark(X), mark(Y)) | |
| a__square#(X) | → | a__times#(mark(X), mark(X)) | mark#(2ndspos(X1, X2)) | → | mark#(X1) | |
| mark#(rcons(X1, X2)) | → | mark#(X1) |
| a__from(X) | → | cons(mark(X), from(s(X))) | a__2ndspos(0, Z) | → | rnil | |
| a__2ndspos(s(N), cons(X, Z)) | → | a__2ndspos(s(mark(N)), cons2(X, mark(Z))) | a__2ndspos(s(N), cons2(X, cons(Y, Z))) | → | rcons(posrecip(mark(Y)), a__2ndsneg(mark(N), mark(Z))) | |
| a__2ndsneg(0, Z) | → | rnil | a__2ndsneg(s(N), cons(X, Z)) | → | a__2ndsneg(s(mark(N)), cons2(X, mark(Z))) | |
| a__2ndsneg(s(N), cons2(X, cons(Y, Z))) | → | rcons(negrecip(mark(Y)), a__2ndspos(mark(N), mark(Z))) | a__pi(X) | → | a__2ndspos(mark(X), a__from(0)) | |
| a__plus(0, Y) | → | mark(Y) | a__plus(s(X), Y) | → | s(a__plus(mark(X), mark(Y))) | |
| a__times(0, Y) | → | 0 | a__times(s(X), Y) | → | a__plus(mark(Y), a__times(mark(X), mark(Y))) | |
| a__square(X) | → | a__times(mark(X), mark(X)) | mark(from(X)) | → | a__from(mark(X)) | |
| mark(2ndspos(X1, X2)) | → | a__2ndspos(mark(X1), mark(X2)) | mark(2ndsneg(X1, X2)) | → | a__2ndsneg(mark(X1), mark(X2)) | |
| mark(pi(X)) | → | a__pi(mark(X)) | mark(plus(X1, X2)) | → | a__plus(mark(X1), mark(X2)) | |
| mark(times(X1, X2)) | → | a__times(mark(X1), mark(X2)) | mark(square(X)) | → | a__square(mark(X)) | |
| mark(0) | → | 0 | mark(s(X)) | → | s(mark(X)) | |
| mark(posrecip(X)) | → | posrecip(mark(X)) | mark(negrecip(X)) | → | negrecip(mark(X)) | |
| mark(nil) | → | nil | mark(cons(X1, X2)) | → | cons(mark(X1), X2) | |
| mark(cons2(X1, X2)) | → | cons2(X1, mark(X2)) | mark(rnil) | → | rnil | |
| mark(rcons(X1, X2)) | → | rcons(mark(X1), mark(X2)) | a__from(X) | → | from(X) | |
| a__2ndspos(X1, X2) | → | 2ndspos(X1, X2) | a__2ndsneg(X1, X2) | → | 2ndsneg(X1, X2) | |
| a__pi(X) | → | pi(X) | a__plus(X1, X2) | → | plus(X1, X2) | |
| a__times(X1, X2) | → | times(X1, X2) | a__square(X) | → | square(X) |
Termination of terms over the following signature is verified: plus, a__square, posrecip, negrecip, cons2, a__pi, rnil, a__2ndspos, a__plus, mark, a__2ndsneg, from, rcons, 2ndspos, 0, s, times, 2ndsneg, square, a__times, pi, a__from, nil, cons