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