%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : SYN431+1 : TPTP v8.1.0. Released v2.1.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n020.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Thu Jul 21 09:02:26 EDT 2022 % Result : CounterSatisfiable 146.59s 146.79s % Output : Saturation 146.65s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : SYN431+1 : TPTP v8.1.0. Released v2.1.0. % 0.04/0.13 % Command : metis --show proof --show saturation %s % 0.13/0.34 % Computer : n020.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Tue Jul 12 00:22:57 EDT 2022 % 0.13/0.34 % CPUTime : % 0.13/0.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 146.59/146.79 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 146.59/146.79 % 146.59/146.79 SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 146.59/146.79 |- ~c0_1 a132 \/ ~hskp0 % 146.59/146.79 |- ~c1_1 a132 \/ ~hskp0 % 146.59/146.79 |- ~c3_1 a132 \/ ~hskp0 % 146.59/146.79 |- ~c0_1 a133 \/ ~hskp1 % 146.59/146.79 |- ~c1_1 a133 \/ ~hskp1 % 146.59/146.79 |- ~hskp1 \/ c2_1 a133 % 146.59/146.79 |- ~c1_1 a146 \/ ~hskp10 % 146.59/146.79 |- ~c2_1 a146 \/ ~hskp10 % 146.59/146.79 |- ~hskp10 \/ c0_1 a146 % 146.59/146.79 |- ~c0_1 a151 \/ ~hskp11 % 146.59/146.79 |- ~c3_1 a151 \/ ~hskp11 % 146.59/146.79 |- ~hskp11 \/ c1_1 a151 % 146.59/146.79 |- ~c1_1 a154 \/ ~hskp12 % 146.59/146.79 |- ~c2_1 a154 \/ ~hskp12 % 146.59/146.79 |- ~c3_1 a154 \/ ~hskp12 % 146.59/146.79 |- ~c0_1 a156 \/ ~hskp13 % 146.59/146.79 |- ~c3_1 a156 \/ ~hskp13 % 146.59/146.79 |- ~hskp13 \/ c1_1 a156 % 146.59/146.79 |- ~c3_1 a159 \/ ~hskp14 % 146.59/146.79 |- ~hskp14 \/ c1_1 a159 % 146.59/146.79 |- ~hskp14 \/ c2_1 a159 % 146.59/146.79 |- ~c1_1 a160 \/ ~hskp15 % 146.59/146.79 |- ~c2_1 a160 \/ ~hskp15 % 146.59/146.79 |- ~c3_1 a160 \/ ~hskp15 % 146.59/146.79 |- ~c1_1 a161 \/ ~hskp16 % 146.59/146.79 |- ~hskp16 \/ c0_1 a161 % 146.59/146.79 |- ~hskp16 \/ c2_1 a161 % 146.59/146.79 |- ~c3_1 a134 \/ ~hskp17 % 146.59/146.79 |- ~hskp17 \/ c0_1 a134 % 146.59/146.79 |- ~hskp17 \/ c2_1 a134 % 146.59/146.79 |- ~c2_1 a138 \/ ~hskp18 % 146.59/146.79 |- ~hskp18 \/ c0_1 a138 % 146.59/146.79 |- ~hskp18 \/ c3_1 a138 % 146.59/146.79 |- ~hskp19 \/ c0_1 a143 % 146.59/146.79 |- ~hskp19 \/ c1_1 a143 % 146.59/146.79 |- ~hskp19 \/ c2_1 a143 % 146.59/146.79 |- ~c0_1 a135 \/ ~hskp2 % 146.59/146.79 |- ~c2_1 a135 \/ ~hskp2 % 146.59/146.79 |- ~hskp2 \/ c1_1 a135 % 146.59/146.79 |- ~c0_1 a144 \/ ~hskp20 % 146.59/146.79 |- ~hskp20 \/ c2_1 a144 % 146.59/146.79 |- ~hskp20 \/ c3_1 a144 % 146.59/146.79 |- ~c0_1 a147 \/ ~hskp21 % 146.59/146.79 |- ~hskp21 \/ c2_1 a147 % 146.59/146.79 |- ~hskp21 \/ c3_1 a147 % 146.59/146.79 |- ~c3_1 a148 \/ ~hskp22 % 146.59/146.79 |- ~hskp22 \/ c1_1 a148 % 146.59/146.79 |- ~hskp22 \/ c2_1 a148 % 146.59/146.79 |- ~c3_1 a149 \/ ~hskp23 % 146.59/146.79 |- ~hskp23 \/ c0_1 a149 % 146.59/146.79 |- ~hskp23 \/ c1_1 a149 % 146.59/146.79 |- ~c2_1 a150 \/ ~hskp24 % 146.59/146.79 |- ~hskp24 \/ c0_1 a150 % 146.59/146.79 |- ~hskp24 \/ c1_1 a150 % 146.59/146.79 |- ~c0_1 a152 \/ ~hskp25 % 146.59/146.79 |- ~hskp25 \/ c2_1 a152 % 146.59/146.79 |- ~hskp25 \/ c3_1 a152 % 146.59/146.79 |- ~c0_1 a153 \/ ~hskp26 % 146.59/146.79 |- ~c3_1 a153 \/ ~hskp26 % 146.59/146.79 |- ~hskp26 \/ c1_1 a153 % 146.59/146.79 |- ~c1_1 a157 \/ ~hskp27 % 146.59/146.79 |- ~hskp27 \/ c2_1 a157 % 146.59/146.79 |- ~hskp27 \/ c3_1 a157 % 146.59/146.79 |- ~c0_1 a158 \/ ~hskp28 % 146.59/146.79 |- ~hskp28 \/ c1_1 a158 % 146.59/146.79 |- ~hskp28 \/ c2_1 a158 % 146.59/146.79 |- ~c0_1 a136 \/ ~hskp3 % 146.59/146.79 |- ~c3_1 a136 \/ ~hskp3 % 146.59/146.79 |- ~hskp3 \/ c2_1 a136 % 146.59/146.79 |- ~c2_1 a137 \/ ~hskp4 % 146.59/146.79 |- ~hskp4 \/ c1_1 a137 % 146.59/146.79 |- ~hskp4 \/ c3_1 a137 % 146.59/146.79 |- ~c1_1 a139 \/ ~hskp5 % 146.59/146.79 |- ~hskp5 \/ c0_1 a139 % 146.59/146.79 |- ~hskp5 \/ c2_1 a139 % 146.59/146.79 |- ~c3_1 a140 \/ ~hskp6 % 146.59/146.79 |- ~hskp6 \/ c0_1 a140 % 146.59/146.79 |- ~hskp6 \/ c1_1 a140 % 146.59/146.79 |- ~c1_1 a141 \/ ~hskp7 % 146.59/146.79 |- ~hskp7 \/ c2_1 a141 % 146.59/146.79 |- ~hskp7 \/ c3_1 a141 % 146.59/146.79 |- ~c0_1 a142 \/ ~hskp8 % 146.59/146.79 |- ~hskp8 \/ c1_1 a142 % 146.59/146.79 |- ~hskp8 \/ c3_1 a142 % 146.59/146.79 |- ~c0_1 a145 \/ ~hskp9 % 146.59/146.79 |- ~c2_1 a145 \/ ~hskp9 % 146.59/146.79 |- ~c3_1 a145 \/ ~hskp9 % 146.59/146.79 |- ~c1_1 $X4 \/ ~c2_1 $X4 \/ ~c2_1 $X5 \/ ~c3_1 $X5 \/ ~ndr1_0 \/ % 146.59/146.79 c1_1 $X5 \/ c3_1 $X4 % 146.59/146.79 |- ~c1_1 $X3 \/ ~c2_1 $X3 \/ ~ndr1_0 \/ c3_1 $X3 \/ hskp10 \/ hskp9 % 146.59/146.79 |- hskp11 \/ hskp25 \/ hskp26 % 146.59/146.79 |- ~c0_1 $X8 \/ ~c1_1 $X9 \/ ~c2_1 $X8 \/ ~c3_1 $X9 \/ ~ndr1_0 \/ % 146.59/146.79 c2_1 $X9 \/ c3_1 $X8 \/ hskp12 % 146.59/146.79 |- hskp13 \/ hskp27 \/ hskp3 % 146.59/146.79 |- ~c1_1 $X10 \/ ~ndr1_0 \/ c0_1 $X10 \/ c3_1 $X10 \/ hskp14 \/ hskp28 % 146.59/146.79 |- ~c0_1 $V \/ ~c3_1 $V \/ ~ndr1_0 \/ c1_1 $V \/ hskp17 \/ hskp2 % 146.59/146.79 |- hskp18 \/ hskp5 \/ hskp6 % 146.59/146.79 |- ~c2_1 $X2 \/ ~ndr1_0 \/ c0_1 $X2 \/ c1_1 $X2 \/ hskp19 \/ hskp20 % 146.59/146.79 |- ~c1_1 $X7 \/ ~c2_1 $X6 \/ ~ndr1_0 \/ c0_1 $X7 \/ c1_1 $X6 \/ c2_1 $X7 \/ % 146.59/146.79 c3_1 $X6 \/ hskp21 % 146.59/146.79 |- hskp22 \/ hskp23 \/ hskp24 % 146.59/146.79 |- ~c0_1 $W \/ ~c2_1 $W \/ ~c3_1 $W \/ ~ndr1_0 \/ hskp3 \/ hskp4 % 146.59/146.79 |- ~c1_1 $X1 \/ ~c2_1 $X1 \/ ~ndr1_0 \/ c3_1 $X1 \/ hskp7 \/ hskp8 % 146.59/146.80 |- ~c0_1 $Y \/ ~c1_1 $X \/ ~c1_1 $Y \/ ~c1_1 $Z \/ ~c2_1 $Z \/ ~ndr1_0 \/ % 146.59/146.80 c0_1 $X \/ c0_1 $Z \/ c2_1 $X \/ c2_1 $Y % 146.59/146.80 |- ~c2_1 $X11 \/ ~c3_1 $X11 \/ ~ndr1_0 \/ c0_1 $X11 % 146.59/146.80 |- c1_1 a153 \/ hskp11 \/ hskp25 % 146.59/146.80 |- c2_1 a136 \/ hskp13 \/ hskp27 % 146.59/146.80 |- c1_1 a140 \/ hskp18 \/ hskp5 % 146.59/146.80 |- c0_1 a140 \/ hskp18 \/ hskp5 % 146.59/146.80 |- c1_1 a150 \/ hskp22 \/ hskp23 % 146.59/146.80 |- c0_1 a150 \/ hskp22 \/ hskp23 % 146.59/146.80 |- ~c1_1 a136 \/ ~ndr1_0 \/ c3_1 a136 \/ hskp10 \/ hskp13 \/ hskp27 \/ % 146.59/146.80 hskp9 % 146.59/146.80 |- hskp11 \/ hskp14 \/ hskp25 \/ hskp28 % 146.59/146.80 |- c2_1 a158 \/ hskp11 \/ hskp14 \/ hskp25 % 146.59/146.80 |- c1_1 a158 \/ hskp11 \/ hskp14 \/ hskp25 % 146.59/146.80 |- c0_1 a136 \/ c1_1 a136 \/ hskp13 \/ hskp19 \/ hskp20 \/ hskp27 % 146.59/146.80 |- ~c1_1 a136 \/ ~ndr1_0 \/ c3_1 a136 \/ hskp13 \/ hskp27 \/ hskp7 \/ hskp8 % 146.59/146.80 |- hskp11 \/ hskp14 \/ hskp25 \/ hskp7 \/ hskp8 % 146.59/146.80 |- c3_1 a142 \/ hskp11 \/ hskp14 \/ hskp25 \/ hskp7 % 146.59/146.80 |- c1_1 a142 \/ hskp11 \/ hskp14 \/ hskp25 \/ hskp7 % 146.59/146.80 |- ~c0_1 a142 \/ ~c2_1 a142 \/ ~ndr1_0 \/ hskp11 \/ hskp14 \/ hskp25 \/ % 146.59/146.80 hskp3 \/ hskp4 \/ hskp7 % 146.59/146.80 |- ~c2_1 a142 \/ ~ndr1_0 \/ c0_1 a142 \/ hskp11 \/ hskp14 \/ hskp25 \/ % 146.59/146.80 hskp7 % 146.59/146.80 |- hskp13 \/ hskp14 \/ hskp19 \/ hskp20 \/ hskp27 \/ hskp28 % 146.59/146.80 |- c2_1 a158 \/ hskp13 \/ hskp14 \/ hskp19 \/ hskp20 \/ hskp27 % 146.59/146.80 |- c1_1 a158 \/ hskp13 \/ hskp14 \/ hskp19 \/ hskp20 \/ hskp27 % 146.59/146.80 |- hskp10 \/ hskp13 \/ hskp19 \/ hskp20 \/ hskp27 \/ hskp9 % 146.59/146.80 |- hskp13 \/ hskp19 \/ hskp20 \/ hskp27 \/ hskp7 \/ hskp8 % 146.59/146.80 |- c3_1 a142 \/ hskp13 \/ hskp19 \/ hskp20 \/ hskp27 \/ hskp7 % 146.59/146.80 |- c1_1 a142 \/ hskp13 \/ hskp19 \/ hskp20 \/ hskp27 \/ hskp7 % 146.59/146.80 |- ~c2_1 a142 \/ ~ndr1_0 \/ c0_1 a142 \/ hskp13 \/ hskp19 \/ hskp20 \/ % 146.59/146.80 hskp27 \/ hskp7 % 146.59/146.80 |- hskp10 \/ hskp11 \/ hskp14 \/ hskp25 \/ hskp9 % 146.59/146.80 |- ~c0_1 $_10 \/ ~c1_1 a142 \/ ~c2_1 $_10 \/ ~ndr1_0 \/ c2_1 a142 \/ % 146.59/146.80 c3_1 $_10 \/ hskp12 \/ hskp13 \/ hskp19 \/ hskp20 \/ hskp27 \/ hskp7 % 146.59/146.80 |- ~c1_1 $_13 \/ ~ndr1_0 \/ c0_1 $_13 \/ c1_1 a136 \/ c2_1 $_13 \/ % 146.59/146.80 c3_1 a136 \/ hskp13 \/ hskp21 \/ hskp27 % 146.59/146.80 |- c0_1 a153 \/ c1_1 a136 \/ c2_1 a153 \/ hskp11 \/ hskp13 \/ hskp21 \/ % 146.59/146.80 hskp25 \/ hskp27 % 146.59/146.80 |- c0_1 a142 \/ c1_1 a136 \/ hskp13 \/ hskp19 \/ hskp20 \/ hskp21 \/ % 146.59/146.80 hskp27 \/ hskp7 % 146.59/146.80 |- hskp11 \/ hskp13 \/ hskp21 \/ hskp25 \/ hskp27 \/ hskp7 \/ hskp8 % 146.59/146.80 |- c3_1 a142 \/ hskp11 \/ hskp13 \/ hskp21 \/ hskp25 \/ hskp27 \/ hskp7 % 146.59/146.80 |- c1_1 a142 \/ hskp11 \/ hskp13 \/ hskp21 \/ hskp25 \/ hskp27 \/ hskp7 % 146.59/146.80 |- ~c0_1 $X8 \/ ~c1_1 a142 \/ ~c2_1 $X8 \/ ~ndr1_0 \/ c2_1 a142 \/ % 146.59/146.80 c3_1 $X8 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp21 \/ hskp25 \/ hskp27 \/ % 146.59/146.80 hskp7 % 146.59/146.80 |- ~c2_1 a142 \/ ~ndr1_0 \/ c0_1 a142 \/ hskp11 \/ hskp13 \/ hskp21 \/ % 146.59/146.80 hskp25 \/ hskp27 \/ hskp7 % 146.59/146.80 |- hskp10 \/ hskp11 \/ hskp13 \/ hskp21 \/ hskp25 \/ hskp27 \/ hskp9 % 146.59/146.80 |- c0_1 a142 \/ c1_1 a136 \/ hskp11 \/ hskp13 \/ hskp21 \/ hskp25 \/ % 146.59/146.80 hskp27 \/ hskp7 % 146.59/146.80 |- ~c0_1 a136 \/ ~ndr1_0 \/ c2_1 a142 \/ c3_1 a136 \/ hskp12 \/ hskp13 \/ % 146.59/146.80 hskp19 \/ hskp20 \/ hskp27 \/ hskp7 % 146.59/146.80 |- ~c0_1 a158 \/ ~ndr1_0 \/ c2_1 a142 \/ c3_1 a158 \/ hskp12 \/ hskp13 \/ % 146.59/146.80 hskp14 \/ hskp19 \/ hskp20 \/ hskp27 \/ hskp7 % 146.59/146.80 |- ~c0_1 $_21 \/ ~c1_1 $_20 \/ ~c1_1 $_21 \/ ~c1_1 a136 \/ ~ndr1_0 \/ % 146.59/146.80 c0_1 $_20 \/ c0_1 a136 \/ c2_1 $_20 \/ c2_1 $_21 \/ hskp13 \/ hskp27 % 146.59/146.80 |- ~c0_1 $_26 \/ ~c1_1 $_26 \/ ~c1_1 a136 \/ ~ndr1_0 \/ c0_1 a136 \/ % 146.59/146.80 c0_1 a142 \/ c2_1 $_26 \/ c2_1 a142 \/ hskp11 \/ hskp13 \/ hskp14 \/ % 146.59/146.80 hskp25 \/ hskp27 \/ hskp7 % 146.59/146.80 |- ~c0_1 $_26 \/ ~c1_1 $_26 \/ ~c1_1 a136 \/ ~ndr1_0 \/ c0_1 a136 \/ % 146.59/146.80 c0_1 a153 \/ c2_1 $_26 \/ c2_1 a153 \/ hskp11 \/ hskp13 \/ hskp25 \/ % 146.59/146.80 hskp27 % 146.59/146.80 |- ~c0_1 a140 \/ ~c1_1 $_25 \/ ~c1_1 a136 \/ ~ndr1_0 \/ c0_1 $_25 \/ % 146.59/146.80 c0_1 a136 \/ c2_1 $_25 \/ c2_1 a140 \/ hskp13 \/ hskp18 \/ hskp27 \/ % 146.59/146.80 hskp5 % 146.59/146.80 |- ~c0_1 a142 \/ ~c1_1 $_25 \/ ~c1_1 a136 \/ ~ndr1_0 \/ c0_1 $_25 \/ % 146.59/146.80 c0_1 a136 \/ c2_1 $_25 \/ c2_1 a142 \/ hskp11 \/ hskp13 \/ hskp21 \/ % 146.59/146.80 hskp25 \/ hskp27 \/ hskp7 % 146.59/146.80 |- ~c0_1 a142 \/ ~c1_1 $_25 \/ ~c1_1 a136 \/ ~ndr1_0 \/ c0_1 $_25 \/ % 146.59/146.80 c0_1 a136 \/ c2_1 $_25 \/ c2_1 a142 \/ hskp11 \/ hskp13 \/ hskp14 \/ % 146.59/146.80 hskp25 \/ hskp27 \/ hskp7 % 146.59/146.80 |- ~c0_1 a150 \/ ~c1_1 $_25 \/ ~c1_1 a136 \/ ~ndr1_0 \/ c0_1 $_25 \/ % 146.59/146.80 c0_1 a136 \/ c2_1 $_25 \/ c2_1 a150 \/ hskp13 \/ hskp22 \/ hskp23 \/ % 146.59/146.80 hskp27 % 146.59/146.80 |- ~c0_1 a153 \/ ~c1_1 $_25 \/ ~c1_1 a136 \/ ~ndr1_0 \/ c0_1 $_25 \/ % 146.59/146.80 c0_1 a136 \/ c2_1 $_25 \/ c2_1 a153 \/ hskp11 \/ hskp13 \/ hskp25 \/ % 146.59/146.80 hskp27 % 146.59/146.80 |- ~c0_1 $_26 \/ ~c1_1 $_25 \/ ~c1_1 $_26 \/ ~ndr1_0 \/ c0_1 $_25 \/ % 146.59/146.80 c0_1 a136 \/ c0_1 a142 \/ c2_1 $_25 \/ c2_1 $_26 \/ hskp11 \/ hskp13 \/ % 146.59/146.80 hskp21 \/ hskp25 \/ hskp27 \/ hskp7 % 146.59/146.80 |- ~c0_1 $_26 \/ ~c1_1 $_25 \/ ~c1_1 $_26 \/ ~ndr1_0 \/ c0_1 $_25 \/ % 146.59/146.80 c0_1 a136 \/ c2_1 $_25 \/ c2_1 $_26 \/ hskp13 \/ hskp19 \/ hskp20 \/ % 146.59/146.80 hskp27 % 146.59/146.80 |- ~c0_1 a140 \/ ~c1_1 a136 \/ ~ndr1_0 \/ c0_1 a136 \/ c0_1 a153 \/ % 146.59/146.80 c2_1 a140 \/ c2_1 a153 \/ hskp11 \/ hskp13 \/ hskp18 \/ hskp25 \/ % 146.59/146.80 hskp27 \/ hskp5 % 146.59/146.80 |- ~c0_1 a142 \/ ~c1_1 a136 \/ ~ndr1_0 \/ c0_1 a136 \/ c0_1 a153 \/ % 146.59/146.80 c2_1 a142 \/ c2_1 a153 \/ hskp11 \/ hskp13 \/ hskp21 \/ hskp25 \/ % 146.59/146.80 hskp27 \/ hskp7 % 146.59/146.80 |- ~c0_1 a142 \/ ~c1_1 a136 \/ ~ndr1_0 \/ c0_1 a136 \/ c0_1 a153 \/ % 146.59/146.80 c2_1 a142 \/ c2_1 a153 \/ hskp11 \/ hskp13 \/ hskp14 \/ hskp25 \/ % 146.59/146.80 hskp27 \/ hskp7 % 146.59/146.80 |- ~c0_1 a150 \/ ~c1_1 a136 \/ ~ndr1_0 \/ c0_1 a136 \/ c0_1 a153 \/ % 146.59/146.80 c2_1 a150 \/ c2_1 a153 \/ hskp11 \/ hskp13 \/ hskp22 \/ hskp23 \/ % 146.59/146.80 hskp25 \/ hskp27 % 146.59/146.80 |- ~c0_1 $_27 \/ ~c1_1 $_27 \/ ~ndr1_0 \/ c0_1 a136 \/ c0_1 a142 \/ % 146.59/146.80 c0_1 a153 \/ c2_1 $_27 \/ c2_1 a153 \/ hskp11 \/ hskp13 \/ hskp21 \/ % 146.59/146.80 hskp25 \/ hskp27 \/ hskp7 % 146.59/146.80 |- ~c0_1 $_27 \/ ~c1_1 $_27 \/ ~ndr1_0 \/ c0_1 a136 \/ c0_1 a153 \/ % 146.59/146.80 c2_1 $_27 \/ c2_1 a153 \/ hskp11 \/ hskp13 \/ hskp19 \/ hskp20 \/ % 146.59/146.80 hskp25 \/ hskp27 % 146.59/146.80 |- ~c0_1 a142 \/ ~ndr1_0 \/ c0_1 a136 \/ c0_1 a153 \/ c2_1 a142 \/ % 146.59/146.80 c2_1 a153 \/ hskp11 \/ hskp13 \/ hskp19 \/ hskp20 \/ hskp25 \/ hskp27 \/ % 146.59/146.80 hskp7 % 146.59/146.80 |- c0_1 a136 \/ c0_1 a153 \/ c2_1 a140 \/ c2_1 a153 \/ hskp11 \/ hskp13 \/ % 146.59/146.80 hskp18 \/ hskp19 \/ hskp20 \/ hskp25 \/ hskp27 \/ hskp5 % 146.59/146.80 |- ~c0_1 a140 \/ ~c1_1 a136 \/ ~ndr1_0 \/ c0_1 a136 \/ c0_1 a142 \/ % 146.59/146.80 c2_1 a140 \/ c2_1 a142 \/ hskp11 \/ hskp13 \/ hskp14 \/ hskp18 \/ % 146.59/146.80 hskp25 \/ hskp27 \/ hskp5 \/ hskp7 % 146.59/146.80 |- ~c0_1 a140 \/ ~c1_1 $_28 \/ ~ndr1_0 \/ c0_1 $_28 \/ c0_1 a136 \/ % 146.59/146.80 c2_1 $_28 \/ c2_1 a140 \/ hskp13 \/ hskp18 \/ hskp19 \/ hskp20 \/ % 146.59/146.80 hskp27 \/ hskp5 % 146.59/146.80 |- c0_1 a136 \/ c0_1 a142 \/ c2_1 a140 \/ hskp13 \/ hskp18 \/ hskp19 \/ % 146.59/146.80 hskp20 \/ hskp27 \/ hskp5 \/ hskp7 % 146.59/146.80 |- c0_1 a136 \/ c0_1 a142 \/ c2_1 a140 \/ hskp11 \/ hskp13 \/ hskp18 \/ % 146.59/146.80 hskp21 \/ hskp25 \/ hskp27 \/ hskp5 \/ hskp7 % 146.59/146.80 |- hskp12 \/ hskp13 \/ hskp17 \/ hskp18 \/ hskp19 \/ hskp2 % 146.59/146.80 |- c1_1 a135 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp18 \/ hskp19 % 146.59/146.80 |- c0_1 a135 \/ c3_1 a135 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp17 \/ % 146.59/146.80 hskp18 \/ hskp19 \/ hskp28 % 146.59/146.80 |- ~c0_1 $X8 \/ ~c1_1 a135 \/ ~c2_1 $X8 \/ ~ndr1_0 \/ c0_1 a135 \/ % 146.59/146.80 c2_1 a135 \/ c3_1 $X8 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp17 \/ % 146.59/146.80 hskp18 \/ hskp19 \/ hskp28 % 146.59/146.80 |- ~c2_1 a135 \/ ~ndr1_0 \/ c0_1 a135 \/ hskp12 \/ hskp13 \/ hskp14 \/ % 146.59/146.80 hskp17 \/ hskp18 \/ hskp19 \/ hskp28 % 146.59/146.80 |- hskp13 \/ hskp17 \/ hskp19 \/ hskp2 \/ hskp20 \/ hskp22 \/ hskp23 % 146.59/146.80 |- c1_1 a149 \/ hskp13 \/ hskp17 \/ hskp19 \/ hskp2 \/ hskp20 \/ hskp22 % 146.59/146.80 |- c0_1 a149 \/ hskp13 \/ hskp17 \/ hskp19 \/ hskp2 \/ hskp20 \/ hskp22 % 146.59/146.80 |- hskp11 \/ hskp13 \/ hskp17 \/ hskp2 \/ hskp21 \/ hskp22 \/ hskp23 % 146.59/146.80 |- c1_1 a149 \/ hskp11 \/ hskp13 \/ hskp17 \/ hskp2 \/ hskp21 \/ hskp22 % 146.59/146.80 |- c0_1 a149 \/ hskp11 \/ hskp13 \/ hskp17 \/ hskp2 \/ hskp21 \/ hskp22 % 146.59/146.80 |- ~c0_1 a149 \/ ~c1_1 a136 \/ ~ndr1_0 \/ c0_1 a136 \/ c0_1 a153 \/ % 146.59/146.80 c2_1 a149 \/ c2_1 a153 \/ hskp11 \/ hskp13 \/ hskp17 \/ hskp2 \/ % 146.59/146.80 hskp21 \/ hskp22 \/ hskp25 \/ hskp27 % 146.59/146.80 |- ~c0_1 a149 \/ ~c1_1 $_20 \/ ~c1_1 a136 \/ ~ndr1_0 \/ c0_1 $_20 \/ % 146.59/146.80 c0_1 a136 \/ c2_1 $_20 \/ c2_1 a149 \/ hskp11 \/ hskp13 \/ hskp17 \/ % 146.59/146.80 hskp2 \/ hskp21 \/ hskp22 \/ hskp27 % 146.59/146.80 |- ~c0_1 a153 \/ ~c1_1 a136 \/ ~ndr1_0 \/ c0_1 a136 \/ c0_1 a142 \/ % 146.59/146.80 c2_1 a142 \/ c2_1 a153 \/ hskp11 \/ hskp13 \/ hskp14 \/ hskp25 \/ % 146.59/146.80 hskp27 \/ hskp7 % 146.59/146.80 |- ~c0_1 a153 \/ ~c1_1 $_30 \/ ~ndr1_0 \/ c0_1 $_30 \/ c0_1 a136 \/ % 146.59/146.80 c0_1 a142 \/ c2_1 $_30 \/ c2_1 a153 \/ hskp11 \/ hskp13 \/ hskp21 \/ % 146.59/146.80 hskp25 \/ hskp27 \/ hskp7 % 146.59/146.80 |- ~c0_1 a153 \/ ~c1_1 $_30 \/ ~ndr1_0 \/ c0_1 $_30 \/ c0_1 a136 \/ % 146.59/146.80 c2_1 $_30 \/ c2_1 a153 \/ hskp11 \/ hskp13 \/ hskp19 \/ hskp20 \/ % 146.59/146.80 hskp25 \/ hskp27 % 146.59/146.80 |- ~c0_1 a153 \/ ~ndr1_0 \/ c0_1 a136 \/ c0_1 a142 \/ c2_1 a142 \/ % 146.59/146.80 c2_1 a153 \/ hskp11 \/ hskp13 \/ hskp21 \/ hskp25 \/ hskp27 \/ hskp7 % 146.59/146.80 |- ~c0_1 a153 \/ ~ndr1_0 \/ c0_1 a136 \/ c0_1 a142 \/ c2_1 a142 \/ % 146.59/146.80 c2_1 a153 \/ hskp11 \/ hskp13 \/ hskp19 \/ hskp20 \/ hskp25 \/ hskp27 \/ % 146.59/146.80 hskp7 % 146.59/146.80 |- ~c0_1 $_33 \/ ~c1_1 $_32 \/ ~c1_1 $_33 \/ ~ndr1_0 \/ c0_1 $_32 \/ % 146.59/146.80 c0_1 a158 \/ c2_1 $_32 \/ c2_1 $_33 \/ hskp11 \/ hskp14 \/ hskp25 % 146.59/146.80 |- ~c0_1 $_35 \/ ~c1_1 $_35 \/ ~ndr1_0 \/ c0_1 a142 \/ c0_1 a158 \/ % 146.59/146.80 c2_1 $_35 \/ c2_1 a142 \/ hskp11 \/ hskp14 \/ hskp25 \/ hskp7 % 146.59/146.80 |- ~c0_1 $_35 \/ ~c1_1 $_35 \/ ~ndr1_0 \/ c0_1 a153 \/ c0_1 a158 \/ % 146.59/146.80 c2_1 $_35 \/ c2_1 a153 \/ hskp11 \/ hskp14 \/ hskp25 % 146.65/146.80 |- ~c0_1 a140 \/ ~c1_1 $_34 \/ ~ndr1_0 \/ c0_1 $_34 \/ c0_1 a158 \/ % 146.65/146.80 c2_1 $_34 \/ c2_1 a140 \/ hskp11 \/ hskp14 \/ hskp18 \/ hskp25 \/ hskp5 % 146.65/146.80 |- ~c0_1 a142 \/ ~c1_1 $_34 \/ ~ndr1_0 \/ c0_1 $_34 \/ c0_1 a158 \/ % 146.65/146.80 c2_1 $_34 \/ c2_1 a142 \/ hskp11 \/ hskp14 \/ hskp25 \/ hskp7 % 146.65/146.80 |- ~c0_1 a153 \/ ~c1_1 $_34 \/ ~ndr1_0 \/ c0_1 $_34 \/ c0_1 a158 \/ % 146.65/146.80 c2_1 $_34 \/ c2_1 a153 \/ hskp11 \/ hskp14 \/ hskp25 % 146.65/146.80 |- ~c0_1 a142 \/ ~ndr1_0 \/ c0_1 a153 \/ c0_1 a158 \/ c2_1 a142 \/ % 146.65/146.80 c2_1 a153 \/ hskp11 \/ hskp14 \/ hskp25 \/ hskp7 % 146.65/146.80 |- c0_1 a153 \/ c0_1 a158 \/ c2_1 a140 \/ c2_1 a153 \/ hskp11 \/ hskp14 \/ % 146.65/146.80 hskp18 \/ hskp25 \/ hskp5 % 146.65/146.80 |- ~c0_1 a153 \/ ~ndr1_0 \/ c0_1 a142 \/ c0_1 a158 \/ c2_1 a142 \/ % 146.65/146.80 c2_1 a153 \/ hskp11 \/ hskp14 \/ hskp25 \/ hskp7 % 146.65/146.80 |- c0_1 a142 \/ c0_1 a158 \/ c2_1 a140 \/ hskp11 \/ hskp14 \/ hskp18 \/ % 146.65/146.80 hskp25 \/ hskp5 \/ hskp7 % 146.65/146.80 |- ~c0_1 $_42 \/ ~c1_1 $_42 \/ ~ndr1_0 \/ c0_1 a136 \/ c0_1 a142 \/ % 146.65/146.80 c2_1 $_42 \/ c2_1 a142 \/ hskp13 \/ hskp19 \/ hskp20 \/ hskp27 \/ hskp7 % 146.65/146.80 |- c0_1 a136 \/ c0_1 a142 \/ c2_1 a142 \/ c2_1 a149 \/ hskp13 \/ hskp17 \/ % 146.65/146.80 hskp19 \/ hskp2 \/ hskp20 \/ hskp22 \/ hskp27 \/ hskp7 % 146.65/146.80 |- hskp12 \/ hskp13 \/ hskp17 \/ hskp19 \/ hskp2 \/ hskp20 \/ hskp22 % 146.65/146.80 |- c2_1 a148 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp19 \/ hskp2 \/ hskp20 % 146.65/146.80 |- c1_1 a148 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp19 \/ hskp2 \/ hskp20 % 146.65/146.80 |- hskp12 \/ hskp13 \/ hskp17 \/ hskp19 \/ hskp2 \/ hskp20 \/ hskp7 \/ % 146.65/146.80 hskp8 % 146.65/146.80 |- c3_1 a142 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp19 \/ hskp2 \/ hskp20 \/ % 146.65/146.80 hskp7 % 146.65/146.80 |- c1_1 a142 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp19 \/ hskp2 \/ hskp20 \/ % 146.65/146.80 hskp7 % 146.65/146.80 |- ~c0_1 $X8 \/ ~c1_1 a142 \/ ~c2_1 $X8 \/ ~ndr1_0 \/ c2_1 a142 \/ % 146.65/146.80 c3_1 $X8 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp19 \/ hskp2 \/ hskp20 \/ % 146.65/146.80 hskp7 % 146.65/146.80 |- ~c0_1 a142 \/ ~c2_1 a142 \/ ~ndr1_0 \/ hskp12 \/ hskp13 \/ hskp17 \/ % 146.65/146.80 hskp19 \/ hskp2 \/ hskp20 \/ hskp3 \/ hskp4 \/ hskp7 % 146.65/146.80 |- ~c2_1 a142 \/ ~ndr1_0 \/ c0_1 a142 \/ hskp12 \/ hskp13 \/ hskp17 \/ % 146.65/146.80 hskp19 \/ hskp2 \/ hskp20 \/ hskp7 % 146.65/146.80 |- hskp10 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp19 \/ hskp2 \/ hskp20 \/ % 146.65/146.80 hskp9 % 146.65/146.80 |- ~c0_1 a142 \/ ~c1_1 $_44 \/ ~ndr1_0 \/ c0_1 $_44 \/ c0_1 a136 \/ % 146.65/146.80 c2_1 $_44 \/ c2_1 a142 \/ hskp13 \/ hskp19 \/ hskp20 \/ hskp27 \/ hskp7 % 146.65/146.80 |- hskp11 \/ hskp14 \/ hskp22 \/ hskp23 % 146.65/146.80 |- c1_1 a149 \/ hskp11 \/ hskp14 \/ hskp22 % 146.65/146.80 |- c0_1 a149 \/ hskp11 \/ hskp14 \/ hskp22 % 146.65/146.80 |- ~c0_1 a149 \/ ~c1_1 $_32 \/ ~ndr1_0 \/ c0_1 $_32 \/ c0_1 a158 \/ % 146.65/146.80 c2_1 $_32 \/ c2_1 a149 \/ hskp11 \/ hskp14 \/ hskp22 \/ hskp25 % 146.65/146.80 |- ~c0_1 a149 \/ ~c1_1 a136 \/ ~ndr1_0 \/ c0_1 a136 \/ c0_1 a153 \/ % 146.65/146.80 c2_1 a149 \/ c2_1 a153 \/ hskp11 \/ hskp13 \/ hskp14 \/ hskp22 \/ % 146.65/146.80 hskp25 \/ hskp27 % 146.65/146.80 |- ~c0_1 a149 \/ ~c1_1 $_20 \/ ~c1_1 a136 \/ ~ndr1_0 \/ c0_1 $_20 \/ % 146.65/146.80 c0_1 a136 \/ c2_1 $_20 \/ c2_1 a149 \/ hskp11 \/ hskp13 \/ hskp14 \/ % 146.65/146.80 hskp22 \/ hskp27 % 146.65/146.80 |- c0_1 a153 \/ c0_1 a158 \/ c2_1 a149 \/ c2_1 a153 \/ hskp11 \/ hskp14 \/ % 146.65/146.80 hskp22 \/ hskp25 % 146.65/146.80 |- c0_1 a142 \/ c0_1 a158 \/ c2_1 a142 \/ c2_1 a149 \/ hskp11 \/ hskp14 \/ % 146.65/146.80 hskp22 \/ hskp25 \/ hskp7 % 146.65/146.80 |- ~c0_1 $_47 \/ ~c1_1 $_47 \/ ~ndr1_0 \/ c0_1 a136 \/ c0_1 a142 \/ % 146.65/146.80 c2_1 $_47 \/ c2_1 a142 \/ hskp11 \/ hskp13 \/ hskp21 \/ hskp25 \/ % 146.65/146.80 hskp27 \/ hskp7 % 146.65/146.80 |- c0_1 a136 \/ c0_1 a142 \/ c2_1 a142 \/ c2_1 a149 \/ hskp11 \/ hskp13 \/ % 146.65/146.80 hskp14 \/ hskp21 \/ hskp22 \/ hskp25 \/ hskp27 \/ hskp7 % 146.65/146.80 |- c0_1 a136 \/ c0_1 a142 \/ c2_1 a142 \/ c2_1 a149 \/ hskp11 \/ hskp13 \/ % 146.65/146.80 hskp17 \/ hskp2 \/ hskp21 \/ hskp22 \/ hskp25 \/ hskp27 \/ hskp7 % 146.65/146.80 |- ~c0_1 a149 \/ ~c1_1 a136 \/ ~ndr1_0 \/ c0_1 a136 \/ c0_1 a142 \/ % 146.65/146.80 c2_1 a142 \/ c2_1 a149 \/ hskp11 \/ hskp13 \/ hskp14 \/ hskp22 \/ % 146.65/146.80 hskp25 \/ hskp27 \/ hskp7 % 146.65/146.80 |- c0_1 a136 \/ c0_1 a153 \/ c2_1 a149 \/ c2_1 a153 \/ hskp11 \/ hskp13 \/ % 146.65/146.80 hskp14 \/ hskp19 \/ hskp20 \/ hskp22 \/ hskp25 \/ hskp27 % 146.65/146.80 |- c0_1 a136 \/ c0_1 a153 \/ c2_1 a149 \/ c2_1 a153 \/ hskp11 \/ hskp13 \/ % 146.65/146.80 hskp17 \/ hskp19 \/ hskp2 \/ hskp20 \/ hskp22 \/ hskp25 \/ hskp27 % 146.65/146.80 |- ~c0_1 a136 \/ ~ndr1_0 \/ c2_1 a142 \/ c3_1 a136 \/ hskp11 \/ hskp12 \/ % 146.65/146.80 hskp13 \/ hskp21 \/ hskp25 \/ hskp27 \/ hskp7 % 146.65/146.80 |- hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp18 \/ hskp2 % 146.65/146.80 |- c1_1 a135 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp18 % 146.65/146.80 |- hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp2 \/ hskp21 \/ hskp22 % 146.65/146.80 |- c2_1 a148 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp2 \/ hskp21 % 146.65/146.80 |- c1_1 a148 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp2 \/ hskp21 % 146.65/146.80 |- hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp2 \/ hskp21 \/ hskp7 \/ % 146.65/146.80 hskp8 % 146.65/146.80 |- c3_1 a142 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp2 \/ hskp21 \/ % 146.65/146.80 hskp7 % 146.65/146.80 |- c1_1 a142 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp2 \/ hskp21 \/ % 146.65/146.80 hskp7 % 146.65/146.80 |- ~c0_1 a142 \/ ~c1_1 $_20 \/ ~c1_1 a136 \/ c0_1 $_20 \/ c0_1 a136 \/ % 146.65/146.80 c2_1 $_20 \/ c2_1 a142 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ % 146.65/146.80 hskp2 \/ hskp21 \/ hskp27 \/ hskp7 % 146.65/146.80 |- ~c0_1 $X8 \/ ~c1_1 a142 \/ ~c2_1 $X8 \/ ~ndr1_0 \/ c2_1 a142 \/ % 146.65/146.80 c3_1 $X8 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp2 \/ hskp21 \/ % 146.65/146.80 hskp7 % 146.65/146.80 |- ~c0_1 a142 \/ ~c2_1 a142 \/ ~ndr1_0 \/ hskp11 \/ hskp12 \/ hskp13 \/ % 146.65/146.80 hskp17 \/ hskp2 \/ hskp21 \/ hskp3 \/ hskp4 \/ hskp7 % 146.65/146.80 |- ~c2_1 a142 \/ ~ndr1_0 \/ c0_1 a142 \/ hskp11 \/ hskp12 \/ hskp13 \/ % 146.65/146.80 hskp17 \/ hskp2 \/ hskp21 \/ hskp7 % 146.65/146.80 |- hskp10 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp2 \/ hskp21 \/ % 146.65/146.80 hskp9 % 146.65/146.80 |- c0_1 a142 \/ c1_1 a136 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ % 146.65/146.80 hskp2 \/ hskp21 \/ hskp27 \/ hskp7 % 146.65/146.80 |- ~c0_1 a153 \/ ~c1_1 $_25 \/ c0_1 $_25 \/ c0_1 a136 \/ c0_1 a142 \/ % 146.65/146.80 c2_1 $_25 \/ c2_1 a153 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ % 146.65/146.80 hskp2 \/ hskp21 \/ hskp25 \/ hskp27 \/ hskp7 % 146.65/146.80 |- ~c0_1 $_26 \/ ~c1_1 $_26 \/ c0_1 a136 \/ c0_1 a142 \/ c0_1 a153 \/ % 146.65/146.80 c2_1 $_26 \/ c2_1 a153 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ % 146.65/146.80 hskp2 \/ hskp21 \/ hskp25 \/ hskp27 \/ hskp7 % 146.65/146.80 |- ~c0_1 $_21 \/ ~c1_1 $_20 \/ ~c1_1 $_21 \/ c0_1 $_20 \/ c0_1 a136 \/ % 146.65/146.80 c0_1 a142 \/ c2_1 $_20 \/ c2_1 $_21 \/ hskp11 \/ hskp12 \/ hskp13 \/ % 146.65/146.80 hskp17 \/ hskp2 \/ hskp21 \/ hskp27 \/ hskp7 % 146.65/146.80 |- ~c0_1 $_63 \/ ~c1_1 $_62 \/ ~c1_1 $_63 \/ ~ndr1_0 \/ c0_1 $_62 \/ % 146.65/146.80 c0_1 a158 \/ c2_1 $_62 \/ c2_1 $_63 \/ hskp13 \/ hskp14 \/ hskp19 \/ % 146.65/146.80 hskp20 \/ hskp27 % 146.65/146.80 |- ~c0_1 $_65 \/ ~c1_1 $_65 \/ ~ndr1_0 \/ c0_1 a142 \/ c0_1 a158 \/ % 146.65/146.80 c2_1 $_65 \/ c2_1 a142 \/ hskp13 \/ hskp14 \/ hskp19 \/ hskp20 \/ % 146.65/146.80 hskp27 \/ hskp7 % 146.65/146.80 |- ~c0_1 a140 \/ ~c1_1 $_64 \/ ~ndr1_0 \/ c0_1 $_64 \/ c0_1 a158 \/ % 146.65/146.80 c2_1 $_64 \/ c2_1 a140 \/ hskp13 \/ hskp14 \/ hskp18 \/ hskp19 \/ % 146.65/146.80 hskp20 \/ hskp27 \/ hskp5 % 146.65/146.81 |- ~c0_1 a142 \/ ~c1_1 $_64 \/ ~ndr1_0 \/ c0_1 $_64 \/ c0_1 a158 \/ % 146.65/146.81 c2_1 $_64 \/ c2_1 a142 \/ hskp13 \/ hskp14 \/ hskp19 \/ hskp20 \/ % 146.65/146.81 hskp27 \/ hskp7 % 146.65/146.81 |- ~c0_1 a149 \/ ~c1_1 $_64 \/ ~ndr1_0 \/ c0_1 $_64 \/ c0_1 a158 \/ % 146.65/146.81 c2_1 $_64 \/ c2_1 a149 \/ hskp11 \/ hskp13 \/ hskp14 \/ hskp19 \/ % 146.65/146.81 hskp20 \/ hskp22 \/ hskp27 % 146.65/146.81 |- ~c0_1 a149 \/ ~c1_1 $_64 \/ ~ndr1_0 \/ c0_1 $_64 \/ c0_1 a158 \/ % 146.65/146.81 c2_1 $_64 \/ c2_1 a149 \/ hskp13 \/ hskp14 \/ hskp17 \/ hskp19 \/ % 146.65/146.81 hskp2 \/ hskp20 \/ hskp22 \/ hskp27 % 146.65/146.81 |- c0_1 a142 \/ c0_1 a158 \/ c2_1 a140 \/ hskp13 \/ hskp14 \/ hskp18 \/ % 146.65/146.81 hskp19 \/ hskp20 \/ hskp27 \/ hskp5 \/ hskp7 % 146.65/146.81 |- c0_1 a142 \/ c0_1 a158 \/ c2_1 a142 \/ c2_1 a149 \/ hskp11 \/ hskp13 \/ % 146.65/146.81 hskp14 \/ hskp19 \/ hskp20 \/ hskp22 \/ hskp27 \/ hskp7 % 146.65/146.81 |- c0_1 a142 \/ c0_1 a158 \/ c2_1 a142 \/ c2_1 a149 \/ hskp13 \/ hskp14 \/ % 146.65/146.81 hskp17 \/ hskp19 \/ hskp2 \/ hskp20 \/ hskp22 \/ hskp27 \/ hskp7 % 146.65/146.81 |- hskp13 \/ hskp19 \/ hskp20 \/ hskp22 \/ hskp23 \/ hskp27 % 146.65/146.81 |- c3_1 a157 \/ hskp13 \/ hskp19 \/ hskp20 \/ hskp22 \/ hskp23 % 146.65/146.81 |- c2_1 a157 \/ hskp13 \/ hskp19 \/ hskp20 \/ hskp22 \/ hskp23 % 146.65/146.81 |- c0_1 a157 \/ hskp13 \/ hskp19 \/ hskp20 \/ hskp22 \/ hskp23 % 146.65/146.81 |- hskp13 \/ hskp19 \/ hskp20 \/ hskp22 \/ hskp23 \/ hskp3 \/ hskp4 % 146.65/146.81 |- c3_1 a137 \/ hskp13 \/ hskp19 \/ hskp20 \/ hskp22 \/ hskp23 \/ hskp3 % 146.65/146.81 |- c1_1 a137 \/ hskp13 \/ hskp19 \/ hskp20 \/ hskp22 \/ hskp23 \/ hskp3 % 146.65/146.81 |- ~c0_1 $X8 \/ ~c1_1 a137 \/ ~c2_1 $X8 \/ ~ndr1_0 \/ c2_1 a137 \/ % 146.65/146.81 c3_1 $X8 \/ hskp12 \/ hskp13 \/ hskp19 \/ hskp20 \/ hskp22 \/ hskp23 \/ % 146.65/146.81 hskp3 % 146.65/146.81 |- ~c2_1 a137 \/ ~ndr1_0 \/ c0_1 a137 \/ hskp13 \/ hskp19 \/ hskp20 \/ % 146.65/146.81 hskp22 \/ hskp23 \/ hskp3 % 146.65/146.81 |- c0_1 a136 \/ c0_1 a142 \/ c2_1 a142 \/ c2_1 a149 \/ hskp11 \/ hskp13 \/ % 146.65/146.81 hskp14 \/ hskp19 \/ hskp20 \/ hskp22 \/ hskp27 \/ hskp7 % 146.65/146.81 |- ~c0_1 a149 \/ ~c1_1 $_77 \/ ~ndr1_0 \/ c0_1 $_77 \/ c0_1 a136 \/ % 146.65/146.81 c2_1 $_77 \/ c2_1 a149 \/ hskp11 \/ hskp13 \/ hskp14 \/ hskp19 \/ % 146.65/146.81 hskp20 \/ hskp22 \/ hskp27 % 146.65/146.81 |- ~c0_1 a149 \/ ~c1_1 $_77 \/ ~ndr1_0 \/ c0_1 $_77 \/ c0_1 a136 \/ % 146.65/146.81 c2_1 $_77 \/ c2_1 a149 \/ hskp13 \/ hskp17 \/ hskp19 \/ hskp2 \/ % 146.65/146.81 hskp20 \/ hskp22 \/ hskp27 % 146.65/146.81 |- c0_1 a136 \/ c0_1 a142 \/ c0_1 a153 \/ c2_1 a149 \/ c2_1 a153 \/ % 146.65/146.81 hskp11 \/ hskp13 \/ hskp14 \/ hskp21 \/ hskp22 \/ hskp25 \/ hskp27 \/ % 146.65/146.81 hskp7 % 146.65/146.81 |- c0_1 a136 \/ c0_1 a142 \/ c0_1 a153 \/ c2_1 a149 \/ c2_1 a153 \/ % 146.65/146.81 hskp11 \/ hskp13 \/ hskp17 \/ hskp2 \/ hskp21 \/ hskp22 \/ hskp25 \/ % 146.65/146.81 hskp27 \/ hskp7 % 146.65/146.81 |- hskp11 \/ hskp13 \/ hskp21 \/ hskp22 \/ hskp23 \/ hskp25 \/ hskp27 % 146.65/146.81 |- c3_1 a157 \/ hskp11 \/ hskp13 \/ hskp21 \/ hskp22 \/ hskp23 \/ hskp25 % 146.65/146.81 |- c2_1 a157 \/ hskp11 \/ hskp13 \/ hskp21 \/ hskp22 \/ hskp23 \/ hskp25 % 146.65/146.81 |- c0_1 a157 \/ hskp11 \/ hskp13 \/ hskp21 \/ hskp22 \/ hskp23 \/ hskp25 % 146.65/146.81 |- hskp11 \/ hskp13 \/ hskp21 \/ hskp22 \/ hskp23 \/ hskp25 \/ hskp3 \/ % 146.65/146.81 hskp4 % 146.65/146.81 |- c3_1 a137 \/ hskp11 \/ hskp13 \/ hskp21 \/ hskp22 \/ hskp23 \/ hskp25 \/ % 146.65/146.81 hskp3 % 146.65/146.81 |- c1_1 a137 \/ hskp11 \/ hskp13 \/ hskp21 \/ hskp22 \/ hskp23 \/ hskp25 \/ % 146.65/146.81 hskp3 % 146.65/146.81 |- ~c0_1 $X8 \/ ~c1_1 a137 \/ ~c2_1 $X8 \/ ~ndr1_0 \/ c2_1 a137 \/ % 146.65/146.81 c3_1 $X8 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp21 \/ hskp22 \/ hskp23 \/ % 146.65/146.81 hskp25 \/ hskp3 % 146.65/146.81 |- ~c2_1 a137 \/ ~ndr1_0 \/ c0_1 a137 \/ hskp11 \/ hskp13 \/ hskp21 \/ % 146.65/146.81 hskp22 \/ hskp23 \/ hskp25 \/ hskp3 % 146.65/146.81 |- ~c0_1 $_93 \/ ~c1_1 $_92 \/ ~c1_1 $_93 \/ ~ndr1_0 \/ c0_1 $_92 \/ % 146.65/146.81 c0_1 a153 \/ c1_1 a136 \/ c2_1 $_92 \/ c2_1 $_93 \/ hskp11 \/ hskp13 \/ % 146.65/146.81 hskp21 \/ hskp25 \/ hskp27 % 146.65/146.81 |- ~c0_1 a140 \/ ~c1_1 $_94 \/ ~ndr1_0 \/ c0_1 $_94 \/ c0_1 a153 \/ % 146.65/146.81 c1_1 a136 \/ c2_1 $_94 \/ c2_1 a140 \/ hskp11 \/ hskp13 \/ hskp18 \/ % 146.65/146.81 hskp21 \/ hskp25 \/ hskp27 \/ hskp5 % 146.65/146.81 |- ~c0_1 a142 \/ ~c1_1 $_94 \/ ~ndr1_0 \/ c0_1 $_94 \/ c0_1 a153 \/ % 146.65/146.81 c1_1 a136 \/ c2_1 $_94 \/ c2_1 a142 \/ hskp11 \/ hskp13 \/ hskp21 \/ % 146.65/146.81 hskp25 \/ hskp27 \/ hskp7 % 146.65/146.81 |- ~c0_1 a149 \/ ~c1_1 $_94 \/ ~ndr1_0 \/ c0_1 $_94 \/ c0_1 a153 \/ % 146.65/146.81 c1_1 a136 \/ c2_1 $_94 \/ c2_1 a149 \/ hskp11 \/ hskp13 \/ hskp14 \/ % 146.65/146.81 hskp21 \/ hskp22 \/ hskp25 \/ hskp27 % 146.65/146.81 |- ~c0_1 a149 \/ ~c1_1 $_94 \/ ~ndr1_0 \/ c0_1 $_94 \/ c0_1 a153 \/ % 146.65/146.81 c1_1 a136 \/ c2_1 $_94 \/ c2_1 a149 \/ hskp11 \/ hskp13 \/ hskp17 \/ % 146.65/146.81 hskp2 \/ hskp21 \/ hskp22 \/ hskp25 \/ hskp27 % 146.65/146.81 |- ~c1_1 $_102 \/ ~c2_1 $_102 \/ ~ndr1_0 \/ c1_1 a157 \/ c3_1 $_102 \/ % 146.65/146.81 hskp13 \/ hskp19 \/ hskp20 \/ hskp22 \/ hskp23 % 146.65/146.81 |- ~c1_1 $_107 \/ ~c2_1 $_107 \/ ~ndr1_0 \/ c1_1 a157 \/ c3_1 $_107 \/ % 146.65/146.81 hskp11 \/ hskp13 \/ hskp21 \/ hskp22 \/ hskp23 \/ hskp25 % 146.65/146.81 |- c0_1 a142 \/ c1_1 a136 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp14 \/ % 146.65/146.81 hskp21 \/ hskp27 \/ hskp7 % 146.65/146.81 |- ~c0_1 $_21 \/ ~c1_1 $_20 \/ ~c1_1 $_21 \/ c0_1 $_20 \/ c0_1 a136 \/ % 146.65/146.81 c0_1 a142 \/ c2_1 $_20 \/ c2_1 $_21 \/ hskp11 \/ hskp12 \/ hskp13 \/ % 146.65/146.81 hskp14 \/ hskp21 \/ hskp27 \/ hskp7 % 146.65/146.81 |- hskp11 \/ hskp12 \/ hskp14 \/ hskp18 % 146.65/146.81 |- c3_1 a138 \/ hskp11 \/ hskp12 \/ hskp14 % 146.65/146.81 |- c0_1 a138 \/ hskp11 \/ hskp12 \/ hskp14 % 146.65/146.81 |- ~c0_1 $X8 \/ ~c1_1 a138 \/ ~c2_1 $X8 \/ ~ndr1_0 \/ c2_1 a138 \/ % 146.65/146.81 c3_1 $X8 \/ hskp11 \/ hskp12 \/ hskp14 % 146.65/146.81 |- ~c1_1 $X4 \/ ~c2_1 $X4 \/ ~c2_1 a138 \/ ~ndr1_0 \/ c1_1 a138 \/ % 146.65/146.81 c3_1 $X4 \/ hskp11 \/ hskp12 \/ hskp14 % 146.65/146.81 |- ~c0_1 a138 \/ ~c2_1 a138 \/ ~ndr1_0 \/ hskp11 \/ hskp12 \/ hskp14 \/ % 146.65/146.81 hskp3 \/ hskp4 % 146.65/146.81 |- ~c0_1 a136 \/ ~c1_1 a138 \/ ~ndr1_0 \/ c2_1 a138 \/ c3_1 a136 \/ % 146.65/146.81 hskp11 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp27 % 146.65/146.81 |- ~c1_1 a153 \/ ~c2_1 a138 \/ ~ndr1_0 \/ c0_1 a153 \/ c1_1 a136 \/ % 146.65/146.81 c1_1 a138 \/ c3_1 a153 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp14 \/ % 146.65/146.81 hskp21 \/ hskp25 \/ hskp27 % 146.65/146.81 |- hskp11 \/ hskp12 \/ hskp14 \/ hskp17 \/ hskp2 % 146.65/146.81 |- c1_1 a135 \/ hskp11 \/ hskp12 \/ hskp14 \/ hskp17 % 146.65/146.81 |- ~c0_1 a135 \/ ~c1_1 $_92 \/ c0_1 $_92 \/ c0_1 a153 \/ c1_1 a136 \/ % 146.65/146.81 c2_1 $_92 \/ c2_1 a135 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp14 \/ % 146.65/146.81 hskp17 \/ hskp21 \/ hskp25 \/ hskp27 % 146.65/146.81 |- ~c0_1 a135 \/ ~c1_1 $_25 \/ c0_1 $_25 \/ c0_1 a136 \/ c2_1 $_25 \/ % 146.65/146.81 c2_1 a135 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp17 \/ hskp19 \/ % 146.65/146.81 hskp20 \/ hskp27 % 146.65/146.81 |- ~c0_1 $_26 \/ ~c1_1 $_26 \/ c0_1 a135 \/ c0_1 a136 \/ c2_1 $_26 \/ % 146.65/146.81 c2_1 a135 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp17 \/ hskp19 \/ % 146.65/146.81 hskp20 \/ hskp27 % 146.65/146.81 |- c0_1 a135 \/ c1_1 a136 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp14 \/ % 146.65/146.81 hskp17 \/ hskp21 \/ hskp27 % 146.65/146.81 |- ~c0_1 a153 \/ ~c1_1 $_25 \/ c0_1 $_25 \/ c0_1 a135 \/ c0_1 a136 \/ % 146.65/146.81 c2_1 $_25 \/ c2_1 a153 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp14 \/ % 146.65/146.81 hskp17 \/ hskp21 \/ hskp25 \/ hskp27 % 146.65/146.81 |- ~c0_1 a142 \/ c0_1 a135 \/ c0_1 a136 \/ c0_1 a153 \/ c2_1 a142 \/ % 146.65/146.81 c2_1 a153 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp17 \/ hskp21 \/ % 146.65/146.81 hskp25 \/ hskp27 \/ hskp7 % 146.65/146.81 |- ~c0_1 $_26 \/ ~c1_1 $_26 \/ c0_1 a135 \/ c0_1 a136 \/ c0_1 a153 \/ % 146.65/146.81 c2_1 $_26 \/ c2_1 a153 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp14 \/ % 146.65/146.81 hskp17 \/ hskp21 \/ hskp25 \/ hskp27 % 146.65/146.81 |- ~c0_1 $_21 \/ ~c1_1 $_20 \/ ~c1_1 $_21 \/ c0_1 $_20 \/ c0_1 a135 \/ % 146.65/146.81 c0_1 a136 \/ c2_1 $_20 \/ c2_1 $_21 \/ hskp11 \/ hskp12 \/ hskp13 \/ % 146.65/146.81 hskp14 \/ hskp17 \/ hskp21 \/ hskp27 % 146.65/146.81 |- ~c0_1 a149 \/ ~c1_1 $_122 \/ ~ndr1_0 \/ c0_1 $_122 \/ c0_1 a136 \/ % 146.65/146.81 c0_1 a142 \/ c2_1 $_122 \/ c2_1 a149 \/ hskp11 \/ hskp13 \/ hskp14 \/ % 146.65/146.81 hskp21 \/ hskp22 \/ hskp25 \/ hskp27 \/ hskp7 % 146.65/146.81 |- ~c0_1 a149 \/ ~c1_1 $_122 \/ ~ndr1_0 \/ c0_1 $_122 \/ c0_1 a136 \/ % 146.65/146.81 c0_1 a142 \/ c2_1 $_122 \/ c2_1 a149 \/ hskp11 \/ hskp13 \/ hskp17 \/ % 146.65/146.81 hskp2 \/ hskp21 \/ hskp22 \/ hskp25 \/ hskp27 \/ hskp7 % 146.65/146.81 |- hskp11 \/ hskp12 \/ hskp14 \/ hskp22 % 146.65/146.81 |- c2_1 a148 \/ hskp11 \/ hskp12 \/ hskp14 % 146.65/146.81 |- c1_1 a148 \/ hskp11 \/ hskp12 \/ hskp14 % 146.65/146.81 |- ~c1_1 a148 \/ ~c2_1 a138 \/ ~ndr1_0 \/ c1_1 a138 \/ c3_1 a148 \/ % 146.65/146.81 hskp11 \/ hskp12 \/ hskp14 % 146.65/146.81 |- ~c0_1 a148 \/ ~c1_1 a138 \/ ~ndr1_0 \/ c2_1 a138 \/ c3_1 a148 \/ % 146.65/146.81 hskp11 \/ hskp12 \/ hskp14 % 146.65/146.81 |- hskp11 \/ hskp12 \/ hskp14 \/ hskp7 \/ hskp8 % 146.65/146.81 |- c3_1 a142 \/ hskp11 \/ hskp12 \/ hskp14 \/ hskp7 % 146.65/146.81 |- c1_1 a142 \/ hskp11 \/ hskp12 \/ hskp14 \/ hskp7 % 146.65/146.81 |- ~c0_1 a142 \/ ~c1_1 $_20 \/ ~c1_1 a136 \/ c0_1 $_20 \/ c0_1 a136 \/ % 146.65/146.81 c2_1 $_20 \/ c2_1 a142 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp14 \/ % 146.65/146.81 hskp27 \/ hskp7 % 146.65/146.81 |- ~c0_1 $_21 \/ ~c1_1 $_21 \/ ~c1_1 a136 \/ c0_1 a136 \/ c0_1 a142 \/ % 146.65/146.81 c2_1 $_21 \/ c2_1 a142 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp14 \/ % 146.65/146.81 hskp27 \/ hskp7 % 146.65/146.81 |- ~c0_1 $X8 \/ ~c1_1 a142 \/ ~c2_1 $X8 \/ ~ndr1_0 \/ c2_1 a142 \/ % 146.65/146.81 c3_1 $X8 \/ hskp11 \/ hskp12 \/ hskp14 \/ hskp7 % 146.65/146.81 |- ~c0_1 a142 \/ ~c2_1 a142 \/ ~ndr1_0 \/ hskp11 \/ hskp12 \/ hskp14 \/ % 146.65/146.81 hskp3 \/ hskp4 \/ hskp7 % 146.65/146.81 |- ~c2_1 a142 \/ ~ndr1_0 \/ c0_1 a142 \/ hskp11 \/ hskp12 \/ hskp14 \/ % 146.65/146.81 hskp7 % 146.65/146.81 |- hskp10 \/ hskp11 \/ hskp12 \/ hskp14 \/ hskp9 % 146.65/146.81 |- ~c0_1 a148 \/ ~ndr1_0 \/ c2_1 a142 \/ c3_1 a148 \/ hskp12 \/ hskp13 \/ % 146.65/146.81 hskp17 \/ hskp19 \/ hskp2 \/ hskp20 \/ hskp7 % 146.65/146.81 |- hskp12 \/ hskp13 \/ hskp14 \/ hskp17 \/ hskp19 \/ hskp2 \/ hskp20 \/ % 146.65/146.81 hskp28 % 146.65/146.81 |- c2_1 a158 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp17 \/ hskp19 \/ hskp2 \/ % 146.65/146.81 hskp20 % 146.65/146.81 |- c1_1 a158 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp17 \/ hskp19 \/ hskp2 \/ % 146.65/146.81 hskp20 % 146.65/146.81 |- ~c0_1 a158 \/ ~ndr1_0 \/ c2_1 a142 \/ c3_1 a158 \/ hskp12 \/ hskp13 \/ % 146.65/146.81 hskp14 \/ hskp17 \/ hskp19 \/ hskp2 \/ hskp20 \/ hskp7 % 146.65/146.81 |- ~c0_1 a148 \/ ~ndr1_0 \/ c2_1 a142 \/ c3_1 a148 \/ hskp11 \/ hskp12 \/ % 146.65/146.81 hskp14 \/ hskp7 % 146.65/146.81 |- ~c0_1 a136 \/ ~ndr1_0 \/ c2_1 a142 \/ c3_1 a136 \/ hskp11 \/ hskp12 \/ % 146.65/146.81 hskp13 \/ hskp14 \/ hskp27 \/ hskp7 % 146.65/146.81 |- hskp12 \/ hskp13 \/ hskp18 \/ hskp19 \/ hskp20 \/ hskp27 % 146.65/146.81 |- c3_1 a157 \/ hskp12 \/ hskp13 \/ hskp18 \/ hskp19 \/ hskp20 % 146.65/146.81 |- c2_1 a157 \/ hskp12 \/ hskp13 \/ hskp18 \/ hskp19 \/ hskp20 % 146.65/146.81 |- c0_1 a157 \/ hskp12 \/ hskp13 \/ hskp18 \/ hskp19 \/ hskp20 % 146.65/146.81 |- hskp12 \/ hskp13 \/ hskp18 \/ hskp19 \/ hskp20 \/ hskp3 \/ hskp4 % 146.65/146.81 |- c3_1 a137 \/ hskp12 \/ hskp13 \/ hskp18 \/ hskp19 \/ hskp20 \/ hskp3 % 146.65/146.81 |- c1_1 a137 \/ hskp12 \/ hskp13 \/ hskp18 \/ hskp19 \/ hskp20 \/ hskp3 % 146.65/146.81 |- ~c0_1 $X8 \/ ~c1_1 a137 \/ ~c2_1 $X8 \/ ~ndr1_0 \/ c2_1 a137 \/ % 146.65/146.81 c3_1 $X8 \/ hskp12 \/ hskp13 \/ hskp18 \/ hskp19 \/ hskp20 \/ hskp3 % 146.65/146.81 |- ~c2_1 a137 \/ ~ndr1_0 \/ c0_1 a137 \/ hskp12 \/ hskp13 \/ hskp18 \/ % 146.65/146.81 hskp19 \/ hskp20 \/ hskp3 % 146.65/146.81 |- ~c1_1 $_147 \/ ~c2_1 $_147 \/ ~ndr1_0 \/ c1_1 a157 \/ c3_1 $_147 \/ % 146.65/146.81 hskp12 \/ hskp13 \/ hskp18 \/ hskp19 \/ hskp20 % 146.65/146.81 |- ~c0_1 a148 \/ ~ndr1_0 \/ c2_1 a142 \/ c3_1 a148 \/ hskp11 \/ hskp12 \/ % 146.65/146.81 hskp13 \/ hskp17 \/ hskp2 \/ hskp21 \/ hskp7 % 146.65/146.81 |- ~c0_1 a136 \/ ~ndr1_0 \/ c2_1 a142 \/ c3_1 a136 \/ hskp11 \/ hskp12 \/ % 146.65/146.81 hskp13 \/ hskp17 \/ hskp2 \/ hskp21 \/ hskp27 \/ hskp7 % 146.65/146.81 |- hskp11 \/ hskp12 \/ hskp13 \/ hskp18 \/ hskp21 \/ hskp25 \/ hskp27 % 146.65/146.81 |- c3_1 a157 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp18 \/ hskp21 \/ hskp25 % 146.65/146.81 |- c2_1 a157 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp18 \/ hskp21 \/ hskp25 % 146.65/146.81 |- c0_1 a157 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp18 \/ hskp21 \/ hskp25 % 146.65/146.81 |- hskp11 \/ hskp12 \/ hskp13 \/ hskp18 \/ hskp21 \/ hskp25 \/ hskp3 \/ % 146.65/146.81 hskp4 % 146.65/146.81 |- c3_1 a137 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp18 \/ hskp21 \/ hskp25 \/ % 146.65/146.81 hskp3 % 146.65/146.81 |- c1_1 a137 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp18 \/ hskp21 \/ hskp25 \/ % 146.65/146.81 hskp3 % 146.65/146.81 |- ~c0_1 $X8 \/ ~c1_1 a137 \/ ~c2_1 $X8 \/ ~ndr1_0 \/ c2_1 a137 \/ % 146.65/146.81 c3_1 $X8 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp18 \/ hskp21 \/ hskp25 \/ % 146.65/146.81 hskp3 % 146.65/146.81 |- ~c2_1 a137 \/ ~ndr1_0 \/ c0_1 a137 \/ hskp11 \/ hskp12 \/ hskp13 \/ % 146.65/146.81 hskp18 \/ hskp21 \/ hskp25 \/ hskp3 % 146.65/146.81 |- ~c1_1 $_157 \/ ~c2_1 $_157 \/ ~ndr1_0 \/ c1_1 a157 \/ c3_1 $_157 \/ % 146.65/146.81 hskp11 \/ hskp12 \/ hskp13 \/ hskp18 \/ hskp21 \/ hskp25 % 146.65/146.81 |- hskp11 \/ hskp12 \/ hskp14 \/ hskp28 % 146.65/146.81 |- c2_1 a158 \/ hskp11 \/ hskp12 \/ hskp14 % 146.65/146.81 |- c1_1 a158 \/ hskp11 \/ hskp12 \/ hskp14 % 146.65/146.81 |- ~c1_1 a158 \/ ~c2_1 a138 \/ ~ndr1_0 \/ c1_1 a138 \/ c3_1 a158 \/ % 146.65/146.81 hskp11 \/ hskp12 \/ hskp14 % 146.65/146.81 |- ~c0_1 a158 \/ ~c1_1 a138 \/ ~ndr1_0 \/ c2_1 a138 \/ c3_1 a158 \/ % 146.65/146.81 hskp11 \/ hskp12 \/ hskp14 % 146.65/146.81 |- ~c0_1 a158 \/ ~ndr1_0 \/ c2_1 a142 \/ c3_1 a158 \/ hskp11 \/ hskp12 \/ % 146.65/146.81 hskp14 \/ hskp7 % 146.65/146.81 |- ~c0_1 a136 \/ ~ndr1_0 \/ c0_1 a135 \/ c2_1 a135 \/ c3_1 a136 \/ % 146.65/146.81 hskp12 \/ hskp13 \/ hskp14 \/ hskp17 \/ hskp18 \/ hskp19 \/ hskp27 \/ % 146.65/146.81 hskp28 % 146.65/146.81 |- ~c0_1 a142 \/ ~c1_1 $_172 \/ c0_1 $_172 \/ c0_1 a135 \/ c0_1 a136 \/ % 146.65/146.81 c2_1 $_172 \/ c2_1 a142 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp14 \/ % 146.65/146.81 hskp17 \/ hskp21 \/ hskp27 \/ hskp7 % 146.65/146.81 |- hskp0 % 146.65/146.81 |- ndr1_0 % 146.65/146.81 |- ~c0_1 a142 \/ c0_1 a135 \/ c0_1 a136 \/ c2_1 a135 \/ c2_1 a142 \/ % 146.65/146.81 hskp11 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp17 \/ hskp21 \/ hskp27 \/ % 146.65/146.81 hskp7 % 146.65/146.81 |- ~c0_1 $_181 \/ ~c1_1 $_180 \/ ~c1_1 $_181 \/ c0_1 $_180 \/ c0_1 a148 \/ % 146.65/146.81 c2_1 $_180 \/ c2_1 $_181 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp19 \/ % 146.65/146.81 hskp2 \/ hskp20 % 146.65/146.81 |- ~c0_1 $_182 \/ ~c1_1 $_182 \/ c0_1 a148 \/ c0_1 a153 \/ c2_1 $_182 \/ % 146.65/146.81 c2_1 a153 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp19 \/ hskp2 \/ % 146.65/146.81 hskp20 \/ hskp25 % 146.65/146.81 |- ~c0_1 a142 \/ c0_1 a148 \/ c0_1 a153 \/ c2_1 a142 \/ c2_1 a153 \/ % 146.65/146.81 hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp19 \/ hskp2 \/ hskp20 \/ % 146.65/146.81 hskp25 \/ hskp7 % 146.65/146.81 |- ~c0_1 a153 \/ ~c1_1 $_184 \/ c0_1 $_184 \/ c0_1 a148 \/ c2_1 $_184 \/ % 146.65/146.81 c2_1 a153 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp19 \/ hskp2 \/ % 146.65/146.81 hskp20 \/ hskp25 % 146.65/146.81 |- ~c0_1 a153 \/ c0_1 a142 \/ c0_1 a148 \/ c2_1 a142 \/ c2_1 a153 \/ % 146.65/146.81 hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp19 \/ hskp2 \/ hskp20 \/ % 146.65/146.81 hskp25 \/ hskp7 % 146.65/146.81 |- ~c0_1 $_187 \/ ~c1_1 $_187 \/ c0_1 a142 \/ c0_1 a148 \/ c2_1 $_187 \/ % 146.65/146.81 c2_1 a142 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp19 \/ hskp2 \/ hskp20 \/ % 146.65/146.81 hskp7 % 146.65/146.81 |- ~c0_1 a142 \/ ~c1_1 $_186 \/ c0_1 $_186 \/ c0_1 a148 \/ c2_1 $_186 \/ % 146.65/146.81 c2_1 a142 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp19 \/ hskp2 \/ hskp20 \/ % 146.65/146.81 hskp7 % 146.65/146.81 |- ~c0_1 a142 \/ ~c1_1 a136 \/ c0_1 a136 \/ c0_1 a153 \/ c2_1 a142 \/ % 146.65/146.81 c2_1 a153 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp2 \/ hskp21 \/ % 146.65/146.81 hskp25 \/ hskp27 \/ hskp7 % 146.65/146.81 |- ~c0_1 a142 \/ ~c1_1 $_190 \/ c0_1 $_190 \/ c0_1 a136 \/ c2_1 $_190 \/ % 146.65/146.81 c2_1 a142 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp19 \/ hskp2 \/ % 146.65/146.81 hskp20 \/ hskp21 \/ hskp27 \/ hskp7 % 146.65/146.81 |- ~c0_1 a142 \/ c0_1 a136 \/ c0_1 a153 \/ c2_1 a142 \/ c2_1 a153 \/ % 146.65/146.81 hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp19 \/ hskp2 \/ hskp20 \/ % 146.65/146.81 hskp21 \/ hskp25 \/ hskp27 \/ hskp7 % 146.65/146.81 |- ~c0_1 $_192 \/ ~c1_1 $_192 \/ c0_1 a136 \/ c0_1 a142 \/ c2_1 $_192 \/ % 146.65/146.81 c2_1 a142 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp2 \/ hskp21 \/ % 146.65/146.81 hskp27 \/ hskp7 % 146.65/146.81 |- ~c0_1 a153 \/ c0_1 a136 \/ c0_1 a142 \/ c2_1 a142 \/ c2_1 a153 \/ % 146.65/146.81 hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp2 \/ hskp21 \/ hskp25 \/ % 146.65/146.81 hskp27 \/ hskp7 % 146.65/146.81 |- ~c0_1 $_195 \/ ~c1_1 $_194 \/ ~c1_1 $_195 \/ c0_1 $_194 \/ c0_1 a136 \/ % 146.65/146.81 c0_1 a153 \/ c2_1 $_194 \/ c2_1 $_195 \/ c2_1 a140 \/ hskp11 \/ % 146.65/146.81 hskp13 \/ hskp18 \/ hskp19 \/ hskp20 \/ hskp25 \/ hskp27 \/ hskp5 % 146.65/146.81 |- ~c0_1 a140 \/ ~c1_1 $_196 \/ c0_1 $_196 \/ c0_1 a136 \/ c0_1 a153 \/ % 146.65/146.81 c2_1 $_196 \/ c2_1 a140 \/ hskp11 \/ hskp13 \/ hskp18 \/ hskp19 \/ % 146.65/146.81 hskp20 \/ hskp25 \/ hskp27 \/ hskp5 % 146.65/146.81 |- ~c0_1 a142 \/ ~c1_1 $_196 \/ c0_1 $_196 \/ c0_1 a136 \/ c0_1 a153 \/ % 146.65/146.81 c2_1 $_196 \/ c2_1 a140 \/ c2_1 a142 \/ hskp11 \/ hskp13 \/ hskp18 \/ % 146.65/146.81 hskp19 \/ hskp20 \/ hskp25 \/ hskp27 \/ hskp5 \/ hskp7 % 146.65/146.81 |- ~c0_1 $_203 \/ ~c1_1 $_202 \/ ~c1_1 $_203 \/ c0_1 $_202 \/ c0_1 a136 \/ % 146.65/146.81 c0_1 a153 \/ c2_1 $_202 \/ c2_1 $_203 \/ c2_1 a149 \/ hskp11 \/ % 146.65/146.81 hskp13 \/ hskp14 \/ hskp19 \/ hskp20 \/ hskp22 \/ hskp25 \/ hskp27 % 146.65/146.81 |- ~c0_1 a142 \/ ~c1_1 $_204 \/ c0_1 $_204 \/ c0_1 a136 \/ c0_1 a153 \/ % 146.65/146.81 c2_1 $_204 \/ c2_1 a142 \/ c2_1 a149 \/ hskp11 \/ hskp13 \/ hskp14 \/ % 146.65/146.81 hskp19 \/ hskp20 \/ hskp22 \/ hskp25 \/ hskp27 \/ hskp7 % 146.65/146.82 |- ~c0_1 a149 \/ ~c1_1 $_204 \/ c0_1 $_204 \/ c0_1 a136 \/ c0_1 a153 \/ % 146.65/146.82 c2_1 $_204 \/ c2_1 a149 \/ hskp11 \/ hskp13 \/ hskp14 \/ hskp19 \/ % 146.65/146.82 hskp20 \/ hskp22 \/ hskp25 \/ hskp27 % 146.65/146.82 |- ~c0_1 a153 \/ c0_1 a135 \/ c0_1 a158 \/ c2_1 a135 \/ c2_1 a153 \/ % 146.65/146.82 hskp11 \/ hskp12 \/ hskp14 \/ hskp17 \/ hskp25 % 146.65/146.82 |- ~c0_1 a135 \/ c0_1 a153 \/ c0_1 a158 \/ c2_1 a135 \/ c2_1 a153 \/ % 146.65/146.82 hskp11 \/ hskp12 \/ hskp14 \/ hskp17 \/ hskp25 % 146.65/146.82 |- ~c0_1 $_227 \/ ~c1_1 $_226 \/ ~c1_1 $_227 \/ c0_1 $_226 \/ c0_1 a136 \/ % 146.65/146.82 c0_1 a153 \/ c2_1 $_226 \/ c2_1 $_227 \/ c2_1 a149 \/ hskp11 \/ % 146.65/146.82 hskp13 \/ hskp17 \/ hskp19 \/ hskp2 \/ hskp20 \/ hskp22 \/ hskp25 \/ % 146.65/146.82 hskp27 % 146.65/146.82 |- ~c0_1 a142 \/ ~c1_1 $_228 \/ c0_1 $_228 \/ c0_1 a136 \/ c0_1 a153 \/ % 146.65/146.82 c2_1 $_228 \/ c2_1 a142 \/ c2_1 a149 \/ hskp11 \/ hskp13 \/ hskp17 \/ % 146.65/146.82 hskp19 \/ hskp2 \/ hskp20 \/ hskp22 \/ hskp25 \/ hskp27 \/ hskp7 % 146.65/146.82 |- ~c0_1 a149 \/ ~c1_1 $_228 \/ c0_1 $_228 \/ c0_1 a136 \/ c0_1 a153 \/ % 146.65/146.82 c2_1 $_228 \/ c2_1 a149 \/ hskp11 \/ hskp13 \/ hskp17 \/ hskp19 \/ % 146.65/146.82 hskp2 \/ hskp20 \/ hskp22 \/ hskp25 \/ hskp27 % 146.65/146.82 |- ~c0_1 a153 \/ ~c1_1 a136 \/ c0_1 a136 \/ c0_1 a142 \/ c2_1 a142 \/ % 146.65/146.82 c2_1 a153 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp25 \/ hskp27 \/ % 146.65/146.82 hskp7 % 146.65/146.82 |- ~c0_1 $_237 \/ ~c1_1 $_237 \/ c0_1 a136 \/ c0_1 a142 \/ c2_1 $_237 \/ % 146.65/146.82 c2_1 a142 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp21 \/ hskp27 \/ % 146.65/146.82 hskp7 % 146.65/146.82 |- ~c0_1 $_237 \/ ~c1_1 $_237 \/ c0_1 a136 \/ c0_1 a142 \/ c2_1 $_237 \/ % 146.65/146.82 c2_1 a142 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp19 \/ hskp20 \/ % 146.65/146.82 hskp27 \/ hskp7 % 146.65/146.82 |- ~c0_1 a153 \/ c0_1 a136 \/ c0_1 a142 \/ c2_1 a142 \/ c2_1 a153 \/ % 146.65/146.82 hskp11 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp21 \/ hskp25 \/ hskp27 \/ % 146.65/146.82 hskp7 % 146.65/146.82 |- ~c0_1 a153 \/ c0_1 a136 \/ c0_1 a142 \/ c2_1 a142 \/ c2_1 a153 \/ % 146.65/146.82 hskp11 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp19 \/ hskp20 \/ hskp25 \/ % 146.65/146.82 hskp27 \/ hskp7 % 146.65/146.82 |- ~c0_1 a135 \/ c0_1 a136 \/ c0_1 a142 \/ c2_1 a135 \/ c2_1 a142 \/ % 146.65/146.82 hskp11 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp17 \/ hskp21 \/ hskp27 \/ % 146.65/146.82 hskp7 % 146.65/146.82 |- ~c0_1 a135 \/ c0_1 a136 \/ c0_1 a142 \/ c2_1 a135 \/ c2_1 a142 \/ % 146.65/146.82 hskp11 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp17 \/ hskp19 \/ hskp20 \/ % 146.65/146.82 hskp27 \/ hskp7 % 146.65/146.82 |- ~c0_1 a142 \/ ~c1_1 a136 \/ c0_1 a136 \/ c0_1 a153 \/ c2_1 a142 \/ % 146.65/146.82 c2_1 a153 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp25 \/ hskp27 \/ % 146.65/146.82 hskp7 % 146.65/146.82 |- ~c0_1 a142 \/ ~c1_1 $_240 \/ c0_1 $_240 \/ c0_1 a136 \/ c2_1 $_240 \/ % 146.65/146.82 c2_1 a142 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp19 \/ hskp20 \/ % 146.65/146.82 hskp27 \/ hskp7 % 146.65/146.82 |- ~c0_1 a142 \/ c0_1 a136 \/ c0_1 a153 \/ c2_1 a142 \/ c2_1 a153 \/ % 146.65/146.82 hskp11 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp19 \/ hskp20 \/ hskp25 \/ % 146.65/146.82 hskp27 \/ hskp7 % 146.65/146.82 |- ~c0_1 a142 \/ c0_1 a135 \/ c0_1 a136 \/ c2_1 a135 \/ c2_1 a142 \/ % 146.65/146.82 hskp11 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp17 \/ hskp19 \/ hskp20 \/ % 146.65/146.82 hskp27 \/ hskp7 % 146.65/146.82 |- ~c0_1 $_256 \/ ~c1_1 $_255 \/ ~c1_1 $_256 \/ c0_1 $_255 \/ c0_1 a136 \/ % 146.65/146.82 c0_1 a142 \/ c0_1 a153 \/ c2_1 $_255 \/ c2_1 $_256 \/ c2_1 a149 \/ % 146.65/146.82 hskp11 \/ hskp13 \/ hskp14 \/ hskp21 \/ hskp22 \/ hskp25 \/ hskp27 \/ % 146.65/146.82 hskp7 % 146.65/146.82 |- ~c0_1 a149 \/ ~c1_1 $_257 \/ c0_1 $_257 \/ c0_1 a136 \/ c0_1 a142 \/ % 146.65/146.82 c0_1 a153 \/ c2_1 $_257 \/ c2_1 a149 \/ hskp11 \/ hskp13 \/ hskp14 \/ % 146.65/146.82 hskp21 \/ hskp22 \/ hskp25 \/ hskp27 \/ hskp7 % 146.65/146.82 |- hskp12 \/ hskp13 \/ hskp17 \/ hskp18 \/ hskp19 \/ hskp21 \/ hskp27 % 146.65/146.82 |- c3_1 a157 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp18 \/ hskp19 \/ hskp21 % 146.65/146.82 |- c2_1 a157 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp18 \/ hskp19 \/ hskp21 % 146.65/146.82 |- c0_1 a157 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp18 \/ hskp19 \/ hskp21 % 146.65/146.82 |- hskp12 \/ hskp13 \/ hskp17 \/ hskp18 \/ hskp19 \/ hskp21 \/ hskp3 \/ % 146.65/146.82 hskp4 % 146.65/146.82 |- c3_1 a137 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp18 \/ hskp19 \/ hskp21 \/ % 146.65/146.82 hskp3 % 146.65/146.82 |- c1_1 a137 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp18 \/ hskp19 \/ hskp21 \/ % 146.65/146.82 hskp3 % 146.65/146.82 |- ~c0_1 $X8 \/ ~c1_1 a137 \/ ~c2_1 $X8 \/ c2_1 a137 \/ c3_1 $X8 \/ % 146.65/146.82 hskp12 \/ hskp13 \/ hskp17 \/ hskp18 \/ hskp19 \/ hskp21 \/ hskp3 % 146.65/146.82 |- ~c2_1 a137 \/ c0_1 a137 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp18 \/ % 146.65/146.82 hskp19 \/ hskp21 \/ hskp3 % 146.65/146.82 |- ~c1_1 $_265 \/ ~c2_1 $_265 \/ c1_1 a157 \/ c3_1 $_265 \/ hskp12 \/ % 146.65/146.82 hskp13 \/ hskp17 \/ hskp18 \/ hskp19 \/ hskp21 % 146.65/146.82 |- ~c0_1 $_271 \/ ~c1_1 $_270 \/ ~c1_1 $_271 \/ c0_1 $_270 \/ c0_1 a148 \/ % 146.65/146.82 c2_1 $_270 \/ c2_1 $_271 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ % 146.65/146.82 hskp2 \/ hskp21 % 146.65/146.82 |- ~c0_1 $_272 \/ ~c1_1 $_272 \/ c0_1 a148 \/ c0_1 a153 \/ c2_1 $_272 \/ % 146.65/146.82 c2_1 a153 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp2 \/ hskp21 \/ % 146.65/146.82 hskp25 % 146.65/146.82 |- ~c0_1 a142 \/ c0_1 a148 \/ c0_1 a153 \/ c2_1 a142 \/ c2_1 a153 \/ % 146.65/146.82 hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp2 \/ hskp21 \/ hskp25 \/ % 146.65/146.82 hskp7 % 146.65/146.82 |- ~c0_1 a153 \/ ~c1_1 $_274 \/ c0_1 $_274 \/ c0_1 a148 \/ c2_1 $_274 \/ % 146.65/146.82 c2_1 a153 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp2 \/ hskp21 \/ % 146.65/146.82 hskp25 % 146.65/146.82 |- ~c0_1 a153 \/ c0_1 a142 \/ c0_1 a148 \/ c2_1 a142 \/ c2_1 a153 \/ % 146.65/146.82 hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp2 \/ hskp21 \/ hskp25 \/ % 146.65/146.82 hskp7 % 146.65/146.82 |- ~c0_1 $_277 \/ ~c1_1 $_277 \/ c0_1 a142 \/ c0_1 a148 \/ c2_1 $_277 \/ % 146.65/146.82 c2_1 a142 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp2 \/ hskp21 \/ % 146.65/146.82 hskp7 % 146.65/146.82 |- ~c0_1 a142 \/ ~c1_1 $_276 \/ c0_1 $_276 \/ c0_1 a148 \/ c2_1 $_276 \/ % 146.65/146.82 c2_1 a142 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp2 \/ hskp21 \/ % 146.65/146.82 hskp7 % 146.65/146.82 |- ~c0_1 $_281 \/ ~c1_1 $_280 \/ ~c1_1 $_281 \/ c0_1 $_280 \/ c0_1 a136 \/ % 146.65/146.82 c0_1 a142 \/ c0_1 a153 \/ c2_1 $_280 \/ c2_1 $_281 \/ c2_1 a149 \/ % 146.65/146.82 hskp11 \/ hskp13 \/ hskp17 \/ hskp2 \/ hskp21 \/ hskp22 \/ hskp25 \/ % 146.65/146.82 hskp27 \/ hskp7 % 146.65/146.82 |- ~c0_1 a149 \/ ~c1_1 $_282 \/ c0_1 $_282 \/ c0_1 a136 \/ c0_1 a142 \/ % 146.65/146.82 c0_1 a153 \/ c2_1 $_282 \/ c2_1 a149 \/ hskp11 \/ hskp13 \/ hskp17 \/ % 146.65/146.82 hskp2 \/ hskp21 \/ hskp22 \/ hskp25 \/ hskp27 \/ hskp7 % 146.65/146.82 |- ~c0_1 $_292 \/ ~c1_1 $_291 \/ ~c1_1 $_292 \/ c0_1 $_291 \/ c0_1 a148 \/ % 146.65/146.82 c2_1 $_291 \/ c2_1 $_292 \/ hskp11 \/ hskp12 \/ hskp14 % 146.65/146.82 |- ~c0_1 $_293 \/ ~c1_1 $_293 \/ c0_1 a148 \/ c0_1 a153 \/ c2_1 $_293 \/ % 146.65/146.82 c2_1 a153 \/ hskp11 \/ hskp12 \/ hskp14 \/ hskp25 % 146.65/146.82 |- ~c0_1 a135 \/ c0_1 a148 \/ c0_1 a153 \/ c2_1 a135 \/ c2_1 a153 \/ % 146.65/146.82 hskp11 \/ hskp12 \/ hskp14 \/ hskp17 \/ hskp25 % 146.65/146.82 |- ~c0_1 a142 \/ c0_1 a148 \/ c0_1 a153 \/ c2_1 a142 \/ c2_1 a153 \/ % 146.65/146.82 hskp11 \/ hskp12 \/ hskp14 \/ hskp25 \/ hskp7 % 146.65/146.82 |- ~c0_1 a153 \/ ~c1_1 $_295 \/ c0_1 $_295 \/ c0_1 a148 \/ c2_1 $_295 \/ % 146.65/146.82 c2_1 a153 \/ hskp11 \/ hskp12 \/ hskp14 \/ hskp25 % 146.65/146.82 |- ~c0_1 a153 \/ c0_1 a135 \/ c0_1 a148 \/ c2_1 a135 \/ c2_1 a153 \/ % 146.65/146.82 hskp11 \/ hskp12 \/ hskp14 \/ hskp17 \/ hskp25 % 146.65/146.82 |- ~c0_1 a153 \/ c0_1 a142 \/ c0_1 a148 \/ c2_1 a142 \/ c2_1 a153 \/ % 146.65/146.82 hskp11 \/ hskp12 \/ hskp14 \/ hskp25 \/ hskp7 % 146.65/146.82 |- ~c0_1 $_298 \/ ~c1_1 $_298 \/ c0_1 a135 \/ c0_1 a148 \/ c2_1 $_298 \/ % 146.65/146.82 c2_1 a135 \/ hskp11 \/ hskp12 \/ hskp14 \/ hskp17 % 146.65/146.82 |- ~c0_1 $_298 \/ ~c1_1 $_298 \/ c0_1 a142 \/ c0_1 a148 \/ c2_1 $_298 \/ % 146.65/146.82 c2_1 a142 \/ hskp11 \/ hskp12 \/ hskp14 \/ hskp7 % 146.65/146.82 |- ~c0_1 a135 \/ ~c1_1 $_297 \/ c0_1 $_297 \/ c0_1 a148 \/ c2_1 $_297 \/ % 146.65/146.82 c2_1 a135 \/ hskp11 \/ hskp12 \/ hskp14 \/ hskp17 % 146.65/146.82 |- ~c0_1 a142 \/ ~c1_1 $_297 \/ c0_1 $_297 \/ c0_1 a148 \/ c2_1 $_297 \/ % 146.65/146.82 c2_1 a142 \/ hskp11 \/ hskp12 \/ hskp14 \/ hskp7 % 146.65/146.82 |- ~c0_1 a142 \/ c0_1 a135 \/ c0_1 a148 \/ c2_1 a135 \/ c2_1 a142 \/ % 146.65/146.82 hskp11 \/ hskp12 \/ hskp14 \/ hskp17 \/ hskp7 % 146.65/146.82 |- ~c0_1 a135 \/ c0_1 a142 \/ c0_1 a148 \/ c2_1 a135 \/ c2_1 a142 \/ % 146.65/146.82 hskp11 \/ hskp12 \/ hskp14 \/ hskp17 \/ hskp7 % 146.65/146.82 |- hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp18 \/ hskp21 \/ hskp27 % 146.65/146.82 |- c3_1 a157 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp18 \/ hskp21 % 146.65/146.82 |- c2_1 a157 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp18 \/ hskp21 % 146.65/146.82 |- c0_1 a157 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp18 \/ hskp21 % 146.65/146.82 |- hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp18 \/ hskp21 \/ hskp3 \/ % 146.65/146.82 hskp4 % 146.65/146.82 |- c3_1 a137 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp18 \/ hskp21 \/ % 146.65/146.82 hskp3 % 146.65/146.82 |- c1_1 a137 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp18 \/ hskp21 \/ % 146.65/146.82 hskp3 % 146.65/146.82 |- ~c0_1 $X8 \/ ~c1_1 a137 \/ ~c2_1 $X8 \/ c2_1 a137 \/ c3_1 $X8 \/ % 146.65/146.82 hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ hskp18 \/ hskp21 \/ hskp3 % 146.65/146.82 |- ~c2_1 a137 \/ c0_1 a137 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp17 \/ % 146.65/146.82 hskp18 \/ hskp21 \/ hskp3 % 146.65/146.82 |- ~c1_1 $_308 \/ ~c2_1 $_308 \/ c1_1 a157 \/ c3_1 $_308 \/ hskp11 \/ % 146.65/146.82 hskp12 \/ hskp13 \/ hskp17 \/ hskp18 \/ hskp21 % 146.65/146.82 |- ~c0_1 a153 \/ c0_1 a135 \/ c0_1 a136 \/ c2_1 a135 \/ c2_1 a153 \/ % 146.65/146.82 hskp11 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp17 \/ hskp19 \/ hskp20 \/ % 146.65/146.82 hskp25 \/ hskp27 % 146.65/146.82 |- ~c0_1 a135 \/ c0_1 a136 \/ c0_1 a153 \/ c2_1 a135 \/ c2_1 a153 \/ % 146.65/146.82 hskp11 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp17 \/ hskp19 \/ hskp20 \/ % 146.65/146.82 hskp25 \/ hskp27 % 146.65/146.82 |- ~c0_1 $_326 \/ ~c1_1 $_325 \/ ~c1_1 $_326 \/ c0_1 $_325 \/ c0_1 a158 \/ % 146.65/146.82 c2_1 $_325 \/ c2_1 $_326 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp17 \/ % 146.65/146.82 hskp19 \/ hskp2 \/ hskp20 % 146.65/146.82 |- ~c0_1 $_328 \/ ~c1_1 $_328 \/ c0_1 a142 \/ c0_1 a158 \/ c2_1 $_328 \/ % 146.65/146.82 c2_1 a142 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp17 \/ hskp19 \/ hskp2 \/ % 146.65/146.82 hskp20 \/ hskp7 % 146.65/146.82 |- ~c0_1 a142 \/ ~c1_1 $_327 \/ c0_1 $_327 \/ c0_1 a158 \/ c2_1 $_327 \/ % 146.65/146.82 c2_1 a142 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp17 \/ hskp19 \/ hskp2 \/ % 146.65/146.82 hskp20 \/ hskp7 % 146.65/146.82 |- ~c0_1 $_332 \/ ~c1_1 $_332 \/ c0_1 a136 \/ c0_1 a142 \/ c0_1 a153 \/ % 146.65/146.82 c2_1 $_332 \/ c2_1 a153 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp14 \/ % 146.65/146.82 hskp21 \/ hskp25 \/ hskp27 \/ hskp7 % 146.65/146.82 |- ~c0_1 a135 \/ ~c1_1 $_331 \/ c0_1 $_331 \/ c0_1 a136 \/ c0_1 a142 \/ % 146.65/146.82 c2_1 $_331 \/ c2_1 a135 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp14 \/ % 146.65/146.82 hskp17 \/ hskp21 \/ hskp27 \/ hskp7 % 146.65/146.82 |- ~c0_1 a153 \/ ~c1_1 $_331 \/ c0_1 $_331 \/ c0_1 a136 \/ c0_1 a142 \/ % 146.65/146.82 c2_1 $_331 \/ c2_1 a153 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp14 \/ % 146.65/146.82 hskp21 \/ hskp25 \/ hskp27 \/ hskp7 % 146.65/146.82 |- ~c0_1 a135 \/ c0_1 a136 \/ c0_1 a142 \/ c0_1 a153 \/ c2_1 a135 \/ % 146.65/146.82 c2_1 a153 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp17 \/ hskp21 \/ % 146.65/146.82 hskp25 \/ hskp27 \/ hskp7 % 146.65/146.82 |- ~c0_1 $_338 \/ ~c1_1 $_337 \/ ~c1_1 $_338 \/ c0_1 $_337 \/ c0_1 a158 \/ % 146.65/146.82 c2_1 $_337 \/ c2_1 $_338 \/ hskp11 \/ hskp12 \/ hskp14 % 146.65/146.82 |- ~c0_1 $_340 \/ ~c1_1 $_340 \/ c0_1 a135 \/ c0_1 a158 \/ c2_1 $_340 \/ % 146.65/146.82 c2_1 a135 \/ hskp11 \/ hskp12 \/ hskp14 \/ hskp17 % 146.65/146.82 |- ~c0_1 $_340 \/ ~c1_1 $_340 \/ c0_1 a142 \/ c0_1 a158 \/ c2_1 $_340 \/ % 146.65/146.82 c2_1 a142 \/ hskp11 \/ hskp12 \/ hskp14 \/ hskp7 % 146.65/146.82 |- ~c0_1 $_340 \/ ~c1_1 $_340 \/ c0_1 a153 \/ c0_1 a158 \/ c2_1 $_340 \/ % 146.65/146.82 c2_1 a153 \/ hskp11 \/ hskp12 \/ hskp14 \/ hskp25 % 146.65/146.82 |- ~c0_1 a135 \/ ~c1_1 $_339 \/ c0_1 $_339 \/ c0_1 a158 \/ c2_1 $_339 \/ % 146.65/146.82 c2_1 a135 \/ hskp11 \/ hskp12 \/ hskp14 \/ hskp17 % 146.65/146.82 |- ~c0_1 a142 \/ ~c1_1 $_339 \/ c0_1 $_339 \/ c0_1 a158 \/ c2_1 $_339 \/ % 146.65/146.82 c2_1 a142 \/ hskp11 \/ hskp12 \/ hskp14 \/ hskp7 % 146.65/146.82 |- ~c0_1 a153 \/ ~c1_1 $_339 \/ c0_1 $_339 \/ c0_1 a158 \/ c2_1 $_339 \/ % 146.65/146.82 c2_1 a153 \/ hskp11 \/ hskp12 \/ hskp14 \/ hskp25 % 146.65/146.82 |- ~c0_1 a142 \/ c0_1 a135 \/ c0_1 a158 \/ c2_1 a135 \/ c2_1 a142 \/ % 146.65/146.82 hskp11 \/ hskp12 \/ hskp14 \/ hskp17 \/ hskp7 % 146.65/146.82 |- ~c0_1 a135 \/ c0_1 a142 \/ c0_1 a158 \/ c2_1 a135 \/ c2_1 a142 \/ % 146.65/146.82 hskp11 \/ hskp12 \/ hskp14 \/ hskp17 \/ hskp7 % 146.65/146.82 |- ~c0_1 a153 \/ c0_1 a142 \/ c0_1 a158 \/ c2_1 a142 \/ c2_1 a153 \/ % 146.65/146.82 hskp11 \/ hskp12 \/ hskp14 \/ hskp25 \/ hskp7 % 146.65/146.82 |- ~c0_1 a142 \/ c0_1 a153 \/ c0_1 a158 \/ c2_1 a142 \/ c2_1 a153 \/ % 146.65/146.82 hskp11 \/ hskp12 \/ hskp14 \/ hskp25 \/ hskp7 % 146.65/146.82 |- ~c0_1 a153 \/ c0_1 a135 \/ c0_1 a136 \/ c2_1 a135 \/ c2_1 a153 \/ % 146.65/146.82 hskp11 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp17 \/ hskp21 \/ hskp25 \/ % 146.65/146.82 hskp27 % 146.65/146.82 |- ~c0_1 $_353 \/ ~c1_1 $_353 \/ c0_1 a135 \/ c0_1 a136 \/ c2_1 $_353 \/ % 146.65/146.82 c2_1 a135 \/ hskp11 \/ hskp12 \/ hskp13 \/ hskp14 \/ hskp17 \/ hskp21 \/ % 146.65/146.82 hskp27 % 146.65/146.82 SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 146.65/146.82 %------------------------------------------------------------------------------