YES

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

The following DP Processors were used


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

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

f#(a, b)f#(a, c)f#(c, d)f#(b, d)

Rewrite Rules

f(a, b)f(a, c)f(c, d)f(b, d)

Original Signature

Termination of terms over the following signature is verified: f, d, b, c, a

Strategy


There are no SCCs!