NO
LCTRS
  Theories
    Core, Ints
  Sorts
    Result, Result1, Result2
  Signature
    hikaku: (Int, Int) -> Int
    max: (Int, Int) -> Result2
    min: (Int, Int) -> Result1
    return: Int -> Int
    return1: Int -> Result1
    return2: Int -> Result2
    sum2: (Int, Int) -> Int
    u1: (Int, Int, Int, Int) -> Int
    u2: (Int, Int, Int, Int, Result1) -> Int
    u3: (Int, Int, Int, Int, Result2) -> Int
  Rules
    max(?68, ?69) -> return2(?68) [>(?68, ?69)]
    max(?70, ?71) -> return2(?71) [not(>(?70, ?71))]
    min(?72, ?73) -> return1(?72) [>(?73, ?72)]
    min(?74, ?75) -> return1(?75) [not(>(?75, ?74))]
    sum2(?76, ?77) -> u1(?76, ?77, 0, ?78)
    u1(?79, ?80, ?81, ?82) -> return(0) [>(?79, ?80)]
    u1(?83, ?84, ?85, ?86) -> u2(?83, ?84, 0, ?86, min(?83, ?84)) [not(>(?83, ?84))]
    u2(?87, ?88, ?89, ?90, return1(?91)) -> u3(?87, ?88, ?89, ?91, max(?87, ?88))
    u3(?92, ?93, ?94, ?95, return2(?96)) -> return(?94) [<=(?95, ?96)]
    u3(?97, ?98, ?99, ?100, return2(?101)) -> u3(?97, ?98, +(?99, ?100), +(?100, 1), max(?97, ?98)) [not(<=(?100, ?101))]
Not confluent by "two different NFs found" with proof:
  * Critical Pair
    Inner Rule
      sum2(?76', ?77') -> u1(?76', ?77', 0, ?78')
    Outer Rule
      sum2(?76", ?77") -> u1(?76", ?77", 0, ?78")
    Pair
      u1(?76", ?77", 0, ?78') ≈ u1(?76", ?77", 0, ?78") [=(?78', ?78'), =(?78", ?78")]
  reaches the non-trivial normal form
    u1(?76", ?77", 0, ?78') ≈ u1(?76", ?77", 0, ?78") [?78' = ?78', ?78" = ?78"]

Elapsed Time: 106.22 ms