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