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