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