Input TRS:
    1: R(x,B2()) -> B2()
    2: W(x,B2()) -> B2()
    3: B1() ->= R(T(),B1())
    4: B1() ->= W(T(),B1())
Number of strict rules: 2
Direct Order(PosReal,>,Poly) ... removes: 1
     W(x1,x2)	weight: x2 + x1
     T()	weight: 0
    B1()	weight: 0
     R(x1,x2)	weight: 2 * x2 + x1
    B2()	weight: (/ 1 4)
Number of strict rules: 1
Direct Order(PosReal,>,Poly) ... removes: 2
     W(x1,x2)	weight: 2 * x2 + x1
     T()	weight: 0
    B1()	weight: 0
     R(x1,x2)	weight: 2 * x2 + x1
    B2()	weight: (/ 1 4)
Number of strict rules: 0
YES