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

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

The following DP Processors were used

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