TIMEOUT

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

The following DP Processors were used

Problem 1 was processed with processor DependencyGraph (148ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (7ms), DependencyGraph (13ms), PolynomialLinearRange4iUR (314ms), DependencyGraph (14ms), PolynomialLinearRange8NegiUR (504ms), DependencyGraph (13ms), ReductionPairSAT (timeout)].

The following open problems remain:

Open Dependency Pair Problem 2

Dependency Pairs

e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)	→	e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)		e4^#(g1(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w)	→	e1^#(x1, x1, x, y, z, w)
e2^#(f1(w, w), x, y, z, f2(w, w), w)	→	e3^#(x, y, x, y, y, z, y, z, x, y, z, w)		e1^#(h1(w), h2(w), x, y, z, w)	→	e2^#(x, x, y, z, z, w)

Rewrite Rules

f1(a, x)	→	g1(x, x)		f1(x, a)	→	g2(x, x)
f2(a, x)	→	g1(x, x)		f2(x, a)	→	g2(x, x)
g1(a, x)	→	h1(x)		g1(x, a)	→	h2(x)
g2(a, x)	→	h1(x)		g2(x, a)	→	h2(x)
h1(a)	→	i		h2(a)	→	i
e1(h1(w), h2(w), x, y, z, w)	→	e2(x, x, y, z, z, w)		e1(x1, x1, x, y, z, a)	→	e5(x1, x, y, z)
e2(f1(w, w), x, y, z, f2(w, w), w)	→	e3(x, y, x, y, y, z, y, z, x, y, z, w)		e2(x, x, y, z, z, a)	→	e6(x, y, z)
e2(i, x, y, z, i, a)	→	e6(x, y, z)		e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)	→	e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)
e3(x, y, x, y, y, z, y, z, x, y, z, a)	→	e6(x, y, z)		e4(g1(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w)	→	e1(x1, x1, x, y, z, w)
e4(i, x1, i, x1, i, x1, i, x1, x, y, z, a)	→	e5(x1, x, y, z)		e4(x, x, x, x, x, x, x, x, x, x, x, a)	→	e6(x, x, x)
e5(i, x, y, z)	→	e6(x, y, z)

Original Signature

Termination of terms over the following signature is verified: a, e6, i, e5, e3, e4, e1, e2, g2, g1, f1, h1, f2, h2

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)	→	e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)		g1^#(a, x)	→	h1^#(x)
f1^#(x, a)	→	g2^#(x, x)		e1^#(h1(w), h2(w), x, y, z, w)	→	e2^#(x, x, y, z, z, w)
f2^#(x, a)	→	g2^#(x, x)		g2^#(a, x)	→	h1^#(x)
e4^#(g1(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w)	→	e1^#(x1, x1, x, y, z, w)		e4^#(i, x1, i, x1, i, x1, i, x1, x, y, z, a)	→	e5^#(x1, x, y, z)
e2^#(f1(w, w), x, y, z, f2(w, w), w)	→	e3^#(x, y, x, y, y, z, y, z, x, y, z, w)		f1^#(a, x)	→	g1^#(x, x)
g2^#(x, a)	→	h2^#(x)		f2^#(a, x)	→	g1^#(x, x)
e1^#(x1, x1, x, y, z, a)	→	e5^#(x1, x, y, z)		g1^#(x, a)	→	h2^#(x)

Rewrite Rules

f1(a, x)	→	g1(x, x)		f1(x, a)	→	g2(x, x)
f2(a, x)	→	g1(x, x)		f2(x, a)	→	g2(x, x)
g1(a, x)	→	h1(x)		g1(x, a)	→	h2(x)
g2(a, x)	→	h1(x)		g2(x, a)	→	h2(x)
h1(a)	→	i		h2(a)	→	i
e1(h1(w), h2(w), x, y, z, w)	→	e2(x, x, y, z, z, w)		e1(x1, x1, x, y, z, a)	→	e5(x1, x, y, z)
e2(f1(w, w), x, y, z, f2(w, w), w)	→	e3(x, y, x, y, y, z, y, z, x, y, z, w)		e2(x, x, y, z, z, a)	→	e6(x, y, z)
e2(i, x, y, z, i, a)	→	e6(x, y, z)		e3(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)	→	e4(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)
e3(x, y, x, y, y, z, y, z, x, y, z, a)	→	e6(x, y, z)		e4(g1(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w)	→	e1(x1, x1, x, y, z, w)
e4(i, x1, i, x1, i, x1, i, x1, x, y, z, a)	→	e5(x1, x, y, z)		e4(x, x, x, x, x, x, x, x, x, x, x, a)	→	e6(x, x, x)
e5(i, x, y, z)	→	e6(x, y, z)

Original Signature

Termination of terms over the following signature is verified: a, e6, i, e5, e3, e4, e1, e2, g2, g1, f1, h1, f2, h2

Strategy

The following SCCs where found

e3^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w) → e4^#(x1, x1, x2, x2, x3, x3, x4, x4, x, y, z, w)	e4^#(g1(w, w), x1, g2(w, w), x1, g1(w, w), x1, g2(w, w), x1, x, y, z, w) → e1^#(x1, x1, x, y, z, w)
e2^#(f1(w, w), x, y, z, f2(w, w), w) → e3^#(x, y, x, y, y, z, y, z, x, y, z, w)	e1^#(h1(w), h2(w), x, y, z, w) → e2^#(x, x, y, z, z, w)