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

Elapsed Time: 120.31 ms