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

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

f# →* f#

The following DP Processors were used


Problem 1 remains open; application of the following processors failed [DependencyGraph (4ms), SubtermCriterion (0ms), DependencyGraph (0ms), PolynomialOrdering (26ms), DependencyGraph (0ms), PolynomialOrdering (26ms), DependencyGraph (1ms), PolynomialOrdering (10ms), DependencyGraph (1ms), ReductionPairSAT (5ms), DependencyGraph (0ms), SizeChangePrinciple (1ms), ForwardNarrowing (7ms), BackwardInstantiation (1ms), ForwardInstantiation (0ms), Propagation (1ms)].