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

Elapsed Time:  92.85 ms