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