c cnf generated by mark.reason.apps.PlgToDimacs written by Mark Chavira
c cnf generated on Wed Nov 17 12:34:50 PST 2004.
c
c Following is the map back to variable name:
c
c 1 X_1_1gat_input
c 2 X_4_4gat_input
c 3 X_8_8gat_input
c 4 X_11_11gat_input
c 5 X_14_14gat_input
c 6 X_17_17gat_input
c 7 X_21_21gat_input
c 8 X_24_24gat_input
c 9 X_27_27gat_input
c 10 X_30_30gat_input
c 11 X_34_34gat_input
c 12 X_37_37gat_input
c 13 X_40_40gat_input
c 14 X_43_43gat_input
c 15 X_47_47gat_input
c 16 X_50_50gat_input
c 17 X_53_53gat_input
c 18 X_56_56gat_input
c 19 X_60_60gat_input
c 20 X_63_63gat_input
c 21 X_66_66gat_input
c 22 X_69_69gat_input
c 23 X_73_73gat_input
c 24 X_76_76gat_input
c 25 X_79_79gat_input
c 26 X_82_82gat_input
c 27 X_86_86gat_input
c 28 X_89_89gat_input
c 29 X_92_92gat_input
c 30 X_95_95gat_input
c 31 X_99_99gat_input
c 32 X_102_102gat_input
c 33 X_105_105gat_input
c 34 X_108_108gat_input
c 35 X_112_112gat_input
c 36 X_115_115gat_input
c 37 X_118_118gat_internal
c 38 X_119_119gat_internal
c 39 X_122_122gat_internal
c 40 X_123_123gat_internal
c 41 X_126_126gat_internal
c 42 X_127_127gat_internal
c 43 X_130_130gat_internal
c 44 X_131_131gat_internal
c 45 X_134_134gat_internal
c 46 X_135_135gat_internal
c 47 X_138_138gat_internal
c 48 X_139_139gat_internal
c 49 X_142_142gat_internal
c 50 X_143_143gat_internal
c 51 X_146_146gat_internal
c 52 X_147_147gat_internal
c 53 X_150_150gat_internal
c 54 X_151_151gat_internal
c 55 X_154_154gat_internal
c 56 X_157_157gat_internal
c 57 X_158_158gat_internal
c 58 X_159_159gat_internal
c 59 X_162_162gat_internal
c 60 X_165_165gat_internal
c 61 X_168_168gat_internal
c 62 X_171_171gat_internal
c 63 X_174_174gat_internal
c 64 X_177_177gat_internal
c 65 X_180_180gat_internal
c 66 X_183_183gat_internal
c 67 X_184_184gat_internal
c 68 X_185_185gat_internal
c 69 X_186_186gat_internal
c 70 X_187_187gat_internal
c 71 X_188_188gat_internal
c 72 X_189_189gat_internal
c 73 X_190_190gat_internal
c 74 X_191_191gat_internal
c 75 X_192_192gat_internal
c 76 X_193_193gat_internal
c 77 X_194_194gat_internal
c 78 X_195_195gat_internal
c 79 X_196_196gat_internal
c 80 X_197_197gat_internal
c 81 X_198_198gat_internal
c 82 X_199_199gat_internal
c 83 X_203_203gat_internal
c 84 X_213_213gat_internal
c 85 X_223_223gat_output
c 86 X_224_224gat_internal
c 87 X_227_227gat_internal
c 88 X_230_230gat_internal
c 89 X_233_233gat_internal
c 90 X_236_236gat_internal
c 91 X_239_239gat_internal
c 92 X_242_242gat_internal
c 93 X_243_243gat_internal
c 94 X_246_246gat_internal
c 95 X_247_247gat_internal
c 96 X_250_250gat_internal
c 97 X_251_251gat_internal
c 98 X_254_254gat_internal
c 99 X_255_255gat_internal
c 100 X_256_256gat_internal
c 101 X_257_257gat_internal
c 102 X_258_258gat_internal
c 103 X_259_259gat_internal
c 104 X_260_260gat_internal
c 105 X_263_263gat_internal
c 106 X_264_264gat_internal
c 107 X_267_267gat_internal
c 108 X_270_270gat_internal
c 109 X_273_273gat_internal
c 110 X_276_276gat_internal
c 111 X_279_279gat_internal
c 112 X_282_282gat_internal
c 113 X_285_285gat_internal
c 114 X_288_288gat_internal
c 115 X_289_289gat_internal
c 116 X_290_290gat_internal
c 117 X_291_291gat_internal
c 118 X_292_292gat_internal
c 119 X_293_293gat_internal
c 120 X_294_294gat_internal
c 121 X_295_295gat_internal
c 122 X_296_296gat_internal
c 123 X_300_300gat_internal
c 124 X_301_301gat_internal
c 125 X_302_302gat_internal
c 126 X_303_303gat_internal
c 127 X_304_304gat_internal
c 128 X_305_305gat_internal
c 129 X_306_306gat_internal
c 130 X_307_307gat_internal
c 131 X_308_308gat_internal
c 132 X_309_309gat_internal
c 133 X_319_319gat_internal
c 134 X_329_329gat_output
c 135 X_330_330gat_internal
c 136 X_331_331gat_internal
c 137 X_332_332gat_internal
c 138 X_333_333gat_internal
c 139 X_334_334gat_internal
c 140 X_335_335gat_internal
c 141 X_336_336gat_internal
c 142 X_337_337gat_internal
c 143 X_338_338gat_internal
c 144 X_339_339gat_internal
c 145 X_340_340gat_internal
c 146 X_341_341gat_internal
c 147 X_342_342gat_internal
c 148 X_343_343gat_internal
c 149 X_344_344gat_internal
c 150 X_345_345gat_internal
c 151 X_346_346gat_internal
c 152 X_347_347gat_internal
c 153 X_348_348gat_internal
c 154 X_349_349gat_internal
c 155 X_350_350gat_internal
c 156 X_351_351gat_internal
c 157 X_352_352gat_internal
c 158 X_353_353gat_internal
c 159 X_354_354gat_internal
c 160 X_355_355gat_internal
c 161 X_356_356gat_internal
c 162 X_357_357gat_internal
c 163 X_360_360gat_internal
c 164 X_370_370gat_output
c 165 X_371_371gat_internal
c 166 X_372_372gat_internal
c 167 X_373_373gat_internal
c 168 X_374_374gat_internal
c 169 X_375_375gat_internal
c 170 X_376_376gat_internal
c 171 X_377_377gat_internal
c 172 X_378_378gat_internal
c 173 X_379_379gat_internal
c 174 X_380_380gat_internal
c 175 X_381_381gat_internal
c 176 X_386_386gat_internal
c 177 X_393_393gat_internal
c 178 X_399_399gat_internal
c 179 X_404_404gat_internal
c 180 X_407_407gat_internal
c 181 X_411_411gat_internal
c 182 X_414_414gat_internal
c 183 X_415_415gat_internal
c 184 X_416_416gat_internal
c 185 X_417_417gat_internal
c 186 X_418_418gat_internal
c 187 X_419_419gat_internal
c 188 X_420_420gat_internal
c 189 X_421_421gat_output
c 190 X_422_422gat_internal
c 191 X_425_425gat_internal
c 192 X_428_428gat_internal
c 193 X_429_429gat_internal
c 194 X_430_430gat_output
c 195 X_431_431gat_output
c 196 X_432_432gat_output
c
p cnf 196 514
-196 -193 -191 -190 -175 0
-195 -192 -191 -176 -175 0
-194 -190 -178 -176 -175 0
-193 -188 -180 -177 -176 0
-192 -187 -178 -177 0
-191 -186 -178 -177 -176 0
-190 -185 -176 0
-189 -184 0
-189 -183 0
-188 -181 0
-187 -180 0
-186 -179 0
-185 -177 0
-184 175 0
-184 176 0
-184 177 0
-184 178 0
-184 179 0
-184 180 0
-184 181 0
-184 182 0
-183 -174 0
-182 -181 -180 -179 -178 -177 -176 -175 184 0
-182 -173 -152 -103 -34 0
-181 -172 -151 -102 -30 0
-180 -171 -150 -101 -26 0
-179 -170 -149 -100 -22 0
-178 -169 -147 -99 -18 0
-177 -168 -145 -98 -14 0
-176 -167 -143 -96 -10 0
-175 -166 -141 -94 -6 0
-174 -165 -139 -92 -2 0
-173 -163 -36 0
-172 -163 -33 0
-171 -163 -29 0
-170 -163 -25 0
-169 -163 -21 0
-168 -163 -17 0
-167 -163 -13 0
-166 -163 -9 0
-165 -163 -5 0
-164 -162 0
-163 -162 0
-162 153 0
-162 154 0
-162 155 0
-162 156 0
-162 157 0
-162 158 0
-162 159 0
-162 160 0
-162 161 0
-161 -160 -159 -158 -157 -156 -155 -154 -153 162 0
-161 -148 -131 0
-160 -146 -130 0
-159 -144 -129 0
-158 -142 -128 0
-157 -140 -127 0
-156 -138 -126 0
-155 -137 -125 0
-154 -136 -124 0
-153 -135 -123 0
-152 -133 -35 0
-151 -133 -31 0
-150 -133 -27 0
-149 -133 -23 0
-148 -132 -113 0
-148 113 132 0
-147 -133 -19 0
-146 -132 -112 0
-146 112 132 0
-145 -133 -15 0
-144 -132 -111 0
-144 111 132 0
-143 -133 -11 0
-142 -132 -110 0
-142 110 132 0
-141 -133 -7 0
-140 -132 -109 0
-140 109 132 0
-139 -133 -3 0
-138 -132 -108 0
-138 108 132 0
-137 -132 -107 0
-137 107 132 0
-136 -132 -106 0
-136 106 132 0
-135 -132 -104 0
-135 104 132 0
-134 -122 0
-133 -122 0
-132 -122 0
-132 104 135 0
-132 106 136 0
-132 107 137 0
-132 108 138 0
-132 109 140 0
-132 110 142 0
-132 111 144 0
-132 112 146 0
-132 113 148 0
-131 -121 0
-130 -120 0
-129 -119 0
-128 -118 0
-127 -117 0
-126 -116 0
-125 -115 0
-124 -114 0
-123 -105 0
-122 104 0
-122 106 0
-122 107 0
-122 108 0
-122 109 0
-122 110 0
-122 111 0
-122 112 0
-122 113 0
-121 -97 -81 0
-120 -95 -79 0
-119 -93 -77 0
-118 -91 -75 0
-117 -90 -73 0
-116 -89 -71 0
-115 -88 -69 0
-114 -87 -67 0
-113 -112 -111 -110 -109 -108 -107 -106 -104 122 0
-113 -97 -80 0
-113 132 148 0
-112 -95 -78 0
-112 132 146 0
-111 -93 -76 0
-111 132 144 0
-110 -91 -74 0
-110 132 142 0
-109 -90 -72 0
-109 132 140 0
-108 -89 -70 0
-108 132 138 0
-107 -88 -68 0
-107 132 137 0
-106 -87 -66 0
-106 132 136 0
-105 -86 -57 0
-104 -86 -56 0
-104 132 135 0
-103 -84 -32 0
-102 -84 -28 0
-101 -84 -24 0
-100 -84 -20 0
-99 -84 -16 0
-98 -84 -12 0
-97 -83 -65 0
-97 65 83 0
-96 -84 -8 0
-95 -83 -64 0
-95 64 83 0
-94 -84 -4 0
-93 -83 -63 0
-93 63 83 0
-92 -84 -1 0
-91 -83 -62 0
-91 62 83 0
-90 -83 -61 0
-90 61 83 0
-89 -83 -60 0
-89 60 83 0
-88 -83 -59 0
-88 59 83 0
-87 -83 -58 0
-87 58 83 0
-86 -83 -55 0
-86 55 83 0
-85 -82 0
-84 -82 0
-83 -82 0
-83 55 86 0
-83 58 87 0
-83 59 88 0
-83 60 89 0
-83 61 90 0
-83 62 91 0
-83 63 93 0
-83 64 95 0
-83 65 97 0
-82 55 0
-82 58 0
-82 59 0
-82 60 0
-82 61 0
-82 62 0
-82 63 0
-82 64 0
-82 65 0
-81 -54 0
-81 -36 0
-80 -54 0
-80 -35 0
-79 -52 0
-79 -33 0
-78 -52 0
-78 -31 0
-77 -50 0
-77 -29 0
-76 -50 0
-76 -27 0
-75 -48 0
-75 -25 0
-74 -48 0
-74 -23 0
-73 -46 0
-73 -21 0
-72 -46 0
-72 -19 0
-71 -44 0
-71 -17 0
-70 -44 0
-70 -15 0
-69 -42 0
-69 -13 0
-68 -42 0
-68 -11 0
-67 -40 0
-67 -9 0
-66 -40 0
-66 -7 0
-65 -64 -63 -62 -61 -60 -59 -58 -55 82 0
-65 -53 -34 0
-65 83 97 0
-64 -51 -30 0
-64 83 95 0
-63 -49 -26 0
-63 83 93 0
-62 -47 -22 0
-62 83 91 0
-61 -45 -18 0
-61 83 90 0
-60 -43 -14 0
-60 83 89 0
-59 -41 -10 0
-59 83 88 0
-58 -39 -6 0
-58 83 87 0
-57 -38 0
-57 -5 0
-56 -38 0
-56 -3 0
-55 -37 -2 0
-55 83 86 0
-54 -34 0
-53 -32 0
-52 -30 0
-51 -28 0
-50 -26 0
-49 -24 0
-48 -22 0
-47 -20 0
-46 -18 0
-45 -16 0
-44 -14 0
-43 -12 0
-42 -10 0
-41 -8 0
-40 -6 0
-39 -4 0
-38 -2 0
-37 -1 0
1 37 0
1 92 0
2 38 0
2 55 0
2 174 0
3 38 56 0
3 139 0
4 39 0
4 94 0
5 38 57 0
5 165 0
6 40 0
6 58 0
6 175 0
7 40 66 0
7 141 0
8 41 0
8 96 0
9 40 67 0
9 166 0
10 42 0
10 59 0
10 176 0
11 42 68 0
11 143 0
12 43 0
12 98 0
13 42 69 0
13 167 0
14 44 0
14 60 0
14 177 0
15 44 70 0
15 145 0
16 45 0
16 99 0
17 44 71 0
17 168 0
18 46 0
18 61 0
18 178 0
19 46 72 0
19 147 0
20 47 0
20 100 0
21 46 73 0
21 169 0
22 48 0
22 62 0
22 179 0
23 48 74 0
23 149 0
24 49 0
24 101 0
25 48 75 0
25 170 0
26 50 0
26 63 0
26 180 0
27 50 76 0
27 150 0
28 51 0
28 102 0
29 50 77 0
29 171 0
30 52 0
30 64 0
30 181 0
31 52 78 0
31 151 0
32 53 0
32 103 0
33 52 79 0
33 172 0
34 54 0
34 65 0
34 182 0
35 54 80 0
35 152 0
36 54 81 0
36 173 0
37 55 0
39 58 0
41 59 0
43 60 0
45 61 0
47 62 0
49 63 0
51 64 0
53 65 0
56 104 0
57 105 0
66 106 0
67 114 0
68 107 0
69 115 0
70 108 0
71 116 0
72 109 0
73 117 0
74 110 0
75 118 0
76 111 0
77 119 0
78 112 0
79 120 0
80 113 0
81 121 0
82 83 0
82 84 0
82 85 0
84 92 0
84 94 0
84 96 0
84 98 0
84 99 0
84 100 0
84 101 0
84 102 0
84 103 0
86 104 0
86 105 0
87 106 0
87 114 0
88 107 0
88 115 0
89 108 0
89 116 0
90 109 0
90 117 0
91 110 0
91 118 0
92 174 0
93 111 0
93 119 0
94 175 0
95 112 0
95 120 0
96 176 0
97 113 0
97 121 0
98 177 0
99 178 0
100 179 0
101 180 0
102 181 0
103 182 0
105 123 0
114 124 0
115 125 0
116 126 0
117 127 0
118 128 0
119 129 0
120 130 0
121 131 0
122 132 0
122 133 0
122 134 0
123 153 0
124 154 0
125 155 0
126 156 0
127 157 0
128 158 0
129 159 0
130 160 0
131 161 0
133 139 0
133 141 0
133 143 0
133 145 0
133 147 0
133 149 0
133 150 0
133 151 0
133 152 0
135 153 0
136 154 0
137 155 0
138 156 0
139 174 0
140 157 0
141 175 0
142 158 0
143 176 0
144 159 0
145 177 0
146 160 0
147 178 0
148 161 0
149 179 0
150 180 0
151 181 0
152 182 0
162 163 0
162 164 0
163 165 0
163 166 0
163 167 0
163 168 0
163 169 0
163 170 0
163 171 0
163 172 0
163 173 0
165 174 0
166 175 0
167 176 0
168 177 0
169 178 0
170 179 0
171 180 0
172 181 0
173 182 0
174 183 0
175 194 0
175 195 0
175 196 0
176 190 0
176 191 0
176 193 0
176 194 0
176 195 0
177 185 0
177 191 0
177 192 0
177 193 0
178 191 0
178 192 0
178 194 0
179 186 0
180 187 0
180 193 0
181 188 0
183 184 189 0
185 190 0
186 191 0
187 192 0
188 193 0
190 194 0
190 196 0
191 195 0
191 196 0
192 195 0
193 196 0
%
0