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

Elapsed Time:  91.99 ms