This input format is only for expressing Conjunctive Normal Form or ``product of sums'' formulas. Variables are represented as positive integers. All top-level Boolean functions are disjunctions or clauses. There is one clause per line of file. A solution to the problem defined in a file is an assignment satisfying all clauses. There are no manipulators or directives in this format. This format is well-known as the DIMACS format10.