YES
LCTRS
  Theories
    Core, Ints
  Signature
    f2: Int -> Int
    u_15: (Int, Int) -> Int
  Rules
    f2(?15) -> ?15 [<=(?15, 1)]
    f2(?16) -> u_15(?16, f2(-(?16, 1))) [>(?16, 1)]
    u_15(?17, ?18) -> +(?17, ?18) [distinct(?17, 10)]
    u_15(?19, ?20) -> 10 [?19 = 10]
Confluent by Weak Orthogonality with proof:
  no critical pairs

Elapsed Time:  72.06 ms