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