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