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

Elapsed Time:  43.38 ms