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