Metis---2.4.SAT-Sat.s

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

% Computer : n025.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 : Mon Jul 18 03:14:12 EDT 2022

% Result   : Satisfiable 0.17s 0.41s
% Output   : Saturation 0.17s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11  % Problem  : NLP044-1 : TPTP v8.1.0. Released v2.4.0.
% 0.11/0.12  % Command  : metis --show proof --show saturation %s
% 0.12/0.32  % Computer : n025.cluster.edu
% 0.12/0.32  % Model    : x86_64 x86_64
% 0.12/0.32  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32  % Memory   : 8042.1875MB
% 0.12/0.32  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32  % CPULimit : 300
% 0.12/0.32  % WCLimit  : 600
% 0.12/0.32  % DateTime : Fri Jul  1 02:52:53 EDT 2022
% 0.12/0.32  % CPUTime  : 
% 0.12/0.32  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.17/0.41  % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.41  
% 0.17/0.41  SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.41  |- actual_world skc33
% 0.17/0.41  |- actual_world skc12
% 0.17/0.41  |- group skc33 skc34 \/ ssSkC0
% 0.17/0.41  |- five skc33 skc34 \/ ssSkC0
% 0.17/0.41  |- nonhuman skc33 skc37 \/ ssSkC0
% 0.17/0.41  |- mia_forename skc33 skc37 \/ ssSkC0
% 0.17/0.41  |- forename skc33 skc37 \/ ssSkC0
% 0.17/0.41  |- ssSkC0 \/ woman skc33 skc38
% 0.17/0.41  |- event skc33 skc35 \/ ssSkC0
% 0.17/0.41  |- past skc33 skc35 \/ ssSkC0
% 0.17/0.41  |- nonreflexive skc33 skc35 \/ ssSkC0
% 0.17/0.41  |- order skc33 skc35 \/ ssSkC0
% 0.17/0.41  |- shake_beverage skc33 skc36 \/ ssSkC0
% 0.17/0.41  |- ~ssSkC0 \/ group skc12 skc13
% 0.17/0.41  |- ~ssSkC0 \/ five skc12 skc13
% 0.17/0.41  |- ~ssSkC0 \/ mia_forename skc12 skc16
% 0.17/0.41  |- ~ssSkC0 \/ forename skc12 skc16
% 0.17/0.41  |- ~ssSkC0 \/ woman skc12 skc17
% 0.17/0.41  |- ~ssSkC0 \/ nonhuman skc12 skc14
% 0.17/0.41  |- ~ssSkC0 \/ event skc12 skc14
% 0.17/0.41  |- ~ssSkC0 \/ past skc12 skc14
% 0.17/0.41  |- ~ssSkC0 \/ nonreflexive skc12 skc14
% 0.17/0.41  |- ~ssSkC0 \/ order skc12 skc14
% 0.17/0.41  |- ~ssSkC0 \/ shake_beverage skc12 skc15
% 0.17/0.41  |- ssSkC0 \/ ssSkP0 skc37 skc34 skc33
% 0.17/0.41  |- agent skc33 skc35 skc38 \/ ssSkC0
% 0.17/0.41  |- of skc33 skc37 skc38 \/ ssSkC0
% 0.17/0.41  |- patient skc33 skc35 skc36 \/ ssSkC0
% 0.17/0.41  |- ~ssSkC0 \/ agent skc12 skc14 skc17
% 0.17/0.41  |- ~ssSkC0 \/ of skc12 skc16 skc17
% 0.17/0.41  |- ~ssSkC0 \/ ssSkP0 skc14 skc13 skc12
% 0.17/0.41  |- ~ssSkC0 \/ patient skc12 skc14 skc15
% 0.17/0.41  |- ~member skc33 $U skc34 \/ dollar skc33 $U \/ ssSkC0
% 0.17/0.41  |- ~member skc12 $U skc13 \/ ~ssSkC0 \/ dollar skc12 $U
% 0.17/0.41  |- member $W (skf8 $U $W $V) $V \/ ssSkP0 $U $V $W
% 0.17/0.41  |- ~member $U $V $W \/ ~ssSkP0 $X $W $U \/ event $U (skf6 $U $Y $Z)
% 0.17/0.41  |- ~member $U $V $W \/ ~ssSkP0 $X $W $U \/ present $U (skf6 $U $Y $Z)
% 0.17/0.41  |- ~member $U $V $W \/ ~ssSkP0 $X $W $U \/ nonreflexive $U (skf6 $U $Y $Z)
% 0.17/0.41  |- ~member $U $V $W \/ ~ssSkP0 $X $W $U \/ cost $U (skf6 $U $Y $Z)
% 0.17/0.41  |- ~member $U $V $W \/ ~ssSkP0 $X $W $U \/ agent $U (skf6 $U $V $X) $X
% 0.17/0.41  |- ~member $U $V $W \/ ~ssSkP0 $X $W $U \/ patient $U (skf6 $U $V $Y) $V
% 0.17/0.41  |- ~agent $U $V $W \/ ~cost $U $V \/ ~event $U $V \/ ~nonreflexive $U $V \/
% 0.17/0.41     ~patient $U $V (skf8 $W $U $X) \/ ~present $U $V \/ ssSkP0 $W $Y $U
% 0.17/0.41  |- ~actual_world $U \/ ~agent $U $X $Y \/ ~event $U $X \/ ~five $U $V \/
% 0.17/0.41     ~forename $U $W \/ ~group $U $V \/ ~mia_forename $U $W \/
% 0.17/0.41     ~nonhuman $U $X \/ ~nonreflexive $U $X \/ ~of $U $W $Y \/
% 0.17/0.41     ~order $U $X \/ ~past $U $X \/ ~patient $U $X $Z \/
% 0.17/0.41     ~shake_beverage $U $Z \/ ~ssSkP0 $X $V $U \/ ~woman $U $Y \/
% 0.17/0.41     member $U (skf10 $U $V) $V \/ ssSkC0
% 0.17/0.41  |- ~actual_world $U \/ ~agent $U $Y $Z \/ ~dollar $U (skf10 $U $V) \/
% 0.17/0.41     ~event $U $Y \/ ~five $U $W \/ ~forename $U $X \/ ~group $U $W \/
% 0.17/0.41     ~mia_forename $U $X \/ ~nonhuman $U $Y \/ ~nonreflexive $U $Y \/
% 0.17/0.41     ~of $U $X $Z \/ ~order $U $Y \/ ~past $U $Y \/ ~patient $U $Y $X1 \/
% 0.17/0.41     ~shake_beverage $U $X1 \/ ~ssSkP0 $Y $W $U \/ ~woman $U $Z \/ ssSkC0
% 0.17/0.41  |- ~actual_world $U \/ ~agent $U $X $Y \/ ~event $U $X \/ ~five $U $V \/
% 0.17/0.41     ~forename $U $W \/ ~group $U $V \/ ~mia_forename $U $W \/
% 0.17/0.41     ~nonhuman $U $W \/ ~nonreflexive $U $X \/ ~of $U $W $Y \/
% 0.17/0.41     ~order $U $X \/ ~past $U $X \/ ~patient $U $X $Z \/
% 0.17/0.41     ~shake_beverage $U $Z \/ ~ssSkC0 \/ ~ssSkP0 $W $V $U \/ ~woman $U $Y \/
% 0.17/0.41     member $U (skf5 $U $V) $V
% 0.17/0.41  |- ~actual_world $U \/ ~agent $U $Y $Z \/ ~dollar $U (skf5 $U $V) \/
% 0.17/0.41     ~event $U $Y \/ ~five $U $W \/ ~forename $U $X \/ ~group $U $W \/
% 0.17/0.41     ~mia_forename $U $X \/ ~nonhuman $U $X \/ ~nonreflexive $U $Y \/
% 0.17/0.41     ~of $U $X $Z \/ ~order $U $Y \/ ~past $U $Y \/ ~patient $U $Y $X1 \/
% 0.17/0.41     ~shake_beverage $U $X1 \/ ~ssSkC0 \/ ~ssSkP0 $X $W $U \/ ~woman $U $Z
% 0.17/0.41  |- ~ssSkC0 \/ dollar skc12 (skf8 $_2 skc12 skc13) \/ ssSkP0 $_2 skc13 skc12
% 0.17/0.41  |- dollar skc33 (skf8 $_2 skc33 skc34) \/ ssSkC0 \/ ssSkP0 $_2 skc34 skc33
% 0.17/0.41  |- ~ssSkP0 $_10 $_9 $_7 \/
% 0.17/0.41     agent $_7 (skf6 $_7 (skf8 $U $_7 $_9) $_10) $_10 \/ ssSkP0 $U $_9 $_7
% 0.17/0.41  |- ~member skc33 $_8 skc34 \/ agent skc33 (skf6 skc33 $_8 skc37) skc37 \/
% 0.17/0.41     ssSkC0
% 0.17/0.41  |- agent skc33 (skf6 skc33 (skf8 $U skc33 skc34) skc37) skc37 \/ ssSkC0 \/
% 0.17/0.41     ssSkP0 $U skc34 skc33
% 0.17/0.41  |- ~ssSkP0 $_16 $_15 $_13 \/
% 0.17/0.41     patient $_13 (skf6 $_13 (skf8 $U $_13 $_15) $_17) (skf8 $U $_13 $_15) \/
% 0.17/0.41     ssSkP0 $U $_15 $_13
% 0.17/0.41  |- ~member skc33 $_14 skc34 \/ patient skc33 (skf6 skc33 $_14 $_17) $_14 \/
% 0.17/0.41     ssSkC0
% 0.17/0.41  |- patient skc33 (skf6 skc33 (skf8 $U skc33 skc34) $_19)
% 0.17/0.41       (skf8 $U skc33 skc34) \/ ssSkC0 \/ ssSkP0 $U skc34 skc33
% 0.17/0.41  |- ~ssSkP0 $_25 $_24 $_22 \/ event $_22 (skf6 $_22 $_26 $_27) \/
% 0.17/0.41     ssSkP0 $U $_24 $_22
% 0.17/0.41  |- ~member skc33 $_23 skc34 \/ event skc33 (skf6 skc33 $_26 $_27) \/ ssSkC0
% 0.17/0.41  |- event skc33 (skf6 skc33 $_29 $_30) \/ ssSkC0 \/ ssSkP0 $U skc34 skc33
% 0.17/0.41  |- ~ssSkP0 $_37 $_36 $_34 \/ present $_34 (skf6 $_34 $_38 $_39) \/
% 0.17/0.41     ssSkP0 $U $_36 $_34
% 0.17/0.41  |- ~member skc33 $_35 skc34 \/ present skc33 (skf6 skc33 $_38 $_39) \/
% 0.17/0.41     ssSkC0
% 0.17/0.41  |- present skc33 (skf6 skc33 $_41 $_42) \/ ssSkC0 \/ ssSkP0 $U skc34 skc33
% 0.17/0.41  |- ~ssSkP0 $_49 $_48 $_46 \/ nonreflexive $_46 (skf6 $_46 $_50 $_51) \/
% 0.17/0.41     ssSkP0 $U $_48 $_46
% 0.17/0.41  |- ~member skc33 $_47 skc34 \/ nonreflexive skc33 (skf6 skc33 $_50 $_51) \/
% 0.17/0.41     ssSkC0
% 0.17/0.41  |- nonreflexive skc33 (skf6 skc33 $_53 $_54) \/ ssSkC0 \/
% 0.17/0.41     ssSkP0 $U skc34 skc33
% 0.17/0.41  |- ~ssSkP0 $_67 $_66 $_64 \/ cost $_64 (skf6 $_64 $_68 $_69) \/
% 0.17/0.41     ssSkP0 $U $_66 $_64
% 0.17/0.41  |- ~member skc33 $_65 skc34 \/ cost skc33 (skf6 skc33 $_68 $_69) \/ ssSkC0
% 0.17/0.41  |- cost skc33 (skf6 skc33 $_71 $_72) \/ ssSkC0 \/ ssSkP0 $U skc34 skc33
% 0.17/0.41  |- ~agent skc33 (skf6 skc33 (skf8 $_105 skc33 skc34) $_19) $_105 \/
% 0.17/0.41     ~cost skc33 (skf6 skc33 (skf8 $_105 skc33 skc34) $_19) \/
% 0.17/0.41     ~event skc33 (skf6 skc33 (skf8 $_105 skc33 skc34) $_19) \/
% 0.17/0.41     ~nonreflexive skc33 (skf6 skc33 (skf8 $_105 skc33 skc34) $_19) \/
% 0.17/0.41     ~present skc33 (skf6 skc33 (skf8 $_105 skc33 skc34) $_19) \/ ssSkC0 \/
% 0.17/0.41     ssSkP0 $_105 $_107 skc33 \/ ssSkP0 $_105 skc34 skc33
% 0.17/0.42  |- ~agent skc33 (skf6 skc33 (skf8 $U skc33 skc34) $_19) $_121 \/
% 0.17/0.42     ~event skc33 (skf6 skc33 (skf8 $U skc33 skc34) $_19) \/
% 0.17/0.42     ~five skc33 $_118 \/ ~forename skc33 $_119 \/ ~group skc33 $_118 \/
% 0.17/0.42     ~mia_forename skc33 $_119 \/
% 0.17/0.42     ~nonhuman skc33 (skf6 skc33 (skf8 $U skc33 skc34) $_19) \/
% 0.17/0.42     ~nonreflexive skc33 (skf6 skc33 (skf8 $U skc33 skc34) $_19) \/
% 0.17/0.42     ~of skc33 $_119 $_121 \/
% 0.17/0.42     ~order skc33 (skf6 skc33 (skf8 $U skc33 skc34) $_19) \/
% 0.17/0.42     ~past skc33 (skf6 skc33 (skf8 $U skc33 skc34) $_19) \/
% 0.17/0.42     ~shake_beverage skc33 (skf8 $U skc33 skc34) \/
% 0.17/0.42     ~ssSkP0 (skf6 skc33 (skf8 $U skc33 skc34) $_19) $_118 skc33 \/
% 0.17/0.42     ~woman skc33 $_121 \/ member skc33 (skf10 skc33 $_118) $_118 \/
% 0.17/0.42     ssSkC0 \/ ssSkP0 $U skc34 skc33
% 0.17/0.42  |- ~agent skc33 skc37 $_121 \/ ~event skc33 skc37 \/ ~five skc33 skc34 \/
% 0.17/0.42     ~forename skc33 $_119 \/ ~group skc33 skc34 \/
% 0.17/0.42     ~mia_forename skc33 $_119 \/ ~nonhuman skc33 skc37 \/
% 0.17/0.42     ~nonreflexive skc33 skc37 \/ ~of skc33 $_119 $_121 \/
% 0.17/0.42     ~order skc33 skc37 \/ ~past skc33 skc37 \/ ~patient skc33 skc37 $_122 \/
% 0.17/0.42     ~shake_beverage skc33 $_122 \/ ~woman skc33 $_121 \/
% 0.17/0.42     member skc33 (skf10 skc33 skc34) skc34 \/ ssSkC0
% 0.17/0.42  |- ~agent skc33 $_120 $_121 \/ ~event skc33 $_120 \/ ~five skc33 skc34 \/
% 0.17/0.42     ~forename skc33 $_119 \/ ~group skc33 skc34 \/
% 0.17/0.42     ~mia_forename skc33 $_119 \/ ~nonhuman skc33 $_120 \/
% 0.17/0.42     ~nonreflexive skc33 $_120 \/ ~of skc33 $_119 $_121 \/
% 0.17/0.42     ~order skc33 $_120 \/ ~past skc33 $_120 \/ ~patient skc33 $_120 $_122 \/
% 0.17/0.42     ~shake_beverage skc33 $_122 \/ ~woman skc33 $_121 \/
% 0.17/0.42     cost skc33 (skf6 skc33 $_71 $_72) \/
% 0.17/0.42     member skc33 (skf10 skc33 skc34) skc34 \/ ssSkC0
% 0.17/0.42  |- ~agent skc33 $_120 $_121 \/ ~event skc33 $_120 \/ ~five skc33 skc34 \/
% 0.17/0.42     ~forename skc33 $_119 \/ ~group skc33 skc34 \/
% 0.17/0.42     ~mia_forename skc33 $_119 \/ ~nonhuman skc33 $_120 \/
% 0.17/0.42     ~nonreflexive skc33 $_120 \/ ~of skc33 $_119 $_121 \/
% 0.17/0.42     ~order skc33 $_120 \/ ~past skc33 $_120 \/ ~patient skc33 $_120 $_122 \/
% 0.17/0.42     ~shake_beverage skc33 $_122 \/ ~woman skc33 $_121 \/
% 0.17/0.42     member skc33 (skf10 skc33 skc34) skc34 \/
% 0.17/0.42     nonreflexive skc33 (skf6 skc33 $_53 $_54) \/ ssSkC0
% 0.17/0.42  |- ~agent skc33 $_120 $_121 \/ ~event skc33 $_120 \/ ~five skc33 skc34 \/
% 0.17/0.42     ~forename skc33 $_119 \/ ~group skc33 skc34 \/
% 0.17/0.42     ~mia_forename skc33 $_119 \/ ~nonhuman skc33 $_120 \/
% 0.17/0.42     ~nonreflexive skc33 $_120 \/ ~of skc33 $_119 $_121 \/
% 0.17/0.42     ~order skc33 $_120 \/ ~past skc33 $_120 \/ ~patient skc33 $_120 $_122 \/
% 0.17/0.42     ~shake_beverage skc33 $_122 \/ ~woman skc33 $_121 \/
% 0.17/0.42     member skc33 (skf10 skc33 skc34) skc34 \/
% 0.17/0.42     present skc33 (skf6 skc33 $_41 $_42) \/ ssSkC0
% 0.17/0.42  |- ~agent skc33 $_120 $_121 \/ ~event skc33 $_120 \/ ~five skc33 skc34 \/
% 0.17/0.42     ~forename skc33 $_119 \/ ~group skc33 skc34 \/
% 0.17/0.42     ~mia_forename skc33 $_119 \/ ~nonhuman skc33 $_120 \/
% 0.17/0.42     ~nonreflexive skc33 $_120 \/ ~of skc33 $_119 $_121 \/
% 0.17/0.42     ~order skc33 $_120 \/ ~past skc33 $_120 \/ ~patient skc33 $_120 $_122 \/
% 0.17/0.42     ~shake_beverage skc33 $_122 \/ ~woman skc33 $_121 \/
% 0.17/0.42     event skc33 (skf6 skc33 $_29 $_30) \/
% 0.17/0.42     member skc33 (skf10 skc33 skc34) skc34 \/ ssSkC0
% 0.17/0.42  |- ~agent skc33 (skf6 skc33 (skf8 $U skc33 skc34) $_19) $_132 \/
% 0.17/0.42     ~dollar skc33 (skf10 skc33 $_127) \/
% 0.17/0.42     ~event skc33 (skf6 skc33 (skf8 $U skc33 skc34) $_19) \/
% 0.17/0.42     ~five skc33 $_128 \/ ~forename skc33 $_129 \/ ~group skc33 $_128 \/
% 0.17/0.42     ~mia_forename skc33 $_129 \/
% 0.17/0.42     ~nonhuman skc33 (skf6 skc33 (skf8 $U skc33 skc34) $_19) \/
% 0.17/0.42     ~nonreflexive skc33 (skf6 skc33 (skf8 $U skc33 skc34) $_19) \/
% 0.17/0.42     ~of skc33 $_129 $_132 \/
% 0.17/0.42     ~order skc33 (skf6 skc33 (skf8 $U skc33 skc34) $_19) \/
% 0.17/0.42     ~past skc33 (skf6 skc33 (skf8 $U skc33 skc34) $_19) \/
% 0.17/0.42     ~shake_beverage skc33 (skf8 $U skc33 skc34) \/
% 0.17/0.42     ~ssSkP0 (skf6 skc33 (skf8 $U skc33 skc34) $_19) $_128 skc33 \/
% 0.17/0.42     ~woman skc33 $_132 \/ ssSkC0 \/ ssSkP0 $U skc34 skc33
% 0.17/0.42  |- ~agent skc33 $_131 $_132 \/ ~dollar skc33 (skf10 skc33 $_127) \/
% 0.17/0.42     ~event skc33 $_131 \/ ~five skc33 skc34 \/ ~forename skc33 $_129 \/
% 0.17/0.42     ~group skc33 skc34 \/ ~mia_forename skc33 $_129 \/
% 0.17/0.42     ~nonhuman skc33 $_131 \/ ~nonreflexive skc33 $_131 \/
% 0.17/0.42     ~of skc33 $_129 $_132 \/ ~order skc33 $_131 \/ ~past skc33 $_131 \/
% 0.17/0.42     ~patient skc33 $_131 $_130 \/ ~shake_beverage skc33 $_130 \/
% 0.17/0.42     ~woman skc33 $_132 \/ cost skc33 (skf6 skc33 $_71 $_72) \/ ssSkC0
% 0.17/0.42  |- ~agent skc33 $_131 $_132 \/ ~dollar skc33 (skf10 skc33 $_127) \/
% 0.17/0.42     ~event skc33 $_131 \/ ~five skc33 skc34 \/ ~forename skc33 $_129 \/
% 0.17/0.42     ~group skc33 skc34 \/ ~mia_forename skc33 $_129 \/
% 0.17/0.42     ~nonhuman skc33 $_131 \/ ~nonreflexive skc33 $_131 \/
% 0.17/0.42     ~of skc33 $_129 $_132 \/ ~order skc33 $_131 \/ ~past skc33 $_131 \/
% 0.17/0.42     ~patient skc33 $_131 $_130 \/ ~shake_beverage skc33 $_130 \/
% 0.17/0.42     ~woman skc33 $_132 \/ nonreflexive skc33 (skf6 skc33 $_53 $_54) \/
% 0.17/0.42     ssSkC0
% 0.17/0.42  |- ~agent skc33 $_131 $_132 \/ ~dollar skc33 (skf10 skc33 $_127) \/
% 0.17/0.42     ~event skc33 $_131 \/ ~five skc33 skc34 \/ ~forename skc33 $_129 \/
% 0.17/0.42     ~group skc33 skc34 \/ ~mia_forename skc33 $_129 \/
% 0.17/0.42     ~nonhuman skc33 $_131 \/ ~nonreflexive skc33 $_131 \/
% 0.17/0.42     ~of skc33 $_129 $_132 \/ ~order skc33 $_131 \/ ~past skc33 $_131 \/
% 0.17/0.42     ~patient skc33 $_131 $_130 \/ ~shake_beverage skc33 $_130 \/
% 0.17/0.42     ~woman skc33 $_132 \/ present skc33 (skf6 skc33 $_41 $_42) \/ ssSkC0
% 0.17/0.42  |- ~agent skc33 $_131 $_132 \/ ~dollar skc33 (skf10 skc33 $_127) \/
% 0.17/0.42     ~event skc33 $_131 \/ ~five skc33 skc34 \/ ~forename skc33 $_129 \/
% 0.17/0.42     ~group skc33 skc34 \/ ~mia_forename skc33 $_129 \/
% 0.17/0.42     ~nonhuman skc33 $_131 \/ ~nonreflexive skc33 $_131 \/
% 0.17/0.42     ~of skc33 $_129 $_132 \/ ~order skc33 $_131 \/ ~past skc33 $_131 \/
% 0.17/0.42     ~patient skc33 $_131 $_130 \/ ~shake_beverage skc33 $_130 \/
% 0.17/0.42     ~woman skc33 $_132 \/ event skc33 (skf6 skc33 $_29 $_30) \/ ssSkC0
% 0.17/0.42  |- ~agent skc33 skc35 $_142 \/ ~event skc33 skc35 \/ ~five skc33 skc34 \/
% 0.17/0.42     ~forename skc33 $_140 \/ ~group skc33 skc34 \/
% 0.17/0.42     ~mia_forename skc33 $_140 \/ ~nonhuman skc33 skc35 \/
% 0.17/0.42     ~nonreflexive skc33 skc35 \/ ~of skc33 $_140 $_142 \/
% 0.17/0.42     ~order skc33 skc35 \/ ~past skc33 skc35 \/
% 0.17/0.42     ~shake_beverage skc33 skc36 \/ ~woman skc33 $_142 \/
% 0.17/0.42     event skc33 (skf6 skc33 $_144 $_145) \/
% 0.17/0.42     member skc33 (skf10 skc33 skc34) skc34 \/ ssSkC0
% 0.17/0.42  |- ~event skc33 skc35 \/ ~five skc33 skc34 \/ ~forename skc33 skc37 \/
% 0.17/0.42     ~group skc33 skc34 \/ ~mia_forename skc33 skc37 \/
% 0.17/0.42     ~nonhuman skc33 skc35 \/ event skc33 (skf6 skc33 $_160 $_161) \/
% 0.17/0.42     member skc33 (skf10 skc33 skc34) skc34 \/ ssSkC0
% 0.17/0.42  |- ~agent skc33 skc35 $_166 \/ ~event skc33 skc35 \/ ~five skc33 skc34 \/
% 0.17/0.42     ~forename skc33 $_164 \/ ~group skc33 skc34 \/
% 0.17/0.42     ~mia_forename skc33 $_164 \/ ~nonhuman skc33 skc35 \/
% 0.17/0.42     ~nonreflexive skc33 skc35 \/ ~of skc33 $_164 $_166 \/
% 0.17/0.42     ~order skc33 skc35 \/ ~past skc33 skc35 \/
% 0.17/0.42     ~shake_beverage skc33 skc36 \/ ~woman skc33 $_166 \/
% 0.17/0.42     member skc33 (skf10 skc33 skc34) skc34 \/
% 0.17/0.42     present skc33 (skf6 skc33 $_168 $_169) \/ ssSkC0
% 0.17/0.42  |- ~event skc33 skc35 \/ ~five skc33 skc34 \/ ~forename skc33 skc37 \/
% 0.17/0.42     ~group skc33 skc34 \/ ~mia_forename skc33 skc37 \/
% 0.17/0.42     ~nonhuman skc33 skc35 \/ member skc33 (skf10 skc33 skc34) skc34 \/
% 0.17/0.42     present skc33 (skf6 skc33 $_184 $_185) \/ ssSkC0
% 0.17/0.42  |- ~agent skc33 skc35 $_190 \/ ~event skc33 skc35 \/ ~five skc33 skc34 \/
% 0.17/0.42     ~forename skc33 $_188 \/ ~group skc33 skc34 \/
% 0.17/0.42     ~mia_forename skc33 $_188 \/ ~nonhuman skc33 skc35 \/
% 0.17/0.42     ~nonreflexive skc33 skc35 \/ ~of skc33 $_188 $_190 \/
% 0.17/0.42     ~order skc33 skc35 \/ ~past skc33 skc35 \/
% 0.17/0.42     ~shake_beverage skc33 skc36 \/ ~woman skc33 $_190 \/
% 0.17/0.42     member skc33 (skf10 skc33 skc34) skc34 \/
% 0.17/0.42     nonreflexive skc33 (skf6 skc33 $_192 $_193) \/ ssSkC0
% 0.17/0.42  |- ~event skc33 skc35 \/ ~five skc33 skc34 \/ ~forename skc33 skc37 \/
% 0.17/0.42     ~group skc33 skc34 \/ ~mia_forename skc33 skc37 \/
% 0.17/0.42     ~nonhuman skc33 skc35 \/ member skc33 (skf10 skc33 skc34) skc34 \/
% 0.17/0.42     nonreflexive skc33 (skf6 skc33 $_208 $_209) \/ ssSkC0
% 0.17/0.42  |- ~agent skc33 skc35 $_214 \/ ~event skc33 skc35 \/ ~five skc33 skc34 \/
% 0.17/0.42     ~forename skc33 $_212 \/ ~group skc33 skc34 \/
% 0.17/0.42     ~mia_forename skc33 $_212 \/ ~nonhuman skc33 skc35 \/
% 0.17/0.42     ~nonreflexive skc33 skc35 \/ ~of skc33 $_212 $_214 \/
% 0.17/0.42     ~order skc33 skc35 \/ ~past skc33 skc35 \/
% 0.17/0.42     ~shake_beverage skc33 skc36 \/ ~woman skc33 $_214 \/
% 0.17/0.42     cost skc33 (skf6 skc33 $_216 $_217) \/
% 0.17/0.42     member skc33 (skf10 skc33 skc34) skc34 \/ ssSkC0
% 0.17/0.42  |- ~event skc33 skc35 \/ ~five skc33 skc34 \/ ~forename skc33 skc37 \/
% 0.17/0.42     ~group skc33 skc34 \/ ~mia_forename skc33 skc37 \/
% 0.17/0.42     ~nonhuman skc33 skc35 \/ cost skc33 (skf6 skc33 $_232 $_233) \/
% 0.17/0.42     member skc33 (skf10 skc33 skc34) skc34 \/ ssSkC0
% 0.17/0.42  SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.42  
%------------------------------------------------------------------------------