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