TIMEOUT

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

The following DP Processors were used

Problem 1 was processed with processor DependencyGraph (111ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (13ms), DependencyGraph (10ms), PolynomialLinearRange4iUR (175ms), DependencyGraph (10ms), PolynomialLinearRange8NegiUR (471ms), DependencyGraph (10ms), ReductionPairSAT (timeout)].

The following open problems remain:

Open Dependency Pair Problem 2

Dependency Pairs

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

Rewrite Rules

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

Original Signature

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

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

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

Original Signature

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

Strategy

The following SCCs where found

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