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