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