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