MAYBE

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (0ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (3ms), PolynomialLinearRange4iUR (237ms), DependencyGraph (2ms), PolynomialLinearRange8NegiUR (831ms), DependencyGraph (2ms), ReductionPairSAT (5177ms), DependencyGraph (1ms), SizeChangePrinciple (78ms)].
 | – Problem 3 was processed with processor SubtermCriterion (0ms).

The following open problems remain:



Open Dependency Pair Problem 2

Dependency Pairs

f#(x, c(x), c(y))f#(y, x, y)f#(x, c(x), c(y))f#(y, y, f(y, x, y))

Rewrite Rules

f(x, c(x), c(y))f(y, y, f(y, x, y))f(s(x), y, z)f(x, s(c(y)), c(z))
f(c(x), x, y)c(y)g(x, y)x
g(x, y)y

Original Signature

Termination of terms over the following signature is verified: f, g, s, c


Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

f#(x, c(x), c(y))f#(y, x, y)f#(x, c(x), c(y))f#(y, y, f(y, x, y))
f#(s(x), y, z)f#(x, s(c(y)), c(z))

Rewrite Rules

f(x, c(x), c(y))f(y, y, f(y, x, y))f(s(x), y, z)f(x, s(c(y)), c(z))
f(c(x), x, y)c(y)g(x, y)x
g(x, y)y

Original Signature

Termination of terms over the following signature is verified: f, g, s, c

Strategy


The following SCCs where found

f#(s(x), y, z) → f#(x, s(c(y)), c(z))

f#(x, c(x), c(y)) → f#(y, x, y)f#(x, c(x), c(y)) → f#(y, y, f(y, x, y))

Problem 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

f#(s(x), y, z)f#(x, s(c(y)), c(z))

Rewrite Rules

f(x, c(x), c(y))f(y, y, f(y, x, y))f(s(x), y, z)f(x, s(c(y)), c(z))
f(c(x), x, y)c(y)g(x, y)x
g(x, y)y

Original Signature

Termination of terms over the following signature is verified: f, g, s, c

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

f#(s(x), y, z)f#(x, s(c(y)), c(z))