c
c The file format read by NB-satz consists of 0 or more comment lines, then a
c line giving the number of variables, clauses and the domain size, and then
c the clauses themselves. Comment lines start with the letter 'c' and continue
c to the end of the line. The next non-empty line after the comments should be:
c
c   nb cnf NUM_VARIABLES NUM_CLAUSES DOMAIN_SIZE
c
c The clauses should immediately follow this line. Each clause is a list of
c variables paired with certain values from the domain (all variables
c implicitly have the same domain). Variables are integers between 1 and
c NUM_VARIABLES inclusive. Domain values are integers beween 0 and
c DOMAIN_SIZE-1 inclusive. Clauses are terminated by the special value 0 (which
c is why variables start at 1). Additionally, clauses and value sets must be
c non-empty (there must be at least 1 variable-value pair in each clause and at
c least 1 value in each value set). An example clause is:
c
c   1{0,1,2} 2{1,2} 3{0} 0
c
c Note that formulas that contain negated value sets can be re-written as
c formulas that contain only positive value sets. Negated value sets are not
c accepted by NB-satz.
c
c   nb cnf 1 1 4
c   1!{2} 0
c
c The above formula can be re-written as:
c
c   nb cnf 1 1 4
c   1{0,1,3} 0
c
c
c The formula contained in this file is a simple 3-node fully connected graph
c colouring problem with 3 colours.
c
nb cnf 3 9 3
1{1,2} 2{1,2} 0
1{0,2} 2{0,2} 0
1{0,1} 2{0,1} 0
1{1,2} 3{1,2} 0
1{0,2} 3{0,2} 0
1{0,1} 3{0,1} 0
2{1,2} 3{1,2} 0
2{0,2} 3{0,2} 0
2{0,1} 3{0,1} 0