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