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