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

Elapsed Time:  95.00 ms