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