The TRS could be proven non-terminating. The proof took 145 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 (1ms), PolynomialOrdering (27ms), DependencyGraph (0ms), PolynomialOrdering (27ms), DependencyGraph (1ms), PolynomialOrdering (9ms), DependencyGraph (1ms), ReductionPairSAT (11ms), DependencyGraph (0ms), SizeChangePrinciple (0ms), BackwardsNarrowing (7ms), BackwardInstantiation (1ms), ForwardInstantiation (1ms), Propagation (2ms)].