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