YES

Problem:
 C(x) -> c(x)
 c(c(x)) -> x
 b(b(x)) -> B(x)
 B(B(x)) -> b(x)
 c(B(c(b(c(x))))) -> B(c(b(c(B(c(b(x)))))))
 b(B(x)) -> x
 B(b(x)) -> x
 c(C(x)) -> x
 C(c(x)) -> x

Proof:
 Church Rosser Transformation Processor:
  strict:
   
  weak:
   
  critical peaks: 21
   c(c(x)) <-0|0[]- c(C(x)) -7|[]-> x
   c(c(x)) <-0|[]- C(c(x)) -8|[]-> x
   c(x183) <-1|0[]- c(c(c(x183))) -1|[]-> c(x183)
   c(B(c(b(x184)))) <-1|0,0,0,0[]- c(B(c(b(c(c(x184)))))) -4|[]-> B(c(b(c(B(c(b(c(x184))))))))
   C(x185) <-1|0[]- C(c(c(x185))) -8|[]-> c(x185)
   b(B(x186)) <-2|0[]- b(b(b(x186))) -2|[]-> B(b(x186))
   B(B(x187)) <-2|0[]- B(b(b(x187))) -6|[]-> b(x187)
   B(b(x188)) <-3|0[]- B(B(B(x188))) -3|[]-> b(B(x188))
   b(b(x189)) <-3|0[]- b(B(B(x189))) -5|[]-> B(x189)
   c(B(c(b(c(B(c(b(x190)))))))) <-4|0[]- c(c(B(c(b(c(x190)))))) -1|[]-> B(c(b(c(x190))))
   c(B(c(b(B(c(b(c(B(c(b(x191))))))))))) <-4|0,0,0,0[]- c(B(c(b(c(B(c(b(c(x191))))))))) -4|
                                                        []-> B(c(b(c(B(c(b(B(c(b(c(x191)))))))))))
   C(B(c(b(c(B(c(b(x192)))))))) <-4|0[]- C(c(B(c(b(c(x192)))))) -8|[]-> B(c(b(c(x192))))
   b(x193) <-5|0[]- b(b(B(x193))) -2|[]-> B(B(x193))
   B(x194) <-5|0[]- B(b(B(x194))) -6|[]-> B(x194)
   B(x195) <-6|0[]- B(B(b(x195))) -3|[]-> b(b(x195))
   b(x196) <-6|0[]- b(B(b(x196))) -5|[]-> b(x196)
   c(x197) <-7|0[]- c(c(C(x197))) -1|[]-> C(x197)
   c(B(c(b(x198)))) <-7|0,0,0,0[]- c(B(c(b(c(C(x198)))))) -4|[]-> B(c(b(c(B(c(b(C(x198))))))))
   C(x199) <-7|0[]- C(c(C(x199))) -8|[]-> C(x199)
   x200 <-8|[]- C(c(x200)) -0|[]-> c(c(x200))
   c(x201) <-8|0[]- c(C(c(x201))) -7|[]-> c(x201)
  Redundant Rules Transformation:
   C(x) -> c(x)
   c(c(x)) -> x
   b(b(x)) -> B(x)
   B(B(x)) -> b(x)
   c(B(c(b(c(x))))) -> B(c(b(c(B(c(b(x)))))))
   b(B(x)) -> x
   B(b(x)) -> x
   Church Rosser Transformation Processor (kb):
    C(x) -> c(x)
    c(c(x)) -> x
    b(b(x)) -> B(x)
    B(B(x)) -> b(x)
    c(B(c(b(c(x))))) -> B(c(b(c(B(c(b(x)))))))
    b(B(x)) -> x
    B(b(x)) -> x
    critical peaks: joinable
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [B](x0) = x0,
      
      [b](x0) = x0,
      
      [c](x0) = 2x0 + 3,
      
      [C](x0) = 4x0 + 3
     orientation:
      C(x) = 4x + 3 >= 2x + 3 = c(x)
      
      c(c(x)) = 4x + 9 >= x = x
      
      b(b(x)) = x >= x = B(x)
      
      B(B(x)) = x >= x = b(x)
      
      c(B(c(b(c(x))))) = 8x + 21 >= 8x + 21 = B(c(b(c(B(c(b(x)))))))
      
      b(B(x)) = x >= x = x
      
      B(b(x)) = x >= x = x
     problem:
      C(x) -> c(x)
      b(b(x)) -> B(x)
      B(B(x)) -> b(x)
      c(B(c(b(c(x))))) -> B(c(b(c(B(c(b(x)))))))
      b(B(x)) -> x
      B(b(x)) -> x
     Bounds Processor:
      bound: 1
      enrichment: match
      automaton:
       final states: {2,5,4,3,1}
       transitions:
        f40() -> 2*
        c0(7) -> 8*
        c0(2) -> 1*
        c0(9) -> 10*
        c0(4) -> 6*
        B0(10) -> 5*
        B0(2) -> 3*
        B0(6) -> 7*
        b0(2) -> 4*
        b0(8) -> 9*
        b1(11) -> 12*
        2 -> 4*
        3 -> 4*
        4 -> 3*
        5 -> 6,1,8
        10 -> 11,9
        12 -> 7*
      problem:
       
      Qed