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