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

Elapsed Time: 104.28 ms