YES

Problem:
 W(W(x)) -> W(x)
 B(I(x)) -> W(x)
 W(B(x)) -> B(x)
 F(H(x),y) -> F(H(x),G(y))
 F(x,I(y)) -> F(G(x),I(y))
 G(x) -> x

Proof:
 sorted: (order)
 0:F(H(x),y) -> F(H(x),G(y))
   F(x,I(y)) -> F(G(x),I(y))
   G(x) -> x
 1:W(W(x)) -> W(x)
   B(I(x)) -> W(x)
   W(B(x)) -> B(x)
 -----
 sorts
   [0>3, 1>2, 2>4, 3>4, 3>6, 4>5, 6>7]
 sort attachment (non-strict)
   W : 1 -> 1
   B : 2 -> 1
   I : 5 -> 4
   F : 3 x 3 -> 0
   H : 7 -> 6
   G : 3 -> 3
 -----
 0:F(H(x),y) -> F(H(x),G(y))
   F(x,I(y)) -> F(G(x),I(y))
   G(x) -> x
   Church Rosser Transformation Processor:
    strict:
     F(H(x),y) -> F(H(x),G(y))
     F(x,I(y)) -> F(G(x),I(y))
     G(x) -> x
    weak:
     
    critical peaks: 2
     F(H(x27),G(I(y))) <-0|[]- F(H(x27),I(y)) -1|[]-> F(G(H(x27)),I(y))
     F(G(H(x)),I(x30)) <-1|[]- F(H(x),I(x30)) -0|[]-> F(H(x),G(I(x30)))
    Closedness Processor (*strongly -- <=7 steps*):
     strict:
      
     weak:
      
     Qed
 
 
 1:W(W(x)) -> W(x)
   B(I(x)) -> W(x)
   W(B(x)) -> B(x)
   Church Rosser Transformation Processor (kb):
    W(W(x)) -> W(x)
    B(I(x)) -> W(x)
    W(B(x)) -> B(x)
    critical peaks: joinable
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [I](x0) = 3x0,
       
       [W](x0) = x0,
       
       [B](x0) = 3x0 + 4
      orientation:
       W(W(x)) = x >= x = W(x)
       
       B(I(x)) = 9x + 4 >= x = W(x)
       
       W(B(x)) = 3x + 4 >= 3x + 4 = B(x)
      problem:
       W(W(x)) -> W(x)
       W(B(x)) -> B(x)
      Matrix Interpretation Processor: dim=1
       
       interpretation:
        [W](x0) = 2x0 + 6,
        
        [B](x0) = 6x0 + 2
       orientation:
        W(W(x)) = 4x + 18 >= 2x + 6 = W(x)
        
        W(B(x)) = 12x + 10 >= 6x + 2 = B(x)
       problem:
        
       Qed