MAYBE
The TRS could not be proven terminating. The proof attempt took 675 ms.
The following DP Processors were used
Problem 1 was processed with processor DependencyGraph (0ms).
| – Problem 2 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (8ms), PolynomialLinearRange4iUR (0ms), DependencyGraph (6ms), PolynomialLinearRange8NegiUR (0ms), DependencyGraph (2ms), PolynomialLinearRange4 (145ms), DependencyGraph (1ms), ReductionPairSAT (29ms), DependencyGraph (2ms), SizeChangePrinciple (82ms)].
The following open problems remain:
Open Dependency Pair Problem 2
Dependency Pairs
| a# | → | U01#(b) | | U02#(x, x) | → | a# |
| U01#(x) | → | U02#(c, x) |
Rewrite Rules
| a | → | U01(b) | | U01(x) | → | U02(c, x) |
| U02(x, x) | → | a | | b | → | U11(d) |
| U11(x) | → | U12(e, x) | | U12(x, x) | → | d |
| c | → | U21(d) | | U21(x) | → | U22(e, x) |
| U22(x, x) | → | d |
Original Signature
Termination of terms over the following signature is verified: d, e, b, c, a
Problem 1: DependencyGraph
Dependency Pair Problem
Dependency Pairs
| a# | → | U01#(b) | | U21#(x) | → | U22#(e, x) |
| c# | → | U21#(d) | | U11#(x) | → | U12#(e, x) |
| b# | → | U11#(d) | | a# | → | b# |
| U02#(x, x) | → | a# | | U01#(x) | → | U02#(c, x) |
| U01#(x) | → | c# |
Rewrite Rules
| a | → | U01(b) | | U01(x) | → | U02(c, x) |
| U02(x, x) | → | a | | b | → | U11(d) |
| U11(x) | → | U12(e, x) | | U12(x, x) | → | d |
| c | → | U21(d) | | U21(x) | → | U22(e, x) |
| U22(x, x) | → | d |
Original Signature
Termination of terms over the following signature is verified: d, e, b, c, a
Strategy
Context-sensitive strategy:
μ(d) = μ(e) = μ(b) = μ(c) = μ(a) = μ(a#) = μ(T) = μ(b#) = μ(c#) = ∅
μ(U11#) = μ(U12#) = μ(U22#) = μ(U21#) = μ(U01) = μ(U02) = μ(U11) = μ(U12) = μ(U02#) = μ(U01#) = μ(U21) = μ(U22) = {1}
The following SCCs where found
| a# → U01#(b) | U02#(x, x) → a# |
| U01#(x) → U02#(c, x) |