MAYBE
LCTRS
  Theories
    Core, Ints
  Signature
    sum: Int -> Int
    sum2: Int -> Int
    u1: (Int, Int, Int) -> Int
    u2: (Int, Int, Int, Int) -> Int
  Rules
    u1(!x, !i, !z) -> !z [not(<=(!i, !x))]
    u2(!x, !i, !j, !z) -> u1(!x, +(!i, 1), !z) [not(<(!j, !i))]
    u2(!x, !i, !j, !z) -> u2(!x, !i, +(!j, 1), +(!z, 1)) [<(!j, !i)]
    u1(!x, !i, !z) -> u2(!x, !i, 0, !z) [<=(!i, !x)]
    sum2(!x) -> u1(!x, 0, 0)
    sum(!x) -> +(!x, sum(-(!x, 1))) [<(0, !x)]
    sum(!x) -> 0 [<=(!x, 0)]
No termination info given.

Elapsed Time:  80.73 ms