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