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