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

Elapsed Time:  98.37 ms