To run this example, you need a BIG xterm -- 260 by 130. I use the command:

  xterm -fn "-misc-fixed-*-*-*-*-7-*-*-*-*-*-*-*"  -geometry 260x130

Again, black background is required. Run 'run.sh' to start the demo. Clauses
are represented by a list of letters. Capital letters are positive literals,
lower case letters are negative literal. Since there are only 26 letters,
several literals are represented by the same letter (just by a 'modulus 26'
operatation).

The example was taken from the old "satlib" page, supposedly a BMC problem.

// Niklas
