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