YES
LCTRS
  Theories
    Core, Ints
  Signature
    f2: Int -> Int
    u_27: (Int, Int) -> Int
  Rules
    f2(?14) -> ?14 [<=(?14, 1)]
    f2(?15) -> u_27(?15, f2(-(?15, 2))) [>(?15, 1)]
    u_27(?16, ?17) -> +(+(?16, -(?16, 1)), ?17)
Confluent by Orthogonality with proof:
  no critical pairs

Elapsed Time:  69.15 ms