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