YES
LCTRS
  Theories
    Core, Ints
  Sorts
    Unit
  Signature
    fastfib: Int -> Unit
    return: Int -> Unit
    u: (Int, Int, Int, Int) -> Unit
  Rules
    u(!num, !f0, !f1, !f2) -> return(!f1) [not(>=(!num, 2))]
    u(!num, !f0, !f1, !f2) -> u(-(!num, 1), !f1, +(!f1, !f0), +(!f1, !f0)) [>=(!num, 2)]
    fastfib(!num) -> u(!num, 1, 1, !rnd)
* DPGraph approximation on the DP problem
  dependency pairs:
    {u#(!num, !f0, !f1, !f2) -> u#(-(!num, 1), !f1, +(!f1, !f0), +(!f1, !f0)) [>=(!num, 2)]
    , fastfib#(!num) -> u#(!num, 1, 1, !rnd)}
  rules:
    {u(!num, !f0, !f1, !f2) -> return(!f1) [not(>=(!num, 2))]
    , u(!num, !f0, !f1, !f2) -> u(-(!num, 1), !f1, +(!f1, !f0), +(!f1, !f0)) [>=(!num, 2)]
    , fastfib(!num) -> u(!num, 1, 1, !rnd)}
resulting in the DP graph
  DPGraph with indexed dependency pairs
    {1: u#(!num, !f0, !f1, !f2) -> u#(-(!num, 1), !f1, +(!f1, !f0), +(!f1, !f0)) [>=(!num, 2)]
    , 2: fastfib#(!num) -> u#(!num, 1, 1, !rnd)}
  and edges
    1 -> {1}
    2 -> {1}
with 1 SCC(s)
  SCC:
    {u#(!num, !f0, !f1, !f2) -> u#(-(!num, 1), !f1, +(!f1, !f0), +(!f1, !f0)) [>=(!num, 2)]}
* Value criterion after 1 iteration(s) with the projections:
  Iteration 1:
    projection(s):
      v(u#) = 1
    removing the rule(s):
      {u#(!num, !f0, !f1, !f2) -> u#(-(!num, 1), !f1, +(!f1, !f0), +(!f1, !f0)) [>=(!num, 2)]}

Elapsed Time:  22.89 ms