MAYBE LCTRS Theories Core, Ints Sorts Result Signature return: Int -> Result sum1: Int -> Result u: (Int, Int, Int) -> Result v: (Int, Int, Int) -> Result Rules v(!n, !i, !s) -> return(!s) [not(>(-(!n, !i), 0))] v(!n, !i, !s) -> v(!n, +(!i, 1), +(!s, -(!n, !i))) [>(-(!n, !i), 0)] u(!n, !i, !s) -> v(!n, 0, !s) [>(!n, 0)] u(!n, !i, !s) -> return(0) [<=(!n, 0)] sum1(!n) -> u(!n, !rnd, 0) No termination info given. Elapsed Time: 43.31 ms