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