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