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