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