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