MAYBE
The TRS could not be proven terminating. The proof attempt took 54536 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (0ms).
| – Problem 2 was processed with processor PolynomialLinearRange4iUR (0ms).
| | – Problem 4 remains open; application of the following processors failed [DependencyGraph (1ms), PolynomialLinearRange4iUR (69ms), DependencyGraph (1ms), PolynomialLinearRange8NegiUR (655ms), DependencyGraph (10ms), ReductionPairSAT (516ms), DependencyGraph (0ms), SizeChangePrinciple (8ms)].
| – Problem 3 was processed with processor PolynomialLinearRange4iUR (0ms).
| | – Problem 5 was processed with processor DependencyGraph (0ms).
| | | – Problem 6 remains open; application of the following processors failed [PolynomialLinearRange4iUR (328ms), DependencyGraph (1ms), PolynomialLinearRange8NegiUR (2365ms), DependencyGraph (2ms), ReductionPairSAT (12218ms), DependencyGraph (0ms), SizeChangePrinciple (56ms)].
| | | – Problem 7 remains open; application of the following processors failed [PolynomialLinearRange4iUR (1485ms), DependencyGraph (1ms), PolynomialLinearRange8NegiUR (10000ms), DependencyGraph (1ms), ReductionPairSAT (21012ms), DependencyGraph (1ms), SizeChangePrinciple (41ms)].
The following open problems remain:
Open Dependency Pair Problem 4
Dependency Pairs
| g#(g(x, a), y) | → | g#(g(a, y), g(a, x)) |
Rewrite Rules
| h(x, x) | → | h(a, b) | | g(g(x, a), y) | → | g(g(a, y), g(a, x)) |
| f(g(x, y)) | → | g(g(f(f(y)), h(a, a)), x) | | h(h(f(f(x)), y), h(z, v)) | → | h(h(f(z), f(f(f(y)))), h(v, x)) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, h
Open Dependency Pair Problem 6
Dependency Pairs
| f#(g(x, y)) | → | f#(f(y)) | | f#(g(x, y)) | → | f#(y) |
Rewrite Rules
| h(x, x) | → | h(a, b) | | g(g(x, a), y) | → | g(g(a, y), g(a, x)) |
| f(g(x, y)) | → | g(g(f(f(y)), h(a, a)), x) | | h(h(f(f(x)), y), h(z, v)) | → | h(h(f(z), f(f(f(y)))), h(v, x)) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, h
Open Dependency Pair Problem 7
Dependency Pairs
| h#(h(f(f(x)), y), h(z, v)) | → | h#(h(f(z), f(f(f(y)))), h(v, x)) | | h#(x, x) | → | h#(a, b) |
Rewrite Rules
| h(x, x) | → | h(a, b) | | g(g(x, a), y) | → | g(g(a, y), g(a, x)) |
| f(g(x, y)) | → | g(g(f(f(y)), h(a, a)), x) | | h(h(f(f(x)), y), h(z, v)) | → | h(h(f(z), f(f(f(y)))), h(v, x)) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, h
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| h#(h(f(f(x)), y), h(z, v)) | → | h#(h(f(z), f(f(f(y)))), h(v, x)) | | g#(g(x, a), y) | → | g#(g(a, y), g(a, x)) |
| g#(g(x, a), y) | → | g#(a, y) | | h#(h(f(f(x)), y), h(z, v)) | → | h#(v, x) |
| f#(g(x, y)) | → | g#(g(f(f(y)), h(a, a)), x) | | h#(x, x) | → | h#(a, b) |
| f#(g(x, y)) | → | f#(f(y)) | | h#(h(f(f(x)), y), h(z, v)) | → | f#(z) |
| h#(h(f(f(x)), y), h(z, v)) | → | f#(y) | | h#(h(f(f(x)), y), h(z, v)) | → | f#(f(y)) |
| f#(g(x, y)) | → | f#(y) | | f#(g(x, y)) | → | g#(f(f(y)), h(a, a)) |
| f#(g(x, y)) | → | h#(a, a) | | h#(h(f(f(x)), y), h(z, v)) | → | f#(f(f(y))) |
| h#(h(f(f(x)), y), h(z, v)) | → | h#(f(z), f(f(f(y)))) | | g#(g(x, a), y) | → | g#(a, x) |
Rewrite Rules
| h(x, x) | → | h(a, b) | | g(g(x, a), y) | → | g(g(a, y), g(a, x)) |
| f(g(x, y)) | → | g(g(f(f(y)), h(a, a)), x) | | h(h(f(f(x)), y), h(z, v)) | → | h(h(f(z), f(f(f(y)))), h(v, x)) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, h
Strategy
The following SCCs where found
| g#(g(x, a), y) → g#(g(a, y), g(a, x)) | g#(g(x, a), y) → g#(a, y) |
| g#(g(x, a), y) → g#(a, x) |
| h#(h(f(f(x)), y), h(z, v)) → h#(h(f(z), f(f(f(y)))), h(v, x)) | f#(g(x, y)) → h#(a, a) |
| h#(h(f(f(x)), y), h(z, v)) → h#(v, x) | h#(h(f(f(x)), y), h(z, v)) → f#(f(f(y))) |
| h#(h(f(f(x)), y), h(z, v)) → h#(f(z), f(f(f(y)))) | h#(x, x) → h#(a, b) |
| h#(h(f(f(x)), y), h(z, v)) → f#(z) | f#(g(x, y)) → f#(f(y)) |
| f#(g(x, y)) → f#(y) | h#(h(f(f(x)), y), h(z, v)) → f#(f(y)) |
| h#(h(f(f(x)), y), h(z, v)) → f#(y) |
Problem 2: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| g#(g(x, a), y) | → | g#(g(a, y), g(a, x)) | | g#(g(x, a), y) | → | g#(a, y) |
| g#(g(x, a), y) | → | g#(a, x) |
Rewrite Rules
| h(x, x) | → | h(a, b) | | g(g(x, a), y) | → | g(g(a, y), g(a, x)) |
| f(g(x, y)) | → | g(g(f(f(y)), h(a, a)), x) | | h(h(f(f(x)), y), h(z, v)) | → | h(h(f(z), f(f(f(y)))), h(v, x)) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, h
Strategy
Polynomial Interpretation
- a: 0
- b: 0
- f(x): 0
- g(x,y): 1
- g#(x,y): 2x
- h(x,y): 0
Improved Usable rules
| g(g(x, a), y) | → | g(g(a, y), g(a, x)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| g#(g(x, a), y) | → | g#(a, y) | | g#(g(x, a), y) | → | g#(a, x) |
Problem 3: PolynomialLinearRange4iUR
Dependency Pair Problem
Dependency Pairs
| h#(h(f(f(x)), y), h(z, v)) | → | h#(h(f(z), f(f(f(y)))), h(v, x)) | | f#(g(x, y)) | → | h#(a, a) |
| h#(h(f(f(x)), y), h(z, v)) | → | h#(v, x) | | h#(h(f(f(x)), y), h(z, v)) | → | f#(f(f(y))) |
| h#(h(f(f(x)), y), h(z, v)) | → | h#(f(z), f(f(f(y)))) | | h#(x, x) | → | h#(a, b) |
| h#(h(f(f(x)), y), h(z, v)) | → | f#(z) | | f#(g(x, y)) | → | f#(f(y)) |
| f#(g(x, y)) | → | f#(y) | | h#(h(f(f(x)), y), h(z, v)) | → | f#(f(y)) |
| h#(h(f(f(x)), y), h(z, v)) | → | f#(y) |
Rewrite Rules
| h(x, x) | → | h(a, b) | | g(g(x, a), y) | → | g(g(a, y), g(a, x)) |
| f(g(x, y)) | → | g(g(f(f(y)), h(a, a)), x) | | h(h(f(f(x)), y), h(z, v)) | → | h(h(f(z), f(f(f(y)))), h(v, x)) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, h
Strategy
Polynomial Interpretation
- a: 0
- b: 0
- f(x): x
- f#(x): 1
- g(x,y): 0
- h(x,y): y + x + 1
- h#(x,y): y + x
Improved Usable rules
| f(g(x, y)) | → | g(g(f(f(y)), h(a, a)), x) | | h(x, x) | → | h(a, b) |
| g(g(x, a), y) | → | g(g(a, y), g(a, x)) | | h(h(f(f(x)), y), h(z, v)) | → | h(h(f(z), f(f(f(y)))), h(v, x)) |
The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:
| f#(g(x, y)) | → | h#(a, a) | | h#(h(f(f(x)), y), h(z, v)) | → | h#(v, x) |
| h#(h(f(f(x)), y), h(z, v)) | → | f#(f(f(y))) | | h#(h(f(f(x)), y), h(z, v)) | → | h#(f(z), f(f(f(y)))) |
| h#(h(f(f(x)), y), h(z, v)) | → | f#(z) | | h#(h(f(f(x)), y), h(z, v)) | → | f#(y) |
| h#(h(f(f(x)), y), h(z, v)) | → | f#(f(y)) |
Problem 5: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| h#(h(f(f(x)), y), h(z, v)) | → | h#(h(f(z), f(f(f(y)))), h(v, x)) | | h#(x, x) | → | h#(a, b) |
| f#(g(x, y)) | → | f#(f(y)) | | f#(g(x, y)) | → | f#(y) |
Rewrite Rules
| h(x, x) | → | h(a, b) | | g(g(x, a), y) | → | g(g(a, y), g(a, x)) |
| f(g(x, y)) | → | g(g(f(f(y)), h(a, a)), x) | | h(h(f(f(x)), y), h(z, v)) | → | h(h(f(z), f(f(f(y)))), h(v, x)) |
Original Signature
Termination of terms over the following signature is verified: f, g, b, a, h
Strategy
The following SCCs where found
| h#(h(f(f(x)), y), h(z, v)) → h#(h(f(z), f(f(f(y)))), h(v, x)) | h#(x, x) → h#(a, b) |
| f#(g(x, y)) → f#(f(y)) | f#(g(x, y)) → f#(y) |