Produce a satisfying assignment for a larger TfP-generated DIMACS CNF instance: 250 variables, 1065 clauses. Still easy for a real solver; impractical by hand.
A result is verified when the submitted assignment file, parsed as SAT-competition v-line format, assigns every variable of the bound CNF instance and satisfies all of its clauses. Assignments mentioning variables outside the instance are rejected. This establishes that the instance is satisfiable and that this assignment witnesses it. It does not establish that the assignment is unique or minimal.