YES
LCTRS
  Theories
    Core, Ints
  Signature
    f1: Int -> Int
    u_13: (Int, Int, Int) -> Int
  Rules
    f1(?30) -> ?30 [<=(?30, 1)]
    f1(?31) -> u_13(?31, -(?31, 1), f1(-(-(?31, 1), 1))) [and(>(?31, 1), >(-(?31, 1), 1))]
    f1(?32) -> +(?32, -(?32, 1)) [and(>(?32, 1), <=(-(?32, 1), 1))]
    u_13(?33, ?34, ?35) -> +(?33, +(?34, ?35))
Confluent by Orthogonality with proof:
  no critical pairs

Elapsed Time:  52.00 ms