YES
LCTRS
  Theories
    Core, Ints
  Signature
    fact: Int -> Int
  Rules
    fact(!x) -> 1 [<=(!x, 0)]
    fact(!x) -> *(fact(-(!x, 1)), !x) [>=(-(!x, 1), 0)]
DPGraph with indexed dependency pairs
  {1: fact#(!x) -> fact#(-(!x, 1)) [>=(-(!x, 1), 0)]}
and edges
  1 -> {1}
with 1 SCC(s)
  SCC:
    {fact#(!x) -> fact#(-(!x, 1)) [>=(-(!x, 1), 0)]}
Value criterion after 1 iteration(s) with the projections:
  Iteration 1:
    projection(s):
      v(fact#) = 1
    removing the rule(s):
      {fact#(!x) -> fact#(-(!x, 1)) [>=(-(!x, 1), 0)]}

Elapsed Time:  37.34 ms