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