TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (199ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (3ms), PolynomialLinearRange4iUR (75ms), DependencyGraph (2ms), PolynomialLinearRange8NegiUR (90ms), DependencyGraph (1ms), ReductionPairSAT (208ms)].
 | – Problem 3 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (116ms), PolynomialLinearRange4iUR (5000ms), DependencyGraph (99ms), PolynomialLinearRange8NegiUR (15027ms), DependencyGraph (89ms), ReductionPairSAT (timeout)].

The following open problems remain:

Open Dependency Pair Problem 2

Dependency Pairs

g#(x, y, x) → g#(c, d, e)g#(x, x, x) → g#(c, d, e)

Rewrite Rules

g(x, x, x) → g(c, d, e)g(x, y, x) → g(c, d, e)
s(f(x, y)) → f(y, f(s(s(x)), a))h(h(x, a), y) → h(h(a, y), h(a, x))
f(x, f(y, f(x, y))) → f(a, f(x, f(y, b)))f(h(a, y), g(x, b, a)) → h(f(x, s(y)), s(b))
h(f(x, s(y)), b) → f(a, g(y, a, f(s(x), a)))f(x, g(x, a, f(s(x), y))) → f(h(x, b), g(a, b, y))
s(y) → b

Original Signature

Termination of terms over the following signature is verified: f, g, d, e, b, s, c, a, h

Open Dependency Pair Problem 3

Dependency Pairs

f#(x, f(y, f(x, y))) → f#(x, f(y, b))s#(f(x, y)) → f#(y, f(s(s(x)), a))
h#(h(x, a), y) → h#(a, x)f#(x, f(y, f(x, y))) → f#(a, f(x, f(y, b)))
f#(x, g(x, a, f(s(x), y))) → h#(x, b)f#(h(a, y), g(x, b, a)) → h#(f(x, s(y)), s(b))
s#(f(x, y)) → s#(s(x))h#(h(x, a), y) → h#(a, y)
s#(f(x, y)) → f#(s(s(x)), a)f#(x, g(x, a, f(s(x), y))) → f#(h(x, b), g(a, b, y))
s#(f(x, y)) → s#(x)f#(h(a, y), g(x, b, a)) → f#(x, s(y))
f#(h(a, y), g(x, b, a)) → s#(b)f#(x, f(y, f(x, y))) → f#(y, b)
h#(f(x, s(y)), b) → f#(s(x), a)h#(f(x, s(y)), b) → f#(a, g(y, a, f(s(x), a)))
h#(h(x, a), y) → h#(h(a, y), h(a, x))h#(f(x, s(y)), b) → s#(x)
f#(h(a, y), g(x, b, a)) → s#(y)

Rewrite Rules

g(x, x, x) → g(c, d, e)g(x, y, x) → g(c, d, e)
s(f(x, y)) → f(y, f(s(s(x)), a))h(h(x, a), y) → h(h(a, y), h(a, x))
f(x, f(y, f(x, y))) → f(a, f(x, f(y, b)))f(h(a, y), g(x, b, a)) → h(f(x, s(y)), s(b))
h(f(x, s(y)), b) → f(a, g(y, a, f(s(x), a)))f(x, g(x, a, f(s(x), y))) → f(h(x, b), g(a, b, y))
s(y) → b

Original Signature

Termination of terms over the following signature is verified: f, g, d, e, b, s, c, a, h

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

g#(x, y, x) → g#(c, d, e)f#(x, f(y, f(x, y))) → f#(x, f(y, b))
s#(f(x, y)) → f#(y, f(s(s(x)), a))h#(h(x, a), y) → h#(a, x)
f#(x, f(y, f(x, y))) → f#(a, f(x, f(y, b)))f#(x, g(x, a, f(s(x), y))) → h#(x, b)
g#(x, x, x) → g#(c, d, e)f#(h(a, y), g(x, b, a)) → h#(f(x, s(y)), s(b))
s#(f(x, y)) → s#(s(x))h#(h(x, a), y) → h#(a, y)
s#(f(x, y)) → f#(s(s(x)), a)f#(x, g(x, a, f(s(x), y))) → f#(h(x, b), g(a, b, y))
s#(f(x, y)) → s#(x)f#(h(a, y), g(x, b, a)) → f#(x, s(y))
f#(x, f(y, f(x, y))) → f#(y, b)f#(h(a, y), g(x, b, a)) → s#(b)
f#(x, g(x, a, f(s(x), y))) → g#(a, b, y)h#(f(x, s(y)), b) → f#(s(x), a)
h#(h(x, a), y) → h#(h(a, y), h(a, x))h#(f(x, s(y)), b) → f#(a, g(y, a, f(s(x), a)))
h#(f(x, s(y)), b) → s#(x)f#(h(a, y), g(x, b, a)) → s#(y)
h#(f(x, s(y)), b) → g#(y, a, f(s(x), a))

Rewrite Rules

g(x, x, x) → g(c, d, e)g(x, y, x) → g(c, d, e)
s(f(x, y)) → f(y, f(s(s(x)), a))h(h(x, a), y) → h(h(a, y), h(a, x))
f(x, f(y, f(x, y))) → f(a, f(x, f(y, b)))f(h(a, y), g(x, b, a)) → h(f(x, s(y)), s(b))
h(f(x, s(y)), b) → f(a, g(y, a, f(s(x), a)))f(x, g(x, a, f(s(x), y))) → f(h(x, b), g(a, b, y))
s(y) → b

Original Signature

Termination of terms over the following signature is verified: f, g, d, e, s, b, c, a, h

Strategy

The following SCCs where found

f#(x, f(y, f(x, y))) → f#(x, f(y, b))s#(f(x, y)) → f#(y, f(s(s(x)), a))
h#(h(x, a), y) → h#(a, x)f#(x, f(y, f(x, y))) → f#(a, f(x, f(y, b)))
f#(h(a, y), g(x, b, a)) → h#(f(x, s(y)), s(b))f#(x, g(x, a, f(s(x), y))) → h#(x, b)
s#(f(x, y)) → s#(s(x))h#(h(x, a), y) → h#(a, y)
s#(f(x, y)) → f#(s(s(x)), a)f#(x, g(x, a, f(s(x), y))) → f#(h(x, b), g(a, b, y))
s#(f(x, y)) → s#(x)f#(h(a, y), g(x, b, a)) → f#(x, s(y))
f#(x, f(y, f(x, y))) → f#(y, b)f#(h(a, y), g(x, b, a)) → s#(b)
h#(f(x, s(y)), b) → f#(s(x), a)h#(h(x, a), y) → h#(h(a, y), h(a, x))
h#(f(x, s(y)), b) → f#(a, g(y, a, f(s(x), a)))h#(f(x, s(y)), b) → s#(x)
f#(h(a, y), g(x, b, a)) → s#(y)
g#(x, y, x) → g#(c, d, e)g#(x, x, x) → g#(c, d, e)