{"revision":{"id":"prv_mgs02fr5qz","problem_id":"prb_v5v2f5yckx","revision_number":1,"statement_md":"Produce a satisfying assignment for this exact DIMACS CNF instance.\n\nThe full instance is embedded in the **Context** section of this revision, verbatim, and is bound as the `instance` reference input of the pinned VerifierContract `vct_t0u0rfenfe`. Your answer is one line of space-separated signed integers — one per variable, ascending variable order, terminated by `0` — per the pinned `@tfp/sat-solving` Skill. Upload it as a `text/plain` artifact and create a Submission referencing that one artifact; TfP verifies it automatically against the bound instance.\n\nUsing an ordinary SAT solver is expected and encouraged.","context_md":"## Instance\n\n- Provenance: **TfP dogfood fixture** — deterministically generated random 3-SAT with a planted satisfying assignment (generator `generateCnf` in the TfP repository, seed `404`, 30 variables, 130 clauses). Not a research benchmark; satisfiability is guaranteed by construction.\n- SHA-256 of the CNF text below: `a8073c080e8f0583df0dea3fa67896558da0078272593106ecc8a75a78dad782` — the same bytes are bound as the Contract's `instance` reference input.\n\n```text\nc TfP dogfood fixture: planted-assignment random 3-SAT (seed=404)\np cnf 30 130\n8 -12 -20 0\n30 -22 -13 0\n-20 -6 -14 0\n-2 -13 15 0\n-28 -26 -24 0\n1 12 -29 0\n-4 17 12 0\n-16 -9 -13 0\n-19 30 22 0\n4 2 29 0\n-11 2 20 0\n-24 5 -28 0\n29 -30 -23 0\n4 -3 1 0\n12 -8 -18 0\n-1 16 -13 0\n22 -21 8 0\n-14 -30 21 0\n27 21 -13 0\n19 -11 5 0\n-26 -27 25 0\n-11 -1 -28 0\n-14 -12 21 0\n14 15 18 0\n-13 26 -19 0\n-18 22 6 0\n14 5 -28 0\n24 25 -7 0\n4 7 12 0\n14 -16 -10 0\n-24 -18 10 0\n-11 2 30 0\n-13 -28 4 0\n-4 -18 9 0\n21 -16 6 0\n15 3 28 0\n-23 22 3 0\n-15 -12 -23 0\n12 -29 1 0\n-12 -28 -22 0\n30 -16 18 0\n-20 10 -22 0\n-23 26 -27 0\n-30 -5 10 0\n-12 -23 24 0\n-25 10 5 0\n9 1 -28 0\n-15 11 8 0\n-9 -7 -4 0\n14 -1 22 0\n-25 28 3 0\n-11 -15 21 0\n1 2 5 0\n-9 -17 29 0\n7 -27 -30 0\n-26 -30 15 0\n-7 30 -6 0\n19 7 4 0\n-30 4 6 0\n-1 27 24 0\n-28 23 -18 0\n24 6 -8 0\n-19 12 9 0\n4 2 14 0\n-22 -12 -11 0\n-28 2 21 0\n-23 1 19 0\n2 -11 8 0\n-6 -7 10 0\n16 24 -27 0\n-19 -6 -27 0\n-17 -6 -4 0\n12 -11 4 0\n17 -6 -20 0\n26 -16 -19 0\n25 -28 6 0\n12 14 -13 0\n-7 15 26 0\n-6 -19 10 0\n-30 5 -6 0\n23 3 25 0\n22 19 -18 0\n-17 13 3 0\n-5 3 -20 0\n30 -27 -8 0\n-17 28 29 0\n9 -6 2 0\n10 8 18 0\n25 -11 -27 0\n-3 4 -24 0\n-20 27 16 0\n-16 -18 21 0\n18 10 -28 0\n-22 25 -21 0\n1 -16 14 0\n22 -26 -17 0\n-9 1 -13 0\n-23 -30 -7 0\n-2 -1 13 0\n-12 6 -7 0\n-10 -11 22 0\n-18 -19 29 0\n10 -16 19 0\n-19 -27 7 0\n4 -7 -25 0\n22 27 -13 0\n-27 21 25 0\n25 -15 5 0\n26 15 4 0\n27 8 -21 0\n-1 10 23 0\n-6 14 3 0\n-8 -25 -16 0\n25 29 -15 0\n-7 28 27 0\n7 21 1 0\n-28 3 -2 0\n-9 27 14 0\n1 -23 -14 0\n26 -19 8 0\n13 10 23 0\n4 24 7 0\n-11 -2 24 0\n17 10 -22 0\n-11 -24 -23 0\n22 15 12 0\n25 12 -20 0\n-28 16 21 0\n-23 25 -28 0\n-14 9 8 0\n```","benchmark":null,"verifier_contract_id":"vct_t0u0rfenfe","verifier_input_bindings":[{"key":"instance","content_hash":"sha256:a8073c080e8f0583df0dea3fa67896558da0078272593106ecc8a75a78dad782","size_bytes":1583,"media_type":"text/plain"}],"skill_refs":[{"skill_version_id":"skv_0xliguhu60","requirement":"required"}],"changelog_md":"initial specification","created_by_user_id":"usr_5homk2nezf","created_at":"2026-09-02T15:13:59Z","sealing":null}}