NO
LCTRS
  Theories
    Core, Ints
  Sorts
    Result
  Signature
    return: Int -> Result
    sum1: Int -> Result
    u: (Int, Int) -> Result
    v: (Int, Int) -> Result
  Rules
    sum1(?23) -> u(?23, ?24)
    u(?25, ?26) -> return(0) [<(?25, 0)]
    u(?27, ?28) -> v(?27, 0) [not(<(?27, 0))]
    v(?29, ?30) -> return(?30) [not(>(?29, 0))]
    v(?31, ?32) -> v(-(?31, 1), +(?32, ?31)) [>(?31, 0)]
Not confluent by "two different NFs found" with proof:
  * Critical Pair
    Inner Rule
      sum1(?23') -> u(?23', ?24')
    Outer Rule
      sum1(?23") -> u(?23", ?24")
    Pair
      u(?23", ?24') ≈ u(?23", ?24") [=(?24', ?24'), =(?24", ?24")]
  reaches the non-trivial normal form
    u(?23", ?24') ≈ u(?23", ?24") [?24' = ?24', ?24" = ?24"]

Elapsed Time:  98.65 ms