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