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