YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (5ms).
 | – Problem 2 was processed with processor SubtermCriterion (0ms).
 | – Problem 3 was processed with processor SubtermCriterion (1ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

b#(r(x))b#(x)b#(w(x))b#(x)
b#(w(x))w#(b(x))w#(r(x))w#(x)

Rewrite Rules

w(r(x))r(w(x))b(r(x))r(b(x))
b(w(x))w(b(x))

Original Signature

Termination of terms over the following signature is verified: w, b, r

Strategy


The following SCCs where found

b#(r(x)) → b#(x)b#(w(x)) → b#(x)

w#(r(x)) → w#(x)

Problem 2: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

b#(r(x))b#(x)b#(w(x))b#(x)

Rewrite Rules

w(r(x))r(w(x))b(r(x))r(b(x))
b(w(x))w(b(x))

Original Signature

Termination of terms over the following signature is verified: w, b, r

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

b#(r(x))b#(x)b#(w(x))b#(x)

Problem 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

w#(r(x))w#(x)

Rewrite Rules

w(r(x))r(w(x))b(r(x))r(b(x))
b(w(x))w(b(x))

Original Signature

Termination of terms over the following signature is verified: w, b, r

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

w#(r(x))w#(x)