MAYBE
LCTRS
  Theories
    Core, Ints
  Signature
    init: (Int, Int, Int) -> Int
    m: (Int, Int, Int) -> Int
    m0: (Int, Int, Int) -> Int
    m1: (Int, Int, Int) -> Int
    m2: (Int, Int, Int) -> Int
    m3: (Int, Int, Int) -> Int
    merge: (Int, Int, Int) -> Int
    split: (Int, Int, Int) -> Int
    tuple: (Int, Int, Int, Int) -> Int
  Rules
    init(!x, !y, !z) -> m(!x, !y, !z)
    m1(!x, !y, !z) -> m(!y, !y, !z)
    m0(!x, !y, !z) -> split(!x, !y, !z)
    m2(!x, !y, !z) -> m(!z, !y, !z)
    m3(!x, !y, !z) -> merge(!y, !z, !z)
    merge(!x, !y, !z) -> merge(-(!x, 1), !y, !z) [and(>=(!x, 1), >=(!y, 1))]
    split(!x, !y, !z) -> split(-(!x, 2), !y, !z) [>=(!x, 2)]
    merge(!x, !y, !z) -> merge(!x, -(!y, 1), !z) [and(>=(!x, 1), >=(!y, 1))]
    m(!x, !y, !z) -> tuple(m0(!x, !u, !v), m1(!x, !u, !v), m2(!x, !u, !v), m3(!x, !u, !v)) [and(>=(!x, 2), and(>=(!u, 0), and(>=(!v, 0), and(>=(+(!x, 1), *(2, !u)), and(>=(*(2, !u), !x), and(>=(!x, *(2, !v)), >=(+(*(2, !v), 1), !x)))))))]
No termination info given.

Elapsed Time: 214.41 ms