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