The Tautology and Contradiction commands test whether the given Boolean expression b is a tautology or a contradiction.

The Tautology(b) calling sequence returns true if b is a tautology (true for every valuation of its variables) and false otherwise.  Similarly, Contradiction(b) returns true if b is a contradiction (false for every valuation of its variables) and false otherwise.

If the parameter p is supplied and the test returns false, then a valuation is assigned to p which demonstrates a negative result. Otherwise, p is assigned NULL. Note that the test may be significantly faster if p is not given.