MAYBE
LCTRS
  Theories
    Core, Ints
  Signature
    sum: Int -> Int
    sum3: (Int, Int) -> Int
    sum_decl: Int -> Int
    u_3: (Int, Int) -> Int
  Rules
    sum3(!x, !n) -> +(!n, sum3(!x, +(!n, 1))) [>=(!x, !n)]
    sum3(!x, !n) -> 0 [<(!x, !n)]
    u_3(!z, !i) -> !z [<=(!i, 0)]
    u_3(!z, !i) -> u_3(+(!z, !i), -(!i, 1)) [>(!i, 0)]
    sum_decl(!x) -> u_3(0, !x)
    sum(!x) -> +(!x, sum(-(!x, 1))) [<=(0, -(!x, 1))]
    sum(!x) -> 0 [<=(!x, 0)]
No termination info given.

Elapsed Time:  72.47 ms