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