YES
LCTRS
  Theories
    Core, Ints
  Signature
    fact: Int -> Int
    return: Int -> Int
    u1: (Int, Int, Int) -> Int
    u2: (Int, Int, Int) -> Int
    u3: (Int, Int, Int) -> Int
  Rules
    fact(?30) -> u1(?30, ?31, ?32)
    u1(?33, ?34, ?35) -> u2(?33, 1, 1)
    u2(?36, ?37, ?38) -> u2(?36, +(?37, 1), *(?38, ?37)) [<=(?37, ?36)]
    u2(?39, ?40, ?41) -> u3(?39, ?40, ?41) [not(<=(?40, ?39))]
    u3(?42, ?43, ?44) -> return(?44)
Confluent by Almost Development Closedness with proof:
    * Critical Pair
      Inner Rule
        Pos ε: fact(?30') -> u1(?30', ?31', ?32')
      Outer Rule
        fact(?30") -> u1(?30", ?31", ?32")
      Pair
        u1(?30", ?31', ?32') ≈ u1(?30", ?31", ?32") [?31' = ?31', ?32' = ?32', ?31" = ?31", ?32" = ?32"]
    which reaches the trivial constrained equation
      u1(?30", ?31', ?32') ≈ u1(?30", ?31", ?32") [?31' = ?31', ?32' = ?32', ?31" = ?31", ?32" = ?32"]
        -o-> u2(?30", 1, 1) ≈ u1(?30", ?31", ?32") [?31' = ?31', ?32' = ?32', ?31" = ?31", ?32" = ?32"]
        -o-> u2(?30", 1, 1) ≈ u2(?30", 1, 1) [?31' = ?31', ?32' = ?32', ?31" = ?31", ?32" = ?32"]

Elapsed Time:  82.39 ms