MAYBE

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

The following DP Processors were used

Problem 1 remains open; application of the following processors failed [DependencyGraph (52ms), SubtermCriterion (1ms), DependencyGraph (15ms), PolynomialLinearRange4iUR (723ms), DependencyGraph (13ms), PolynomialLinearRange8NegiUR (2396ms), DependencyGraph (10ms), ReductionPairSAT (951ms), DependencyGraph (11ms), SizeChangePrinciple (109ms)].

The following open problems remain:

Open Dependency Pair Problem 1

Dependency Pairs

a^#(p(x, y), z)	→	a^#(y, z)		a^#(p(x, y), z)	→	a^#(x, z)
a^#(a(x, y), z)	→	a^#(y, z)		a^#(lambda(x), y)	→	a^#(x, p(1, a(y, t)))
a^#(a(x, y), z)	→	a^#(x, a(y, z))		a^#(lambda(x), y)	→	a^#(y, t)

Rewrite Rules

a(lambda(x), y)	→	lambda(a(x, p(1, a(y, t))))		a(p(x, y), z)	→	p(a(x, z), a(y, z))
a(a(x, y), z)	→	a(x, a(y, z))		a(id, x)	→	x
a(1, id)	→	1		a(t, id)	→	t
a(1, p(x, y))	→	x		a(t, p(x, y))	→	y

Original Signature

Termination of terms over the following signature is verified: id, lambda, 1, t, a, p