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