YES
LCTRS
  Theories
    Core, Ints
  Signature
    f1: (Int, Int) -> Int
    u_11: (Int, Int) -> Int
    u_14: Int -> Int
    u_7: Int -> Int
  Rules
    f1(?29, ?30) -> +(?30, 1) [?29 = 0]
    f1(?31, ?32) -> u_11(?31, f1(?31, -(?32, 1))) [and(distinct(?31, 0), or(<=(?31, 0), distinct(?32, 0)))]
    f1(?33, ?34) -> u_7(f1(-(?33, 1), 1)) [and(and(distinct(?33, 0), >(?33, 0)), ?34 = 0)]
    u_11(?35, ?36) -> u_14(f1(-(?35, 1), ?36))
    u_14(?37) -> ?37
    u_7(?38) -> ?38
Confluent by Orthogonality with proof:
  no critical pairs

Elapsed Time:  74.02 ms