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