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