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