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

Elapsed Time:  39.95 ms