Satisfy a larger 3-SAT instance (250 variables)

{
  "problem": {
    "id": "prb_mriiieerce",
    "slug": "sat-dogfood-large",
    "title": "Satisfy a larger 3-SAT instance (250 variables)",
    "structure": "SOLVE",
    "status": "archived",
    "campaign": "sat-solver-dogfood",
    "summary": "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."
  },
  "revision": {
    "id": "prv_hab47gn864",
    "revision_number": 1,
    "created_at": "2026-09-02T06:59:47Z",
    "changelog_md": "initial specification",
    "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_wacbq9qe4y`. 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 `303`, 250 variables, 1065 clauses). Not a research benchmark; satisfiability is guaranteed by construction.\n- SHA-256 of the CNF text below: `7548d44a36d06d93496d91f8bf9fa938669129ecec7ae472003717011c7b743a` — 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=303)\np cnf 250 1065\n174 -168 -102 0\n-141 143 239 0\n163 162 160 0\n160 223 181 0\n144 27 46 0\n-143 -241 198 0\n-53 34 -99 0\n25 106 122 0\n-33 182 19 0\n214 -17 -181 0\n82 146 204 0\n42 -34 17 0\n-2 154 78 0\n12 -59 -173 0\n-124 -158 -166 0\n188 -231 81 0\n76 -212 177 0\n-218 -173 246 0\n221 59 -199 0\n-45 224 -112 0\n41 -186 -145 0\n208 192 203 0\n-97 46 -100 0\n83 24 -148 0\n-124 248 -144 0\n-47 -101 54 0\n170 -219 146 0\n-188 -234 -238 0\n-199 -29 -200 0\n-6 198 20 0\n20 -191 205 0\n-8 -216 -70 0\n13 -39 -124 0\n-100 111 -88 0\n25 210 -249 0\n128 82 50 0\n114 50 93 0\n-163 -198 -11 0\n-90 138 173 0\n162 54 106 0\n-228 -126 131 0\n-110 -17 177 0\n-64 -161 176 0\n-2 -152 -130 0\n-199 246 74 0\n109 20 48 0\n72 128 114 0\n-202 -49 68 0\n-227 93 73 0\n220 9 179 0\n-241 132 -205 0\n3 201 167 0\n-150 -54 -245 0\n-26 246 -59 0\n-201 -55 26 0\n85 36 238 0\n138 244 -231 0\n66 237 84 0\n-3 -99 205 0\n-218 -35 187 0\n98 206 205 0\n195 232 43 0\n-39 154 -237 0\n233 -106 -205 0\n-202 -7 215 0\n-102 143 -112 0\n160 183 -32 0\n-193 195 -31 0\n-184 230 -39 0\n-104 -96 -77 0\n90 -239 -91 0\n-159 186 -16 0\n132 -45 227 0\n158 -14 160 0\n205 -135 -234 0\n-150 -149 -39 0\n8 -137 -56 0\n123 -228 -57 0\n170 -121 -139 0\n-93 68 -147 0\n-55 159 -47 0\n-27 -142 -148 0\n151 -237 54 0\n244 -22 146 0\n-85 -178 -160 0\n250 -153 -152 0\n16 234 20 0\n157 -116 -212 0\n127 -45 -218 0\n-208 -47 228 0\n-157 -99 88 0\n-246 225 36 0\n-48 215 224 0\n92 -134 -230 0\n197 -130 49 0\n-203 -173 170 0\n184 -152 -199 0\n78 -172 233 0\n-249 235 -184 0\n131 49 -202 0\n30 8 -207 0\n-111 15 113 0\n230 -158 186 0\n93 182 170 0\n36 20 180 0\n196 108 -14 0\n-152 -39 170 0\n214 122 15 0\n-120 69 -231 0\n30 26 239 0\n-214 -58 238 0\n-45 249 -62 0\n-105 -27 206 0\n-63 28 6 0\n-115 103 206 0\n212 141 105 0\n-202 -98 -142 0\n169 42 -112 0\n-35 56 -213 0\n208 125 -153 0\n-23 -155 -162 0\n124 -137 151 0\n207 46 42 0\n-187 -20 -4 0\n-95 170 217 0\n-48 -40 143 0\n-34 -49 -61 0\n-11 37 101 0\n181 -39 238 0\n-196 -216 -237 0\n-54 -158 -25 0\n14 -150 138 0\n-75 -56 -233 0\n246 13 -32 0\n-64 -31 -113 0\n82 -80 219 0\n108 233 -99 0\n-93 -25 229 0\n-151 23 -246 0\n242 79 121 0\n29 -45 -18 0\n-83 -147 -228 0\n167 93 229 0\n41 238 208 0\n-221 -208 -14 0\n-1 42 104 0\n-110 -103 9 0\n-74 -198 -134 0\n-47 217 -29 0\n-31 217 -172 0\n106 26 -157 0\n239 -170 -57 0\n147 -68 -113 0\n-232 -80 -10 0\n-151 126 192 0\n-162 -206 -247 0\n-2 -14 -24 0\n-242 -218 -14 0\n122 71 -150 0\n194 57 3 0\n-93 -131 -68 0\n250 -37 202 0\n10 65 -47 0\n9 197 50 0\n199 -68 -246 0\n164 217 150 0\n14 6 209 0\n9 -88 14 0\n223 201 -37 0\n250 -123 228 0\n-135 177 -167 0\n233 134 18 0\n-210 246 10 0\n9 27 198 0\n-166 -148 52 0\n22 29 143 0\n-173 64 -69 0\n-113 -248 -103 0\n-88 8 -63 0\n4 101 -227 0\n146 175 -197 0\n-122 135 239 0\n-165 -66 106 0\n22 206 30 0\n101 -151 65 0\n-26 225 -244 0\n-60 208 -14 0\n36 -148 167 0\n233 -32 230 0\n225 -53 193 0\n216 -85 48 0\n-22 -249 243 0\n-157 205 89 0\n99 -72 -103 0\n-210 -35 -87 0\n-22 -41 220 0\n20 -194 -226 0\n-219 243 50 0\n127 20 49 0\n57 136 -145 0\n30 -152 -201 0\n227 -164 -218 0\n-63 120 -115 0\n131 103 -187 0\n234 -199 -18 0\n226 167 61 0\n-194 -110 -171 0\n131 -24 -148 0\n89 -8 141 0\n-145 -155 82 0\n-45 78 -39 0\n-6 137 124 0\n143 168 53 0\n93 7 29 0\n68 -2 -45 0\n-153 211 -112 0\n-174 177 192 0\n-193 175 174 0\n-134 -98 -124 0\n-188 163 172 0\n-49 -48 171 0\n91 -148 -160 0\n109 88 -220 0\n-157 142 -146 0\n132 -189 -122 0\n43 54 -36 0\n16 -189 98 0\n98 123 128 0\n90 -190 -240 0\n222 60 214 0\n224 -55 -149 0\n-145 -65 -173 0\n103 38 -205 0\n-47 -24 -91 0\n74 190 -132 0\n-160 -24 17 0\n-24 -189 -2 0\n-244 -74 105 0\n128 99 -25 0\n-175 -205 223 0\n129 -68 -162 0\n-206 -77 -105 0\n-44 111 183 0\n-44 61 206 0\n-238 129 -84 0\n-1 78 52 0\n127 -78 -19 0\n184 -94 65 0\n61 230 24 0\n36 -37 -152 0\n231 76 -122 0\n-72 87 -228 0\n238 13 -145 0\n-88 147 140 0\n-47 196 -164 0\n-28 76 -156 0\n-100 -156 -101 0\n183 -132 -187 0\n146 225 108 0\n156 -123 -168 0\n92 236 -27 0\n30 -237 -250 0\n-86 97 -34 0\n54 -91 36 0\n40 -200 -91 0\n-245 -159 -202 0\n201 -120 -60 0\n250 -135 -207 0\n121 -193 -85 0\n-56 -41 151 0\n-134 -82 -187 0\n65 39 -35 0\n-80 38 89 0\n-186 16 -189 0\n-82 -34 90 0\n179 43 235 0\n2 145 182 0\n97 247 -161 0\n-208 139 242 0\n182 10 6 0\n-105 161 -221 0\n-145 -234 9 0\n-102 -6 -128 0\n-152 110 -114 0\n167 -149 120 0\n189 -1 80 0\n-218 154 143 0\n-168 33 -225 0\n-172 -199 93 0\n-227 63 -173 0\n212 106 -109 0\n219 -168 100 0\n-184 103 -62 0\n-195 -134 -32 0\n-210 198 41 0\n128 -91 -204 0\n154 14 41 0\n189 88 39 0\n129 -22 -40 0\n-221 238 -87 0\n97 -157 -176 0\n3 25 118 0\n-171 22 -69 0\n-227 224 230 0\n39 -130 172 0\n-60 -146 65 0\n-175 -16 -228 0\n-108 -7 -244 0\n-44 218 -219 0\n210 15 -198 0\n59 -16 -62 0\n-215 -139 -22 0\n76 195 60 0\n-173 82 223 0\n-181 216 -57 0\n206 -73 -158 0\n-169 23 -12 0\n135 -22 211 0\n-14 -31 170 0\n-62 155 -161 0\n-171 217 181 0\n-136 -179 -156 0\n177 208 58 0\n-50 -159 -155 0\n-84 -170 126 0\n-250 54 -79 0\n248 25 -134 0\n225 -243 -83 0\n81 101 -67 0\n46 -32 -114 0\n-6 -53 173 0\n-107 -33 -77 0\n65 193 -83 0\n-45 243 184 0\n-1 -59 103 0\n128 -199 -41 0\n-204 -19 -140 0\n-226 15 187 0\n216 28 62 0\n132 243 -225 0\n-154 -29 -120 0\n-138 -173 95 0\n-22 79 143 0\n-125 -248 139 0\n-64 121 -244 0\n-157 237 -47 0\n-147 37 -78 0\n235 230 -248 0\n160 -206 -173 0\n128 6 -62 0\n158 45 -48 0\n239 -125 244 0\n-180 -157 -221 0\n139 47 121 0\n242 -55 -226 0\n-82 -43 74 0\n-243 167 -1 0\n125 240 -241 0\n-168 -199 110 0\n-95 -241 -7 0\n-243 158 -57 0\n-36 211 -117 0\n-186 41 -65 0\n-143 145 -175 0\n-181 146 170 0\n-70 137 -19 0\n-27 11 158 0\n209 -90 -188 0\n-19 -32 -14 0\n-122 -173 -144 0\n41 133 46 0\n-99 -76 -173 0\n-118 -179 81 0\n-234 -48 -19 0\n-144 -67 -13 0\n214 230 -162 0\n240 152 28 0\n-74 99 -223 0\n-117 128 -203 0\n-9 -50 140 0\n-193 231 -192 0\n-74 51 146 0\n-80 -156 -91 0\n-118 -111 -56 0\n177 211 23 0\n200 -204 10 0\n-243 2 -64 0\n-50 53 -80 0\n145 -169 -91 0\n14 79 150 0\n-202 165 -123 0\n60 54 65 0\n55 -218 214 0\n-196 -46 -211 0\n-103 132 137 0\n225 182 191 0\n204 -86 -231 0\n82 50 -231 0\n240 102 137 0\n-171 -103 -55 0\n-225 124 -125 0\n-149 194 -184 0\n-190 -148 97 0\n64 -187 -86 0\n149 132 -158 0\n-185 68 98 0\n50 49 202 0\n215 211 -53 0\n-164 76 -45 0\n-1 64 99 0\n211 87 -133 0\n10 -241 -181 0\n240 -228 -172 0\n-165 -78 37 0\n-18 76 -97 0\n-177 165 -150 0\n240 174 230 0\n20 -186 119 0\n-72 -128 -49 0\n-221 -66 -93 0\n-192 -91 159 0\n76 -80 -220 0\n-131 -56 -96 0\n-56 232 9 0\n-63 35 -201 0\n247 -58 109 0\n26 -57 -111 0\n14 226 236 0\n158 33 97 0\n4 139 -84 0\n61 43 -155 0\n-195 -113 38 0\n-20 -156 184 0\n-196 -144 -15 0\n217 89 133 0\n156 214 -92 0\n27 70 -220 0\n-250 145 236 0\n103 -60 -250 0\n-246 162 158 0\n90 69 76 0\n207 65 43 0\n-171 -10 -17 0\n223 -221 22 0\n-237 -185 243 0\n44 116 -210 0\n-45 78 170 0\n46 143 214 0\n-90 193 46 0\n-39 -38 -16 0\n-31 -130 211 0\n-63 89 -36 0\n200 -57 -243 0\n82 67 164 0\n21 -59 -44 0\n-227 40 -116 0\n183 -73 202 0\n71 95 10 0\n-50 -150 -216 0\n-71 138 67 0\n-134 216 -229 0\n162 5 22 0\n10 -181 -87 0\n167 204 -200 0\n-56 197 -97 0\n-115 -6 -135 0\n192 -153 -168 0\n-27 156 88 0\n162 -149 -137 0\n236 -121 -125 0\n192 -215 -213 0\n-55 30 120 0\n187 137 -11 0\n-123 217 -148 0\n-27 64 5 0\n43 29 -210 0\n-116 108 -145 0\n-87 -29 80 0\n174 118 -58 0\n-241 -142 63 0\n-106 208 12 0\n-118 135 -207 0\n-5 -88 -175 0\n-226 38 -1 0\n189 169 110 0\n-84 65 228 0\n95 -116 223 0\n-11 -87 -82 0\n-242 -179 -39 0\n98 202 -197 0\n248 -73 108 0\n-127 -79 -210 0\n195 26 -102 0\n208 210 167 0\n-23 -172 -165 0\n-54 -34 -151 0\n62 223 -80 0\n-47 -172 -33 0\n-213 125 117 0\n31 -87 239 0\n132 133 113 0\n9 -115 -5 0\n-218 36 -170 0\n-83 -208 193 0\n-68 2 -79 0\n-65 -212 182 0\n180 -202 107 0\n-188 91 133 0\n240 -193 219 0\n-62 -60 66 0\n156 -142 -92 0\n133 -69 155 0\n-179 -187 -198 0\n79 -136 122 0\n-219 -149 223 0\n117 -171 136 0\n84 -37 13 0\n224 38 -60 0\n-214 8 -102 0\n21 61 -120 0\n223 180 -94 0\n171 -104 -241 0\n30 -225 -93 0\n-227 141 -218 0\n229 -103 -40 0\n80 68 21 0\n102 -157 -188 0\n-75 -2 -4 0\n12 145 -102 0\n105 63 -114 0\n-246 104 -8 0\n114 7 227 0\n19 45 43 0\n-77 -19 132 0\n208 200 -58 0\n-147 -248 133 0\n152 199 -218 0\n-155 -130 99 0\n120 -19 17 0\n185 65 70 0\n224 -178 47 0\n191 -230 -97 0\n-83 -120 103 0\n171 -137 182 0\n71 104 100 0\n223 -222 155 0\n132 237 -176 0\n85 -164 -33 0\n196 -133 -56 0\n7 -11 -129 0\n128 -99 63 0\n236 -163 60 0\n-184 224 -36 0\n-149 98 161 0\n211 103 135 0\n160 -247 86 0\n-121 1 -48 0\n10 187 155 0\n23 128 -57 0\n190 -57 -91 0\n-191 -162 -63 0\n-16 67 219 0\n-72 181 -43 0\n10 -152 -19 0\n135 -179 -22 0\n243 23 137 0\n-66 -142 -164 0\n78 110 114 0\n120 54 -171 0\n-185 -164 203 0\n-172 -211 -60 0\n218 191 168 0\n-142 -17 119 0\n189 162 250 0\n-213 25 89 0\n-136 52 -8 0\n-111 245 197 0\n-154 8 -233 0\n40 -154 98 0\n-228 181 73 0\n-162 237 -225 0\n-39 27 -34 0\n-199 -236 -185 0\n-206 100 -161 0\n25 105 -186 0\n-238 211 129 0\n-36 38 -147 0\n82 -183 -203 0\n159 182 -97 0\n175 100 -227 0\n5 -21 -171 0\n197 -97 -54 0\n84 -57 219 0\n-11 -34 -165 0\n-41 192 146 0\n50 -224 17 0\n16 91 -60 0\n236 224 -69 0\n-172 58 119 0\n108 156 -16 0\n31 128 137 0\n81 116 -196 0\n172 -122 -26 0\n141 106 -129 0\n169 -19 126 0\n-199 -43 -167 0\n-125 -131 83 0\n3 72 -200 0\n-2 -84 -179 0\n-55 106 97 0\n-172 -14 -3 0\n227 78 -171 0\n-198 -226 43 0\n207 -130 211 0\n-178 -62 14 0\n-150 -176 26 0\n202 -135 159 0\n-35 -212 89 0\n-136 105 -101 0\n-225 -227 -129 0\n-154 196 -165 0\n-91 160 -188 0\n-124 -93 242 0\n-20 198 -60 0\n-155 32 103 0\n-151 -120 -179 0\n-200 -21 97 0\n-190 161 76 0\n-10 209 14 0\n-181 -22 -161 0\n177 -210 193 0\n31 36 -154 0\n171 -229 -163 0\n175 109 204 0\n-211 87 100 0\n-155 171 78 0\n49 -164 -5 0\n-152 231 -133 0\n-87 198 -200 0\n-18 180 249 0\n-219 124 184 0\n-64 3 -1 0\n129 215 -243 0\n-96 139 46 0\n208 198 -232 0\n-97 -12 223 0\n-153 -64 189 0\n157 221 -59 0\n211 174 35 0\n173 68 104 0\n-87 206 117 0\n4 -218 -77 0\n-223 -188 -180 0\n-190 -23 14 0\n-58 -154 -176 0\n27 -80 -95 0\n-102 -24 129 0\n199 -84 158 0\n236 178 22 0\n-208 -181 116 0\n220 -150 68 0\n-55 240 -25 0\n233 84 142 0\n-163 -179 -188 0\n114 133 -176 0\n221 -62 -182 0\n3 -2 161 0\n90 240 -247 0\n-244 135 -58 0\n-247 -120 3 0\n207 -105 -77 0\n-131 132 -206 0\n-69 76 115 0\n-169 -248 -163 0\n8 -59 -108 0\n2 -44 21 0\n72 82 -175 0\n-241 235 -138 0\n-186 29 -171 0\n139 15 -85 0\n191 143 -33 0\n93 52 -68 0\n-32 -241 -33 0\n-184 -122 -104 0\n211 -243 -115 0\n106 175 -70 0\n-120 -55 -3 0\n2 199 -51 0\n-51 -102 -192 0\n14 -79 50 0\n-200 -22 -5 0\n-4 -60 81 0\n229 -170 -67 0\n-211 -181 245 0\n-143 129 183 0\n-246 -85 117 0\n31 -44 -209 0\n-216 -62 -20 0\n228 -184 -185 0\n-148 19 99 0\n136 -210 -212 0\n38 28 177 0\n236 -30 -82 0\n-114 -158 200 0\n177 -6 101 0\n-156 66 -150 0\n232 -227 191 0\n202 50 -218 0\n-34 -118 56 0\n5 140 -123 0\n-78 -165 -86 0\n-96 -157 -36 0\n-110 73 -27 0\n-224 161 -189 0\n78 203 172 0\n235 169 243 0\n108 -113 59 0\n-201 232 -79 0\n-123 67 -92 0\n128 16 197 0\n-32 101 -105 0\n45 -12 -152 0\n69 91 -126 0\n-183 112 -164 0\n-40 114 -196 0\n241 -68 38 0\n167 -36 -187 0\n-203 239 -103 0\n160 152 1 0\n212 -73 16 0\n-211 9 187 0\n162 213 -145 0\n-179 156 -101 0\n167 -147 211 0\n-22 -113 72 0\n-162 65 -80 0\n107 -90 -232 0\n-190 -115 209 0\n185 33 -11 0\n-116 20 58 0\n25 222 -47 0\n-180 250 -191 0\n-75 -81 -118 0\n-19 132 -114 0\n-175 144 -155 0\n62 -220 -245 0\n-101 -31 -56 0\n42 -181 134 0\n117 -163 138 0\n233 231 61 0\n-185 -57 92 0\n-236 -57 97 0\n108 -136 106 0\n5 -87 -106 0\n79 -156 53 0\n-18 231 54 0\n-87 -59 -221 0\n99 -91 -24 0\n-137 208 135 0\n-180 237 -162 0\n-203 63 235 0\n-193 139 -131 0\n-85 -5 -171 0\n-117 -66 98 0\n-235 193 12 0\n-145 57 -47 0\n-184 30 -116 0\n-96 -49 -150 0\n99 233 35 0\n65 -167 10 0\n108 58 -198 0\n42 -22 116 0\n14 -196 -134 0\n-199 -36 -32 0\n209 -185 79 0\n-154 -186 151 0\n177 9 -67 0\n-46 12 -185 0\n-22 -209 195 0\n-51 97 -43 0\n207 -63 -190 0\n-125 239 242 0\n219 196 147 0\n91 -170 -80 0\n157 119 -202 0\n228 -70 167 0\n-71 28 3 0\n-106 242 115 0\n-218 137 174 0\n-55 -27 -2 0\n60 -13 -185 0\n-14 -74 141 0\n-163 -172 240 0\n-228 218 235 0\n-196 -136 -113 0\n217 -246 -132 0\n-5 -188 -79 0\n178 11 158 0\n208 234 174 0\n176 20 -152 0\n-116 70 -51 0\n21 -242 238 0\n-172 -61 -193 0\n-113 138 36 0\n7 -132 -96 0\n-169 -147 -117 0\n-187 63 185 0\n204 191 -48 0\n-188 -180 -53 0\n-101 -204 185 0\n73 -196 133 0\n-217 242 -125 0\n-210 -59 176 0\n-69 -176 87 0\n-1 6 -121 0\n-195 -164 -40 0\n-167 160 -199 0\n-171 -147 183 0\n-103 -68 223 0\n-124 27 -200 0\n235 -226 217 0\n-188 -169 115 0\n-57 -141 90 0\n-73 134 -131 0\n97 -25 -196 0\n115 143 50 0\n-183 -196 219 0\n-56 182 -163 0\n-128 48 -35 0\n72 25 224 0\n-188 4 67 0\n225 184 10 0\n-144 203 -223 0\n-93 175 -78 0\n89 15 -19 0\n-72 -108 248 0\n18 -101 190 0\n98 29 -47 0\n-16 -176 84 0\n-1 -109 -3 0\n21 -125 -161 0\n-48 73 195 0\n153 99 88 0\n43 40 233 0\n-121 162 -36 0\n-49 -58 205 0\n-98 191 -172 0\n23 -130 220 0\n-235 -151 98 0\n2 17 221 0\n98 -126 -167 0\n-230 -17 30 0\n-189 49 50 0\n54 152 -212 0\n233 -81 210 0\n-83 146 26 0\n75 28 -228 0\n183 -97 249 0\n-49 146 147 0\n90 -212 245 0\n-24 -244 7 0\n-126 -46 -85 0\n-220 -234 -180 0\n146 238 -202 0\n-6 -187 158 0\n184 -149 -120 0\n-34 174 -217 0\n-157 197 27 0\n18 30 -40 0\n197 17 77 0\n-12 -215 -111 0\n84 191 236 0\n-60 120 3 0\n-27 -133 183 0\n97 -33 -121 0\n-175 -33 -105 0\n-148 -173 94 0\n-123 242 -113 0\n5 -144 -178 0\n111 -66 -103 0\n97 208 154 0\n208 -132 -224 0\n-160 -24 155 0\n14 -30 -90 0\n238 83 119 0\n-38 48 -148 0\n143 128 -231 0\n11 17 188 0\n125 196 -13 0\n245 191 117 0\n-16 -26 36 0\n-116 -159 212 0\n185 -114 205 0\n3 -231 -223 0\n-121 -7 169 0\n-178 -69 85 0\n-188 -102 145 0\n-32 78 48 0\n-196 146 -225 0\n-109 76 -8 0\n-122 111 137 0\n205 60 -47 0\n-116 75 -175 0\n-209 -240 160 0\n-231 -153 -30 0\n120 -144 5 0\n241 -38 -57 0\n236 245 139 0\n-105 -102 22 0\n88 83 -231 0\n-176 64 -201 0\n-145 -62 -74 0\n-103 -145 -69 0\n74 117 -166 0\n-113 218 -211 0\n64 158 -63 0\n-221 219 -61 0\n-170 242 -121 0\n-227 82 -148 0\n104 146 162 0\n-33 205 112 0\n90 -62 8 0\n-237 125 243 0\n240 -80 -107 0\n-171 214 105 0\n191 197 -45 0\n-198 -107 25 0\n-18 25 243 0\n-205 100 -148 0\n-165 -116 228 0\n-218 -19 -74 0\n235 -185 206 0\n-194 183 -2 0\n-9 221 -126 0\n111 146 -125 0\n141 -194 -32 0\n-67 -123 60 0\n44 -248 -199 0\n215 197 153 0\n-195 -212 140 0\n227 83 239 0\n-32 197 100 0\n-105 -79 -161 0\n-35 -245 27 0\n-33 203 -172 0\n-64 -129 -150 0\n182 168 -199 0\n184 60 -166 0\n-51 -165 10 0\n26 -4 -9 0\n42 -223 148 0\n171 20 -21 0\n-101 -228 -158 0\n-241 41 -55 0\n30 140 20 0\n163 -198 -34 0\n-57 -45 -63 0\n146 113 -15 0\n-141 41 -173 0\n-34 30 -138 0\n-156 89 -246 0\n3 145 239 0\n-77 -122 -178 0\n-102 -247 243 0\n-67 -11 239 0\n-1 92 -227 0\n-67 2 -229 0\n190 38 15 0\n-20 -37 28 0\n58 -200 -76 0\n232 -173 -86 0\n-46 250 37 0\n151 102 177 0\n-152 -172 -193 0\n-186 246 90 0\n-24 -85 54 0\n225 39 148 0\n209 -40 100 0\n46 91 67 0\n202 -180 119 0\n-70 230 205 0\n-133 -197 -161 0\n74 -197 -58 0\n-226 64 116 0\n244 -153 -57 0\n-220 -113 139 0\n-165 -78 158 0\n-12 128 -94 0\n-4 -38 143 0\n-138 228 139 0\n217 45 -65 0\n-164 -59 -215 0\n51 6 -123 0\n67 -111 -201 0\n82 -177 -199 0\n2 -79 -98 0\n89 76 9 0\n139 -166 38 0\n-103 232 -139 0\n98 21 -158 0\n-229 2 -178 0\n-202 -113 -6 0\n26 234 131 0\n191 42 -114 0\n-26 240 191 0\n-212 -61 -133 0\n150 42 207 0\n236 -185 -163 0\n137 190 -85 0\n178 225 -125 0\n12 87 -116 0\n-187 -15 236 0\n52 -86 -203 0\n-180 -73 -33 0\n-149 -4 118 0\n-160 -222 -16 0\n40 -59 -58 0\n-166 206 121 0\n-154 139 28 0\n-53 -48 184 0\n155 -203 -193 0\n-161 -10 -153 0\n7 -147 214 0\n-82 206 -209 0\n-40 199 -49 0\n172 -131 -79 0\n146 69 -102 0\n-48 189 58 0\n-178 11 37 0\n249 245 195 0\n190 217 -94 0\n177 216 21 0\n-173 -88 -199 0\n118 17 -1 0\n95 168 -13 0\n57 -190 -47 0\n-157 -53 -164 0\n-21 -165 -66 0\n-207 150 195 0\n-224 2 191 0\n140 -237 -250 0\n-223 187 -66 0\n-131 147 -95 0\n5 -199 129 0\n234 39 -35 0\n-47 161 -204 0\n196 154 -14 0\n61 -133 144 0\n70 11 108 0\n-22 -221 -135 0\n-67 32 -186 0\n-16 95 -32 0\n4 -242 -175 0\n172 -144 222 0\n72 236 -163 0\n-232 -59 133 0\n-80 -64 -31 0\n-215 208 -22 0\n140 149 30 0\n210 -15 206 0\n197 98 -201 0\n-125 -221 -48 0\n44 -222 -40 0\n-56 -64 94 0\n-189 -42 -127 0\n```",
    "benchmark": null,
    "skill_refs": [
      {
        "skill_version_id": "skv_0xliguhu60",
        "requirement": "required"
      }
    ],
    "verifier_contract_id": "vct_wacbq9qe4y",
    "verifier_input_bindings": [
      {
        "key": "instance",
        "content_hash": "sha256:7548d44a36d06d93496d91f8bf9fa938669129ecec7ae472003717011c7b743a",
        "size_bytes": 15241,
        "media_type": "text/plain"
      }
    ],
    "sealing": null
  },
  "verifier_contract": {
    "id": "vct_wacbq9qe4y",
    "title": "Satisfying assignment for the bound CNF instance",
    "statement_md": "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.",
    "result_kind": "pass_fail",
    "stages": [
      {
        "acceptance": null,
        "description_md": "Parses the assignment and evaluates every clause of the bound instance. Establishes clause satisfaction only.",
        "evidence_schema": {
          "properties": {
            "clauses_satisfied": {
              "type": "integer"
            },
            "clauses_total": {
              "type": "integer"
            }
          },
          "required": [
            "clauses_total",
            "clauses_satisfied"
          ],
          "type": "object"
        },
        "external_system": null,
        "key": "assignment_check",
        "kind": "sandbox",
        "review_protocol_id": null,
        "rule_owner": null,
        "title": "Clause satisfaction check"
      }
    ],
    "reference_inputs": [
      {
        "description": "The CNF instance in DIMACS format that the submitted assignment must satisfy.",
        "key": "instance",
        "max_bytes": 10485760,
        "media_types": [
          "text/plain"
        ],
        "required": true
      }
    ],
    "submission_requirements": {
      "accepts_text_only": false,
      "answer_format_md": null,
      "required_artifacts": [
        {
          "description": "A satisfying assignment in SAT-competition v-line format.",
          "max_bytes": 1048576,
          "media_types": [
            "text/plain"
          ],
          "role": "assignment"
        }
      ]
    },
    "score": null
  },
  "api": {
    "problem": "/api/problems/prb_mriiieerce",
    "revision": "/api/problems/prb_mriiieerce/revisions/1",
    "mcp": "start_attempt {\"problem\":\"sat-dogfood-large\",\"revision\":1,\"provenance\":\"mixed\"}"
  }
}