c cnf generated by mark.reason.apps.PlgToDimacs written by Mark Chavira
c cnf generated on Wed Nov 17 12:34:54 PST 2004.
c
c Following is the map back to variable name:
c
c 1 X_1_id0_input
c 2 X_5_id1_input
c 3 X_9_id2_input
c 4 X_13_id3_input
c 5 X_17_id4_input
c 6 X_21_id5_input
c 7 X_25_id6_input
c 8 X_29_id7_input
c 9 X_33_id8_input
c 10 X_37_id9_input
c 11 X_41_id10_input
c 12 X_45_id11_input
c 13 X_49_id12_input
c 14 X_53_id13_input
c 15 X_57_id14_input
c 16 X_61_id15_input
c 17 X_65_id16_input
c 18 X_69_id17_input
c 19 X_73_id18_input
c 20 X_77_id19_input
c 21 X_81_id20_input
c 22 X_85_id21_input
c 23 X_89_id22_input
c 24 X_93_id23_input
c 25 X_97_id24_input
c 26 X_101_id25_input
c 27 X_105_id26_input
c 28 X_109_id27_input
c 29 X_113_id28_input
c 30 X_117_id29_input
c 31 X_121_id30_input
c 32 X_125_id31_input
c 33 X_129_ic0_input
c 34 X_130_ic1_input
c 35 X_131_ic2_input
c 36 X_132_ic3_input
c 37 X_133_ic4_input
c 38 X_134_ic5_input
c 39 X_135_ic6_input
c 40 X_136_ic7_input
c 41 X_137_r_input
c 42 X_250_xa0_internal
c 43 X_251_xa1_internal
c 44 X_252_xa2_internal
c 45 X_253_xa3_internal
c 46 X_254_xa4_internal
c 47 X_255_xa5_internal
c 48 X_256_xa6_internal
c 49 X_257_xa7_internal
c 50 X_258_xa8_internal
c 51 X_259_xa9_internal
c 52 X_260_xa10_internal
c 53 X_261_xa11_internal
c 54 X_262_xa12_internal
c 55 X_263_xa13_internal
c 56 X_264_xa14_internal
c 57 X_265_xa15_internal
c 58 X_266_h0_internal
c 59 X_267_h1_internal
c 60 X_268_h2_internal
c 61 X_269_h3_internal
c 62 X_270_h4_internal
c 63 X_271_h5_internal
c 64 X_272_h6_internal
c 65 X_273_h7_internal
c 66 X_274_xb0_internal
c 67 X_275_xc0_internal
c 68 X_276_xb1_internal
c 69 X_277_xc1_internal
c 70 X_278_xb2_internal
c 71 X_279_xc2_internal
c 72 X_280_xb3_internal
c 73 X_281_xc3_internal
c 74 X_282_xb4_internal
c 75 X_283_xc4_internal
c 76 X_284_xb5_internal
c 77 X_285_xc5_internal
c 78 X_286_xb6_internal
c 79 X_287_xc6_internal
c 80 X_288_xb7_internal
c 81 X_289_xc7_internal
c 82 X_290_f0_internal
c 83 X_293_f1_internal
c 84 X_296_f2_internal
c 85 X_299_f3_internal
c 86 X_302_f4_internal
c 87 X_305_f5_internal
c 88 X_308_f6_internal
c 89 X_311_f7_internal
c 90 X_314_xe0_internal
c 91 X_315_xe1_internal
c 92 X_316_xe2_internal
c 93 X_317_xe3_internal
c 94 X_318_xe4_internal
c 95 X_319_xe5_internal
c 96 X_320_xe6_internal
c 97 X_321_xe7_internal
c 98 X_338_g0_internal
c 99 X_339_g1_internal
c 100 X_340_g2_internal
c 101 X_341_g3_internal
c 102 X_342_g4_internal
c 103 X_343_g5_internal
c 104 X_344_g6_internal
c 105 X_345_g7_internal
c 106 X_346_xd0_internal
c 107 X_347_xd1_internal
c 108 X_348_xd2_internal
c 109 X_349_xd3_internal
c 110 X_350_xd4_internal
c 111 X_351_xd5_internal
c 112 X_352_xd6_internal
c 113 X_353_xd7_internal
c 114 X_354_s0_internal
c 115 X_367_s1_internal
c 116 X_380_s2_internal
c 117 X_393_s3_internal
c 118 X_406_s4_internal
c 119 X_419_s5_internal
c 120 X_432_s6_internal
c 121 X_445_s7_internal
c 122 X_554_y0a_internal
c 123 X_555_y1a_internal
c 124 X_556_y2a_internal
c 125 X_557_y0b_internal
c 126 X_558_y1b_internal
c 127 X_559_y3b_internal
c 128 X_560_y0c_internal
c 129 X_561_y2c_internal
c 130 X_562_y3c_internal
c 131 X_563_y1d_internal
c 132 X_564_y2d_internal
c 133 X_565_y3d_internal
c 134 X_566_y5i_internal
c 135 X_567_y7i_internal
c 136 X_568_y5j_internal
c 137 X_569_y6j_internal
c 138 X_570_y4k_internal
c 139 X_571_y7k_internal
c 140 X_572_y4l_internal
c 141 X_573_y6l_internal
c 142 X_574_y4a_internal
c 143 X_575_y5a_internal
c 144 X_576_y6a_internal
c 145 X_577_y4b_internal
c 146 X_578_y5b_internal
c 147 X_579_y7b_internal
c 148 X_580_y4c_internal
c 149 X_581_y6c_internal
c 150 X_582_y7c_internal
c 151 X_583_y5d_internal
c 152 X_584_y6d_internal
c 153 X_585_y7d_internal
c 154 X_586_y1i_internal
c 155 X_587_y3i_internal
c 156 X_588_y1j_internal
c 157 X_589_y2j_internal
c 158 X_590_y0k_internal
c 159 X_591_y3k_internal
c 160 X_592_y0l_internal
c 161 X_593_y2l_internal
c 162 X_594_t0_internal
c 163 X_595_t1_internal
c 164 X_596_t2_internal
c 165 X_597_t3_internal
c 166 X_598_t4_internal
c 167 X_599_t5_internal
c 168 X_600_t6_internal
c 169 X_601_t7_internal
c 170 X_602_u0_internal
c 171 X_607_u1_internal
c 172 X_620_wa_internal
c 173 X_625_wb_internal
c 174 X_630_wc_internal
c 175 X_635_wd_internal
c 176 X_640_we_internal
c 177 X_645_wf_internal
c 178 X_650_wg_internal
c 179 X_655_wh_internal
c 180 X_692_e0_internal
c 181 X_693_e1_internal
c 182 X_694_e2_internal
c 183 X_695_e3_internal
c 184 X_696_e4_internal
c 185 X_697_e5_internal
c 186 X_698_e6_internal
c 187 X_699_e7_internal
c 188 X_700_e8_internal
c 189 X_701_e9_internal
c 190 X_702_e10_internal
c 191 X_703_e11_internal
c 192 X_704_e12_internal
c 193 X_705_e13_internal
c 194 X_706_e14_internal
c 195 X_707_e15_internal
c 196 X_708_e16_internal
c 197 X_709_e17_internal
c 198 X_710_e18_internal
c 199 X_711_e19_internal
c 200 X_712_e20_internal
c 201 X_713_e21_internal
c 202 X_714_e22_internal
c 203 X_715_e23_internal
c 204 X_716_e24_internal
c 205 X_717_e25_internal
c 206 X_718_e26_internal
c 207 X_719_e27_internal
c 208 X_720_e28_internal
c 209 X_721_e29_internal
c 210 X_722_e30_internal
c 211 X_723_e31_internal
c 212 X_724_od0_output
c 213 X_725_od1_output
c 214 X_726_od2_output
c 215 X_727_od3_output
c 216 X_728_od4_output
c 217 X_729_od5_output
c 218 X_730_od6_output
c 219 X_731_od7_output
c 220 X_732_od8_output
c 221 X_733_od9_output
c 222 X_734_od10_output
c 223 X_735_od11_output
c 224 X_736_od12_output
c 225 X_737_od13_output
c 226 X_738_od14_output
c 227 X_739_od15_output
c 228 X_740_od16_output
c 229 X_741_od17_output
c 230 X_742_od18_output
c 231 X_743_od19_output
c 232 X_744_od20_output
c 233 X_745_od21_output
c 234 X_746_od22_output
c 235 X_747_od23_output
c 236 X_748_od24_output
c 237 X_749_od25_output
c 238 X_750_od26_output
c 239 X_751_od27_output
c 240 X_752_od28_output
c 241 X_753_od29_output
c 242 X_754_od30_output
c 243 X_755_od31_output
c
p cnf 243 714
-243 -211 -32 0
-243 32 211 0
-242 -210 -31 0
-242 31 210 0
-241 -209 -30 0
-241 30 209 0
-240 -208 -29 0
-240 29 208 0
-239 -207 -28 0
-239 28 207 0
-238 -206 -27 0
-238 27 206 0
-237 -205 -26 0
-237 26 205 0
-236 -204 -25 0
-236 25 204 0
-235 -203 -24 0
-235 24 203 0
-234 -202 -23 0
-234 23 202 0
-233 -201 -22 0
-233 22 201 0
-232 -200 -21 0
-232 21 200 0
-231 -199 -20 0
-231 20 199 0
-230 -198 -19 0
-230 19 198 0
-229 -197 -18 0
-229 18 197 0
-228 -196 -17 0
-228 17 196 0
-227 -195 -16 0
-227 16 195 0
-226 -194 -15 0
-226 15 194 0
-225 -193 -14 0
-225 14 193 0
-224 -192 -13 0
-224 13 192 0
-223 -191 -12 0
-223 12 191 0
-222 -190 -11 0
-222 11 190 0
-221 -189 -10 0
-221 10 189 0
-220 -188 -9 0
-220 9 188 0
-219 -187 -8 0
-219 8 187 0
-218 -186 -7 0
-218 7 186 0
-217 -185 -6 0
-217 6 185 0
-216 -184 -5 0
-216 5 184 0
-215 -183 -4 0
-215 4 183 0
-214 -182 -3 0
-214 3 182 0
-213 -181 -2 0
-213 2 181 0
-212 -180 -1 0
-212 1 180 0
-211 32 243 0
-211 121 0
-211 179 0
-210 31 242 0
-210 120 0
-210 179 0
-209 30 241 0
-209 119 0
-209 179 0
-208 29 240 0
-208 118 0
-208 179 0
-207 28 239 0
-207 121 0
-207 178 0
-206 27 238 0
-206 120 0
-206 178 0
-205 26 237 0
-205 119 0
-205 178 0
-204 25 236 0
-204 118 0
-204 178 0
-203 24 235 0
-203 121 0
-203 177 0
-202 23 234 0
-202 120 0
-202 177 0
-201 22 233 0
-201 119 0
-201 177 0
-200 21 232 0
-200 118 0
-200 177 0
-199 20 231 0
-199 121 0
-199 176 0
-198 19 230 0
-198 120 0
-198 176 0
-197 18 229 0
-197 119 0
-197 176 0
-196 17 228 0
-196 118 0
-196 176 0
-195 16 227 0
-195 117 0
-195 175 0
-194 15 226 0
-194 116 0
-194 175 0
-193 14 225 0
-193 115 0
-193 175 0
-192 13 224 0
-192 114 0
-192 175 0
-191 12 223 0
-191 117 0
-191 174 0
-190 11 222 0
-190 116 0
-190 174 0
-189 10 221 0
-189 115 0
-189 174 0
-188 9 220 0
-188 114 0
-188 174 0
-187 8 219 0
-187 117 0
-187 173 0
-186 7 218 0
-186 116 0
-186 173 0
-185 6 217 0
-185 115 0
-185 173 0
-184 5 216 0
-184 114 0
-184 173 0
-183 4 215 0
-183 117 0
-183 172 0
-182 3 214 0
-182 116 0
-182 172 0
-181 2 213 0
-181 115 0
-181 172 0
-180 1 212 0
-180 114 0
-180 172 0
-179 -121 211 0
-179 -120 210 0
-179 -119 209 0
-179 -118 208 0
-179 115 0
-179 117 0
-179 160 0
-179 161 0
-179 171 0
-178 -121 207 0
-178 -120 206 0
-178 -119 205 0
-178 -118 204 0
-178 115 0
-178 116 0
-178 158 0
-178 159 0
-178 171 0
-177 -121 203 0
-177 -120 202 0
-177 -119 201 0
-177 -118 200 0
-177 114 0
-177 117 0
-177 156 0
-177 157 0
-177 171 0
-176 -121 199 0
-176 -120 198 0
-176 -119 197 0
-176 -118 196 0
-176 114 0
-176 116 0
-176 154 0
-176 155 0
-176 171 0
-175 -117 195 0
-175 -116 194 0
-175 -115 193 0
-175 -114 192 0
-175 119 0
-175 121 0
-175 140 0
-175 141 0
-175 170 0
-174 -117 191 0
-174 -116 190 0
-174 -115 189 0
-174 -114 188 0
-174 119 0
-174 120 0
-174 138 0
-174 139 0
-174 170 0
-173 -117 187 0
-173 -116 186 0
-173 -115 185 0
-173 -114 184 0
-173 118 0
-173 121 0
-173 136 0
-173 137 0
-173 170 0
-172 -117 183 0
-172 -116 182 0
-172 -115 181 0
-172 -114 180 0
-172 118 0
-172 120 0
-172 134 0
-172 135 0
-172 170 0
-171 -161 -160 -117 -115 179 0
-171 -159 -158 -116 -115 178 0
-171 -157 -156 -117 -114 177 0
-171 -155 -154 -116 -114 176 0
-171 166 167 168 169 0
-170 -141 -140 -121 -119 175 0
-170 -139 -138 -120 -119 174 0
-170 -137 -136 -121 -118 173 0
-170 -135 -134 -120 -118 172 0
-170 162 163 164 165 0
-169 118 0
-169 151 0
-169 152 0
-169 153 0
-169 171 0
-168 119 0
-168 148 0
-168 149 0
-168 150 0
-168 171 0
-167 120 0
-167 145 0
-167 146 0
-167 147 0
-167 171 0
-166 121 0
-166 142 0
-166 143 0
-166 144 0
-166 171 0
-165 114 0
-165 131 0
-165 132 0
-165 133 0
-165 170 0
-164 115 0
-164 128 0
-164 129 0
-164 130 0
-164 170 0
-163 116 0
-163 125 0
-163 126 0
-163 127 0
-163 170 0
-162 117 0
-162 122 0
-162 123 0
-162 124 0
-162 170 0
-161 -116 0
-160 -114 0
-159 -117 0
-158 -114 0
-157 -116 0
-156 -115 0
-155 -117 0
-154 -115 0
-153 -152 -151 -118 169 0
-153 -121 0
-152 -120 0
-151 -119 0
-150 -149 -148 -119 168 0
-150 -121 0
-149 -120 0
-148 -118 0
-147 -146 -145 -120 167 0
-147 -121 0
-146 -119 0
-145 -118 0
-144 -143 -142 -121 166 0
-144 -120 0
-143 -119 0
-142 -118 0
-141 -120 0
-140 -118 0
-139 -121 0
-138 -118 0
-137 -120 0
-136 -119 0
-135 -121 0
-134 -119 0
-133 -132 -131 -114 165 0
-133 -117 0
-132 -116 0
-131 -115 0
-130 -129 -128 -115 164 0
-130 -117 0
-129 -116 0
-128 -114 0
-127 -126 -125 -116 163 0
-127 -117 0
-126 -115 0
-125 -114 0
-124 -123 -122 -117 162 0
-124 -116 0
-123 -115 0
-122 -114 0
-121 -113 -97 0
-121 97 113 0
-120 -112 -96 0
-120 96 112 0
-119 -111 -95 0
-119 95 111 0
-118 -110 -94 0
-118 94 110 0
-117 -109 -93 0
-117 93 109 0
-116 -108 -92 0
-116 92 108 0
-115 -107 -91 0
-115 91 107 0
-114 -106 -90 0
-114 90 106 0
-113 -101 -65 0
-113 65 101 0
-113 97 121 0
-112 -100 -64 0
-112 64 100 0
-112 96 120 0
-111 -99 -63 0
-111 63 99 0
-111 95 119 0
-110 -98 -62 0
-110 62 98 0
-110 94 118 0
-109 -105 -61 0
-109 61 105 0
-109 93 117 0
-108 -104 -60 0
-108 60 104 0
-108 92 116 0
-107 -103 -59 0
-107 59 103 0
-107 91 115 0
-106 -102 -58 0
-106 58 102 0
-106 90 114 0
-105 -89 -87 0
-105 61 109 0
-105 87 89 0
-104 -88 -86 0
-104 60 108 0
-104 86 88 0
-103 -89 -88 0
-103 59 107 0
-103 88 89 0
-102 -87 -86 0
-102 58 106 0
-102 86 87 0
-101 -85 -83 0
-101 65 113 0
-101 83 85 0
-100 -84 -82 0
-100 64 112 0
-100 82 84 0
-99 -85 -84 0
-99 63 111 0
-99 84 85 0
-98 -83 -82 0
-98 62 110 0
-98 82 83 0
-97 -81 -80 0
-97 80 81 0
-97 113 121 0
-96 -79 -78 0
-96 78 79 0
-96 112 120 0
-95 -77 -76 0
-95 76 77 0
-95 111 119 0
-94 -75 -74 0
-94 74 75 0
-94 110 118 0
-93 -73 -72 0
-93 72 73 0
-93 109 117 0
-92 -71 -70 0
-92 70 71 0
-92 108 116 0
-91 -69 -68 0
-91 68 69 0
-91 107 115 0
-90 -67 -66 0
-90 66 67 0
-90 106 114 0
-89 -57 -56 0
-89 56 57 0
-89 87 105 0
-89 88 103 0
-88 -55 -54 0
-88 54 55 0
-88 86 104 0
-88 89 103 0
-87 -53 -52 0
-87 52 53 0
-87 86 102 0
-87 89 105 0
-86 -51 -50 0
-86 50 51 0
-86 87 102 0
-86 88 104 0
-85 -49 -48 0
-85 48 49 0
-85 83 101 0
-85 84 99 0
-84 -47 -46 0
-84 46 47 0
-84 82 100 0
-84 85 99 0
-83 -45 -44 0
-83 44 45 0
-83 82 98 0
-83 85 101 0
-82 -43 -42 0
-82 42 43 0
-82 83 98 0
-82 84 100 0
-81 -32 -28 0
-81 28 32 0
-81 80 97 0
-80 -24 -20 0
-80 20 24 0
-80 81 97 0
-79 -31 -27 0
-79 27 31 0
-79 78 96 0
-78 -23 -19 0
-78 19 23 0
-78 79 96 0
-77 -30 -26 0
-77 26 30 0
-77 76 95 0
-76 -22 -18 0
-76 18 22 0
-76 77 95 0
-75 -29 -25 0
-75 25 29 0
-75 74 94 0
-74 -21 -17 0
-74 17 21 0
-74 75 94 0
-73 -16 -12 0
-73 12 16 0
-73 72 93 0
-72 -8 -4 0
-72 4 8 0
-72 73 93 0
-71 -15 -11 0
-71 11 15 0
-71 70 92 0
-70 -7 -3 0
-70 3 7 0
-70 71 92 0
-69 -14 -10 0
-69 10 14 0
-69 68 91 0
-68 -6 -2 0
-68 2 6 0
-68 69 91 0
-67 -13 -9 0
-67 9 13 0
-67 66 90 0
-66 -5 -1 0
-66 1 5 0
-66 67 90 0
-65 40 0
-65 41 0
-65 101 113 0
-64 39 0
-64 41 0
-64 100 112 0
-63 38 0
-63 41 0
-63 99 111 0
-62 37 0
-62 41 0
-62 98 110 0
-61 36 0
-61 41 0
-61 105 109 0
-60 35 0
-60 41 0
-60 104 108 0
-59 34 0
-59 41 0
-59 103 107 0
-58 33 0
-58 41 0
-58 102 106 0
-57 -32 -31 0
-57 31 32 0
-57 56 89 0
-56 -30 -29 0
-56 29 30 0
-56 57 89 0
-55 -28 -27 0
-55 27 28 0
-55 54 88 0
-54 -26 -25 0
-54 25 26 0
-54 55 88 0
-53 -24 -23 0
-53 23 24 0
-53 52 87 0
-52 -22 -21 0
-52 21 22 0
-52 53 87 0
-51 -20 -19 0
-51 19 20 0
-51 50 86 0
-50 -18 -17 0
-50 17 18 0
-50 51 86 0
-49 -16 -15 0
-49 15 16 0
-49 48 85 0
-48 -14 -13 0
-48 13 14 0
-48 49 85 0
-47 -12 -11 0
-47 11 12 0
-47 46 84 0
-46 -10 -9 0
-46 9 10 0
-46 47 84 0
-45 -8 -7 0
-45 7 8 0
-45 44 83 0
-44 -6 -5 0
-44 5 6 0
-44 45 83 0
-43 -4 -3 0
-43 3 4 0
-43 42 82 0
-42 -2 -1 0
-42 1 2 0
-42 43 82 0
-41 -40 65 0
-41 -39 64 0
-41 -38 63 0
-41 -37 62 0
-41 -36 61 0
-41 -35 60 0
-41 -34 59 0
-41 -33 58 0
-32 28 81 0
-32 31 57 0
-32 211 243 0
-31 27 79 0
-31 32 57 0
-31 210 242 0
-30 26 77 0
-30 29 56 0
-30 209 241 0
-29 25 75 0
-29 30 56 0
-29 208 240 0
-28 27 55 0
-28 32 81 0
-28 207 239 0
-27 28 55 0
-27 31 79 0
-27 206 238 0
-26 25 54 0
-26 30 77 0
-26 205 237 0
-25 26 54 0
-25 29 75 0
-25 204 236 0
-24 20 80 0
-24 23 53 0
-24 203 235 0
-23 19 78 0
-23 24 53 0
-23 202 234 0
-22 18 76 0
-22 21 52 0
-22 201 233 0
-21 17 74 0
-21 22 52 0
-21 200 232 0
-20 19 51 0
-20 24 80 0
-20 199 231 0
-19 20 51 0
-19 23 78 0
-19 198 230 0
-18 17 50 0
-18 22 76 0
-18 197 229 0
-17 18 50 0
-17 21 74 0
-17 196 228 0
-16 12 73 0
-16 15 49 0
-16 195 227 0
-15 11 71 0
-15 16 49 0
-15 194 226 0
-14 10 69 0
-14 13 48 0
-14 193 225 0
-13 9 67 0
-13 14 48 0
-13 192 224 0
-12 11 47 0
-12 16 73 0
-12 191 223 0
-11 12 47 0
-11 15 71 0
-11 190 222 0
-10 9 46 0
-10 14 69 0
-10 189 221 0
-9 10 46 0
-9 13 67 0
-9 188 220 0
-8 4 72 0
-8 7 45 0
-8 187 219 0
-7 3 70 0
-7 8 45 0
-7 186 218 0
-6 2 68 0
-6 5 44 0
-6 185 217 0
-5 1 66 0
-5 6 44 0
-5 184 216 0
-4 3 43 0
-4 8 72 0
-4 183 215 0
-3 4 43 0
-3 7 70 0
-3 182 214 0
-2 1 42 0
-2 6 68 0
-2 181 213 0
-1 2 42 0
-1 5 66 0
-1 180 212 0
114 122 0
114 125 0
114 128 0
114 158 0
114 160 0
115 123 0
115 126 0
115 131 0
115 154 0
115 156 0
116 124 0
116 129 0
116 132 0
116 157 0
116 161 0
117 127 0
117 130 0
117 133 0
117 155 0
117 159 0
118 138 0
118 140 0
118 142 0
118 145 0
118 148 0
119 134 0
119 136 0
119 143 0
119 146 0
119 151 0
120 137 0
120 141 0
120 144 0
120 149 0
120 152 0
121 135 0
121 139 0
121 147 0
121 150 0
121 153 0
%
0