YES
LCTRS
  Theories
    Core, Ints
  Sorts
    Result, Unit
  Signature
    ditch_globals: Unit -> Result
    return: (Int, Int, Int) -> Unit
    return1: Int -> Result
    sum1: (Int, Int, Int) -> Unit
    u: (Int, Int, Int) -> Unit
  Rules
    ditch_globals(return(?30, ?31, ?32)) -> return1(?32)
    sum1(?33, ?34, ?35) -> return(?34, ?35, 0) [<(?33, 0)]
    sum1(?36, ?37, ?38) -> u(?36, 0, 0) [not(<(?36, 0))]
    u(?39, ?40, ?41) -> return(?40, ?41, ?41) [not(<=(?40, ?39))]
    u(?42, ?43, ?44) -> u(?42, +(?43, 1), +(?44, ?43)) [<=(?43, ?42)]
Confluent by Development Closedness with proof:
  no critical pairs

Elapsed Time:  75.24 ms