NO

The TRS could be proven non-terminating. The proof took 220 ms.

The following reduction sequence is a witness for non-termination:

eq# →* eq#

The following DP Processors were used


Problem 1 remains open; application of the following processors failed [DependencyGraph (5ms), SubtermCriterion (1ms), DependencyGraph (6ms), PolynomialLinearRange4iUR (40ms), DependencyGraph (1ms), PolynomialLinearRange8NegiUR (31ms), DependencyGraph (1ms), ReductionPairSAT (17ms), DependencyGraph (1ms), SizeChangePrinciple (1ms), ForwardNarrowing (0ms), BackwardInstantiation (1ms), ForwardInstantiation (1ms), Propagation (1ms)].