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

Elapsed Time:  50.11 ms