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