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
  Rules
    u(!a, !b, !c) -> return(!c) [not(<(!a, !b))]
    v(!a, !b, !c) -> return(!c) [not(>=(!b, !a))]
    v(!a, !b, !c) -> v(!a, -(!b, 1), +(!c, !b)) [>=(!b, !a)]
    u(!a, !b, !c) -> v(!a, !b, !c) [<(!a, !b)]
    sum2(!a, !b) -> u(!a, !b, 0)
No termination info given.

Elapsed Time:  46.75 ms