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