TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (133ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (16ms), PolynomialLinearRange4iUR (3333ms), DependencyGraph (13ms), PolynomialLinearRange8NegiUR (10000ms), DependencyGraph (16ms), ReductionPairSAT (timeout)].
 | – Problem 3 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (0ms), PolynomialLinearRange4iUR (120ms), DependencyGraph (0ms), PolynomialLinearRange8NegiUR (28ms), DependencyGraph (1ms)].
 | – Problem 4 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (16ms), PolynomialLinearRange4iUR (1922ms), DependencyGraph (14ms), PolynomialLinearRange8NegiUR (4ms), DependencyGraph (13ms)].

The following open problems remain:

Open Dependency Pair Problem 2

Dependency Pairs

h#(i(x, y)) → h#(h(y))f#(s(x)) → f#(h(s(x)))
h#(i(x, y)) → h#(y)h#(g(x, s(y))) → h#(g(s(x), y))
f#(s(x)) → h#(s(x))h#(s(f(x))) → f#(x)
f#(g(s(x), y)) → f#(g(x, s(y)))h#(s(f(x))) → h#(f(x))

Rewrite Rules

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

Original Signature

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

Open Dependency Pair Problem 3

Dependency Pairs

i#(x, x) → i#(a, b)

Rewrite Rules

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

Original Signature

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

Open Dependency Pair Problem 4

Dependency Pairs

g#(a, g(x, g(b, g(a, g(x, y))))) → g#(a, g(a, g(a, g(x, g(b, g(b, y))))))g#(a, g(x, g(b, g(a, g(x, y))))) → g#(a, g(a, g(x, g(b, g(b, y)))))
g#(a, g(x, g(b, g(a, g(x, y))))) → g#(x, g(b, g(b, y)))g#(x, x) → g#(a, b)
g#(a, g(x, g(b, g(a, g(x, y))))) → g#(a, g(x, g(b, g(b, y))))g#(a, g(x, g(b, g(a, g(x, y))))) → g#(b, g(b, y))
g#(a, g(x, g(b, g(a, g(x, y))))) → g#(b, y)

Rewrite Rules

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

Original Signature

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

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

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

Original Signature

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

Strategy

The following SCCs where found

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