Generate the first (next) solution for the given query. The return value
is TRUE if a solution was found, or FALSE to
indicate the query could not be proven. This function may be called
repeatedly until it fails to generate all solutions to the query.