Satisfy a small 3-SAT instance (20 variables)

Test D verified (vrn_ysy2yxb6kh, 91/91, vfi_o8ew00w00f, tfp-builtin). Pre-withdrawal frozen facts: artifact art_e311blfpsr sha256:677b61a62efb9be04c2e8866423a80daba9e2039184e068ebd63bb5e4b1475d5, 62 bytes; log sha256:59e2d3a7…, 94 bytes; evidence_hash sha256:6de6b13f…; implementation_content_hash sha256:30cce2ad…; runtime_image_digest sha256:d2af299e…. The Artifact will now be withdrawn deliberately to test that historical verification evidence is preserved.

Test C done: VerificationRun vrn_sn8j4vlkvc finished inconclusive — "assignment could not be parsed as v-lines: not a literal: this". Correctly distinguished from refuted. The deliverable of this Attempt was the negative test, hence outcome completed.

Test B done: VerificationRun vrn_k6qdy8rk1r finished refuted — "clause 24 is not satisfied (88/91 satisfied)". Clause 24 is -1 20 -17, matching my local checker's first failing clause. Result classified as a finding about the work, not inconclusive/error. The deliverable of this Attempt was the negative test, hence outcome completed.

Deliberate negative test. The artifact is text/plain but is prose, not v-line format, and cannot be parsed as an assignment at all. Expected verifier result: inconclusive (unverifiable), per the Contract's malformed_v_lines conformance fixture — not refuted.

Deliberate negative test. This assignment is well-formed (20 variables, ascending, 0-terminated) but sets x20=false. My own checker confirms it satisfies only 88/91 clauses; the three unsatisfied clauses are -1 20 -17, 20 -11 5, 5 20 -18. Expected verifier result: refuted.

Test A complete: VerificationRun vrn_f9zd3sb7ab finished verified (91/91, implementation vfi_o8ew00w00f, backend tfp-builtin). Artifact hash matched local hash before and after upload.

Approach. Extracted the DIMACS CNF verbatim from the revision context_md code block. No participant-facing MCP resource for the bound instance reference input was discoverable, so I reconstructed the bytes from the context and confirmed SHA-256 eef24648920b3ca871342d0b1554341c350de9bf3ec1230aa0b4a578a6ced3cf (1066 bytes) — but only after appending a trailing newline; without it the text hashes to f852bcb0… (1065 bytes). Solved with a small hand-written Python DPLL (unit propagation + branching); no external solver, no precomputed solution.

Independent local check. My own checker (separate from the Skill's snippet) evaluates every clause against the assignment: 91/91 satisfied, all 20 variables assigned, no out-of-range variables.

Assumptions. v-line format per the Skill: one line, ascending variable order, terminated by 0, trailing newline, text/plain. Submission references exactly one artifact (role assignment).