MAYBE
LCTRS
  Theories
    Core, Ints
  Sorts
    Result
  Signature
    return: Int -> Result
    sum1: Int -> Result
    u: (Int, Int, Int) -> Result
    v: (Int, Int, Int) -> Result
    w: (Int, Int, Int) -> Result
  Rules
    w(!n, !i, !s) -> return(!s) [not(<(!s, 0))]
    w(!n, !i, !s) -> return(-1) [<(!s, 0)]
    v(!n, !i, !s) -> w(!n, !i, !s) [not(and(<=(!i, !n), >=(!s, 0)))]
    v(!n, !i, !s) -> v(!n, +(!i, 1), +(!s, !i)) [and(<=(!i, !n), >=(!s, 0))]
    u(!n, !i, !s) -> v(!n, 0, !s) [not(<(!n, 0))]
    u(!n, !i, !s) -> return(0) [<(!n, 0)]
    sum1(!n) -> u(!n, !rnd, 0)
No termination info given.

Elapsed Time:  54.62 ms