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