↑ Up

Metis---2.4.SAT-Sat.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : Metis---2.4
% Problem  : SYN541-1 : TPTP v8.1.0. Released v2.1.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : metis --show proof --show saturation %s

% Computer : n026.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:51 EDT 2022

% Result   : Satisfiable 0.21s 0.48s
% Output   : Saturation 0.21s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13  % Problem  : SYN541-1 : TPTP v8.1.0. Released v2.1.0.
% 0.08/0.14  % Command  : metis --show proof --show saturation %s
% 0.13/0.36  % Computer : n026.cluster.edu
% 0.13/0.36  % Model    : x86_64 x86_64
% 0.13/0.36  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.36  % Memory   : 8042.1875MB
% 0.13/0.36  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.36  % CPULimit : 300
% 0.13/0.36  % WCLimit  : 600
% 0.13/0.36  % DateTime : Mon Jul 11 16:56:12 EDT 2022
% 0.13/0.36  % CPUTime  : 
% 0.13/0.36  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.21/0.48  % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.21/0.48  
% 0.21/0.48  SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.21/0.48  |- ndr1_0
% 0.21/0.48  |- c2_1 a731
% 0.21/0.48  |- c4_1 a731
% 0.21/0.48  |- ~ssSkC5 \/ ndr1_1 a759
% 0.21/0.48  |- ~ssSkC5 \/ c3_1 a759
% 0.21/0.48  |- ~c4_0 \/ c1_0
% 0.21/0.48  |- ~c2_0 \/ c3_0
% 0.21/0.48  |- ~c5_0 \/ c4_0
% 0.21/0.48  |- ndr1_1 a772 \/ ssSkC7
% 0.21/0.48  |- c2_1 a772 \/ ssSkC7
% 0.21/0.48  |- c5_1 a772 \/ ssSkC7
% 0.21/0.48  |- ndr1_1 $U \/ ssSkP0 $U
% 0.21/0.48  |- ndr1_1 a750 \/ ssSkC4
% 0.21/0.48  |- ndr1_1 a744 \/ ssSkC3
% 0.21/0.48  |- c3_1 a744 \/ ssSkC3
% 0.21/0.48  |- ndr1_1 a742 \/ ssSkC2
% 0.21/0.48  |- c3_1 a742 \/ ssSkC2
% 0.21/0.48  |- c4_1 a734 \/ ssSkC1
% 0.21/0.48  |- ndr1_1 a726 \/ ssSkC0
% 0.21/0.48  |- ~ssSkC7 \/ c1_0 \/ c3_1 a774
% 0.21/0.48  |- c1_0 \/ c4_0 \/ c4_1 a771
% 0.21/0.48  |- ~ssSkC6 \/ c1_0 \/ ndr1_1 a767
% 0.21/0.48  |- ~ssSkC6 \/ c1_0 \/ c5_1 a767
% 0.21/0.48  |- ~ssSkC5 \/ c4_2 a759 a760
% 0.21/0.48  |- ~c2_0 \/ c4_1 a757
% 0.21/0.48  |- ~c4_0 \/ c2_1 a741
% 0.21/0.48  |- ~c4_0 \/ c3_1 a741
% 0.21/0.48  |- c5_2 a772 a773 \/ ssSkC7
% 0.21/0.48  |- c3_2 $U a755 \/ ssSkP0 $U
% 0.21/0.48  |- c4_2 a750 a751 \/ ssSkC4
% 0.21/0.48  |- c2_2 a750 a751 \/ ssSkC4
% 0.21/0.48  |- ~c2_1 a750 \/ ssSkC4
% 0.21/0.48  |- c3_2 a744 a745 \/ ssSkC3
% 0.21/0.48  |- c1_2 a744 a745 \/ ssSkC3
% 0.21/0.48  |- ~c5_1 a744 \/ ssSkC3
% 0.21/0.48  |- c2_2 a742 a743 \/ ssSkC2
% 0.21/0.48  |- ~c5_1 a734 \/ ssSkC1
% 0.21/0.48  |- c2_2 a726 a728 \/ ssSkC0
% 0.21/0.48  |- c2_2 a726 a727 \/ ssSkC0
% 0.21/0.48  |- c4_2 a726 a727 \/ ssSkC0
% 0.21/0.48  |- ~ssSkC6 \/ c1_0 \/ c4_2 a767 a768
% 0.21/0.48  |- ~ssSkC6 \/ c1_0 \/ c3_2 a767 a768
% 0.21/0.48  |- ~c4_1 a767 \/ ~ssSkC6 \/ c1_0
% 0.21/0.48  |- ~c1_2 a759 a760 \/ ~ssSkC5
% 0.21/0.48  |- ~c3_2 a759 a760 \/ ~ssSkC5
% 0.21/0.48  |- ~c1_1 a757 \/ ~c2_0
% 0.21/0.48  |- ~c4_0 \/ c5_0 \/ ndr1_1 a747
% 0.21/0.48  |- ~c4_0 \/ ~c4_1 a741
% 0.21/0.48  |- ~c1_0 \/ c2_0 \/ ndr1_1 a736
% 0.21/0.48  |- ~c1_0 \/ c2_0 \/ c4_1 a736
% 0.21/0.48  |- ~c3_0 \/ ~ssSkC0 \/ c4_1 a729
% 0.21/0.48  |- ~c1_2 a772 a773 \/ ssSkC7
% 0.21/0.48  |- ~c4_2 a772 a773 \/ ssSkC7
% 0.21/0.48  |- ~c4_2 $U a755 \/ ssSkP0 $U
% 0.21/0.48  |- ~c1_2 a750 a751 \/ ssSkC4
% 0.21/0.48  |- ~c4_2 a744 a745 \/ ssSkC3
% 0.21/0.48  |- ~c4_2 a742 a743 \/ ssSkC2
% 0.21/0.48  |- ~c1_2 a742 a743 \/ ssSkC2
% 0.21/0.48  |- ~c4_2 a726 a728 \/ ssSkC0
% 0.21/0.48  |- ~c5_2 a726 a727 \/ ssSkC0
% 0.21/0.48  |- ~c1_0 \/ ~c3_0 \/ ndr1_1 a769
% 0.21/0.48  |- ~c5_2 a767 a768 \/ ~ssSkC6 \/ c1_0
% 0.21/0.48  |- ~c3_0 \/ ~c4_0 \/ c5_1 a765
% 0.21/0.48  |- ~c4_0 \/ c3_2 a747 a749 \/ c5_0
% 0.21/0.48  |- ~c1_0 \/ c2_0 \/ c5_2 a736 a737
% 0.21/0.48  |- ~c1_0 \/ ~c3_1 a736 \/ c2_0
% 0.21/0.48  |- ~c1_0 \/ ~c3_0 \/ c4_2 a769 a770
% 0.21/0.48  |- ~c1_0 \/ ~c3_0 \/ c3_2 a769 a770
% 0.21/0.48  |- ~c1_0 \/ ~c3_0 \/ ~c3_1 a769
% 0.21/0.48  |- ~c3_0 \/ ~c4_0 \/ ~c4_1 a765
% 0.21/0.48  |- ~c2_2 a747 a749 \/ ~c4_0 \/ c5_0
% 0.21/0.48  |- ~c4_0 \/ ~c4_2 a747 a749 \/ c5_0
% 0.21/0.48  |- ~c4_0 \/ ~c4_2 a747 a748 \/ c5_0
% 0.21/0.48  |- ~c2_2 a747 a748 \/ ~c4_0 \/ c5_0
% 0.21/0.48  |- ~c3_2 a747 a748 \/ ~c4_0 \/ c5_0
% 0.21/0.48  |- ~c1_0 \/ ~c4_2 a736 a737 \/ c2_0
% 0.21/0.48  |- ~c1_0 \/ ~c3_2 a736 a737 \/ c2_0
% 0.21/0.48  |- ~c1_0 \/ ~c2_2 a769 a770 \/ ~c3_0
% 0.21/0.48  |- ~c4_1 $U \/ ~ssSkC1 \/ c5_1 $U \/ ndr1_1 $U
% 0.21/0.48  |- ~c5_1 $U \/ c2_1 $U \/ c3_0 \/ ndr1_1 a732
% 0.21/0.48  |- ~c4_1 $U \/ ~ssSkC1 \/ c1_2 $U a735 \/ c5_1 $U
% 0.21/0.48  |- ~c4_1 $U \/ ~ssSkC1 \/ c4_2 $U a735 \/ c5_1 $U
% 0.21/0.49  |- ~c5_1 $U \/ c2_1 $U \/ c3_0 \/ c4_2 a732 a733
% 0.21/0.49  |- ~c2_1 a732 \/ ~c5_1 $U \/ c2_1 $U \/ c3_0
% 0.21/0.49  |- ~c2_0 \/ ~ssSkP0 $U \/ c1_0 \/ c1_2 $U a756 \/ c4_1 $U
% 0.21/0.49  |- ~c2_0 \/ ~ssSkP0 $U \/ c1_0 \/ c4_1 $U \/ c5_2 $U a756
% 0.21/0.49  |- ~c1_1 $U \/ c3_1 $U \/ c4_0 \/ c4_1 $U \/ ndr1_1 a738
% 0.21/0.49  |- ~c4_1 $U \/ ~c5_2 $U a735 \/ ~ssSkC1 \/ c5_1 $U
% 0.21/0.49  |- ~c5_2 a726 $U \/ ~ndr1_1 a726 \/ c3_2 a726 $U \/ ssSkC0
% 0.21/0.49  |- ~c4_2 a774 $U \/ ~ndr1_1 a774 \/ ~ssSkC7 \/ c1_0 \/ c1_2 a774 $U
% 0.21/0.49  |- ~c1_2 a774 $U \/ ~ndr1_1 a774 \/ ~ssSkC7 \/ c1_0 \/ c2_2 a774 $U
% 0.21/0.49  |- ~c3_2 a732 a733 \/ ~c5_1 $U \/ c2_1 $U \/ c3_0
% 0.21/0.49  |- ~c2_0 \/ ~c4_2 $U a756 \/ ~ssSkP0 $U \/ c1_0 \/ c4_1 $U
% 0.21/0.49  |- ~c1_1 $U \/ c1_2 a738 a740 \/ c3_1 $U \/ c4_0 \/ c4_1 $U
% 0.21/0.49  |- ~c1_2 a750 $U \/ ~c2_2 a750 $U \/ ~ndr1_1 a750 \/ ssSkC4
% 0.21/0.49  |- ~c3_2 a747 $U \/ ~c4_0 \/ ~ndr1_1 a747 \/ c1_2 a747 $U \/ c5_0
% 0.21/0.49  |- ~c1_1 $U \/ ~c5_2 a738 a740 \/ c3_1 $U \/ c4_0 \/ c4_1 $U
% 0.21/0.49  |- ~c1_1 $U \/ ~c4_2 a738 a739 \/ c3_1 $U \/ c4_0 \/ c4_1 $U
% 0.21/0.49  |- ~c1_1 $U \/ ~c1_2 a738 a739 \/ c3_1 $U \/ c4_0 \/ c4_1 $U
% 0.21/0.49  |- ~c1_1 $U \/ ~c5_2 a738 a739 \/ c3_1 $U \/ c4_0 \/ c4_1 $U
% 0.21/0.49  |- ~c3_0 \/ ~c3_1 $U \/ ~c4_1 $U \/ ~c5_0 \/ ndr1_1 $U
% 0.21/0.49  |- ~c1_2 a729 $U \/ ~c3_0 \/ ~c4_2 a729 $U \/ ~ndr1_1 a729 \/ ~ssSkC0
% 0.21/0.49  |- ~c2_2 a759 $U \/ ~c5_2 a759 $U \/ ~ndr1_1 a759 \/ ~ssSkC5 \/
% 0.21/0.49     c1_2 a759 $U
% 0.21/0.49  |- ~c2_2 a771 $U \/ ~c5_2 a771 $U \/ ~ndr1_1 a771 \/ c1_0 \/
% 0.21/0.49     c3_2 a771 $U \/ c4_0
% 0.21/0.49  |- ~c1_0 \/ ~c3_0 \/ ~ndr1_1 a769 \/ c1_2 a769 $U \/ c3_2 a769 $U \/
% 0.21/0.49     c4_2 a769 $U
% 0.21/0.49  |- ~c2_2 $U a730 \/ ~c3_0 \/ ~c3_1 $U \/ ~c4_1 $U \/ ~c5_0
% 0.21/0.49  |- ~c3_0 \/ ~c3_1 $U \/ ~c3_2 $U a730 \/ ~c4_1 $U \/ ~c5_0
% 0.21/0.49  |- ~c5_2 $U $V \/ ~ndr1_1 $U \/ c3_2 $U $V \/ c3_2 $U a766 \/ c5_1 $U \/
% 0.21/0.49     ssSkC6
% 0.21/0.49  |- ~c4_2 $U $V \/ ~ndr1_1 $U \/ c1_1 $U \/ c1_2 $U $V \/ c5_2 $U a758 \/
% 0.21/0.49     ssSkC5
% 0.21/0.49  |- ~c3_0 \/ ~c3_2 a765 $U \/ ~c4_0 \/ ~ndr1_1 a765 \/ c1_2 a765 $U \/
% 0.21/0.49     c2_2 a765 $U
% 0.21/0.49  |- ~c1_2 a729 $U \/ ~c3_0 \/ ~c5_2 a729 $U \/ ~ndr1_1 a729 \/ ~ssSkC0 \/
% 0.21/0.49     c4_2 a729 $U
% 0.21/0.49  |- ~c1_2 $U $V \/ ~c2_2 $U $V \/ ~c5_2 $U $V \/ ~ndr1_1 $U \/ c1_0 \/ c5_0
% 0.21/0.49  |- ~c2_2 $U $V \/ ~c4_0 \/ ~ndr1_1 $U \/ c1_2 $U $V \/ c2_1 $U \/
% 0.21/0.49     c4_2 $U $V \/ c5_0
% 0.21/0.49  |- ~c2_2 $U a766 \/ ~c5_2 $U $V \/ ~ndr1_1 $U \/ c3_2 $U $V \/ c5_1 $U \/
% 0.21/0.49     ssSkC6
% 0.21/0.49  |- ~c1_2 $U a766 \/ ~c5_2 $U $V \/ ~ndr1_1 $U \/ c3_2 $U $V \/ c5_1 $U \/
% 0.21/0.49     ssSkC6
% 0.21/0.49  |- ~c2_2 $U a758 \/ ~c4_2 $U $V \/ ~ndr1_1 $U \/ c1_1 $U \/ c1_2 $U $V \/
% 0.21/0.49     ssSkC5
% 0.21/0.49  |- ~c2_2 $U $V \/ ~c3_2 $U $V \/ ~c4_0 \/ ~ndr1_1 $U \/ c3_0 \/ c4_1 $U \/
% 0.21/0.49     c5_1 $U
% 0.21/0.49  |- ~c1_2 $U $V \/ ~c2_1 $W \/ ~ndr1_1 $U \/ c2_2 $U $V \/ c5_1 $U \/
% 0.21/0.49     c5_2 $U $V \/ ndr1_1 $W
% 0.21/0.49  |- ~c4_2 $U $V \/ ~ndr1_1 $U \/ c1_1 $U \/ c2_0 \/ c3_2 $U $V \/
% 0.21/0.49     c3_2 $U a754 \/ c4_0 \/ c5_2 $U $V
% 0.21/0.49  |- ~c1_0 \/ ~c3_2 $U $V \/ ~ndr1_1 $U \/ c1_2 $U $V \/ c2_2 $U $V \/
% 0.21/0.49     c3_1 $U \/ c4_0 \/ c4_1 $U
% 0.21/0.49  |- ~c1_2 $U $V \/ ~c2_1 $W \/ ~ndr1_1 $U \/ c2_2 $U $V \/ c3_2 $W a762 \/
% 0.21/0.49     c5_1 $U \/ c5_2 $U $V
% 0.21/0.49  |- ~c1_2 $U $V \/ ~c2_1 $W \/ ~ndr1_1 $U \/ c2_2 $U $V \/ c2_2 $W a762 \/
% 0.21/0.49     c5_1 $U \/ c5_2 $U $V
% 0.21/0.49  |- ~c4_2 $U $V \/ ~c5_2 $U a754 \/ ~ndr1_1 $U \/ c1_1 $U \/ c2_0 \/
% 0.21/0.49     c3_2 $U $V \/ c4_0 \/ c5_2 $U $V
% 0.21/0.49  |- ~c1_1 $U \/ ~c1_2 $U $V \/ ~c2_2 $U $V \/ ~c4_0 \/ ~ndr1_1 $U \/
% 0.21/0.49     c2_1 $U \/ c3_2 $U $V
% 0.21/0.49  |- ~c2_1 $U \/ ~c2_2 $U $V \/ ~c5_2 $U $V \/ ~ndr1_1 $U \/ c2_0 \/
% 0.21/0.49     c3_1 $U \/ c4_2 $U $V \/ ndr1_1 a763
% 0.21/0.49  |- ~c2_1 $U \/ ~c2_2 $U $V \/ ~c4_2 $U $W \/ ~ndr1_1 $U \/ c1_0 \/
% 0.21/0.49     c1_2 $U $W \/ c4_2 $U $V \/ c5_2 $U $V
% 0.21/0.49  |- ~c2_1 $U \/ ~c2_2 $U $V \/ ~c5_2 $U $V \/ ~ndr1_1 $U \/
% 0.21/0.49     c1_2 a763 a764 \/ c2_0 \/ c3_1 $U \/ c4_2 $U $V
% 0.21/0.49  |- ~c2_1 $U \/ ~c2_2 $U $V \/ ~c5_2 $U $V \/ ~ndr1_1 $U \/ c2_0 \/
% 0.21/0.49     c2_2 a763 a764 \/ c3_1 $U \/ c4_2 $U $V
% 0.21/0.49  |- ~c2_1 $U \/ ~c2_2 $U $V \/ ~c5_2 $U $V \/ ~ndr1_1 $U \/ c2_0 \/
% 0.21/0.49     c3_1 $U \/ c4_2 $U $V \/ c5_2 a763 a764
% 0.21/0.49  |- ~c2_1 $U \/ ~c2_1 a763 \/ ~c2_2 $U $V \/ ~c5_2 $U $V \/ ~ndr1_1 $U \/
% 0.21/0.49     c2_0 \/ c3_1 $U \/ c4_2 $U $V
% 0.21/0.49  |- ~c1_2 $U $V \/ ~c3_2 $U $V \/ ~c5_1 $U \/ ~c5_2 $U $V \/ ~ndr1_1 $U \/
% 0.21/0.49     ~ssSkC2 \/ ~ssSkC3 \/ c5_2 $U a746
% 0.21/0.49  |- ~c1_2 $U $V \/ ~c3_2 $U $V \/ ~c5_1 $U \/ ~c5_2 $U $V \/ ~ndr1_1 $U \/
% 0.21/0.49     ~ssSkC2 \/ ~ssSkC3 \/ c1_2 $U a746
% 0.21/0.49  |- ~c1_2 $U $V \/ ~c2_1 $U \/ ~c2_2 $U $V \/ ~c3_0 \/ ~c3_1 $W \/
% 0.21/0.49     ~c5_1 $U \/ ~ndr1_1 $U \/ ndr1_1 $W
% 0.21/0.49  |- ~c1_2 $U $V \/ ~c2_1 $U \/ ~c2_2 $U $V \/ ~c3_0 \/ ~c3_1 $W \/
% 0.21/0.49     ~c5_1 $U \/ ~ndr1_1 $U \/ c3_2 $W a761
% 0.21/0.49  |- ~c1_2 $U $V \/ ~c2_1 $U \/ ~c2_2 $U $V \/ ~c3_0 \/ ~c3_1 $W \/
% 0.21/0.49     ~c5_1 $U \/ ~ndr1_1 $U \/ c5_2 $W a761
% 0.21/0.49  |- ~c1_2 $U $V \/ ~c1_2 $W a761 \/ ~c2_1 $U \/ ~c2_2 $U $V \/ ~c3_0 \/
% 0.21/0.49     ~c3_1 $W \/ ~c5_1 $U \/ ~ndr1_1 $U
% 0.21/0.49  |- ~c1_1 $W \/ ~c1_2 $U $V \/ ~c2_1 $W \/ ~c3_2 $U $V \/ ~c4_0 \/
% 0.21/0.49     ~c5_1 $U \/ ~ndr1_1 $U \/ c2_2 $U $V \/ c3_1 $U \/ ndr1_1 $W
% 0.21/0.49  |- ~c1_1 $W \/ ~c1_2 $U $V \/ ~c2_1 $W \/ ~c3_2 $U $V \/ ~c4_0 \/
% 0.21/0.49     ~c5_1 $U \/ ~ndr1_1 $U \/ c2_2 $U $V \/ c2_2 $W a753 \/ c3_1 $U
% 0.21/0.49  |- ~c1_2 $U $V \/ ~c3_2 $U $V \/ ~c4_2 $U $V \/ ~c4_2 $U $W \/
% 0.21/0.49     ~c5_2 $U $W \/ ~ndr1_1 $U \/ ~ssSkC4 \/ c2_0 \/ c3_2 $U $W \/
% 0.21/0.49     c3_2 $U a752
% 0.21/0.49  |- ~c1_2 $U $V \/ ~c3_2 $U $V \/ ~c4_2 $U $V \/ ~c4_2 $U $W \/
% 0.21/0.49     ~c5_2 $U $W \/ ~ndr1_1 $U \/ ~ssSkC4 \/ c2_0 \/ c3_2 $U $W \/
% 0.21/0.49     c5_2 $U a752
% 0.21/0.49  |- ~c1_1 $W \/ ~c1_2 $U $V \/ ~c2_1 $W \/ ~c3_2 $U $V \/ ~c4_0 \/
% 0.21/0.49     ~c5_1 $U \/ ~c5_2 $W a753 \/ ~ndr1_1 $U \/ c2_2 $U $V \/ c3_1 $U
% 0.21/0.49  |- ~c1_1 $W \/ ~c1_2 $U $V \/ ~c1_2 $W a753 \/ ~c2_1 $W \/ ~c3_2 $U $V \/
% 0.21/0.49     ~c4_0 \/ ~c5_1 $U \/ ~ndr1_1 $U \/ c2_2 $U $V \/ c3_1 $U
% 0.21/0.49  |- ~c2_1 $U \/ ~c2_2 $U $V \/ ~c5_2 $U $V \/ ~ndr1_1 $U \/ ~ndr1_1 a763 \/
% 0.21/0.49     c2_0 \/ c2_2 a763 $W \/ c3_1 $U \/ c4_2 $U $V \/ c4_2 a763 $W \/
% 0.21/0.49     c5_2 a763 $W
% 0.21/0.49  |- ~ssSkC1 \/ c5_1 a731 \/ ndr1_1 a731
% 0.21/0.49  |- ~ssSkC1 \/ c1_0 \/ c4_0 \/ c5_1 a771 \/ ndr1_1 a771
% 0.21/0.49  |- ~ssSkC1 \/ c4_2 a731 a735 \/ c5_1 a731
% 0.21/0.49  |- ~ssSkC1 \/ c1_0 \/ c4_0 \/ c4_2 a771 a735 \/ c5_1 a771
% 0.21/0.49  |- ~ssSkC1 \/ c1_2 a731 a735 \/ c5_1 a731
% 0.21/0.49  |- ~ssSkC1 \/ c1_0 \/ c1_2 a771 a735 \/ c4_0 \/ c5_1 a771
% 0.21/0.49  |- ~c2_0 \/ c1_0 \/ c4_1 $_13 \/ ndr1_1 $_13
% 0.21/0.49  |- ~c3_0 \/ ~c3_1 a731 \/ ~c5_0 \/ ndr1_1 a731
% 0.21/0.49  |- ~c3_0 \/ ~c3_1 a734 \/ ~c5_0 \/ ndr1_1 a734 \/ ssSkC1
% 0.21/0.49  |- ~c4_0 \/ ~ndr1_1 a747 \/ c1_2 a747 a755 \/ c5_0 \/ ssSkP0 a747
% 0.21/0.49  |- c1_2 a742 $_31 \/ c3_2 a742 $_31 \/ c4_2 a742 $_31 \/ ssSkC2
% 0.21/0.49  |- c1_2 a742 a743 \/ c3_2 a742 a743 \/ ssSkC2
% 0.21/0.49  |- ~c3_0 \/ ~c4_0 \/ ~ndr1_1 a765 \/ c1_2 a765 a755 \/ c2_2 a765 a755 \/
% 0.21/0.49     ssSkP0 a765
% 0.21/0.49  |- c1_1 a726 \/ c1_2 a726 a727 \/ c5_2 a726 a758 \/ ssSkC0 \/ ssSkC5
% 0.21/0.49  |- c1_1 a750 \/ c1_2 a750 a751 \/ c5_2 a750 a758 \/ ssSkC4 \/ ssSkC5
% 0.21/0.49  |- c1_1 a726 \/ c1_2 a726 a727 \/ c3_2 a726 a758 \/ ssSkC0 \/ ssSkC5
% 0.21/0.49  |- c1_1 a750 \/ c1_2 a750 a751 \/ c3_2 a750 a758 \/ c3_2 a750 a766 \/
% 0.21/0.49     c5_1 a750 \/ ssSkC4 \/ ssSkC5 \/ ssSkC6
% 0.21/0.49  |- ~c2_2 a750 a766 \/ ~ndr1_1 a750 \/ c1_1 a750 \/ c1_2 a750 a751 \/
% 0.21/0.49     c3_2 a750 a758 \/ c5_1 a750 \/ ssSkC4 \/ ssSkC5 \/ ssSkC6
% 0.21/0.49  |- ~c1_2 a750 a766 \/ ~ndr1_1 a750 \/ c1_1 a750 \/ c1_2 a750 a751 \/
% 0.21/0.49     c3_2 a750 a758 \/ c5_1 a750 \/ ssSkC4 \/ ssSkC5 \/ ssSkC6
% 0.21/0.49  |- ~c2_2 a726 a758 \/ ~ndr1_1 a726 \/ c1_1 a726 \/ c1_2 a726 a727 \/
% 0.21/0.49     ssSkC0 \/ ssSkC5
% 0.21/0.49  |- ~c2_2 a742 a758 \/ ~ndr1_1 a742 \/ c1_1 a742 \/ c1_2 a742 $_49 \/
% 0.21/0.49     c3_2 a742 $_49 \/ ssSkC2 \/ ssSkC5
% 0.21/0.49  |- ~c2_2 a750 a758 \/ ~ndr1_1 a750 \/ c1_1 a750 \/ c1_2 a750 a751 \/
% 0.21/0.49     ssSkC4 \/ ssSkC5
% 0.21/0.49  |- c1_1 a742 \/ c1_2 a742 $_50 \/ c3_2 a742 $_50 \/ c5_2 a742 a758 \/
% 0.21/0.49     ssSkC2 \/ ssSkC5
% 0.21/0.49  |- ~c1_2 a742 a766 \/ ~ndr1_1 a742 \/ c1_1 a742 \/ c1_2 a742 $_51 \/
% 0.21/0.49     c3_2 a742 $_51 \/ c3_2 a742 a758 \/ c5_1 a742 \/ ssSkC2 \/ ssSkC5 \/
% 0.21/0.49     ssSkC6
% 0.21/0.49  |- ~c2_2 a742 a766 \/ ~ndr1_1 a742 \/ c1_1 a742 \/ c1_2 a742 $_51 \/
% 0.21/0.49     c3_2 a742 $_51 \/ c3_2 a742 a758 \/ c5_1 a742 \/ ssSkC2 \/ ssSkC5 \/
% 0.21/0.49     ssSkC6
% 0.21/0.49  |- ~c2_2 a742 $_54 \/ ~c4_0 \/ ~ndr1_1 a742 \/ c1_1 a742 \/
% 0.21/0.49     c1_2 a742 $_54 \/ c3_0 \/ c4_1 a742 \/ c5_1 a742 \/ c5_2 a742 a758 \/
% 0.21/0.49     ssSkC2 \/ ssSkC5
% 0.21/0.49  |- ~c2_2 a744 a745 \/ ~c4_0 \/ ~ndr1_1 a744 \/ c3_0 \/ c4_1 a744 \/
% 0.21/0.49     c5_1 a744 \/ ssSkC3
% 0.21/0.49  |- ~c2_2 $_53 a755 \/ ~c4_0 \/ ~ndr1_1 $_53 \/ c3_0 \/ c4_1 $_53 \/
% 0.21/0.49     c5_1 $_53 \/ ssSkP0 $_53
% 0.21/0.49  |- ~c4_0 \/ c1_2 a742 a743 \/ c3_0 \/ c4_1 a742 \/ c5_1 a742 \/ ssSkC2
% 0.21/0.49  |- ~c4_0 \/ c1_2 a726 a728 \/ c2_1 a726 \/ c4_2 a726 a728 \/ c5_0 \/ ssSkC0
% 0.21/0.49  |- ~c4_0 \/ c1_2 a742 a743 \/ c2_1 a742 \/ c4_2 a742 a743 \/ c5_0 \/ ssSkC2
% 0.21/0.49  |- ~c1_1 a726 \/ ~c1_2 a726 a727 \/ ~c4_0 \/ ~ndr1_1 a726 \/ c2_1 a726 \/
% 0.21/0.49     c3_2 a726 a727 \/ ssSkC0
% 0.21/0.49  |- ~c1_1 a726 \/ ~c1_2 a726 a728 \/ ~c4_0 \/ ~ndr1_1 a726 \/ c2_1 a726 \/
% 0.21/0.49     c3_2 a726 a728 \/ ssSkC0
% 0.21/0.49  |- ~c1_0 \/ ~ndr1_1 $_60 \/ c1_2 $_60 a755 \/ c2_2 $_60 a755 \/
% 0.21/0.49     c3_1 $_60 \/ c4_0 \/ c4_1 $_60 \/ ssSkP0 $_60
% 0.21/0.49  |- ~c1_0 \/ c1_1 a726 \/ c1_2 a726 a727 \/ c1_2 a726 a758 \/
% 0.21/0.49     c2_2 a726 a758 \/ c3_1 a726 \/ c4_0 \/ c4_1 a726 \/ ssSkC0 \/ ssSkC5
% 0.21/0.49  |- ~c1_0 \/ c1_2 a726 a755 \/ c2_2 a726 a755 \/ c3_1 a726 \/ c4_0 \/
% 0.21/0.49     c4_1 a726 \/ ssSkC0 \/ ssSkP0 a726
% 0.21/0.49  |- ~c1_0 \/ c1_2 a750 a755 \/ c2_2 a750 a755 \/ c3_1 a750 \/ c4_0 \/
% 0.21/0.49     c4_1 a750 \/ ssSkC4 \/ ssSkP0 a750
% 0.21/0.49  |- ~c1_0 \/ c1_2 a772 a755 \/ c2_2 a772 a755 \/ c3_1 a772 \/ c4_0 \/
% 0.21/0.49     c4_1 a772 \/ ssSkC7 \/ ssSkP0 a772
% 0.21/0.49  |- c1_1 a726 \/ c2_0 \/ c3_2 a726 a727 \/ c3_2 a726 a754 \/ c4_0 \/ ssSkC0
% 0.21/0.49  |- c1_1 a750 \/ c2_0 \/ c3_2 a750 a751 \/ c3_2 a750 a754 \/ c4_0 \/
% 0.21/0.49     c5_2 a750 a751 \/ ssSkC4
% 0.21/0.49  |- ~c1_2 a750 a766 \/ ~ndr1_1 a750 \/ c1_1 a750 \/ c2_0 \/
% 0.21/0.49     c3_2 a750 a751 \/ c3_2 a750 a754 \/ c4_0 \/ c5_1 a750 \/ ssSkC4 \/
% 0.21/0.49     ssSkC6
% 0.21/0.49  |- ~c2_2 a750 a766 \/ ~ndr1_1 a750 \/ c1_1 a750 \/ c2_0 \/
% 0.21/0.49     c3_2 a750 a751 \/ c3_2 a750 a754 \/ c4_0 \/ c5_1 a750 \/ ssSkC4 \/
% 0.21/0.49     ssSkC6
% 0.21/0.49  |- c1_1 a750 \/ c2_0 \/ c3_2 a750 a751 \/ c3_2 a750 a754 \/
% 0.21/0.49     c3_2 a750 a766 \/ c4_0 \/ c5_1 a750 \/ ssSkC4 \/ ssSkC6
% 0.21/0.49  |- ~c1_0 \/ c1_1 a726 \/ c1_2 a726 a754 \/ c2_0 \/ c2_2 a726 a754 \/
% 0.21/0.49     c3_1 a726 \/ c3_2 a726 a727 \/ c4_0 \/ c4_1 a726 \/ ssSkC0
% 0.21/0.49  |- c1_1 a742 \/ c1_2 a742 $_65 \/ c2_0 \/ c3_2 a742 $_65 \/
% 0.21/0.49     c3_2 a742 a754 \/ c4_0 \/ c5_2 a742 $_65 \/ ssSkC2
% 0.21/0.49  |- ~c1_2 a742 a766 \/ ~ndr1_1 a742 \/ c1_1 a742 \/ c1_2 a742 $_66 \/
% 0.21/0.49     c2_0 \/ c3_2 a742 $_66 \/ c3_2 a742 a754 \/ c4_0 \/ c5_1 a742 \/
% 0.21/0.49     ssSkC2 \/ ssSkC6
% 0.21/0.49  |- ~c2_2 a742 a766 \/ ~ndr1_1 a742 \/ c1_1 a742 \/ c1_2 a742 $_66 \/
% 0.21/0.49     c2_0 \/ c3_2 a742 $_66 \/ c3_2 a742 a754 \/ c4_0 \/ c5_1 a742 \/
% 0.21/0.49     ssSkC2 \/ ssSkC6
% 0.21/0.49  |- ~c5_2 a742 a754 \/ ~ndr1_1 a742 \/ c1_1 a742 \/ c1_2 a742 $_68 \/
% 0.21/0.49     c2_0 \/ c3_2 a742 $_68 \/ c4_0 \/ c5_2 a742 $_68 \/ ssSkC2
% 0.21/0.49  |- ~c2_1 a772 \/ ~c2_2 a772 a773 \/ ~ndr1_1 a772 \/ c2_0 \/ c3_1 a772 \/
% 0.21/0.49     c4_2 a772 a773 \/ ndr1_1 a763 \/ ssSkC7
% 0.21/0.49  |- ~c2_1 a763 \/ ~c2_1 a772 \/ ~c2_2 a772 a773 \/ ~ndr1_1 a772 \/ c2_0 \/
% 0.21/0.49     c3_1 a772 \/ c4_2 a772 a773 \/ ssSkC7
% 0.21/0.49  |- ~c1_2 a750 a758 \/ ~c3_2 a750 a758 \/ ~c5_1 a750 \/ ~ndr1_1 a750 \/
% 0.21/0.49     ~ssSkC2 \/ ~ssSkC3 \/ c1_1 a750 \/ c1_2 a750 a751 \/ c5_2 a750 a746 \/
% 0.21/0.49     ssSkC4 \/ ssSkC5
% 0.21/0.49  |- ~c1_2 a726 a758 \/ ~c5_1 a726 \/ ~ndr1_1 a726 \/ ~ssSkC2 \/ ~ssSkC3 \/
% 0.21/0.49     c1_1 a726 \/ c1_2 a726 a727 \/ c5_2 a726 a746 \/ ssSkC0 \/ ssSkC5
% 0.21/0.49  |- ~c1_2 a750 a758 \/ ~c3_2 a750 a758 \/ ~c5_1 a750 \/ ~ndr1_1 a750 \/
% 0.21/0.49     ~ssSkC2 \/ ~ssSkC3 \/ c1_1 a750 \/ c1_2 a750 a746 \/ c1_2 a750 a751 \/
% 0.21/0.49     ssSkC4 \/ ssSkC5
% 0.21/0.50  |- ~c1_2 a726 a758 \/ ~c5_1 a726 \/ ~ndr1_1 a726 \/ ~ssSkC2 \/ ~ssSkC3 \/
% 0.21/0.50     c1_1 a726 \/ c1_2 a726 a727 \/ c1_2 a726 a746 \/ ssSkC0 \/ ssSkC5
% 0.21/0.50  |- ~c2_1 a772 \/ ~c2_2 a772 a773 \/ ~ndr1_1 a772 \/ c1_2 a763 a764 \/
% 0.21/0.50     c2_0 \/ c3_1 a772 \/ c4_2 a772 a773 \/ ssSkC7
% 0.21/0.50  |- ~c2_1 a772 \/ ~c2_2 a772 a773 \/ ~ndr1_1 a772 \/ c2_0 \/
% 0.21/0.50     c2_2 a763 a764 \/ c3_1 a772 \/ c4_2 a772 a773 \/ ssSkC7
% 0.21/0.50  |- ~c2_1 a772 \/ ~c2_2 a772 a773 \/ ~ndr1_1 a772 \/ c2_0 \/ c3_1 a772 \/
% 0.21/0.50     c4_2 a772 a773 \/ c5_2 a763 a764 \/ ssSkC7
% 0.21/0.50  |- ~c1_0 \/ c1_1 a750 \/ c1_2 a750 a751 \/ c1_2 a750 a766 \/
% 0.21/0.50     c2_2 a750 a766 \/ c3_1 a750 \/ c3_2 a750 a758 \/ c4_0 \/ c4_1 a750 \/
% 0.21/0.50     c5_1 a750 \/ ssSkC4 \/ ssSkC5 \/ ssSkC6
% 0.21/0.50  |- ~c2_1 $_87 \/ c2_2 a744 a745 \/ c5_1 a744 \/ c5_2 a744 a745 \/
% 0.21/0.50     ndr1_1 $_87 \/ ssSkC3
% 0.21/0.50  |- c2_2 a744 a745 \/ c5_1 a744 \/ c5_2 a744 a745 \/ ndr1_1 a731 \/ ssSkC3
% 0.21/0.50  |- ~c2_1 $_92 \/ c2_2 a744 a745 \/ c3_2 $_92 a762 \/ c5_1 a744 \/
% 0.21/0.50     c5_2 a744 a745 \/ ssSkC3
% 0.21/0.50  |- c2_2 a744 a745 \/ c3_2 a731 a762 \/ c5_1 a744 \/ c5_2 a744 a745 \/
% 0.21/0.50     ssSkC3
% 0.21/0.50  |- c2_2 a744 a745 \/ c3_2 a772 a762 \/ c5_1 a744 \/ c5_2 a744 a745 \/
% 0.21/0.50     ssSkC3 \/ ssSkC7
% 0.21/0.50  |- ~c2_1 $_97 \/ c2_2 $_97 a762 \/ c2_2 a744 a745 \/ c5_1 a744 \/
% 0.21/0.50     c5_2 a744 a745 \/ ssSkC3
% 0.21/0.50  |- c2_2 a731 a762 \/ c2_2 a744 a745 \/ c5_1 a744 \/ c5_2 a744 a745 \/
% 0.21/0.50     ssSkC3
% 0.21/0.50  |- c2_2 a744 a745 \/ c2_2 a772 a762 \/ c5_1 a744 \/ c5_2 a744 a745 \/
% 0.21/0.50     ssSkC3 \/ ssSkC7
% 0.21/0.50  |- ~c1_2 a726 a727 \/ ~c2_1 a726 \/ ~c3_0 \/ ~c3_1 $_101 \/ ~c5_1 a726 \/
% 0.21/0.50     ~ndr1_1 a726 \/ ndr1_1 $_101 \/ ssSkC0
% 0.21/0.50  |- ~c1_2 a726 a728 \/ ~c2_1 a726 \/ ~c3_0 \/ ~c3_1 $_101 \/ ~c5_1 a726 \/
% 0.21/0.50     ~ndr1_1 a726 \/ ndr1_1 $_101 \/ ssSkC0
% 0.21/0.50  |- ~c1_0 \/ c1_1 a750 \/ c1_2 a750 a766 \/ c2_0 \/ c2_2 a750 a766 \/
% 0.21/0.50     c3_1 a750 \/ c3_2 a750 a751 \/ c3_2 a750 a754 \/ c4_0 \/ c4_1 a750 \/
% 0.21/0.50     c5_1 a750 \/ ssSkC4 \/ ssSkC6
% 0.21/0.50  |- ~c1_2 a726 a727 \/ ~c2_1 a726 \/ ~c3_0 \/ ~c3_1 $_106 \/ ~c5_1 a726 \/
% 0.21/0.50     ~ndr1_1 a726 \/ c3_2 $_106 a761 \/ ssSkC0
% 0.21/0.50  |- ~c1_2 a726 a728 \/ ~c2_1 a726 \/ ~c3_0 \/ ~c3_1 $_106 \/ ~c5_1 a726 \/
% 0.21/0.50     ~ndr1_1 a726 \/ c3_2 $_106 a761 \/ ssSkC0
% 0.21/0.50  |- ~c1_2 a726 a727 \/ ~c2_1 a726 \/ ~c3_0 \/ ~c3_1 $_111 \/ ~c5_1 a726 \/
% 0.21/0.50     ~ndr1_1 a726 \/ c5_2 $_111 a761 \/ ssSkC0
% 0.21/0.50  |- ~c1_2 a726 a728 \/ ~c2_1 a726 \/ ~c3_0 \/ ~c3_1 $_111 \/ ~c5_1 a726 \/
% 0.21/0.50     ~ndr1_1 a726 \/ c5_2 $_111 a761 \/ ssSkC0
% 0.21/0.50  |- ~c1_2 $_116 a761 \/ ~c1_2 a726 a727 \/ ~c2_1 a726 \/ ~c3_0 \/
% 0.21/0.50     ~c3_1 $_116 \/ ~c5_1 a726 \/ ~ndr1_1 a726 \/ ssSkC0
% 0.21/0.50  |- ~c1_2 $_116 a761 \/ ~c1_2 a726 a728 \/ ~c2_1 a726 \/ ~c3_0 \/
% 0.21/0.50     ~c3_1 $_116 \/ ~c5_1 a726 \/ ~ndr1_1 a726 \/ ssSkC0
% 0.21/0.50  |- c1_1 a742 \/ c1_2 a742 $_122 \/ c3_2 a742 $_122 \/ c3_2 a742 a758 \/
% 0.21/0.50     c3_2 a742 a766 \/ c5_1 a742 \/ ssSkC2 \/ ssSkC5 \/ ssSkC6
% 0.21/0.50  |- c1_1 a742 \/ c1_2 a742 a766 \/ c3_2 a742 a758 \/ c3_2 a742 a766 \/
% 0.21/0.50     c5_1 a742 \/ ssSkC2 \/ ssSkC5 \/ ssSkC6
% 0.21/0.50  |- ~c2_2 a742 a766 \/ ~c4_0 \/ ~ndr1_1 a742 \/ c1_1 a742 \/
% 0.21/0.50     c1_2 a742 a766 \/ c3_0 \/ c3_2 a742 a758 \/ c4_1 a742 \/ c5_1 a742 \/
% 0.21/0.50     ssSkC2 \/ ssSkC5 \/ ssSkC6
% 0.21/0.50  |- ~c2_2 a742 $_123 \/ ~c4_0 \/ ~ndr1_1 a742 \/ c1_1 a742 \/
% 0.21/0.50     c1_2 a742 $_123 \/ c3_0 \/ c3_2 a742 a758 \/ c3_2 a742 a766 \/
% 0.21/0.50     c4_1 a742 \/ c5_1 a742 \/ ssSkC2 \/ ssSkC5 \/ ssSkC6
% 0.21/0.50  |- ~c2_1 a726 \/ ~c2_2 a726 $_125 \/ ~ndr1_1 a726 \/ c1_0 \/
% 0.21/0.50     c1_2 a726 a727 \/ c4_2 a726 $_125 \/ c5_2 a726 $_125 \/ ssSkC0
% 0.21/0.50  |- ~c2_1 a742 \/ ~c2_2 a742 $_125 \/ ~ndr1_1 a742 \/ c1_0 \/
% 0.21/0.50     c1_2 a742 $_126 \/ c3_2 a742 $_126 \/ c4_2 a742 $_125 \/
% 0.21/0.50     c5_2 a742 $_125 \/ ssSkC2
% 0.21/0.50  |- ~c2_1 a726 \/ c1_0 \/ c1_2 a726 a727 \/ c4_2 a726 a728 \/
% 0.21/0.50     c5_2 a726 a728 \/ ssSkC0
% 0.21/0.50  |- ~c2_1 a742 \/ c1_0 \/ c1_2 a742 $_130 \/ c3_2 a742 $_130 \/
% 0.21/0.50     c4_2 a742 a743 \/ c5_2 a742 a743 \/ ssSkC2
% 0.21/0.50  |- c1_1 a742 \/ c1_2 a742 $_134 \/ c2_0 \/ c3_2 a742 $_134 \/
% 0.21/0.50     c3_2 a742 a754 \/ c3_2 a742 a766 \/ c4_0 \/ c5_1 a742 \/ ssSkC2 \/
% 0.21/0.50     ssSkC6
% 0.21/0.50  |- c1_1 a742 \/ c1_2 a742 a766 \/ c2_0 \/ c3_2 a742 a754 \/
% 0.21/0.50     c3_2 a742 a766 \/ c4_0 \/ c5_1 a742 \/ ssSkC2 \/ ssSkC6
% 0.21/0.50  |- ~c1_1 $_138 \/ ~c1_2 a726 a758 \/ ~c2_1 $_138 \/ ~c4_0 \/ ~c5_1 a726 \/
% 0.21/0.50     ~ndr1_1 a726 \/ c1_1 a726 \/ c1_2 a726 a727 \/ c2_2 a726 a758 \/
% 0.21/0.50     c3_1 a726 \/ ndr1_1 $_138 \/ ssSkC0 \/ ssSkC5
% 0.21/0.50  |- ~c1_1 $_138 \/ ~c1_2 $_136 a755 \/ ~c2_1 $_138 \/ ~c4_0 \/
% 0.21/0.50     ~c5_1 $_136 \/ ~ndr1_1 $_136 \/ c2_2 $_136 a755 \/ c3_1 $_136 \/
% 0.21/0.50     ndr1_1 $_138 \/ ssSkP0 $_136
% 0.21/0.50  |- ~c1_1 $_144 \/ ~c1_2 a726 a758 \/ ~c2_1 $_144 \/ ~c4_0 \/ ~c5_1 a726 \/
% 0.21/0.50     ~ndr1_1 a726 \/ c1_1 a726 \/ c1_2 a726 a727 \/ c2_2 $_144 a753 \/
% 0.21/0.50     c2_2 a726 a758 \/ c3_1 a726 \/ ssSkC0 \/ ssSkC5
% 0.21/0.50  |- ~c1_1 $_144 \/ ~c1_2 $_142 a755 \/ ~c2_1 $_144 \/ ~c4_0 \/
% 0.21/0.50     ~c5_1 $_142 \/ ~ndr1_1 $_142 \/ c2_2 $_142 a755 \/ c2_2 $_144 a753 \/
% 0.21/0.50     c3_1 $_142 \/ ssSkP0 $_142
% 0.21/0.50  |- ~c1_1 $_150 \/ ~c1_2 $_148 a755 \/ ~c2_1 $_150 \/ ~c4_0 \/
% 0.21/0.50     ~c5_1 $_148 \/ ~c5_2 $_150 a753 \/ ~ndr1_1 $_148 \/ c2_2 $_148 a755 \/
% 0.21/0.50     c3_1 $_148 \/ ssSkP0 $_148
% 0.21/0.50  |- ~c1_1 $_155 \/ ~c1_2 $_155 a753 \/ ~c1_2 a726 a758 \/ ~c2_1 $_155 \/
% 0.21/0.50     ~c4_0 \/ ~c5_1 a726 \/ ~ndr1_1 a726 \/ c1_1 a726 \/ c1_2 a726 a727 \/
% 0.21/0.50     c2_2 a726 a758 \/ c3_1 a726 \/ ssSkC0 \/ ssSkC5
% 0.21/0.50  |- ~c1_1 $_155 \/ ~c1_2 $_153 a755 \/ ~c1_2 $_155 a753 \/ ~c2_1 $_155 \/
% 0.21/0.50     ~c4_0 \/ ~c5_1 $_153 \/ ~ndr1_1 $_153 \/ c2_2 $_153 a755 \/
% 0.21/0.50     c3_1 $_153 \/ ssSkP0 $_153
% 0.21/0.50  |- ~c1_2 a742 $_160 \/ ~c3_2 a742 $_160 \/ ~c4_2 a742 $_160 \/
% 0.21/0.50     ~c4_2 a742 a758 \/ ~ndr1_1 a742 \/ ~ssSkC4 \/ c1_1 a742 \/
% 0.21/0.50     c1_2 a742 $_50 \/ c2_0 \/ c3_2 a742 $_50 \/ c3_2 a742 a752 \/
% 0.21/0.50     c3_2 a742 a758 \/ ssSkC2 \/ ssSkC5
% 0.21/0.50  |- ~c1_2 a742 $_163 \/ ~c3_2 a742 $_163 \/ ~c4_2 a742 $_163 \/
% 0.21/0.50     ~c4_2 a742 a758 \/ ~ndr1_1 a742 \/ ~ssSkC4 \/ c1_1 a742 \/
% 0.21/0.50     c1_2 a742 $_50 \/ c2_0 \/ c3_2 a742 $_50 \/ c3_2 a742 a758 \/
% 0.21/0.50     c5_2 a742 a752 \/ ssSkC2 \/ ssSkC5
% 0.21/0.50  |- ~c2_1 a772 \/ ~c2_2 a772 a773 \/ ~ndr1_1 a763 \/ ~ndr1_1 a772 \/ c2_0 \/
% 0.21/0.50     c2_2 a763 $_168 \/ c3_1 a772 \/ c4_2 a763 $_168 \/ c4_2 a772 a773 \/
% 0.21/0.50     c5_2 a763 $_168 \/ ssSkC7
% 0.21/0.50  |- ~c1_2 a742 $_170 \/ ~c3_2 a742 $_170 \/ ~c4_2 a742 $_170 \/
% 0.21/0.50     ~ndr1_1 a742 \/ ~ssSkC4 \/ c1_1 a742 \/ c1_2 a742 $_171 \/
% 0.21/0.50     c1_2 a742 a758 \/ c2_0 \/ c3_2 a742 $_171 \/ c3_2 a742 a752 \/
% 0.21/0.50     c3_2 a742 a758 \/ ssSkC2 \/ ssSkC5
% 0.21/0.50  |- ~c1_2 a742 $_172 \/ ~c3_2 a742 $_172 \/ ~c4_2 a742 $_172 \/
% 0.21/0.50     ~ndr1_1 a742 \/ ~ssSkC4 \/ c1_1 a742 \/ c1_2 a742 $_173 \/ c2_0 \/
% 0.21/0.50     c3_2 a742 $_173 \/ c3_2 a742 a752 \/ c3_2 a742 a754 \/ c4_0 \/ ssSkC2
% 0.21/0.50  |- ~c1_2 a742 $_176 \/ ~c3_2 a742 $_176 \/ ~c4_2 a742 $_176 \/
% 0.21/0.50     ~ndr1_1 a742 \/ ~ssSkC4 \/ c1_1 a742 \/ c1_2 a742 $_177 \/ c2_0 \/
% 0.21/0.50     c3_2 a742 $_177 \/ c3_2 a742 a754 \/ c4_0 \/ c5_2 a742 a752 \/ ssSkC2
% 0.21/0.50  |- ~c1_2 a742 $_180 \/ ~c3_2 a742 $_180 \/ ~c4_2 a742 $_180 \/
% 0.21/0.50     ~ndr1_1 a742 \/ ~ssSkC4 \/ c1_1 a742 \/ c1_2 a742 $_181 \/
% 0.21/0.50     c1_2 a742 a758 \/ c2_0 \/ c3_2 a742 $_181 \/ c3_2 a742 a758 \/
% 0.21/0.50     c5_2 a742 a752 \/ ssSkC2 \/ ssSkC5
% 0.21/0.50  SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.21/0.50  
%------------------------------------------------------------------------------