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