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

Elapsed Time:  54.72 ms