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