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