↑ Up

Metis---2.4.SAT-Sat.s

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

% Computer : n027.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:22 EDT 2022

% Result   : Satisfiable 0.19s 0.51s
% Output   : Saturation 0.19s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12  % Problem  : SYN740-1 : TPTP v8.1.0. Released v2.5.0.
% 0.03/0.13  % Command  : metis --show proof --show saturation %s
% 0.13/0.34  % Computer : n027.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 : Mon Jul 11 12:57:34 EDT 2022
% 0.13/0.34  % CPUTime  : 
% 0.13/0.34  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.19/0.51  % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.51  
% 0.19/0.51  SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.51  |- ssRr $U (skf1 $U)
% 0.19/0.51  |- ~ssPv3 $U \/ ~ssRr $U $V \/ ssPv1 $U \/ ssPv2 $U \/ ssPv3 $V
% 0.19/0.51  |- ~ssPv1 $U \/ ~ssPv3 $U \/ ~ssRr $U $V \/ ssPv2 $U \/ ssPv4 $V
% 0.19/0.51  |- ~ssPv1 $U \/ ~ssPv1 $V \/ ~ssPv2 $U \/ ~ssPv3 $U \/ ~ssRr $U $V
% 0.19/0.51  |- ~ssPv3 $U \/ ~ssPv4 $U \/ ~ssRr $U $V \/ ~ssRr $U $W \/ ssPv3 $W \/
% 0.19/0.51     ssPv4 $V
% 0.19/0.51  |- ~ssPv1 $U \/ ~ssPv4 $U \/ ~ssRr $U $V \/ ~ssRr $U $W \/ ssPv2 $W \/
% 0.19/0.51     ssPv3 $V
% 0.19/0.51  |- ~ssPv3 $U \/ ~ssPv4 $V \/ ~ssRr $U $V \/ ~ssRr $U $W \/ ssPv4 $U \/
% 0.19/0.51     ssPv4 $W
% 0.19/0.51  |- ~ssPv1 $V \/ ~ssPv3 $U \/ ~ssRr $U $V \/ ~ssRr $U $W \/ ssPv1 $W \/
% 0.19/0.51     ssPv4 $U
% 0.19/0.51  |- ~ssPv1 $U \/ ~ssPv1 $V \/ ~ssRr $U $V \/ ~ssRr $U $W \/ ssPv3 $W \/
% 0.19/0.51     ssPv4 $U
% 0.19/0.51  |- ~ssPv1 $V \/ ~ssPv2 $U \/ ~ssRr $U $V \/ ~ssRr $U $W \/ ssPv1 $W \/
% 0.19/0.51     ssPv3 $U
% 0.19/0.51  |- ~ssPv1 $U \/ ~ssPv4 $V \/ ~ssRr $U $V \/ ~ssRr $U $W \/ ssPv3 $U \/
% 0.19/0.51     ssPv3 $W
% 0.19/0.51  |- ~ssPv1 $U \/ ~ssPv2 $V \/ ~ssRr $U $V \/ ~ssRr $U $W \/ ssPv1 $W \/
% 0.19/0.51     ssPv3 $U
% 0.19/0.51  |- ~ssPv2 $W \/ ~ssPv4 $V \/ ~ssRr $U $V \/ ~ssRr $U $W \/ ssPv3 $U \/
% 0.19/0.51     ssPv4 $U
% 0.19/0.51  |- ~ssPv1 $U \/ ~ssPv4 $V \/ ~ssRr $U $V \/ ~ssRr $U $W \/ ssPv2 $U \/
% 0.19/0.51     ssPv3 $W
% 0.19/0.51  |- ~ssPv3 $W \/ ~ssPv4 $V \/ ~ssRr $U $V \/ ~ssRr $U $W \/ ssPv2 $U \/
% 0.19/0.51     ssPv3 $U
% 0.19/0.51  |- ~ssPv3 $U \/ ~ssPv4 $V \/ ~ssRr $U $V \/ ~ssRr $U $W \/ ssPv1 $U \/
% 0.19/0.51     ssPv2 $W
% 0.19/0.51  |- ~ssPv2 $U \/ ~ssPv3 $V \/ ~ssPv4 $U \/ ~ssRr $U $V \/ ~ssRr $U $W \/
% 0.19/0.51     ssPv1 $W
% 0.19/0.51  |- ~ssPv2 $U \/ ~ssPv3 $U \/ ~ssPv4 $V \/ ~ssRr $U $V \/ ~ssRr $U $W \/
% 0.19/0.51     ssPv3 $W
% 0.19/0.51  |- ~ssPv2 $U \/ ~ssPv3 $U \/ ~ssPv3 $V \/ ~ssRr $U $V \/ ~ssRr $U $W \/
% 0.19/0.51     ssPv1 $W
% 0.19/0.51  |- ~ssPv1 $V \/ ~ssPv2 $U \/ ~ssPv3 $U \/ ~ssRr $U $V \/ ~ssRr $U $W \/
% 0.19/0.51     ssPv1 $W
% 0.19/0.51  |- ~ssPv2 $W \/ ~ssPv4 $U \/ ~ssPv4 $V \/ ~ssRr $U $V \/ ~ssRr $U $W \/
% 0.19/0.51     ssPv2 $U
% 0.19/0.51  |- ~ssPv1 $U \/ ~ssPv1 $W \/ ~ssPv4 $V \/ ~ssRr $U $V \/ ~ssRr $U $W \/
% 0.19/0.51     ssPv2 $U
% 0.19/0.51  |- ~ssPv1 $U \/ ~ssPv2 $U \/ ~ssPv2 $W \/ ~ssPv4 $V \/ ~ssRr $U $V \/
% 0.19/0.51     ~ssRr $U $W
% 0.19/0.51  |- ~ssPv1 $U \/ ~ssPv1 $W \/ ~ssPv2 $U \/ ~ssPv2 $V \/ ~ssRr $U $V \/
% 0.19/0.51     ~ssRr $U $W
% 0.19/0.51  |- ~ssPv2 $W \/ ~ssPv4 $V \/ ~ssRr $U $V \/ ~ssRr $U $W \/ ~ssRr $U $X \/
% 0.19/0.51     ssPv3 $X \/ ssPv4 $U
% 0.19/0.51  |- ~ssPv1 $W \/ ~ssPv3 $V \/ ~ssRr $U $V \/ ~ssRr $U $W \/ ~ssRr $U $X \/
% 0.19/0.51     ssPv1 $X \/ ssPv3 $U
% 0.19/0.51  |- ~ssPv1 $W \/ ~ssPv2 $V \/ ~ssRr $U $V \/ ~ssRr $U $W \/ ~ssRr $U $X \/
% 0.19/0.51     ssPv1 $U \/ ssPv2 $X
% 0.19/0.51  |- ~ssPv2 $U \/ ~ssPv2 $W \/ ~ssPv3 $V \/ ~ssRr $U $V \/ ~ssRr $U $W \/
% 0.19/0.51     ~ssRr $U $X \/ ssPv3 $X
% 0.19/0.51  |- ~ssPv1 $U \/ ~ssPv3 $W \/ ~ssPv4 $V \/ ~ssRr $U $V \/ ~ssRr $U $W \/
% 0.19/0.51     ~ssRr $U $X \/ ssPv4 $X
% 0.19/0.51  |- ~ssPv1 $U \/ ~ssPv1 $W \/ ~ssPv2 $V \/ ~ssRr $U $V \/ ~ssRr $U $W \/
% 0.19/0.51     ~ssRr $U $X \/ ssPv1 $X
% 0.19/0.51  |- ~ssPv1 $W \/ ~ssPv2 $U \/ ~ssPv2 $V \/ ~ssRr $U $V \/ ~ssRr $U $W \/
% 0.19/0.51     ~ssRr $U $X \/ ssPv4 $X
% 0.19/0.51  |- ~ssPv3 $U \/ ~ssPv4 $U \/ ~ssRr $U $W \/ ssPv3 $W \/ ssPv4 $W
% 0.19/0.51  |- ~ssPv1 $U \/ ~ssPv4 $U \/ ~ssRr $U $W \/ ssPv2 $W \/ ssPv3 $W
% 0.19/0.51  |- ~ssPv1 $U \/ ~ssPv1 $W \/ ~ssRr $U $W \/ ssPv3 $W \/ ssPv4 $U
% 0.19/0.51  |- ~ssPv1 $U \/ ~ssPv4 $W \/ ~ssRr $U $W \/ ssPv3 $U \/ ssPv3 $W
% 0.19/0.51  |- ~ssPv1 $U \/ ~ssPv2 $W \/ ~ssRr $U $W \/ ssPv1 $W \/ ssPv3 $U
% 0.19/0.51  |- ~ssPv2 $W \/ ~ssPv4 $W \/ ~ssRr $U $W \/ ssPv3 $U \/ ssPv4 $U
% 0.19/0.51  |- ~ssPv1 $U \/ ~ssPv4 $W \/ ~ssRr $U $W \/ ssPv2 $U \/ ssPv3 $W
% 0.19/0.51  |- ~ssPv3 $W \/ ~ssPv4 $W \/ ~ssRr $U $W \/ ssPv2 $U \/ ssPv3 $U
% 0.19/0.51  |- ~ssPv3 $U \/ ~ssPv4 $W \/ ~ssRr $U $W \/ ssPv1 $U \/ ssPv2 $W
% 0.19/0.51  |- ~ssPv2 $U \/ ~ssPv3 $W \/ ~ssPv4 $U \/ ~ssRr $U $W \/ ssPv1 $W
% 0.19/0.51  |- ~ssPv2 $U \/ ~ssPv3 $U \/ ~ssPv4 $W \/ ~ssRr $U $W \/ ssPv3 $W
% 0.19/0.51  |- ~ssPv2 $U \/ ~ssPv3 $U \/ ~ssPv3 $W \/ ~ssRr $U $W \/ ssPv1 $W
% 0.19/0.51  |- ~ssPv2 $W \/ ~ssPv4 $U \/ ~ssPv4 $W \/ ~ssRr $U $W \/ ssPv2 $U
% 0.19/0.51  |- ~ssPv1 $U \/ ~ssPv1 $W \/ ~ssPv4 $W \/ ~ssRr $U $W \/ ssPv2 $U
% 0.19/0.51  |- ~ssPv1 $U \/ ~ssPv2 $U \/ ~ssPv2 $W \/ ~ssPv4 $W \/ ~ssRr $U $W
% 0.19/0.51  |- ~ssPv1 $U \/ ~ssPv1 $W \/ ~ssPv2 $U \/ ~ssPv2 $W \/ ~ssRr $U $W
% 0.19/0.51  |- ~ssPv2 $W \/ ~ssPv4 $W \/ ~ssRr $U $W \/ ~ssRr $U $X \/ ssPv3 $X \/
% 0.19/0.51     ssPv4 $U
% 0.19/0.51  |- ~ssPv2 $W \/ ~ssPv4 $X \/ ~ssRr $U $W \/ ~ssRr $U $X \/ ssPv3 $X \/
% 0.19/0.51     ssPv4 $U
% 0.19/0.51  |- ~ssPv2 $X \/ ~ssPv4 $V \/ ~ssRr $U $V \/ ~ssRr $U $X \/ ssPv3 $X \/
% 0.19/0.51     ssPv4 $U
% 0.19/0.51  |- ~ssPv2 $X \/ ~ssPv4 $X \/ ~ssRr $U $X \/ ssPv3 $X \/ ssPv4 $U
% 0.19/0.51  |- ~ssPv1 $W \/ ~ssPv3 $W \/ ~ssRr $U $W \/ ~ssRr $U $X \/ ssPv1 $X \/
% 0.19/0.51     ssPv3 $U
% 0.19/0.51  |- ~ssPv1 $W \/ ~ssPv3 $X \/ ~ssRr $U $W \/ ~ssRr $U $X \/ ssPv1 $X \/
% 0.19/0.51     ssPv3 $U
% 0.19/0.51  |- ~ssPv1 $W \/ ~ssPv2 $W \/ ~ssRr $U $W \/ ~ssRr $U $X \/ ssPv1 $U \/
% 0.19/0.51     ssPv2 $X
% 0.19/0.51  |- ~ssPv1 $X \/ ~ssPv2 $V \/ ~ssRr $U $V \/ ~ssRr $U $X \/ ssPv1 $U \/
% 0.19/0.51     ssPv2 $X
% 0.19/0.51  |- ~ssPv2 $U \/ ~ssPv2 $W \/ ~ssPv3 $W \/ ~ssRr $U $W \/ ~ssRr $U $X \/
% 0.19/0.51     ssPv3 $X
% 0.19/0.51  |- ~ssPv2 $U \/ ~ssPv2 $X \/ ~ssPv3 $V \/ ~ssRr $U $V \/ ~ssRr $U $X \/
% 0.19/0.51     ssPv3 $X
% 0.19/0.51  |- ~ssPv1 $U \/ ~ssPv3 $W \/ ~ssPv4 $W \/ ~ssRr $U $W \/ ~ssRr $U $X \/
% 0.19/0.51     ssPv4 $X
% 0.19/0.51  |- ~ssPv1 $U \/ ~ssPv3 $X \/ ~ssPv4 $V \/ ~ssRr $U $V \/ ~ssRr $U $X \/
% 0.19/0.51     ssPv4 $X
% 0.19/0.51  |- ~ssPv1 $U \/ ~ssPv1 $W \/ ~ssPv2 $W \/ ~ssRr $U $W \/ ~ssRr $U $X \/
% 0.19/0.51     ssPv1 $X
% 0.19/0.51  |- ~ssPv1 $U \/ ~ssPv1 $W \/ ~ssPv2 $X \/ ~ssRr $U $W \/ ~ssRr $U $X \/
% 0.19/0.51     ssPv1 $X
% 0.19/0.51  |- ~ssPv1 $W \/ ~ssPv2 $U \/ ~ssPv2 $W \/ ~ssRr $U $W \/ ~ssRr $U $X \/
% 0.19/0.51     ssPv4 $X
% 0.19/0.51  |- ~ssPv1 $W \/ ~ssPv2 $U \/ ~ssPv2 $X \/ ~ssRr $U $W \/ ~ssRr $U $X \/
% 0.19/0.51     ssPv4 $X
% 0.19/0.51  |- ~ssPv1 $X \/ ~ssPv2 $U \/ ~ssPv2 $V \/ ~ssRr $U $V \/ ~ssRr $U $X \/
% 0.19/0.51     ssPv4 $X
% 0.19/0.51  |- ~ssPv1 $X \/ ~ssPv2 $U \/ ~ssPv2 $X \/ ~ssRr $U $X \/ ssPv4 $X
% 0.19/0.51  |- ~ssPv3 $_1 \/ ssPv1 $_1 \/ ssPv2 $_1 \/ ssPv3 (skf1 $_1)
% 0.19/0.51  |- ~ssPv1 $_4 \/ ~ssPv3 $_4 \/ ssPv2 $_4 \/ ssPv4 (skf1 $_4)
% 0.19/0.51  |- ~ssPv1 $_7 \/ ~ssPv1 (skf1 $_7) \/ ~ssPv2 $_7 \/ ~ssPv3 $_7
% 0.19/0.51  |- ~ssPv3 $_10 \/ ~ssPv4 $_10 \/ ssPv3 (skf1 $_10) \/ ssPv4 (skf1 $_10)
% 0.19/0.51  |- ~ssPv1 $_13 \/ ~ssPv4 $_13 \/ ssPv2 (skf1 $_13) \/ ssPv3 (skf1 $_13)
% 0.19/0.51  |- ~ssPv1 $_16 \/ ~ssPv1 (skf1 $_16) \/ ssPv3 (skf1 $_16) \/ ssPv4 $_16
% 0.19/0.51  |- ~ssPv1 $_19 \/ ~ssPv4 (skf1 $_19) \/ ssPv3 $_19 \/ ssPv3 (skf1 $_19)
% 0.19/0.51  |- ~ssPv1 $_22 \/ ~ssPv2 (skf1 $_22) \/ ssPv1 (skf1 $_22) \/ ssPv3 $_22
% 0.19/0.51  |- ~ssPv2 (skf1 $_25) \/ ~ssPv4 (skf1 $_25) \/ ssPv3 $_25 \/ ssPv4 $_25
% 0.19/0.51  |- ~ssPv1 $_28 \/ ~ssPv4 (skf1 $_28) \/ ssPv2 $_28 \/ ssPv3 (skf1 $_28)
% 0.19/0.51  |- ~ssPv3 (skf1 $_31) \/ ~ssPv4 (skf1 $_31) \/ ssPv2 $_31 \/ ssPv3 $_31
% 0.19/0.51  |- ~ssPv3 $_34 \/ ~ssPv4 (skf1 $_34) \/ ssPv1 $_34 \/ ssPv2 (skf1 $_34)
% 0.19/0.51  |- ~ssPv2 $_37 \/ ~ssPv3 (skf1 $_37) \/ ~ssPv4 $_37 \/ ssPv1 (skf1 $_37)
% 0.19/0.51  |- ~ssPv2 $_40 \/ ~ssPv3 $_40 \/ ~ssPv4 (skf1 $_40) \/ ssPv3 (skf1 $_40)
% 0.19/0.51  |- ~ssPv2 $_43 \/ ~ssPv3 $_43 \/ ~ssPv3 (skf1 $_43) \/ ssPv1 (skf1 $_43)
% 0.19/0.51  |- ~ssPv2 (skf1 $_46) \/ ~ssPv4 $_46 \/ ~ssPv4 (skf1 $_46) \/ ssPv2 $_46
% 0.19/0.52  |- ~ssPv1 $_49 \/ ~ssPv1 (skf1 $_49) \/ ~ssPv4 (skf1 $_49) \/ ssPv2 $_49
% 0.19/0.52  |- ~ssPv1 $_52 \/ ~ssPv2 $_52 \/ ~ssPv2 (skf1 $_52) \/ ~ssPv4 (skf1 $_52)
% 0.19/0.52  |- ~ssPv1 $_55 \/ ~ssPv1 (skf1 $_55) \/ ~ssPv2 $_55 \/ ~ssPv2 (skf1 $_55)
% 0.19/0.52  |- ~ssPv2 (skf1 $_58) \/ ~ssPv4 (skf1 $_58) \/ ssPv3 (skf1 $_58) \/
% 0.19/0.52     ssPv4 $_58
% 0.19/0.52  |- ~ssPv1 (skf1 $_61) \/ ~ssPv2 $_61 \/ ~ssPv2 (skf1 $_61) \/
% 0.19/0.52     ssPv4 (skf1 $_61)
% 0.19/0.52  |- ~ssPv3 $_64 \/ ~ssPv4 $_64 \/ ~ssRr $_64 $_66 \/ ssPv3 $_66 \/
% 0.19/0.52     ssPv4 (skf1 $_64)
% 0.19/0.52  |- ~ssPv3 $_64 \/ ~ssPv4 $_64 \/ ~ssRr $_64 $_65 \/ ssPv3 (skf1 $_64) \/
% 0.19/0.52     ssPv4 $_65
% 0.19/0.52  |- ~ssPv1 $_71 \/ ~ssPv4 $_71 \/ ~ssRr $_71 $_73 \/ ssPv2 $_73 \/
% 0.19/0.52     ssPv3 (skf1 $_71)
% 0.19/0.52  |- ~ssPv1 $_71 \/ ~ssPv4 $_71 \/ ~ssRr $_71 $_72 \/ ssPv2 (skf1 $_71) \/
% 0.19/0.52     ssPv3 $_72
% 0.19/0.52  |- ~ssPv3 $_78 \/ ~ssPv4 (skf1 $_78) \/ ~ssRr $_78 $_80 \/ ssPv4 $_78 \/
% 0.19/0.52     ssPv4 $_80
% 0.19/0.52  |- ~ssPv3 $_78 \/ ~ssPv4 $_79 \/ ~ssRr $_78 $_79 \/ ssPv4 $_78 \/
% 0.19/0.52     ssPv4 (skf1 $_78)
% 0.19/0.52  |- ~ssPv1 (skf1 $_85) \/ ~ssPv3 $_85 \/ ~ssRr $_85 $_87 \/ ssPv1 $_87 \/
% 0.19/0.52     ssPv4 $_85
% 0.19/0.52  |- ~ssPv1 $_86 \/ ~ssPv3 $_85 \/ ~ssRr $_85 $_86 \/ ssPv1 (skf1 $_85) \/
% 0.19/0.52     ssPv4 $_85
% 0.19/0.52  |- ~ssPv1 $_92 \/ ~ssPv1 (skf1 $_92) \/ ~ssRr $_92 $_94 \/ ssPv3 $_94 \/
% 0.19/0.52     ssPv4 $_92
% 0.19/0.52  |- ~ssPv1 $_92 \/ ~ssPv1 $_93 \/ ~ssRr $_92 $_93 \/ ssPv3 (skf1 $_92) \/
% 0.19/0.52     ssPv4 $_92
% 0.19/0.52  |- ~ssPv1 (skf1 $_99) \/ ~ssPv2 $_99 \/ ~ssRr $_99 $_101 \/ ssPv1 $_101 \/
% 0.19/0.52     ssPv3 $_99
% 0.19/0.52  |- ~ssPv1 $_100 \/ ~ssPv2 $_99 \/ ~ssRr $_99 $_100 \/ ssPv1 (skf1 $_99) \/
% 0.19/0.52     ssPv3 $_99
% 0.19/0.52  |- ~ssPv1 $_106 \/ ~ssPv4 (skf1 $_106) \/ ~ssRr $_106 $_108 \/
% 0.19/0.52     ssPv3 $_106 \/ ssPv3 $_108
% 0.19/0.52  |- ~ssPv1 $_106 \/ ~ssPv4 $_107 \/ ~ssRr $_106 $_107 \/ ssPv3 $_106 \/
% 0.19/0.52     ssPv3 (skf1 $_106)
% 0.19/0.52  |- ~ssPv1 $_113 \/ ~ssPv2 (skf1 $_113) \/ ~ssRr $_113 $_115 \/
% 0.19/0.52     ssPv1 $_115 \/ ssPv3 $_113
% 0.19/0.52  |- ~ssPv1 $_113 \/ ~ssPv2 $_114 \/ ~ssRr $_113 $_114 \/
% 0.19/0.52     ssPv1 (skf1 $_113) \/ ssPv3 $_113
% 0.19/0.52  |- ~ssPv2 $_122 \/ ~ssPv4 (skf1 $_120) \/ ~ssRr $_120 $_122 \/
% 0.19/0.52     ssPv3 $_120 \/ ssPv4 $_120
% 0.19/0.52  |- ~ssPv2 (skf1 $_120) \/ ~ssPv4 $_121 \/ ~ssRr $_120 $_121 \/
% 0.19/0.52     ssPv3 $_120 \/ ssPv4 $_120
% 0.19/0.52  |- ~ssPv1 $_127 \/ ~ssPv4 (skf1 $_127) \/ ~ssRr $_127 $_129 \/
% 0.19/0.52     ssPv2 $_127 \/ ssPv3 $_129
% 0.19/0.52  |- ~ssPv1 $_127 \/ ~ssPv4 $_128 \/ ~ssRr $_127 $_128 \/ ssPv2 $_127 \/
% 0.19/0.52     ssPv3 (skf1 $_127)
% 0.19/0.52  |- ~ssPv3 $_136 \/ ~ssPv4 (skf1 $_134) \/ ~ssRr $_134 $_136 \/
% 0.19/0.52     ssPv2 $_134 \/ ssPv3 $_134
% 0.19/0.52  |- ~ssPv3 (skf1 $_134) \/ ~ssPv4 $_135 \/ ~ssRr $_134 $_135 \/
% 0.19/0.52     ssPv2 $_134 \/ ssPv3 $_134
% 0.19/0.52  |- ~ssPv3 $_141 \/ ~ssPv4 (skf1 $_141) \/ ~ssRr $_141 $_143 \/
% 0.19/0.52     ssPv1 $_141 \/ ssPv2 $_143
% 0.19/0.52  |- ~ssPv3 $_141 \/ ~ssPv4 $_142 \/ ~ssRr $_141 $_142 \/ ssPv1 $_141 \/
% 0.19/0.52     ssPv2 (skf1 $_141)
% 0.19/0.52  |- ~ssPv2 $_148 \/ ~ssPv3 (skf1 $_148) \/ ~ssPv4 $_148 \/
% 0.19/0.52     ~ssRr $_148 $_150 \/ ssPv1 $_150
% 0.19/0.52  |- ~ssPv2 $_148 \/ ~ssPv3 $_149 \/ ~ssPv4 $_148 \/ ~ssRr $_148 $_149 \/
% 0.19/0.52     ssPv1 (skf1 $_148)
% 0.19/0.52  |- ~ssPv2 $_155 \/ ~ssPv3 $_155 \/ ~ssPv4 (skf1 $_155) \/
% 0.19/0.52     ~ssRr $_155 $_157 \/ ssPv3 $_157
% 0.19/0.52  |- ~ssPv2 $_155 \/ ~ssPv3 $_155 \/ ~ssPv4 $_156 \/ ~ssRr $_155 $_156 \/
% 0.19/0.52     ssPv3 (skf1 $_155)
% 0.19/0.52  |- ~ssPv2 $_162 \/ ~ssPv3 $_162 \/ ~ssPv3 (skf1 $_162) \/
% 0.19/0.52     ~ssRr $_162 $_164 \/ ssPv1 $_164
% 0.19/0.52  |- ~ssPv2 $_162 \/ ~ssPv3 $_162 \/ ~ssPv3 $_163 \/ ~ssRr $_162 $_163 \/
% 0.19/0.52     ssPv1 (skf1 $_162)
% 0.19/0.52  |- ~ssPv1 (skf1 $_169) \/ ~ssPv2 $_169 \/ ~ssPv3 $_169 \/
% 0.19/0.52     ~ssRr $_169 $_171 \/ ssPv1 $_171
% 0.19/0.52  |- ~ssPv1 $_170 \/ ~ssPv2 $_169 \/ ~ssPv3 $_169 \/ ~ssRr $_169 $_170 \/
% 0.19/0.52     ssPv1 (skf1 $_169)
% 0.19/0.52  |- ~ssPv2 $_178 \/ ~ssPv4 $_176 \/ ~ssPv4 (skf1 $_176) \/
% 0.19/0.52     ~ssRr $_176 $_178 \/ ssPv2 $_176
% 0.19/0.52  |- ~ssPv2 (skf1 $_176) \/ ~ssPv4 $_176 \/ ~ssPv4 $_177 \/
% 0.19/0.52     ~ssRr $_176 $_177 \/ ssPv2 $_176
% 0.19/0.52  |- ~ssPv1 $_183 \/ ~ssPv1 $_185 \/ ~ssPv4 (skf1 $_183) \/
% 0.19/0.52     ~ssRr $_183 $_185 \/ ssPv2 $_183
% 0.19/0.52  |- ~ssPv1 $_183 \/ ~ssPv1 (skf1 $_183) \/ ~ssPv4 $_184 \/
% 0.19/0.52     ~ssRr $_183 $_184 \/ ssPv2 $_183
% 0.19/0.52  |- ~ssPv1 $_190 \/ ~ssPv2 $_190 \/ ~ssPv2 $_192 \/ ~ssPv4 (skf1 $_190) \/
% 0.19/0.52     ~ssRr $_190 $_192
% 0.19/0.52  |- ~ssPv1 $_190 \/ ~ssPv2 $_190 \/ ~ssPv2 (skf1 $_190) \/ ~ssPv4 $_191 \/
% 0.19/0.52     ~ssRr $_190 $_191
% 0.19/0.52  |- ~ssPv1 $_197 \/ ~ssPv1 $_199 \/ ~ssPv2 $_197 \/ ~ssPv2 (skf1 $_197) \/
% 0.19/0.52     ~ssRr $_197 $_199
% 0.19/0.52  |- ~ssPv1 $_197 \/ ~ssPv1 (skf1 $_197) \/ ~ssPv2 $_197 \/ ~ssPv2 $_198 \/
% 0.19/0.52     ~ssRr $_197 $_198
% 0.19/0.52  |- ~ssPv2 (skf1 $_204) \/ ~ssPv4 (skf1 $_204) \/ ~ssRr $_204 $_206 \/
% 0.19/0.52     ssPv3 $_206 \/ ssPv4 $_204
% 0.19/0.52  |- ~ssPv2 $_205 \/ ~ssPv4 $_205 \/ ~ssRr $_204 $_205 \/
% 0.19/0.52     ssPv3 (skf1 $_204) \/ ssPv4 $_204
% 0.19/0.52  |- ~ssPv2 (skf1 $_211) \/ ~ssPv4 $_213 \/ ~ssRr $_211 $_213 \/
% 0.19/0.52     ssPv3 $_213 \/ ssPv4 $_211
% 0.19/0.52  |- ~ssPv2 $_212 \/ ~ssPv4 (skf1 $_211) \/ ~ssRr $_211 $_212 \/
% 0.19/0.52     ssPv3 (skf1 $_211) \/ ssPv4 $_211
% 0.19/0.52  |- ~ssPv2 $_220 \/ ~ssPv4 (skf1 $_218) \/ ~ssRr $_218 $_220 \/
% 0.19/0.52     ssPv3 $_220 \/ ssPv4 $_218
% 0.19/0.52  |- ~ssPv2 (skf1 $_218) \/ ~ssPv4 $_219 \/ ~ssRr $_218 $_219 \/
% 0.19/0.52     ssPv3 (skf1 $_218) \/ ssPv4 $_218
% 0.19/0.52  |- ~ssPv1 (skf1 $_225) \/ ~ssPv3 (skf1 $_225) \/ ~ssRr $_225 $_227 \/
% 0.19/0.52     ssPv1 $_227 \/ ssPv3 $_225
% 0.19/0.52  |- ~ssPv1 $_226 \/ ~ssPv3 $_226 \/ ~ssRr $_225 $_226 \/
% 0.19/0.52     ssPv1 (skf1 $_225) \/ ssPv3 $_225
% 0.19/0.52  |- ~ssPv1 (skf1 $_232) \/ ~ssPv3 $_234 \/ ~ssRr $_232 $_234 \/
% 0.19/0.52     ssPv1 $_234 \/ ssPv3 $_232
% 0.19/0.52  |- ~ssPv1 $_233 \/ ~ssPv3 (skf1 $_232) \/ ~ssRr $_232 $_233 \/
% 0.19/0.52     ssPv1 (skf1 $_232) \/ ssPv3 $_232
% 0.19/0.52  |- ~ssPv1 (skf1 $_239) \/ ~ssPv2 (skf1 $_239) \/ ~ssRr $_239 $_241 \/
% 0.19/0.52     ssPv1 $_239 \/ ssPv2 $_241
% 0.19/0.52  |- ~ssPv1 $_240 \/ ~ssPv2 $_240 \/ ~ssRr $_239 $_240 \/ ssPv1 $_239 \/
% 0.19/0.52     ssPv2 (skf1 $_239)
% 0.19/0.52  |- ~ssPv1 $_248 \/ ~ssPv2 (skf1 $_246) \/ ~ssRr $_246 $_248 \/
% 0.19/0.52     ssPv1 $_246 \/ ssPv2 $_248
% 0.19/0.52  |- ~ssPv1 (skf1 $_246) \/ ~ssPv2 $_247 \/ ~ssRr $_246 $_247 \/
% 0.19/0.52     ssPv1 $_246 \/ ssPv2 (skf1 $_246)
% 0.19/0.52  |- ~ssPv2 $_253 \/ ~ssPv2 (skf1 $_253) \/ ~ssPv3 (skf1 $_253) \/
% 0.19/0.52     ~ssRr $_253 $_255 \/ ssPv3 $_255
% 0.19/0.52  |- ~ssPv2 $_253 \/ ~ssPv2 $_254 \/ ~ssPv3 $_254 \/ ~ssRr $_253 $_254 \/
% 0.19/0.52     ssPv3 (skf1 $_253)
% 0.19/0.52  |- ~ssPv2 $_260 \/ ~ssPv2 $_262 \/ ~ssPv3 (skf1 $_260) \/
% 0.19/0.52     ~ssRr $_260 $_262 \/ ssPv3 $_262
% 0.19/0.52  |- ~ssPv2 $_260 \/ ~ssPv2 (skf1 $_260) \/ ~ssPv3 $_261 \/
% 0.19/0.52     ~ssRr $_260 $_261 \/ ssPv3 (skf1 $_260)
% 0.19/0.52  |- ~ssPv1 $_267 \/ ~ssPv3 (skf1 $_267) \/ ~ssPv4 (skf1 $_267) \/
% 0.19/0.52     ~ssRr $_267 $_269 \/ ssPv4 $_269
% 0.19/0.53  |- ~ssPv1 $_267 \/ ~ssPv3 $_268 \/ ~ssPv4 $_268 \/ ~ssRr $_267 $_268 \/
% 0.19/0.53     ssPv4 (skf1 $_267)
% 0.19/0.53  |- ~ssPv1 $_274 \/ ~ssPv3 $_276 \/ ~ssPv4 (skf1 $_274) \/
% 0.19/0.53     ~ssRr $_274 $_276 \/ ssPv4 $_276
% 0.19/0.53  |- ~ssPv1 $_274 \/ ~ssPv3 (skf1 $_274) \/ ~ssPv4 $_275 \/
% 0.19/0.53     ~ssRr $_274 $_275 \/ ssPv4 (skf1 $_274)
% 0.19/0.53  |- ~ssPv1 $_281 \/ ~ssPv1 (skf1 $_281) \/ ~ssPv2 (skf1 $_281) \/
% 0.19/0.53     ~ssRr $_281 $_283 \/ ssPv1 $_283
% 0.19/0.53  |- ~ssPv1 $_281 \/ ~ssPv1 $_282 \/ ~ssPv2 $_282 \/ ~ssRr $_281 $_282 \/
% 0.19/0.53     ssPv1 (skf1 $_281)
% 0.19/0.53  |- ~ssPv1 $_288 \/ ~ssPv1 (skf1 $_288) \/ ~ssPv2 $_290 \/
% 0.19/0.53     ~ssRr $_288 $_290 \/ ssPv1 $_290
% 0.19/0.53  |- ~ssPv1 $_288 \/ ~ssPv1 $_289 \/ ~ssPv2 (skf1 $_288) \/
% 0.19/0.53     ~ssRr $_288 $_289 \/ ssPv1 (skf1 $_288)
% 0.19/0.53  |- ~ssPv1 (skf1 $_295) \/ ~ssPv2 $_295 \/ ~ssPv2 (skf1 $_295) \/
% 0.19/0.53     ~ssRr $_295 $_297 \/ ssPv4 $_297
% 0.19/0.53  |- ~ssPv1 $_296 \/ ~ssPv2 $_295 \/ ~ssPv2 $_296 \/ ~ssRr $_295 $_296 \/
% 0.19/0.53     ssPv4 (skf1 $_295)
% 0.19/0.53  |- ~ssPv1 (skf1 $_302) \/ ~ssPv2 $_302 \/ ~ssPv2 $_304 \/
% 0.19/0.53     ~ssRr $_302 $_304 \/ ssPv4 $_304
% 0.19/0.53  |- ~ssPv1 $_303 \/ ~ssPv2 $_302 \/ ~ssPv2 (skf1 $_302) \/
% 0.19/0.53     ~ssRr $_302 $_303 \/ ssPv4 (skf1 $_302)
% 0.19/0.53  |- ~ssPv1 $_311 \/ ~ssPv2 $_309 \/ ~ssPv2 (skf1 $_309) \/
% 0.19/0.53     ~ssRr $_309 $_311 \/ ssPv4 $_311
% 0.19/0.53  |- ~ssPv1 (skf1 $_309) \/ ~ssPv2 $_309 \/ ~ssPv2 $_310 \/
% 0.19/0.53     ~ssRr $_309 $_310 \/ ssPv4 (skf1 $_309)
% 0.19/0.53  |- ~ssPv2 $_318 \/ ~ssPv4 (skf1 $_316) \/ ~ssRr $_316 $_318 \/
% 0.19/0.53     ~ssRr $_316 $_319 \/ ssPv3 $_319 \/ ssPv4 $_316
% 0.19/0.53  |- ~ssPv2 (skf1 $_316) \/ ~ssPv4 $_317 \/ ~ssRr $_316 $_317 \/
% 0.19/0.53     ~ssRr $_316 $_319 \/ ssPv3 $_319 \/ ssPv4 $_316
% 0.19/0.53  |- ~ssPv2 $_318 \/ ~ssPv4 $_317 \/ ~ssRr $_316 $_317 \/
% 0.19/0.53     ~ssRr $_316 $_318 \/ ssPv3 (skf1 $_316) \/ ssPv4 $_316
% 0.19/0.53  |- ~ssPv1 $_331 \/ ~ssPv3 (skf1 $_329) \/ ~ssRr $_329 $_331 \/
% 0.19/0.53     ~ssRr $_329 $_332 \/ ssPv1 $_332 \/ ssPv3 $_329
% 0.19/0.53  |- ~ssPv1 (skf1 $_329) \/ ~ssPv3 $_330 \/ ~ssRr $_329 $_330 \/
% 0.19/0.53     ~ssRr $_329 $_332 \/ ssPv1 $_332 \/ ssPv3 $_329
% 0.19/0.53  |- ~ssPv1 $_331 \/ ~ssPv3 $_330 \/ ~ssRr $_329 $_330 \/
% 0.19/0.53     ~ssRr $_329 $_331 \/ ssPv1 (skf1 $_329) \/ ssPv3 $_329
% 0.19/0.53  |- ~ssPv1 $_344 \/ ~ssPv2 (skf1 $_342) \/ ~ssRr $_342 $_344 \/
% 0.19/0.53     ~ssRr $_342 $_345 \/ ssPv1 $_342 \/ ssPv2 $_345
% 0.19/0.53  |- ~ssPv1 (skf1 $_342) \/ ~ssPv2 $_343 \/ ~ssRr $_342 $_343 \/
% 0.19/0.53     ~ssRr $_342 $_345 \/ ssPv1 $_342 \/ ssPv2 $_345
% 0.19/0.53  |- ~ssPv1 $_344 \/ ~ssPv2 $_343 \/ ~ssRr $_342 $_343 \/
% 0.19/0.53     ~ssRr $_342 $_344 \/ ssPv1 $_342 \/ ssPv2 (skf1 $_342)
% 0.19/0.53  |- ~ssPv2 $_355 \/ ~ssPv2 $_357 \/ ~ssPv3 (skf1 $_355) \/
% 0.19/0.53     ~ssRr $_355 $_357 \/ ~ssRr $_355 $_358 \/ ssPv3 $_358
% 0.19/0.53  |- ~ssPv2 $_355 \/ ~ssPv2 (skf1 $_355) \/ ~ssPv3 $_356 \/
% 0.19/0.53     ~ssRr $_355 $_356 \/ ~ssRr $_355 $_358 \/ ssPv3 $_358
% 0.19/0.53  |- ~ssPv2 $_355 \/ ~ssPv2 $_357 \/ ~ssPv3 $_356 \/ ~ssRr $_355 $_356 \/
% 0.19/0.53     ~ssRr $_355 $_357 \/ ssPv3 (skf1 $_355)
% 0.19/0.53  |- ~ssPv1 $_368 \/ ~ssPv3 $_370 \/ ~ssPv4 (skf1 $_368) \/
% 0.19/0.53     ~ssRr $_368 $_370 \/ ~ssRr $_368 $_371 \/ ssPv4 $_371
% 0.19/0.53  |- ~ssPv1 $_368 \/ ~ssPv3 (skf1 $_368) \/ ~ssPv4 $_369 \/
% 0.19/0.53     ~ssRr $_368 $_369 \/ ~ssRr $_368 $_371 \/ ssPv4 $_371
% 0.19/0.53  |- ~ssPv1 $_368 \/ ~ssPv3 $_370 \/ ~ssPv4 $_369 \/ ~ssRr $_368 $_369 \/
% 0.19/0.53     ~ssRr $_368 $_370 \/ ssPv4 (skf1 $_368)
% 0.19/0.53  |- ~ssPv1 $_381 \/ ~ssPv1 $_383 \/ ~ssPv2 (skf1 $_381) \/
% 0.19/0.53     ~ssRr $_381 $_383 \/ ~ssRr $_381 $_384 \/ ssPv1 $_384
% 0.19/0.53  |- ~ssPv1 $_381 \/ ~ssPv1 (skf1 $_381) \/ ~ssPv2 $_382 \/
% 0.19/0.53     ~ssRr $_381 $_382 \/ ~ssRr $_381 $_384 \/ ssPv1 $_384
% 0.19/0.53  |- ~ssPv1 $_381 \/ ~ssPv1 $_383 \/ ~ssPv2 $_382 \/ ~ssRr $_381 $_382 \/
% 0.19/0.53     ~ssRr $_381 $_383 \/ ssPv1 (skf1 $_381)
% 0.19/0.53  |- ~ssPv1 $_396 \/ ~ssPv2 $_394 \/ ~ssPv2 (skf1 $_394) \/
% 0.19/0.53     ~ssRr $_394 $_396 \/ ~ssRr $_394 $_397 \/ ssPv4 $_397
% 0.19/0.53  |- ~ssPv1 (skf1 $_394) \/ ~ssPv2 $_394 \/ ~ssPv2 $_395 \/
% 0.19/0.53     ~ssRr $_394 $_395 \/ ~ssRr $_394 $_397 \/ ssPv4 $_397
% 0.19/0.53  |- ~ssPv1 $_396 \/ ~ssPv2 $_394 \/ ~ssPv2 $_395 \/ ~ssRr $_394 $_395 \/
% 0.19/0.53     ~ssRr $_394 $_396 \/ ssPv4 (skf1 $_394)
% 0.19/0.53  SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.53  
%------------------------------------------------------------------------------