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