YES Problem: w(r(x)) -> r(w(x)) b(r(x)) -> r(b(x)) b(w(x)) -> w(b(x)) Proof: DP Processor: DPs: w#(r(x)) -> w#(x) b#(r(x)) -> b#(x) b#(w(x)) -> b#(x) b#(w(x)) -> w#(b(x)) TRS: w(r(x)) -> r(w(x)) b(r(x)) -> r(b(x)) b(w(x)) -> w(b(x)) TDG Processor: DPs: w#(r(x)) -> w#(x) b#(r(x)) -> b#(x) b#(w(x)) -> b#(x) b#(w(x)) -> w#(b(x)) TRS: w(r(x)) -> r(w(x)) b(r(x)) -> r(b(x)) b(w(x)) -> w(b(x)) graph: b#(w(x)) -> b#(x) -> b#(w(x)) -> w#(b(x)) b#(w(x)) -> b#(x) -> b#(w(x)) -> b#(x) b#(w(x)) -> b#(x) -> b#(r(x)) -> b#(x) b#(w(x)) -> w#(b(x)) -> w#(r(x)) -> w#(x) b#(r(x)) -> b#(x) -> b#(w(x)) -> w#(b(x)) b#(r(x)) -> b#(x) -> b#(w(x)) -> b#(x) b#(r(x)) -> b#(x) -> b#(r(x)) -> b#(x) w#(r(x)) -> w#(x) -> w#(r(x)) -> w#(x) CDG Processor: DPs: w#(r(x)) -> w#(x) b#(r(x)) -> b#(x) b#(w(x)) -> b#(x) b#(w(x)) -> w#(b(x)) TRS: w(r(x)) -> r(w(x)) b(r(x)) -> r(b(x)) b(w(x)) -> w(b(x)) graph: b#(w(x)) -> w#(b(x)) -> w#(r(x)) -> w#(x) SCC Processor: #sccs: 0 #rules: 0 #arcs: 1/16