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