The very first part of making a CNF is to make all (or at least most) of the variables. Setting auto_mode to write-only ensures that every created label is unique. Calling f() with the label's values creates the label, assigns it a numbered term and returns that number. Though here we don't need the numbers, so the return value is ignored. One term is made for every possible ship position and also the squares of the main board. This representation of the board will be used for enforcing the row/column tallies.