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