Metis---2.4.SAT-Sat.s

%------------------------------------------------------------------------------
% File     : Metis---2.4
% Problem  : SYN538-1 : TPTP v8.1.0. Released v2.1.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : metis --show proof --show saturation %s

% Computer : n016.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:03:48 EDT 2022

% Result   : Satisfiable 0.66s 0.83s
% Output   : Saturation 0.71s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12  % Problem  : SYN538-1 : TPTP v8.1.0. Released v2.1.0.
% 0.07/0.13  % Command  : metis --show proof --show saturation %s
% 0.13/0.34  % Computer : n016.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 01:07:13 EDT 2022
% 0.13/0.34  % CPUTime  : 
% 0.13/0.35  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.66/0.83  % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.66/0.83  
% 0.66/0.83  SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.66/0.83  |- c1_0 \/ c4_0
% 0.66/0.83  |- ndr1_0 \/ ssSkC7
% 0.66/0.83  |- ndr1_0 \/ ssSkC5
% 0.66/0.83  |- ndr1_0 \/ ssSkC3
% 0.66/0.83  |- ndr1_0 \/ ssSkC1
% 0.66/0.83  |- ndr1_0 \/ ssSkC0
% 0.66/0.83  |- ~ssSkC6 \/ c1_0 \/ ndr1_0
% 0.66/0.83  |- ~ssSkC3 \/ ~ssSkC4 \/ ndr1_0
% 0.66/0.83  |- ~c1_0 \/ c3_0
% 0.66/0.83  |- c3_1 a583 \/ ssSkC7
% 0.66/0.83  |- c5_1 a583 \/ ssSkC7
% 0.66/0.83  |- ndr1_1 $U \/ ssSkP3 $U
% 0.66/0.83  |- ndr1_1 a567 \/ ssSkC5
% 0.66/0.83  |- c1_1 a567 \/ ssSkC5
% 0.66/0.83  |- c2_1 a567 \/ ssSkC5
% 0.66/0.83  |- ndr1_1 $U \/ ssSkP2 $U
% 0.66/0.83  |- ndr1_1 $U \/ ssSkP1 $U
% 0.66/0.83  |- c5_1 a556 \/ ssSkC1
% 0.66/0.83  |- ndr1_1 $U \/ ssSkP0 $U
% 0.66/0.83  |- ndr1_1 a546 \/ ssSkC0
% 0.66/0.83  |- c2_1 a546 \/ ssSkC0
% 0.66/0.83  |- ~c4_0 \/ c3_0 \/ ndr1_0
% 0.66/0.83  |- ~ssSkC6 \/ c1_0 \/ c1_1 a577
% 0.66/0.83  |- ~ssSkC6 \/ c1_0 \/ c4_1 a577
% 0.66/0.83  |- ~c2_0 \/ ~c4_0
% 0.66/0.83  |- ~c3_0 \/ c4_0 \/ c5_0
% 0.66/0.83  |- ~c4_1 a583 \/ ssSkC7
% 0.66/0.83  |- c3_2 $U a579 \/ ssSkP3 $U
% 0.66/0.83  |- c4_2 a567 a568 \/ ssSkC5
% 0.66/0.83  |- c2_2 $U a562 \/ ssSkP2 $U
% 0.66/0.83  |- c5_2 $U a562 \/ ssSkP2 $U
% 0.66/0.83  |- ~c1_1 a561 \/ ssSkC3
% 0.66/0.83  |- c1_2 $U a557 \/ ssSkP1 $U
% 0.66/0.83  |- ~c4_1 a556 \/ ssSkC1
% 0.66/0.83  |- c5_2 $U a548 \/ ssSkP0 $U
% 0.66/0.83  |- c2_2 $U a548 \/ ssSkP0 $U
% 0.66/0.83  |- c2_2 a546 a547 \/ ssSkC0
% 0.66/0.83  |- c5_2 a546 a547 \/ ssSkC0
% 0.66/0.83  |- ~c1_0 \/ ~c4_0 \/ ndr1_0
% 0.66/0.83  |- ~c2_1 a584 \/ ~ssSkC7 \/ c4_0
% 0.66/0.83  |- ~c5_1 a584 \/ ~ssSkC7 \/ c4_0
% 0.66/0.83  |- ~c4_0 \/ c3_0 \/ c5_1 a578
% 0.66/0.83  |- ~c1_1 a569 \/ ~ssSkC5 \/ c5_0
% 0.66/0.83  |- ~c2_1 a569 \/ ~ssSkC5 \/ c5_0
% 0.66/0.83  |- ~c3_0 \/ ~c5_0 \/ ndr1_0
% 0.66/0.83  |- ~c3_1 a564 \/ ~ssSkC3 \/ ~ssSkC4
% 0.66/0.83  |- ~c1_1 a564 \/ ~ssSkC3 \/ ~ssSkC4
% 0.66/0.83  |- ~c2_1 $U \/ ~ndr1_0 \/ c2_0
% 0.66/0.83  |- ~c2_2 $U a579 \/ ssSkP3 $U
% 0.66/0.83  |- ~c1_2 a567 a568 \/ ssSkC5
% 0.66/0.83  |- ~c4_2 $U a562 \/ ssSkP2 $U
% 0.66/0.83  |- ~c3_2 $U a557 \/ ssSkP1 $U
% 0.66/0.83  |- ~c1_2 $U a548 \/ ssSkP0 $U
% 0.66/0.83  |- ~c4_2 a546 a547 \/ ssSkC0
% 0.66/0.83  |- ~c1_0 \/ ~c4_0 \/ c2_1 a585
% 0.66/0.83  |- ~c1_0 \/ ~c4_0 \/ c5_1 a585
% 0.66/0.83  |- ~c2_1 a578 \/ ~c4_0 \/ c3_0
% 0.66/0.83  |- ~c4_0 \/ ~c5_1 a550 \/ c3_0
% 0.66/0.83  |- ~c1_0 \/ ~c1_1 a585 \/ ~c4_0
% 0.66/0.83  |- ~c1_1 a565 \/ ~c3_0 \/ ~c5_0
% 0.66/0.83  |- ~c2_1 $U \/ ~ndr1_0 \/ c3_1 $U \/ ndr1_1 $U \/ ssSkC6
% 0.66/0.83  |- ~ndr1_0 \/ ~ssSkP2 $U \/ c1_2 $U a563 \/ c3_1 $U \/ ssSkC4
% 0.66/0.83  |- ~ndr1_0 \/ ~ssSkP2 $U \/ c3_1 $U \/ c4_2 $U a563 \/ ssSkC4
% 0.66/0.83  |- ~ndr1_0 \/ ~ssSkC1 \/ ~ssSkP1 $U \/ c2_1 $U \/ c2_2 $U a558 \/ c5_0
% 0.66/0.83  |- ~c3_1 $U \/ ~ndr1_0 \/ c1_0 \/ c5_0 \/ c5_1 $U \/ ndr1_1 $U
% 0.66/0.83  |- ~c2_1 $U \/ ~c4_1 $U \/ ~ndr1_0 \/ c3_0 \/ c3_1 $U
% 0.66/0.83  |- ~c2_1 $U \/ ~ndr1_0 \/ c2_2 $U a576 \/ c3_1 $U \/ ssSkC6
% 0.66/0.83  |- ~c2_2 $U a563 \/ ~ndr1_0 \/ ~ssSkP2 $U \/ c3_1 $U \/ ssSkC4
% 0.66/0.83  |- ~c3_1 $U \/ ~c4_1 $U \/ ~ndr1_0 \/ ~ssSkC2 \/ c2_0 \/ ndr1_1 $U
% 0.66/0.83  |- ~c5_2 $U a558 \/ ~ndr1_0 \/ ~ssSkC1 \/ ~ssSkP1 $U \/ c2_1 $U \/ c5_0
% 0.66/0.83  |- ~c3_2 $U a558 \/ ~ndr1_0 \/ ~ssSkC1 \/ ~ssSkP1 $U \/ c2_1 $U \/ c5_0
% 0.66/0.83  |- ~c3_0 \/ ~c3_1 $U \/ ~ndr1_0 \/ c1_0 \/ c1_1 $U \/ c4_1 $U
% 0.66/0.83  |- ~c2_2 a569 $U \/ ~ndr1_1 a569 \/ ~ssSkC5 \/ c3_2 a569 $U \/ c5_0
% 0.66/0.83  |- ~c2_1 $U \/ ~c5_2 $U a576 \/ ~ndr1_0 \/ c3_1 $U \/ ssSkC6
% 0.66/0.83  |- ~c3_1 $U \/ ~c4_1 $V \/ ~ndr1_0 \/ c2_1 $V \/ c4_1 $U \/ ndr1_1 $V
% 0.66/0.83  |- ~c3_1 $U \/ ~c4_1 $U \/ ~ndr1_0 \/ ~ssSkC2 \/ c2_0 \/ c5_2 $U a560
% 0.66/0.83  |- ~c3_1 $U \/ ~c4_1 $U \/ ~ndr1_0 \/ ~ssSkC2 \/ c2_0 \/ c3_2 $U a560
% 0.66/0.83  |- ~c3_1 $U \/ ~c5_2 $U a555 \/ ~ndr1_0 \/ c1_0 \/ c5_0 \/ c5_1 $U
% 0.66/0.83  |- ~c1_2 $U a555 \/ ~c3_1 $U \/ ~ndr1_0 \/ c1_0 \/ c5_0 \/ c5_1 $U
% 0.66/0.83  |- ~c3_1 $U \/ ~c4_2 $U a555 \/ ~ndr1_0 \/ c1_0 \/ c5_0 \/ c5_1 $U
% 0.66/0.83  |- ~c4_0 \/ ~c5_2 a578 $U \/ ~ndr1_1 a578 \/ c3_0 \/ c4_2 a578 $U
% 0.66/0.83  |- ~c1_1 a551 \/ ~c3_1 $U \/ ~c4_0 \/ ~c4_1 $U \/ ~ndr1_0
% 0.66/0.83  |- ~c3_1 $U \/ ~c4_1 $V \/ ~ndr1_0 \/ c2_1 $V \/ c2_2 $V a575 \/ c4_1 $U
% 0.66/0.83  |- ~c3_1 $U \/ ~c4_1 $V \/ ~ndr1_0 \/ c1_2 $V a575 \/ c2_1 $V \/ c4_1 $U
% 0.66/0.83  |- ~c2_0 \/ ~c2_1 $U \/ ~c4_1 $U \/ ~ndr1_0 \/ c1_1 $U \/ ndr1_1 a571
% 0.66/0.83  |- ~c2_0 \/ ~c2_1 $U \/ ~c4_1 $U \/ ~ndr1_0 \/ c1_1 $U \/ c1_1 a571
% 0.66/0.83  |- ~c3_1 $U \/ ~c3_2 $V a575 \/ ~c4_1 $V \/ ~ndr1_0 \/ c2_1 $V \/ c4_1 $U
% 0.66/0.83  |- ~c2_0 \/ ~c2_1 $U \/ ~c4_1 $U \/ ~ndr1_0 \/ c1_1 $U \/ c3_2 a571 a573
% 0.66/0.83  |- ~c2_0 \/ ~c2_1 $U \/ ~c4_1 $U \/ ~ndr1_0 \/ c1_1 $U \/ c1_2 a571 a573
% 0.66/0.83  |- ~c2_0 \/ ~c2_1 $U \/ ~c4_1 $U \/ ~ndr1_0 \/ c1_1 $U \/ c5_2 a571 a572
% 0.66/0.83  |- ~c1_2 a565 $U \/ ~c2_2 a565 $U \/ ~c3_0 \/ ~c5_0 \/ ~ndr1_1 a565
% 0.66/0.83  |- ~c2_0 \/ ~c2_1 $U \/ ~c4_1 $U \/ ~c4_2 a571 a573 \/ ~ndr1_0 \/ c1_1 $U
% 0.66/0.83  |- ~c2_0 \/ ~c2_1 $U \/ ~c3_2 a571 a572 \/ ~c4_1 $U \/ ~ndr1_0 \/ c1_1 $U
% 0.66/0.83  |- ~c1_2 a571 a572 \/ ~c2_0 \/ ~c2_1 $U \/ ~c4_1 $U \/ ~ndr1_0 \/ c1_1 $U
% 0.66/0.83  |- ~c2_2 a561 $U \/ ~c4_2 a561 $U \/ ~c5_2 a561 $U \/ ~ndr1_1 a561 \/
% 0.66/0.83     ssSkC3
% 0.66/0.83  |- ~c3_1 $U \/ ~c3_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_2 $U $V \/
% 0.66/0.83     c4_1 $U \/ c4_2 $U $V \/ ndr1_1 a552
% 0.66/0.83  |- ~c1_1 $U \/ ~c4_2 $U $V \/ ~c5_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/
% 0.66/0.83     c1_2 $U $V \/ c2_1 $U \/ c5_0
% 0.66/0.83  |- ~c2_2 $U $V \/ ~c3_0 \/ ~c4_1 $U \/ ~ndr1_0 \/ ~ndr1_1 $U \/
% 0.66/0.83     c1_2 $U $V \/ c3_2 $U $V \/ c5_1 $U
% 0.66/0.83  |- ~c2_0 \/ ~c2_2 $U a570 \/ ~c5_1 $U \/ ~c5_2 $U $V \/ ~ndr1_0 \/
% 0.66/0.83     ~ndr1_1 $U \/ c2_2 $U $V \/ c5_0
% 0.66/0.83  |- ~c2_0 \/ ~c3_2 $U a570 \/ ~c5_1 $U \/ ~c5_2 $U $V \/ ~ndr1_0 \/
% 0.66/0.83     ~ndr1_1 $U \/ c2_2 $U $V \/ c5_0
% 0.66/0.83  |- ~c2_0 \/ ~c4_2 $U a570 \/ ~c5_1 $U \/ ~c5_2 $U $V \/ ~ndr1_0 \/
% 0.66/0.83     ~ndr1_1 $U \/ c2_2 $U $V \/ c5_0
% 0.66/0.83  |- ~c3_1 $U \/ ~c3_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_2 $U $V \/
% 0.66/0.83     c2_2 a552 a553 \/ c4_1 $U \/ c4_2 $U $V
% 0.66/0.83  |- ~c3_1 $U \/ ~c3_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_2 $U $V \/
% 0.66/0.83     c1_2 a552 a553 \/ c4_1 $U \/ c4_2 $U $V
% 0.66/0.84  |- ~c1_2 $U $V \/ ~c2_0 \/ ~c5_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/
% 0.66/0.84     c4_1 $U \/ c4_2 $U $V \/ c5_1 $U \/ ndr1_1 a581
% 0.66/0.84  |- ~c1_2 $U $V \/ ~c2_0 \/ ~c5_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/
% 0.66/0.84     c3_1 a581 \/ c4_1 $U \/ c4_2 $U $V \/ c5_1 $U
% 0.66/0.84  |- ~c1_2 $U $V \/ ~c3_2 $U $V \/ ~c5_1 $U \/ ~ndr1_0 \/ ~ndr1_1 $U \/
% 0.66/0.84     c2_1 $U \/ c2_2 $U $V \/ c5_0 \/ c5_1 a574
% 0.66/0.84  |- ~c2_2 a552 a554 \/ ~c3_1 $U \/ ~c3_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/
% 0.66/0.84     c1_2 $U $V \/ c4_1 $U \/ c4_2 $U $V
% 0.66/0.84  |- ~c3_1 $U \/ ~c3_2 $U $V \/ ~c4_2 a552 a554 \/ ~ndr1_0 \/ ~ndr1_1 $U \/
% 0.66/0.84     c1_2 $U $V \/ c4_1 $U \/ c4_2 $U $V
% 0.66/0.84  |- ~c3_1 $U \/ ~c3_2 $U $V \/ ~c3_2 a552 a553 \/ ~ndr1_0 \/ ~ndr1_1 $U \/
% 0.66/0.84     c1_2 $U $V \/ c4_1 $U \/ c4_2 $U $V
% 0.66/0.84  |- ~c1_2 $V $W \/ ~c3_1 $U \/ ~c4_1 $V \/ ~ndr1_0 \/ ~ndr1_1 $V \/
% 0.66/0.84     ~ssSkP3 $U \/ c2_2 $U a580 \/ c5_1 $V \/ c5_2 $V $W
% 0.66/0.84  |- ~c1_2 $U $V \/ ~c2_0 \/ ~c5_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/
% 0.66/0.84     c4_1 $U \/ c4_2 $U $V \/ c5_1 $U \/ c5_2 a581 a582
% 0.66/0.84  |- ~c1_2 $U $V \/ ~c2_0 \/ ~c5_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/
% 0.66/0.84     c1_2 a581 a582 \/ c4_1 $U \/ c4_2 $U $V \/ c5_1 $U
% 0.66/0.84  |- ~c1_2 $U $V \/ ~c2_0 \/ ~c2_1 a581 \/ ~c5_2 $U $V \/ ~ndr1_0 \/
% 0.66/0.84     ~ndr1_1 $U \/ c4_1 $U \/ c4_2 $U $V \/ c5_1 $U
% 0.66/0.84  |- ~c1_1 a574 \/ ~c1_2 $U $V \/ ~c3_2 $U $V \/ ~c5_1 $U \/ ~ndr1_0 \/
% 0.66/0.84     ~ndr1_1 $U \/ c2_1 $U \/ c2_2 $U $V \/ c5_0
% 0.66/0.84  |- ~c2_2 a551 $V \/ ~c3_1 $U \/ ~c4_0 \/ ~c4_1 $U \/ ~ndr1_0 \/
% 0.66/0.84     ~ndr1_1 a551 \/ c4_2 a551 $V \/ c5_2 a551 $V
% 0.66/0.84  |- ~c2_2 $U $W \/ ~c3_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_2 $U $W \/
% 0.66/0.84     c2_2 $U $V \/ c3_2 $U a559 \/ c5_2 $U $V \/ ssSkC2
% 0.66/0.84  |- ~c2_2 $U $W \/ ~c3_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_2 $U $W \/
% 0.66/0.84     c2_2 $U $V \/ c4_2 $U a559 \/ c5_2 $U $V \/ ssSkC2
% 0.66/0.84  |- ~c3_0 \/ ~c5_1 $U \/ ~c5_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/ c1_1 $W \/
% 0.66/0.84     c3_2 $U $V \/ c4_1 $W \/ c5_1 $W \/ c5_2 $U a586
% 0.66/0.84  |- ~c1_2 $U a580 \/ ~c1_2 $V $W \/ ~c3_1 $U \/ ~c4_1 $V \/ ~ndr1_0 \/
% 0.66/0.84     ~ndr1_1 $V \/ ~ssSkP3 $U \/ c5_1 $V \/ c5_2 $V $W
% 0.66/0.84  |- ~c1_2 $U $V \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~c5_2 $U $V \/ ~ndr1_0 \/
% 0.66/0.84     ~ndr1_1 $U \/ c4_1 $U \/ c4_2 $U $V \/ c5_1 $U
% 0.66/0.84  |- ~c3_1 $U \/ ~c3_2 a551 $V \/ ~c4_0 \/ ~c4_1 $U \/ ~c4_2 a551 $V \/
% 0.66/0.84     ~ndr1_0 \/ ~ndr1_1 a551 \/ c1_2 a551 $V
% 0.66/0.84  |- ~c1_2 $U a559 \/ ~c2_2 $U $W \/ ~c3_2 $U $V \/ ~ndr1_0 \/ ~ndr1_1 $U \/
% 0.66/0.84     c1_2 $U $W \/ c2_2 $U $V \/ c5_2 $U $V \/ ssSkC2
% 0.66/0.84  |- ~c3_0 \/ ~c4_2 $U a586 \/ ~c5_1 $U \/ ~c5_2 $U $V \/ ~ndr1_0 \/
% 0.66/0.84     ~ndr1_1 $U \/ c1_1 $W \/ c3_2 $U $V \/ c4_1 $W \/ c5_1 $W
% 0.66/0.84  |- ~c1_2 $U a586 \/ ~c3_0 \/ ~c5_1 $U \/ ~c5_2 $U $V \/ ~ndr1_0 \/
% 0.66/0.84     ~ndr1_1 $U \/ c1_1 $W \/ c3_2 $U $V \/ c4_1 $W \/ c5_1 $W
% 0.66/0.84  |- ~c1_1 $V \/ ~c2_1 $U \/ ~c2_2 $V $W \/ ~c4_2 $V $W \/ ~c5_1 $U \/
% 0.66/0.84     ~ndr1_0 \/ ~ndr1_1 $V \/ c3_2 $V $W \/ c4_2 $V a566
% 0.66/0.84  |- ~c1_1 $V \/ ~c2_1 $U \/ ~c2_2 $V $W \/ ~c2_2 $V a566 \/ ~c4_2 $V $W \/
% 0.66/0.84     ~c5_1 $U \/ ~ndr1_0 \/ ~ndr1_1 $V \/ c3_2 $V $W
% 0.66/0.84  |- ~c1_1 $V \/ ~c2_1 $U \/ ~c2_2 $V $W \/ ~c3_2 $V a566 \/ ~c4_2 $V $W \/
% 0.66/0.84     ~c5_1 $U \/ ~ndr1_0 \/ ~ndr1_1 $V \/ c3_2 $V $W
% 0.66/0.84  |- ~c1_1 $V \/ ~c2_2 $V $W \/ ~c3_2 $V $W \/ ~c5_2 $U $X \/ ~ndr1_0 \/
% 0.66/0.84     ~ndr1_1 $U \/ ~ndr1_1 $V \/ ~ssSkC0 \/ ~ssSkP0 $U \/ c1_2 $U $X \/
% 0.66/0.84     c2_1 $V \/ c5_2 $U a549
% 0.66/0.84  |- ~c1_1 $V \/ ~c2_2 $V $W \/ ~c3_2 $V $W \/ ~c5_2 $U $X \/ ~ndr1_0 \/
% 0.66/0.84     ~ndr1_1 $U \/ ~ndr1_1 $V \/ ~ssSkC0 \/ ~ssSkP0 $U \/ c1_2 $U $X \/
% 0.66/0.84     c2_1 $V \/ c2_2 $U a549
% 0.66/0.84  |- ~c1_1 $V \/ ~c2_2 $V $W \/ ~c3_2 $V $W \/ ~c4_2 $U a549 \/
% 0.66/0.84     ~c5_2 $U $X \/ ~ndr1_0 \/ ~ndr1_1 $U \/ ~ndr1_1 $V \/ ~ssSkC0 \/
% 0.66/0.84     ~ssSkP0 $U \/ c1_2 $U $X \/ c2_1 $V
% 0.66/0.84  |- ~c1_2 $U $V \/ ~c1_2 a574 $W \/ ~c3_2 $U $V \/ ~c5_1 $U \/ ~ndr1_0 \/
% 0.66/0.84     ~ndr1_1 $U \/ ~ndr1_1 a574 \/ c2_1 $U \/ c2_2 $U $V \/ c3_2 a574 $W \/
% 0.66/0.84     c4_2 a574 $W \/ c5_0
% 0.66/0.84  |- ~c3_1 a552 \/ ~c3_2 a552 a553 \/ ~ndr1_0 \/ ~ndr1_1 a552 \/
% 0.66/0.84     c1_2 a552 a553 \/ c4_1 a552 \/ c4_2 a552 a553
% 0.66/0.84  |- ~c1_2 $V a580 \/ ~c3_1 $V \/ ~c4_1 $V \/ ~ndr1_0 \/ ~ndr1_1 $V \/
% 0.66/0.84     ~ssSkP3 $V \/ c5_1 $V \/ c5_2 $V a580
% 0.66/0.84  |- ~c2_0 \/ c1_0
% 0.66/0.84  |- c4_0 \/ ndr1_0
% 0.66/0.84  |- c5_0 \/ ndr1_0
% 0.66/0.84  |- c1_0 \/ c3_0 \/ ndr1_0
% 0.66/0.84  |- c1_0 \/ c3_0 \/ c5_1 a578
% 0.66/0.84  |- ~ndr1_0 \/ c2_0 \/ ssSkC0
% 0.66/0.84  |- ~ndr1_0 \/ c2_0 \/ ssSkC5
% 0.66/0.84  |- c1_0 \/ c2_0 \/ c3_0 \/ ssSkC0
% 0.66/0.84  |- c2_0 \/ c5_0 \/ ssSkC0
% 0.66/0.84  |- c2_0 \/ c4_0 \/ ssSkC0
% 0.66/0.84  |- c1_0 \/ c2_0 \/ c3_0 \/ ssSkC5
% 0.66/0.84  |- c2_0 \/ c5_0 \/ ssSkC5
% 0.66/0.84  |- c2_0 \/ c4_0 \/ ssSkC5
% 0.66/0.84  |- ~ndr1_0 \/ c3_1 $_15 \/ ndr1_1 $_15 \/ ssSkC4
% 0.66/0.84  |- c1_0 \/ c3_0 \/ c3_1 $_16 \/ ndr1_1 $_16 \/ ssSkC4
% 0.66/0.84  |- c3_1 $_16 \/ c5_0 \/ ndr1_1 $_16 \/ ssSkC4
% 0.66/0.84  |- c3_1 $_16 \/ c4_0 \/ ndr1_1 $_16 \/ ssSkC4
% 0.66/0.84  |- ~ndr1_0 \/ c2_2 a546 a576 \/ c3_1 a546 \/ ssSkC0 \/ ssSkC6
% 0.66/0.84  |- ~ndr1_0 \/ c2_2 a567 a576 \/ c3_1 a567 \/ ssSkC5 \/ ssSkC6
% 0.66/0.84  |- c1_0 \/ c2_2 a546 a576 \/ c3_0 \/ c3_1 a546 \/ ssSkC0 \/ ssSkC6
% 0.66/0.84  |- c2_2 a546 a576 \/ c3_1 a546 \/ c5_0 \/ ssSkC0 \/ ssSkC6
% 0.66/0.84  |- c2_2 a546 a576 \/ c3_1 a546 \/ c4_0 \/ ssSkC0 \/ ssSkC6
% 0.66/0.84  |- c1_0 \/ c2_2 a567 a576 \/ c3_0 \/ c3_1 a567 \/ ssSkC5 \/ ssSkC6
% 0.66/0.84  |- c2_2 a567 a576 \/ c3_1 a567 \/ c5_0 \/ ssSkC5 \/ ssSkC6
% 0.66/0.84  |- c2_2 a567 a576 \/ c3_1 a567 \/ c4_0 \/ ssSkC5 \/ ssSkC6
% 0.66/0.84  |- ~ndr1_1 a569 \/ ~ssSkC5 \/ c3_2 a569 a548 \/ c5_0 \/ ssSkP0 a569
% 0.66/0.84  |- ~ndr1_1 a569 \/ ~ssSkC5 \/ c3_2 a569 a562 \/ c5_0 \/ ssSkP2 a569
% 0.66/0.84  |- ~ssSkC5 \/ c3_1 a569 \/ c3_2 a569 a548 \/ c5_0 \/ ssSkC4 \/ ssSkP0 a569
% 0.66/0.84  |- ~ssSkC5 \/ c3_1 a569 \/ c3_2 a569 a562 \/ c5_0 \/ ssSkC4 \/ ssSkP2 a569
% 0.66/0.84  |- c2_0 \/ c3_1 a569 \/ c3_2 a569 a548 \/ c5_0 \/ ssSkC4 \/ ssSkP0 a569
% 0.66/0.84  |- c2_0 \/ c3_1 a569 \/ c3_2 a569 a562 \/ c5_0 \/ ssSkC4 \/ ssSkP2 a569
% 0.66/0.84  |- ~c4_0 \/ ~ndr1_1 a578 \/ c3_0 \/ c4_2 a578 a548 \/ ssSkP0 a578
% 0.66/0.84  |- ~c4_0 \/ ~ndr1_1 a578 \/ c3_0 \/ c4_2 a578 a562 \/ ssSkP2 a578
% 0.66/0.84  |- ~c4_0 \/ c3_0 \/ c3_1 a578 \/ c4_2 a578 a548 \/ c5_0 \/ ssSkC4 \/
% 0.66/0.84     ssSkP0 a578
% 0.66/0.84  |- ~c4_0 \/ c3_0 \/ c3_1 a578 \/ c4_2 a578 a562 \/ c5_0 \/ ssSkC4 \/
% 0.66/0.84     ssSkP2 a578
% 0.66/0.84  |- c1_0 \/ c3_0 \/ c3_1 a578 \/ c4_2 a578 a548 \/ ssSkC4 \/ ssSkP0 a578
% 0.66/0.84  |- c1_0 \/ c3_0 \/ c3_1 a578 \/ ssSkC4 \/ ssSkP2 a578
% 0.66/0.84  |- c1_0 \/ c3_0 \/ c3_1 a578 \/ c4_2 a578 a563 \/ ssSkC4
% 0.66/0.84  |- c1_0 \/ c1_2 a578 a563 \/ c3_0 \/ c3_1 a578 \/ ssSkC4
% 0.66/0.84  |- ~c1_2 a565 a562 \/ ~c3_0 \/ ~c5_0 \/ ~ndr1_1 a565 \/ ssSkP2 a565
% 0.66/0.84  |- ~ndr1_0 \/ ~ssSkC1 \/ c2_1 $_31 \/ c5_0 \/ ndr1_1 $_31
% 0.66/0.84  |- ~c3_0 \/ ~ndr1_0 \/ c1_0 \/ c1_1 a583 \/ c4_1 a583 \/ ssSkC7
% 0.66/0.84  |- ~c3_0 \/ c1_0 \/ c1_1 a583 \/ c4_1 a583 \/ c5_0 \/ ssSkC7
% 0.66/0.84  |- ~c2_2 a561 a548 \/ ~c4_2 a561 a548 \/ ~ndr1_1 a561 \/ ssSkC3 \/
% 0.66/0.84     ssSkP0 a561
% 0.66/0.84  |- ~c1_1 $_68 \/ ~c4_2 $_68 a548 \/ ~ndr1_0 \/ ~ndr1_1 $_68 \/
% 0.66/0.84     c1_2 $_68 a548 \/ c2_1 $_68 \/ c5_0 \/ ssSkP0 $_68
% 0.66/0.84  |- ~c1_1 a578 \/ ~ndr1_0 \/ c1_0 \/ c1_2 a578 a548 \/ c2_1 a578 \/ c3_0 \/
% 0.66/0.84     c3_1 a578 \/ c5_0 \/ ssSkC4 \/ ssSkP0 a578
% 0.66/0.84  |- ~c3_0 \/ ~c4_1 $_71 \/ ~ndr1_0 \/ ~ndr1_1 $_71 \/ c1_2 $_71 a548 \/
% 0.66/0.84     c3_2 $_71 a548 \/ c5_1 $_71 \/ ssSkP0 $_71
% 0.66/0.84  |- ~c3_0 \/ ~c4_1 $_71 \/ ~ndr1_0 \/ ~ndr1_1 $_71 \/ c1_2 $_71 a562 \/
% 0.66/0.84     c3_2 $_71 a562 \/ c5_1 $_71 \/ ssSkP2 $_71
% 0.66/0.84  |- ~c3_0 \/ ~c4_1 a546 \/ ~ndr1_0 \/ c1_2 a546 a547 \/ c3_2 a546 a547 \/
% 0.66/0.84     c5_1 a546 \/ ssSkC0
% 0.66/0.84  |- ~c3_0 \/ ~c4_1 a546 \/ ~ndr1_0 \/ c1_2 a546 a576 \/ c3_1 a546 \/
% 0.66/0.84     c3_2 a546 a576 \/ c4_0 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC6
% 0.66/0.84  |- ~c3_0 \/ ~c4_1 a546 \/ ~ndr1_0 \/ c1_2 a546 a576 \/ c3_1 a546 \/
% 0.66/0.84     c3_2 a546 a576 \/ c5_0 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC6
% 0.66/0.84  |- ~c3_0 \/ ~c4_1 a567 \/ ~ndr1_0 \/ c1_2 a567 a576 \/ c3_1 a567 \/
% 0.66/0.84     c3_2 a567 a576 \/ c4_0 \/ c5_1 a567 \/ ssSkC5 \/ ssSkC6
% 0.66/0.84  |- ~c3_0 \/ ~c4_1 a567 \/ ~ndr1_0 \/ c1_2 a567 a576 \/ c3_1 a567 \/
% 0.66/0.84     c3_2 a567 a576 \/ c5_0 \/ c5_1 a567 \/ ssSkC5 \/ ssSkC6
% 0.66/0.84  |- ~c3_0 \/ ~c4_1 a546 \/ ~ndr1_0 \/ c1_2 a546 a548 \/ c3_2 a546 a548 \/
% 0.66/0.84     c5_1 a546 \/ ssSkC0 \/ ssSkP0 a546
% 0.66/0.84  |- ~c3_0 \/ ~c4_1 a567 \/ ~ndr1_0 \/ c1_2 a567 a548 \/ c3_2 a567 a548 \/
% 0.66/0.84     c5_1 a567 \/ ssSkC5 \/ ssSkP0 a567
% 0.66/0.84  |- ~c3_0 \/ ~c4_1 $_73 \/ ~ndr1_0 \/ c1_2 $_73 a548 \/ c3_1 $_73 \/
% 0.66/0.84     c3_2 $_73 a548 \/ c4_0 \/ c5_1 $_73 \/ ssSkC4 \/ ssSkP0 $_73
% 0.66/0.84  |- ~c3_0 \/ ~c4_1 $_73 \/ ~ndr1_0 \/ c1_2 $_73 a548 \/ c3_1 $_73 \/
% 0.66/0.84     c3_2 $_73 a548 \/ c5_0 \/ c5_1 $_73 \/ ssSkC4 \/ ssSkP0 $_73
% 0.66/0.84  |- ~c3_0 \/ ~c4_1 a546 \/ ~ndr1_0 \/ c1_2 a546 a562 \/ c3_2 a546 a562 \/
% 0.66/0.84     c5_1 a546 \/ ssSkC0 \/ ssSkP2 a546
% 0.66/0.84  |- ~c3_0 \/ ~c4_1 a567 \/ ~ndr1_0 \/ c1_2 a567 a562 \/ c3_2 a567 a562 \/
% 0.66/0.84     c5_1 a567 \/ ssSkC5 \/ ssSkP2 a567
% 0.66/0.84  |- ~c3_0 \/ ~c4_1 $_74 \/ ~ndr1_0 \/ c1_2 $_74 a562 \/ c3_1 $_74 \/
% 0.66/0.84     c3_2 $_74 a562 \/ c4_0 \/ c5_1 $_74 \/ ssSkC4 \/ ssSkP2 $_74
% 0.66/0.84  |- ~c3_0 \/ ~c4_1 $_74 \/ ~ndr1_0 \/ c1_2 $_74 a562 \/ c3_1 $_74 \/
% 0.66/0.84     c3_2 $_74 a562 \/ c5_0 \/ c5_1 $_74 \/ ssSkC4 \/ ssSkP2 $_74
% 0.66/0.84  |- ~c3_1 $_79 \/ ~ndr1_0 \/ ~ndr1_1 $_79 \/ c1_2 $_79 a579 \/ c4_1 $_79 \/
% 0.66/0.84     c4_2 $_79 a579 \/ ndr1_1 a552 \/ ssSkP3 $_79
% 0.66/0.84  |- ~c3_1 a546 \/ ~ndr1_0 \/ c1_2 a546 a579 \/ c4_1 a546 \/
% 0.66/0.84     c4_2 a546 a579 \/ ndr1_1 a552 \/ ssSkC0 \/ ssSkP3 a546
% 0.66/0.84  |- ~c3_1 a567 \/ ~ndr1_0 \/ c1_2 a567 a579 \/ c4_1 a567 \/
% 0.66/0.84     c4_2 a567 a579 \/ ndr1_1 a552 \/ ssSkC5 \/ ssSkP3 a567
% 0.66/0.84  |- ~c3_1 $_82 \/ ~ndr1_0 \/ ~ndr1_1 $_82 \/ c1_2 $_82 a579 \/
% 0.66/0.84     c2_2 a552 a553 \/ c4_1 $_82 \/ c4_2 $_82 a579 \/ ssSkP3 $_82
% 0.66/0.84  |- ~c3_1 a546 \/ ~ndr1_0 \/ c1_2 a546 a579 \/ c2_2 a552 a553 \/
% 0.66/0.84     c4_1 a546 \/ c4_2 a546 a579 \/ ssSkC0 \/ ssSkP3 a546
% 0.66/0.84  |- ~c3_1 a567 \/ ~ndr1_0 \/ c1_2 a567 a579 \/ c2_2 a552 a553 \/
% 0.66/0.84     c4_1 a567 \/ c4_2 a567 a579 \/ ssSkC5 \/ ssSkP3 a567
% 0.66/0.84  |- ~c3_1 $_85 \/ ~ndr1_0 \/ ~ndr1_1 $_85 \/ c1_2 $_85 a579 \/
% 0.66/0.84     c1_2 a552 a553 \/ c4_1 $_85 \/ c4_2 $_85 a579 \/ ssSkP3 $_85
% 0.66/0.84  |- ~c3_1 a546 \/ ~ndr1_0 \/ c1_2 a546 a579 \/ c1_2 a552 a553 \/
% 0.66/0.84     c4_1 a546 \/ c4_2 a546 a579 \/ ssSkC0 \/ ssSkP3 a546
% 0.66/0.84  |- ~c3_1 a567 \/ ~ndr1_0 \/ c1_2 a552 a553 \/ c1_2 a567 a579 \/
% 0.66/0.84     c4_1 a567 \/ c4_2 a567 a579 \/ ssSkC5 \/ ssSkP3 a567
% 0.66/0.84  |- ~c2_2 a552 a554 \/ ~c3_1 $_88 \/ ~ndr1_0 \/ ~ndr1_1 $_88 \/
% 0.66/0.84     c1_2 $_88 a579 \/ c4_1 $_88 \/ c4_2 $_88 a579 \/ ssSkP3 $_88
% 0.66/0.84  |- ~c3_1 $_91 \/ ~c4_2 a552 a554 \/ ~ndr1_0 \/ ~ndr1_1 $_91 \/
% 0.66/0.84     c1_2 $_91 a579 \/ c4_1 $_91 \/ c4_2 $_91 a579 \/ ssSkP3 $_91
% 0.66/0.84  |- ~c3_1 $_94 \/ ~c3_2 a552 a553 \/ ~ndr1_0 \/ ~ndr1_1 $_94 \/
% 0.66/0.84     c1_2 $_94 a579 \/ c4_1 $_94 \/ c4_2 $_94 a579 \/ ssSkP3 $_94
% 0.66/0.84  |- ~c1_2 a546 a547 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c4_1 a546 \/
% 0.66/0.84     c4_2 a546 a547 \/ c5_1 a546 \/ ndr1_1 a581 \/ ssSkC0
% 0.66/0.84  |- ~c1_2 $_97 a562 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_97 \/ c4_1 $_97 \/
% 0.66/0.84     c4_2 $_97 a562 \/ c5_1 $_97 \/ ndr1_1 a581 \/ ssSkP2 $_97
% 0.66/0.84  |- ~c1_2 a546 a547 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c3_1 a581 \/
% 0.66/0.84     c4_1 a546 \/ c4_2 a546 a547 \/ c5_1 a546 \/ ssSkC0
% 0.66/0.84  |- ~c1_2 $_100 a562 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_100 \/ c3_1 a581 \/
% 0.66/0.84     c4_1 $_100 \/ c4_2 $_100 a562 \/ c5_1 $_100 \/ ssSkP2 $_100
% 0.66/0.84  |- ~c1_2 $_103 a579 \/ ~c5_1 $_103 \/ ~ndr1_0 \/ ~ndr1_1 $_103 \/
% 0.66/0.84     c2_1 $_103 \/ c2_2 $_103 a579 \/ c5_0 \/ c5_1 a574 \/ ssSkP3 $_103
% 0.66/0.84  |- ~c1_2 a546 a547 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.66/0.84     c4_1 a546 \/ c4_2 a546 a547 \/ c5_1 a546 \/ ssSkC0
% 0.66/0.84  |- ~c1_2 $_106 a562 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 $_106 \/
% 0.66/0.84     c4_1 $_106 \/ c4_2 $_106 a562 \/ c5_1 $_106 \/ ssSkP2 $_106
% 0.66/0.84  |- ~c1_1 a574 \/ ~c1_2 $_109 a579 \/ ~c5_1 $_109 \/ ~ndr1_0 \/
% 0.66/0.84     ~ndr1_1 $_109 \/ c2_1 $_109 \/ c2_2 $_109 a579 \/ c5_0 \/ ssSkP3 $_109
% 0.66/0.84  |- ~c1_2 a546 a547 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c4_1 a546 \/
% 0.66/0.84     c4_2 a546 a547 \/ c5_1 a546 \/ c5_2 a581 a582 \/ ssSkC0
% 0.66/0.84  |- ~c1_2 $_112 a562 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_112 \/ c4_1 $_112 \/
% 0.66/0.84     c4_2 $_112 a562 \/ c5_1 $_112 \/ c5_2 a581 a582 \/ ssSkP2 $_112
% 0.66/0.84  |- ~c1_2 a546 a547 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a581 a582 \/
% 0.66/0.84     c4_1 a546 \/ c4_2 a546 a547 \/ c5_1 a546 \/ ssSkC0
% 0.66/0.84  |- ~c1_2 $_115 a562 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_115 \/
% 0.66/0.84     c1_2 a581 a582 \/ c4_1 $_115 \/ c4_2 $_115 a562 \/ c5_1 $_115 \/
% 0.66/0.84     ssSkP2 $_115
% 0.66/0.84  |- ~c1_2 a546 a547 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.66/0.84     ~ndr1_1 a546 \/ c4_1 a546 \/ c4_2 a546 a547 \/ c5_1 a546 \/ ssSkC0
% 0.66/0.84  |- ~c1_2 $_118 a562 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.66/0.84     ~ndr1_1 $_118 \/ c4_1 $_118 \/ c4_2 $_118 a562 \/ c5_1 $_118 \/
% 0.66/0.84     ssSkP2 $_118
% 0.66/0.84  |- ~c1_2 $_126 $_127 \/ ~c3_1 $_125 \/ ~c4_1 $_126 \/ ~ndr1_0 \/
% 0.66/0.84     ~ndr1_1 $_126 \/ c5_1 $_126 \/ c5_2 $_126 $_127 \/ ndr1_1 $_125
% 0.66/0.84  |- ~c3_1 $_128 \/ ~c4_1 $_129 \/ ~ndr1_0 \/ ~ndr1_1 $_129 \/ c5_1 $_129 \/
% 0.66/0.84     c5_2 $_129 a557 \/ ndr1_1 $_128 \/ ssSkP1 $_129
% 0.66/0.84  |- ~c3_1 $_130 \/ ~c4_1 a546 \/ ~ndr1_0 \/ c5_1 a546 \/ c5_2 a546 a557 \/
% 0.66/0.84     ndr1_1 $_130 \/ ssSkC0 \/ ssSkP1 a546
% 0.66/0.84  |- ~c3_1 $_130 \/ ~c4_1 a567 \/ ~ndr1_0 \/ c5_1 a567 \/ c5_2 a567 a557 \/
% 0.66/0.84     ndr1_1 $_130 \/ ssSkC5 \/ ssSkP1 a567
% 0.66/0.84  |- ~c3_1 $_137 \/ ~c4_1 $_138 \/ ~ndr1_0 \/ ~ndr1_1 $_138 \/
% 0.66/0.84     ~ssSkP3 $_137 \/ c2_2 $_137 a580 \/ c5_1 $_138 \/ c5_2 $_138 a557 \/
% 0.66/0.84     ssSkP1 $_138
% 0.66/0.84  |- ~c3_1 $_140 \/ ~c4_1 $_141 \/ ~ndr1_0 \/ ~ssSkP3 $_140 \/ c1_0 \/
% 0.66/0.84     c2_2 $_140 a580 \/ c3_0 \/ c3_1 $_141 \/ c5_1 $_141 \/
% 0.66/0.84     c5_2 $_141 a557 \/ ssSkC4 \/ ssSkP1 $_141
% 0.66/0.84  |- ~c3_1 $_140 \/ ~c4_1 $_141 \/ ~ndr1_0 \/ ~ssSkP3 $_140 \/
% 0.66/0.84     c2_2 $_140 a580 \/ c3_1 $_141 \/ c4_0 \/ c5_1 $_141 \/
% 0.66/0.84     c5_2 $_141 a557 \/ ssSkC4 \/ ssSkP1 $_141
% 0.66/0.84  |- ~c3_1 $_140 \/ ~c4_1 $_141 \/ ~ndr1_0 \/ ~ssSkP3 $_140 \/
% 0.66/0.84     c2_2 $_140 a580 \/ c3_1 $_141 \/ c5_0 \/ c5_1 $_141 \/
% 0.66/0.84     c5_2 $_141 a557 \/ ssSkC4 \/ ssSkP1 $_141
% 0.66/0.84  |- ~c1_2 $_142 a580 \/ ~c3_1 $_142 \/ ~c4_1 $_143 \/ ~ndr1_0 \/
% 0.66/0.84     ~ndr1_1 $_143 \/ ~ssSkP3 $_142 \/ c5_1 $_143 \/ c5_2 $_143 a557 \/
% 0.66/0.84     ssSkP1 $_143
% 0.66/0.84  |- ~c1_2 $_145 a580 \/ ~c3_1 $_145 \/ ~c4_1 $_146 \/ ~ndr1_0 \/
% 0.66/0.84     ~ssSkP3 $_145 \/ c1_0 \/ c3_0 \/ c3_1 $_146 \/ c5_1 $_146 \/
% 0.66/0.84     c5_2 $_146 a557 \/ ssSkC4 \/ ssSkP1 $_146
% 0.66/0.84  |- ~c1_2 $_145 a580 \/ ~c3_1 $_145 \/ ~c4_1 $_146 \/ ~ndr1_0 \/
% 0.66/0.84     ~ssSkP3 $_145 \/ c3_1 $_146 \/ c4_0 \/ c5_1 $_146 \/ c5_2 $_146 a557 \/
% 0.66/0.84     ssSkC4 \/ ssSkP1 $_146
% 0.66/0.84  |- ~c1_2 $_145 a580 \/ ~c3_1 $_145 \/ ~c4_1 $_146 \/ ~ndr1_0 \/
% 0.66/0.84     ~ssSkP3 $_145 \/ c3_1 $_146 \/ c5_0 \/ c5_1 $_146 \/ c5_2 $_146 a557 \/
% 0.66/0.84     ssSkC4 \/ ssSkP1 $_146
% 0.66/0.84  |- ~c1_1 a567 \/ ~c2_1 $_147 \/ ~c2_2 a567 a568 \/ ~c5_1 $_147 \/
% 0.66/0.84     ~ndr1_0 \/ ~ndr1_1 a567 \/ c3_2 a567 a568 \/ c4_2 a567 a566 \/ ssSkC5
% 0.66/0.84  |- ~c1_1 a578 \/ ~c2_1 $_147 \/ ~c2_2 a578 a563 \/ ~c5_1 $_147 \/
% 0.66/0.84     ~ndr1_0 \/ ~ndr1_1 a578 \/ c1_0 \/ c3_0 \/ c3_1 a578 \/
% 0.66/0.84     c3_2 a578 a563 \/ c4_2 a578 a566 \/ ssSkC4
% 0.66/0.85  |- ~c1_1 a567 \/ ~c2_1 $_152 \/ ~c2_2 a567 a566 \/ ~c2_2 a567 a568 \/
% 0.66/0.85     ~c5_1 $_152 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c3_2 a567 a568 \/ ssSkC5
% 0.66/0.85  |- ~c1_1 a578 \/ ~c2_1 $_152 \/ ~c2_2 a578 a548 \/ ~c2_2 a578 a566 \/
% 0.66/0.85     ~c5_1 $_152 \/ ~ndr1_0 \/ ~ndr1_1 a578 \/ c1_0 \/ c3_0 \/ c3_1 a578 \/
% 0.66/0.85     c3_2 a578 a548 \/ ssSkC4 \/ ssSkP0 a578
% 0.66/0.85  |- ~c1_1 a578 \/ ~c2_1 $_152 \/ ~c2_2 a578 a563 \/ ~c2_2 a578 a566 \/
% 0.66/0.85     ~c5_1 $_152 \/ ~ndr1_0 \/ ~ndr1_1 a578 \/ c1_0 \/ c3_0 \/ c3_1 a578 \/
% 0.66/0.85     c3_2 a578 a563 \/ ssSkC4
% 0.66/0.85  |- ~c1_1 a567 \/ ~c2_1 $_157 \/ ~c2_2 a567 a568 \/ ~c3_2 a567 a566 \/
% 0.66/0.85     ~c5_1 $_157 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c3_2 a567 a568 \/ ssSkC5
% 0.66/0.85  |- ~c1_1 a578 \/ ~c2_1 $_157 \/ ~c2_2 a578 a548 \/ ~c3_2 a578 a566 \/
% 0.66/0.85     ~c5_1 $_157 \/ ~ndr1_0 \/ ~ndr1_1 a578 \/ c1_0 \/ c3_0 \/ c3_1 a578 \/
% 0.66/0.85     c3_2 a578 a548 \/ ssSkC4 \/ ssSkP0 a578
% 0.66/0.85  |- ~c1_1 a578 \/ ~c2_1 $_157 \/ ~c2_2 a578 a563 \/ ~c3_2 a578 a566 \/
% 0.66/0.85     ~c5_1 $_157 \/ ~ndr1_0 \/ ~ndr1_1 a578 \/ c1_0 \/ c3_0 \/ c3_1 a578 \/
% 0.66/0.85     c3_2 a578 a563 \/ ssSkC4
% 0.66/0.85  |- ~c2_2 $_162 $_164 \/ ~ndr1_0 \/ ~ndr1_1 $_162 \/ c1_2 $_162 $_164 \/
% 0.66/0.85     c2_2 $_162 a579 \/ c3_2 $_162 a559 \/ c5_2 $_162 a579 \/ ssSkC2 \/
% 0.66/0.85     ssSkP3 $_162
% 0.66/0.85  |- ~ndr1_0 \/ ~ndr1_1 $_165 \/ c1_2 $_165 a548 \/ c2_2 $_165 a579 \/
% 0.66/0.85     c3_2 $_165 a559 \/ c5_2 $_165 a579 \/ ssSkC2 \/ ssSkP0 $_165 \/
% 0.66/0.85     ssSkP3 $_165
% 0.66/0.85  |- ~ndr1_0 \/ ~ndr1_1 $_165 \/ c1_2 $_165 a562 \/ c2_2 $_165 a579 \/
% 0.66/0.85     c3_2 $_165 a559 \/ c5_2 $_165 a579 \/ ssSkC2 \/ ssSkP2 $_165 \/
% 0.66/0.85     ssSkP3 $_165
% 0.66/0.85  |- ~ndr1_0 \/ c1_2 a546 a547 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/
% 0.66/0.85     c5_2 a546 a579 \/ ssSkC0 \/ ssSkC2 \/ ssSkP3 a546
% 0.66/0.85  |- c1_0 \/ c1_2 a546 a547 \/ c2_2 a546 a579 \/ c3_0 \/ c3_2 a546 a559 \/
% 0.66/0.85     c5_2 a546 a579 \/ ssSkC0 \/ ssSkC2 \/ ssSkP3 a546
% 0.66/0.85  |- c1_2 a546 a547 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/ c5_0 \/
% 0.66/0.85     c5_2 a546 a579 \/ ssSkC0 \/ ssSkC2 \/ ssSkP3 a546
% 0.66/0.85  |- c1_2 a546 a547 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/ c4_0 \/
% 0.66/0.85     c5_2 a546 a579 \/ ssSkC0 \/ ssSkC2 \/ ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.66/0.85     ~ndr1_1 a546 \/ c1_2 a546 a547 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/
% 0.66/0.85     c4_1 a546 \/ c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.66/0.85     ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a547 \/
% 0.66/0.85     c1_2 a581 a582 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/ c4_1 a546 \/
% 0.66/0.85     c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/ ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a547 \/
% 0.66/0.85     c2_2 a546 a579 \/ c3_2 a546 a559 \/ c4_1 a546 \/ c4_2 a546 a579 \/
% 0.66/0.85     c5_0 \/ c5_1 a546 \/ c5_2 a581 a582 \/ ssSkC0 \/ ssSkC2 \/ ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.66/0.85     c1_2 a546 a547 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/ c4_1 a546 \/
% 0.66/0.85     c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/ ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a547 \/
% 0.66/0.85     c2_2 a546 a579 \/ c3_1 a581 \/ c3_2 a546 a559 \/ c4_1 a546 \/
% 0.66/0.85     c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/ ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a547 \/
% 0.66/0.85     c2_2 a546 a579 \/ c3_2 a546 a559 \/ c4_1 a546 \/ c4_2 a546 a579 \/
% 0.66/0.85     c5_0 \/ c5_1 a546 \/ ndr1_1 a581 \/ ssSkC0 \/ ssSkC2 \/ ssSkP3 a546
% 0.66/0.85  |- ~c2_0 \/ ~c4_2 a546 a570 \/ ~c5_1 a546 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.66/0.85     c1_2 a546 a547 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/ c5_0 \/ ssSkC0 \/
% 0.66/0.85     ssSkC2 \/ ssSkP3 a546
% 0.66/0.85  |- ~c2_0 \/ ~c3_2 a546 a570 \/ ~c5_1 a546 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.66/0.85     c1_2 a546 a547 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/ c5_0 \/ ssSkC0 \/
% 0.66/0.85     ssSkC2 \/ ssSkP3 a546
% 0.66/0.85  |- ~c2_0 \/ ~c2_2 a546 a570 \/ ~c5_1 a546 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.66/0.85     c1_2 a546 a547 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/ c5_0 \/ ssSkC0 \/
% 0.66/0.85     ssSkC2 \/ ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.66/0.85     ~ndr1_1 a546 \/ c1_2 a546 a547 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/
% 0.66/0.85     c4_0 \/ c4_1 a546 \/ c4_2 a546 a579 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.66/0.85     ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a547 \/
% 0.66/0.85     c1_2 a581 a582 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/ c4_0 \/
% 0.66/0.85     c4_1 a546 \/ c4_2 a546 a579 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.66/0.85     ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a547 \/
% 0.66/0.85     c2_2 a546 a579 \/ c3_2 a546 a559 \/ c4_0 \/ c4_1 a546 \/
% 0.66/0.85     c4_2 a546 a579 \/ c5_1 a546 \/ c5_2 a581 a582 \/ ssSkC0 \/ ssSkC2 \/
% 0.66/0.85     ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.66/0.85     c1_2 a546 a547 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/ c4_0 \/
% 0.66/0.85     c4_1 a546 \/ c4_2 a546 a579 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.66/0.85     ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a547 \/
% 0.66/0.85     c2_2 a546 a579 \/ c3_1 a581 \/ c3_2 a546 a559 \/ c4_0 \/ c4_1 a546 \/
% 0.66/0.85     c4_2 a546 a579 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/ ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a547 \/
% 0.66/0.85     c2_2 a546 a579 \/ c3_2 a546 a559 \/ c4_0 \/ c4_1 a546 \/
% 0.66/0.85     c4_2 a546 a579 \/ c5_1 a546 \/ ndr1_1 a581 \/ ssSkC0 \/ ssSkC2 \/
% 0.66/0.85     ssSkP3 a546
% 0.66/0.85  |- c1_2 a546 a576 \/ c2_2 a546 a579 \/ c3_1 a546 \/ c3_2 a546 a559 \/
% 0.66/0.85     c4_0 \/ c5_2 a546 a579 \/ ssSkC0 \/ ssSkC2 \/ ssSkC6 \/ ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.66/0.85     ~ndr1_1 a546 \/ c1_2 a546 a576 \/ c2_2 a546 a579 \/ c3_1 a546 \/
% 0.66/0.85     c3_2 a546 a559 \/ c4_0 \/ c4_1 a546 \/ c4_2 a546 a579 \/ c5_1 a546 \/
% 0.66/0.85     ssSkC0 \/ ssSkC2 \/ ssSkC6 \/ ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a576 \/
% 0.66/0.85     c1_2 a581 a582 \/ c2_2 a546 a579 \/ c3_1 a546 \/ c3_2 a546 a559 \/
% 0.66/0.85     c4_0 \/ c4_1 a546 \/ c4_2 a546 a579 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.66/0.85     ssSkC6 \/ ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a576 \/
% 0.66/0.85     c2_2 a546 a579 \/ c3_1 a546 \/ c3_2 a546 a559 \/ c4_0 \/ c4_1 a546 \/
% 0.66/0.85     c4_2 a546 a579 \/ c5_1 a546 \/ c5_2 a581 a582 \/ ssSkC0 \/ ssSkC2 \/
% 0.66/0.85     ssSkC6 \/ ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.66/0.85     c1_2 a546 a576 \/ c2_2 a546 a579 \/ c3_1 a546 \/ c3_2 a546 a559 \/
% 0.66/0.85     c4_0 \/ c4_1 a546 \/ c4_2 a546 a579 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.66/0.85     ssSkC6 \/ ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a576 \/
% 0.66/0.85     c2_2 a546 a579 \/ c3_1 a546 \/ c3_1 a581 \/ c3_2 a546 a559 \/ c4_0 \/
% 0.66/0.85     c4_1 a546 \/ c4_2 a546 a579 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.66/0.85     ssSkC6 \/ ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a576 \/
% 0.66/0.85     c2_2 a546 a579 \/ c3_1 a546 \/ c3_2 a546 a559 \/ c4_0 \/ c4_1 a546 \/
% 0.66/0.85     c4_2 a546 a579 \/ c5_1 a546 \/ ndr1_1 a581 \/ ssSkC0 \/ ssSkC2 \/
% 0.66/0.85     ssSkC6 \/ ssSkP3 a546
% 0.66/0.85  |- c1_2 a546 a576 \/ c2_2 a546 a579 \/ c3_1 a546 \/ c3_2 a546 a559 \/
% 0.66/0.85     c5_0 \/ c5_2 a546 a579 \/ ssSkC0 \/ ssSkC2 \/ ssSkC6 \/ ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.66/0.85     ~ndr1_1 a546 \/ c1_2 a546 a576 \/ c2_2 a546 a579 \/ c3_1 a546 \/
% 0.66/0.85     c3_2 a546 a559 \/ c4_1 a546 \/ c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/
% 0.66/0.85     ssSkC0 \/ ssSkC2 \/ ssSkC6 \/ ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a576 \/
% 0.66/0.85     c1_2 a581 a582 \/ c2_2 a546 a579 \/ c3_1 a546 \/ c3_2 a546 a559 \/
% 0.66/0.85     c4_1 a546 \/ c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.66/0.85     ssSkC6 \/ ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a576 \/
% 0.66/0.85     c2_2 a546 a579 \/ c3_1 a546 \/ c3_2 a546 a559 \/ c4_1 a546 \/
% 0.66/0.85     c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/ c5_2 a581 a582 \/ ssSkC0 \/
% 0.66/0.85     ssSkC2 \/ ssSkC6 \/ ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.66/0.85     c1_2 a546 a576 \/ c2_2 a546 a579 \/ c3_1 a546 \/ c3_2 a546 a559 \/
% 0.66/0.85     c4_1 a546 \/ c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.66/0.85     ssSkC6 \/ ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a576 \/
% 0.66/0.85     c2_2 a546 a579 \/ c3_1 a546 \/ c3_1 a581 \/ c3_2 a546 a559 \/
% 0.66/0.85     c4_1 a546 \/ c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.66/0.85     ssSkC6 \/ ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a576 \/
% 0.66/0.85     c2_2 a546 a579 \/ c3_1 a546 \/ c3_2 a546 a559 \/ c4_1 a546 \/
% 0.66/0.85     c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/ ndr1_1 a581 \/ ssSkC0 \/
% 0.66/0.85     ssSkC2 \/ ssSkC6 \/ ssSkP3 a546
% 0.66/0.85  |- ~c2_0 \/ ~c4_2 a546 a570 \/ ~c5_1 a546 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.66/0.85     c1_2 a546 a576 \/ c2_2 a546 a579 \/ c3_1 a546 \/ c3_2 a546 a559 \/
% 0.66/0.85     c5_0 \/ ssSkC0 \/ ssSkC2 \/ ssSkC6 \/ ssSkP3 a546
% 0.66/0.85  |- ~c2_0 \/ ~c3_2 a546 a570 \/ ~c5_1 a546 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.66/0.85     c1_2 a546 a576 \/ c2_2 a546 a579 \/ c3_1 a546 \/ c3_2 a546 a559 \/
% 0.66/0.85     c5_0 \/ ssSkC0 \/ ssSkC2 \/ ssSkC6 \/ ssSkP3 a546
% 0.66/0.85  |- ~c2_0 \/ ~c2_2 a546 a570 \/ ~c5_1 a546 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.66/0.85     c1_2 a546 a576 \/ c2_2 a546 a579 \/ c3_1 a546 \/ c3_2 a546 a559 \/
% 0.66/0.85     c5_0 \/ ssSkC0 \/ ssSkC2 \/ ssSkC6 \/ ssSkP3 a546
% 0.66/0.85  |- c1_2 a567 a576 \/ c2_2 a567 a579 \/ c3_1 a567 \/ c3_2 a567 a559 \/
% 0.66/0.85     c4_0 \/ c5_2 a567 a579 \/ ssSkC2 \/ ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.66/0.85  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.66/0.85     ~ndr1_1 a567 \/ c1_2 a567 a576 \/ c2_2 a567 a579 \/ c3_1 a567 \/
% 0.66/0.85     c3_2 a567 a559 \/ c4_0 \/ c4_1 a567 \/ c4_2 a567 a579 \/ c5_1 a567 \/
% 0.66/0.85     ssSkC2 \/ ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.66/0.85  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a576 \/
% 0.66/0.85     c1_2 a581 a582 \/ c2_2 a567 a579 \/ c3_1 a567 \/ c3_2 a567 a559 \/
% 0.66/0.85     c4_0 \/ c4_1 a567 \/ c4_2 a567 a579 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/
% 0.66/0.85     ssSkC6 \/ ssSkP3 a567
% 0.66/0.85  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a576 \/
% 0.66/0.85     c2_2 a567 a579 \/ c3_1 a567 \/ c3_2 a567 a559 \/ c4_0 \/ c4_1 a567 \/
% 0.66/0.85     c4_2 a567 a579 \/ c5_1 a567 \/ c5_2 a581 a582 \/ ssSkC2 \/ ssSkC5 \/
% 0.66/0.85     ssSkC6 \/ ssSkP3 a567
% 0.66/0.85  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/
% 0.66/0.85     c1_2 a567 a576 \/ c2_2 a567 a579 \/ c3_1 a567 \/ c3_2 a567 a559 \/
% 0.66/0.85     c4_0 \/ c4_1 a567 \/ c4_2 a567 a579 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/
% 0.66/0.85     ssSkC6 \/ ssSkP3 a567
% 0.66/0.85  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a576 \/
% 0.66/0.85     c2_2 a567 a579 \/ c3_1 a567 \/ c3_1 a581 \/ c3_2 a567 a559 \/ c4_0 \/
% 0.66/0.85     c4_1 a567 \/ c4_2 a567 a579 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/
% 0.66/0.85     ssSkC6 \/ ssSkP3 a567
% 0.66/0.85  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a576 \/
% 0.66/0.85     c2_2 a567 a579 \/ c3_1 a567 \/ c3_2 a567 a559 \/ c4_0 \/ c4_1 a567 \/
% 0.66/0.85     c4_2 a567 a579 \/ c5_1 a567 \/ ndr1_1 a581 \/ ssSkC2 \/ ssSkC5 \/
% 0.66/0.85     ssSkC6 \/ ssSkP3 a567
% 0.66/0.85  |- c1_2 a567 a576 \/ c2_2 a567 a579 \/ c3_1 a567 \/ c3_2 a567 a559 \/
% 0.66/0.85     c5_0 \/ c5_2 a567 a579 \/ ssSkC2 \/ ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.66/0.85  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.66/0.85     ~ndr1_1 a567 \/ c1_2 a567 a576 \/ c2_2 a567 a579 \/ c3_1 a567 \/
% 0.66/0.85     c3_2 a567 a559 \/ c4_1 a567 \/ c4_2 a567 a579 \/ c5_0 \/ c5_1 a567 \/
% 0.66/0.85     ssSkC2 \/ ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.66/0.85  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a576 \/
% 0.66/0.85     c1_2 a581 a582 \/ c2_2 a567 a579 \/ c3_1 a567 \/ c3_2 a567 a559 \/
% 0.66/0.85     c4_1 a567 \/ c4_2 a567 a579 \/ c5_0 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/
% 0.66/0.85     ssSkC6 \/ ssSkP3 a567
% 0.66/0.85  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a576 \/
% 0.66/0.85     c2_2 a567 a579 \/ c3_1 a567 \/ c3_2 a567 a559 \/ c4_1 a567 \/
% 0.66/0.85     c4_2 a567 a579 \/ c5_0 \/ c5_1 a567 \/ c5_2 a581 a582 \/ ssSkC2 \/
% 0.66/0.85     ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.66/0.85  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/
% 0.66/0.85     c1_2 a567 a576 \/ c2_2 a567 a579 \/ c3_1 a567 \/ c3_2 a567 a559 \/
% 0.66/0.85     c4_1 a567 \/ c4_2 a567 a579 \/ c5_0 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/
% 0.66/0.85     ssSkC6 \/ ssSkP3 a567
% 0.66/0.85  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a576 \/
% 0.66/0.85     c2_2 a567 a579 \/ c3_1 a567 \/ c3_1 a581 \/ c3_2 a567 a559 \/
% 0.66/0.85     c4_1 a567 \/ c4_2 a567 a579 \/ c5_0 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/
% 0.66/0.85     ssSkC6 \/ ssSkP3 a567
% 0.66/0.85  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a576 \/
% 0.66/0.85     c2_2 a567 a579 \/ c3_1 a567 \/ c3_2 a567 a559 \/ c4_1 a567 \/
% 0.66/0.85     c4_2 a567 a579 \/ c5_0 \/ c5_1 a567 \/ ndr1_1 a581 \/ ssSkC2 \/
% 0.66/0.85     ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.66/0.85  |- ~c2_0 \/ ~c4_2 a567 a570 \/ ~c5_1 a567 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/
% 0.66/0.85     c1_2 a567 a576 \/ c2_2 a567 a579 \/ c3_1 a567 \/ c3_2 a567 a559 \/
% 0.66/0.85     c5_0 \/ ssSkC2 \/ ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.66/0.85  |- ~c2_0 \/ ~c3_2 a567 a570 \/ ~c5_1 a567 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/
% 0.66/0.85     c1_2 a567 a576 \/ c2_2 a567 a579 \/ c3_1 a567 \/ c3_2 a567 a559 \/
% 0.66/0.85     c5_0 \/ ssSkC2 \/ ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.66/0.85  |- ~c2_0 \/ ~c2_2 a567 a570 \/ ~c5_1 a567 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/
% 0.66/0.85     c1_2 a567 a576 \/ c2_2 a567 a579 \/ c3_1 a567 \/ c3_2 a567 a559 \/
% 0.66/0.85     c5_0 \/ ssSkC2 \/ ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.66/0.85  |- c1_0 \/ c1_2 a546 a576 \/ c2_2 a546 a579 \/ c3_0 \/ c3_1 a546 \/
% 0.66/0.85     c3_2 a546 a559 \/ c5_2 a546 a579 \/ ssSkC0 \/ ssSkC2 \/ ssSkC6 \/
% 0.66/0.85     ssSkP3 a546
% 0.66/0.85  |- c1_0 \/ c1_2 a567 a576 \/ c2_2 a567 a579 \/ c3_0 \/ c3_1 a567 \/
% 0.66/0.85     c3_2 a567 a559 \/ c5_2 a567 a579 \/ ssSkC2 \/ ssSkC5 \/ ssSkC6 \/
% 0.66/0.85     ssSkP3 a567
% 0.66/0.85  |- ~ndr1_0 \/ c1_2 a546 a548 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/
% 0.66/0.85     c5_2 a546 a579 \/ ssSkC0 \/ ssSkC2 \/ ssSkP0 a546 \/ ssSkP3 a546
% 0.66/0.85  |- ~ndr1_0 \/ c1_2 a567 a548 \/ c2_2 a567 a579 \/ c3_2 a567 a559 \/
% 0.66/0.85     c5_2 a567 a579 \/ ssSkC2 \/ ssSkC5 \/ ssSkP0 a567 \/ ssSkP3 a567
% 0.66/0.85  |- c1_0 \/ c1_2 a546 a548 \/ c2_2 a546 a579 \/ c3_0 \/ c3_2 a546 a559 \/
% 0.66/0.85     c5_2 a546 a579 \/ ssSkC0 \/ ssSkC2 \/ ssSkP0 a546 \/ ssSkP3 a546
% 0.66/0.85  |- c1_2 a546 a548 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/ c5_0 \/
% 0.66/0.85     c5_2 a546 a579 \/ ssSkC0 \/ ssSkC2 \/ ssSkP0 a546 \/ ssSkP3 a546
% 0.66/0.85  |- c1_2 a546 a548 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/ c4_0 \/
% 0.66/0.85     c5_2 a546 a579 \/ ssSkC0 \/ ssSkC2 \/ ssSkP0 a546 \/ ssSkP3 a546
% 0.66/0.85  |- c1_0 \/ c1_2 a567 a548 \/ c2_2 a567 a579 \/ c3_0 \/ c3_2 a567 a559 \/
% 0.66/0.85     c5_2 a567 a579 \/ ssSkC2 \/ ssSkC5 \/ ssSkP0 a567 \/ ssSkP3 a567
% 0.66/0.85  |- c1_2 a567 a548 \/ c2_2 a567 a579 \/ c3_2 a567 a559 \/ c5_0 \/
% 0.66/0.85     c5_2 a567 a579 \/ ssSkC2 \/ ssSkC5 \/ ssSkP0 a567 \/ ssSkP3 a567
% 0.66/0.85  |- c1_2 a567 a548 \/ c2_2 a567 a579 \/ c3_2 a567 a559 \/ c4_0 \/
% 0.66/0.85     c5_2 a567 a579 \/ ssSkC2 \/ ssSkC5 \/ ssSkP0 a567 \/ ssSkP3 a567
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.66/0.85     ~ndr1_1 a546 \/ c1_2 a546 a548 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/
% 0.66/0.85     c4_1 a546 \/ c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.66/0.85     ssSkP0 a546 \/ ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a548 \/
% 0.66/0.85     c1_2 a581 a582 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/ c4_1 a546 \/
% 0.66/0.85     c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.66/0.85     ssSkP0 a546 \/ ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a548 \/
% 0.66/0.85     c2_2 a546 a579 \/ c3_2 a546 a559 \/ c4_1 a546 \/ c4_2 a546 a579 \/
% 0.66/0.85     c5_0 \/ c5_1 a546 \/ c5_2 a581 a582 \/ ssSkC0 \/ ssSkC2 \/
% 0.66/0.85     ssSkP0 a546 \/ ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.66/0.85     c1_2 a546 a548 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/ c4_1 a546 \/
% 0.66/0.85     c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.66/0.85     ssSkP0 a546 \/ ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a548 \/
% 0.66/0.85     c2_2 a546 a579 \/ c3_1 a581 \/ c3_2 a546 a559 \/ c4_1 a546 \/
% 0.66/0.85     c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.66/0.85     ssSkP0 a546 \/ ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a548 \/
% 0.66/0.85     c2_2 a546 a579 \/ c3_2 a546 a559 \/ c4_1 a546 \/ c4_2 a546 a579 \/
% 0.66/0.85     c5_0 \/ c5_1 a546 \/ ndr1_1 a581 \/ ssSkC0 \/ ssSkC2 \/ ssSkP0 a546 \/
% 0.66/0.85     ssSkP3 a546
% 0.66/0.85  |- ~c2_0 \/ ~c4_2 a546 a570 \/ ~c5_1 a546 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.66/0.85     c1_2 a546 a548 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/ c5_0 \/ ssSkC0 \/
% 0.66/0.85     ssSkC2 \/ ssSkP0 a546 \/ ssSkP3 a546
% 0.66/0.85  |- ~c2_0 \/ ~c3_2 a546 a570 \/ ~c5_1 a546 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.66/0.85     c1_2 a546 a548 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/ c5_0 \/ ssSkC0 \/
% 0.66/0.85     ssSkC2 \/ ssSkP0 a546 \/ ssSkP3 a546
% 0.66/0.85  |- ~c2_0 \/ ~c2_2 a546 a570 \/ ~c5_1 a546 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.66/0.85     c1_2 a546 a548 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/ c5_0 \/ ssSkC0 \/
% 0.66/0.85     ssSkC2 \/ ssSkP0 a546 \/ ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.66/0.85     ~ndr1_1 a546 \/ c1_2 a546 a548 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/
% 0.66/0.85     c4_0 \/ c4_1 a546 \/ c4_2 a546 a579 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.66/0.85     ssSkP0 a546 \/ ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a548 \/
% 0.66/0.85     c1_2 a581 a582 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/ c4_0 \/
% 0.66/0.85     c4_1 a546 \/ c4_2 a546 a579 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.66/0.85     ssSkP0 a546 \/ ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a548 \/
% 0.66/0.85     c2_2 a546 a579 \/ c3_2 a546 a559 \/ c4_0 \/ c4_1 a546 \/
% 0.66/0.85     c4_2 a546 a579 \/ c5_1 a546 \/ c5_2 a581 a582 \/ ssSkC0 \/ ssSkC2 \/
% 0.66/0.85     ssSkP0 a546 \/ ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.66/0.85     c1_2 a546 a548 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/ c4_0 \/
% 0.66/0.85     c4_1 a546 \/ c4_2 a546 a579 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.66/0.85     ssSkP0 a546 \/ ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a548 \/
% 0.66/0.85     c2_2 a546 a579 \/ c3_1 a581 \/ c3_2 a546 a559 \/ c4_0 \/ c4_1 a546 \/
% 0.66/0.85     c4_2 a546 a579 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/ ssSkP0 a546 \/
% 0.66/0.85     ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a548 \/
% 0.66/0.85     c2_2 a546 a579 \/ c3_2 a546 a559 \/ c4_0 \/ c4_1 a546 \/
% 0.66/0.85     c4_2 a546 a579 \/ c5_1 a546 \/ ndr1_1 a581 \/ ssSkC0 \/ ssSkC2 \/
% 0.66/0.85     ssSkP0 a546 \/ ssSkP3 a546
% 0.66/0.85  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.66/0.85     ~ndr1_1 a567 \/ c1_2 a567 a548 \/ c2_2 a567 a579 \/ c3_2 a567 a559 \/
% 0.66/0.85     c4_1 a567 \/ c4_2 a567 a579 \/ c5_0 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/
% 0.66/0.85     ssSkP0 a567 \/ ssSkP3 a567
% 0.66/0.85  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a548 \/
% 0.66/0.85     c1_2 a581 a582 \/ c2_2 a567 a579 \/ c3_2 a567 a559 \/ c4_1 a567 \/
% 0.66/0.85     c4_2 a567 a579 \/ c5_0 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/
% 0.66/0.85     ssSkP0 a567 \/ ssSkP3 a567
% 0.66/0.85  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a548 \/
% 0.66/0.85     c2_2 a567 a579 \/ c3_2 a567 a559 \/ c4_1 a567 \/ c4_2 a567 a579 \/
% 0.66/0.85     c5_0 \/ c5_1 a567 \/ c5_2 a581 a582 \/ ssSkC2 \/ ssSkC5 \/
% 0.66/0.85     ssSkP0 a567 \/ ssSkP3 a567
% 0.66/0.85  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/
% 0.66/0.85     c1_2 a567 a548 \/ c2_2 a567 a579 \/ c3_2 a567 a559 \/ c4_1 a567 \/
% 0.66/0.85     c4_2 a567 a579 \/ c5_0 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/
% 0.66/0.85     ssSkP0 a567 \/ ssSkP3 a567
% 0.66/0.85  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a548 \/
% 0.66/0.85     c2_2 a567 a579 \/ c3_1 a581 \/ c3_2 a567 a559 \/ c4_1 a567 \/
% 0.66/0.85     c4_2 a567 a579 \/ c5_0 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/
% 0.66/0.85     ssSkP0 a567 \/ ssSkP3 a567
% 0.66/0.85  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a548 \/
% 0.66/0.85     c2_2 a567 a579 \/ c3_2 a567 a559 \/ c4_1 a567 \/ c4_2 a567 a579 \/
% 0.66/0.85     c5_0 \/ c5_1 a567 \/ ndr1_1 a581 \/ ssSkC2 \/ ssSkC5 \/ ssSkP0 a567 \/
% 0.66/0.85     ssSkP3 a567
% 0.66/0.85  |- ~c2_0 \/ ~c4_2 a567 a570 \/ ~c5_1 a567 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/
% 0.66/0.85     c1_2 a567 a548 \/ c2_2 a567 a579 \/ c3_2 a567 a559 \/ c5_0 \/ ssSkC2 \/
% 0.66/0.85     ssSkC5 \/ ssSkP0 a567 \/ ssSkP3 a567
% 0.66/0.85  |- ~c2_0 \/ ~c3_2 a567 a570 \/ ~c5_1 a567 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/
% 0.66/0.85     c1_2 a567 a548 \/ c2_2 a567 a579 \/ c3_2 a567 a559 \/ c5_0 \/ ssSkC2 \/
% 0.66/0.85     ssSkC5 \/ ssSkP0 a567 \/ ssSkP3 a567
% 0.66/0.85  |- ~c2_0 \/ ~c2_2 a567 a570 \/ ~c5_1 a567 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/
% 0.66/0.85     c1_2 a567 a548 \/ c2_2 a567 a579 \/ c3_2 a567 a559 \/ c5_0 \/ ssSkC2 \/
% 0.66/0.85     ssSkC5 \/ ssSkP0 a567 \/ ssSkP3 a567
% 0.66/0.85  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.66/0.85     ~ndr1_1 a567 \/ c1_2 a567 a548 \/ c2_2 a567 a579 \/ c3_2 a567 a559 \/
% 0.66/0.85     c4_0 \/ c4_1 a567 \/ c4_2 a567 a579 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/
% 0.66/0.85     ssSkP0 a567 \/ ssSkP3 a567
% 0.66/0.85  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a548 \/
% 0.66/0.85     c1_2 a581 a582 \/ c2_2 a567 a579 \/ c3_2 a567 a559 \/ c4_0 \/
% 0.66/0.85     c4_1 a567 \/ c4_2 a567 a579 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/
% 0.66/0.85     ssSkP0 a567 \/ ssSkP3 a567
% 0.66/0.85  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a548 \/
% 0.66/0.85     c2_2 a567 a579 \/ c3_2 a567 a559 \/ c4_0 \/ c4_1 a567 \/
% 0.66/0.85     c4_2 a567 a579 \/ c5_1 a567 \/ c5_2 a581 a582 \/ ssSkC2 \/ ssSkC5 \/
% 0.66/0.85     ssSkP0 a567 \/ ssSkP3 a567
% 0.66/0.85  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/
% 0.66/0.85     c1_2 a567 a548 \/ c2_2 a567 a579 \/ c3_2 a567 a559 \/ c4_0 \/
% 0.66/0.85     c4_1 a567 \/ c4_2 a567 a579 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/
% 0.66/0.85     ssSkP0 a567 \/ ssSkP3 a567
% 0.66/0.85  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a548 \/
% 0.66/0.85     c2_2 a567 a579 \/ c3_1 a581 \/ c3_2 a567 a559 \/ c4_0 \/ c4_1 a567 \/
% 0.66/0.85     c4_2 a567 a579 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/ ssSkP0 a567 \/
% 0.66/0.85     ssSkP3 a567
% 0.66/0.85  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a548 \/
% 0.66/0.85     c2_2 a567 a579 \/ c3_2 a567 a559 \/ c4_0 \/ c4_1 a567 \/
% 0.66/0.85     c4_2 a567 a579 \/ c5_1 a567 \/ ndr1_1 a581 \/ ssSkC2 \/ ssSkC5 \/
% 0.66/0.85     ssSkP0 a567 \/ ssSkP3 a567
% 0.66/0.86  |- ~ndr1_0 \/ c1_2 a546 a562 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/
% 0.66/0.86     c5_2 a546 a579 \/ ssSkC0 \/ ssSkC2 \/ ssSkP2 a546 \/ ssSkP3 a546
% 0.66/0.86  |- ~ndr1_0 \/ c1_2 a567 a562 \/ c2_2 a567 a579 \/ c3_2 a567 a559 \/
% 0.66/0.86     c5_2 a567 a579 \/ ssSkC2 \/ ssSkC5 \/ ssSkP2 a567 \/ ssSkP3 a567
% 0.66/0.86  |- c1_0 \/ c1_2 a546 a562 \/ c2_2 a546 a579 \/ c3_0 \/ c3_2 a546 a559 \/
% 0.66/0.86     c5_2 a546 a579 \/ ssSkC0 \/ ssSkC2 \/ ssSkP2 a546 \/ ssSkP3 a546
% 0.66/0.86  |- c1_2 a546 a562 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/ c5_0 \/
% 0.66/0.86     c5_2 a546 a579 \/ ssSkC0 \/ ssSkC2 \/ ssSkP2 a546 \/ ssSkP3 a546
% 0.66/0.86  |- c1_2 a546 a562 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/ c4_0 \/
% 0.66/0.86     c5_2 a546 a579 \/ ssSkC0 \/ ssSkC2 \/ ssSkP2 a546 \/ ssSkP3 a546
% 0.71/0.86  |- c1_0 \/ c1_2 a567 a562 \/ c2_2 a567 a579 \/ c3_0 \/ c3_2 a567 a559 \/
% 0.71/0.86     c5_2 a567 a579 \/ ssSkC2 \/ ssSkC5 \/ ssSkP2 a567 \/ ssSkP3 a567
% 0.71/0.86  |- c1_2 a567 a562 \/ c2_2 a567 a579 \/ c3_2 a567 a559 \/ c5_0 \/
% 0.71/0.86     c5_2 a567 a579 \/ ssSkC2 \/ ssSkC5 \/ ssSkP2 a567 \/ ssSkP3 a567
% 0.71/0.86  |- c1_2 a567 a562 \/ c2_2 a567 a579 \/ c3_2 a567 a559 \/ c4_0 \/
% 0.71/0.86     c5_2 a567 a579 \/ ssSkC2 \/ ssSkC5 \/ ssSkP2 a567 \/ ssSkP3 a567
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.71/0.86     ~ndr1_1 a546 \/ c1_2 a546 a562 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/
% 0.71/0.86     c4_1 a546 \/ c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.86     ssSkP2 a546 \/ ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a562 \/
% 0.71/0.86     c1_2 a581 a582 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/ c4_1 a546 \/
% 0.71/0.86     c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.86     ssSkP2 a546 \/ ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a562 \/
% 0.71/0.86     c2_2 a546 a579 \/ c3_2 a546 a559 \/ c4_1 a546 \/ c4_2 a546 a579 \/
% 0.71/0.86     c5_0 \/ c5_1 a546 \/ c5_2 a581 a582 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.86     ssSkP2 a546 \/ ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.71/0.86     c1_2 a546 a562 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/ c4_1 a546 \/
% 0.71/0.86     c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.86     ssSkP2 a546 \/ ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a562 \/
% 0.71/0.86     c2_2 a546 a579 \/ c3_1 a581 \/ c3_2 a546 a559 \/ c4_1 a546 \/
% 0.71/0.86     c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.86     ssSkP2 a546 \/ ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a562 \/
% 0.71/0.86     c2_2 a546 a579 \/ c3_2 a546 a559 \/ c4_1 a546 \/ c4_2 a546 a579 \/
% 0.71/0.86     c5_0 \/ c5_1 a546 \/ ndr1_1 a581 \/ ssSkC0 \/ ssSkC2 \/ ssSkP2 a546 \/
% 0.71/0.86     ssSkP3 a546
% 0.71/0.86  |- ~c2_0 \/ ~c4_2 a546 a570 \/ ~c5_1 a546 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.71/0.86     c1_2 a546 a562 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/ c5_0 \/ ssSkC0 \/
% 0.71/0.86     ssSkC2 \/ ssSkP2 a546 \/ ssSkP3 a546
% 0.71/0.86  |- ~c2_0 \/ ~c3_2 a546 a570 \/ ~c5_1 a546 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.71/0.86     c1_2 a546 a562 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/ c5_0 \/ ssSkC0 \/
% 0.71/0.86     ssSkC2 \/ ssSkP2 a546 \/ ssSkP3 a546
% 0.71/0.86  |- ~c2_0 \/ ~c2_2 a546 a570 \/ ~c5_1 a546 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.71/0.86     c1_2 a546 a562 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/ c5_0 \/ ssSkC0 \/
% 0.71/0.86     ssSkC2 \/ ssSkP2 a546 \/ ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.71/0.86     ~ndr1_1 a546 \/ c1_2 a546 a562 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/
% 0.71/0.86     c4_0 \/ c4_1 a546 \/ c4_2 a546 a579 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.86     ssSkP2 a546 \/ ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a562 \/
% 0.71/0.86     c1_2 a581 a582 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/ c4_0 \/
% 0.71/0.86     c4_1 a546 \/ c4_2 a546 a579 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.86     ssSkP2 a546 \/ ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a562 \/
% 0.71/0.86     c2_2 a546 a579 \/ c3_2 a546 a559 \/ c4_0 \/ c4_1 a546 \/
% 0.71/0.86     c4_2 a546 a579 \/ c5_1 a546 \/ c5_2 a581 a582 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.86     ssSkP2 a546 \/ ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.71/0.86     c1_2 a546 a562 \/ c2_2 a546 a579 \/ c3_2 a546 a559 \/ c4_0 \/
% 0.71/0.86     c4_1 a546 \/ c4_2 a546 a579 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.86     ssSkP2 a546 \/ ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a562 \/
% 0.71/0.86     c2_2 a546 a579 \/ c3_1 a581 \/ c3_2 a546 a559 \/ c4_0 \/ c4_1 a546 \/
% 0.71/0.86     c4_2 a546 a579 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/ ssSkP2 a546 \/
% 0.71/0.86     ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a562 \/
% 0.71/0.86     c2_2 a546 a579 \/ c3_2 a546 a559 \/ c4_0 \/ c4_1 a546 \/
% 0.71/0.86     c4_2 a546 a579 \/ c5_1 a546 \/ ndr1_1 a581 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.86     ssSkP2 a546 \/ ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.71/0.86     ~ndr1_1 a567 \/ c1_2 a567 a562 \/ c2_2 a567 a579 \/ c3_2 a567 a559 \/
% 0.71/0.86     c4_1 a567 \/ c4_2 a567 a579 \/ c5_0 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/
% 0.71/0.86     ssSkP2 a567 \/ ssSkP3 a567
% 0.71/0.86  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a562 \/
% 0.71/0.86     c1_2 a581 a582 \/ c2_2 a567 a579 \/ c3_2 a567 a559 \/ c4_1 a567 \/
% 0.71/0.86     c4_2 a567 a579 \/ c5_0 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/
% 0.71/0.86     ssSkP2 a567 \/ ssSkP3 a567
% 0.71/0.86  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a562 \/
% 0.71/0.86     c2_2 a567 a579 \/ c3_2 a567 a559 \/ c4_1 a567 \/ c4_2 a567 a579 \/
% 0.71/0.86     c5_0 \/ c5_1 a567 \/ c5_2 a581 a582 \/ ssSkC2 \/ ssSkC5 \/
% 0.71/0.86     ssSkP2 a567 \/ ssSkP3 a567
% 0.71/0.86  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/
% 0.71/0.86     c1_2 a567 a562 \/ c2_2 a567 a579 \/ c3_2 a567 a559 \/ c4_1 a567 \/
% 0.71/0.86     c4_2 a567 a579 \/ c5_0 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/
% 0.71/0.86     ssSkP2 a567 \/ ssSkP3 a567
% 0.71/0.86  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a562 \/
% 0.71/0.86     c2_2 a567 a579 \/ c3_1 a581 \/ c3_2 a567 a559 \/ c4_1 a567 \/
% 0.71/0.86     c4_2 a567 a579 \/ c5_0 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/
% 0.71/0.86     ssSkP2 a567 \/ ssSkP3 a567
% 0.71/0.86  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a562 \/
% 0.71/0.86     c2_2 a567 a579 \/ c3_2 a567 a559 \/ c4_1 a567 \/ c4_2 a567 a579 \/
% 0.71/0.86     c5_0 \/ c5_1 a567 \/ ndr1_1 a581 \/ ssSkC2 \/ ssSkC5 \/ ssSkP2 a567 \/
% 0.71/0.86     ssSkP3 a567
% 0.71/0.86  |- ~c2_0 \/ ~c4_2 a567 a570 \/ ~c5_1 a567 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/
% 0.71/0.86     c1_2 a567 a562 \/ c2_2 a567 a579 \/ c3_2 a567 a559 \/ c5_0 \/ ssSkC2 \/
% 0.71/0.86     ssSkC5 \/ ssSkP2 a567 \/ ssSkP3 a567
% 0.71/0.86  |- ~c2_0 \/ ~c3_2 a567 a570 \/ ~c5_1 a567 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/
% 0.71/0.86     c1_2 a567 a562 \/ c2_2 a567 a579 \/ c3_2 a567 a559 \/ c5_0 \/ ssSkC2 \/
% 0.71/0.86     ssSkC5 \/ ssSkP2 a567 \/ ssSkP3 a567
% 0.71/0.86  |- ~c2_0 \/ ~c2_2 a567 a570 \/ ~c5_1 a567 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/
% 0.71/0.86     c1_2 a567 a562 \/ c2_2 a567 a579 \/ c3_2 a567 a559 \/ c5_0 \/ ssSkC2 \/
% 0.71/0.86     ssSkC5 \/ ssSkP2 a567 \/ ssSkP3 a567
% 0.71/0.86  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.71/0.86     ~ndr1_1 a567 \/ c1_2 a567 a562 \/ c2_2 a567 a579 \/ c3_2 a567 a559 \/
% 0.71/0.86     c4_0 \/ c4_1 a567 \/ c4_2 a567 a579 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/
% 0.71/0.86     ssSkP2 a567 \/ ssSkP3 a567
% 0.71/0.86  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a562 \/
% 0.71/0.86     c1_2 a581 a582 \/ c2_2 a567 a579 \/ c3_2 a567 a559 \/ c4_0 \/
% 0.71/0.86     c4_1 a567 \/ c4_2 a567 a579 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/
% 0.71/0.86     ssSkP2 a567 \/ ssSkP3 a567
% 0.71/0.86  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a562 \/
% 0.71/0.86     c2_2 a567 a579 \/ c3_2 a567 a559 \/ c4_0 \/ c4_1 a567 \/
% 0.71/0.86     c4_2 a567 a579 \/ c5_1 a567 \/ c5_2 a581 a582 \/ ssSkC2 \/ ssSkC5 \/
% 0.71/0.86     ssSkP2 a567 \/ ssSkP3 a567
% 0.71/0.86  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/
% 0.71/0.86     c1_2 a567 a562 \/ c2_2 a567 a579 \/ c3_2 a567 a559 \/ c4_0 \/
% 0.71/0.86     c4_1 a567 \/ c4_2 a567 a579 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/
% 0.71/0.86     ssSkP2 a567 \/ ssSkP3 a567
% 0.71/0.86  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a562 \/
% 0.71/0.86     c2_2 a567 a579 \/ c3_1 a581 \/ c3_2 a567 a559 \/ c4_0 \/ c4_1 a567 \/
% 0.71/0.86     c4_2 a567 a579 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/ ssSkP2 a567 \/
% 0.71/0.86     ssSkP3 a567
% 0.71/0.86  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a562 \/
% 0.71/0.86     c2_2 a567 a579 \/ c3_2 a567 a559 \/ c4_0 \/ c4_1 a567 \/
% 0.71/0.86     c4_2 a567 a579 \/ c5_1 a567 \/ ndr1_1 a581 \/ ssSkC2 \/ ssSkC5 \/
% 0.71/0.86     ssSkP2 a567 \/ ssSkP3 a567
% 0.71/0.86  |- ~c2_2 $_169 $_171 \/ ~ndr1_0 \/ ~ndr1_1 $_169 \/ c1_2 $_169 $_171 \/
% 0.71/0.86     c2_2 $_169 a579 \/ c4_2 $_169 a559 \/ c5_2 $_169 a579 \/ ssSkC2 \/
% 0.71/0.86     ssSkP3 $_169
% 0.71/0.86  |- ~ndr1_0 \/ ~ndr1_1 $_172 \/ c1_2 $_172 a548 \/ c2_2 $_172 a579 \/
% 0.71/0.86     c4_2 $_172 a559 \/ c5_2 $_172 a579 \/ ssSkC2 \/ ssSkP0 $_172 \/
% 0.71/0.86     ssSkP3 $_172
% 0.71/0.86  |- ~ndr1_0 \/ ~ndr1_1 $_172 \/ c1_2 $_172 a562 \/ c2_2 $_172 a579 \/
% 0.71/0.86     c4_2 $_172 a559 \/ c5_2 $_172 a579 \/ ssSkC2 \/ ssSkP2 $_172 \/
% 0.71/0.86     ssSkP3 $_172
% 0.71/0.86  |- ~ndr1_0 \/ c1_2 a546 a547 \/ c2_2 a546 a579 \/ c4_2 a546 a559 \/
% 0.71/0.86     c5_2 a546 a579 \/ ssSkC0 \/ ssSkC2 \/ ssSkP3 a546
% 0.71/0.86  |- c1_0 \/ c1_2 a546 a547 \/ c2_2 a546 a579 \/ c3_0 \/ c4_2 a546 a559 \/
% 0.71/0.86     c5_2 a546 a579 \/ ssSkC0 \/ ssSkC2 \/ ssSkP3 a546
% 0.71/0.86  |- c1_2 a546 a547 \/ c2_2 a546 a579 \/ c4_2 a546 a559 \/ c5_0 \/
% 0.71/0.86     c5_2 a546 a579 \/ ssSkC0 \/ ssSkC2 \/ ssSkP3 a546
% 0.71/0.86  |- c1_2 a546 a547 \/ c2_2 a546 a579 \/ c4_0 \/ c4_2 a546 a559 \/
% 0.71/0.86     c5_2 a546 a579 \/ ssSkC0 \/ ssSkC2 \/ ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.71/0.86     ~ndr1_1 a546 \/ c1_2 a546 a547 \/ c2_2 a546 a579 \/ c4_1 a546 \/
% 0.71/0.86     c4_2 a546 a559 \/ c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/ ssSkC0 \/
% 0.71/0.86     ssSkC2 \/ ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a547 \/
% 0.71/0.86     c1_2 a581 a582 \/ c2_2 a546 a579 \/ c4_1 a546 \/ c4_2 a546 a559 \/
% 0.71/0.86     c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/ ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a547 \/
% 0.71/0.86     c2_2 a546 a579 \/ c4_1 a546 \/ c4_2 a546 a559 \/ c4_2 a546 a579 \/
% 0.71/0.86     c5_0 \/ c5_1 a546 \/ c5_2 a581 a582 \/ ssSkC0 \/ ssSkC2 \/ ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.71/0.86     c1_2 a546 a547 \/ c2_2 a546 a579 \/ c4_1 a546 \/ c4_2 a546 a559 \/
% 0.71/0.86     c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/ ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a547 \/
% 0.71/0.86     c2_2 a546 a579 \/ c3_1 a581 \/ c4_1 a546 \/ c4_2 a546 a559 \/
% 0.71/0.86     c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/ ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a547 \/
% 0.71/0.86     c2_2 a546 a579 \/ c4_1 a546 \/ c4_2 a546 a559 \/ c4_2 a546 a579 \/
% 0.71/0.86     c5_0 \/ c5_1 a546 \/ ndr1_1 a581 \/ ssSkC0 \/ ssSkC2 \/ ssSkP3 a546
% 0.71/0.86  |- ~c2_0 \/ ~c4_2 a546 a570 \/ ~c5_1 a546 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.71/0.86     c1_2 a546 a547 \/ c2_2 a546 a579 \/ c4_2 a546 a559 \/ c5_0 \/ ssSkC0 \/
% 0.71/0.86     ssSkC2 \/ ssSkP3 a546
% 0.71/0.86  |- ~c2_0 \/ ~c3_2 a546 a570 \/ ~c5_1 a546 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.71/0.86     c1_2 a546 a547 \/ c2_2 a546 a579 \/ c4_2 a546 a559 \/ c5_0 \/ ssSkC0 \/
% 0.71/0.86     ssSkC2 \/ ssSkP3 a546
% 0.71/0.86  |- ~c2_0 \/ ~c2_2 a546 a570 \/ ~c5_1 a546 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.71/0.86     c1_2 a546 a547 \/ c2_2 a546 a579 \/ c4_2 a546 a559 \/ c5_0 \/ ssSkC0 \/
% 0.71/0.86     ssSkC2 \/ ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.71/0.86     ~ndr1_1 a546 \/ c1_2 a546 a547 \/ c2_2 a546 a579 \/ c4_0 \/ c4_1 a546 \/
% 0.71/0.86     c4_2 a546 a559 \/ c4_2 a546 a579 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.86     ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a547 \/
% 0.71/0.86     c1_2 a581 a582 \/ c2_2 a546 a579 \/ c4_0 \/ c4_1 a546 \/
% 0.71/0.86     c4_2 a546 a559 \/ c4_2 a546 a579 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.86     ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a547 \/
% 0.71/0.86     c2_2 a546 a579 \/ c4_0 \/ c4_1 a546 \/ c4_2 a546 a559 \/
% 0.71/0.86     c4_2 a546 a579 \/ c5_1 a546 \/ c5_2 a581 a582 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.86     ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.71/0.86     c1_2 a546 a547 \/ c2_2 a546 a579 \/ c4_0 \/ c4_1 a546 \/
% 0.71/0.86     c4_2 a546 a559 \/ c4_2 a546 a579 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.86     ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a547 \/
% 0.71/0.86     c2_2 a546 a579 \/ c3_1 a581 \/ c4_0 \/ c4_1 a546 \/ c4_2 a546 a559 \/
% 0.71/0.86     c4_2 a546 a579 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/ ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a547 \/
% 0.71/0.86     c2_2 a546 a579 \/ c4_0 \/ c4_1 a546 \/ c4_2 a546 a559 \/
% 0.71/0.86     c4_2 a546 a579 \/ c5_1 a546 \/ ndr1_1 a581 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.86     ssSkP3 a546
% 0.71/0.86  |- c1_2 a546 a576 \/ c2_2 a546 a579 \/ c3_1 a546 \/ c4_0 \/
% 0.71/0.86     c4_2 a546 a559 \/ c5_2 a546 a579 \/ ssSkC0 \/ ssSkC2 \/ ssSkC6 \/
% 0.71/0.86     ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.71/0.86     ~ndr1_1 a546 \/ c1_2 a546 a576 \/ c2_2 a546 a579 \/ c3_1 a546 \/ c4_0 \/
% 0.71/0.86     c4_1 a546 \/ c4_2 a546 a559 \/ c4_2 a546 a579 \/ c5_1 a546 \/ ssSkC0 \/
% 0.71/0.86     ssSkC2 \/ ssSkC6 \/ ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a576 \/
% 0.71/0.86     c1_2 a581 a582 \/ c2_2 a546 a579 \/ c3_1 a546 \/ c4_0 \/ c4_1 a546 \/
% 0.71/0.86     c4_2 a546 a559 \/ c4_2 a546 a579 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.86     ssSkC6 \/ ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a576 \/
% 0.71/0.86     c2_2 a546 a579 \/ c3_1 a546 \/ c4_0 \/ c4_1 a546 \/ c4_2 a546 a559 \/
% 0.71/0.86     c4_2 a546 a579 \/ c5_1 a546 \/ c5_2 a581 a582 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.86     ssSkC6 \/ ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.71/0.86     c1_2 a546 a576 \/ c2_2 a546 a579 \/ c3_1 a546 \/ c4_0 \/ c4_1 a546 \/
% 0.71/0.86     c4_2 a546 a559 \/ c4_2 a546 a579 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.86     ssSkC6 \/ ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a576 \/
% 0.71/0.86     c2_2 a546 a579 \/ c3_1 a546 \/ c3_1 a581 \/ c4_0 \/ c4_1 a546 \/
% 0.71/0.86     c4_2 a546 a559 \/ c4_2 a546 a579 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.86     ssSkC6 \/ ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a576 \/
% 0.71/0.86     c2_2 a546 a579 \/ c3_1 a546 \/ c4_0 \/ c4_1 a546 \/ c4_2 a546 a559 \/
% 0.71/0.86     c4_2 a546 a579 \/ c5_1 a546 \/ ndr1_1 a581 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.86     ssSkC6 \/ ssSkP3 a546
% 0.71/0.86  |- c1_2 a546 a576 \/ c2_2 a546 a579 \/ c3_1 a546 \/ c4_2 a546 a559 \/
% 0.71/0.86     c5_0 \/ c5_2 a546 a579 \/ ssSkC0 \/ ssSkC2 \/ ssSkC6 \/ ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.71/0.86     ~ndr1_1 a546 \/ c1_2 a546 a576 \/ c2_2 a546 a579 \/ c3_1 a546 \/
% 0.71/0.86     c4_1 a546 \/ c4_2 a546 a559 \/ c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/
% 0.71/0.86     ssSkC0 \/ ssSkC2 \/ ssSkC6 \/ ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a576 \/
% 0.71/0.86     c1_2 a581 a582 \/ c2_2 a546 a579 \/ c3_1 a546 \/ c4_1 a546 \/
% 0.71/0.86     c4_2 a546 a559 \/ c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/ ssSkC0 \/
% 0.71/0.86     ssSkC2 \/ ssSkC6 \/ ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a576 \/
% 0.71/0.86     c2_2 a546 a579 \/ c3_1 a546 \/ c4_1 a546 \/ c4_2 a546 a559 \/
% 0.71/0.86     c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/ c5_2 a581 a582 \/ ssSkC0 \/
% 0.71/0.86     ssSkC2 \/ ssSkC6 \/ ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.71/0.86     c1_2 a546 a576 \/ c2_2 a546 a579 \/ c3_1 a546 \/ c4_1 a546 \/
% 0.71/0.86     c4_2 a546 a559 \/ c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/ ssSkC0 \/
% 0.71/0.86     ssSkC2 \/ ssSkC6 \/ ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a576 \/
% 0.71/0.86     c2_2 a546 a579 \/ c3_1 a546 \/ c3_1 a581 \/ c4_1 a546 \/
% 0.71/0.86     c4_2 a546 a559 \/ c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/ ssSkC0 \/
% 0.71/0.86     ssSkC2 \/ ssSkC6 \/ ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a576 \/
% 0.71/0.86     c2_2 a546 a579 \/ c3_1 a546 \/ c4_1 a546 \/ c4_2 a546 a559 \/
% 0.71/0.86     c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/ ndr1_1 a581 \/ ssSkC0 \/
% 0.71/0.86     ssSkC2 \/ ssSkC6 \/ ssSkP3 a546
% 0.71/0.86  |- ~c2_0 \/ ~c4_2 a546 a570 \/ ~c5_1 a546 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.71/0.86     c1_2 a546 a576 \/ c2_2 a546 a579 \/ c3_1 a546 \/ c4_2 a546 a559 \/
% 0.71/0.86     c5_0 \/ ssSkC0 \/ ssSkC2 \/ ssSkC6 \/ ssSkP3 a546
% 0.71/0.86  |- ~c2_0 \/ ~c3_2 a546 a570 \/ ~c5_1 a546 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.71/0.86     c1_2 a546 a576 \/ c2_2 a546 a579 \/ c3_1 a546 \/ c4_2 a546 a559 \/
% 0.71/0.86     c5_0 \/ ssSkC0 \/ ssSkC2 \/ ssSkC6 \/ ssSkP3 a546
% 0.71/0.86  |- ~c2_0 \/ ~c2_2 a546 a570 \/ ~c5_1 a546 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.71/0.86     c1_2 a546 a576 \/ c2_2 a546 a579 \/ c3_1 a546 \/ c4_2 a546 a559 \/
% 0.71/0.86     c5_0 \/ ssSkC0 \/ ssSkC2 \/ ssSkC6 \/ ssSkP3 a546
% 0.71/0.86  |- c1_2 a567 a576 \/ c2_2 a567 a579 \/ c3_1 a567 \/ c4_0 \/
% 0.71/0.86     c4_2 a567 a559 \/ c5_2 a567 a579 \/ ssSkC2 \/ ssSkC5 \/ ssSkC6 \/
% 0.71/0.86     ssSkP3 a567
% 0.71/0.86  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.71/0.86     ~ndr1_1 a567 \/ c1_2 a567 a576 \/ c2_2 a567 a579 \/ c3_1 a567 \/ c4_0 \/
% 0.71/0.86     c4_1 a567 \/ c4_2 a567 a559 \/ c4_2 a567 a579 \/ c5_1 a567 \/ ssSkC2 \/
% 0.71/0.86     ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.71/0.86  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a576 \/
% 0.71/0.86     c1_2 a581 a582 \/ c2_2 a567 a579 \/ c3_1 a567 \/ c4_0 \/ c4_1 a567 \/
% 0.71/0.86     c4_2 a567 a559 \/ c4_2 a567 a579 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/
% 0.71/0.86     ssSkC6 \/ ssSkP3 a567
% 0.71/0.86  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a576 \/
% 0.71/0.86     c2_2 a567 a579 \/ c3_1 a567 \/ c4_0 \/ c4_1 a567 \/ c4_2 a567 a559 \/
% 0.71/0.86     c4_2 a567 a579 \/ c5_1 a567 \/ c5_2 a581 a582 \/ ssSkC2 \/ ssSkC5 \/
% 0.71/0.86     ssSkC6 \/ ssSkP3 a567
% 0.71/0.86  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/
% 0.71/0.86     c1_2 a567 a576 \/ c2_2 a567 a579 \/ c3_1 a567 \/ c4_0 \/ c4_1 a567 \/
% 0.71/0.86     c4_2 a567 a559 \/ c4_2 a567 a579 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/
% 0.71/0.86     ssSkC6 \/ ssSkP3 a567
% 0.71/0.86  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a576 \/
% 0.71/0.86     c2_2 a567 a579 \/ c3_1 a567 \/ c3_1 a581 \/ c4_0 \/ c4_1 a567 \/
% 0.71/0.86     c4_2 a567 a559 \/ c4_2 a567 a579 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/
% 0.71/0.86     ssSkC6 \/ ssSkP3 a567
% 0.71/0.86  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a576 \/
% 0.71/0.86     c2_2 a567 a579 \/ c3_1 a567 \/ c4_0 \/ c4_1 a567 \/ c4_2 a567 a559 \/
% 0.71/0.86     c4_2 a567 a579 \/ c5_1 a567 \/ ndr1_1 a581 \/ ssSkC2 \/ ssSkC5 \/
% 0.71/0.86     ssSkC6 \/ ssSkP3 a567
% 0.71/0.86  |- c1_2 a567 a576 \/ c2_2 a567 a579 \/ c3_1 a567 \/ c4_2 a567 a559 \/
% 0.71/0.86     c5_0 \/ c5_2 a567 a579 \/ ssSkC2 \/ ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.71/0.86  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.71/0.86     ~ndr1_1 a567 \/ c1_2 a567 a576 \/ c2_2 a567 a579 \/ c3_1 a567 \/
% 0.71/0.86     c4_1 a567 \/ c4_2 a567 a559 \/ c4_2 a567 a579 \/ c5_0 \/ c5_1 a567 \/
% 0.71/0.86     ssSkC2 \/ ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.71/0.86  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a576 \/
% 0.71/0.86     c1_2 a581 a582 \/ c2_2 a567 a579 \/ c3_1 a567 \/ c4_1 a567 \/
% 0.71/0.86     c4_2 a567 a559 \/ c4_2 a567 a579 \/ c5_0 \/ c5_1 a567 \/ ssSkC2 \/
% 0.71/0.86     ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.71/0.86  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a576 \/
% 0.71/0.86     c2_2 a567 a579 \/ c3_1 a567 \/ c4_1 a567 \/ c4_2 a567 a559 \/
% 0.71/0.86     c4_2 a567 a579 \/ c5_0 \/ c5_1 a567 \/ c5_2 a581 a582 \/ ssSkC2 \/
% 0.71/0.86     ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.71/0.86  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/
% 0.71/0.86     c1_2 a567 a576 \/ c2_2 a567 a579 \/ c3_1 a567 \/ c4_1 a567 \/
% 0.71/0.86     c4_2 a567 a559 \/ c4_2 a567 a579 \/ c5_0 \/ c5_1 a567 \/ ssSkC2 \/
% 0.71/0.86     ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.71/0.86  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a576 \/
% 0.71/0.86     c2_2 a567 a579 \/ c3_1 a567 \/ c3_1 a581 \/ c4_1 a567 \/
% 0.71/0.86     c4_2 a567 a559 \/ c4_2 a567 a579 \/ c5_0 \/ c5_1 a567 \/ ssSkC2 \/
% 0.71/0.86     ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.71/0.86  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a576 \/
% 0.71/0.86     c2_2 a567 a579 \/ c3_1 a567 \/ c4_1 a567 \/ c4_2 a567 a559 \/
% 0.71/0.86     c4_2 a567 a579 \/ c5_0 \/ c5_1 a567 \/ ndr1_1 a581 \/ ssSkC2 \/
% 0.71/0.86     ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.71/0.86  |- ~c2_0 \/ ~c4_2 a567 a570 \/ ~c5_1 a567 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/
% 0.71/0.86     c1_2 a567 a576 \/ c2_2 a567 a579 \/ c3_1 a567 \/ c4_2 a567 a559 \/
% 0.71/0.86     c5_0 \/ ssSkC2 \/ ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.71/0.86  |- ~c2_0 \/ ~c3_2 a567 a570 \/ ~c5_1 a567 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/
% 0.71/0.86     c1_2 a567 a576 \/ c2_2 a567 a579 \/ c3_1 a567 \/ c4_2 a567 a559 \/
% 0.71/0.86     c5_0 \/ ssSkC2 \/ ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.71/0.86  |- ~c2_0 \/ ~c2_2 a567 a570 \/ ~c5_1 a567 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/
% 0.71/0.86     c1_2 a567 a576 \/ c2_2 a567 a579 \/ c3_1 a567 \/ c4_2 a567 a559 \/
% 0.71/0.86     c5_0 \/ ssSkC2 \/ ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.71/0.86  |- c1_0 \/ c1_2 a546 a576 \/ c2_2 a546 a579 \/ c3_0 \/ c3_1 a546 \/
% 0.71/0.86     c4_2 a546 a559 \/ c5_2 a546 a579 \/ ssSkC0 \/ ssSkC2 \/ ssSkC6 \/
% 0.71/0.86     ssSkP3 a546
% 0.71/0.86  |- c1_0 \/ c1_2 a567 a576 \/ c2_2 a567 a579 \/ c3_0 \/ c3_1 a567 \/
% 0.71/0.86     c4_2 a567 a559 \/ c5_2 a567 a579 \/ ssSkC2 \/ ssSkC5 \/ ssSkC6 \/
% 0.71/0.86     ssSkP3 a567
% 0.71/0.86  |- ~ndr1_0 \/ c1_2 a546 a548 \/ c2_2 a546 a579 \/ c4_2 a546 a559 \/
% 0.71/0.86     c5_2 a546 a579 \/ ssSkC0 \/ ssSkC2 \/ ssSkP0 a546 \/ ssSkP3 a546
% 0.71/0.86  |- ~ndr1_0 \/ c1_2 a567 a548 \/ c2_2 a567 a579 \/ c4_2 a567 a559 \/
% 0.71/0.86     c5_2 a567 a579 \/ ssSkC2 \/ ssSkC5 \/ ssSkP0 a567 \/ ssSkP3 a567
% 0.71/0.86  |- c1_0 \/ c1_2 a546 a548 \/ c2_2 a546 a579 \/ c3_0 \/ c4_2 a546 a559 \/
% 0.71/0.86     c5_2 a546 a579 \/ ssSkC0 \/ ssSkC2 \/ ssSkP0 a546 \/ ssSkP3 a546
% 0.71/0.86  |- c1_2 a546 a548 \/ c2_2 a546 a579 \/ c4_2 a546 a559 \/ c5_0 \/
% 0.71/0.86     c5_2 a546 a579 \/ ssSkC0 \/ ssSkC2 \/ ssSkP0 a546 \/ ssSkP3 a546
% 0.71/0.86  |- c1_2 a546 a548 \/ c2_2 a546 a579 \/ c4_0 \/ c4_2 a546 a559 \/
% 0.71/0.86     c5_2 a546 a579 \/ ssSkC0 \/ ssSkC2 \/ ssSkP0 a546 \/ ssSkP3 a546
% 0.71/0.86  |- c1_0 \/ c1_2 a567 a548 \/ c2_2 a567 a579 \/ c3_0 \/ c4_2 a567 a559 \/
% 0.71/0.86     c5_2 a567 a579 \/ ssSkC2 \/ ssSkC5 \/ ssSkP0 a567 \/ ssSkP3 a567
% 0.71/0.86  |- c1_2 a567 a548 \/ c2_2 a567 a579 \/ c4_2 a567 a559 \/ c5_0 \/
% 0.71/0.86     c5_2 a567 a579 \/ ssSkC2 \/ ssSkC5 \/ ssSkP0 a567 \/ ssSkP3 a567
% 0.71/0.86  |- c1_2 a567 a548 \/ c2_2 a567 a579 \/ c4_0 \/ c4_2 a567 a559 \/
% 0.71/0.86     c5_2 a567 a579 \/ ssSkC2 \/ ssSkC5 \/ ssSkP0 a567 \/ ssSkP3 a567
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.71/0.86     ~ndr1_1 a546 \/ c1_2 a546 a548 \/ c2_2 a546 a579 \/ c4_1 a546 \/
% 0.71/0.86     c4_2 a546 a559 \/ c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/ ssSkC0 \/
% 0.71/0.86     ssSkC2 \/ ssSkP0 a546 \/ ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a548 \/
% 0.71/0.86     c1_2 a581 a582 \/ c2_2 a546 a579 \/ c4_1 a546 \/ c4_2 a546 a559 \/
% 0.71/0.86     c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.86     ssSkP0 a546 \/ ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a548 \/
% 0.71/0.86     c2_2 a546 a579 \/ c4_1 a546 \/ c4_2 a546 a559 \/ c4_2 a546 a579 \/
% 0.71/0.86     c5_0 \/ c5_1 a546 \/ c5_2 a581 a582 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.86     ssSkP0 a546 \/ ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.71/0.86     c1_2 a546 a548 \/ c2_2 a546 a579 \/ c4_1 a546 \/ c4_2 a546 a559 \/
% 0.71/0.86     c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.86     ssSkP0 a546 \/ ssSkP3 a546
% 0.71/0.86  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a548 \/
% 0.71/0.86     c2_2 a546 a579 \/ c3_1 a581 \/ c4_1 a546 \/ c4_2 a546 a559 \/
% 0.71/0.86     c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.86     ssSkP0 a546 \/ ssSkP3 a546
% 0.71/0.87  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a548 \/
% 0.71/0.87     c2_2 a546 a579 \/ c4_1 a546 \/ c4_2 a546 a559 \/ c4_2 a546 a579 \/
% 0.71/0.87     c5_0 \/ c5_1 a546 \/ ndr1_1 a581 \/ ssSkC0 \/ ssSkC2 \/ ssSkP0 a546 \/
% 0.71/0.87     ssSkP3 a546
% 0.71/0.87  |- ~c2_0 \/ ~c4_2 a546 a570 \/ ~c5_1 a546 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.71/0.87     c1_2 a546 a548 \/ c2_2 a546 a579 \/ c4_2 a546 a559 \/ c5_0 \/ ssSkC0 \/
% 0.71/0.87     ssSkC2 \/ ssSkP0 a546 \/ ssSkP3 a546
% 0.71/0.87  |- ~c2_0 \/ ~c3_2 a546 a570 \/ ~c5_1 a546 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.71/0.87     c1_2 a546 a548 \/ c2_2 a546 a579 \/ c4_2 a546 a559 \/ c5_0 \/ ssSkC0 \/
% 0.71/0.87     ssSkC2 \/ ssSkP0 a546 \/ ssSkP3 a546
% 0.71/0.87  |- ~c2_0 \/ ~c2_2 a546 a570 \/ ~c5_1 a546 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.71/0.87     c1_2 a546 a548 \/ c2_2 a546 a579 \/ c4_2 a546 a559 \/ c5_0 \/ ssSkC0 \/
% 0.71/0.87     ssSkC2 \/ ssSkP0 a546 \/ ssSkP3 a546
% 0.71/0.87  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.71/0.87     ~ndr1_1 a546 \/ c1_2 a546 a548 \/ c2_2 a546 a579 \/ c4_0 \/ c4_1 a546 \/
% 0.71/0.87     c4_2 a546 a559 \/ c4_2 a546 a579 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.87     ssSkP0 a546 \/ ssSkP3 a546
% 0.71/0.87  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a548 \/
% 0.71/0.87     c1_2 a581 a582 \/ c2_2 a546 a579 \/ c4_0 \/ c4_1 a546 \/
% 0.71/0.87     c4_2 a546 a559 \/ c4_2 a546 a579 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.87     ssSkP0 a546 \/ ssSkP3 a546
% 0.71/0.87  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a548 \/
% 0.71/0.87     c2_2 a546 a579 \/ c4_0 \/ c4_1 a546 \/ c4_2 a546 a559 \/
% 0.71/0.87     c4_2 a546 a579 \/ c5_1 a546 \/ c5_2 a581 a582 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.87     ssSkP0 a546 \/ ssSkP3 a546
% 0.71/0.87  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.71/0.87     c1_2 a546 a548 \/ c2_2 a546 a579 \/ c4_0 \/ c4_1 a546 \/
% 0.71/0.87     c4_2 a546 a559 \/ c4_2 a546 a579 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.87     ssSkP0 a546 \/ ssSkP3 a546
% 0.71/0.87  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a548 \/
% 0.71/0.87     c2_2 a546 a579 \/ c3_1 a581 \/ c4_0 \/ c4_1 a546 \/ c4_2 a546 a559 \/
% 0.71/0.87     c4_2 a546 a579 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/ ssSkP0 a546 \/
% 0.71/0.87     ssSkP3 a546
% 0.71/0.87  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a548 \/
% 0.71/0.87     c2_2 a546 a579 \/ c4_0 \/ c4_1 a546 \/ c4_2 a546 a559 \/
% 0.71/0.87     c4_2 a546 a579 \/ c5_1 a546 \/ ndr1_1 a581 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.87     ssSkP0 a546 \/ ssSkP3 a546
% 0.71/0.87  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.71/0.87     ~ndr1_1 a567 \/ c1_2 a567 a548 \/ c2_2 a567 a579 \/ c4_1 a567 \/
% 0.71/0.87     c4_2 a567 a559 \/ c4_2 a567 a579 \/ c5_0 \/ c5_1 a567 \/ ssSkC2 \/
% 0.71/0.87     ssSkC5 \/ ssSkP0 a567 \/ ssSkP3 a567
% 0.71/0.87  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a548 \/
% 0.71/0.87     c1_2 a581 a582 \/ c2_2 a567 a579 \/ c4_1 a567 \/ c4_2 a567 a559 \/
% 0.71/0.87     c4_2 a567 a579 \/ c5_0 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/
% 0.71/0.87     ssSkP0 a567 \/ ssSkP3 a567
% 0.71/0.87  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a548 \/
% 0.71/0.87     c2_2 a567 a579 \/ c4_1 a567 \/ c4_2 a567 a559 \/ c4_2 a567 a579 \/
% 0.71/0.87     c5_0 \/ c5_1 a567 \/ c5_2 a581 a582 \/ ssSkC2 \/ ssSkC5 \/
% 0.71/0.87     ssSkP0 a567 \/ ssSkP3 a567
% 0.71/0.87  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/
% 0.71/0.87     c1_2 a567 a548 \/ c2_2 a567 a579 \/ c4_1 a567 \/ c4_2 a567 a559 \/
% 0.71/0.87     c4_2 a567 a579 \/ c5_0 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/
% 0.71/0.87     ssSkP0 a567 \/ ssSkP3 a567
% 0.71/0.87  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a548 \/
% 0.71/0.87     c2_2 a567 a579 \/ c3_1 a581 \/ c4_1 a567 \/ c4_2 a567 a559 \/
% 0.71/0.87     c4_2 a567 a579 \/ c5_0 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/
% 0.71/0.87     ssSkP0 a567 \/ ssSkP3 a567
% 0.71/0.87  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a548 \/
% 0.71/0.87     c2_2 a567 a579 \/ c4_1 a567 \/ c4_2 a567 a559 \/ c4_2 a567 a579 \/
% 0.71/0.87     c5_0 \/ c5_1 a567 \/ ndr1_1 a581 \/ ssSkC2 \/ ssSkC5 \/ ssSkP0 a567 \/
% 0.71/0.87     ssSkP3 a567
% 0.71/0.87  |- ~c2_0 \/ ~c4_2 a567 a570 \/ ~c5_1 a567 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/
% 0.71/0.87     c1_2 a567 a548 \/ c2_2 a567 a579 \/ c4_2 a567 a559 \/ c5_0 \/ ssSkC2 \/
% 0.71/0.87     ssSkC5 \/ ssSkP0 a567 \/ ssSkP3 a567
% 0.71/0.87  |- ~c2_0 \/ ~c3_2 a567 a570 \/ ~c5_1 a567 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/
% 0.71/0.87     c1_2 a567 a548 \/ c2_2 a567 a579 \/ c4_2 a567 a559 \/ c5_0 \/ ssSkC2 \/
% 0.71/0.87     ssSkC5 \/ ssSkP0 a567 \/ ssSkP3 a567
% 0.71/0.87  |- ~c2_0 \/ ~c2_2 a567 a570 \/ ~c5_1 a567 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/
% 0.71/0.87     c1_2 a567 a548 \/ c2_2 a567 a579 \/ c4_2 a567 a559 \/ c5_0 \/ ssSkC2 \/
% 0.71/0.87     ssSkC5 \/ ssSkP0 a567 \/ ssSkP3 a567
% 0.71/0.87  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.71/0.87     ~ndr1_1 a567 \/ c1_2 a567 a548 \/ c2_2 a567 a579 \/ c4_0 \/ c4_1 a567 \/
% 0.71/0.87     c4_2 a567 a559 \/ c4_2 a567 a579 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/
% 0.71/0.87     ssSkP0 a567 \/ ssSkP3 a567
% 0.71/0.87  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a548 \/
% 0.71/0.87     c1_2 a581 a582 \/ c2_2 a567 a579 \/ c4_0 \/ c4_1 a567 \/
% 0.71/0.87     c4_2 a567 a559 \/ c4_2 a567 a579 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/
% 0.71/0.87     ssSkP0 a567 \/ ssSkP3 a567
% 0.71/0.87  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a548 \/
% 0.71/0.87     c2_2 a567 a579 \/ c4_0 \/ c4_1 a567 \/ c4_2 a567 a559 \/
% 0.71/0.87     c4_2 a567 a579 \/ c5_1 a567 \/ c5_2 a581 a582 \/ ssSkC2 \/ ssSkC5 \/
% 0.71/0.87     ssSkP0 a567 \/ ssSkP3 a567
% 0.71/0.87  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/
% 0.71/0.87     c1_2 a567 a548 \/ c2_2 a567 a579 \/ c4_0 \/ c4_1 a567 \/
% 0.71/0.87     c4_2 a567 a559 \/ c4_2 a567 a579 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/
% 0.71/0.87     ssSkP0 a567 \/ ssSkP3 a567
% 0.71/0.87  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a548 \/
% 0.71/0.87     c2_2 a567 a579 \/ c3_1 a581 \/ c4_0 \/ c4_1 a567 \/ c4_2 a567 a559 \/
% 0.71/0.87     c4_2 a567 a579 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/ ssSkP0 a567 \/
% 0.71/0.87     ssSkP3 a567
% 0.71/0.87  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a548 \/
% 0.71/0.87     c2_2 a567 a579 \/ c4_0 \/ c4_1 a567 \/ c4_2 a567 a559 \/
% 0.71/0.87     c4_2 a567 a579 \/ c5_1 a567 \/ ndr1_1 a581 \/ ssSkC2 \/ ssSkC5 \/
% 0.71/0.87     ssSkP0 a567 \/ ssSkP3 a567
% 0.71/0.87  |- ~ndr1_0 \/ c1_2 a546 a562 \/ c2_2 a546 a579 \/ c4_2 a546 a559 \/
% 0.71/0.87     c5_2 a546 a579 \/ ssSkC0 \/ ssSkC2 \/ ssSkP2 a546 \/ ssSkP3 a546
% 0.71/0.87  |- ~ndr1_0 \/ c1_2 a567 a562 \/ c2_2 a567 a579 \/ c4_2 a567 a559 \/
% 0.71/0.87     c5_2 a567 a579 \/ ssSkC2 \/ ssSkC5 \/ ssSkP2 a567 \/ ssSkP3 a567
% 0.71/0.87  |- c1_0 \/ c1_2 a546 a562 \/ c2_2 a546 a579 \/ c3_0 \/ c4_2 a546 a559 \/
% 0.71/0.87     c5_2 a546 a579 \/ ssSkC0 \/ ssSkC2 \/ ssSkP2 a546 \/ ssSkP3 a546
% 0.71/0.87  |- c1_2 a546 a562 \/ c2_2 a546 a579 \/ c4_2 a546 a559 \/ c5_0 \/
% 0.71/0.87     c5_2 a546 a579 \/ ssSkC0 \/ ssSkC2 \/ ssSkP2 a546 \/ ssSkP3 a546
% 0.71/0.87  |- c1_2 a546 a562 \/ c2_2 a546 a579 \/ c4_0 \/ c4_2 a546 a559 \/
% 0.71/0.87     c5_2 a546 a579 \/ ssSkC0 \/ ssSkC2 \/ ssSkP2 a546 \/ ssSkP3 a546
% 0.71/0.87  |- c1_0 \/ c1_2 a567 a562 \/ c2_2 a567 a579 \/ c3_0 \/ c4_2 a567 a559 \/
% 0.71/0.87     c5_2 a567 a579 \/ ssSkC2 \/ ssSkC5 \/ ssSkP2 a567 \/ ssSkP3 a567
% 0.71/0.87  |- c1_2 a567 a562 \/ c2_2 a567 a579 \/ c4_2 a567 a559 \/ c5_0 \/
% 0.71/0.87     c5_2 a567 a579 \/ ssSkC2 \/ ssSkC5 \/ ssSkP2 a567 \/ ssSkP3 a567
% 0.71/0.87  |- c1_2 a567 a562 \/ c2_2 a567 a579 \/ c4_0 \/ c4_2 a567 a559 \/
% 0.71/0.87     c5_2 a567 a579 \/ ssSkC2 \/ ssSkC5 \/ ssSkP2 a567 \/ ssSkP3 a567
% 0.71/0.87  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.71/0.87     ~ndr1_1 a546 \/ c1_2 a546 a562 \/ c2_2 a546 a579 \/ c4_1 a546 \/
% 0.71/0.87     c4_2 a546 a559 \/ c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/ ssSkC0 \/
% 0.71/0.87     ssSkC2 \/ ssSkP2 a546 \/ ssSkP3 a546
% 0.71/0.87  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a562 \/
% 0.71/0.87     c1_2 a581 a582 \/ c2_2 a546 a579 \/ c4_1 a546 \/ c4_2 a546 a559 \/
% 0.71/0.87     c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.87     ssSkP2 a546 \/ ssSkP3 a546
% 0.71/0.87  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a562 \/
% 0.71/0.87     c2_2 a546 a579 \/ c4_1 a546 \/ c4_2 a546 a559 \/ c4_2 a546 a579 \/
% 0.71/0.87     c5_0 \/ c5_1 a546 \/ c5_2 a581 a582 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.87     ssSkP2 a546 \/ ssSkP3 a546
% 0.71/0.87  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.71/0.87     c1_2 a546 a562 \/ c2_2 a546 a579 \/ c4_1 a546 \/ c4_2 a546 a559 \/
% 0.71/0.87     c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.87     ssSkP2 a546 \/ ssSkP3 a546
% 0.71/0.87  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a562 \/
% 0.71/0.87     c2_2 a546 a579 \/ c3_1 a581 \/ c4_1 a546 \/ c4_2 a546 a559 \/
% 0.71/0.87     c4_2 a546 a579 \/ c5_0 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.87     ssSkP2 a546 \/ ssSkP3 a546
% 0.71/0.87  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a562 \/
% 0.71/0.87     c2_2 a546 a579 \/ c4_1 a546 \/ c4_2 a546 a559 \/ c4_2 a546 a579 \/
% 0.71/0.87     c5_0 \/ c5_1 a546 \/ ndr1_1 a581 \/ ssSkC0 \/ ssSkC2 \/ ssSkP2 a546 \/
% 0.71/0.87     ssSkP3 a546
% 0.71/0.87  |- ~c2_0 \/ ~c4_2 a546 a570 \/ ~c5_1 a546 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.71/0.87     c1_2 a546 a562 \/ c2_2 a546 a579 \/ c4_2 a546 a559 \/ c5_0 \/ ssSkC0 \/
% 0.71/0.87     ssSkC2 \/ ssSkP2 a546 \/ ssSkP3 a546
% 0.71/0.87  |- ~c2_0 \/ ~c3_2 a546 a570 \/ ~c5_1 a546 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.71/0.87     c1_2 a546 a562 \/ c2_2 a546 a579 \/ c4_2 a546 a559 \/ c5_0 \/ ssSkC0 \/
% 0.71/0.87     ssSkC2 \/ ssSkP2 a546 \/ ssSkP3 a546
% 0.71/0.87  |- ~c2_0 \/ ~c2_2 a546 a570 \/ ~c5_1 a546 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.71/0.87     c1_2 a546 a562 \/ c2_2 a546 a579 \/ c4_2 a546 a559 \/ c5_0 \/ ssSkC0 \/
% 0.71/0.87     ssSkC2 \/ ssSkP2 a546 \/ ssSkP3 a546
% 0.71/0.87  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.71/0.87     ~ndr1_1 a546 \/ c1_2 a546 a562 \/ c2_2 a546 a579 \/ c4_0 \/ c4_1 a546 \/
% 0.71/0.87     c4_2 a546 a559 \/ c4_2 a546 a579 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.87     ssSkP2 a546 \/ ssSkP3 a546
% 0.71/0.87  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a562 \/
% 0.71/0.87     c1_2 a581 a582 \/ c2_2 a546 a579 \/ c4_0 \/ c4_1 a546 \/
% 0.71/0.87     c4_2 a546 a559 \/ c4_2 a546 a579 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.87     ssSkP2 a546 \/ ssSkP3 a546
% 0.71/0.87  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a562 \/
% 0.71/0.87     c2_2 a546 a579 \/ c4_0 \/ c4_1 a546 \/ c4_2 a546 a559 \/
% 0.71/0.87     c4_2 a546 a579 \/ c5_1 a546 \/ c5_2 a581 a582 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.87     ssSkP2 a546 \/ ssSkP3 a546
% 0.71/0.87  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.71/0.87     c1_2 a546 a562 \/ c2_2 a546 a579 \/ c4_0 \/ c4_1 a546 \/
% 0.71/0.87     c4_2 a546 a559 \/ c4_2 a546 a579 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.87     ssSkP2 a546 \/ ssSkP3 a546
% 0.71/0.87  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a562 \/
% 0.71/0.87     c2_2 a546 a579 \/ c3_1 a581 \/ c4_0 \/ c4_1 a546 \/ c4_2 a546 a559 \/
% 0.71/0.87     c4_2 a546 a579 \/ c5_1 a546 \/ ssSkC0 \/ ssSkC2 \/ ssSkP2 a546 \/
% 0.71/0.87     ssSkP3 a546
% 0.71/0.87  |- ~c1_2 a546 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a562 \/
% 0.71/0.87     c2_2 a546 a579 \/ c4_0 \/ c4_1 a546 \/ c4_2 a546 a559 \/
% 0.71/0.87     c4_2 a546 a579 \/ c5_1 a546 \/ ndr1_1 a581 \/ ssSkC0 \/ ssSkC2 \/
% 0.71/0.87     ssSkP2 a546 \/ ssSkP3 a546
% 0.71/0.87  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.71/0.87     ~ndr1_1 a567 \/ c1_2 a567 a562 \/ c2_2 a567 a579 \/ c4_1 a567 \/
% 0.71/0.87     c4_2 a567 a559 \/ c4_2 a567 a579 \/ c5_0 \/ c5_1 a567 \/ ssSkC2 \/
% 0.71/0.87     ssSkC5 \/ ssSkP2 a567 \/ ssSkP3 a567
% 0.71/0.87  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a562 \/
% 0.71/0.87     c1_2 a581 a582 \/ c2_2 a567 a579 \/ c4_1 a567 \/ c4_2 a567 a559 \/
% 0.71/0.87     c4_2 a567 a579 \/ c5_0 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/
% 0.71/0.87     ssSkP2 a567 \/ ssSkP3 a567
% 0.71/0.87  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a562 \/
% 0.71/0.87     c2_2 a567 a579 \/ c4_1 a567 \/ c4_2 a567 a559 \/ c4_2 a567 a579 \/
% 0.71/0.87     c5_0 \/ c5_1 a567 \/ c5_2 a581 a582 \/ ssSkC2 \/ ssSkC5 \/
% 0.71/0.87     ssSkP2 a567 \/ ssSkP3 a567
% 0.71/0.87  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/
% 0.71/0.87     c1_2 a567 a562 \/ c2_2 a567 a579 \/ c4_1 a567 \/ c4_2 a567 a559 \/
% 0.71/0.87     c4_2 a567 a579 \/ c5_0 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/
% 0.71/0.87     ssSkP2 a567 \/ ssSkP3 a567
% 0.71/0.87  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a562 \/
% 0.71/0.87     c2_2 a567 a579 \/ c3_1 a581 \/ c4_1 a567 \/ c4_2 a567 a559 \/
% 0.71/0.87     c4_2 a567 a579 \/ c5_0 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/
% 0.71/0.87     ssSkP2 a567 \/ ssSkP3 a567
% 0.71/0.87  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a562 \/
% 0.71/0.87     c2_2 a567 a579 \/ c4_1 a567 \/ c4_2 a567 a559 \/ c4_2 a567 a579 \/
% 0.71/0.87     c5_0 \/ c5_1 a567 \/ ndr1_1 a581 \/ ssSkC2 \/ ssSkC5 \/ ssSkP2 a567 \/
% 0.71/0.87     ssSkP3 a567
% 0.71/0.87  |- ~c2_0 \/ ~c4_2 a567 a570 \/ ~c5_1 a567 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/
% 0.71/0.87     c1_2 a567 a562 \/ c2_2 a567 a579 \/ c4_2 a567 a559 \/ c5_0 \/ ssSkC2 \/
% 0.71/0.87     ssSkC5 \/ ssSkP2 a567 \/ ssSkP3 a567
% 0.71/0.87  |- ~c2_0 \/ ~c3_2 a567 a570 \/ ~c5_1 a567 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/
% 0.71/0.87     c1_2 a567 a562 \/ c2_2 a567 a579 \/ c4_2 a567 a559 \/ c5_0 \/ ssSkC2 \/
% 0.71/0.87     ssSkC5 \/ ssSkP2 a567 \/ ssSkP3 a567
% 0.71/0.87  |- ~c2_0 \/ ~c2_2 a567 a570 \/ ~c5_1 a567 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/
% 0.71/0.87     c1_2 a567 a562 \/ c2_2 a567 a579 \/ c4_2 a567 a559 \/ c5_0 \/ ssSkC2 \/
% 0.71/0.87     ssSkC5 \/ ssSkP2 a567 \/ ssSkP3 a567
% 0.71/0.87  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.71/0.87     ~ndr1_1 a567 \/ c1_2 a567 a562 \/ c2_2 a567 a579 \/ c4_0 \/ c4_1 a567 \/
% 0.71/0.87     c4_2 a567 a559 \/ c4_2 a567 a579 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/
% 0.71/0.87     ssSkP2 a567 \/ ssSkP3 a567
% 0.71/0.87  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a562 \/
% 0.71/0.87     c1_2 a581 a582 \/ c2_2 a567 a579 \/ c4_0 \/ c4_1 a567 \/
% 0.71/0.87     c4_2 a567 a559 \/ c4_2 a567 a579 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/
% 0.71/0.87     ssSkP2 a567 \/ ssSkP3 a567
% 0.71/0.87  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a562 \/
% 0.71/0.87     c2_2 a567 a579 \/ c4_0 \/ c4_1 a567 \/ c4_2 a567 a559 \/
% 0.71/0.87     c4_2 a567 a579 \/ c5_1 a567 \/ c5_2 a581 a582 \/ ssSkC2 \/ ssSkC5 \/
% 0.71/0.87     ssSkP2 a567 \/ ssSkP3 a567
% 0.71/0.87  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/
% 0.71/0.87     c1_2 a567 a562 \/ c2_2 a567 a579 \/ c4_0 \/ c4_1 a567 \/
% 0.71/0.87     c4_2 a567 a559 \/ c4_2 a567 a579 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/
% 0.71/0.87     ssSkP2 a567 \/ ssSkP3 a567
% 0.71/0.87  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a562 \/
% 0.71/0.87     c2_2 a567 a579 \/ c3_1 a581 \/ c4_0 \/ c4_1 a567 \/ c4_2 a567 a559 \/
% 0.71/0.87     c4_2 a567 a579 \/ c5_1 a567 \/ ssSkC2 \/ ssSkC5 \/ ssSkP2 a567 \/
% 0.71/0.87     ssSkP3 a567
% 0.71/0.87  |- ~c1_2 a567 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a562 \/
% 0.71/0.87     c2_2 a567 a579 \/ c4_0 \/ c4_1 a567 \/ c4_2 a567 a559 \/
% 0.71/0.87     c4_2 a567 a579 \/ c5_1 a567 \/ ndr1_1 a581 \/ ssSkC2 \/ ssSkC5 \/
% 0.71/0.87     ssSkP2 a567 \/ ssSkP3 a567
% 0.71/0.87  |- ~c1_2 $_176 a559 \/ ~c2_2 $_176 $_178 \/ ~ndr1_0 \/ ~ndr1_1 $_176 \/
% 0.71/0.87     c1_2 $_176 $_178 \/ c2_2 $_176 a579 \/ c5_2 $_176 a579 \/ ssSkC2 \/
% 0.71/0.87     ssSkP3 $_176
% 0.71/0.87  |- ~c1_2 a546 a559 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a547 \/
% 0.71/0.87     c2_2 a546 a579 \/ c5_2 a546 a579 \/ ssSkC0 \/ ssSkC2 \/ ssSkP3 a546
% 0.71/0.87  |- ~c1_2 a546 a559 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_0 \/ c1_2 a546 a576 \/
% 0.71/0.87     c2_2 a546 a579 \/ c3_0 \/ c3_1 a546 \/ c5_2 a546 a579 \/ ssSkC0 \/
% 0.71/0.87     ssSkC2 \/ ssSkC6 \/ ssSkP3 a546
% 0.71/0.87  |- ~c1_2 a546 a559 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a576 \/
% 0.71/0.87     c2_2 a546 a579 \/ c3_1 a546 \/ c4_0 \/ c5_2 a546 a579 \/ ssSkC0 \/
% 0.71/0.87     ssSkC2 \/ ssSkC6 \/ ssSkP3 a546
% 0.71/0.87  |- ~c1_2 a546 a559 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/ c1_2 a546 a576 \/
% 0.71/0.87     c2_2 a546 a579 \/ c3_1 a546 \/ c5_0 \/ c5_2 a546 a579 \/ ssSkC0 \/
% 0.71/0.87     ssSkC2 \/ ssSkC6 \/ ssSkP3 a546
% 0.71/0.87  |- ~c1_2 a567 a559 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_0 \/ c1_2 a567 a576 \/
% 0.71/0.87     c2_2 a567 a579 \/ c3_0 \/ c3_1 a567 \/ c5_2 a567 a579 \/ ssSkC2 \/
% 0.71/0.87     ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.71/0.87  |- ~c1_2 a567 a559 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a576 \/
% 0.71/0.87     c2_2 a567 a579 \/ c3_1 a567 \/ c4_0 \/ c5_2 a567 a579 \/ ssSkC2 \/
% 0.71/0.87     ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.71/0.87  |- ~c1_2 a567 a559 \/ ~ndr1_0 \/ ~ndr1_1 a567 \/ c1_2 a567 a576 \/
% 0.71/0.87     c2_2 a567 a579 \/ c3_1 a567 \/ c5_0 \/ c5_2 a567 a579 \/ ssSkC2 \/
% 0.71/0.87     ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.71/0.87  |- ~c1_2 $_179 a559 \/ ~ndr1_0 \/ ~ndr1_1 $_179 \/ c1_2 $_179 a548 \/
% 0.71/0.87     c2_2 $_179 a579 \/ c5_2 $_179 a579 \/ ssSkC2 \/ ssSkP0 $_179 \/
% 0.71/0.87     ssSkP3 $_179
% 0.71/0.87  |- ~c1_2 $_179 a559 \/ ~ndr1_0 \/ ~ndr1_1 $_179 \/ c1_2 $_179 a562 \/
% 0.71/0.87     c2_2 $_179 a579 \/ c5_2 $_179 a579 \/ ssSkC2 \/ ssSkP2 $_179 \/
% 0.71/0.87     ssSkP3 $_179
% 0.71/0.87  |- ~c1_1 a578 \/ ~c2_1 $_184 \/ ~c5_1 $_184 \/ ~ndr1_0 \/ c1_0 \/ c3_0 \/
% 0.71/0.87     c3_1 a578 \/ c3_2 a578 a548 \/ c4_2 a578 a566 \/ ssSkC4 \/ ssSkP0 a578
% 0.71/0.87  |- ~c1_1 a578 \/ ~c2_1 a556 \/ ~ndr1_0 \/ c1_0 \/ c3_0 \/ c3_1 a578 \/
% 0.71/0.87     c3_2 a578 a548 \/ c4_2 a578 a566 \/ ssSkC1 \/ ssSkC4 \/ ssSkP0 a578
% 0.71/0.87  |- ~c1_1 a578 \/ ~c2_1 a578 \/ ~ndr1_0 \/ c1_0 \/ c3_0 \/ c3_1 a578 \/
% 0.71/0.87     c3_2 a578 a548 \/ c4_2 a578 a566 \/ ssSkC4 \/ ssSkP0 a578
% 0.71/0.87  |- ~c1_1 a578 \/ ~c2_1 a583 \/ ~ndr1_0 \/ c1_0 \/ c3_0 \/ c3_1 a578 \/
% 0.71/0.87     c3_2 a578 a548 \/ c4_2 a578 a566 \/ ssSkC4 \/ ssSkC7 \/ ssSkP0 a578
% 0.71/0.87  |- ~c3_0 \/ ~c5_1 $_188 \/ ~ndr1_0 \/ ~ndr1_1 $_188 \/ c1_1 $_190 \/
% 0.71/0.87     c3_2 $_188 a548 \/ c4_1 $_190 \/ c5_1 $_190 \/ c5_2 $_188 a586 \/
% 0.71/0.87     ssSkP0 $_188
% 0.71/0.87  |- ~c3_0 \/ ~c5_1 $_188 \/ ~ndr1_0 \/ ~ndr1_1 $_188 \/ c1_1 $_190 \/
% 0.71/0.87     c3_2 $_188 a562 \/ c4_1 $_190 \/ c5_1 $_190 \/ c5_2 $_188 a586 \/
% 0.71/0.87     ssSkP2 $_188
% 0.71/0.87  |- ~c3_0 \/ ~c5_1 a546 \/ ~ndr1_0 \/ c1_1 $_191 \/ c3_2 a546 a547 \/
% 0.71/0.87     c4_1 $_191 \/ c5_1 $_191 \/ c5_2 a546 a586 \/ ssSkC0
% 0.71/0.87  |- ~c3_0 \/ ~c5_1 a546 \/ ~ndr1_0 \/ c1_1 $_194 \/ c3_2 a546 a548 \/
% 0.71/0.87     c4_1 $_194 \/ c5_1 $_194 \/ c5_2 a546 a586 \/ ssSkC0 \/ ssSkP0 a546
% 0.71/0.87  |- ~c3_0 \/ ~c5_1 a567 \/ ~ndr1_0 \/ c1_1 $_194 \/ c3_2 a567 a548 \/
% 0.71/0.87     c4_1 $_194 \/ c5_1 $_194 \/ c5_2 a567 a586 \/ ssSkC5 \/ ssSkP0 a567
% 0.71/0.87  |- ~c3_0 \/ ~c5_1 $_193 \/ ~ndr1_0 \/ c1_1 $_194 \/ c3_1 $_193 \/
% 0.71/0.87     c3_2 $_193 a548 \/ c4_0 \/ c4_1 $_194 \/ c5_1 $_194 \/
% 0.71/0.87     c5_2 $_193 a586 \/ ssSkC4 \/ ssSkP0 $_193
% 0.71/0.87  |- ~c3_0 \/ ~c5_1 $_193 \/ ~ndr1_0 \/ c1_1 $_194 \/ c3_1 $_193 \/
% 0.71/0.87     c3_2 $_193 a548 \/ c4_1 $_194 \/ c5_0 \/ c5_1 $_194 \/
% 0.71/0.87     c5_2 $_193 a586 \/ ssSkC4 \/ ssSkP0 $_193
% 0.71/0.87  |- ~c3_0 \/ ~c5_1 a546 \/ ~ndr1_0 \/ c1_1 $_198 \/ c3_2 a546 a562 \/
% 0.71/0.87     c4_1 $_198 \/ c5_1 $_198 \/ c5_2 a546 a586 \/ ssSkC0 \/ ssSkP2 a546
% 0.71/0.87  |- ~c3_0 \/ ~c5_1 a567 \/ ~ndr1_0 \/ c1_1 $_198 \/ c3_2 a567 a562 \/
% 0.71/0.87     c4_1 $_198 \/ c5_1 $_198 \/ c5_2 a567 a586 \/ ssSkC5 \/ ssSkP2 a567
% 0.71/0.87  |- ~c3_0 \/ ~c5_1 $_197 \/ ~ndr1_0 \/ c1_1 $_198 \/ c3_1 $_197 \/
% 0.71/0.87     c3_2 $_197 a562 \/ c4_0 \/ c4_1 $_198 \/ c5_1 $_198 \/
% 0.71/0.87     c5_2 $_197 a586 \/ ssSkC4 \/ ssSkP2 $_197
% 0.71/0.87  |- ~c3_0 \/ ~c5_1 $_197 \/ ~ndr1_0 \/ c1_1 $_198 \/ c3_1 $_197 \/
% 0.71/0.87     c3_2 $_197 a562 \/ c4_1 $_198 \/ c5_0 \/ c5_1 $_198 \/
% 0.71/0.87     c5_2 $_197 a586 \/ ssSkC4 \/ ssSkP2 $_197
% 0.71/0.87  |- ~c3_0 \/ ~c4_2 a546 a586 \/ ~c5_1 a546 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.71/0.87     c1_1 $_203 \/ c3_2 a546 a547 \/ c4_1 $_203 \/ c5_1 $_203 \/ ssSkC0
% 0.71/0.87  |- ~c3_0 \/ ~c4_2 $_201 a586 \/ ~c5_1 $_201 \/ ~ndr1_0 \/ ~ndr1_1 $_201 \/
% 0.71/0.87     c1_1 $_203 \/ c3_2 $_201 a548 \/ c4_1 $_203 \/ c5_1 $_203 \/
% 0.71/0.87     ssSkP0 $_201
% 0.71/0.87  |- ~c3_0 \/ ~c4_2 $_201 a586 \/ ~c5_1 $_201 \/ ~ndr1_0 \/ ~ndr1_1 $_201 \/
% 0.71/0.87     c1_1 $_203 \/ c3_2 $_201 a562 \/ c4_1 $_203 \/ c5_1 $_203 \/
% 0.71/0.87     ssSkP2 $_201
% 0.71/0.87  |- ~c1_2 a546 a586 \/ ~c3_0 \/ ~c5_1 a546 \/ ~ndr1_0 \/ ~ndr1_1 a546 \/
% 0.71/0.87     c1_1 $_211 \/ c3_2 a546 a547 \/ c4_1 $_211 \/ c5_1 $_211 \/ ssSkC0
% 0.71/0.87  |- ~c1_2 $_209 a586 \/ ~c3_0 \/ ~c5_1 $_209 \/ ~ndr1_0 \/ ~ndr1_1 $_209 \/
% 0.71/0.87     c1_1 $_211 \/ c3_2 $_209 a548 \/ c4_1 $_211 \/ c5_1 $_211 \/
% 0.71/0.87     ssSkP0 $_209
% 0.71/0.87  |- ~c1_2 $_209 a586 \/ ~c3_0 \/ ~c5_1 $_209 \/ ~ndr1_0 \/ ~ndr1_1 $_209 \/
% 0.71/0.87     c1_1 $_211 \/ c3_2 $_209 a562 \/ c4_1 $_211 \/ c5_1 $_211 \/
% 0.71/0.87     ssSkP2 $_209
% 0.71/0.87  |- c1_2 $_229 a548 \/ c2_2 $_229 a579 \/ c3_1 $_229 \/ c3_2 $_229 a559 \/
% 0.71/0.87     c4_0 \/ c5_2 $_229 a579 \/ ssSkC2 \/ ssSkC4 \/ ssSkP0 $_229 \/
% 0.71/0.87     ssSkP3 $_229
% 0.71/0.87  |- ~c1_2 $_230 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.71/0.87     ~ndr1_1 $_230 \/ c1_2 $_230 a548 \/ c2_2 $_230 a579 \/ c3_1 $_230 \/
% 0.71/0.87     c3_2 $_230 a559 \/ c4_0 \/ c4_1 $_230 \/ c4_2 $_230 a579 \/
% 0.71/0.87     c5_1 $_230 \/ ssSkC2 \/ ssSkC4 \/ ssSkP0 $_230 \/ ssSkP3 $_230
% 0.71/0.87  |- ~c1_2 $_230 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_230 \/
% 0.71/0.87     c1_2 $_230 a548 \/ c1_2 a581 a582 \/ c2_2 $_230 a579 \/ c3_1 $_230 \/
% 0.71/0.87     c3_2 $_230 a559 \/ c4_0 \/ c4_1 $_230 \/ c4_2 $_230 a579 \/
% 0.71/0.87     c5_1 $_230 \/ ssSkC2 \/ ssSkC4 \/ ssSkP0 $_230 \/ ssSkP3 $_230
% 0.71/0.87  |- ~c1_2 $_230 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_230 \/
% 0.71/0.87     c1_2 $_230 a548 \/ c2_2 $_230 a579 \/ c3_1 $_230 \/ c3_2 $_230 a559 \/
% 0.71/0.87     c4_0 \/ c4_1 $_230 \/ c4_2 $_230 a579 \/ c5_1 $_230 \/ c5_2 a581 a582 \/
% 0.71/0.87     ssSkC2 \/ ssSkC4 \/ ssSkP0 $_230 \/ ssSkP3 $_230
% 0.71/0.87  |- ~c1_2 $_230 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 $_230 \/
% 0.71/0.87     c1_2 $_230 a548 \/ c2_2 $_230 a579 \/ c3_1 $_230 \/ c3_2 $_230 a559 \/
% 0.71/0.87     c4_0 \/ c4_1 $_230 \/ c4_2 $_230 a579 \/ c5_1 $_230 \/ ssSkC2 \/
% 0.71/0.87     ssSkC4 \/ ssSkP0 $_230 \/ ssSkP3 $_230
% 0.71/0.87  |- ~c1_2 $_230 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_230 \/
% 0.71/0.87     c1_2 $_230 a548 \/ c2_2 $_230 a579 \/ c3_1 $_230 \/ c3_1 a581 \/
% 0.71/0.87     c3_2 $_230 a559 \/ c4_0 \/ c4_1 $_230 \/ c4_2 $_230 a579 \/
% 0.71/0.87     c5_1 $_230 \/ ssSkC2 \/ ssSkC4 \/ ssSkP0 $_230 \/ ssSkP3 $_230
% 0.71/0.87  |- ~c1_2 $_230 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_230 \/
% 0.71/0.87     c1_2 $_230 a548 \/ c2_2 $_230 a579 \/ c3_1 $_230 \/ c3_2 $_230 a559 \/
% 0.71/0.87     c4_0 \/ c4_1 $_230 \/ c4_2 $_230 a579 \/ c5_1 $_230 \/ ndr1_1 a581 \/
% 0.71/0.87     ssSkC2 \/ ssSkC4 \/ ssSkP0 $_230 \/ ssSkP3 $_230
% 0.71/0.87  |- c1_2 $_231 a548 \/ c2_2 $_231 a579 \/ c3_1 $_231 \/ c3_2 $_231 a559 \/
% 0.71/0.87     c5_0 \/ c5_2 $_231 a579 \/ ssSkC2 \/ ssSkC4 \/ ssSkP0 $_231 \/
% 0.71/0.87     ssSkP3 $_231
% 0.71/0.87  |- ~c1_2 $_232 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.71/0.87     ~ndr1_1 $_232 \/ c1_2 $_232 a548 \/ c2_2 $_232 a579 \/ c3_1 $_232 \/
% 0.71/0.87     c3_2 $_232 a559 \/ c4_1 $_232 \/ c4_2 $_232 a579 \/ c5_0 \/
% 0.71/0.87     c5_1 $_232 \/ ssSkC2 \/ ssSkC4 \/ ssSkP0 $_232 \/ ssSkP3 $_232
% 0.71/0.87  |- ~c1_2 $_232 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_232 \/
% 0.71/0.87     c1_2 $_232 a548 \/ c1_2 a581 a582 \/ c2_2 $_232 a579 \/ c3_1 $_232 \/
% 0.71/0.87     c3_2 $_232 a559 \/ c4_1 $_232 \/ c4_2 $_232 a579 \/ c5_0 \/
% 0.71/0.87     c5_1 $_232 \/ ssSkC2 \/ ssSkC4 \/ ssSkP0 $_232 \/ ssSkP3 $_232
% 0.71/0.87  |- ~c1_2 $_232 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_232 \/
% 0.71/0.87     c1_2 $_232 a548 \/ c2_2 $_232 a579 \/ c3_1 $_232 \/ c3_2 $_232 a559 \/
% 0.71/0.87     c4_1 $_232 \/ c4_2 $_232 a579 \/ c5_0 \/ c5_1 $_232 \/ c5_2 a581 a582 \/
% 0.71/0.87     ssSkC2 \/ ssSkC4 \/ ssSkP0 $_232 \/ ssSkP3 $_232
% 0.71/0.87  |- ~c1_2 $_232 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 $_232 \/
% 0.71/0.87     c1_2 $_232 a548 \/ c2_2 $_232 a579 \/ c3_1 $_232 \/ c3_2 $_232 a559 \/
% 0.71/0.87     c4_1 $_232 \/ c4_2 $_232 a579 \/ c5_0 \/ c5_1 $_232 \/ ssSkC2 \/
% 0.71/0.87     ssSkC4 \/ ssSkP0 $_232 \/ ssSkP3 $_232
% 0.71/0.87  |- ~c1_2 $_232 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_232 \/
% 0.71/0.87     c1_2 $_232 a548 \/ c2_2 $_232 a579 \/ c3_1 $_232 \/ c3_1 a581 \/
% 0.71/0.87     c3_2 $_232 a559 \/ c4_1 $_232 \/ c4_2 $_232 a579 \/ c5_0 \/
% 0.71/0.87     c5_1 $_232 \/ ssSkC2 \/ ssSkC4 \/ ssSkP0 $_232 \/ ssSkP3 $_232
% 0.71/0.87  |- ~c1_2 $_232 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_232 \/
% 0.71/0.87     c1_2 $_232 a548 \/ c2_2 $_232 a579 \/ c3_1 $_232 \/ c3_2 $_232 a559 \/
% 0.71/0.87     c4_1 $_232 \/ c4_2 $_232 a579 \/ c5_0 \/ c5_1 $_232 \/ ndr1_1 a581 \/
% 0.71/0.87     ssSkC2 \/ ssSkC4 \/ ssSkP0 $_232 \/ ssSkP3 $_232
% 0.71/0.87  |- ~c1_1 $_232 \/ ~c4_2 $_232 a579 \/ ~ndr1_0 \/ ~ndr1_1 $_232 \/
% 0.71/0.87     c1_2 $_232 a548 \/ c1_2 $_232 a579 \/ c2_1 $_232 \/ c2_2 $_232 a579 \/
% 0.71/0.87     c3_1 $_232 \/ c3_2 $_232 a559 \/ c5_0 \/ ssSkC2 \/ ssSkC4 \/
% 0.71/0.87     ssSkP0 $_232 \/ ssSkP3 $_232
% 0.71/0.87  |- ~c2_0 \/ ~c4_2 $_232 a570 \/ ~c5_1 $_232 \/ ~ndr1_0 \/ ~ndr1_1 $_232 \/
% 0.71/0.87     c1_2 $_232 a548 \/ c2_2 $_232 a579 \/ c3_1 $_232 \/ c3_2 $_232 a559 \/
% 0.71/0.87     c5_0 \/ ssSkC2 \/ ssSkC4 \/ ssSkP0 $_232 \/ ssSkP3 $_232
% 0.71/0.87  |- ~c2_0 \/ ~c3_2 $_232 a570 \/ ~c5_1 $_232 \/ ~ndr1_0 \/ ~ndr1_1 $_232 \/
% 0.71/0.87     c1_2 $_232 a548 \/ c2_2 $_232 a579 \/ c3_1 $_232 \/ c3_2 $_232 a559 \/
% 0.71/0.87     c5_0 \/ ssSkC2 \/ ssSkC4 \/ ssSkP0 $_232 \/ ssSkP3 $_232
% 0.71/0.87  |- ~c2_0 \/ ~c2_2 $_232 a570 \/ ~c5_1 $_232 \/ ~ndr1_0 \/ ~ndr1_1 $_232 \/
% 0.71/0.87     c1_2 $_232 a548 \/ c2_2 $_232 a579 \/ c3_1 $_232 \/ c3_2 $_232 a559 \/
% 0.71/0.87     c5_0 \/ ssSkC2 \/ ssSkC4 \/ ssSkP0 $_232 \/ ssSkP3 $_232
% 0.71/0.87  |- ~c4_0 \/ c1_2 a578 a548 \/ c2_2 a578 a579 \/ c3_0 \/ c3_1 a578 \/
% 0.71/0.87     c3_2 a578 a559 \/ c4_2 a578 a579 \/ c5_0 \/ ssSkC2 \/ ssSkC4 \/
% 0.71/0.87     ssSkP0 a578 \/ ssSkP3 a578
% 0.71/0.88  |- c1_2 $_233 a562 \/ c2_2 $_233 a579 \/ c3_1 $_233 \/ c3_2 $_233 a559 \/
% 0.71/0.88     c4_0 \/ c5_2 $_233 a579 \/ ssSkC2 \/ ssSkC4 \/ ssSkP2 $_233 \/
% 0.71/0.88     ssSkP3 $_233
% 0.71/0.88  |- ~c1_2 $_234 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.71/0.88     ~ndr1_1 $_234 \/ c1_2 $_234 a562 \/ c2_2 $_234 a579 \/ c3_1 $_234 \/
% 0.71/0.88     c3_2 $_234 a559 \/ c4_0 \/ c4_1 $_234 \/ c4_2 $_234 a579 \/
% 0.71/0.88     c5_1 $_234 \/ ssSkC2 \/ ssSkC4 \/ ssSkP2 $_234 \/ ssSkP3 $_234
% 0.71/0.88  |- ~c1_2 $_234 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_234 \/
% 0.71/0.88     c1_2 $_234 a562 \/ c1_2 a581 a582 \/ c2_2 $_234 a579 \/ c3_1 $_234 \/
% 0.71/0.88     c3_2 $_234 a559 \/ c4_0 \/ c4_1 $_234 \/ c4_2 $_234 a579 \/
% 0.71/0.88     c5_1 $_234 \/ ssSkC2 \/ ssSkC4 \/ ssSkP2 $_234 \/ ssSkP3 $_234
% 0.71/0.88  |- ~c1_2 $_234 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_234 \/
% 0.71/0.88     c1_2 $_234 a562 \/ c2_2 $_234 a579 \/ c3_1 $_234 \/ c3_2 $_234 a559 \/
% 0.71/0.88     c4_0 \/ c4_1 $_234 \/ c4_2 $_234 a579 \/ c5_1 $_234 \/ c5_2 a581 a582 \/
% 0.71/0.88     ssSkC2 \/ ssSkC4 \/ ssSkP2 $_234 \/ ssSkP3 $_234
% 0.71/0.88  |- ~c1_2 $_234 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 $_234 \/
% 0.71/0.88     c1_2 $_234 a562 \/ c2_2 $_234 a579 \/ c3_1 $_234 \/ c3_2 $_234 a559 \/
% 0.71/0.88     c4_0 \/ c4_1 $_234 \/ c4_2 $_234 a579 \/ c5_1 $_234 \/ ssSkC2 \/
% 0.71/0.88     ssSkC4 \/ ssSkP2 $_234 \/ ssSkP3 $_234
% 0.71/0.88  |- ~c1_2 $_234 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_234 \/
% 0.71/0.88     c1_2 $_234 a562 \/ c2_2 $_234 a579 \/ c3_1 $_234 \/ c3_1 a581 \/
% 0.71/0.88     c3_2 $_234 a559 \/ c4_0 \/ c4_1 $_234 \/ c4_2 $_234 a579 \/
% 0.71/0.88     c5_1 $_234 \/ ssSkC2 \/ ssSkC4 \/ ssSkP2 $_234 \/ ssSkP3 $_234
% 0.71/0.88  |- ~c1_2 $_234 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_234 \/
% 0.71/0.88     c1_2 $_234 a562 \/ c2_2 $_234 a579 \/ c3_1 $_234 \/ c3_2 $_234 a559 \/
% 0.71/0.88     c4_0 \/ c4_1 $_234 \/ c4_2 $_234 a579 \/ c5_1 $_234 \/ ndr1_1 a581 \/
% 0.71/0.88     ssSkC2 \/ ssSkC4 \/ ssSkP2 $_234 \/ ssSkP3 $_234
% 0.71/0.88  |- c1_2 $_235 a562 \/ c2_2 $_235 a579 \/ c3_1 $_235 \/ c3_2 $_235 a559 \/
% 0.71/0.88     c5_0 \/ c5_2 $_235 a579 \/ ssSkC2 \/ ssSkC4 \/ ssSkP2 $_235 \/
% 0.71/0.88     ssSkP3 $_235
% 0.71/0.88  |- ~c1_2 $_236 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.71/0.88     ~ndr1_1 $_236 \/ c1_2 $_236 a562 \/ c2_2 $_236 a579 \/ c3_1 $_236 \/
% 0.71/0.88     c3_2 $_236 a559 \/ c4_1 $_236 \/ c4_2 $_236 a579 \/ c5_0 \/
% 0.71/0.88     c5_1 $_236 \/ ssSkC2 \/ ssSkC4 \/ ssSkP2 $_236 \/ ssSkP3 $_236
% 0.71/0.88  |- ~c1_2 $_236 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_236 \/
% 0.71/0.88     c1_2 $_236 a562 \/ c1_2 a581 a582 \/ c2_2 $_236 a579 \/ c3_1 $_236 \/
% 0.71/0.88     c3_2 $_236 a559 \/ c4_1 $_236 \/ c4_2 $_236 a579 \/ c5_0 \/
% 0.71/0.88     c5_1 $_236 \/ ssSkC2 \/ ssSkC4 \/ ssSkP2 $_236 \/ ssSkP3 $_236
% 0.71/0.88  |- ~c1_2 $_236 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_236 \/
% 0.71/0.88     c1_2 $_236 a562 \/ c2_2 $_236 a579 \/ c3_1 $_236 \/ c3_2 $_236 a559 \/
% 0.71/0.88     c4_1 $_236 \/ c4_2 $_236 a579 \/ c5_0 \/ c5_1 $_236 \/ c5_2 a581 a582 \/
% 0.71/0.88     ssSkC2 \/ ssSkC4 \/ ssSkP2 $_236 \/ ssSkP3 $_236
% 0.71/0.88  |- ~c1_2 $_236 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 $_236 \/
% 0.71/0.88     c1_2 $_236 a562 \/ c2_2 $_236 a579 \/ c3_1 $_236 \/ c3_2 $_236 a559 \/
% 0.71/0.88     c4_1 $_236 \/ c4_2 $_236 a579 \/ c5_0 \/ c5_1 $_236 \/ ssSkC2 \/
% 0.71/0.88     ssSkC4 \/ ssSkP2 $_236 \/ ssSkP3 $_236
% 0.71/0.88  |- ~c1_2 $_236 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_236 \/
% 0.71/0.88     c1_2 $_236 a562 \/ c2_2 $_236 a579 \/ c3_1 $_236 \/ c3_1 a581 \/
% 0.71/0.88     c3_2 $_236 a559 \/ c4_1 $_236 \/ c4_2 $_236 a579 \/ c5_0 \/
% 0.71/0.88     c5_1 $_236 \/ ssSkC2 \/ ssSkC4 \/ ssSkP2 $_236 \/ ssSkP3 $_236
% 0.71/0.88  |- ~c1_2 $_236 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_236 \/
% 0.71/0.88     c1_2 $_236 a562 \/ c2_2 $_236 a579 \/ c3_1 $_236 \/ c3_2 $_236 a559 \/
% 0.71/0.88     c4_1 $_236 \/ c4_2 $_236 a579 \/ c5_0 \/ c5_1 $_236 \/ ndr1_1 a581 \/
% 0.71/0.88     ssSkC2 \/ ssSkC4 \/ ssSkP2 $_236 \/ ssSkP3 $_236
% 0.71/0.88  |- ~c1_1 $_236 \/ ~c4_2 $_236 a579 \/ ~ndr1_0 \/ ~ndr1_1 $_236 \/
% 0.71/0.88     c1_2 $_236 a562 \/ c1_2 $_236 a579 \/ c2_1 $_236 \/ c2_2 $_236 a579 \/
% 0.71/0.88     c3_1 $_236 \/ c3_2 $_236 a559 \/ c5_0 \/ ssSkC2 \/ ssSkC4 \/
% 0.71/0.88     ssSkP2 $_236 \/ ssSkP3 $_236
% 0.71/0.88  |- ~c2_0 \/ ~c4_2 $_236 a570 \/ ~c5_1 $_236 \/ ~ndr1_0 \/ ~ndr1_1 $_236 \/
% 0.71/0.88     c1_2 $_236 a562 \/ c2_2 $_236 a579 \/ c3_1 $_236 \/ c3_2 $_236 a559 \/
% 0.71/0.88     c5_0 \/ ssSkC2 \/ ssSkC4 \/ ssSkP2 $_236 \/ ssSkP3 $_236
% 0.71/0.88  |- ~c2_0 \/ ~c3_2 $_236 a570 \/ ~c5_1 $_236 \/ ~ndr1_0 \/ ~ndr1_1 $_236 \/
% 0.71/0.88     c1_2 $_236 a562 \/ c2_2 $_236 a579 \/ c3_1 $_236 \/ c3_2 $_236 a559 \/
% 0.71/0.88     c5_0 \/ ssSkC2 \/ ssSkC4 \/ ssSkP2 $_236 \/ ssSkP3 $_236
% 0.71/0.88  |- ~c2_0 \/ ~c2_2 $_236 a570 \/ ~c5_1 $_236 \/ ~ndr1_0 \/ ~ndr1_1 $_236 \/
% 0.71/0.88     c1_2 $_236 a562 \/ c2_2 $_236 a579 \/ c3_1 $_236 \/ c3_2 $_236 a559 \/
% 0.71/0.88     c5_0 \/ ssSkC2 \/ ssSkC4 \/ ssSkP2 $_236 \/ ssSkP3 $_236
% 0.71/0.88  |- ~c4_0 \/ c1_2 a578 a562 \/ c2_2 a578 a579 \/ c3_0 \/ c3_1 a578 \/
% 0.71/0.88     c3_2 a578 a559 \/ c4_2 a578 a579 \/ c5_0 \/ ssSkC2 \/ ssSkC4 \/
% 0.71/0.88     ssSkP2 a578 \/ ssSkP3 a578
% 0.71/0.88  |- c1_2 $_237 a548 \/ c2_2 $_237 a579 \/ c3_1 $_237 \/ c4_2 $_237 a559 \/
% 0.71/0.88     c5_0 \/ c5_2 $_237 a579 \/ ssSkC2 \/ ssSkC4 \/ ssSkP0 $_237 \/
% 0.71/0.88     ssSkP3 $_237
% 0.71/0.88  |- ~c1_2 $_238 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.71/0.88     ~ndr1_1 $_238 \/ c1_2 $_238 a548 \/ c2_2 $_238 a579 \/ c3_1 $_238 \/
% 0.71/0.88     c4_1 $_238 \/ c4_2 $_238 a559 \/ c4_2 $_238 a579 \/ c5_0 \/
% 0.71/0.88     c5_1 $_238 \/ ssSkC2 \/ ssSkC4 \/ ssSkP0 $_238 \/ ssSkP3 $_238
% 0.71/0.88  |- ~c1_2 $_238 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_238 \/
% 0.71/0.88     c1_2 $_238 a548 \/ c1_2 a581 a582 \/ c2_2 $_238 a579 \/ c3_1 $_238 \/
% 0.71/0.88     c4_1 $_238 \/ c4_2 $_238 a559 \/ c4_2 $_238 a579 \/ c5_0 \/
% 0.71/0.88     c5_1 $_238 \/ ssSkC2 \/ ssSkC4 \/ ssSkP0 $_238 \/ ssSkP3 $_238
% 0.71/0.88  |- ~c1_2 $_238 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_238 \/
% 0.71/0.88     c1_2 $_238 a548 \/ c2_2 $_238 a579 \/ c3_1 $_238 \/ c4_1 $_238 \/
% 0.71/0.88     c4_2 $_238 a559 \/ c4_2 $_238 a579 \/ c5_0 \/ c5_1 $_238 \/
% 0.71/0.88     c5_2 a581 a582 \/ ssSkC2 \/ ssSkC4 \/ ssSkP0 $_238 \/ ssSkP3 $_238
% 0.71/0.88  |- ~c1_2 $_238 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 $_238 \/
% 0.71/0.88     c1_2 $_238 a548 \/ c2_2 $_238 a579 \/ c3_1 $_238 \/ c4_1 $_238 \/
% 0.71/0.88     c4_2 $_238 a559 \/ c4_2 $_238 a579 \/ c5_0 \/ c5_1 $_238 \/ ssSkC2 \/
% 0.71/0.88     ssSkC4 \/ ssSkP0 $_238 \/ ssSkP3 $_238
% 0.71/0.88  |- ~c1_2 $_238 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_238 \/
% 0.71/0.88     c1_2 $_238 a548 \/ c2_2 $_238 a579 \/ c3_1 $_238 \/ c3_1 a581 \/
% 0.71/0.88     c4_1 $_238 \/ c4_2 $_238 a559 \/ c4_2 $_238 a579 \/ c5_0 \/
% 0.71/0.88     c5_1 $_238 \/ ssSkC2 \/ ssSkC4 \/ ssSkP0 $_238 \/ ssSkP3 $_238
% 0.71/0.88  |- ~c1_2 $_238 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_238 \/
% 0.71/0.88     c1_2 $_238 a548 \/ c2_2 $_238 a579 \/ c3_1 $_238 \/ c4_1 $_238 \/
% 0.71/0.88     c4_2 $_238 a559 \/ c4_2 $_238 a579 \/ c5_0 \/ c5_1 $_238 \/
% 0.71/0.88     ndr1_1 a581 \/ ssSkC2 \/ ssSkC4 \/ ssSkP0 $_238 \/ ssSkP3 $_238
% 0.71/0.88  |- ~c1_1 $_238 \/ ~c4_2 $_238 a579 \/ ~ndr1_0 \/ ~ndr1_1 $_238 \/
% 0.71/0.88     c1_2 $_238 a548 \/ c1_2 $_238 a579 \/ c2_1 $_238 \/ c2_2 $_238 a579 \/
% 0.71/0.88     c3_1 $_238 \/ c4_2 $_238 a559 \/ c5_0 \/ ssSkC2 \/ ssSkC4 \/
% 0.71/0.88     ssSkP0 $_238 \/ ssSkP3 $_238
% 0.71/0.88  |- ~c2_0 \/ ~c4_2 $_238 a570 \/ ~c5_1 $_238 \/ ~ndr1_0 \/ ~ndr1_1 $_238 \/
% 0.71/0.88     c1_2 $_238 a548 \/ c2_2 $_238 a579 \/ c3_1 $_238 \/ c4_2 $_238 a559 \/
% 0.71/0.88     c5_0 \/ ssSkC2 \/ ssSkC4 \/ ssSkP0 $_238 \/ ssSkP3 $_238
% 0.71/0.88  |- ~c2_0 \/ ~c3_2 $_238 a570 \/ ~c5_1 $_238 \/ ~ndr1_0 \/ ~ndr1_1 $_238 \/
% 0.71/0.88     c1_2 $_238 a548 \/ c2_2 $_238 a579 \/ c3_1 $_238 \/ c4_2 $_238 a559 \/
% 0.71/0.88     c5_0 \/ ssSkC2 \/ ssSkC4 \/ ssSkP0 $_238 \/ ssSkP3 $_238
% 0.71/0.88  |- ~c2_0 \/ ~c2_2 $_238 a570 \/ ~c5_1 $_238 \/ ~ndr1_0 \/ ~ndr1_1 $_238 \/
% 0.71/0.88     c1_2 $_238 a548 \/ c2_2 $_238 a579 \/ c3_1 $_238 \/ c4_2 $_238 a559 \/
% 0.71/0.88     c5_0 \/ ssSkC2 \/ ssSkC4 \/ ssSkP0 $_238 \/ ssSkP3 $_238
% 0.71/0.88  |- ~c4_0 \/ c1_2 a578 a548 \/ c2_2 a578 a579 \/ c3_0 \/ c3_1 a578 \/
% 0.71/0.88     c4_2 a578 a559 \/ c4_2 a578 a579 \/ c5_0 \/ ssSkC2 \/ ssSkC4 \/
% 0.71/0.88     ssSkP0 a578 \/ ssSkP3 a578
% 0.71/0.88  |- c1_2 $_239 a548 \/ c2_2 $_239 a579 \/ c3_1 $_239 \/ c4_0 \/
% 0.71/0.88     c4_2 $_239 a559 \/ c5_2 $_239 a579 \/ ssSkC2 \/ ssSkC4 \/
% 0.71/0.88     ssSkP0 $_239 \/ ssSkP3 $_239
% 0.71/0.88  |- ~c1_2 $_240 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.71/0.88     ~ndr1_1 $_240 \/ c1_2 $_240 a548 \/ c2_2 $_240 a579 \/ c3_1 $_240 \/
% 0.71/0.88     c4_0 \/ c4_1 $_240 \/ c4_2 $_240 a559 \/ c4_2 $_240 a579 \/
% 0.71/0.88     c5_1 $_240 \/ ssSkC2 \/ ssSkC4 \/ ssSkP0 $_240 \/ ssSkP3 $_240
% 0.71/0.88  |- ~c1_2 $_240 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_240 \/
% 0.71/0.88     c1_2 $_240 a548 \/ c1_2 a581 a582 \/ c2_2 $_240 a579 \/ c3_1 $_240 \/
% 0.71/0.88     c4_0 \/ c4_1 $_240 \/ c4_2 $_240 a559 \/ c4_2 $_240 a579 \/
% 0.71/0.88     c5_1 $_240 \/ ssSkC2 \/ ssSkC4 \/ ssSkP0 $_240 \/ ssSkP3 $_240
% 0.71/0.88  |- ~c1_2 $_240 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_240 \/
% 0.71/0.88     c1_2 $_240 a548 \/ c2_2 $_240 a579 \/ c3_1 $_240 \/ c4_0 \/
% 0.71/0.88     c4_1 $_240 \/ c4_2 $_240 a559 \/ c4_2 $_240 a579 \/ c5_1 $_240 \/
% 0.71/0.88     c5_2 a581 a582 \/ ssSkC2 \/ ssSkC4 \/ ssSkP0 $_240 \/ ssSkP3 $_240
% 0.71/0.88  |- ~c1_2 $_240 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 $_240 \/
% 0.71/0.88     c1_2 $_240 a548 \/ c2_2 $_240 a579 \/ c3_1 $_240 \/ c4_0 \/
% 0.71/0.88     c4_1 $_240 \/ c4_2 $_240 a559 \/ c4_2 $_240 a579 \/ c5_1 $_240 \/
% 0.71/0.88     ssSkC2 \/ ssSkC4 \/ ssSkP0 $_240 \/ ssSkP3 $_240
% 0.71/0.88  |- ~c1_2 $_240 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_240 \/
% 0.71/0.88     c1_2 $_240 a548 \/ c2_2 $_240 a579 \/ c3_1 $_240 \/ c3_1 a581 \/ c4_0 \/
% 0.71/0.88     c4_1 $_240 \/ c4_2 $_240 a559 \/ c4_2 $_240 a579 \/ c5_1 $_240 \/
% 0.71/0.88     ssSkC2 \/ ssSkC4 \/ ssSkP0 $_240 \/ ssSkP3 $_240
% 0.71/0.88  |- ~c1_2 $_240 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_240 \/
% 0.71/0.88     c1_2 $_240 a548 \/ c2_2 $_240 a579 \/ c3_1 $_240 \/ c4_0 \/
% 0.71/0.88     c4_1 $_240 \/ c4_2 $_240 a559 \/ c4_2 $_240 a579 \/ c5_1 $_240 \/
% 0.71/0.88     ndr1_1 a581 \/ ssSkC2 \/ ssSkC4 \/ ssSkP0 $_240 \/ ssSkP3 $_240
% 0.71/0.88  |- c1_2 $_241 a562 \/ c2_2 $_241 a579 \/ c3_1 $_241 \/ c4_2 $_241 a559 \/
% 0.71/0.88     c5_0 \/ c5_2 $_241 a579 \/ ssSkC2 \/ ssSkC4 \/ ssSkP2 $_241 \/
% 0.71/0.88     ssSkP3 $_241
% 0.71/0.88  |- ~c1_2 $_242 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.71/0.88     ~ndr1_1 $_242 \/ c1_2 $_242 a562 \/ c2_2 $_242 a579 \/ c3_1 $_242 \/
% 0.71/0.88     c4_1 $_242 \/ c4_2 $_242 a559 \/ c4_2 $_242 a579 \/ c5_0 \/
% 0.71/0.88     c5_1 $_242 \/ ssSkC2 \/ ssSkC4 \/ ssSkP2 $_242 \/ ssSkP3 $_242
% 0.71/0.88  |- ~c1_2 $_242 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_242 \/
% 0.71/0.88     c1_2 $_242 a562 \/ c1_2 a581 a582 \/ c2_2 $_242 a579 \/ c3_1 $_242 \/
% 0.71/0.88     c4_1 $_242 \/ c4_2 $_242 a559 \/ c4_2 $_242 a579 \/ c5_0 \/
% 0.71/0.88     c5_1 $_242 \/ ssSkC2 \/ ssSkC4 \/ ssSkP2 $_242 \/ ssSkP3 $_242
% 0.71/0.88  |- ~c1_2 $_242 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_242 \/
% 0.71/0.88     c1_2 $_242 a562 \/ c2_2 $_242 a579 \/ c3_1 $_242 \/ c4_1 $_242 \/
% 0.71/0.88     c4_2 $_242 a559 \/ c4_2 $_242 a579 \/ c5_0 \/ c5_1 $_242 \/
% 0.71/0.88     c5_2 a581 a582 \/ ssSkC2 \/ ssSkC4 \/ ssSkP2 $_242 \/ ssSkP3 $_242
% 0.71/0.88  |- ~c1_2 $_242 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 $_242 \/
% 0.71/0.88     c1_2 $_242 a562 \/ c2_2 $_242 a579 \/ c3_1 $_242 \/ c4_1 $_242 \/
% 0.71/0.88     c4_2 $_242 a559 \/ c4_2 $_242 a579 \/ c5_0 \/ c5_1 $_242 \/ ssSkC2 \/
% 0.71/0.88     ssSkC4 \/ ssSkP2 $_242 \/ ssSkP3 $_242
% 0.71/0.88  |- ~c1_2 $_242 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_242 \/
% 0.71/0.88     c1_2 $_242 a562 \/ c2_2 $_242 a579 \/ c3_1 $_242 \/ c3_1 a581 \/
% 0.71/0.88     c4_1 $_242 \/ c4_2 $_242 a559 \/ c4_2 $_242 a579 \/ c5_0 \/
% 0.71/0.88     c5_1 $_242 \/ ssSkC2 \/ ssSkC4 \/ ssSkP2 $_242 \/ ssSkP3 $_242
% 0.71/0.88  |- ~c1_2 $_242 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_242 \/
% 0.71/0.88     c1_2 $_242 a562 \/ c2_2 $_242 a579 \/ c3_1 $_242 \/ c4_1 $_242 \/
% 0.71/0.88     c4_2 $_242 a559 \/ c4_2 $_242 a579 \/ c5_0 \/ c5_1 $_242 \/
% 0.71/0.88     ndr1_1 a581 \/ ssSkC2 \/ ssSkC4 \/ ssSkP2 $_242 \/ ssSkP3 $_242
% 0.71/0.88  |- ~c1_1 $_242 \/ ~c4_2 $_242 a579 \/ ~ndr1_0 \/ ~ndr1_1 $_242 \/
% 0.71/0.88     c1_2 $_242 a562 \/ c1_2 $_242 a579 \/ c2_1 $_242 \/ c2_2 $_242 a579 \/
% 0.71/0.88     c3_1 $_242 \/ c4_2 $_242 a559 \/ c5_0 \/ ssSkC2 \/ ssSkC4 \/
% 0.71/0.88     ssSkP2 $_242 \/ ssSkP3 $_242
% 0.71/0.88  |- ~c2_0 \/ ~c4_2 $_242 a570 \/ ~c5_1 $_242 \/ ~ndr1_0 \/ ~ndr1_1 $_242 \/
% 0.71/0.88     c1_2 $_242 a562 \/ c2_2 $_242 a579 \/ c3_1 $_242 \/ c4_2 $_242 a559 \/
% 0.71/0.88     c5_0 \/ ssSkC2 \/ ssSkC4 \/ ssSkP2 $_242 \/ ssSkP3 $_242
% 0.71/0.88  |- ~c2_0 \/ ~c3_2 $_242 a570 \/ ~c5_1 $_242 \/ ~ndr1_0 \/ ~ndr1_1 $_242 \/
% 0.71/0.88     c1_2 $_242 a562 \/ c2_2 $_242 a579 \/ c3_1 $_242 \/ c4_2 $_242 a559 \/
% 0.71/0.88     c5_0 \/ ssSkC2 \/ ssSkC4 \/ ssSkP2 $_242 \/ ssSkP3 $_242
% 0.71/0.88  |- ~c2_0 \/ ~c2_2 $_242 a570 \/ ~c5_1 $_242 \/ ~ndr1_0 \/ ~ndr1_1 $_242 \/
% 0.71/0.88     c1_2 $_242 a562 \/ c2_2 $_242 a579 \/ c3_1 $_242 \/ c4_2 $_242 a559 \/
% 0.71/0.88     c5_0 \/ ssSkC2 \/ ssSkC4 \/ ssSkP2 $_242 \/ ssSkP3 $_242
% 0.71/0.88  |- ~c4_0 \/ c1_2 a578 a562 \/ c2_2 a578 a579 \/ c3_0 \/ c3_1 a578 \/
% 0.71/0.88     c4_2 a578 a559 \/ c4_2 a578 a579 \/ c5_0 \/ ssSkC2 \/ ssSkC4 \/
% 0.71/0.88     ssSkP2 a578 \/ ssSkP3 a578
% 0.71/0.88  |- c1_2 $_243 a562 \/ c2_2 $_243 a579 \/ c3_1 $_243 \/ c4_0 \/
% 0.71/0.88     c4_2 $_243 a559 \/ c5_2 $_243 a579 \/ ssSkC2 \/ ssSkC4 \/
% 0.71/0.88     ssSkP2 $_243 \/ ssSkP3 $_243
% 0.71/0.88  |- ~c1_2 $_244 a579 \/ ~c2_0 \/ ~c2_2 a581 a582 \/ ~ndr1_0 \/
% 0.71/0.88     ~ndr1_1 $_244 \/ c1_2 $_244 a562 \/ c2_2 $_244 a579 \/ c3_1 $_244 \/
% 0.71/0.88     c4_0 \/ c4_1 $_244 \/ c4_2 $_244 a559 \/ c4_2 $_244 a579 \/
% 0.71/0.88     c5_1 $_244 \/ ssSkC2 \/ ssSkC4 \/ ssSkP2 $_244 \/ ssSkP3 $_244
% 0.71/0.88  |- ~c1_2 $_244 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_244 \/
% 0.71/0.88     c1_2 $_244 a562 \/ c1_2 a581 a582 \/ c2_2 $_244 a579 \/ c3_1 $_244 \/
% 0.71/0.88     c4_0 \/ c4_1 $_244 \/ c4_2 $_244 a559 \/ c4_2 $_244 a579 \/
% 0.71/0.88     c5_1 $_244 \/ ssSkC2 \/ ssSkC4 \/ ssSkP2 $_244 \/ ssSkP3 $_244
% 0.71/0.88  |- ~c1_2 $_244 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_244 \/
% 0.71/0.88     c1_2 $_244 a562 \/ c2_2 $_244 a579 \/ c3_1 $_244 \/ c4_0 \/
% 0.71/0.88     c4_1 $_244 \/ c4_2 $_244 a559 \/ c4_2 $_244 a579 \/ c5_1 $_244 \/
% 0.71/0.88     c5_2 a581 a582 \/ ssSkC2 \/ ssSkC4 \/ ssSkP2 $_244 \/ ssSkP3 $_244
% 0.71/0.88  |- ~c1_2 $_244 a579 \/ ~c2_0 \/ ~c2_1 a581 \/ ~ndr1_0 \/ ~ndr1_1 $_244 \/
% 0.71/0.88     c1_2 $_244 a562 \/ c2_2 $_244 a579 \/ c3_1 $_244 \/ c4_0 \/
% 0.71/0.88     c4_1 $_244 \/ c4_2 $_244 a559 \/ c4_2 $_244 a579 \/ c5_1 $_244 \/
% 0.71/0.88     ssSkC2 \/ ssSkC4 \/ ssSkP2 $_244 \/ ssSkP3 $_244
% 0.71/0.88  |- ~c1_2 $_244 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_244 \/
% 0.71/0.88     c1_2 $_244 a562 \/ c2_2 $_244 a579 \/ c3_1 $_244 \/ c3_1 a581 \/ c4_0 \/
% 0.71/0.88     c4_1 $_244 \/ c4_2 $_244 a559 \/ c4_2 $_244 a579 \/ c5_1 $_244 \/
% 0.71/0.88     ssSkC2 \/ ssSkC4 \/ ssSkP2 $_244 \/ ssSkP3 $_244
% 0.71/0.88  |- ~c1_2 $_244 a579 \/ ~c2_0 \/ ~ndr1_0 \/ ~ndr1_1 $_244 \/
% 0.71/0.88     c1_2 $_244 a562 \/ c2_2 $_244 a579 \/ c3_1 $_244 \/ c4_0 \/
% 0.71/0.88     c4_1 $_244 \/ c4_2 $_244 a559 \/ c4_2 $_244 a579 \/ c5_1 $_244 \/
% 0.71/0.88     ndr1_1 a581 \/ ssSkC2 \/ ssSkC4 \/ ssSkP2 $_244 \/ ssSkP3 $_244
% 0.71/0.88  |- ~c3_1 $_245 \/ ~c4_1 $_246 \/ ~ndr1_0 \/ c3_1 $_246 \/ c4_0 \/
% 0.71/0.88     c5_1 $_246 \/ c5_2 $_246 a557 \/ ndr1_1 $_245 \/ ssSkC4 \/ ssSkP1 $_246
% 0.71/0.88  |- ~c3_1 $_249 \/ ~c4_1 $_250 \/ ~ndr1_0 \/ c3_1 $_250 \/ c5_0 \/
% 0.71/0.88     c5_1 $_250 \/ c5_2 $_250 a557 \/ ndr1_1 $_249 \/ ssSkC4 \/ ssSkP1 $_250
% 0.71/0.88  |- c1_0 \/ c1_2 $_259 a548 \/ c2_2 $_259 a579 \/ c3_0 \/ c3_1 $_259 \/
% 0.71/0.88     c3_2 $_259 a559 \/ c5_2 $_259 a579 \/ ssSkC2 \/ ssSkC4 \/
% 0.71/0.88     ssSkP0 $_259 \/ ssSkP3 $_259
% 0.71/0.88  |- c1_0 \/ c1_2 a578 a548 \/ c2_2 a578 a579 \/ c3_0 \/ c3_1 a578 \/
% 0.71/0.88     c3_2 a578 a559 \/ c4_2 a578 a579 \/ ssSkC2 \/ ssSkC4 \/ ssSkP0 a578 \/
% 0.71/0.88     ssSkP3 a578
% 0.71/0.88  |- c1_0 \/ c1_2 $_261 a562 \/ c2_2 $_261 a579 \/ c3_0 \/ c3_1 $_261 \/
% 0.71/0.88     c3_2 $_261 a559 \/ c5_2 $_261 a579 \/ ssSkC2 \/ ssSkC4 \/
% 0.71/0.88     ssSkP2 $_261 \/ ssSkP3 $_261
% 0.71/0.88  |- c1_0 \/ c1_2 $_263 a548 \/ c2_2 $_263 a579 \/ c3_0 \/ c3_1 $_263 \/
% 0.71/0.88     c4_2 $_263 a559 \/ c5_2 $_263 a579 \/ ssSkC2 \/ ssSkC4 \/
% 0.71/0.88     ssSkP0 $_263 \/ ssSkP3 $_263
% 0.71/0.88  |- c1_0 \/ c1_2 a578 a548 \/ c2_2 a578 a579 \/ c3_0 \/ c3_1 a578 \/
% 0.71/0.88     c4_2 a578 a559 \/ c4_2 a578 a579 \/ ssSkC2 \/ ssSkC4 \/ ssSkP0 a578 \/
% 0.71/0.88     ssSkP3 a578
% 0.71/0.88  |- c1_0 \/ c1_2 $_265 a562 \/ c2_2 $_265 a579 \/ c3_0 \/ c3_1 $_265 \/
% 0.71/0.88     c4_2 $_265 a559 \/ c5_2 $_265 a579 \/ ssSkC2 \/ ssSkC4 \/
% 0.71/0.88     ssSkP2 $_265 \/ ssSkP3 $_265
% 0.71/0.88  |- ~c3_1 $_267 \/ ~c4_1 $_268 \/ ~ndr1_0 \/ c1_0 \/ c3_0 \/ c3_1 $_268 \/
% 0.71/0.88     c5_1 $_268 \/ c5_2 $_268 a557 \/ ndr1_1 $_267 \/ ssSkC4 \/ ssSkP1 $_268
% 0.71/0.88  |- ~c3_0 \/ c1_1 $_273 \/ c3_1 a556 \/ c3_2 a556 a548 \/ c4_0 \/
% 0.71/0.88     c4_1 $_273 \/ c5_1 $_273 \/ c5_2 a556 a586 \/ ssSkC1 \/ ssSkC4 \/
% 0.71/0.88     ssSkP0 a556
% 0.71/0.88  |- ~c3_0 \/ c1_1 $_277 \/ c3_1 a556 \/ c3_2 a556 a548 \/ c4_1 $_277 \/
% 0.71/0.88     c5_0 \/ c5_1 $_277 \/ c5_2 a556 a586 \/ ssSkC1 \/ ssSkC4 \/ ssSkP0 a556
% 0.71/0.88  |- ~c3_0 \/ c1_1 $_281 \/ c3_1 a556 \/ c3_2 a556 a562 \/ c4_0 \/
% 0.71/0.88     c4_1 $_281 \/ c5_1 $_281 \/ c5_2 a556 a586 \/ ssSkC1 \/ ssSkC4 \/
% 0.71/0.88     ssSkP2 a556
% 0.71/0.88  |- ~c3_0 \/ c1_1 $_285 \/ c3_1 a556 \/ c3_2 a556 a562 \/ c4_1 $_285 \/
% 0.71/0.88     c5_0 \/ c5_1 $_285 \/ c5_2 a556 a586 \/ ssSkC1 \/ ssSkC4 \/ ssSkP2 a556
% 0.71/0.88  |- ~c1_2 $_287 a579 \/ ~c1_2 a574 $_289 \/ ~c5_1 $_287 \/ ~ndr1_0 \/
% 0.71/0.88     ~ndr1_1 $_287 \/ ~ndr1_1 a574 \/ c2_1 $_287 \/ c2_2 $_287 a579 \/
% 0.71/0.88     c3_2 a574 $_289 \/ c4_2 a574 $_289 \/ c5_0 \/ ssSkP3 $_287
% 0.71/0.88  |- ~c1_2 $_290 a579 \/ ~c5_1 $_290 \/ ~ndr1_0 \/ ~ndr1_1 $_290 \/
% 0.71/0.88     ~ndr1_1 a574 \/ c2_1 $_290 \/ c2_2 $_290 a579 \/ c3_2 a574 a557 \/
% 0.71/0.88     c4_2 a574 a557 \/ c5_0 \/ ssSkP1 a574 \/ ssSkP3 $_290
% 0.71/0.88  |- ~c1_1 $_294 \/ ~c2_2 $_294 $_295 \/ ~c3_2 $_294 $_295 \/ ~ndr1_0 \/
% 0.71/0.88     ~ndr1_1 $_294 \/ ~ndr1_1 a567 \/ ~ssSkC0 \/ ~ssSkP0 a567 \/ c1_0 \/
% 0.71/0.88     c1_2 a567 a576 \/ c1_2 a567 a579 \/ c2_1 $_294 \/ c2_2 a567 a579 \/
% 0.71/0.88     c3_0 \/ c3_1 a567 \/ c4_2 a567 a559 \/ c5_2 a567 a549 \/ ssSkC2 \/
% 0.71/0.88     ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.71/0.88  |- ~c1_1 $_294 \/ ~c2_2 $_294 $_295 \/ ~c3_2 $_294 $_295 \/ ~ndr1_0 \/
% 0.71/0.88     ~ndr1_1 $_294 \/ ~ndr1_1 a567 \/ ~ssSkC0 \/ ~ssSkP0 a567 \/
% 0.71/0.88     c1_2 a567 a576 \/ c1_2 a567 a579 \/ c2_1 $_294 \/ c2_2 a567 a579 \/
% 0.71/0.88     c3_1 a567 \/ c4_2 a567 a559 \/ c5_0 \/ c5_2 a567 a549 \/ ssSkC2 \/
% 0.71/0.88     ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.71/0.88  |- ~c1_1 $_294 \/ ~c2_2 $_294 $_295 \/ ~c3_2 $_294 $_295 \/ ~ndr1_0 \/
% 0.71/0.88     ~ndr1_1 $_294 \/ ~ndr1_1 a567 \/ ~ssSkC0 \/ ~ssSkP0 a567 \/
% 0.71/0.88     c1_2 a567 a576 \/ c1_2 a567 a579 \/ c2_1 $_294 \/ c2_2 a567 a579 \/
% 0.71/0.88     c3_1 a567 \/ c4_0 \/ c4_2 a567 a559 \/ c5_2 a567 a549 \/ ssSkC2 \/
% 0.71/0.88     ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.71/0.88  |- ~c1_1 $_294 \/ ~c2_2 $_294 $_295 \/ ~c3_2 $_294 $_295 \/ ~ndr1_0 \/
% 0.71/0.88     ~ndr1_1 $_294 \/ ~ndr1_1 a567 \/ ~ssSkC0 \/ ~ssSkP0 a567 \/ c1_0 \/
% 0.71/0.88     c1_2 a567 a576 \/ c1_2 a567 a579 \/ c2_1 $_294 \/ c2_2 a567 a579 \/
% 0.71/0.88     c3_0 \/ c3_1 a567 \/ c3_2 a567 a559 \/ c5_2 a567 a549 \/ ssSkC2 \/
% 0.71/0.88     ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.71/0.88  |- ~c1_1 $_294 \/ ~c2_2 $_294 $_295 \/ ~c3_2 $_294 $_295 \/ ~ndr1_0 \/
% 0.71/0.88     ~ndr1_1 $_294 \/ ~ndr1_1 a567 \/ ~ssSkC0 \/ ~ssSkP0 a567 \/
% 0.71/0.88     c1_2 a567 a576 \/ c1_2 a567 a579 \/ c2_1 $_294 \/ c2_2 a567 a579 \/
% 0.71/0.88     c3_1 a567 \/ c3_2 a567 a559 \/ c5_0 \/ c5_2 a567 a549 \/ ssSkC2 \/
% 0.71/0.88     ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.71/0.88  |- ~c1_1 $_294 \/ ~c2_2 $_294 $_295 \/ ~c3_2 $_294 $_295 \/ ~ndr1_0 \/
% 0.71/0.88     ~ndr1_1 $_294 \/ ~ndr1_1 a567 \/ ~ssSkC0 \/ ~ssSkP0 a567 \/
% 0.71/0.88     c1_2 a567 a576 \/ c1_2 a567 a579 \/ c2_1 $_294 \/ c2_2 a567 a579 \/
% 0.71/0.88     c3_1 a567 \/ c3_2 a567 a559 \/ c4_0 \/ c5_2 a567 a549 \/ ssSkC2 \/
% 0.71/0.88     ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.71/0.88  |- ~c1_1 $_294 \/ ~c2_2 $_294 $_295 \/ ~c3_2 $_294 $_295 \/ ~ndr1_0 \/
% 0.71/0.88     ~ndr1_1 $_293 \/ ~ndr1_1 $_294 \/ ~ssSkC0 \/ ~ssSkP0 $_293 \/
% 0.71/0.88     c1_2 $_293 a562 \/ c2_1 $_294 \/ c5_2 $_293 a549 \/ ssSkP2 $_293
% 0.71/0.88  |- ~c1_1 $_298 \/ ~c2_2 $_298 $_299 \/ ~c3_2 $_298 $_299 \/ ~ndr1_0 \/
% 0.71/0.88     ~ndr1_1 $_298 \/ ~ndr1_1 a567 \/ ~ssSkC0 \/ ~ssSkP0 a567 \/ c1_0 \/
% 0.71/0.88     c1_2 a567 a576 \/ c1_2 a567 a579 \/ c2_1 $_298 \/ c2_2 a567 a549 \/
% 0.71/0.88     c2_2 a567 a579 \/ c3_0 \/ c3_1 a567 \/ c4_2 a567 a559 \/ ssSkC2 \/
% 0.71/0.88     ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.71/0.88  |- ~c1_1 $_298 \/ ~c2_2 $_298 $_299 \/ ~c3_2 $_298 $_299 \/ ~ndr1_0 \/
% 0.71/0.88     ~ndr1_1 $_298 \/ ~ndr1_1 a567 \/ ~ssSkC0 \/ ~ssSkP0 a567 \/
% 0.71/0.88     c1_2 a567 a576 \/ c1_2 a567 a579 \/ c2_1 $_298 \/ c2_2 a567 a549 \/
% 0.71/0.88     c2_2 a567 a579 \/ c3_1 a567 \/ c4_2 a567 a559 \/ c5_0 \/ ssSkC2 \/
% 0.71/0.88     ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.71/0.88  |- ~c1_1 $_298 \/ ~c2_2 $_298 $_299 \/ ~c3_2 $_298 $_299 \/ ~ndr1_0 \/
% 0.71/0.88     ~ndr1_1 $_298 \/ ~ndr1_1 a567 \/ ~ssSkC0 \/ ~ssSkP0 a567 \/
% 0.71/0.88     c1_2 a567 a576 \/ c1_2 a567 a579 \/ c2_1 $_298 \/ c2_2 a567 a549 \/
% 0.71/0.88     c2_2 a567 a579 \/ c3_1 a567 \/ c4_0 \/ c4_2 a567 a559 \/ ssSkC2 \/
% 0.71/0.88     ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.71/0.88  |- ~c1_1 $_298 \/ ~c2_2 $_298 $_299 \/ ~c3_2 $_298 $_299 \/ ~ndr1_0 \/
% 0.71/0.88     ~ndr1_1 $_298 \/ ~ndr1_1 a567 \/ ~ssSkC0 \/ ~ssSkP0 a567 \/ c1_0 \/
% 0.71/0.88     c1_2 a567 a576 \/ c1_2 a567 a579 \/ c2_1 $_298 \/ c2_2 a567 a549 \/
% 0.71/0.88     c2_2 a567 a579 \/ c3_0 \/ c3_1 a567 \/ c3_2 a567 a559 \/ ssSkC2 \/
% 0.71/0.88     ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.71/0.88  |- ~c1_1 $_298 \/ ~c2_2 $_298 $_299 \/ ~c3_2 $_298 $_299 \/ ~ndr1_0 \/
% 0.71/0.88     ~ndr1_1 $_298 \/ ~ndr1_1 a567 \/ ~ssSkC0 \/ ~ssSkP0 a567 \/
% 0.71/0.88     c1_2 a567 a576 \/ c1_2 a567 a579 \/ c2_1 $_298 \/ c2_2 a567 a549 \/
% 0.71/0.88     c2_2 a567 a579 \/ c3_1 a567 \/ c3_2 a567 a559 \/ c5_0 \/ ssSkC2 \/
% 0.71/0.88     ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.71/0.88  |- ~c1_1 $_298 \/ ~c2_2 $_298 $_299 \/ ~c3_2 $_298 $_299 \/ ~ndr1_0 \/
% 0.71/0.88     ~ndr1_1 $_298 \/ ~ndr1_1 a567 \/ ~ssSkC0 \/ ~ssSkP0 a567 \/
% 0.71/0.88     c1_2 a567 a576 \/ c1_2 a567 a579 \/ c2_1 $_298 \/ c2_2 a567 a549 \/
% 0.71/0.88     c2_2 a567 a579 \/ c3_1 a567 \/ c3_2 a567 a559 \/ c4_0 \/ ssSkC2 \/
% 0.71/0.88     ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.71/0.88  |- ~c1_1 $_298 \/ ~c2_2 $_298 $_299 \/ ~c3_2 $_298 $_299 \/ ~ndr1_0 \/
% 0.71/0.88     ~ndr1_1 $_297 \/ ~ndr1_1 $_298 \/ ~ssSkC0 \/ ~ssSkP0 $_297 \/
% 0.71/0.88     c1_2 $_297 a562 \/ c2_1 $_298 \/ c2_2 $_297 a549 \/ ssSkP2 $_297
% 0.71/0.88  |- ~c1_1 $_302 \/ ~c2_2 $_302 $_303 \/ ~c3_2 $_302 $_303 \/
% 0.71/0.88     ~c4_2 a567 a549 \/ ~ndr1_0 \/ ~ndr1_1 $_302 \/ ~ndr1_1 a567 \/
% 0.71/0.88     ~ssSkC0 \/ ~ssSkP0 a567 \/ c1_0 \/ c1_2 a567 a576 \/ c1_2 a567 a579 \/
% 0.71/0.88     c2_1 $_302 \/ c2_2 a567 a579 \/ c3_0 \/ c3_1 a567 \/ c4_2 a567 a559 \/
% 0.71/0.88     ssSkC2 \/ ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.71/0.88  |- ~c1_1 $_302 \/ ~c2_2 $_302 $_303 \/ ~c3_2 $_302 $_303 \/
% 0.71/0.88     ~c4_2 a567 a549 \/ ~ndr1_0 \/ ~ndr1_1 $_302 \/ ~ndr1_1 a567 \/
% 0.71/0.88     ~ssSkC0 \/ ~ssSkP0 a567 \/ c1_2 a567 a576 \/ c1_2 a567 a579 \/
% 0.71/0.88     c2_1 $_302 \/ c2_2 a567 a579 \/ c3_1 a567 \/ c4_2 a567 a559 \/ c5_0 \/
% 0.71/0.88     ssSkC2 \/ ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.71/0.88  |- ~c1_1 $_302 \/ ~c2_2 $_302 $_303 \/ ~c3_2 $_302 $_303 \/
% 0.71/0.88     ~c4_2 a567 a549 \/ ~ndr1_0 \/ ~ndr1_1 $_302 \/ ~ndr1_1 a567 \/
% 0.71/0.88     ~ssSkC0 \/ ~ssSkP0 a567 \/ c1_2 a567 a576 \/ c1_2 a567 a579 \/
% 0.71/0.88     c2_1 $_302 \/ c2_2 a567 a579 \/ c3_1 a567 \/ c4_0 \/ c4_2 a567 a559 \/
% 0.71/0.88     ssSkC2 \/ ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.71/0.88  |- ~c1_1 $_302 \/ ~c2_2 $_302 $_303 \/ ~c3_2 $_302 $_303 \/
% 0.71/0.88     ~c4_2 a567 a549 \/ ~ndr1_0 \/ ~ndr1_1 $_302 \/ ~ndr1_1 a567 \/
% 0.71/0.88     ~ssSkC0 \/ ~ssSkP0 a567 \/ c1_0 \/ c1_2 a567 a576 \/ c1_2 a567 a579 \/
% 0.71/0.88     c2_1 $_302 \/ c2_2 a567 a579 \/ c3_0 \/ c3_1 a567 \/ c3_2 a567 a559 \/
% 0.71/0.88     ssSkC2 \/ ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.71/0.88  |- ~c1_1 $_302 \/ ~c2_2 $_302 $_303 \/ ~c3_2 $_302 $_303 \/
% 0.71/0.88     ~c4_2 a567 a549 \/ ~ndr1_0 \/ ~ndr1_1 $_302 \/ ~ndr1_1 a567 \/
% 0.71/0.88     ~ssSkC0 \/ ~ssSkP0 a567 \/ c1_2 a567 a576 \/ c1_2 a567 a579 \/
% 0.71/0.88     c2_1 $_302 \/ c2_2 a567 a579 \/ c3_1 a567 \/ c3_2 a567 a559 \/ c5_0 \/
% 0.71/0.88     ssSkC2 \/ ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.71/0.88  |- ~c1_1 $_302 \/ ~c2_2 $_302 $_303 \/ ~c3_2 $_302 $_303 \/
% 0.71/0.88     ~c4_2 a567 a549 \/ ~ndr1_0 \/ ~ndr1_1 $_302 \/ ~ndr1_1 a567 \/
% 0.71/0.88     ~ssSkC0 \/ ~ssSkP0 a567 \/ c1_2 a567 a576 \/ c1_2 a567 a579 \/
% 0.71/0.88     c2_1 $_302 \/ c2_2 a567 a579 \/ c3_1 a567 \/ c3_2 a567 a559 \/ c4_0 \/
% 0.71/0.88     ssSkC2 \/ ssSkC5 \/ ssSkC6 \/ ssSkP3 a567
% 0.71/0.88  |- ~c1_1 $_302 \/ ~c2_2 $_302 $_303 \/ ~c3_2 $_302 $_303 \/
% 0.71/0.88     ~c4_2 $_301 a549 \/ ~ndr1_0 \/ ~ndr1_1 $_301 \/ ~ndr1_1 $_302 \/
% 0.71/0.88     ~ssSkC0 \/ ~ssSkP0 $_301 \/ c1_2 $_301 a562 \/ c2_1 $_302 \/
% 0.71/0.88     ssSkP2 $_301
% 0.71/0.88  |- ~c1_1 a569 \/ ~ndr1_0 \/ ~ndr1_1 $_320 \/ ~ndr1_1 a569 \/ ~ssSkC0 \/
% 0.71/0.88     ~ssSkP0 $_320 \/ c1_2 $_320 a562 \/ c2_0 \/ c2_1 a569 \/ c3_1 a569 \/
% 0.71/0.88     c5_0 \/ c5_2 $_320 a549 \/ ssSkC4 \/ ssSkP0 a569 \/ ssSkP2 $_320
% 0.71/0.88  |- ~c1_1 a569 \/ ~ndr1_0 \/ ~ndr1_1 $_322 \/ ~ndr1_1 a569 \/ ~ssSkC0 \/
% 0.71/0.88     ~ssSkP0 $_322 \/ c1_2 $_322 a562 \/ c2_0 \/ c2_1 a569 \/ c3_1 a569 \/
% 0.71/0.88     c5_0 \/ c5_2 $_322 a549 \/ ssSkC4 \/ ssSkP2 $_322 \/ ssSkP2 a569
% 0.71/0.88  |- ~c1_1 a569 \/ ~ndr1_0 \/ ~ndr1_1 $_327 \/ ~ndr1_1 a569 \/ ~ssSkC0 \/
% 0.71/0.88     ~ssSkP0 $_327 \/ c1_2 $_327 a562 \/ c2_0 \/ c2_1 a569 \/
% 0.71/0.88     c2_2 $_327 a549 \/ c3_1 a569 \/ c5_0 \/ ssSkC4 \/ ssSkP2 $_327 \/
% 0.71/0.88     ssSkP2 a569
% 0.71/0.88  |- ~c1_1 a569 \/ ~ndr1_0 \/ ~ndr1_1 $_329 \/ ~ndr1_1 a569 \/ ~ssSkC0 \/
% 0.71/0.88     ~ssSkP0 $_329 \/ c1_2 $_329 a562 \/ c2_0 \/ c2_1 a569 \/
% 0.71/0.88     c2_2 $_329 a549 \/ c3_1 a569 \/ c5_0 \/ ssSkC4 \/ ssSkP0 a569 \/
% 0.71/0.88     ssSkP2 $_329
% 0.71/0.88  SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.71/0.88  
%------------------------------------------------------------------------------