↑ Up

Metis---2.4.SAT-Sat.s

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

% Computer : n009.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:05:45 EDT 2022

% Result   : Satisfiable 0.49s 0.64s
% Output   : Saturation 0.52s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12  % Problem  : SYN774-1 : TPTP v8.1.0. Released v2.5.0.
% 0.03/0.12  % Command  : metis --show proof --show saturation %s
% 0.13/0.33  % Computer : n009.cluster.edu
% 0.13/0.33  % Model    : x86_64 x86_64
% 0.13/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33  % Memory   : 8042.1875MB
% 0.13/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33  % CPULimit : 300
% 0.13/0.33  % WCLimit  : 600
% 0.13/0.33  % DateTime : Mon Jul 11 17:36:07 EDT 2022
% 0.13/0.33  % CPUTime  : 
% 0.13/0.34  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.49/0.64  % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.49/0.64  
% 0.49/0.64  SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.49/0.64  |- ssRr (skf3 $U) $U
% 0.49/0.64  |- ssRr $U (skf2 $U)
% 0.49/0.64  |- ~ssPv3 $U \/ ~ssRr $U $V \/ ssPv1 $V \/ ssPv3 $V \/ ssPv4 $V
% 0.49/0.64  |- ~ssPv1 $V \/ ~ssPv3 $V \/ ~ssRr $U $V \/ ssPv2 $U \/ ssPv4 $V
% 0.49/0.64  |- ~ssPv3 $U \/ ~ssPv4 $V \/ ~ssRr $U $V \/ ssPv2 $V \/ ssPv3 $V
% 0.49/0.64  |- ~ssPv3 $V \/ ~ssPv4 $V \/ ~ssRr $U $V \/ ssPv1 $U \/ ssPv1 $V
% 0.49/0.64  |- ~ssPv1 $V \/ ~ssPv3 $V \/ ~ssPv4 $U \/ ~ssRr $U $V \/ ssPv2 $V
% 0.49/0.64  |- ~ssPv1 $U \/ ~ssPv1 $V \/ ~ssPv2 $V \/ ~ssPv4 $V \/ ~ssRr $U $V
% 0.49/0.64  |- ~ssPv3 $V \/ ~ssRr $U $V \/ ~ssRr $V $W \/ ssPv3 $U \/ ssPv4 $V \/
% 0.49/0.64     ssPv4 $W
% 0.49/0.64  |- ~ssPv4 $V \/ ~ssRr $U $V \/ ~ssRr $W $V \/ ssPv1 $W \/ ssPv2 $U \/
% 0.49/0.64     ssPv3 $V
% 0.49/0.64  |- ~ssPv4 $V \/ ~ssRr $U $V \/ ~ssRr $U $W \/ ssPv3 $U \/ ssPv3 $W \/
% 0.49/0.64     ssPv4 $U
% 0.49/0.64  |- ~ssPv1 $U \/ ~ssRr $U $V \/ ~ssRr $U $W \/ ssPv2 $U \/ ssPv2 $W \/
% 0.49/0.64     ssPv4 $V
% 0.49/0.64  |- ~ssPv3 $U \/ ~ssPv4 $U \/ ~ssPv4 $V \/ ~ssRr $U $V \/ ~ssRr $U $W \/
% 0.49/0.64     ssPv4 $W
% 0.49/0.64  |- ~ssPv2 $V \/ ~ssPv2 $W \/ ~ssPv3 $V \/ ~ssRr $U $V \/ ~ssRr $V $W \/
% 0.49/0.64     ssPv1 $U
% 0.49/0.64  |- ~ssPv1 $V \/ ~ssPv3 $U \/ ~ssPv4 $V \/ ~ssRr $U $V \/ ~ssRr $W $V \/
% 0.49/0.64     ssPv4 $W
% 0.49/0.64  |- ~ssPv1 $V \/ ~ssPv2 $U \/ ~ssPv3 $V \/ ~ssRr $U $V \/ ~ssRr $V $W \/
% 0.49/0.64     ssPv3 $W
% 0.49/0.64  |- ~ssPv2 $U \/ ~ssPv3 $V \/ ~ssPv3 $W \/ ~ssRr $U $V \/ ~ssRr $V $W \/
% 0.49/0.64     ssPv4 $V
% 0.49/0.64  |- ~ssPv2 $W \/ ~ssPv3 $U \/ ~ssPv4 $V \/ ~ssRr $U $V \/ ~ssRr $W $V \/
% 0.49/0.64     ssPv2 $V
% 0.49/0.64  |- ~ssPv3 $V \/ ~ssPv4 $U \/ ~ssPv4 $V \/ ~ssPv4 $W \/ ~ssRr $U $V \/
% 0.49/0.64     ~ssRr $V $W
% 0.49/0.64  |- ~ssPv1 $W \/ ~ssPv2 $U \/ ~ssPv2 $V \/ ~ssPv3 $U \/ ~ssRr $U $V \/
% 0.49/0.64     ~ssRr $U $W
% 0.49/0.64  |- ~ssPv1 $U \/ ~ssPv1 $W \/ ~ssPv3 $U \/ ~ssPv3 $V \/ ~ssRr $U $V \/
% 0.49/0.64     ~ssRr $U $W
% 0.49/0.64  |- ~ssPv2 $X \/ ~ssRr $U $V \/ ~ssRr $V $X \/ ~ssRr $W $V \/ ssPv2 $V \/
% 0.49/0.64     ssPv2 $W \/ ssPv3 $U
% 0.49/0.64  |- ~ssPv1 $U \/ ~ssPv4 $X \/ ~ssRr $U $V \/ ~ssRr $V $X \/ ~ssRr $W $V \/
% 0.49/0.64     ssPv3 $V \/ ssPv3 $W
% 0.49/0.64  |- ~ssPv2 $U \/ ~ssPv3 $V \/ ~ssRr $U $V \/ ~ssRr $V $X \/ ~ssRr $W $V \/
% 0.49/0.64     ssPv3 $X \/ ssPv4 $W
% 0.49/0.64  |- ~ssPv2 $X \/ ~ssPv3 $W \/ ~ssRr $U $V \/ ~ssRr $V $W \/ ~ssRr $V $X \/
% 0.49/0.64     ssPv2 $U \/ ssPv2 $V
% 0.49/0.64  |- ~ssPv2 $U \/ ~ssPv4 $X \/ ~ssRr $U $V \/ ~ssRr $V $X \/ ~ssRr $W $V \/
% 0.49/0.64     ssPv1 $V \/ ssPv4 $W
% 0.49/0.64  |- ~ssPv1 $U \/ ~ssPv3 $W \/ ~ssPv4 $V \/ ~ssRr $U $V \/ ~ssRr $V $W \/
% 0.49/0.64     ~ssRr $V $X \/ ssPv2 $X
% 0.49/0.64  |- ~ssPv1 $W \/ ~ssPv2 $V \/ ~ssPv4 $U \/ ~ssRr $U $V \/ ~ssRr $V $W \/
% 0.49/0.64     ~ssRr $V $X \/ ssPv4 $X
% 0.49/0.64  |- ~ssPv1 $W \/ ~ssPv2 $U \/ ~ssPv2 $V \/ ~ssRr $U $V \/ ~ssRr $V $W \/
% 0.49/0.64     ~ssRr $V $X \/ ssPv1 $X
% 0.49/0.64  |- ~ssPv1 $W \/ ~ssPv2 $U \/ ~ssPv3 $V \/ ~ssRr $U $V \/ ~ssRr $V $X \/
% 0.49/0.64     ~ssRr $W $V \/ ssPv1 $X
% 0.49/0.64  |- ~ssPv1 $V \/ ~ssPv2 $U \/ ~ssPv4 $X \/ ~ssRr $U $V \/ ~ssRr $V $X \/
% 0.49/0.64     ~ssRr $W $V \/ ssPv1 $W
% 0.49/0.64  |- ~ssPv2 $U \/ ~ssPv3 $V \/ ~ssPv3 $X \/ ~ssPv4 $W \/ ~ssRr $U $V \/
% 0.49/0.64     ~ssRr $V $W \/ ~ssRr $V $X
% 0.49/0.64  |- ~ssPv4 $V \/ ~ssRr $W $V \/ ssPv1 $W \/ ssPv2 $W \/ ssPv3 $V
% 0.49/0.64  |- ~ssPv4 $W \/ ~ssRr $U $W \/ ssPv3 $U \/ ssPv3 $W \/ ssPv4 $U
% 0.49/0.64  |- ~ssPv1 $U \/ ~ssRr $U $W \/ ssPv2 $U \/ ssPv2 $W \/ ssPv4 $W
% 0.49/0.64  |- ~ssPv2 $W \/ ~ssPv3 $W \/ ~ssRr $W $W \/ ssPv1 $W
% 0.49/0.64  |- ~ssPv1 $V \/ ~ssPv3 $W \/ ~ssPv4 $V \/ ~ssRr $W $V \/ ssPv4 $W
% 0.49/0.64  |- ~ssPv2 $W \/ ~ssPv3 $W \/ ~ssRr $W $W \/ ssPv4 $W
% 0.49/0.64  |- ~ssPv2 $W \/ ~ssPv3 $W \/ ~ssPv4 $V \/ ~ssRr $W $V \/ ssPv2 $V
% 0.49/0.64  |- ~ssPv3 $W \/ ~ssPv4 $W \/ ~ssRr $W $W
% 0.49/0.64  |- ~ssPv1 $W \/ ~ssPv2 $U \/ ~ssPv2 $W \/ ~ssPv3 $U \/ ~ssRr $U $W
% 0.49/0.64  |- ~ssPv1 $U \/ ~ssPv1 $W \/ ~ssPv3 $U \/ ~ssPv3 $W \/ ~ssRr $U $W
% 0.49/0.64  |- ~ssPv2 $X \/ ~ssRr $V $X \/ ~ssRr $W $V \/ ssPv2 $V \/ ssPv2 $W \/
% 0.49/0.64     ssPv3 $W
% 0.49/0.64  |- ~ssPv1 $W \/ ~ssPv4 $X \/ ~ssRr $V $X \/ ~ssRr $W $V \/ ssPv3 $V \/
% 0.49/0.64     ssPv3 $W
% 0.49/0.64  |- ~ssPv1 $U \/ ~ssPv4 $W \/ ~ssRr $U $W \/ ~ssRr $W $W \/ ssPv3 $W
% 0.49/0.64  |- ~ssPv1 $W \/ ~ssPv4 $W \/ ~ssRr $W $W \/ ssPv3 $W
% 0.49/0.64  |- ~ssPv2 $W \/ ~ssPv3 $V \/ ~ssRr $V $X \/ ~ssRr $W $V \/ ssPv3 $X \/
% 0.49/0.64     ssPv4 $W
% 0.49/0.64  |- ~ssPv2 $X \/ ~ssPv3 $W \/ ~ssRr $W $W \/ ~ssRr $W $X \/ ssPv2 $W
% 0.49/0.64  |- ~ssPv2 $X \/ ~ssPv3 $X \/ ~ssRr $U $V \/ ~ssRr $V $X \/ ssPv2 $U \/
% 0.49/0.64     ssPv2 $V
% 0.49/0.64  |- ~ssPv2 $X \/ ~ssPv4 $X \/ ~ssRr $W $X \/ ~ssRr $X $X \/ ssPv1 $X \/
% 0.49/0.64     ssPv4 $W
% 0.49/0.64  |- ~ssPv2 $W \/ ~ssPv4 $X \/ ~ssRr $V $X \/ ~ssRr $W $V \/ ssPv1 $V \/
% 0.49/0.64     ssPv4 $W
% 0.49/0.64  |- ~ssPv1 $X \/ ~ssPv3 $W \/ ~ssPv4 $X \/ ~ssRr $X $W \/ ~ssRr $X $X \/
% 0.49/0.64     ssPv2 $X
% 0.49/0.64  |- ~ssPv1 $U \/ ~ssPv3 $X \/ ~ssPv4 $V \/ ~ssRr $U $V \/ ~ssRr $V $X \/
% 0.49/0.64     ssPv2 $X
% 0.49/0.64  |- ~ssPv1 $X \/ ~ssPv2 $V \/ ~ssPv4 $U \/ ~ssRr $U $V \/ ~ssRr $V $X \/
% 0.49/0.64     ssPv4 $X
% 0.49/0.64  |- ~ssPv1 $W \/ ~ssPv2 $W \/ ~ssRr $W $W \/ ~ssRr $W $X \/ ssPv1 $X
% 0.49/0.64  |- ~ssPv1 $W \/ ~ssPv2 $X \/ ~ssRr $X $W \/ ~ssRr $X $X \/ ssPv1 $X
% 0.49/0.64  |- ~ssPv1 $W \/ ~ssPv2 $W \/ ~ssPv3 $V \/ ~ssRr $V $X \/ ~ssRr $W $V \/
% 0.49/0.64     ssPv1 $X
% 0.49/0.64  |- ~ssPv1 $V \/ ~ssPv2 $W \/ ~ssPv4 $X \/ ~ssRr $V $X \/ ~ssRr $W $V \/
% 0.49/0.64     ssPv1 $W
% 0.49/0.64  |- ~ssPv2 $X \/ ~ssPv3 $X \/ ~ssPv4 $W \/ ~ssRr $X $W \/ ~ssRr $X $X
% 0.49/0.64  |- ~ssPv2 $U \/ ~ssPv3 $V \/ ~ssPv3 $X \/ ~ssPv4 $X \/ ~ssRr $U $V \/
% 0.49/0.64     ~ssRr $V $X
% 0.49/0.64  |- ~ssPv3 (skf3 $_7) \/ ssPv1 $_7 \/ ssPv3 $_7 \/ ssPv4 $_7
% 0.49/0.64  |- ~ssPv3 $_6 \/ ssPv1 (skf2 $_6) \/ ssPv3 (skf2 $_6) \/ ssPv4 (skf2 $_6)
% 0.49/0.64  |- ~ssPv1 $_11 \/ ~ssPv3 $_11 \/ ssPv2 (skf3 $_11) \/ ssPv4 $_11
% 0.49/0.64  |- ~ssPv1 (skf2 $_10) \/ ~ssPv3 (skf2 $_10) \/ ssPv2 $_10 \/
% 0.49/0.64     ssPv4 (skf2 $_10)
% 0.49/0.64  |- ~ssPv3 (skf3 $_15) \/ ~ssPv4 $_15 \/ ssPv2 $_15 \/ ssPv3 $_15
% 0.49/0.64  |- ~ssPv3 $_14 \/ ~ssPv4 (skf2 $_14) \/ ssPv2 (skf2 $_14) \/
% 0.49/0.64     ssPv3 (skf2 $_14)
% 0.49/0.64  |- ~ssPv3 $_19 \/ ~ssPv4 $_19 \/ ssPv1 $_19 \/ ssPv1 (skf3 $_19)
% 0.49/0.64  |- ~ssPv3 (skf2 $_18) \/ ~ssPv4 (skf2 $_18) \/ ssPv1 $_18 \/
% 0.49/0.64     ssPv1 (skf2 $_18)
% 0.49/0.64  |- ~ssPv1 $_23 \/ ~ssPv3 $_23 \/ ~ssPv4 (skf3 $_23) \/ ssPv2 $_23
% 0.49/0.64  |- ~ssPv1 (skf2 $_22) \/ ~ssPv3 (skf2 $_22) \/ ~ssPv4 $_22 \/
% 0.49/0.64     ssPv2 (skf2 $_22)
% 0.49/0.64  |- ~ssPv1 $_27 \/ ~ssPv1 (skf3 $_27) \/ ~ssPv2 $_27 \/ ~ssPv4 $_27
% 0.49/0.64  |- ~ssPv1 $_26 \/ ~ssPv1 (skf2 $_26) \/ ~ssPv2 (skf2 $_26) \/
% 0.49/0.64     ~ssPv4 (skf2 $_26)
% 0.49/0.64  |- ~ssPv4 $_30 \/ ssPv1 (skf3 $_30) \/ ssPv2 (skf3 $_30) \/ ssPv3 $_30
% 0.49/0.64  |- ~ssPv4 (skf2 $_31) \/ ssPv1 $_31 \/ ssPv2 $_31 \/ ssPv3 (skf2 $_31)
% 0.49/0.64  |- ~ssPv4 $_35 \/ ssPv3 $_35 \/ ssPv3 (skf3 $_35) \/ ssPv4 (skf3 $_35)
% 0.49/0.64  |- ~ssPv4 (skf2 $_34) \/ ssPv3 $_34 \/ ssPv3 (skf2 $_34) \/ ssPv4 $_34
% 0.49/0.64  |- ~ssPv1 (skf3 $_39) \/ ssPv2 $_39 \/ ssPv2 (skf3 $_39) \/ ssPv4 $_39
% 0.49/0.64  |- ~ssPv1 $_38 \/ ssPv2 $_38 \/ ssPv2 (skf2 $_38) \/ ssPv4 (skf2 $_38)
% 0.49/0.64  |- ~ssPv1 $_42 \/ ~ssPv3 (skf3 $_42) \/ ~ssPv4 $_42 \/ ssPv4 (skf3 $_42)
% 0.49/0.64  |- ~ssPv1 (skf2 $_43) \/ ~ssPv3 $_43 \/ ~ssPv4 (skf2 $_43) \/ ssPv4 $_43
% 0.49/0.64  |- ~ssPv2 (skf3 $_46) \/ ~ssPv3 (skf3 $_46) \/ ~ssPv4 $_46 \/ ssPv2 $_46
% 0.49/0.64  |- ~ssPv2 $_47 \/ ~ssPv3 $_47 \/ ~ssPv4 (skf2 $_47) \/ ssPv2 (skf2 $_47)
% 0.49/0.64  |- ~ssPv1 $_51 \/ ~ssPv2 $_51 \/ ~ssPv2 (skf3 $_51) \/ ~ssPv3 (skf3 $_51)
% 0.49/0.64  |- ~ssPv1 (skf2 $_50) \/ ~ssPv2 $_50 \/ ~ssPv2 (skf2 $_50) \/ ~ssPv3 $_50
% 0.49/0.64  |- ~ssPv1 $_55 \/ ~ssPv1 (skf3 $_55) \/ ~ssPv3 $_55 \/ ~ssPv3 (skf3 $_55)
% 0.49/0.64  |- ~ssPv1 $_54 \/ ~ssPv1 (skf2 $_54) \/ ~ssPv3 $_54 \/ ~ssPv3 (skf2 $_54)
% 0.49/0.64  |- ~ssPv1 (skf3 $_59) \/ ~ssPv4 $_59 \/ ~ssRr $_59 $_59 \/ ssPv3 $_59
% 0.49/0.64  |- ~ssPv2 (skf2 $_61) \/ ~ssPv3 $_61 \/ ~ssRr $_61 $_61 \/ ssPv2 $_61
% 0.49/0.64  |- ~ssPv1 $_64 \/ ~ssPv2 $_64 \/ ~ssRr $_64 $_64 \/ ssPv1 (skf2 $_64)
% 0.49/0.64  |- ~ssPv1 (skf2 $_68) \/ ~ssPv2 $_68 \/ ~ssRr $_68 $_68 \/ ssPv1 $_68
% 0.49/0.64  |- ~ssPv2 $_71 \/ ~ssPv3 $_71 \/ ~ssPv4 (skf2 $_71) \/ ~ssRr $_71 $_71
% 0.49/0.64  |- ~ssPv2 $_74 \/ ~ssPv4 $_74 \/ ~ssRr $_74 $_74 \/ ssPv1 $_74 \/
% 0.49/0.64     ssPv4 (skf3 $_74)
% 0.49/0.64  |- ~ssPv1 $_77 \/ ~ssPv3 (skf2 $_77) \/ ~ssPv4 $_77 \/ ~ssRr $_77 $_77 \/
% 0.49/0.64     ssPv2 $_77
% 0.49/0.64  |- ~ssPv3 $_80 \/ ~ssRr $_80 $_81 \/ ssPv3 (skf3 $_80) \/ ssPv4 $_80 \/
% 0.49/0.64     ssPv4 $_81
% 0.49/0.64  |- ~ssPv3 (skf2 $_79) \/ ~ssRr (skf2 $_79) $_81 \/ ssPv3 $_79 \/
% 0.49/0.64     ssPv4 $_81 \/ ssPv4 (skf2 $_79)
% 0.49/0.64  |- ~ssPv3 (skf3 $_81) \/ ~ssRr $_79 (skf3 $_81) \/ ssPv3 $_79 \/
% 0.49/0.64     ssPv4 $_81 \/ ssPv4 (skf3 $_81)
% 0.49/0.64  |- ~ssPv3 $_80 \/ ~ssRr $_79 $_80 \/ ssPv3 $_79 \/ ssPv4 $_80 \/
% 0.49/0.64     ssPv4 (skf2 $_80)
% 0.49/0.64  |- ~ssPv3 (skf2 $_82) \/ ssPv3 $_82 \/ ssPv4 (skf2 $_82) \/
% 0.49/0.64     ssPv4 (skf2 (skf2 $_82))
% 0.49/0.64  |- ~ssPv3 (skf3 $_86) \/ ssPv3 (skf3 (skf3 $_86)) \/ ssPv4 $_86 \/
% 0.49/0.64     ssPv4 (skf3 $_86)
% 0.49/0.64  |- ~ssPv3 $_85 \/ ssPv3 (skf3 $_85) \/ ssPv4 $_85 \/ ssPv4 (skf2 $_85)
% 0.49/0.64  |- ~ssPv4 $_94 \/ ~ssRr $_95 $_94 \/ ssPv1 $_95 \/ ssPv2 (skf3 $_94) \/
% 0.49/0.64     ssPv3 $_94
% 0.49/0.64  |- ~ssPv4 (skf2 $_93) \/ ~ssRr $_95 (skf2 $_93) \/ ssPv1 $_95 \/
% 0.49/0.64     ssPv2 $_93 \/ ssPv3 (skf2 $_93)
% 0.49/0.64  |- ~ssPv4 $_94 \/ ~ssRr $_93 $_94 \/ ssPv1 (skf3 $_94) \/ ssPv2 $_93 \/
% 0.49/0.64     ssPv3 $_94
% 0.49/0.64  |- ~ssPv4 (skf2 $_95) \/ ~ssRr $_93 (skf2 $_95) \/ ssPv1 $_95 \/
% 0.49/0.64     ssPv2 $_93 \/ ssPv3 (skf2 $_95)
% 0.49/0.64  |- ~ssPv4 (skf2 $_97) \/ ssPv1 $_97 \/ ssPv2 (skf3 (skf2 $_97)) \/
% 0.49/0.64     ssPv3 (skf2 $_97)
% 0.49/0.64  |- ~ssPv4 (skf2 $_99) \/ ssPv1 (skf3 (skf2 $_99)) \/ ssPv2 $_99 \/
% 0.49/0.64     ssPv3 (skf2 $_99)
% 0.49/0.64  |- ~ssPv4 $_107 \/ ~ssRr (skf3 $_107) $_108 \/ ssPv3 $_108 \/
% 0.49/0.64     ssPv3 (skf3 $_107) \/ ssPv4 (skf3 $_107)
% 0.49/0.64  |- ~ssPv4 (skf2 $_106) \/ ~ssRr $_106 $_108 \/ ssPv3 $_106 \/
% 0.49/0.64     ssPv3 $_108 \/ ssPv4 $_106
% 0.49/0.64  |- ~ssPv4 $_107 \/ ~ssRr (skf3 $_108) $_107 \/ ssPv3 $_108 \/
% 0.49/0.64     ssPv3 (skf3 $_108) \/ ssPv4 (skf3 $_108)
% 0.49/0.64  |- ~ssPv4 $_107 \/ ~ssRr $_106 $_107 \/ ssPv3 $_106 \/
% 0.49/0.64     ssPv3 (skf2 $_106) \/ ssPv4 $_106
% 0.49/0.64  |- ~ssPv4 (skf2 (skf3 $_110)) \/ ssPv3 $_110 \/ ssPv3 (skf3 $_110) \/
% 0.49/0.64     ssPv4 (skf3 $_110)
% 0.49/0.64  |- ~ssPv4 $_115 \/ ssPv3 (skf2 (skf3 $_115)) \/ ssPv3 (skf3 $_115) \/
% 0.49/0.64     ssPv4 (skf3 $_115)
% 0.49/0.64  |- ~ssPv1 (skf3 $_120) \/ ~ssRr (skf3 $_120) $_121 \/ ssPv2 $_121 \/
% 0.49/0.64     ssPv2 (skf3 $_120) \/ ssPv4 $_120
% 0.49/0.64  |- ~ssPv1 $_119 \/ ~ssRr $_119 $_121 \/ ssPv2 $_119 \/ ssPv2 $_121 \/
% 0.49/0.64     ssPv4 (skf2 $_119)
% 0.49/0.64  |- ~ssPv1 (skf3 $_121) \/ ~ssRr (skf3 $_121) $_120 \/ ssPv2 $_121 \/
% 0.49/0.64     ssPv2 (skf3 $_121) \/ ssPv4 $_120
% 0.49/0.65  |- ~ssPv1 $_119 \/ ~ssRr $_119 $_120 \/ ssPv2 $_119 \/
% 0.49/0.65     ssPv2 (skf2 $_119) \/ ssPv4 $_120
% 0.49/0.65  |- ~ssPv1 (skf3 $_123) \/ ssPv2 $_123 \/ ssPv2 (skf3 $_123) \/
% 0.49/0.65     ssPv4 (skf2 (skf3 $_123))
% 0.49/0.65  |- ~ssPv1 (skf3 $_126) \/ ssPv2 (skf2 (skf3 $_126)) \/
% 0.49/0.65     ssPv2 (skf3 $_126) \/ ssPv4 $_126
% 0.49/0.65  |- ~ssPv3 (skf3 $_133) \/ ~ssPv4 $_133 \/ ~ssPv4 (skf3 $_133) \/
% 0.49/0.65     ~ssRr (skf3 $_133) $_134 \/ ssPv4 $_134
% 0.49/0.65  |- ~ssPv3 $_132 \/ ~ssPv4 $_132 \/ ~ssPv4 (skf2 $_132) \/
% 0.49/0.65     ~ssRr $_132 $_134 \/ ssPv4 $_134
% 0.49/0.65  |- ~ssPv3 (skf3 $_134) \/ ~ssPv4 $_133 \/ ~ssPv4 (skf3 $_134) \/
% 0.49/0.65     ~ssRr (skf3 $_134) $_133 \/ ssPv4 $_134
% 0.49/0.65  |- ~ssPv3 $_132 \/ ~ssPv4 $_132 \/ ~ssPv4 $_133 \/ ~ssRr $_132 $_133 \/
% 0.49/0.65     ssPv4 (skf2 $_132)
% 0.49/0.65  |- ~ssPv3 (skf3 $_136) \/ ~ssPv4 (skf2 (skf3 $_136)) \/
% 0.49/0.65     ~ssPv4 (skf3 $_136) \/ ssPv4 $_136
% 0.49/0.65  |- ~ssPv3 (skf3 $_139) \/ ~ssPv4 $_139 \/ ~ssPv4 (skf3 $_139) \/
% 0.49/0.65     ssPv4 (skf2 (skf3 $_139))
% 0.49/0.65  |- ~ssPv2 $_146 \/ ~ssPv2 $_147 \/ ~ssPv3 $_146 \/ ~ssRr $_146 $_147 \/
% 0.49/0.65     ssPv1 (skf3 $_146)
% 0.49/0.65  |- ~ssPv2 $_147 \/ ~ssPv2 (skf2 $_145) \/ ~ssPv3 (skf2 $_145) \/
% 0.49/0.65     ~ssRr (skf2 $_145) $_147 \/ ssPv1 $_145
% 0.49/0.65  |- ~ssPv2 $_147 \/ ~ssPv2 (skf3 $_147) \/ ~ssPv3 (skf3 $_147) \/
% 0.49/0.65     ~ssRr $_145 (skf3 $_147) \/ ssPv1 $_145
% 0.49/0.65  |- ~ssPv2 $_146 \/ ~ssPv2 (skf2 $_146) \/ ~ssPv3 $_146 \/
% 0.49/0.65     ~ssRr $_145 $_146 \/ ssPv1 $_145
% 0.49/0.65  |- ~ssPv2 (skf2 $_148) \/ ~ssPv2 (skf2 (skf2 $_148)) \/
% 0.49/0.65     ~ssPv3 (skf2 $_148) \/ ssPv1 $_148
% 0.49/0.65  |- ~ssPv2 $_152 \/ ~ssPv2 (skf3 $_152) \/ ~ssPv3 (skf3 $_152) \/
% 0.49/0.65     ssPv1 (skf3 (skf3 $_152))
% 0.49/0.65  |- ~ssPv2 $_151 \/ ~ssPv2 (skf2 $_151) \/ ~ssPv3 $_151 \/
% 0.49/0.65     ssPv1 (skf3 $_151)
% 0.49/0.65  |- ~ssPv1 $_160 \/ ~ssPv3 (skf3 $_160) \/ ~ssPv4 $_160 \/
% 0.49/0.65     ~ssRr $_161 $_160 \/ ssPv4 $_161
% 0.49/0.65  |- ~ssPv1 (skf2 $_159) \/ ~ssPv3 $_159 \/ ~ssPv4 (skf2 $_159) \/
% 0.49/0.65     ~ssRr $_161 (skf2 $_159) \/ ssPv4 $_161
% 0.49/0.65  |- ~ssPv1 $_160 \/ ~ssPv3 $_159 \/ ~ssPv4 $_160 \/ ~ssRr $_159 $_160 \/
% 0.49/0.65     ssPv4 (skf3 $_160)
% 0.49/0.65  |- ~ssPv1 (skf2 $_161) \/ ~ssPv3 $_159 \/ ~ssPv4 (skf2 $_161) \/
% 0.49/0.65     ~ssRr $_159 (skf2 $_161) \/ ssPv4 $_161
% 0.49/0.65  |- ~ssPv1 (skf2 $_163) \/ ~ssPv3 (skf3 (skf2 $_163)) \/
% 0.49/0.65     ~ssPv4 (skf2 $_163) \/ ssPv4 $_163
% 0.49/0.65  |- ~ssPv1 (skf2 $_165) \/ ~ssPv3 $_165 \/ ~ssPv4 (skf2 $_165) \/
% 0.49/0.65     ssPv4 (skf3 (skf2 $_165))
% 0.49/0.65  |- ~ssPv1 $_173 \/ ~ssPv2 (skf3 $_173) \/ ~ssPv3 $_173 \/
% 0.49/0.65     ~ssRr $_173 $_174 \/ ssPv3 $_174
% 0.49/0.65  |- ~ssPv1 (skf2 $_172) \/ ~ssPv2 $_172 \/ ~ssPv3 (skf2 $_172) \/
% 0.49/0.65     ~ssRr (skf2 $_172) $_174 \/ ssPv3 $_174
% 0.49/0.65  |- ~ssPv1 (skf3 $_174) \/ ~ssPv2 $_172 \/ ~ssPv3 (skf3 $_174) \/
% 0.49/0.65     ~ssRr $_172 (skf3 $_174) \/ ssPv3 $_174
% 0.49/0.65  |- ~ssPv1 $_173 \/ ~ssPv2 $_172 \/ ~ssPv3 $_173 \/ ~ssRr $_172 $_173 \/
% 0.49/0.65     ssPv3 (skf2 $_173)
% 0.49/0.65  |- ~ssPv1 (skf3 $_176) \/ ~ssPv2 (skf3 (skf3 $_176)) \/
% 0.49/0.65     ~ssPv3 (skf3 $_176) \/ ssPv3 $_176
% 0.49/0.65  |- ~ssPv1 $_175 \/ ~ssPv2 (skf3 $_175) \/ ~ssPv3 $_175 \/
% 0.49/0.65     ssPv3 (skf2 $_175)
% 0.49/0.65  |- ~ssPv1 (skf2 $_179) \/ ~ssPv2 $_179 \/ ~ssPv3 (skf2 $_179) \/
% 0.49/0.65     ssPv3 (skf2 (skf2 $_179))
% 0.49/0.65  |- ~ssPv2 (skf3 $_187) \/ ~ssPv3 $_187 \/ ~ssPv3 $_188 \/
% 0.49/0.65     ~ssRr $_187 $_188 \/ ssPv4 $_187
% 0.49/0.65  |- ~ssPv2 $_186 \/ ~ssPv3 $_188 \/ ~ssPv3 (skf2 $_186) \/
% 0.49/0.65     ~ssRr (skf2 $_186) $_188 \/ ssPv4 (skf2 $_186)
% 0.49/0.65  |- ~ssPv2 $_186 \/ ~ssPv3 $_188 \/ ~ssPv3 (skf3 $_188) \/
% 0.49/0.65     ~ssRr $_186 (skf3 $_188) \/ ssPv4 (skf3 $_188)
% 0.49/0.65  |- ~ssPv2 $_186 \/ ~ssPv3 $_187 \/ ~ssPv3 (skf2 $_187) \/
% 0.49/0.65     ~ssRr $_186 $_187 \/ ssPv4 $_187
% 0.49/0.65  |- ~ssPv2 (skf3 (skf3 $_190)) \/ ~ssPv3 $_190 \/ ~ssPv3 (skf3 $_190) \/
% 0.49/0.65     ssPv4 (skf3 $_190)
% 0.49/0.65  |- ~ssPv2 (skf3 $_189) \/ ~ssPv3 $_189 \/ ~ssPv3 (skf2 $_189) \/
% 0.49/0.65     ssPv4 $_189
% 0.49/0.65  |- ~ssPv2 $_193 \/ ~ssPv3 (skf2 $_193) \/ ~ssPv3 (skf2 (skf2 $_193)) \/
% 0.49/0.65     ssPv4 (skf2 $_193)
% 0.49/0.65  |- ~ssPv2 $_202 \/ ~ssPv3 (skf3 $_201) \/ ~ssPv4 $_201 \/
% 0.49/0.65     ~ssRr $_202 $_201 \/ ssPv2 $_201
% 0.49/0.65  |- ~ssPv2 $_202 \/ ~ssPv3 $_200 \/ ~ssPv4 (skf2 $_200) \/
% 0.49/0.65     ~ssRr $_202 (skf2 $_200) \/ ssPv2 (skf2 $_200)
% 0.49/0.65  |- ~ssPv2 (skf3 $_201) \/ ~ssPv3 $_200 \/ ~ssPv4 $_201 \/
% 0.49/0.65     ~ssRr $_200 $_201 \/ ssPv2 $_201
% 0.49/0.65  |- ~ssPv2 $_202 \/ ~ssPv3 $_200 \/ ~ssPv4 (skf2 $_202) \/
% 0.49/0.65     ~ssRr $_200 (skf2 $_202) \/ ssPv2 (skf2 $_202)
% 0.49/0.65  |- ~ssPv2 $_204 \/ ~ssPv3 (skf3 (skf2 $_204)) \/ ~ssPv4 (skf2 $_204) \/
% 0.49/0.65     ssPv2 (skf2 $_204)
% 0.49/0.65  |- ~ssPv2 (skf3 (skf2 $_206)) \/ ~ssPv3 $_206 \/ ~ssPv4 (skf2 $_206) \/
% 0.49/0.65     ssPv2 (skf2 $_206)
% 0.49/0.65  |- ~ssPv3 $_214 \/ ~ssPv4 $_214 \/ ~ssPv4 $_215 \/ ~ssPv4 (skf3 $_214) \/
% 0.49/0.65     ~ssRr $_214 $_215
% 0.49/0.65  |- ~ssPv3 (skf2 $_213) \/ ~ssPv4 $_213 \/ ~ssPv4 $_215 \/
% 0.49/0.65     ~ssPv4 (skf2 $_213) \/ ~ssRr (skf2 $_213) $_215
% 0.49/0.65  |- ~ssPv3 (skf3 $_215) \/ ~ssPv4 $_213 \/ ~ssPv4 $_215 \/
% 0.49/0.65     ~ssPv4 (skf3 $_215) \/ ~ssRr $_213 (skf3 $_215)
% 0.49/0.65  |- ~ssPv3 $_214 \/ ~ssPv4 $_213 \/ ~ssPv4 $_214 \/ ~ssPv4 (skf2 $_214) \/
% 0.49/0.65     ~ssRr $_213 $_214
% 0.49/0.65  |- ~ssPv3 (skf3 $_217) \/ ~ssPv4 $_217 \/ ~ssPv4 (skf3 $_217) \/
% 0.49/0.65     ~ssPv4 (skf3 (skf3 $_217))
% 0.49/0.65  |- ~ssPv3 $_216 \/ ~ssPv4 $_216 \/ ~ssPv4 (skf2 $_216) \/
% 0.49/0.65     ~ssPv4 (skf3 $_216)
% 0.49/0.65  |- ~ssPv3 (skf2 $_220) \/ ~ssPv4 $_220 \/ ~ssPv4 (skf2 $_220) \/
% 0.49/0.65     ~ssPv4 (skf2 (skf2 $_220))
% 0.49/0.65  |- ~ssPv1 $_229 \/ ~ssPv2 $_228 \/ ~ssPv2 (skf3 $_228) \/
% 0.49/0.65     ~ssPv3 (skf3 $_228) \/ ~ssRr (skf3 $_228) $_229
% 0.49/0.65  |- ~ssPv1 $_229 \/ ~ssPv2 $_227 \/ ~ssPv2 (skf2 $_227) \/ ~ssPv3 $_227 \/
% 0.49/0.65     ~ssRr $_227 $_229
% 0.49/0.65  |- ~ssPv1 $_229 \/ ~ssPv2 $_228 \/ ~ssPv2 (skf3 $_229) \/
% 0.49/0.65     ~ssPv3 (skf3 $_229) \/ ~ssRr (skf3 $_229) $_228
% 0.49/0.65  |- ~ssPv1 (skf2 $_227) \/ ~ssPv2 $_227 \/ ~ssPv2 $_228 \/ ~ssPv3 $_227 \/
% 0.49/0.65     ~ssRr $_227 $_228
% 0.49/0.65  |- ~ssPv1 $_231 \/ ~ssPv2 (skf2 (skf3 $_231)) \/ ~ssPv2 (skf3 $_231) \/
% 0.49/0.65     ~ssPv3 (skf3 $_231)
% 0.49/0.65  |- ~ssPv1 (skf2 (skf3 $_234)) \/ ~ssPv2 $_234 \/ ~ssPv2 (skf3 $_234) \/
% 0.49/0.65     ~ssPv3 (skf3 $_234)
% 0.49/0.65  |- ~ssPv1 $_242 \/ ~ssPv1 (skf3 $_241) \/ ~ssPv3 $_241 \/
% 0.49/0.65     ~ssPv3 (skf3 $_241) \/ ~ssRr (skf3 $_241) $_242
% 0.49/0.65  |- ~ssPv1 $_240 \/ ~ssPv1 $_242 \/ ~ssPv3 $_240 \/ ~ssPv3 (skf2 $_240) \/
% 0.49/0.65     ~ssRr $_240 $_242
% 0.49/0.65  |- ~ssPv1 $_242 \/ ~ssPv1 (skf3 $_242) \/ ~ssPv3 $_241 \/
% 0.49/0.65     ~ssPv3 (skf3 $_242) \/ ~ssRr (skf3 $_242) $_241
% 0.49/0.65  |- ~ssPv1 $_240 \/ ~ssPv1 (skf2 $_240) \/ ~ssPv3 $_240 \/ ~ssPv3 $_241 \/
% 0.49/0.65     ~ssRr $_240 $_241
% 0.49/0.65  |- ~ssPv1 $_244 \/ ~ssPv1 (skf3 $_244) \/ ~ssPv3 (skf2 (skf3 $_244)) \/
% 0.49/0.65     ~ssPv3 (skf3 $_244)
% 0.49/0.65  |- ~ssPv1 (skf2 (skf3 $_247)) \/ ~ssPv1 (skf3 $_247) \/ ~ssPv3 $_247 \/
% 0.49/0.65     ~ssPv3 (skf3 $_247)
% 0.49/0.65  |- ~ssPv2 $_255 \/ ~ssRr $_254 (skf3 $_255) \/ ssPv2 $_254 \/
% 0.49/0.65     ssPv2 (skf3 $_255) \/ ssPv3 $_254
% 0.49/0.65  |- ~ssPv2 (skf2 $_253) \/ ~ssRr $_254 $_253 \/ ssPv2 $_253 \/
% 0.49/0.65     ssPv2 $_254 \/ ssPv3 $_254
% 0.49/0.65  |- ~ssPv2 $_255 \/ ~ssRr $_253 $_255 \/ ssPv2 $_253 \/
% 0.49/0.65     ssPv2 (skf3 $_253) \/ ssPv3 (skf3 $_253)
% 0.49/0.65  |- ~ssPv2 $_255 \/ ~ssRr (skf2 $_254) $_255 \/ ssPv2 $_254 \/
% 0.49/0.65     ssPv2 (skf2 $_254) \/ ssPv3 $_254
% 0.49/0.65  |- ~ssPv2 (skf2 $_256) \/ ssPv2 $_256 \/ ssPv2 (skf3 $_256) \/
% 0.49/0.65     ssPv3 (skf3 $_256)
% 0.49/0.65  |- ~ssPv2 (skf2 (skf2 $_257)) \/ ssPv2 $_257 \/ ssPv2 (skf2 $_257) \/
% 0.49/0.65     ssPv3 $_257
% 0.49/0.65  |- ~ssPv2 $_261 \/ ssPv2 (skf3 $_261) \/ ssPv2 (skf3 (skf3 $_261)) \/
% 0.49/0.65     ssPv3 (skf3 (skf3 $_261))
% 0.49/0.65  |- ~ssPv1 $_268 \/ ~ssPv4 $_269 \/ ~ssRr $_268 (skf3 $_269) \/
% 0.49/0.65     ssPv3 $_268 \/ ssPv3 (skf3 $_269)
% 0.49/0.65  |- ~ssPv1 $_268 \/ ~ssPv4 (skf2 $_267) \/ ~ssRr $_268 $_267 \/
% 0.49/0.65     ssPv3 $_267 \/ ssPv3 $_268
% 0.49/0.65  |- ~ssPv1 (skf3 $_267) \/ ~ssPv4 $_269 \/ ~ssRr $_267 $_269 \/
% 0.49/0.65     ssPv3 $_267 \/ ssPv3 (skf3 $_267)
% 0.49/0.65  |- ~ssPv1 $_268 \/ ~ssPv4 $_269 \/ ~ssRr (skf2 $_268) $_269 \/
% 0.49/0.65     ssPv3 $_268 \/ ssPv3 (skf2 $_268)
% 0.49/0.65  |- ~ssPv1 (skf3 $_270) \/ ~ssPv4 (skf2 $_270) \/ ssPv3 $_270 \/
% 0.49/0.65     ssPv3 (skf3 $_270)
% 0.49/0.65  |- ~ssPv1 $_271 \/ ~ssPv4 (skf2 (skf2 $_271)) \/ ssPv3 $_271 \/
% 0.49/0.65     ssPv3 (skf2 $_271)
% 0.49/0.65  |- ~ssPv1 (skf3 (skf3 $_275)) \/ ~ssPv4 $_275 \/ ssPv3 (skf3 $_275) \/
% 0.49/0.65     ssPv3 (skf3 (skf3 $_275))
% 0.49/0.65  |- ~ssPv2 $_282 \/ ~ssPv3 (skf3 $_283) \/ ~ssRr $_282 (skf3 $_283) \/
% 0.49/0.65     ssPv3 $_283 \/ ssPv4 $_282
% 0.49/0.65  |- ~ssPv2 $_282 \/ ~ssPv3 $_281 \/ ~ssRr $_282 $_281 \/
% 0.49/0.65     ssPv3 (skf2 $_281) \/ ssPv4 $_282
% 0.49/0.65  |- ~ssPv2 (skf3 $_281) \/ ~ssPv3 $_281 \/ ~ssRr $_281 $_283 \/
% 0.49/0.65     ssPv3 $_283 \/ ssPv4 (skf3 $_281)
% 0.49/0.65  |- ~ssPv2 $_282 \/ ~ssPv3 (skf2 $_282) \/ ~ssRr (skf2 $_282) $_283 \/
% 0.49/0.65     ssPv3 $_283 \/ ssPv4 $_282
% 0.49/0.65  |- ~ssPv2 (skf3 $_284) \/ ~ssPv3 $_284 \/ ssPv3 (skf2 $_284) \/
% 0.49/0.65     ssPv4 (skf3 $_284)
% 0.49/0.65  |- ~ssPv2 $_285 \/ ~ssPv3 (skf2 $_285) \/ ssPv3 (skf2 (skf2 $_285)) \/
% 0.49/0.65     ssPv4 $_285
% 0.49/0.65  |- ~ssPv2 (skf3 (skf3 $_289)) \/ ~ssPv3 (skf3 $_289) \/ ssPv3 $_289 \/
% 0.49/0.65     ssPv4 (skf3 (skf3 $_289))
% 0.49/0.65  |- ~ssPv2 $_297 \/ ~ssPv3 $_297 \/ ~ssRr $_296 $_297 \/ ssPv2 $_296 \/
% 0.49/0.65     ssPv2 (skf3 $_296)
% 0.49/0.65  |- ~ssPv2 $_297 \/ ~ssPv3 $_297 \/ ~ssRr (skf2 $_295) $_297 \/
% 0.49/0.65     ssPv2 $_295 \/ ssPv2 (skf2 $_295)
% 0.49/0.65  |- ~ssPv2 $_297 \/ ~ssPv3 $_297 \/ ~ssRr $_295 (skf3 $_297) \/
% 0.49/0.65     ssPv2 $_295 \/ ssPv2 (skf3 $_297)
% 0.49/0.65  |- ~ssPv2 (skf2 $_296) \/ ~ssPv3 (skf2 $_296) \/ ~ssRr $_295 $_296 \/
% 0.49/0.65     ssPv2 $_295 \/ ssPv2 $_296
% 0.49/0.65  |- ~ssPv2 $_299 \/ ~ssPv3 $_299 \/ ssPv2 (skf3 $_299) \/
% 0.49/0.65     ssPv2 (skf3 (skf3 $_299))
% 0.49/0.65  |- ~ssPv2 (skf2 $_298) \/ ~ssPv3 (skf2 $_298) \/ ssPv2 $_298 \/
% 0.49/0.65     ssPv2 (skf3 $_298)
% 0.49/0.65  |- ~ssPv2 (skf2 (skf2 $_302)) \/ ~ssPv3 (skf2 (skf2 $_302)) \/
% 0.49/0.65     ssPv2 $_302 \/ ssPv2 (skf2 $_302)
% 0.49/0.65  |- ~ssPv2 $_310 \/ ~ssPv4 $_311 \/ ~ssRr $_310 (skf3 $_311) \/
% 0.49/0.65     ssPv1 (skf3 $_311) \/ ssPv4 $_310
% 0.49/0.65  |- ~ssPv2 $_310 \/ ~ssPv4 (skf2 $_309) \/ ~ssRr $_310 $_309 \/
% 0.49/0.65     ssPv1 $_309 \/ ssPv4 $_310
% 0.49/0.65  |- ~ssPv2 (skf3 $_309) \/ ~ssPv4 $_311 \/ ~ssRr $_309 $_311 \/
% 0.49/0.65     ssPv1 $_309 \/ ssPv4 (skf3 $_309)
% 0.49/0.65  |- ~ssPv2 $_310 \/ ~ssPv4 $_311 \/ ~ssRr (skf2 $_310) $_311 \/
% 0.49/0.65     ssPv1 (skf2 $_310) \/ ssPv4 $_310
% 0.49/0.65  |- ~ssPv2 (skf3 $_312) \/ ~ssPv4 (skf2 $_312) \/ ssPv1 $_312 \/
% 0.49/0.65     ssPv4 (skf3 $_312)
% 0.49/0.65  |- ~ssPv2 $_313 \/ ~ssPv4 (skf2 (skf2 $_313)) \/ ssPv1 (skf2 $_313) \/
% 0.49/0.65     ssPv4 $_313
% 0.49/0.65  |- ~ssPv2 (skf3 (skf3 $_317)) \/ ~ssPv4 $_317 \/ ssPv1 (skf3 $_317) \/
% 0.49/0.65     ssPv4 (skf3 (skf3 $_317))
% 0.49/0.65  |- ~ssPv1 (skf3 $_324) \/ ~ssPv3 $_325 \/ ~ssPv4 $_324 \/
% 0.49/0.65     ~ssRr $_324 $_325 \/ ssPv2 $_325
% 0.49/0.65  |- ~ssPv1 $_323 \/ ~ssPv3 $_325 \/ ~ssPv4 (skf2 $_323) \/
% 0.49/0.65     ~ssRr (skf2 $_323) $_325 \/ ssPv2 $_325
% 0.49/0.65  |- ~ssPv1 $_323 \/ ~ssPv3 $_325 \/ ~ssPv4 (skf3 $_325) \/
% 0.49/0.65     ~ssRr $_323 (skf3 $_325) \/ ssPv2 $_325
% 0.49/0.65  |- ~ssPv1 $_323 \/ ~ssPv3 (skf2 $_324) \/ ~ssPv4 $_324 \/
% 0.49/0.65     ~ssRr $_323 $_324 \/ ssPv2 (skf2 $_324)
% 0.49/0.65  |- ~ssPv1 (skf3 (skf3 $_327)) \/ ~ssPv3 $_327 \/ ~ssPv4 (skf3 $_327) \/
% 0.49/0.65     ssPv2 $_327
% 0.49/0.65  |- ~ssPv1 (skf3 $_326) \/ ~ssPv3 (skf2 $_326) \/ ~ssPv4 $_326 \/
% 0.49/0.65     ssPv2 (skf2 $_326)
% 0.49/0.65  |- ~ssPv1 $_330 \/ ~ssPv3 (skf2 (skf2 $_330)) \/ ~ssPv4 (skf2 $_330) \/
% 0.49/0.65     ssPv2 (skf2 (skf2 $_330))
% 0.49/0.65  |- ~ssPv1 $_339 \/ ~ssPv2 $_338 \/ ~ssPv4 (skf3 $_338) \/
% 0.49/0.65     ~ssRr $_338 $_339 \/ ssPv4 $_339
% 0.49/0.65  |- ~ssPv1 $_339 \/ ~ssPv2 (skf2 $_337) \/ ~ssPv4 $_337 \/
% 0.49/0.65     ~ssRr (skf2 $_337) $_339 \/ ssPv4 $_339
% 0.49/0.65  |- ~ssPv1 $_339 \/ ~ssPv2 (skf3 $_339) \/ ~ssPv4 $_337 \/
% 0.49/0.65     ~ssRr $_337 (skf3 $_339) \/ ssPv4 $_339
% 0.49/0.65  |- ~ssPv1 (skf2 $_338) \/ ~ssPv2 $_338 \/ ~ssPv4 $_337 \/
% 0.49/0.65     ~ssRr $_337 $_338 \/ ssPv4 (skf2 $_338)
% 0.49/0.65  |- ~ssPv1 $_341 \/ ~ssPv2 (skf3 $_341) \/ ~ssPv4 (skf3 (skf3 $_341)) \/
% 0.49/0.65     ssPv4 $_341
% 0.49/0.65  |- ~ssPv1 (skf2 $_340) \/ ~ssPv2 $_340 \/ ~ssPv4 (skf3 $_340) \/
% 0.49/0.65     ssPv4 (skf2 $_340)
% 0.49/0.65  |- ~ssPv1 (skf2 (skf2 $_344)) \/ ~ssPv2 (skf2 $_344) \/ ~ssPv4 $_344 \/
% 0.49/0.65     ssPv4 (skf2 (skf2 $_344))
% 0.49/0.65  |- ~ssPv1 $_352 \/ ~ssPv2 $_352 \/ ~ssPv3 (skf3 $_353) \/
% 0.49/0.65     ~ssRr $_352 (skf3 $_353) \/ ssPv1 $_353
% 0.49/0.65  |- ~ssPv1 $_352 \/ ~ssPv2 $_352 \/ ~ssPv3 $_351 \/ ~ssRr $_352 $_351 \/
% 0.49/0.65     ssPv1 (skf2 $_351)
% 0.49/0.65  |- ~ssPv1 (skf3 $_351) \/ ~ssPv2 (skf3 $_351) \/ ~ssPv3 $_351 \/
% 0.49/0.65     ~ssRr $_351 $_353 \/ ssPv1 $_353
% 0.49/0.65  |- ~ssPv1 $_352 \/ ~ssPv2 $_352 \/ ~ssPv3 (skf2 $_352) \/
% 0.49/0.65     ~ssRr (skf2 $_352) $_353 \/ ssPv1 $_353
% 0.49/0.65  |- ~ssPv1 (skf3 $_354) \/ ~ssPv2 (skf3 $_354) \/ ~ssPv3 $_354 \/
% 0.49/0.65     ssPv1 (skf2 $_354)
% 0.49/0.65  |- ~ssPv1 $_355 \/ ~ssPv2 $_355 \/ ~ssPv3 (skf2 $_355) \/
% 0.49/0.65     ssPv1 (skf2 (skf2 $_355))
% 0.49/0.65  |- ~ssPv1 (skf3 (skf3 $_359)) \/ ~ssPv2 (skf3 (skf3 $_359)) \/
% 0.49/0.65     ~ssPv3 (skf3 $_359) \/ ssPv1 $_359
% 0.49/0.65  |- ~ssPv1 (skf3 $_367) \/ ~ssPv2 $_366 \/ ~ssPv4 $_367 \/
% 0.49/0.65     ~ssRr $_366 (skf3 $_367) \/ ssPv1 $_366
% 0.49/0.65  |- ~ssPv1 $_365 \/ ~ssPv2 $_366 \/ ~ssPv4 (skf2 $_365) \/
% 0.49/0.65     ~ssRr $_366 $_365 \/ ssPv1 $_366
% 0.49/0.65  |- ~ssPv1 $_365 \/ ~ssPv2 (skf3 $_365) \/ ~ssPv4 $_367 \/
% 0.49/0.65     ~ssRr $_365 $_367 \/ ssPv1 (skf3 $_365)
% 0.49/0.65  |- ~ssPv1 (skf2 $_366) \/ ~ssPv2 $_366 \/ ~ssPv4 $_367 \/
% 0.49/0.65     ~ssRr (skf2 $_366) $_367 \/ ssPv1 $_366
% 0.49/0.65  |- ~ssPv1 (skf2 $_368) \/ ~ssPv2 $_368 \/ ~ssPv4 (skf2 (skf2 $_368)) \/
% 0.49/0.65     ssPv1 $_368
% 0.49/0.65  |- ~ssPv1 $_371 \/ ~ssPv2 (skf3 $_371) \/ ~ssPv4 (skf2 $_371) \/
% 0.49/0.65     ssPv1 (skf3 $_371)
% 0.49/0.65  |- ~ssPv1 (skf3 $_375) \/ ~ssPv2 (skf3 (skf3 $_375)) \/ ~ssPv4 $_375 \/
% 0.49/0.65     ssPv1 (skf3 (skf3 $_375))
% 0.49/0.65  |- ~ssPv2 (skf3 $_380) \/ ~ssPv3 $_380 \/ ~ssPv3 $_381 \/ ~ssPv4 $_381 \/
% 0.49/0.65     ~ssRr $_380 $_381
% 0.49/0.65  |- ~ssPv2 $_379 \/ ~ssPv3 $_381 \/ ~ssPv3 (skf2 $_379) \/ ~ssPv4 $_381 \/
% 0.49/0.65     ~ssRr (skf2 $_379) $_381
% 0.49/0.65  |- ~ssPv2 $_379 \/ ~ssPv3 $_381 \/ ~ssPv3 (skf3 $_381) \/ ~ssPv4 $_381 \/
% 0.49/0.65     ~ssRr $_379 (skf3 $_381)
% 0.49/0.65  |- ~ssPv2 $_379 \/ ~ssPv3 $_380 \/ ~ssPv3 (skf2 $_380) \/
% 0.49/0.65     ~ssPv4 (skf2 $_380) \/ ~ssRr $_379 $_380
% 0.49/0.65  |- ~ssPv2 (skf3 (skf3 $_383)) \/ ~ssPv3 $_383 \/ ~ssPv3 (skf3 $_383) \/
% 0.49/0.65     ~ssPv4 $_383
% 0.49/0.65  |- ~ssPv2 (skf3 $_382) \/ ~ssPv3 $_382 \/ ~ssPv3 (skf2 $_382) \/
% 0.49/0.65     ~ssPv4 (skf2 $_382)
% 0.49/0.65  |- ~ssPv2 $_386 \/ ~ssPv3 (skf2 $_386) \/ ~ssPv3 (skf2 (skf2 $_386)) \/
% 0.49/0.65     ~ssPv4 (skf2 (skf2 $_386))
% 0.49/0.65  |- ~ssPv2 $_396 \/ ~ssRr $_394 $_396 \/ ~ssRr $_395 $_394 \/ ssPv2 $_394 \/
% 0.49/0.65     ssPv2 $_395 \/ ssPv3 (skf3 $_394)
% 0.49/0.65  |- ~ssPv2 $_396 \/ ~ssRr $_395 (skf2 $_393) \/ ~ssRr (skf2 $_393) $_396 \/
% 0.49/0.65     ssPv2 $_395 \/ ssPv2 (skf2 $_393) \/ ssPv3 $_393
% 0.49/0.65  |- ~ssPv2 $_396 \/ ~ssRr $_393 (skf3 $_396) \/ ~ssRr $_395 (skf3 $_396) \/
% 0.49/0.65     ssPv2 $_395 \/ ssPv2 (skf3 $_396) \/ ssPv3 $_393
% 0.49/0.65  |- ~ssPv2 (skf2 $_394) \/ ~ssRr $_393 $_394 \/ ~ssRr $_395 $_394 \/
% 0.49/0.65     ssPv2 $_394 \/ ssPv2 $_395 \/ ssPv3 $_393
% 0.49/0.65  |- ~ssPv2 $_396 \/ ~ssRr $_393 $_394 \/ ~ssRr $_394 $_396 \/ ssPv2 $_394 \/
% 0.49/0.65     ssPv2 (skf3 $_394) \/ ssPv3 $_393
% 0.49/0.66  |- ~ssPv2 $_396 \/ ~ssRr $_393 (skf2 $_395) \/ ~ssRr (skf2 $_395) $_396 \/
% 0.49/0.66     ssPv2 $_395 \/ ssPv2 (skf2 $_395) \/ ssPv3 $_393
% 0.49/0.66  |- ~ssPv2 $_399 \/ ~ssRr $_398 (skf3 $_399) \/ ssPv2 $_398 \/
% 0.49/0.66     ssPv2 (skf3 $_399) \/ ssPv3 (skf3 (skf3 $_399))
% 0.49/0.66  |- ~ssPv2 (skf2 $_397) \/ ~ssRr $_398 $_397 \/ ssPv2 $_397 \/
% 0.49/0.66     ssPv2 $_398 \/ ssPv3 (skf3 $_397)
% 0.49/0.66  |- ~ssPv2 $_399 \/ ~ssRr (skf2 $_398) $_399 \/ ssPv2 $_398 \/
% 0.49/0.66     ssPv2 (skf2 $_398) \/ ssPv3 (skf3 (skf2 $_398))
% 0.49/0.66  |- ~ssPv2 (skf2 (skf2 $_401)) \/ ssPv2 $_401 \/ ssPv2 (skf2 $_401) \/
% 0.49/0.66     ssPv3 (skf3 (skf2 $_401))
% 0.49/0.66  |- ~ssPv2 (skf2 (skf2 $_407)) \/ ~ssRr $_409 (skf2 $_407) \/ ssPv2 $_409 \/
% 0.49/0.66     ssPv2 (skf2 $_407) \/ ssPv3 $_407
% 0.49/0.66  |- ~ssPv2 (skf2 $_408) \/ ~ssRr $_407 $_408 \/ ssPv2 $_408 \/
% 0.49/0.66     ssPv2 (skf3 $_408) \/ ssPv3 $_407
% 0.49/0.66  |- ~ssPv2 (skf2 (skf2 $_409)) \/ ~ssRr $_407 (skf2 $_409) \/ ssPv2 $_409 \/
% 0.49/0.66     ssPv2 (skf2 $_409) \/ ssPv3 $_407
% 0.49/0.66  |- ~ssPv2 (skf2 (skf2 $_410)) \/ ssPv2 (skf2 $_410) \/
% 0.49/0.66     ssPv2 (skf3 (skf2 $_410)) \/ ssPv3 $_410
% 0.49/0.66  |- ~ssPv2 $_419 \/ ~ssRr (skf2 $_417) $_419 \/ ssPv2 (skf2 $_417) \/
% 0.49/0.66     ssPv2 (skf3 (skf2 $_417)) \/ ssPv3 $_417
% 0.49/0.66  |- ~ssPv2 $_419 \/ ~ssRr $_417 (skf3 $_419) \/ ssPv2 (skf3 $_419) \/
% 0.49/0.66     ssPv2 (skf3 (skf3 $_419)) \/ ssPv3 $_417
% 0.49/0.66  |- ~ssPv1 (skf3 $_434) \/ ~ssPv4 $_436 \/ ~ssRr $_434 $_436 \/
% 0.49/0.66     ~ssRr $_435 $_434 \/ ssPv3 $_434 \/ ssPv3 $_435
% 0.49/0.66  |- ~ssPv1 $_433 \/ ~ssPv4 $_436 \/ ~ssRr $_435 (skf2 $_433) \/
% 0.49/0.66     ~ssRr (skf2 $_433) $_436 \/ ssPv3 $_435 \/ ssPv3 (skf2 $_433)
% 0.49/0.66  |- ~ssPv1 $_433 \/ ~ssPv4 $_436 \/ ~ssRr $_433 (skf3 $_436) \/
% 0.49/0.66     ~ssRr $_435 (skf3 $_436) \/ ssPv3 $_435 \/ ssPv3 (skf3 $_436)
% 0.49/0.66  |- ~ssPv1 $_433 \/ ~ssPv4 (skf2 $_434) \/ ~ssRr $_433 $_434 \/
% 0.49/0.66     ~ssRr $_435 $_434 \/ ssPv3 $_434 \/ ssPv3 $_435
% 0.49/0.66  |- ~ssPv1 $_433 \/ ~ssPv4 $_436 \/ ~ssRr $_433 $_434 \/
% 0.49/0.66     ~ssRr $_434 $_436 \/ ssPv3 $_434 \/ ssPv3 (skf3 $_434)
% 0.49/0.66  |- ~ssPv1 $_433 \/ ~ssPv4 $_436 \/ ~ssRr $_433 (skf2 $_435) \/
% 0.49/0.66     ~ssRr (skf2 $_435) $_436 \/ ssPv3 $_435 \/ ssPv3 (skf2 $_435)
% 0.49/0.66  |- ~ssPv1 $_433 \/ ~ssPv4 (skf2 $_433) \/
% 0.49/0.66     ~ssRr (skf2 $_433) (skf2 $_433) \/ ssPv3 (skf2 $_433)
% 0.49/0.66  |- ~ssPv1 (skf3 (skf3 $_440)) \/ ~ssPv4 $_440 \/
% 0.49/0.66     ~ssRr $_439 (skf3 $_440) \/ ssPv3 $_439 \/ ssPv3 (skf3 $_440)
% 0.49/0.66  |- ~ssPv1 (skf3 $_438) \/ ~ssPv4 (skf2 $_438) \/ ~ssRr $_439 $_438 \/
% 0.49/0.66     ssPv3 $_438 \/ ssPv3 $_439
% 0.49/0.66  |- ~ssPv1 (skf3 (skf2 $_439)) \/ ~ssPv4 $_440 \/
% 0.49/0.66     ~ssRr (skf2 $_439) $_440 \/ ssPv3 $_439 \/ ssPv3 (skf2 $_439)
% 0.49/0.66  |- ~ssPv1 (skf3 (skf2 $_442)) \/ ~ssPv4 (skf2 (skf2 $_442)) \/
% 0.49/0.66     ssPv3 $_442 \/ ssPv3 (skf2 $_442)
% 0.49/0.66  |- ~ssPv1 $_448 \/ ~ssPv4 (skf2 (skf2 $_448)) \/
% 0.49/0.66     ~ssRr $_450 (skf2 $_448) \/ ssPv3 $_450 \/ ssPv3 (skf2 $_448)
% 0.49/0.66  |- ~ssPv1 $_448 \/ ~ssPv4 (skf2 $_449) \/ ~ssRr $_448 $_449 \/
% 0.49/0.66     ssPv3 $_449 \/ ssPv3 (skf3 $_449)
% 0.49/0.66  |- ~ssPv1 $_448 \/ ~ssPv4 (skf2 (skf2 $_450)) \/
% 0.49/0.66     ~ssRr $_448 (skf2 $_450) \/ ssPv3 $_450 \/ ssPv3 (skf2 $_450)
% 0.49/0.66  |- ~ssPv1 $_451 \/ ~ssPv4 (skf2 (skf2 $_451)) \/ ssPv3 (skf2 $_451) \/
% 0.49/0.66     ssPv3 (skf3 (skf2 $_451))
% 0.49/0.66  |- ~ssPv1 $_458 \/ ~ssPv4 $_460 \/ ~ssRr (skf2 $_458) $_460 \/
% 0.49/0.66     ssPv3 (skf2 $_458) \/ ssPv3 (skf3 (skf2 $_458))
% 0.49/0.66  |- ~ssPv1 $_458 \/ ~ssPv4 $_460 \/ ~ssRr $_458 (skf3 $_460) \/
% 0.49/0.66     ssPv3 (skf3 $_460) \/ ssPv3 (skf3 (skf3 $_460))
% 0.49/0.66  |- ~ssPv2 (skf3 $_466) \/ ~ssPv3 $_466 \/ ~ssRr $_466 $_468 \/
% 0.49/0.66     ~ssRr $_467 $_466 \/ ssPv3 $_468 \/ ssPv4 $_467
% 0.49/0.66  |- ~ssPv2 $_465 \/ ~ssPv3 (skf2 $_465) \/ ~ssRr $_467 (skf2 $_465) \/
% 0.49/0.66     ~ssRr (skf2 $_465) $_468 \/ ssPv3 $_468 \/ ssPv4 $_467
% 0.49/0.66  |- ~ssPv2 $_465 \/ ~ssPv3 (skf3 $_468) \/ ~ssRr $_465 (skf3 $_468) \/
% 0.49/0.66     ~ssRr $_467 (skf3 $_468) \/ ssPv3 $_468 \/ ssPv4 $_467
% 0.49/0.66  |- ~ssPv2 $_465 \/ ~ssPv3 $_466 \/ ~ssRr $_465 $_466 \/
% 0.49/0.66     ~ssRr $_467 $_466 \/ ssPv3 (skf2 $_466) \/ ssPv4 $_467
% 0.49/0.66  |- ~ssPv2 $_465 \/ ~ssPv3 $_466 \/ ~ssRr $_465 $_466 \/
% 0.49/0.66     ~ssRr $_466 $_468 \/ ssPv3 $_468 \/ ssPv4 (skf3 $_466)
% 0.49/0.66  |- ~ssPv2 $_465 \/ ~ssPv3 (skf2 $_467) \/ ~ssRr $_465 (skf2 $_467) \/
% 0.49/0.66     ~ssRr (skf2 $_467) $_468 \/ ssPv3 $_468 \/ ssPv4 $_467
% 0.49/0.66  |- ~ssPv2 (skf3 (skf3 $_471)) \/ ~ssPv3 (skf3 $_471) \/
% 0.49/0.66     ~ssRr $_470 (skf3 $_471) \/ ssPv3 $_471 \/ ssPv4 $_470
% 0.49/0.66  |- ~ssPv2 (skf3 $_469) \/ ~ssPv3 $_469 \/ ~ssRr $_470 $_469 \/
% 0.49/0.66     ssPv3 (skf2 $_469) \/ ssPv4 $_470
% 0.49/0.66  |- ~ssPv2 (skf3 (skf2 $_470)) \/ ~ssPv3 (skf2 $_470) \/
% 0.49/0.66     ~ssRr (skf2 $_470) $_471 \/ ssPv3 $_471 \/ ssPv4 $_470
% 0.49/0.66  |- ~ssPv2 (skf3 (skf2 $_473)) \/ ~ssPv3 (skf2 $_473) \/
% 0.49/0.66     ssPv3 (skf2 (skf2 $_473)) \/ ssPv4 $_473
% 0.49/0.66  |- ~ssPv2 $_479 \/ ~ssPv3 (skf2 $_479) \/ ~ssRr $_481 (skf2 $_479) \/
% 0.49/0.66     ssPv3 (skf2 (skf2 $_479)) \/ ssPv4 $_481
% 0.49/0.66  |- ~ssPv2 $_479 \/ ~ssPv3 $_480 \/ ~ssRr $_479 $_480 \/
% 0.49/0.66     ssPv3 (skf2 $_480) \/ ssPv4 (skf3 $_480)
% 0.49/0.66  |- ~ssPv2 $_479 \/ ~ssPv3 (skf2 $_481) \/ ~ssRr $_479 (skf2 $_481) \/
% 0.49/0.66     ssPv3 (skf2 (skf2 $_481)) \/ ssPv4 $_481
% 0.49/0.66  |- ~ssPv2 $_482 \/ ~ssPv3 (skf2 $_482) \/ ssPv3 (skf2 (skf2 $_482)) \/
% 0.49/0.66     ssPv4 (skf3 (skf2 $_482))
% 0.49/0.66  |- ~ssPv2 $_489 \/ ~ssPv3 (skf2 $_489) \/ ~ssRr (skf2 $_489) $_491 \/
% 0.49/0.66     ssPv3 $_491 \/ ssPv4 (skf3 (skf2 $_489))
% 0.49/0.66  |- ~ssPv2 $_489 \/ ~ssPv3 (skf3 $_491) \/ ~ssRr $_489 (skf3 $_491) \/
% 0.49/0.66     ssPv3 $_491 \/ ssPv4 (skf3 (skf3 $_491))
% 0.49/0.66  |- ~ssPv2 $_508 \/ ~ssPv3 $_507 \/ ~ssRr $_506 $_507 \/
% 0.49/0.66     ~ssRr $_506 $_508 \/ ssPv2 $_506 \/ ssPv2 (skf3 $_506)
% 0.49/0.66  |- ~ssPv2 $_508 \/ ~ssPv3 $_507 \/ ~ssRr (skf2 $_505) $_507 \/
% 0.49/0.66     ~ssRr (skf2 $_505) $_508 \/ ssPv2 $_505 \/ ssPv2 (skf2 $_505)
% 0.49/0.66  |- ~ssPv2 $_508 \/ ~ssPv3 $_507 \/ ~ssRr $_505 (skf3 $_507) \/
% 0.49/0.66     ~ssRr (skf3 $_507) $_508 \/ ssPv2 $_505 \/ ssPv2 (skf3 $_507)
% 0.49/0.66  |- ~ssPv2 $_508 \/ ~ssPv3 (skf2 $_506) \/ ~ssRr $_505 $_506 \/
% 0.49/0.66     ~ssRr $_506 $_508 \/ ssPv2 $_505 \/ ssPv2 $_506
% 0.49/0.66  |- ~ssPv2 $_508 \/ ~ssPv3 $_507 \/ ~ssRr $_505 (skf3 $_508) \/
% 0.49/0.66     ~ssRr (skf3 $_508) $_507 \/ ssPv2 $_505 \/ ssPv2 (skf3 $_508)
% 0.49/0.66  |- ~ssPv2 (skf2 $_506) \/ ~ssPv3 $_507 \/ ~ssRr $_505 $_506 \/
% 0.49/0.66     ~ssRr $_506 $_507 \/ ssPv2 $_505 \/ ssPv2 $_506
% 0.49/0.66  |- ~ssPv2 $_508 \/ ~ssPv3 (skf3 $_508) \/
% 0.49/0.66     ~ssRr (skf3 $_508) (skf3 $_508) \/ ssPv2 (skf3 $_508)
% 0.49/0.66  |- ~ssPv2 $_512 \/ ~ssPv3 $_511 \/ ~ssRr (skf3 $_511) $_512 \/
% 0.49/0.66     ssPv2 (skf3 $_511) \/ ssPv2 (skf3 (skf3 $_511))
% 0.49/0.66  |- ~ssPv2 $_512 \/ ~ssPv3 (skf2 $_510) \/ ~ssRr $_510 $_512 \/
% 0.49/0.66     ssPv2 $_510 \/ ssPv2 (skf3 $_510)
% 0.49/0.66  |- ~ssPv2 $_512 \/ ~ssPv3 $_511 \/ ~ssRr (skf3 $_512) $_511 \/
% 0.49/0.66     ssPv2 (skf3 $_512) \/ ssPv2 (skf3 (skf3 $_512))
% 0.49/0.66  |- ~ssPv2 (skf2 $_510) \/ ~ssPv3 $_511 \/ ~ssRr $_510 $_511 \/
% 0.49/0.66     ssPv2 $_510 \/ ssPv2 (skf3 $_510)
% 0.49/0.66  |- ~ssPv2 $_514 \/ ~ssPv3 (skf2 (skf3 $_514)) \/ ssPv2 (skf3 $_514) \/
% 0.49/0.66     ssPv2 (skf3 (skf3 $_514))
% 0.49/0.66  |- ~ssPv2 (skf2 (skf3 $_517)) \/ ~ssPv3 $_517 \/ ssPv2 (skf3 $_517) \/
% 0.49/0.66     ssPv2 (skf3 (skf3 $_517))
% 0.49/0.66  |- ~ssPv2 $_525 \/ ~ssPv3 (skf2 (skf2 $_523)) \/
% 0.49/0.66     ~ssRr (skf2 $_523) $_525 \/ ssPv2 $_523 \/ ssPv2 (skf2 $_523)
% 0.49/0.66  |- ~ssPv2 $_525 \/ ~ssPv3 (skf2 (skf3 $_525)) \/
% 0.49/0.66     ~ssRr $_523 (skf3 $_525) \/ ssPv2 $_523 \/ ssPv2 (skf3 $_525)
% 0.49/0.66  |- ~ssPv2 (skf2 (skf2 $_530)) \/ ~ssPv3 $_532 \/
% 0.49/0.66     ~ssRr (skf2 $_530) $_532 \/ ssPv2 $_530 \/ ssPv2 (skf2 $_530)
% 0.49/0.66  |- ~ssPv2 (skf2 (skf3 $_532)) \/ ~ssPv3 $_532 \/
% 0.49/0.66     ~ssRr $_530 (skf3 $_532) \/ ssPv2 $_530 \/ ssPv2 (skf3 $_532)
% 0.49/0.66  |- ~ssPv2 (skf3 $_538) \/ ~ssPv4 $_540 \/ ~ssRr $_538 $_540 \/
% 0.49/0.66     ~ssRr $_539 $_538 \/ ssPv1 $_538 \/ ssPv4 $_539
% 0.49/0.66  |- ~ssPv2 $_537 \/ ~ssPv4 $_540 \/ ~ssRr $_539 (skf2 $_537) \/
% 0.49/0.66     ~ssRr (skf2 $_537) $_540 \/ ssPv1 (skf2 $_537) \/ ssPv4 $_539
% 0.49/0.66  |- ~ssPv2 $_537 \/ ~ssPv4 $_540 \/ ~ssRr $_537 (skf3 $_540) \/
% 0.49/0.66     ~ssRr $_539 (skf3 $_540) \/ ssPv1 (skf3 $_540) \/ ssPv4 $_539
% 0.49/0.66  |- ~ssPv2 $_537 \/ ~ssPv4 (skf2 $_538) \/ ~ssRr $_537 $_538 \/
% 0.49/0.66     ~ssRr $_539 $_538 \/ ssPv1 $_538 \/ ssPv4 $_539
% 0.49/0.66  |- ~ssPv2 $_537 \/ ~ssPv4 $_540 \/ ~ssRr $_537 $_538 \/
% 0.49/0.66     ~ssRr $_538 $_540 \/ ssPv1 $_538 \/ ssPv4 (skf3 $_538)
% 0.49/0.66  |- ~ssPv2 $_537 \/ ~ssPv4 $_540 \/ ~ssRr $_537 (skf2 $_539) \/
% 0.49/0.66     ~ssRr (skf2 $_539) $_540 \/ ssPv1 (skf2 $_539) \/ ssPv4 $_539
% 0.49/0.66  |- ~ssPv2 (skf2 $_539) \/ ~ssPv4 (skf2 $_539) \/
% 0.49/0.66     ~ssRr (skf2 $_539) (skf2 $_539) \/ ssPv1 (skf2 $_539) \/ ssPv4 $_539
% 0.49/0.66  |- ~ssPv2 (skf3 (skf3 $_544)) \/ ~ssPv4 $_544 \/
% 0.49/0.66     ~ssRr $_543 (skf3 $_544) \/ ssPv1 (skf3 $_544) \/ ssPv4 $_543
% 0.49/0.66  |- ~ssPv2 (skf3 $_542) \/ ~ssPv4 (skf2 $_542) \/ ~ssRr $_543 $_542 \/
% 0.49/0.66     ssPv1 $_542 \/ ssPv4 $_543
% 0.49/0.66  |- ~ssPv2 (skf3 (skf2 $_543)) \/ ~ssPv4 $_544 \/
% 0.49/0.66     ~ssRr (skf2 $_543) $_544 \/ ssPv1 (skf2 $_543) \/ ssPv4 $_543
% 0.49/0.66  |- ~ssPv2 (skf3 (skf2 $_546)) \/ ~ssPv4 (skf2 (skf2 $_546)) \/
% 0.49/0.66     ssPv1 (skf2 $_546) \/ ssPv4 $_546
% 0.49/0.66  |- ~ssPv2 $_552 \/ ~ssPv4 (skf2 (skf2 $_552)) \/
% 0.49/0.66     ~ssRr $_554 (skf2 $_552) \/ ssPv1 (skf2 $_552) \/ ssPv4 $_554
% 0.49/0.66  |- ~ssPv2 $_552 \/ ~ssPv4 (skf2 $_553) \/ ~ssRr $_552 $_553 \/
% 0.49/0.66     ssPv1 $_553 \/ ssPv4 (skf3 $_553)
% 0.49/0.66  |- ~ssPv2 $_552 \/ ~ssPv4 (skf2 (skf2 $_554)) \/
% 0.49/0.66     ~ssRr $_552 (skf2 $_554) \/ ssPv1 (skf2 $_554) \/ ssPv4 $_554
% 0.49/0.66  |- ~ssPv2 $_555 \/ ~ssPv4 (skf2 (skf2 $_555)) \/ ssPv1 (skf2 $_555) \/
% 0.49/0.66     ssPv4 (skf3 (skf2 $_555))
% 0.49/0.66  |- ~ssPv2 $_562 \/ ~ssPv4 $_564 \/ ~ssRr (skf2 $_562) $_564 \/
% 0.49/0.66     ssPv1 (skf2 $_562) \/ ssPv4 (skf3 (skf2 $_562))
% 0.49/0.66  |- ~ssPv2 $_562 \/ ~ssPv4 $_564 \/ ~ssRr $_562 (skf3 $_564) \/
% 0.49/0.66     ssPv1 (skf3 $_564) \/ ssPv4 (skf3 (skf3 $_564))
% 0.49/0.66  |- ~ssPv1 (skf3 $_570) \/ ~ssPv3 $_571 \/ ~ssPv4 $_570 \/
% 0.49/0.66     ~ssRr $_570 $_571 \/ ~ssRr $_570 $_572 \/ ssPv2 $_572
% 0.49/0.66  |- ~ssPv1 $_569 \/ ~ssPv3 $_571 \/ ~ssPv4 (skf2 $_569) \/
% 0.49/0.66     ~ssRr (skf2 $_569) $_571 \/ ~ssRr (skf2 $_569) $_572 \/ ssPv2 $_572
% 0.49/0.66  |- ~ssPv1 $_569 \/ ~ssPv3 $_571 \/ ~ssPv4 (skf3 $_571) \/
% 0.49/0.66     ~ssRr $_569 (skf3 $_571) \/ ~ssRr (skf3 $_571) $_572 \/ ssPv2 $_572
% 0.49/0.66  |- ~ssPv1 $_569 \/ ~ssPv3 (skf2 $_570) \/ ~ssPv4 $_570 \/
% 0.49/0.66     ~ssRr $_569 $_570 \/ ~ssRr $_570 $_572 \/ ssPv2 $_572
% 0.49/0.66  |- ~ssPv1 $_569 \/ ~ssPv3 $_571 \/ ~ssPv4 (skf3 $_572) \/
% 0.49/0.66     ~ssRr $_569 (skf3 $_572) \/ ~ssRr (skf3 $_572) $_571 \/ ssPv2 $_572
% 0.49/0.66  |- ~ssPv1 $_569 \/ ~ssPv3 $_571 \/ ~ssPv4 $_570 \/ ~ssRr $_569 $_570 \/
% 0.49/0.66     ~ssRr $_570 $_571 \/ ssPv2 (skf2 $_570)
% 0.49/0.66  |- ~ssPv1 (skf3 $_571) \/ ~ssPv3 $_571 \/ ~ssPv4 (skf3 $_571) \/
% 0.49/0.66     ~ssRr (skf3 $_571) (skf3 $_571) \/ ssPv2 (skf3 $_571)
% 0.49/0.66  |- ~ssPv1 (skf3 (skf3 $_575)) \/ ~ssPv3 $_575 \/ ~ssPv4 (skf3 $_575) \/
% 0.49/0.66     ~ssRr (skf3 $_575) $_576 \/ ssPv2 $_576
% 0.49/0.66  |- ~ssPv1 (skf3 $_574) \/ ~ssPv3 (skf2 $_574) \/ ~ssPv4 $_574 \/
% 0.49/0.66     ~ssRr $_574 $_576 \/ ssPv2 $_576
% 0.49/0.66  |- ~ssPv1 (skf3 (skf3 $_576)) \/ ~ssPv3 $_575 \/ ~ssPv4 (skf3 $_576) \/
% 0.49/0.66     ~ssRr (skf3 $_576) $_575 \/ ssPv2 $_576
% 0.49/0.66  |- ~ssPv1 (skf3 $_574) \/ ~ssPv3 $_575 \/ ~ssPv4 $_574 \/
% 0.49/0.66     ~ssRr $_574 $_575 \/ ssPv2 (skf2 $_574)
% 0.49/0.66  |- ~ssPv1 (skf3 (skf3 $_578)) \/ ~ssPv3 (skf2 (skf3 $_578)) \/
% 0.49/0.66     ~ssPv4 (skf3 $_578) \/ ssPv2 $_578
% 0.49/0.66  |- ~ssPv1 (skf3 (skf3 $_581)) \/ ~ssPv3 $_581 \/ ~ssPv4 (skf3 $_581) \/
% 0.49/0.66     ssPv2 (skf2 (skf3 $_581))
% 0.49/0.66  |- ~ssPv1 $_587 \/ ~ssPv3 (skf2 (skf2 $_587)) \/ ~ssPv4 (skf2 $_587) \/
% 0.49/0.66     ~ssRr (skf2 $_587) $_589 \/ ssPv2 $_589
% 0.49/0.66  |- ~ssPv1 $_587 \/ ~ssPv3 (skf2 (skf3 $_589)) \/ ~ssPv4 (skf3 $_589) \/
% 0.49/0.66     ~ssRr $_587 (skf3 $_589) \/ ssPv2 $_589
% 0.49/0.66  |- ~ssPv1 $_594 \/ ~ssPv3 $_596 \/ ~ssPv4 (skf2 $_594) \/
% 0.49/0.66     ~ssRr (skf2 $_594) $_596 \/ ssPv2 (skf2 (skf2 $_594))
% 0.49/0.66  |- ~ssPv1 $_594 \/ ~ssPv3 $_596 \/ ~ssPv4 (skf3 $_596) \/
% 0.49/0.66     ~ssRr $_594 (skf3 $_596) \/ ssPv2 (skf2 (skf3 $_596))
% 0.49/0.66  |- ~ssPv1 $_603 \/ ~ssPv2 $_602 \/ ~ssPv4 (skf3 $_602) \/
% 0.49/0.66     ~ssRr $_602 $_603 \/ ~ssRr $_602 $_604 \/ ssPv4 $_604
% 0.49/0.66  |- ~ssPv1 $_603 \/ ~ssPv2 (skf2 $_601) \/ ~ssPv4 $_601 \/
% 0.49/0.66     ~ssRr (skf2 $_601) $_603 \/ ~ssRr (skf2 $_601) $_604 \/ ssPv4 $_604
% 0.49/0.66  |- ~ssPv1 $_603 \/ ~ssPv2 (skf3 $_603) \/ ~ssPv4 $_601 \/
% 0.49/0.66     ~ssRr $_601 (skf3 $_603) \/ ~ssRr (skf3 $_603) $_604 \/ ssPv4 $_604
% 0.49/0.66  |- ~ssPv1 (skf2 $_602) \/ ~ssPv2 $_602 \/ ~ssPv4 $_601 \/
% 0.49/0.66     ~ssRr $_601 $_602 \/ ~ssRr $_602 $_604 \/ ssPv4 $_604
% 0.49/0.66  |- ~ssPv1 $_603 \/ ~ssPv2 (skf3 $_604) \/ ~ssPv4 $_601 \/
% 0.49/0.66     ~ssRr $_601 (skf3 $_604) \/ ~ssRr (skf3 $_604) $_603 \/ ssPv4 $_604
% 0.49/0.66  |- ~ssPv1 $_603 \/ ~ssPv2 $_602 \/ ~ssPv4 $_601 \/ ~ssRr $_601 $_602 \/
% 0.49/0.66     ~ssRr $_602 $_603 \/ ssPv4 (skf2 $_602)
% 0.49/0.66  |- ~ssPv1 $_606 \/ ~ssPv2 (skf3 $_606) \/ ~ssPv4 (skf3 (skf3 $_606)) \/
% 0.49/0.66     ~ssRr (skf3 $_606) $_607 \/ ssPv4 $_607
% 0.49/0.66  |- ~ssPv1 (skf2 $_605) \/ ~ssPv2 $_605 \/ ~ssPv4 (skf3 $_605) \/
% 0.49/0.66     ~ssRr $_605 $_607 \/ ssPv4 $_607
% 0.49/0.66  |- ~ssPv1 $_606 \/ ~ssPv2 (skf3 $_607) \/ ~ssPv4 (skf3 (skf3 $_607)) \/
% 0.49/0.66     ~ssRr (skf3 $_607) $_606 \/ ssPv4 $_607
% 0.49/0.66  |- ~ssPv1 $_606 \/ ~ssPv2 $_605 \/ ~ssPv4 (skf3 $_605) \/
% 0.49/0.66     ~ssRr $_605 $_606 \/ ssPv4 (skf2 $_605)
% 0.49/0.66  |- ~ssPv1 (skf2 (skf3 $_609)) \/ ~ssPv2 (skf3 $_609) \/
% 0.49/0.66     ~ssPv4 (skf3 (skf3 $_609)) \/ ssPv4 $_609
% 0.49/0.66  |- ~ssPv1 $_612 \/ ~ssPv2 (skf3 $_612) \/ ~ssPv4 (skf3 (skf3 $_612)) \/
% 0.49/0.66     ssPv4 (skf2 (skf3 $_612))
% 0.49/0.66  |- ~ssPv1 (skf2 (skf2 $_618)) \/ ~ssPv2 (skf2 $_618) \/ ~ssPv4 $_618 \/
% 0.49/0.66     ~ssRr (skf2 $_618) $_620 \/ ssPv4 $_620
% 0.49/0.66  |- ~ssPv1 (skf2 (skf3 $_620)) \/ ~ssPv2 (skf3 $_620) \/ ~ssPv4 $_618 \/
% 0.49/0.66     ~ssRr $_618 (skf3 $_620) \/ ssPv4 $_620
% 0.49/0.66  |- ~ssPv1 $_627 \/ ~ssPv2 (skf2 $_625) \/ ~ssPv4 $_625 \/
% 0.49/0.66     ~ssRr (skf2 $_625) $_627 \/ ssPv4 (skf2 (skf2 $_625))
% 0.49/0.66  |- ~ssPv1 $_627 \/ ~ssPv2 (skf3 $_627) \/ ~ssPv4 $_625 \/
% 0.49/0.66     ~ssRr $_625 (skf3 $_627) \/ ssPv4 (skf2 (skf3 $_627))
% 0.49/0.66  |- ~ssPv1 $_643 \/ ~ssPv2 $_642 \/ ~ssPv2 (skf3 $_642) \/
% 0.49/0.66     ~ssRr $_642 $_643 \/ ~ssRr $_642 $_644 \/ ssPv1 $_644
% 0.49/0.66  |- ~ssPv1 $_643 \/ ~ssPv2 $_641 \/ ~ssPv2 (skf2 $_641) \/
% 0.49/0.66     ~ssRr (skf2 $_641) $_643 \/ ~ssRr (skf2 $_641) $_644 \/ ssPv1 $_644
% 0.49/0.66  |- ~ssPv1 $_643 \/ ~ssPv2 $_641 \/ ~ssPv2 (skf3 $_643) \/
% 0.49/0.66     ~ssRr $_641 (skf3 $_643) \/ ~ssRr (skf3 $_643) $_644 \/ ssPv1 $_644
% 0.49/0.66  |- ~ssPv1 (skf2 $_642) \/ ~ssPv2 $_641 \/ ~ssPv2 $_642 \/
% 0.49/0.66     ~ssRr $_641 $_642 \/ ~ssRr $_642 $_644 \/ ssPv1 $_644
% 0.49/0.66  |- ~ssPv1 $_643 \/ ~ssPv2 $_641 \/ ~ssPv2 (skf3 $_644) \/
% 0.49/0.66     ~ssRr $_641 (skf3 $_644) \/ ~ssRr (skf3 $_644) $_643 \/ ssPv1 $_644
% 0.49/0.66  |- ~ssPv1 $_643 \/ ~ssPv2 $_641 \/ ~ssPv2 $_642 \/ ~ssRr $_641 $_642 \/
% 0.49/0.66     ~ssRr $_642 $_643 \/ ssPv1 (skf2 $_642)
% 0.49/0.66  |- ~ssPv1 $_643 \/ ~ssPv2 (skf3 $_643) \/
% 0.49/0.66     ~ssRr (skf3 $_643) (skf3 $_643) \/ ssPv1 (skf3 $_643)
% 0.49/0.66  |- ~ssPv1 (skf3 $_644) \/ ~ssPv2 (skf3 $_644) \/
% 0.49/0.66     ~ssRr (skf3 $_644) (skf3 $_644) \/ ssPv1 $_644
% 0.49/0.66  |- ~ssPv1 $_648 \/ ~ssPv2 (skf3 $_648) \/ ~ssPv2 (skf3 (skf3 $_648)) \/
% 0.49/0.66     ~ssRr (skf3 $_648) $_649 \/ ssPv1 $_649
% 0.49/0.66  |- ~ssPv1 (skf2 $_647) \/ ~ssPv2 $_647 \/ ~ssPv2 (skf3 $_647) \/
% 0.49/0.66     ~ssRr $_647 $_649 \/ ssPv1 $_649
% 0.49/0.66  |- ~ssPv1 $_648 \/ ~ssPv2 (skf3 $_649) \/ ~ssPv2 (skf3 (skf3 $_649)) \/
% 0.49/0.66     ~ssRr (skf3 $_649) $_648 \/ ssPv1 $_649
% 0.49/0.66  |- ~ssPv1 $_648 \/ ~ssPv2 $_647 \/ ~ssPv2 (skf3 $_647) \/
% 0.49/0.66     ~ssRr $_647 $_648 \/ ssPv1 (skf2 $_647)
% 0.49/0.66  |- ~ssPv1 (skf2 (skf3 $_651)) \/ ~ssPv2 (skf3 $_651) \/
% 0.49/0.66     ~ssPv2 (skf3 (skf3 $_651)) \/ ssPv1 $_651
% 0.49/0.66  |- ~ssPv1 $_654 \/ ~ssPv2 (skf3 $_654) \/ ~ssPv2 (skf3 (skf3 $_654)) \/
% 0.49/0.66     ssPv1 (skf2 (skf3 $_654))
% 0.49/0.66  |- ~ssPv1 (skf2 (skf2 $_660)) \/ ~ssPv2 $_660 \/ ~ssPv2 (skf2 $_660) \/
% 0.49/0.66     ~ssRr (skf2 $_660) $_662 \/ ssPv1 $_662
% 0.49/0.66  |- ~ssPv1 (skf2 (skf3 $_662)) \/ ~ssPv2 $_660 \/ ~ssPv2 (skf3 $_662) \/
% 0.49/0.66     ~ssRr $_660 (skf3 $_662) \/ ssPv1 $_662
% 0.49/0.66  |- ~ssPv1 $_669 \/ ~ssPv2 $_667 \/ ~ssPv2 (skf2 $_667) \/
% 0.49/0.66     ~ssRr (skf2 $_667) $_669 \/ ssPv1 (skf2 (skf2 $_667))
% 0.49/0.66  |- ~ssPv1 $_669 \/ ~ssPv2 $_667 \/ ~ssPv2 (skf3 $_669) \/
% 0.49/0.66     ~ssRr $_667 (skf3 $_669) \/ ssPv1 (skf2 (skf3 $_669))
% 0.49/0.66  |- ~ssPv1 $_676 \/ ~ssPv2 (skf3 $_675) \/ ~ssPv3 $_675 \/
% 0.49/0.66     ~ssRr $_675 $_677 \/ ~ssRr $_676 $_675 \/ ssPv1 $_677
% 0.49/0.66  |- ~ssPv1 $_676 \/ ~ssPv2 $_674 \/ ~ssPv3 (skf2 $_674) \/
% 0.49/0.66     ~ssRr $_676 (skf2 $_674) \/ ~ssRr (skf2 $_674) $_677 \/ ssPv1 $_677
% 0.49/0.66  |- ~ssPv1 $_676 \/ ~ssPv2 $_674 \/ ~ssPv3 (skf3 $_677) \/
% 0.49/0.66     ~ssRr $_674 (skf3 $_677) \/ ~ssRr $_676 (skf3 $_677) \/ ssPv1 $_677
% 0.49/0.66  |- ~ssPv1 $_676 \/ ~ssPv2 $_674 \/ ~ssPv3 $_675 \/ ~ssRr $_674 $_675 \/
% 0.49/0.66     ~ssRr $_676 $_675 \/ ssPv1 (skf2 $_675)
% 0.52/0.67  |- ~ssPv1 (skf3 $_675) \/ ~ssPv2 $_674 \/ ~ssPv3 $_675 \/
% 0.52/0.67     ~ssRr $_674 $_675 \/ ~ssRr $_675 $_677 \/ ssPv1 $_677
% 0.52/0.67  |- ~ssPv1 $_676 \/ ~ssPv2 $_674 \/ ~ssPv3 (skf2 $_676) \/
% 0.52/0.67     ~ssRr $_674 (skf2 $_676) \/ ~ssRr (skf2 $_676) $_677 \/ ssPv1 $_677
% 0.52/0.67  |- ~ssPv1 $_679 \/ ~ssPv2 (skf3 (skf3 $_680)) \/ ~ssPv3 (skf3 $_680) \/
% 0.52/0.67     ~ssRr $_679 (skf3 $_680) \/ ssPv1 $_680
% 0.52/0.67  |- ~ssPv1 $_679 \/ ~ssPv2 (skf3 $_678) \/ ~ssPv3 $_678 \/
% 0.52/0.67     ~ssRr $_679 $_678 \/ ssPv1 (skf2 $_678)
% 0.52/0.67  |- ~ssPv1 $_679 \/ ~ssPv2 (skf3 (skf2 $_679)) \/ ~ssPv3 (skf2 $_679) \/
% 0.52/0.67     ~ssRr (skf2 $_679) $_680 \/ ssPv1 $_680
% 0.52/0.67  |- ~ssPv1 $_682 \/ ~ssPv2 (skf3 (skf2 $_682)) \/ ~ssPv3 (skf2 $_682) \/
% 0.52/0.67     ssPv1 (skf2 (skf2 $_682))
% 0.52/0.67  |- ~ssPv1 $_690 \/ ~ssPv2 $_688 \/ ~ssPv3 (skf2 $_688) \/
% 0.52/0.67     ~ssRr $_690 (skf2 $_688) \/ ssPv1 (skf2 (skf2 $_688))
% 0.52/0.67  |- ~ssPv1 (skf3 $_689) \/ ~ssPv2 $_688 \/ ~ssPv3 $_689 \/
% 0.52/0.67     ~ssRr $_688 $_689 \/ ssPv1 (skf2 $_689)
% 0.52/0.67  |- ~ssPv1 $_690 \/ ~ssPv2 $_688 \/ ~ssPv3 (skf2 $_690) \/
% 0.52/0.67     ~ssRr $_688 (skf2 $_690) \/ ssPv1 (skf2 (skf2 $_690))
% 0.52/0.67  |- ~ssPv1 (skf3 (skf2 $_691)) \/ ~ssPv2 $_691 \/ ~ssPv3 (skf2 $_691) \/
% 0.52/0.67     ssPv1 (skf2 (skf2 $_691))
% 0.52/0.67  |- ~ssPv1 (skf3 (skf2 $_698)) \/ ~ssPv2 $_698 \/ ~ssPv3 (skf2 $_698) \/
% 0.52/0.67     ~ssRr (skf2 $_698) $_700 \/ ssPv1 $_700
% 0.52/0.67  |- ~ssPv1 (skf3 (skf3 $_700)) \/ ~ssPv2 $_698 \/ ~ssPv3 (skf3 $_700) \/
% 0.52/0.67     ~ssRr $_698 (skf3 $_700) \/ ssPv1 $_700
% 0.52/0.67  |- ~ssPv1 $_715 \/ ~ssPv2 (skf3 $_715) \/ ~ssPv4 $_717 \/
% 0.52/0.67     ~ssRr $_715 $_717 \/ ~ssRr $_716 $_715 \/ ssPv1 $_716
% 0.52/0.67  |- ~ssPv1 (skf2 $_714) \/ ~ssPv2 $_714 \/ ~ssPv4 $_717 \/
% 0.52/0.67     ~ssRr $_716 (skf2 $_714) \/ ~ssRr (skf2 $_714) $_717 \/ ssPv1 $_716
% 0.52/0.67  |- ~ssPv1 (skf3 $_717) \/ ~ssPv2 $_714 \/ ~ssPv4 $_717 \/
% 0.52/0.67     ~ssRr $_714 (skf3 $_717) \/ ~ssRr $_716 (skf3 $_717) \/ ssPv1 $_716
% 0.52/0.67  |- ~ssPv1 $_715 \/ ~ssPv2 $_714 \/ ~ssPv4 (skf2 $_715) \/
% 0.52/0.67     ~ssRr $_714 $_715 \/ ~ssRr $_716 $_715 \/ ssPv1 $_716
% 0.52/0.67  |- ~ssPv1 $_715 \/ ~ssPv2 $_714 \/ ~ssPv4 $_717 \/ ~ssRr $_714 $_715 \/
% 0.52/0.67     ~ssRr $_715 $_717 \/ ssPv1 (skf3 $_715)
% 0.52/0.67  |- ~ssPv1 (skf2 $_716) \/ ~ssPv2 $_714 \/ ~ssPv4 $_717 \/
% 0.52/0.67     ~ssRr $_714 (skf2 $_716) \/ ~ssRr (skf2 $_716) $_717 \/ ssPv1 $_716
% 0.52/0.67  |- ~ssPv1 (skf3 $_720) \/ ~ssPv2 (skf3 (skf3 $_720)) \/ ~ssPv4 $_720 \/
% 0.52/0.67     ~ssRr $_719 (skf3 $_720) \/ ssPv1 $_719
% 0.52/0.67  |- ~ssPv1 $_718 \/ ~ssPv2 (skf3 $_718) \/ ~ssPv4 (skf2 $_718) \/
% 0.52/0.67     ~ssRr $_719 $_718 \/ ssPv1 $_719
% 0.52/0.67  |- ~ssPv1 (skf2 $_719) \/ ~ssPv2 (skf3 (skf2 $_719)) \/ ~ssPv4 $_720 \/
% 0.52/0.67     ~ssRr (skf2 $_719) $_720 \/ ssPv1 $_719
% 0.52/0.67  |- ~ssPv1 (skf2 $_722) \/ ~ssPv2 (skf3 (skf2 $_722)) \/
% 0.52/0.67     ~ssPv4 (skf2 (skf2 $_722)) \/ ssPv1 $_722
% 0.52/0.67  |- ~ssPv1 (skf2 $_728) \/ ~ssPv2 $_728 \/ ~ssPv4 (skf2 (skf2 $_728)) \/
% 0.52/0.67     ~ssRr $_730 (skf2 $_728) \/ ssPv1 $_730
% 0.52/0.67  |- ~ssPv1 $_729 \/ ~ssPv2 $_728 \/ ~ssPv4 (skf2 $_729) \/
% 0.52/0.67     ~ssRr $_728 $_729 \/ ssPv1 (skf3 $_729)
% 0.52/0.67  |- ~ssPv1 (skf2 $_730) \/ ~ssPv2 $_728 \/ ~ssPv4 (skf2 (skf2 $_730)) \/
% 0.52/0.67     ~ssRr $_728 (skf2 $_730) \/ ssPv1 $_730
% 0.52/0.67  |- ~ssPv1 (skf2 $_731) \/ ~ssPv2 $_731 \/ ~ssPv4 (skf2 (skf2 $_731)) \/
% 0.52/0.67     ssPv1 (skf3 (skf2 $_731))
% 0.52/0.67  |- ~ssPv1 (skf2 $_738) \/ ~ssPv2 $_738 \/ ~ssPv4 $_740 \/
% 0.52/0.67     ~ssRr (skf2 $_738) $_740 \/ ssPv1 (skf3 (skf2 $_738))
% 0.52/0.67  |- ~ssPv1 (skf3 $_740) \/ ~ssPv2 $_738 \/ ~ssPv4 $_740 \/
% 0.52/0.67     ~ssRr $_738 (skf3 $_740) \/ ssPv1 (skf3 (skf3 $_740))
% 0.52/0.67  |- ~ssPv2 (skf3 $_755) \/ ~ssPv3 $_755 \/ ~ssPv3 $_757 \/ ~ssPv4 $_756 \/
% 0.52/0.67     ~ssRr $_755 $_756 \/ ~ssRr $_755 $_757
% 0.52/0.67  |- ~ssPv2 $_754 \/ ~ssPv3 $_757 \/ ~ssPv3 (skf2 $_754) \/ ~ssPv4 $_756 \/
% 0.52/0.67     ~ssRr (skf2 $_754) $_756 \/ ~ssRr (skf2 $_754) $_757
% 0.52/0.67  |- ~ssPv2 $_754 \/ ~ssPv3 $_757 \/ ~ssPv3 (skf3 $_756) \/ ~ssPv4 $_756 \/
% 0.52/0.67     ~ssRr $_754 (skf3 $_756) \/ ~ssRr (skf3 $_756) $_757
% 0.52/0.67  |- ~ssPv2 $_754 \/ ~ssPv3 $_755 \/ ~ssPv3 $_757 \/ ~ssPv4 (skf2 $_755) \/
% 0.52/0.67     ~ssRr $_754 $_755 \/ ~ssRr $_755 $_757
% 0.52/0.67  |- ~ssPv2 $_754 \/ ~ssPv3 $_757 \/ ~ssPv3 (skf3 $_757) \/ ~ssPv4 $_756 \/
% 0.52/0.67     ~ssRr $_754 (skf3 $_757) \/ ~ssRr (skf3 $_757) $_756
% 0.52/0.67  |- ~ssPv2 $_754 \/ ~ssPv3 $_755 \/ ~ssPv3 (skf2 $_755) \/ ~ssPv4 $_756 \/
% 0.52/0.67     ~ssRr $_754 $_755 \/ ~ssRr $_755 $_756
% 0.52/0.67  |- ~ssPv2 (skf3 $_756) \/ ~ssPv3 (skf3 $_756) \/ ~ssPv4 $_756 \/
% 0.52/0.67     ~ssRr (skf3 $_756) (skf3 $_756)
% 0.52/0.67  |- ~ssPv2 (skf3 (skf3 $_760)) \/ ~ssPv3 $_761 \/ ~ssPv3 (skf3 $_760) \/
% 0.52/0.67     ~ssPv4 $_760 \/ ~ssRr (skf3 $_760) $_761
% 0.52/0.67  |- ~ssPv2 (skf3 $_759) \/ ~ssPv3 $_759 \/ ~ssPv3 $_761 \/
% 0.52/0.67     ~ssPv4 (skf2 $_759) \/ ~ssRr $_759 $_761
% 0.52/0.67  |- ~ssPv2 (skf3 (skf3 $_761)) \/ ~ssPv3 $_761 \/ ~ssPv3 (skf3 $_761) \/
% 0.52/0.67     ~ssPv4 $_760 \/ ~ssRr (skf3 $_761) $_760
% 0.52/0.67  |- ~ssPv2 (skf3 $_759) \/ ~ssPv3 $_759 \/ ~ssPv3 (skf2 $_759) \/
% 0.52/0.67     ~ssPv4 $_760 \/ ~ssRr $_759 $_760
% 0.52/0.67  |- ~ssPv2 (skf3 (skf3 $_763)) \/ ~ssPv3 $_763 \/ ~ssPv3 (skf3 $_763) \/
% 0.52/0.67     ~ssPv4 (skf2 (skf3 $_763))
% 0.52/0.67  |- ~ssPv2 (skf3 (skf3 $_766)) \/ ~ssPv3 (skf2 (skf3 $_766)) \/
% 0.52/0.67     ~ssPv3 (skf3 $_766) \/ ~ssPv4 $_766
% 0.52/0.67  |- ~ssPv2 $_772 \/ ~ssPv3 $_774 \/ ~ssPv3 (skf2 $_772) \/
% 0.52/0.67     ~ssPv4 (skf2 (skf2 $_772)) \/ ~ssRr (skf2 $_772) $_774
% 0.52/0.67  |- ~ssPv2 $_772 \/ ~ssPv3 $_774 \/ ~ssPv3 (skf3 $_774) \/
% 0.52/0.67     ~ssPv4 (skf2 (skf3 $_774)) \/ ~ssRr $_772 (skf3 $_774)
% 0.52/0.67  |- ~ssPv2 $_779 \/ ~ssPv3 (skf2 $_779) \/ ~ssPv3 (skf2 (skf2 $_779)) \/
% 0.52/0.67     ~ssPv4 $_781 \/ ~ssRr (skf2 $_779) $_781
% 0.52/0.67  |- ~ssPv2 $_779 \/ ~ssPv3 (skf2 (skf3 $_781)) \/ ~ssPv3 (skf3 $_781) \/
% 0.52/0.67     ~ssPv4 $_781 \/ ~ssRr $_779 (skf3 $_781)
% 0.52/0.67  SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.52/0.67  
%------------------------------------------------------------------------------