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