c This Formular is generated by mcnf
c
c    horn? no 
c    forced? no 
c    mixed sat? no 
c    clause length = 3 
c
p cnf 200  860 
 -164 -36 35 0
192 158 -84 0
22 26 -74 0
112 -65 149 0
-26 170 -117 0
-153 47 -155 0
-74 2 -95 0
-91 -83 -191 0
116 -54 -63 0
88 -145 143 0
124 80 71 0
-15 141 -83 0
74 -188 -27 0
-63 -68 -22 0
97 19 84 0
-64 147 -91 0
16 -40 -98 0
41 23 -184 0
36 150 -2 0
197 171 -153 0
-92 73 -122 0
140 -22 -187 0
34 160 159 0
-152 -62 195 0
87 -116 39 0
-15 88 -120 0
84 10 148 0
-7 81 27 0
10 49 115 0
-72 -88 -149 0
158 142 -31 0
-4 162 -110 0
18 -38 44 0
11 -184 12 0
-86 -73 -194 0
153 141 168 0
-34 180 -179 0
2 49 -174 0
-142 61 92 0
-199 -160 -149 0
129 -109 -90 0
-165 -172 88 0
79 158 -147 0
160 145 -58 0
128 97 93 0
-25 -16 156 0
-21 77 65 0
-7 -97 -178 0
150 -108 125 0
140 -87 119 0
80 187 -22 0
-129 121 10 0
-14 -35 126 0
173 -138 -181 0
120 -85 -26 0
45 196 175 0
1 -159 195 0
-39 -166 59 0
37 130 -184 0
-158 -147 -14 0
-171 30 -127 0
20 -97 115 0
39 -146 -32 0
-143 -146 -119 0
56 -121 91 0
-1 75 105 0
-84 40 99 0
65 -93 151 0
86 133 -5 0
148 -116 -89 0
114 -186 67 0
-20 -196 -126 0
123 -58 73 0
-132 40 195 0
-105 191 -170 0
185 -142 141 0
137 180 49 0
-44 21 100 0
-179 -25 -93 0
-28 66 -126 0
152 43 96 0
-146 31 -36 0
-35 136 153 0
188 31 71 0
-16 32 -97 0
-96 181 197 0
48 18 121 0
-16 -46 149 0
14 168 31 0
115 63 66 0
-166 100 -75 0
-53 139 -165 0
-186 37 22 0
-135 -18 169 0
1 17 79 0
161 -193 183 0
-182 -8 13 0
-122 -166 71 0
-145 36 -93 0
129 2 11 0
91 29 -31 0
-147 -45 -194 0
194 112 140 0
139 -200 76 0
27 42 -78 0
-75 139 174 0
91 -159 81 0
-58 -111 183 0
-38 -113 -145 0
192 67 8 0
179 186 -190 0
-104 160 -66 0
-158 16 150 0
-33 -167 -8 0
174 22 186 0
-192 20 -52 0
-130 -146 -88 0
-171 79 -122 0
-184 106 142 0
-169 61 -118 0
20 65 172 0
200 -176 160 0
-193 140 158 0
89 44 137 0
127 -3 -86 0
-196 176 24 0
-180 -47 45 0
-20 127 155 0
-8 -130 58 0
170 -86 94 0
13 126 26 0
-107 73 120 0
-166 31 181 0
-135 -16 -151 0
-84 -129 -197 0
27 197 -53 0
125 139 17 0
99 -55 58 0
101 -110 80 0
-162 -185 -169 0
-85 188 -148 0
82 165 119 0
-125 -108 64 0
-48 -87 148 0
-167 100 -33 0
87 144 182 0
-15 162 -186 0
142 -184 104 0
-43 -14 -177 0
38 108 15 0
65 -130 16 0
68 -179 -58 0
-49 53 100 0
42 100 79 0
-133 -128 -127 0
21 -63 99 0
-133 176 -41 0
106 78 4 0
70 161 -149 0
-21 -179 95 0
189 -39 162 0
-157 -123 64 0
51 29 20 0
125 127 42 0
-42 35 70 0
-199 191 85 0
184 -172 -155 0
63 169 -135 0
163 149 -118 0
-96 -63 -167 0
12 -197 -161 0
128 -140 147 0
-188 -51 32 0
113 96 4 0
-163 -195 88 0
99 171 83 0
-34 195 -179 0
45 -63 -16 0
-132 -97 -44 0
161 90 137 0
135 -118 -68 0
55 -11 129 0
199 -36 67 0
163 -43 148 0
149 -139 -164 0
182 -121 100 0
-184 192 87 0
-116 22 112 0
-33 198 67 0
54 152 -183 0
199 18 89 0
175 -50 17 0
138 77 63 0
-73 91 96 0
-183 -123 50 0
133 139 -104 0
48 11 -20 0
-105 9 -58 0
-65 130 6 0
-59 50 -199 0
195 -147 -76 0
68 16 -123 0
-69 -184 2 0
41 -15 189 0
-122 -33 -105 0
-58 136 66 0
-46 -101 -50 0
-162 -58 113 0
23 24 79 0
-67 -191 85 0
-91 167 -162 0
190 -145 96 0
168 75 -141 0
145 62 147 0
-75 -139 -7 0
-186 -1 -83 0
141 -146 128 0
120 153 -115 0
-184 -178 16 0
-146 75 -27 0
-68 -20 137 0
133 -107 39 0
100 -62 175 0
-169 106 -186 0
71 -182 61 0
-34 -2 114 0
-63 -85 -186 0
124 44 -190 0
107 27 17 0
-78 -80 -35 0
-32 -10 -170 0
25 -43 -7 0
-139 -67 195 0
40 -71 80 0
-109 -41 -169 0
112 -11 -155 0
4 -180 -177 0
-161 129 -187 0
8 -97 -22 0
-175 62 25 0
88 -117 -14 0
-178 2 -149 0
75 -172 -68 0
12 133 -21 0
17 -194 34 0
45 25 -156 0
-26 -45 -155 0
-114 -74 138 0
-105 -146 196 0
-98 194 -9 0
-171 -79 170 0
79 -162 81 0
-199 50 153 0
-199 135 33 0
10 158 4 0
-163 -59 117 0
168 63 -15 0
128 94 200 0
-168 28 164 0
10 32 180 0
-51 -12 -128 0
20 -111 175 0
-185 -87 -164 0
-14 -135 21 0
-200 -144 -75 0
-49 -7 136 0
88 193 -190 0
132 -12 36 0
-88 -10 138 0
152 -186 -16 0
151 -14 -179 0
-166 -78 -145 0
-104 -71 -184 0
141 -54 -189 0
-151 -114 -161 0
-138 -91 -140 0
68 143 -7 0
-184 -1 -17 0
-146 -80 -36 0
109 111 -70 0
-13 -141 136 0
196 -59 72 0
-191 157 35 0
103 -176 53 0
146 -43 161 0
-11 129 152 0
12 52 128 0
-101 50 -40 0
152 -108 112 0
55 -90 88 0
-27 115 -132 0
-46 -73 40 0
-56 -148 96 0
143 -61 148 0
-95 75 18 0
-114 -10 21 0
47 -38 40 0
58 84 191 0
-191 -98 -165 0
-140 -197 -27 0
1 110 -114 0
-88 -131 148 0
22 189 167 0
-35 -28 101 0
-152 106 -200 0
-81 63 -105 0
105 172 119 0
-136 -120 39 0
106 -168 104 0
9 118 175 0
-4 -176 -100 0
96 -74 155 0
-64 -61 -173 0
178 68 73 0
-150 82 157 0
161 94 -27 0
-44 -98 -69 0
52 176 55 0
129 -55 -86 0
-40 85 -41 0
47 169 25 0
-69 72 123 0
-131 -122 10 0
4 75 142 0
48 -116 -162 0
19 158 -138 0
-69 99 -38 0
26 -167 -30 0
121 156 -49 0
-140 -91 -40 0
71 198 -109 0
175 109 39 0
-120 -125 -41 0
-124 -81 -148 0
-97 -82 83 0
-87 53 59 0
-135 35 -8 0
48 -167 -33 0
81 40 72 0
-20 109 97 0
163 -132 -131 0
-121 62 27 0
36 -82 -41 0
-60 51 196 0
147 -99 -116 0
121 -163 92 0
43 105 -80 0
-143 -69 -196 0
-139 -196 16 0
142 -74 -193 0
-18 37 -155 0
127 131 43 0
-121 -143 144 0
82 -65 75 0
-193 -141 -76 0
-178 -16 -28 0
-71 51 47 0
-189 178 -190 0
11 176 -180 0
-88 67 -120 0
-155 -29 133 0
-99 -33 -108 0
-193 135 142 0
97 -77 12 0
-56 50 151 0
93 -168 -32 0
-83 -49 -25 0
155 -186 -105 0
-132 -65 48 0
-28 -197 59 0
181 65 -39 0
5 -173 38 0
-200 118 -18 0
-75 146 -50 0
-132 117 -188 0
-62 77 -24 0
-90 -93 88 0
-158 122 -168 0
160 101 128 0
-200 -154 133 0
-146 -6 -105 0
-84 -195 85 0
-22 79 -128 0
171 14 53 0
115 22 -29 0
-75 -153 178 0
172 -6 -78 0
-63 -198 -78 0
-142 157 -146 0
70 169 -189 0
71 91 149 0
131 42 76 0
8 -160 49 0
-17 91 192 0
-130 155 16 0
114 -124 -122 0
133 -103 -33 0
-60 118 89 0
-143 -20 128 0
-182 111 168 0
-28 142 -144 0
-140 -137 -17 0
-102 -5 45 0
-28 -56 67 0
-169 -172 -158 0
156 -195 -128 0
15 83 69 0
158 -156 -18 0
-50 -173 -185 0
-164 97 -146 0
108 188 109 0
166 -102 -135 0
47 90 145 0
-194 142 -64 0
152 -23 -88 0
-11 51 -107 0
-171 51 95 0
95 -132 117 0
-130 -189 151 0
185 118 -31 0
-191 -26 98 0
116 162 187 0
-115 -178 -129 0
85 -162 88 0
-61 46 -127 0
123 87 127 0
112 -147 199 0
111 82 -23 0
177 -120 159 0
161 -58 -133 0
-189 -113 -80 0
-153 -45 57 0
196 54 -104 0
-16 -70 60 0
-60 -95 -114 0
185 170 -17 0
174 -37 -195 0
-53 183 191 0
-97 -17 154 0
-12 51 -182 0
29 27 133 0
-194 65 54 0
-126 -148 24 0
-200 -1 42 0
40 167 -82 0
-185 -120 151 0
-134 -158 106 0
28 -72 148 0
-76 -187 52 0
148 179 175 0
-153 -185 -186 0
145 35 108 0
50 -126 197 0
175 -100 92 0
18 -82 69 0
-3 133 125 0
-139 190 -118 0
-11 169 165 0
-85 181 113 0
15 38 102 0
104 -59 182 0
97 102 53 0
-182 -72 -64 0
159 66 -126 0
-90 -56 183 0
40 42 96 0
-84 -167 159 0
33 -163 93 0
-42 -67 -141 0
112 27 -37 0
132 57 17 0
85 162 53 0
-65 131 -196 0
-32 68 -170 0
-154 146 -133 0
-166 -171 7 0
-68 -82 -46 0
-154 -190 74 0
52 -179 168 0
127 104 -148 0
9 59 -157 0
-100 108 -36 0
-89 -182 152 0
63 182 77 0
-32 -129 130 0
-165 197 -81 0
-76 112 29 0
73 -146 -38 0
-122 -171 -149 0
-25 31 80 0
176 174 64 0
178 171 188 0
-63 -155 191 0
68 101 69 0
167 123 -99 0
-114 -52 -82 0
52 86 148 0
84 155 -185 0
173 -122 -63 0
110 -106 -83 0
-117 65 -10 0
-175 -93 4 0
-152 16 -49 0
-99 -63 -26 0
123 14 69 0
-164 -139 -85 0
92 112 -18 0
190 -186 166 0
-142 -20 119 0
-131 -104 36 0
-19 73 -197 0
29 138 46 0
-197 21 -65 0
-17 -1 -5 0
-157 98 -90 0
52 116 -72 0
182 47 55 0
-106 90 -107 0
-155 68 -167 0
146 -160 -32 0
-35 4 43 0
23 33 109 0
164 -165 -91 0
36 89 10 0
-137 195 -172 0
-96 -64 -127 0
-200 193 11 0
110 -33 -36 0
-142 -139 -59 0
-163 78 -101 0
-58 141 -194 0
-162 -79 156 0
43 96 -58 0
-47 -38 99 0
-12 152 -118 0
43 -143 -104 0
-200 88 61 0
179 -103 143 0
196 -27 76 0
135 144 -17 0
-15 -99 -46 0
-100 134 -60 0
-7 -67 23 0
188 -98 -30 0
-129 -127 -105 0
48 -193 -60 0
-65 -10 128 0
44 -176 -81 0
68 -113 81 0
-58 105 -198 0
-124 -98 168 0
-176 -55 87 0
-118 22 -32 0
181 156 70 0
-133 110 152 0
107 -196 99 0
152 153 -144 0
-94 -173 144 0
-83 152 187 0
-199 146 149 0
152 182 -17 0
139 8 147 0
-5 140 -176 0
-180 147 -99 0
-5 98 -56 0
-175 199 -114 0
-184 187 177 0
-133 74 162 0
-55 -1 173 0
-64 -172 170 0
-51 100 15 0
-133 74 -51 0
132 137 193 0
118 99 -15 0
-162 115 154 0
-148 84 178 0
26 180 -142 0
-196 -21 -83 0
2 -31 26 0
-199 83 192 0
31 -162 -108 0
77 151 135 0
163 22 -44 0
-172 11 -187 0
75 -27 190 0
-90 9 166 0
152 -94 40 0
-110 -74 88 0
110 90 -108 0
3 -162 -193 0
-116 -149 161 0
-65 -59 -91 0
61 -44 -45 0
124 -52 -49 0
23 -100 146 0
-11 -42 -34 0
-23 -20 59 0
-70 32 72 0
-55 -170 85 0
89 13 122 0
-120 38 89 0
153 -32 63 0
-38 -14 -65 0
143 182 81 0
-49 174 -83 0
-18 127 -147 0
151 32 -188 0
-47 -80 146 0
-22 -131 -55 0
173 -6 -114 0
-164 -195 -48 0
67 52 160 0
-187 112 81 0
5 -45 -1 0
-200 -120 -164 0
35 138 135 0
-11 -115 -88 0
171 156 65 0
-121 -93 132 0
80 152 -198 0
-184 -100 -109 0
154 -192 72 0
194 -132 196 0
145 103 -176 0
-155 -104 -79 0
124 130 42 0
189 1 -16 0
100 36 108 0
-179 -39 193 0
-80 69 121 0
-101 -144 197 0
-167 165 44 0
158 124 121 0
-155 -198 -53 0
165 -31 36 0
-152 89 -200 0
191 -198 -140 0
119 138 -87 0
-54 -157 104 0
-73 -69 84 0
-164 104 -161 0
138 41 -191 0
-40 194 -107 0
-33 -87 -66 0
190 -66 -39 0
-145 -138 -95 0
99 -38 186 0
-59 155 54 0
-74 114 -174 0
-110 -39 33 0
139 -58 144 0
-178 -61 -82 0
24 -8 151 0
-165 -46 -145 0
-106 96 -33 0
146 183 -2 0
133 -194 -25 0
11 -181 -161 0
-24 -199 -136 0
69 -81 -162 0
152 -106 108 0
-174 115 97 0
-199 -53 52 0
150 135 -3 0
-14 -165 -68 0
-81 -124 97 0
-60 -139 133 0
27 125 -56 0
82 -34 -102 0
-72 -133 -163 0
130 -189 59 0
-45 -37 161 0
182 19 12 0
-4 178 129 0
104 133 180 0
1 2 76 0
82 74 90 0
-129 32 -101 0
-35 -73 175 0
-10 -81 169 0
-76 148 42 0
5 -89 -144 0
176 -59 27 0
73 -34 -168 0
83 -6 -26 0
-91 71 -121 0
-3 -27 -16 0
-141 -97 5 0
61 46 37 0
-174 176 39 0
173 117 -104 0
21 -51 154 0
-183 -137 -171 0
191 -164 189 0
59 -166 57 0
131 137 199 0
-160 51 98 0
-187 70 -31 0
101 47 98 0
171 132 55 0
-110 -160 -156 0
156 153 -36 0
-148 53 192 0
112 -110 -95 0
-98 -170 -100 0
-171 106 88 0
-111 169 34 0
68 -169 -151 0
108 60 71 0
170 -166 38 0
199 89 -140 0
-167 125 -122 0
99 -137 112 0
10 -103 -119 0
-149 -75 153 0
-20 142 -159 0
112 -195 -97 0
176 -93 103 0
147 151 -2 0
51 -179 -181 0
73 -185 67 0
-4 56 89 0
-67 -64 -175 0
69 -98 67 0
-176 12 77 0
-80 -88 -26 0
-41 123 -24 0
-12 91 -176 0
-102 -129 -24 0
-66 -173 197 0
183 -9 99 0
177 -195 -140 0
113 -135 -54 0
14 -22 42 0
21 -56 -12 0
-29 -181 -150 0
144 -165 99 0
47 -78 157 0
13 178 99 0
-93 35 -144 0
-45 81 -122 0
-98 150 75 0
-19 -80 117 0
-51 192 60 0
-37 138 -109 0
122 88 41 0
153 -179 197 0
-66 -193 109 0
-64 -18 -79 0
-196 -4 -62 0
-65 -107 191 0
-152 -102 50 0
178 -195 -17 0
174 -40 -2 0
176 159 -173 0
-141 127 64 0
3 -182 115 0
78 -107 38 0
79 167 54 0
49 194 174 0
179 -172 -163 0
-55 -106 -175 0
13 -36 12 0
-64 9 -171 0
-133 -137 183 0
-143 -137 184 0
98 33 -192 0
-177 15 -187 0
-193 128 125 0
-152 177 -150 0
-146 -26 45 0
17 28 55 0
-159 77 -71 0
-61 58 -63 0
-198 -172 -84 0
56 -51 -192 0
-122 197 149 0
-33 -163 -126 0
38 -168 48 0
6 151 -39 0
55 154 -195 0
-168 -176 -171 0
165 184 138 0
-80 124 -12 0
195 -29 115 0
-177 172 166 0
-146 -186 -195 0
92 -66 130 0
74 -34 -141 0
-49 -155 -192 0
-176 -165 80 0
-160 -81 -84 0
100 -89 50 0
-47 191 -38 0
-150 125 -153 0
-49 63 104 0
-27 -164 -120 0
-95 17 -6 0
-149 93 -114 0
-185 -28 -113 0
-76 -17 63 0
-19 171 -29 0
55 -174 163 0
183 67 -102 0
-85 -37 -8 0
197 49 -192 0
-125 -47 -106 0
99 40 160 0
-71 -82 -144 0
-152 62 33 0
-136 55 127 0
-39 -129 -169 0
-91 153 -113 0
-23 -134 -194 0
173 -163 106 0
-86 -23 167 0
38 -34 -198 0
120 -99 64 0
94 -83 -188 0
-34 -167 80 0
-179 83 -70 0
-175 -120 -8 0
-123 -69 52 0
40 -35 84 0
144 156 44 0
-70 74 123 0
-114 -194 125 0
-74 88 142 0
127 -113 117 0
-89 -83 195 0
173 -176 -162 0
101 -28 -174 0
98 -23 27 0
122 75 -12 0
77 -175 -35 0
-160 -79 116 0
102 74 57 0
15 197 -28 0
-140 -158 -50 0
-104 -74 110 0
-78 104 94 0
22 128 142 0
-84 18 37 0
-86 -198 31 0
-71 -53 100 0
196 68 -148 0
157 -82 -101 0
-139 -44 -121 0
47 -41 -177 0
104 47 -179 0
-48 -23 36 0
169 -69 -178 0
173 105 -182 0
73 127 -177 0
-175 -108 200 0
-122 -159 -49 0
53 -123 -29 0
-168 164 -100 0
85 -130 -106 0
14 -153 -16 0
%
0