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