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