NO
LCTRS
  Theories
    Core, Ints
  Sorts
    Unit
  Signature
    fastfib: Int -> Unit
    return: Int -> Unit
    u: (Int, Int, Int, Int, Int) -> Unit
    v: (Int, Int, Int, Int, Int) -> Unit
    w: (Int, Int, Int, Int, Int) -> Unit
  Rules
    fastfib(?86) -> u(?86, 1, 0, ?87, ?88)
    u(?89, ?90, ?91, ?92, ?93) -> return(-1) [<(?89, 0)]
    u(?94, ?95, ?96, ?97, ?98) -> return(0) [and(not(<(?94, 0)), ?94 = 0)]
    u(?99, ?100, ?101, ?102, ?103) -> return(1) [and(and(not(<(?99, 0)), not(?99 = 0)), ?99 = 1)]
    u(?104, ?105, ?106, ?107, ?108) -> v(?104, ?105, ?106, ?107, 1) [and(and(not(<(?104, 0)), not(?104 = 0)), not(?104 = 1))]
    v(?109, ?110, ?111, ?112, ?113) -> return(?112) [not(<(?113, ?109))]
    v(?114, ?115, ?116, ?117, ?118) -> w(?114, ?115, ?116, +(?115, ?116), ?118) [<(?118, ?114)]
    w(?119, ?120, ?121, ?122, ?123) -> return(-2) [<(?122, ?120)]
    w(?124, ?125, ?126, ?127, ?128) -> v(?124, ?127, ?125, ?127, +(?128, 1)) [not(<(?127, ?125))]
Not confluent by "two different NFs found" with proof:
  * Critical Pair
    Inner Rule
      fastfib(?86') -> u(?86', 1, 0, ?87', ?88')
    Outer Rule
      fastfib(?86") -> u(?86", 1, 0, ?87", ?88")
    Pair
      u(?86", 1, 0, ?87', ?88') ≈ u(?86", 1, 0, ?87", ?88") [=(?87', ?87'), =(?88', ?88'), =(?87", ?87"), =(?88", ?88")]
  reaches the non-trivial normal form
    u(?86", 1, 0, ?87', ?88') ≈ u(?86", 1, 0, ?87", ?88") [?87' = ?87', ?88' = ?88', ?87" = ?87", ?88" = ?88"]

Elapsed Time:  92.90 ms