3See [110] for several alternative equational specifications besides BOOL-OPS, as well as a detailed explanation of how satisfying assignments for satisfiable expressions can be obtained in an equational manner.