MAYBE
LCTRS
  Theories
    Core, Ints
  Sorts
    Result, Unit
  Signature
    ditch_globals: Unit -> Result
    return: (Int, Int, Int) -> Unit
    return1: Int -> Result
    sum1: (Int, Int, Int) -> Unit
    u: (Int, Int, Int) -> Unit
  Rules
    ditch_globals(return(!x, !y, !z)) -> return1(!z)
    u(!num, !i, !answer) -> return(!i, !answer, !answer) [not(<=(!i, !num))]
    u(!num, !i, !answer) -> u(!num, +(!i, 1), +(!answer, !i)) [<=(!i, !num)]
    sum1(!num, !i, !answer) -> u(!num, 0, 0) [not(<(!num, 0))]
    sum1(!num, !i, !answer) -> return(!i, !answer, 0) [<(!num, 0)]
No termination info given.

Elapsed Time:  45.15 ms