TIMEOUT
The TRS could not be proven terminating. The proof attempt took 60023 ms.
The following DP Processors were used
Problem 1 was processed with processor PolynomialLinearRange4iUR (2248ms).
| – Problem 2 remains open; application of the following processors failed [DependencyGraph (3ms), PolynomialLinearRange4iUR (1284ms), DependencyGraph (3ms), PolynomialLinearRange8NegiUR (24702ms), DependencyGraph (2ms), ReductionPairSAT (timeout)].
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| f#(a(x), a(y)) | → | a#(f(x, y)) | | f#(b(x), b(y)) | → | f#(x, y) |
| f#(a(x), a(y)) | → | f#(x, y) | | a#(a(f(x, y))) | → | f#(a(b(a(b(a(x))))), a(b(a(b(a(y)))))) |
Rewrite Rules
| a(a(f(x, y))) | → | f(a(b(a(b(a(x))))), a(b(a(b(a(y)))))) | | f(a(x), a(y)) | → | a(f(x, y)) |
| f(b(x), b(y)) | → | b(f(x, y)) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Problem 1: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| a#(a(f(x, y))) | → | a#(b(a(b(a(x))))) | | f#(a(x), a(y)) | → | a#(f(x, y)) |
| a#(a(f(x, y))) | → | a#(b(a(x))) | | a#(a(f(x, y))) | → | a#(x) |
| a#(a(f(x, y))) | → | a#(b(a(y))) | | a#(a(f(x, y))) | → | a#(y) |
| f#(b(x), b(y)) | → | f#(x, y) | | f#(a(x), a(y)) | → | f#(x, y) |
| a#(a(f(x, y))) | → | f#(a(b(a(b(a(x))))), a(b(a(b(a(y)))))) | | a#(a(f(x, y))) | → | a#(b(a(b(a(y))))) |
Rewrite Rules
| a(a(f(x, y))) | → | f(a(b(a(b(a(x))))), a(b(a(b(a(y)))))) | | f(a(x), a(y)) | → | a(f(x, y)) |
| f(b(x), b(y)) | → | b(f(x, y)) |
Original Signature
Termination of terms over the following signature is verified: f, b, a
Strategy
Polynomial Interpretation
- a(x): x
- a#(x): x
- b(x): x
- f(x,y): y + 2x + 1
- f#(x,y): y + 2x + 1
Improved Usable rules
| f(b(x), b(y)) | → | b(f(x, y)) | | a(a(f(x, y))) | → | f(a(b(a(b(a(x))))), a(b(a(b(a(y)))))) |
| f(a(x), a(y)) | → | a(f(x, y)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| a#(a(f(x, y))) | → | a#(b(a(b(a(x))))) | | a#(a(f(x, y))) | → | a#(b(a(y))) |
| a#(a(f(x, y))) | → | a#(x) | | a#(a(f(x, y))) | → | a#(b(a(x))) |
| a#(a(f(x, y))) | → | a#(y) | | a#(a(f(x, y))) | → | a#(b(a(b(a(y))))) |