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(?46) -> u(?46, 1, 0, ?47, ?48)
    u(?49, ?50, ?51, ?52, ?53) -> return(0) [<=(?49, 0)]
    u(?54, ?55, ?56, ?57, ?58) -> v(?54, ?55, ?56, ?57, 1) [not(<=(?54, 0))]
    v(?59, ?60, ?61, ?62, ?63) -> return(?60) [not(<(?63, ?59))]
    v(?64, ?65, ?66, ?67, ?68) -> v(?64, +(?65, ?66), ?65, +(?65, ?66), +(?68, 1)) [<(?68, ?64)]
Not confluent by "two different NFs found" with proof:
  * Critical Pair
    Inner Rule
      fastfib(?46') -> u(?46', 1, 0, ?47', ?48')
    Outer Rule
      fastfib(?46") -> u(?46", 1, 0, ?47", ?48")
    Pair
      u(?46", 1, 0, ?47', ?48') ≈ u(?46", 1, 0, ?47", ?48") [=(?47', ?47'), =(?48', ?48'), =(?47", ?47"), =(?48", ?48")]
  reaches the non-trivial normal form
    u(?46", 1, 0, ?47', ?48') ≈ u(?46", 1, 0, ?47", ?48") [?47' = ?47', ?48' = ?48', ?47" = ?47", ?48" = ?48"]

Elapsed Time:  87.82 ms