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