MAYBE
LCTRS
  Theories
    Core, Ints
  Signature
    geq: (Int, Int) -> Bool
    plus: (Int, Int) -> Int
    sum: Int -> Int
    sum2: (Bool, Int) -> Int
  Rules
    sum(!x) -> sum2(geq(0, !x), !x)
    sum2(true, !x) -> 0
    sum2(false, !x) -> plus(!x, sum(plus(!x, -1)))
    plus(!n, !m) -> !k [+(!n, !m) = !k]
    geq(!n, !m) -> true [>=(!n, !m)]
    geq(!n, !m) -> false [<(!n, !m)]
No termination info given.

Elapsed Time:  38.38 ms