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