YES
LCTRS
  Theories
    Core, FixedSizeBitVectors
  Signature
    cnt: BitVec 4 -> BitVec 4
    u1: (BitVec 4, BitVec 4, BitVec 4) -> BitVec 4
  Rules
    cnt(?14) -> u1(?14, #b0000, #b0000)
    u1(?15, ?16, ?17) -> ?17 [not(bvult(?16, ?15))]
    u1(?18, ?19, ?20) -> u1(?18, bvadd(?19, #b0001), bvadd(?20, #b0001)) [bvult(?19, ?18)]
Confluent by Strongly Closedness with proof:
  no critical pairs
Elapsed Time:  92.71 ms