YES
LCTRS
  Theories
    Core, Ints
  Signature
    f2: (Int, Int) -> Int
    u_16: Int -> Int
  Rules
    f2(?17, ?18) -> ?18 [?17 = 0]
    f2(?19, ?20) -> u_16(f2(-(?19, 1), +(?20, 1))) [and(distinct(?19, 0), distinct(?19, 1))]
    f2(?21, ?22) -> +(?22, 1) [and(distinct(?21, 0), ?21 = 1)]
    u_16(?23) -> ?23
Confluent by Orthogonality with proof:
  no critical pairs

Elapsed Time:  73.86 ms