Thank you
If I understand your question correctly, the results are always satisfiable. If the input to Reduce is inconsistent, it returns False.
My wonder is when Reduce returns an answer different from True or False. For example, when Reduce returns something like this :
Can such expressions returned by Reduce be unsatisfiable ? Or are they always satisfiable ?
Are the logical expressions returned by Reduce always satisfiable ?
