YES We show the termination of the TRS R: w(r(x)) -> r(w(x)) b(r(x)) -> r(b(x)) b(w(x)) -> w(b(x)) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: w#(r(x)) -> w#(x) p2: b#(r(x)) -> b#(x) p3: b#(w(x)) -> w#(b(x)) p4: b#(w(x)) -> b#(x) and R consists of: r1: w(r(x)) -> r(w(x)) r2: b(r(x)) -> r(b(x)) r3: b(w(x)) -> w(b(x)) The estimated dependency graph contains the following SCCs: {p2, p4} {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: b#(w(x)) -> b#(x) p2: b#(r(x)) -> b#(x) and R consists of: r1: w(r(x)) -> r(w(x)) r2: b(r(x)) -> r(b(x)) r3: b(w(x)) -> w(b(x)) The set of usable rules consists of r1 Take the reduction pair: generalized weighted path order (>=MG, >MG) base order 1: matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: b#_A(x1) = x1 w_A(x1) = x1 + 2 r_A(x1) = x1 + 3 base order 2: precedence: b# > w > r partial status: pi(b#) = [1] pi(w) = [1] pi(r) = [1] The following rules are removed: p1 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: b#(r(x)) -> b#(x) and R consists of: r1: w(r(x)) -> r(w(x)) r2: b(r(x)) -> r(b(x)) r3: b(w(x)) -> w(b(x)) The estimated dependency graph contains the following SCCs: {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: b#(r(x)) -> b#(x) and R consists of: r1: w(r(x)) -> r(w(x)) r2: b(r(x)) -> r(b(x)) r3: b(w(x)) -> w(b(x)) The set of usable rules consists of r1 Take the monotone reduction pair: generalized weighted path order (>=MG, >MG) base order 1: matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: b#_A(x1) = x1 r_A(x1) = x1 + 3 w_A(x1) = x1 + 2 base order 2: precedence: r = w > b# partial status: pi(b#) = [1] pi(r) = [1] pi(w) = [1] The following rules are removed: p1 Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: w#(r(x)) -> w#(x) and R consists of: r1: w(r(x)) -> r(w(x)) r2: b(r(x)) -> r(b(x)) r3: b(w(x)) -> w(b(x)) The set of usable rules consists of r1 Take the monotone reduction pair: generalized weighted path order (>=MG, >MG) base order 1: matrix interpretation with standard point-wise order: carrier: N^1 order: standard order interpretations: w#_A(x1) = x1 r_A(x1) = x1 + 3 w_A(x1) = x1 + 2 base order 2: precedence: r = w > w# partial status: pi(w#) = [1] pi(r) = [1] pi(w) = [1] The following rules are removed: p1 Then no dependency pair remains.