0 QTRS
↳1 DirectTerminationProof (⇔)
↳2 TRUE
w(r(x)) → r(w(x)) b(r(x)) → r(b(x)) b(w(x)) → w(b(x))
b1 > w1 > r1
w_1=2 r_1=1 b_1=3