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

Elapsed Time:  72.93 ms