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

Elapsed Time: 100.84 ms