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