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
  Rules
    fastfib(?60) -> u(?60, ?61, ?62, ?63, ?64)
    u(?65, ?66, ?67, ?68, ?69) -> return(0) [<=(?65, 0)]
    u(?70, ?71, ?72, ?73, ?74) -> return(1) [and(not(<=(?70, 0)), ?70 = 1)]
    u(?75, ?76, ?77, ?78, ?79) -> v(?75, 1, 1, 3, ?79) [and(not(<=(?75, 0)), not(?75 = 1))]
    v(?80, ?81, ?82, ?83, ?84) -> return(?82) [not(<=(?83, ?80))]
    v(?85, ?86, ?87, ?88, ?89) -> v(?85, ?87, +(?87, ?86), +(?88, 1), ?86) [<=(?88, ?85)]
Not confluent by "two different NFs found" with proof:
  * Critical Pair
    Inner Rule
      fastfib(?60') -> u(?60', ?61', ?62', ?63', ?64')
    Outer Rule
      fastfib(?60") -> u(?60", ?61", ?62", ?63", ?64")
    Pair
      u(?60", ?61', ?62', ?63', ?64') ≈ u(?60", ?61", ?62", ?63", ?64") [=(?61', ?61'), =(?62', ?62'), =(?63', ?63'), =(?64', ?64'), =(?61", ?61"), =(?62", ?62"), =(?63", ?63"), =(?64", ?64")]
  reaches the non-trivial normal form
    u(?60", ?61', ?62', ?63', ?64') ≈ u(?60", ?61", ?62", ?63", ?64") [?61' = ?61', ?62' = ?62', ?63' = ?63', ?64' = ?64', ?61" = ?61", ?62" = ?62", ?63" = ?63", ?64" = ?64"]

Elapsed Time: 102.20 ms