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