MAYBE
LCTRS
  Theories
    Core, Ints
  Signature
    f2: (Int, Int) -> Int
    u_25: Int -> Int
    u_31: (Int, Int) -> Int
    u_34: Int -> Int
  Rules
    u_34(!w_10) -> !w_10
    u_31(!m, !w_9) -> u_34(f2(-(!m, 1), !w_9))
    u_25(!w_8) -> !w_8
    f2(!m, !n) -> u_31(!m, f2(!m, -(!n, 1))) [and(or(<=(!m, 0), distinct(!n, 0)), distinct(!m, 0))]
    f2(!m, !n) -> +(!n, 1) [and(or(<=(!m, 0), distinct(!n, 0)), !m = 0)]
    f2(!m, !n) -> u_25(f2(-(!m, 1), 1)) [and(>(!m, 0), !n = 0)]
No termination info given.

Elapsed Time:  85.74 ms