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