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