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