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 (41ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (7ms), DependencyGraph (8ms), PolynomialLinearRange4iUR (167ms), DependencyGraph (7ms), PolynomialLinearRange8NegiUR (367ms), DependencyGraph (6ms), 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
e1(h1, h2, x, y, z)	→	e2(x, x, y, z, z)		e2(f1, x, y, z, f2)	→	e3(x, y, x, y, y, z, y, z, 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)		e4(g1, x1, g2, x1, g1, x1, g2, x1, x, y, z)	→	e1(x1, x1, x, y, z)

Original Signature

Termination of terms over the following signature is verified: 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)		f1^#	→	g2^#
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^#		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
e1(h1, h2, x, y, z)	→	e2(x, x, y, z, z)		e2(f1, x, y, z, f2)	→	e3(x, y, x, y, y, z, y, z, 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)		e4(g1, x1, g2, x1, g1, x1, g2, x1, x, y, z)	→	e1(x1, x1, x, y, z)

Original Signature

Termination of terms over the following signature is verified: 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)