>>11429951No, you could also write the sentence out in propositional logic, and use the fact that (XOR, AND) is equivalent to Zmod2 to reduce the sentence until it has a sum of at most 2^n unique terms (possibly including '1'), where n is the number of atomic symbols in your original sentence. If it reduces to 1, it's a tautology, if it reduces to 0, it's always false, if it reduces to anything else, then you have your most simplified sentence equivalent to what you started with.
