MAYBE
LCTRS
  Theories
    Core, Ints
  Signature
    U2: (Int, Int, Int, Int) -> Int
    U7: (Int, Int, Int, Int) -> Int
    ackermann: (Int, Int) -> Int
  Rules
    ackermann(!x, !y) -> U2(!x, !y, !x, !y)
    U7(!x, !y, !m, !n) -> U7(!x, !y, -(!m, 1), 1) [and(<=(!n, 0), >(!m, 0))]
    U7(!x, !y, !m, !n) -> +(!n, 1) [and(<=(!n, 0), not(>(!m, 0)))]
    U7(!x, !y, !m, !n) -> U7(!x, !y, -(!m, 1), U2(!m, -(!n, 1), !m, -(!n, 1))) [and(not(<=(!n, 0)), >(!m, 0))]
    U7(!x, !y, !m, !n) -> +(!n, 1) [and(not(<=(!n, 0)), not(>(!m, 0)))]
    U2(!x, !y, !m, !n) -> 0 [or(<(!y, 0), <(!x, 0))]
    U2(!x, !y, !m, !n) -> U7(!x, !y, !m, !n) [and(not(or(<(!y, 0), <(!x, 0))), >(!m, 0))]
    U2(!x, !y, !m, !n) -> +(!n, 1) [and(not(or(<(!y, 0), <(!x, 0))), not(>(!m, 0)))]
No termination info given.

Elapsed Time: 288.04 ms