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