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