YES

The TRS could be proven terminating. The proof took 19 ms.

The following DP Processors were used

Problem 1 was processed with processor DependencyGraph (3ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

c^#(u(x))

→

b^#(x)

d^#(u(x))

→

c^#(x)

Rewrite Rules

d(x)	→	e(u(x))		d(u(x))	→	c(x)
c(u(x))	→	b(x)		v(e(x))	→	x
b(u(x))	→	a(e(x))

Original Signature

Termination of terms over the following signature is verified: v, u, d, e, b, c, a

Strategy

There are no SCCs!