TIMEOUT

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

The following DP Processors were used


Problem 1 remains open; application of the following processors failed [DependencyGraph (43ms), SubtermCriterion (0ms), DependencyGraph (17ms), PolynomialLinearRange4iUR (1331ms), DependencyGraph (14ms), PolynomialLinearRange8NegiUR (19046ms), DependencyGraph (14ms), ReductionPairSAT (timeout)].

The following open problems remain:

Open Dependency Pair Problem 1

Dependency Pairs

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

Rewrite Rules

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

Original Signature

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