MAYBE
LCTRS
  Theories
    Core, Ints
  Signature
    f1: (Int, Int) -> Int
    u_11: (Int, Int) -> Int
    u_14: Int -> Int
    u_7: Int -> Int
  Rules
    u_14(!w_5) -> !w_5
    u_11(!m, !w_4) -> u_14(f1(-(!m, 1), !w_4))
    u_7(!w_3) -> !w_3
    f1(!m, !n) -> u_11(!m, f1(!m, -(!n, 1))) [and(distinct(!m, 0), or(<=(!m, 0), distinct(!n, 0)))]
    f1(!m, !n) -> u_7(f1(-(!m, 1), 1)) [and(and(distinct(!m, 0), >(!m, 0)), !n = 0)]
    f1(!m, !n) -> +(!n, 1) [!m = 0]
No termination info given.

Elapsed Time:  80.18 ms