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