Each line of the file is a function. Each line has the following
form:

`<grouping> ... <grouping> = [0|1]`

where `<grouping>` has the form

`<variable>...<variable>`

and `<variable>` has the form

`x<number>`

where `<number>` is a positive integer no greater than
`<max-var-number>`. The following are examples:

`x1 x2 x3 = 1`
`x1x2x3 = 1`
`x1x2x3 x2x3 x4x5x6 = 0`

`sbsat` interprets a line as an `xor` of conjunctions, each
consisting of variables identified in a `<grouping>`. The
following table shows the above as expressions in canonical form:

This ... |
is equivalent to this |

x1 x2 x3 = 1 |
equ( xor(1, 2, 3), T) |

x1x2x3 = 1 |
equ( and(1, 2, 3), T) |

x1x2x3 x2x3 x4x5x6 = 0 |
equ(xor(and(1, 2, 3), and(2, 3), and(4, 5, 6)), F) |

John Franco 2011-09-15