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