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