The TRS could be proven non-terminating. The proof took 257 ms.
The following reduction sequence is a witness for non-termination:
f#(a) →* f#(a)
Problem 1 remains open; application of the following processors failed [DependencyGraph (5ms), SubtermCriterion (0ms), DependencyGraph (1ms), PolynomialLinearRange4iUR (72ms), DependencyGraph (1ms), PolynomialLinearRange8NegiUR (44ms), DependencyGraph (1ms), ReductionPairSAT (11ms), DependencyGraph (1ms), SizeChangePrinciple (46ms), ForwardNarrowing (1ms), BackwardInstantiation (1ms), ForwardInstantiation (0ms), Propagation (2ms)].