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