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

Elapsed Time:  98.76 ms