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