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