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

Elapsed Time:  45.29 ms