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