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