NO
LCTRS
  Theories
    Core, Ints
  Sorts
    Unit
  Signature
    fastfib: Int -> Unit
    return: Int -> Unit
    u: (Int, Int, Int, Int) -> Unit
  Rules
    fastfib(?23) -> u(?23, 1, 1, ?24)
    u(?25, ?26, ?27, ?28) -> return(?27) [not(>=(?25, 2))]
    u(?29, ?30, ?31, ?32) -> u(-(?29, 1), ?31, +(?31, ?30), +(?31, ?30)) [>=(?29, 2)]
Not confluent by "two different NFs found" with proof:
  * Critical Pair
    Inner Rule
      fastfib(?23') -> u(?23', 1, 1, ?24')
    Outer Rule
      fastfib(?23") -> u(?23", 1, 1, ?24")
    Pair
      u(?23", 1, 1, ?24') ≈ u(?23", 1, 1, ?24") [=(?24', ?24'), =(?24", ?24")]
  reaches the non-trivial normal form
    u(?23", 1, 1, ?24') ≈ u(?23", 1, 1, ?24") [?24' = ?24', ?24" = ?24"]

Elapsed Time:  92.26 ms