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 satisfied by the variable assignment given in Section c). If the optimal solution is found [see Section b)], then this is the largest 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 names of all variables. Those with a negative sign “-” prepended to the name have value 0 in the optimal solution, all the others have value 1

d) Statistics Section

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