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