YES
LCTRS
  Theories
    Core, Ints
  Signature
    f2: Int -> Int
    u_10: Int -> Int
    u_15: Int -> Int
  Rules
    f2(?13) -> u_10(f2(-(?13, 2))) [>(?13, 1)]
    f2(?14) -> u_15(?14) [<=(?14, 1)]
    u_10(?15) -> u_15(+(?15, 2))
    u_15(?16) -> ?16 [>=(?16, 0)]
    u_15(?17) -> 0 [<(?17, 0)]
Confluent by Almost Development Closedness with proof:
  no critical pairs

Elapsed Time:  38.65 ms