YES
LCTRS
  Theories
    Core, Ints
  Signature
    f1: Int -> Int
    u_5: (Int, Int) -> Int
  Rules
    f1(?11) -> ?11 [<=(?11, 0)]
    f1(?12) -> u_5(?12, f1(-(?12, 1))) [>(?12, 0)]
    u_5(?13, ?14) -> +(?13, ?14)
Confluent by Orthogonality with proof:
  no critical pairs

Elapsed Time:  43.46 ms