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