The output file contains the following four sections that  appear in the order shown:

a) Objective Value Section 

it is made of a single line starting with the letter “o” (lower case) and followed by the optimal solution value, which is the total weight of the clauses that are not satisfied by the variable assignment given in Section c). If the optimal solution is found [see Section b)], then this is the least possible value for such a weight.

b) Status Section

it is made of a single line starting with the letter “s” (lower case) and followed by one of the two strings: “OPTIMUM FOUND” and “UNKNOWN” . The string “UNKNOWN” is produced when the optimal solution could not be certified, typically for having reached the computing time limit. In this case the solution given in the sections a) and c) is the best found during the computation and is NOT GUARANTEED to be optimal.

c) Variable Section

it is made of a single line starting with the letter “v” (lower case) and followed by the list of values of the variables ordered from 1 to n.

d) Statistics Section

it starts with the string “c total running time: ” followed by the total running time in seconds