NO
LCTRS
  Theories
    Core, Ints
  Sorts
    Unit
  Signature
    fastfib: Int -> Unit
    p: (Int, Int, Int, Int, Int) -> Unit
    return: Int -> Unit
    u: (Int, Int, Int, Int, Int) -> Unit
    v: (Int, Int, Int, Int, Int) -> Unit
    w: (Int, Int, Int, Int, Int) -> Unit
  Rules
    fastfib(?86) -> u(?86, 1, 0, ?87, ?88)
    p(?89, ?90, ?91, ?92, ?93) -> p(?89, +(?90, ?91), ?90, ?90, +(?93, 1)) [<(?93, ?89)]
    p(?94, ?95, ?96, ?97, ?98) -> return(?95) [not(<(?98, ?94))]
    u(?99, ?100, ?101, ?102, ?103) -> v(?99, ?100, ?101, ?102, ?103) [<=(?99, 1)]
    u(?104, ?105, ?106, ?107, ?108) -> w(?104, ?105, ?106, ?107, ?108) [not(<=(?104, 1))]
    v(?109, ?110, ?111, ?112, ?113) -> return(?109) [not(<(?109, 0))]
    v(?114, ?115, ?116, ?117, ?118) -> return(0) [<(?114, 0)]
    w(?119, ?120, ?121, ?122, ?123) -> p(?119, ?120, ?121, ?122, 1) [not(>(?119, 46))]
    w(?124, ?125, ?126, ?127, ?128) -> return(-1) [>(?124, 46)]
Not confluent by "two different NFs found" with proof:
  * Critical Pair
    Inner Rule
      fastfib(?86') -> u(?86', 1, 0, ?87', ?88')
    Outer Rule
      fastfib(?86") -> u(?86", 1, 0, ?87", ?88")
    Pair
      u(?86", 1, 0, ?87', ?88') ≈ u(?86", 1, 0, ?87", ?88") [=(?87', ?87'), =(?88', ?88'), =(?87", ?87"), =(?88", ?88")]
  reaches the non-trivial normal form
    u(?86", 1, 0, ?87', ?88') ≈ u(?86", 1, 0, ?87", ?88") [?87' = ?87', ?88' = ?88', ?87" = ?87", ?88" = ?88"]

Elapsed Time: 106.67 ms