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