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