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