The following DP Processors were used

Problem 1 remains open; application of the following processors failed [DependencyGraph (26ms), SubtermCriterion (1ms), DependencyGraph (11ms), PolynomialLinearRange4iUR (1461ms), DependencyGraph (7ms), PolynomialLinearRange8NegiUR (13779ms), DependencyGraph (7ms), ReductionPairSAT (timeout)].

The following open problems remain:

Open Dependency Pair Problem 1

Dependency Pairs

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

Rewrite Rules

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

Original Signature

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