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

Elapsed Time:  96.50 ms