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