c status 10
c--failedmineff=0
c--minimizedepth=2
c--otfs=0
c--phase=0
c--probeinit=0
c--probeint=0
c--reduceinit=0
c--rephaseinit=96
c--substitute=0
c--ternary=0
c--vivifymineff=0
p cnf 129 198
-1 -5 0
3 -4 0
5 -2 0
-6 -3 0
-9 7 0
14 -12 19 0
9 -13 0
17 -15 0
-19 4 0
6 -13 0
-19 17 2 0
-16 17 13 0
-18 15 5 0
11 -18 0
16 12 0
12 -9 0
-23 10 0
26 -23 0
22 -11 0
27 25 0
20 -22 -21 27 0
-10 28 -25 0
34 1 0
24 -37 0
20 -7 -36 0
40 41 0
26 -24 0
21 31 0
-23 -17 0
-32 -27 0
-20 -33 0
-28 -30 0
25 -19 15 0
23 -40 -27 0
-43 32 40 0
37 21 0
-64 68 0
-51 -24 0
-48 8 0
-53 37 0
67 -35 -60 0
-56 -66 -59 -31 0
-44 32 0
-66 48 51 0
-42 -57 -50 0
23 55 32 0
-37 -35 -68 0
-58 55 -56 0
22 16 0
-49 18 0
-40 -50 60 0
35 52 53 0
-53 69 19 0
26 -67 0
-14 62 0
-34 52 0
60 -45 0
-15 -60 0
39 36 44 0
-45 68 0
-35 22 0
67 42 -68 0
24 18 0
62 27 48 0
-59 35 -39 0
66 -63 0
42 45 0
-54 48 0
31 32 0
-44 -9 0
46 54 -52 0
78 20 76 0
33 -29 -48 0
-85 38 62 0
-84 -37 86 0
-92 43 0
47 -76 0
-74 -21 0
87 -27 -77 0
-25 -33 -76 0
63 -78 -53 0
-90 -22 0
-20 -79 0
-69 59 0
-8 56 0
-44 -84 0
81 -52 0
-80 -61 0
-75 -46 24 0
-62 72 49 54 0
77 63 0
22 -47 89 0
33 90 74 0
-76 50 0
-88 76 0
60 -87 0
-49 -88 0
57 -33 0
65 -19 0
-49 -86 0
-26 -81 59 0
63 64 70 0
66 -35 0
-41 85 35 0
26 -78 -75 0
-62 -59 84 0
55 -78 -37 0
9 -48 0
79 -93 0
-88 93 0
-38 0
-83 -29 0
82 -80 0
-72 41 0
88 82 -84 0
75 22 0
107 71 0
-99 -55 0
37 56 0
-84 -88 -106 0
102 1 0
58 95 0
74 -107 -110 0
29 -47 0
-104 79 0
30 7 0
78 -81 -97 0
95 97 0
99 78 -100 -73 0
100 47 0
-24 -105 -72 0
-95 105 0
-65 79 0
-109 104 0
30 -89 0
-98 73 0
-100 -85 0
-83 94 0
99 -103 0
-93 75 0
110 -35 0
83 98 0
105 110 0
-106 -90 0
95 76 -77 0
92 -106 0
-91 -67 0
-80 -102 0
-89 53 0
-114 117 0
-94 -96 0
-83 114 0
108 -118 0
111 19 -118 0
-72 -117 0
-103 116 -92 0
110 -107 0
-107 -116 0
-106 102 0
113 -120 0
-48 -117 0
-117 65 0
52 106 0
-113 102 0
116 70 0
-110 -63 0
-74 107 -102 0
103 96 0
61 -31 0
-70 120 0
111 112 0
34 67 0
40 -118 0
117 59 114 0
-114 -112 73 0
122 80 0
100 53 -126 0
129 128 0
124 123 0
-27 -120 0
126 118 0
91 -111 0
-120 -95 0
-120 103 111 0
-121 115 0
127 -82 -105 0
-118 113 0
119 3 0
100 123 0
-85 -110 0
125 119 0
118 95 -128 0
108 -123 0
70 -99 84 0
-91 -119 -126 0
-78 107 128 0
109 110 0
121 -108 0