MAYBE

The TRS could not be proven terminating. The proof attempt took 31105 ms.

The following DP Processors were used


Problem 1 remains open; application of the following processors failed [DependencyGraph (17ms), SubtermCriterion (1ms), DependencyGraph (5ms), PolynomialLinearRange4iUR (654ms), DependencyGraph (4ms), PolynomialLinearRange8NegiUR (6743ms), DependencyGraph (2ms), ReductionPairSAT (23547ms), DependencyGraph (5ms), SizeChangePrinciple (10ms)].

The following open problems remain:

Open Dependency Pair Problem 1

Dependency Pairs

a#(b(a(b(x)))) → a#(a(b(x)))a#(b(a(b(x)))) → a#(b(a(a(b(x)))))
a#(b(a(b(x)))) → a#(b(x))

Rewrite Rules

a(b(a(b(x)))) → b(a(b(a(a(b(x))))))

Original Signature

Termination of terms over the following signature is verified: b, a