MAYBE
LCTRS
  Theories
    Core, Ints
  Sorts
    Result, Result1, Result2
  Signature
    hikaku: (Int, Int) -> Int
    max: (Int, Int) -> Result2
    min: (Int, Int) -> Result1
    return: Int -> Int
    return1: Int -> Result1
    return2: Int -> Result2
    sum2: (Int, Int) -> Int
    u1: (Int, Int, Int, Int) -> Int
    u2: (Int, Int, Int, Int, Result1) -> Int
    u3: (Int, Int, Int, Int, Result2) -> Int
  Rules
    u3(!x, !y, !t, !i, return2(!k)) -> u3(!x, !y, +(!t, !i), +(!i, 1), max(!x, !y)) [not(<=(!i, !k))]
    u3(!x, !y, !t, !i, return2(!k)) -> return(!t) [<=(!i, !k)]
    u2(!x, !y, !t, !i, return1(!k)) -> u3(!x, !y, !t, !k, max(!x, !y))
    u1(!x, !y, !t, !i) -> u2(!x, !y, 0, !i, min(!x, !y)) [not(>(!x, !y))]
    u1(!x, !y, !t, !i) -> return(0) [>(!x, !y)]
    sum2(!x, !y) -> u1(!x, !y, 0, !rnd)
    min(!x, !y) -> return1(!y) [not(>(!y, !x))]
    min(!x, !y) -> return1(!x) [>(!y, !x)]
    max(!x, !y) -> return2(!y) [not(>(!x, !y))]
    max(!x, !y) -> return2(!x) [>(!x, !y)]
No termination info given.

Elapsed Time:  62.28 ms