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