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