The following DP Processors were used

Problem 1 remains open; application of the following processors failed [DependencyGraph (11ms), SubtermCriterion (1ms), DependencyGraph (4ms), PolynomialLinearRange4iUR (220ms), DependencyGraph (2ms), PolynomialLinearRange8NegiUR (1865ms), DependencyGraph (2ms), ReductionPairSAT (9818ms), DependencyGraph (2ms), SizeChangePrinciple (18ms)].

The following open problems remain:

Open Dependency Pair Problem 1

Dependency Pairs

h^#(x, c(y, z))

→

h^#(c(s(y), x), z)

h^#(c(s(x), c(s(0), y)), z)

→

h^#(y, c(s(0), c(x, z)))

Rewrite Rules

h(x, c(y, z))

→

h(c(s(y), x), z)

h(c(s(x), c(s(0), y)), z)

→

h(y, c(s(0), c(x, z)))

Original Signature

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