MAYBE

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

The following DP Processors were used


Problem 1 remains open; application of the following processors failed [DependencyGraph (28ms), SubtermCriterion (1ms), DependencyGraph (12ms), PolynomialLinearRange4iUR (530ms), DependencyGraph (7ms), PolynomialLinearRange8NegiUR (4635ms), DependencyGraph (49ms), ReductionPairSAT (4715ms), DependencyGraph (47ms), SizeChangePrinciple (19ms)].

The following open problems remain:

Open Dependency Pair Problem 1

Dependency Pairs

c#(a(a(0, x), y)) → c#(c(c(0)))c#(c(c(y))) → c#(a(y, 0))
c#(a(a(0, x), y)) → c#(0)c#(a(a(0, x), y)) → c#(c(0))
c#(c(c(y))) → c#(c(a(y, 0)))

Rewrite Rules

c(c(c(y))) → c(c(a(y, 0)))c(a(a(0, x), y)) → a(c(c(c(0))), y)
c(y) → y

Original Signature

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