NO
LCTRS
  Theories
    Core, Ints
  Sorts
    Result
  Signature
    return: Int -> Result
    sum1: Int -> Result
    u: (Int, Int, Int) -> Result
    v: (Int, Int, Int) -> Result
    w: (Int, Int, Int) -> Result
  Rules
    sum1(?40) -> u(?40, ?41, 0)
    u(?42, ?43, ?44) -> return(0) [<(?42, 0)]
    u(?45, ?46, ?47) -> v(?45, 0, ?47) [not(<(?45, 0))]
    v(?48, ?49, ?50) -> v(?48, +(?49, 1), +(?50, ?49)) [and(<=(?49, ?48), >=(?50, 0))]
    v(?51, ?52, ?53) -> w(?51, ?52, ?53) [not(and(<=(?52, ?51), >=(?53, 0)))]
    w(?54, ?55, ?56) -> return(?56) [not(<(?56, 0))]
    w(?57, ?58, ?59) -> return(-1) [<(?59, 0)]
Not confluent by "two different NFs found" with proof:
  * Critical Pair
    Inner Rule
      sum1(?40') -> u(?40', ?41', 0)
    Outer Rule
      sum1(?40") -> u(?40", ?41", 0)
    Pair
      u(?40", ?41', 0) ≈ u(?40", ?41", 0) [=(?41', ?41'), =(?41", ?41")]
  reaches the non-trivial normal form
    u(?40", ?41', 0) ≈ u(?40", ?41", 0) [?41' = ?41', ?41" = ?41"]

Elapsed Time: 101.69 ms