MAYBE
LCTRS
  Theories
    Core, Ints
  Signature
    fact: Int -> Int
    return: Int -> Int
    u1: (Int, Int, Int) -> Int
    u2: (Int, Int, Int) -> Int
    u3: (Int, Int, Int) -> Int
  Rules
    fact(!x) -> u1(!x, !i, !z)
    u1(!x, !i, !z) -> u2(!x, 1, 1)
    u2(!x, !i, !z) -> u2(!x, +(!i, 1), *(!z, !i)) [<=(!i, !x)]
    u2(!x, !i, !z) -> u3(!x, !i, !z) [not(<=(!i, !x))]
    u3(!x, !i, !z) -> return(!z)
No termination info given.

Elapsed Time:  44.20 ms