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