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