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