↑ Up

Metis---2.4.SAT-Sat.s

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

% Computer : n012.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:16:16 EDT 2022

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

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12  % Problem  : NLP224-1 : TPTP v8.1.0. Released v2.4.0.
% 0.10/0.13  % Command  : metis --show proof --show saturation %s
% 0.13/0.33  % Computer : n012.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 : Thu Jun 30 18:56:18 EDT 2022
% 0.13/0.34  % CPUTime  : 
% 0.13/0.34  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.19/0.44  % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.44  
% 0.19/0.44  SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.44  |- ~state $U $V \/ eventuality $U $V
% 0.19/0.44  |- ~eventuality $U $V \/ thing $U $V
% 0.19/0.44  |- ~thing $U $V \/ singleton $U $V
% 0.19/0.44  |- ~eventuality $U $V \/ specific $U $V
% 0.19/0.44  |- ~eventuality $U $V \/ nonexistent $U $V
% 0.19/0.44  |- ~eventuality $U $V \/ unisex $U $V
% 0.19/0.44  |- ~state $U $V \/ event $U $V
% 0.19/0.44  |- ~event $U $V \/ eventuality $U $V
% 0.19/0.44  |- ~man $U $V \/ human_person $U $V
% 0.19/0.44  |- ~human_person $U $V \/ organism $U $V
% 0.19/0.44  |- ~organism $U $V \/ entity $U $V
% 0.19/0.44  |- ~entity $U $V \/ thing $U $V
% 0.19/0.44  |- ~entity $U $V \/ specific $U $V
% 0.19/0.44  |- ~entity $U $V \/ existent $U $V
% 0.19/0.44  |- ~organism $U $V \/ impartial $U $V
% 0.19/0.44  |- ~organism $U $V \/ living $U $V
% 0.19/0.44  |- ~human_person $U $V \/ human $U $V
% 0.19/0.44  |- ~human_person $U $V \/ animate $U $V
% 0.19/0.44  |- ~man $U $V \/ male $U $V
% 0.19/0.44  |- ~forename $U $V \/ relname $U $V
% 0.19/0.44  |- ~relname $U $V \/ relation $U $V
% 0.19/0.44  |- ~relation $U $V \/ abstraction $U $V
% 0.19/0.44  |- ~abstraction $U $V \/ thing $U $V
% 0.19/0.44  |- ~abstraction $U $V \/ nonhuman $U $V
% 0.19/0.44  |- ~abstraction $U $V \/ general $U $V
% 0.19/0.44  |- ~abstraction $U $V \/ unisex $U $V
% 0.19/0.44  |- ~jules_forename $U $V \/ forename $U $V
% 0.19/0.44  |- ~smoke $U $V \/ event $U $V
% 0.19/0.44  |- ~proposition $U $V \/ relation $U $V
% 0.19/0.44  |- ~vincent_forename $U $V \/ forename $U $V
% 0.19/0.44  |- ~male $U $V \/ ~unisex $U $V
% 0.19/0.44  |- ~general $U $V \/ ~specific $U $V
% 0.19/0.44  |- ~human $U $V \/ ~nonhuman $U $V
% 0.19/0.44  |- ~existent $U $V \/ ~nonexistent $U $V
% 0.19/0.44  |- ~be $U $V $W $X \/ $W = $X
% 0.19/0.44  |- ~accessible_world $U $V \/ ~state $U $W \/ state $V $W
% 0.19/0.44  |- ~accessible_world $U $V \/ ~eventuality $U $W \/ eventuality $V $W
% 0.19/0.44  |- ~accessible_world $U $V \/ ~thing $U $W \/ thing $V $W
% 0.19/0.44  |- ~accessible_world $U $V \/ ~singleton $U $W \/ singleton $V $W
% 0.19/0.44  |- ~accessible_world $U $V \/ ~specific $U $W \/ specific $V $W
% 0.19/0.44  |- ~accessible_world $U $V \/ ~nonexistent $U $W \/ nonexistent $V $W
% 0.19/0.44  |- ~accessible_world $U $V \/ ~unisex $U $W \/ unisex $V $W
% 0.19/0.44  |- ~accessible_world $U $V \/ ~event $U $W \/ event $V $W
% 0.19/0.44  |- ~accessible_world $U $V \/ ~man $U $W \/ man $V $W
% 0.19/0.44  |- ~accessible_world $U $V \/ ~human_person $U $W \/ human_person $V $W
% 0.19/0.44  |- ~accessible_world $U $V \/ ~organism $U $W \/ organism $V $W
% 0.19/0.44  |- ~accessible_world $U $V \/ ~entity $U $W \/ entity $V $W
% 0.19/0.44  |- ~accessible_world $U $V \/ ~existent $U $W \/ existent $V $W
% 0.19/0.44  |- ~accessible_world $U $V \/ ~impartial $U $W \/ impartial $V $W
% 0.19/0.44  |- ~accessible_world $U $V \/ ~living $U $W \/ living $V $W
% 0.19/0.44  |- ~accessible_world $U $V \/ ~human $U $W \/ human $V $W
% 0.19/0.44  |- ~accessible_world $U $V \/ ~animate $U $W \/ animate $V $W
% 0.19/0.44  |- ~accessible_world $U $V \/ ~male $U $W \/ male $V $W
% 0.19/0.44  |- ~accessible_world $U $V \/ ~forename $U $W \/ forename $V $W
% 0.19/0.44  |- ~accessible_world $U $V \/ ~relname $U $W \/ relname $V $W
% 0.19/0.44  |- ~accessible_world $U $V \/ ~relation $U $W \/ relation $V $W
% 0.19/0.44  |- ~abstraction $U $W \/ ~accessible_world $U $V \/ abstraction $V $W
% 0.19/0.44  |- ~accessible_world $U $V \/ ~nonhuman $U $W \/ nonhuman $V $W
% 0.19/0.44  |- ~accessible_world $U $V \/ ~general $U $W \/ general $V $W
% 0.19/0.44  |- ~accessible_world $U $V \/ ~jules_forename $U $W \/ jules_forename $V $W
% 0.19/0.44  |- ~accessible_world $U $V \/ ~smoke $U $W \/ smoke $V $W
% 0.19/0.44  |- ~accessible_world $U $V \/ ~present $U $W \/ present $V $W
% 0.19/0.44  |- ~accessible_world $U $V \/ ~think_believe_consider $U $W \/
% 0.19/0.44     think_believe_consider $V $W
% 0.19/0.44  |- ~accessible_world $U $V \/ ~proposition $U $W \/ proposition $V $W
% 0.19/0.44  |- ~accessible_world $U $V \/ ~vincent_forename $U $W \/
% 0.19/0.44     vincent_forename $V $W
% 0.19/0.44  |- ~accessible_world $U $V \/ ~of $U $W $X \/ of $V $W $X
% 0.19/0.44  |- ~accessible_world $U $V \/ ~agent $U $W $X \/ agent $V $W $X
% 0.19/0.44  |- ~accessible_world $U $V \/ ~theme $U $W $X \/ theme $V $W $X
% 0.19/0.44  |- ~accessible_world $U $V \/ ~be $U $W $X $Y \/ be $V $W $X $Y
% 0.19/0.44  |- ~entity $U $X \/ ~forename $U $V \/ ~forename $U $W \/ ~of $U $V $X \/
% 0.19/0.44     ~of $U $W $X \/ $W = $V
% 0.19/0.44  |- ~agent $U $X $Z \/ ~agent $U $Y $Z \/ ~proposition $U $V \/
% 0.19/0.44     ~proposition $U $W \/ ~theme $U $X $V \/ ~theme $U $Y $W \/
% 0.19/0.44     ~think_believe_consider $U $X \/ ~think_believe_consider $U $Y \/
% 0.19/0.44     $V = $W
% 0.19/0.45  |- ~agent $U $Y $Z \/ ~proposition $U $V \/ ~proposition $U $W \/
% 0.19/0.45     ~theme $U $Y $V \/ ~theme $U $Y $W \/ ~think_believe_consider $U $Y \/
% 0.19/0.45     $V = $W
% 0.19/0.45  |- actual_world skc9
% 0.19/0.45  |- man skc9 skc17
% 0.19/0.45  |- forename skc9 skc16
% 0.19/0.45  |- vincent_forename skc9 skc16
% 0.19/0.45  |- event skc9 skc15
% 0.19/0.45  |- present skc9 skc15
% 0.19/0.45  |- think_believe_consider skc9 skc15
% 0.19/0.45  |- forename skc9 skc12
% 0.19/0.45  |- jules_forename skc9 skc12
% 0.19/0.45  |- man skc9 skc11
% 0.19/0.45  |- state skc9 skc10
% 0.19/0.45  |- accessible_world skc9 skc14
% 0.19/0.45  |- proposition skc9 skc14
% 0.19/0.45  |- of skc9 skc16 skc17
% 0.19/0.45  |- agent skc9 skc15 skc17
% 0.19/0.45  |- theme skc9 skc15 skc14
% 0.19/0.45  |- of skc9 skc12 skc11
% 0.19/0.45  |- be skc9 skc10 skc11 skc11
% 0.19/0.45  |- ~man skc14 $U \/ agent skc14 (skf1 $U) $U
% 0.19/0.45  |- eventuality skc9 skc10
% 0.19/0.45  |- thing skc9 skc10
% 0.19/0.45  |- singleton skc9 skc10
% 0.19/0.45  |- specific skc9 skc10
% 0.19/0.45  |- nonexistent skc9 skc10
% 0.19/0.45  |- unisex skc9 skc10
% 0.19/0.45  |- event skc9 skc10
% 0.19/0.45  |- eventuality skc9 skc15
% 0.19/0.45  |- unisex skc9 skc15
% 0.19/0.45  |- nonexistent skc9 skc15
% 0.19/0.45  |- specific skc9 skc15
% 0.19/0.45  |- thing skc9 skc15
% 0.19/0.45  |- singleton skc9 skc15
% 0.19/0.45  |- human_person skc9 skc11
% 0.19/0.45  |- human_person skc9 skc17
% 0.19/0.45  |- organism skc9 skc11
% 0.19/0.45  |- organism skc9 skc17
% 0.19/0.45  |- entity skc9 skc11
% 0.19/0.45  |- entity skc9 skc17
% 0.19/0.45  |- thing skc9 skc11
% 0.19/0.45  |- thing skc9 skc17
% 0.19/0.45  |- singleton skc9 skc11
% 0.19/0.45  |- singleton skc9 skc17
% 0.19/0.45  |- specific skc9 skc11
% 0.19/0.45  |- specific skc9 skc17
% 0.19/0.45  |- existent skc9 skc11
% 0.19/0.45  |- existent skc9 skc17
% 0.19/0.45  |- impartial skc9 skc11
% 0.19/0.45  |- impartial skc9 skc17
% 0.19/0.45  |- living skc9 skc11
% 0.19/0.45  |- living skc9 skc17
% 0.19/0.45  |- human skc9 skc11
% 0.19/0.45  |- human skc9 skc17
% 0.19/0.45  |- animate skc9 skc11
% 0.19/0.45  |- animate skc9 skc17
% 0.19/0.45  |- male skc9 skc11
% 0.19/0.45  |- male skc9 skc17
% 0.19/0.45  |- relname skc9 skc12
% 0.19/0.45  |- relname skc9 skc16
% 0.19/0.45  |- relation skc9 skc12
% 0.19/0.45  |- relation skc9 skc16
% 0.19/0.45  |- abstraction skc9 skc12
% 0.19/0.45  |- abstraction skc9 skc16
% 0.19/0.45  |- thing skc9 skc12
% 0.19/0.45  |- thing skc9 skc16
% 0.19/0.45  |- singleton skc9 skc16
% 0.19/0.45  |- singleton skc9 skc12
% 0.19/0.45  |- nonhuman skc9 skc12
% 0.19/0.45  |- nonhuman skc9 skc16
% 0.19/0.45  |- general skc9 skc12
% 0.19/0.45  |- general skc9 skc16
% 0.19/0.45  |- unisex skc9 skc12
% 0.19/0.45  |- unisex skc9 skc16
% 0.19/0.45  |- relation skc9 skc14
% 0.19/0.45  |- abstraction skc9 skc14
% 0.19/0.45  |- unisex skc9 skc14
% 0.19/0.45  |- general skc9 skc14
% 0.19/0.45  |- nonhuman skc9 skc14
% 0.19/0.45  |- thing skc9 skc14
% 0.19/0.45  |- singleton skc9 skc14
% 0.19/0.45  |- ~male skc9 skc10
% 0.19/0.45  |- ~male skc9 skc12
% 0.19/0.45  |- ~male skc9 skc14
% 0.19/0.45  |- ~male skc9 skc15
% 0.19/0.45  |- ~male skc9 skc16
% 0.19/0.45  |- ~general skc9 skc10
% 0.19/0.45  |- ~general skc9 skc11
% 0.19/0.45  |- ~general skc9 skc15
% 0.19/0.45  |- ~general skc9 skc17
% 0.19/0.45  |- ~human skc9 skc12
% 0.19/0.45  |- ~human skc9 skc14
% 0.19/0.45  |- ~human skc9 skc16
% 0.19/0.45  |- ~existent skc9 skc10
% 0.19/0.45  |- ~existent skc9 skc15
% 0.19/0.45  |- skc13 = skc11
% 0.19/0.45  |- ~accessible_world skc9 $_80 \/ state $_80 skc10
% 0.19/0.45  |- state skc14 skc10
% 0.19/0.45  |- ~accessible_world skc14 $V \/ state $V skc10
% 0.19/0.45  |- event skc14 skc10
% 0.19/0.45  |- eventuality skc14 skc10
% 0.19/0.45  |- unisex skc14 skc10
% 0.19/0.45  |- nonexistent skc14 skc10
% 0.19/0.45  |- specific skc14 skc10
% 0.19/0.45  |- thing skc14 skc10
% 0.19/0.45  |- ~male skc14 skc10
% 0.19/0.45  |- ~general skc14 skc10
% 0.19/0.45  |- ~existent skc14 skc10
% 0.19/0.45  |- singleton skc14 skc10
% 0.19/0.45  |- ~accessible_world skc14 $_85 \/ eventuality $_85 skc10
% 0.19/0.45  |- ~accessible_world skc9 $_85 \/ eventuality $_85 skc10
% 0.19/0.45  |- ~accessible_world skc9 $_85 \/ eventuality $_85 skc15
% 0.19/0.45  |- eventuality skc14 skc15
% 0.19/0.45  |- ~accessible_world skc14 $V \/ eventuality $V skc15
% 0.19/0.45  |- unisex skc14 skc15
% 0.19/0.45  |- nonexistent skc14 skc15
% 0.19/0.45  |- specific skc14 skc15
% 0.19/0.45  |- thing skc14 skc15
% 0.19/0.45  |- ~existent skc14 skc15
% 0.19/0.46  |- ~general skc14 skc15
% 0.19/0.46  |- singleton skc14 skc15
% 0.19/0.46  |- ~male skc14 skc15
% 0.19/0.46  |- ~accessible_world skc14 $_92 \/ thing $_92 skc10
% 0.19/0.46  |- ~accessible_world skc14 $_92 \/ thing $_92 skc15
% 0.19/0.46  |- ~accessible_world skc9 $_92 \/ thing $_92 skc10
% 0.19/0.46  |- ~accessible_world skc9 $_92 \/ thing $_92 skc11
% 0.19/0.46  |- ~accessible_world skc9 $_92 \/ thing $_92 skc12
% 0.19/0.46  |- ~accessible_world skc9 $_92 \/ thing $_92 skc14
% 0.19/0.46  |- ~accessible_world skc9 $_92 \/ thing $_92 skc15
% 0.19/0.46  |- ~accessible_world skc9 $_92 \/ thing $_92 skc16
% 0.19/0.46  |- ~accessible_world skc9 $_92 \/ thing $_92 skc17
% 0.19/0.46  |- thing skc14 skc12
% 0.19/0.46  |- ~accessible_world skc14 $V \/ thing $V skc12
% 0.19/0.46  |- singleton skc14 skc12
% 0.19/0.46  |- thing skc14 skc11
% 0.19/0.46  |- ~accessible_world skc14 $V \/ thing $V skc11
% 0.19/0.46  |- singleton skc14 skc11
% 0.19/0.46  |- thing skc14 skc14
% 0.19/0.46  |- ~accessible_world skc14 $V \/ thing $V skc14
% 0.19/0.46  |- singleton skc14 skc14
% 0.19/0.46  |- thing skc14 skc17
% 0.19/0.46  |- ~accessible_world skc14 $V \/ thing $V skc17
% 0.19/0.46  |- singleton skc14 skc17
% 0.19/0.46  |- thing skc14 skc16
% 0.19/0.46  |- ~accessible_world skc14 $V \/ thing $V skc16
% 0.19/0.46  |- singleton skc14 skc16
% 0.19/0.46  |- ~accessible_world skc14 $_109 \/ singleton $_109 skc10
% 0.19/0.46  |- ~accessible_world skc14 $_109 \/ singleton $_109 skc11
% 0.19/0.46  |- ~accessible_world skc14 $_109 \/ singleton $_109 skc12
% 0.19/0.46  |- ~accessible_world skc14 $_109 \/ singleton $_109 skc14
% 0.19/0.46  |- ~accessible_world skc14 $_109 \/ singleton $_109 skc15
% 0.19/0.46  |- ~accessible_world skc14 $_109 \/ singleton $_109 skc16
% 0.19/0.46  |- ~accessible_world skc14 $_109 \/ singleton $_109 skc17
% 0.19/0.46  |- ~accessible_world skc9 $_109 \/ singleton $_109 skc10
% 0.19/0.46  |- ~accessible_world skc9 $_109 \/ singleton $_109 skc11
% 0.19/0.46  |- ~accessible_world skc9 $_109 \/ singleton $_109 skc12
% 0.19/0.46  |- ~accessible_world skc9 $_109 \/ singleton $_109 skc14
% 0.19/0.46  |- ~accessible_world skc9 $_109 \/ singleton $_109 skc15
% 0.19/0.46  |- ~accessible_world skc9 $_109 \/ singleton $_109 skc16
% 0.19/0.46  |- ~accessible_world skc9 $_109 \/ singleton $_109 skc17
% 0.19/0.46  |- ~accessible_world skc14 $_126 \/ specific $_126 skc10
% 0.19/0.46  |- ~accessible_world skc14 $_126 \/ specific $_126 skc15
% 0.19/0.46  |- ~accessible_world skc9 $_126 \/ specific $_126 skc10
% 0.19/0.46  |- ~accessible_world skc9 $_126 \/ specific $_126 skc11
% 0.19/0.46  |- ~accessible_world skc9 $_126 \/ specific $_126 skc15
% 0.19/0.46  |- ~accessible_world skc9 $_126 \/ specific $_126 skc17
% 0.19/0.46  |- specific skc14 skc11
% 0.19/0.46  |- ~accessible_world skc14 $V \/ specific $V skc11
% 0.19/0.46  |- ~general skc14 skc11
% 0.19/0.46  |- specific skc14 skc17
% 0.19/0.46  |- ~accessible_world skc14 $V \/ specific $V skc17
% 0.19/0.46  |- ~general skc14 skc17
% 0.19/0.46  |- ~accessible_world skc14 $_137 \/ nonexistent $_137 skc10
% 0.19/0.46  |- ~accessible_world skc14 $_137 \/ nonexistent $_137 skc15
% 0.19/0.46  |- ~accessible_world skc9 $_137 \/ nonexistent $_137 skc10
% 0.19/0.46  |- ~accessible_world skc9 $_137 \/ nonexistent $_137 skc15
% 0.19/0.46  |- ~accessible_world skc14 $_144 \/ unisex $_144 skc10
% 0.19/0.46  |- ~accessible_world skc14 $_144 \/ unisex $_144 skc15
% 0.19/0.46  |- ~accessible_world skc9 $_144 \/ unisex $_144 skc10
% 0.19/0.46  |- ~accessible_world skc9 $_144 \/ unisex $_144 skc12
% 0.19/0.46  |- ~accessible_world skc9 $_144 \/ unisex $_144 skc14
% 0.19/0.46  |- ~accessible_world skc9 $_144 \/ unisex $_144 skc15
% 0.19/0.46  |- ~accessible_world skc9 $_144 \/ unisex $_144 skc16
% 0.19/0.46  |- unisex skc14 skc12
% 0.19/0.46  |- ~accessible_world skc14 $V \/ unisex $V skc12
% 0.19/0.46  |- ~male skc14 skc12
% 0.19/0.46  |- unisex skc14 skc14
% 0.19/0.46  |- ~accessible_world skc14 $V \/ unisex $V skc14
% 0.19/0.46  |- ~male skc14 skc14
% 0.19/0.46  |- unisex skc14 skc16
% 0.19/0.46  |- ~accessible_world skc14 $V \/ unisex $V skc16
% 0.19/0.46  |- ~male skc14 skc16
% 0.19/0.46  |- ~accessible_world skc14 $_157 \/ event $_157 skc10
% 0.19/0.46  |- ~accessible_world skc9 $_157 \/ event $_157 skc10
% 0.19/0.46  |- ~accessible_world skc9 $_157 \/ event $_157 skc15
% 0.19/0.46  |- event skc14 skc15
% 0.19/0.46  |- ~accessible_world skc14 $V \/ event $V skc15
% 0.19/0.46  |- ~accessible_world skc9 $_164 \/ man $_164 skc11
% 0.19/0.46  |- ~accessible_world skc9 $_164 \/ man $_164 skc17
% 0.19/0.46  |- man skc14 skc11
% 0.19/0.46  |- ~accessible_world skc14 $V \/ man $V skc11
% 0.19/0.46  |- male skc14 skc11
% 0.19/0.46  |- human_person skc14 skc11
% 0.19/0.46  |- event skc14 (skf1 $V)
% 0.19/0.46  |- smoke skc14 (skf1 $V)
% 0.19/0.46  |- agent skc14 (skf1 skc11) skc11
% 0.19/0.46  |- present skc14 (skf1 $V)
% 0.19/0.46  |- animate skc14 skc11
% 0.19/0.46  |- human skc14 skc11
% 0.19/0.46  |- organism skc14 skc11
% 0.19/0.46  |- living skc14 skc11
% 0.19/0.46  |- impartial skc14 skc11
% 0.19/0.46  |- entity skc14 skc11
% 0.19/0.46  |- existent skc14 skc11
% 0.19/0.46  |- ~accessible_world skc14 $V \/ event $V (skf1 $_168)
% 0.19/0.46  |- eventuality skc14 (skf1 $_168)
% 0.19/0.46  |- ~accessible_world skc14 $V \/ eventuality $V (skf1 $_169)
% 0.19/0.46  |- unisex skc14 (skf1 $_169)
% 0.19/0.46  |- nonexistent skc14 (skf1 $_169)
% 0.19/0.46  |- specific skc14 (skf1 $_169)
% 0.19/0.46  |- thing skc14 (skf1 $_169)
% 0.19/0.46  |- ~accessible_world skc14 $V \/ nonexistent $V (skf1 $_170)
% 0.19/0.46  |- ~existent skc14 (skf1 $_170)
% 0.19/0.46  |- ~accessible_world skc14 $V \/ unisex $V (skf1 $_172)
% 0.19/0.46  |- ~male skc14 (skf1 $_172)
% 0.19/0.46  |- ~accessible_world skc14 $V \/ thing $V (skf1 $_174)
% 0.19/0.46  |- singleton skc14 (skf1 $_174)
% 0.19/0.46  |- ~accessible_world skc14 $V \/ specific $V (skf1 $_175)
% 0.19/0.46  |- ~general skc14 (skf1 $_175)
% 0.19/0.46  |- ~accessible_world skc14 $V \/ singleton $V (skf1 $_177)
% 0.19/0.46  |- man skc14 skc17
% 0.19/0.46  |- ~accessible_world skc14 $V \/ man $V skc17
% 0.19/0.46  |- male skc14 skc17
% 0.19/0.46  |- human_person skc14 skc17
% 0.19/0.46  |- agent skc14 (skf1 skc17) skc17
% 0.19/0.46  |- animate skc14 skc17
% 0.19/0.46  |- human skc14 skc17
% 0.19/0.46  |- organism skc14 skc17
% 0.19/0.46  |- living skc14 skc17
% 0.19/0.46  |- impartial skc14 skc17
% 0.19/0.46  |- entity skc14 skc17
% 0.19/0.46  |- existent skc14 skc17
% 0.19/0.46  |- ~accessible_world skc14 $_197 \/ human_person $_197 skc11
% 0.19/0.46  |- ~accessible_world skc14 $_197 \/ human_person $_197 skc17
% 0.19/0.47  |- ~accessible_world skc9 $_197 \/ human_person $_197 skc11
% 0.19/0.47  |- ~accessible_world skc9 $_197 \/ human_person $_197 skc17
% 0.19/0.47  |- ~accessible_world skc14 $_204 \/ organism $_204 skc11
% 0.19/0.47  |- ~accessible_world skc14 $_204 \/ organism $_204 skc17
% 0.19/0.47  |- ~accessible_world skc9 $_204 \/ organism $_204 skc11
% 0.19/0.47  |- ~accessible_world skc9 $_204 \/ organism $_204 skc17
% 0.19/0.47  |- ~accessible_world skc14 $_211 \/ entity $_211 skc11
% 0.19/0.47  |- ~accessible_world skc14 $_211 \/ entity $_211 skc17
% 0.19/0.47  |- ~accessible_world skc9 $_211 \/ entity $_211 skc11
% 0.19/0.47  |- ~accessible_world skc9 $_211 \/ entity $_211 skc17
% 0.19/0.47  |- ~accessible_world skc14 $_218 \/ existent $_218 skc11
% 0.19/0.47  |- ~accessible_world skc14 $_218 \/ existent $_218 skc17
% 0.19/0.47  |- ~accessible_world skc9 $_218 \/ existent $_218 skc11
% 0.19/0.47  |- ~accessible_world skc9 $_218 \/ existent $_218 skc17
% 0.19/0.47  |- ~accessible_world skc14 $_225 \/ impartial $_225 skc11
% 0.19/0.47  |- ~accessible_world skc14 $_225 \/ impartial $_225 skc17
% 0.19/0.47  |- ~accessible_world skc9 $_225 \/ impartial $_225 skc11
% 0.19/0.47  |- ~accessible_world skc9 $_225 \/ impartial $_225 skc17
% 0.19/0.47  |- ~accessible_world skc14 $_232 \/ living $_232 skc11
% 0.19/0.47  |- ~accessible_world skc14 $_232 \/ living $_232 skc17
% 0.19/0.47  |- ~accessible_world skc9 $_232 \/ living $_232 skc11
% 0.19/0.47  |- ~accessible_world skc9 $_232 \/ living $_232 skc17
% 0.19/0.47  |- ~accessible_world skc14 $_239 \/ human $_239 skc11
% 0.19/0.47  |- ~accessible_world skc14 $_239 \/ human $_239 skc17
% 0.19/0.47  |- ~accessible_world skc9 $_239 \/ human $_239 skc11
% 0.19/0.47  |- ~accessible_world skc9 $_239 \/ human $_239 skc17
% 0.19/0.47  |- ~accessible_world skc14 $_246 \/ animate $_246 skc11
% 0.19/0.47  |- ~accessible_world skc14 $_246 \/ animate $_246 skc17
% 0.19/0.47  |- ~accessible_world skc9 $_246 \/ animate $_246 skc11
% 0.19/0.47  |- ~accessible_world skc9 $_246 \/ animate $_246 skc17
% 0.19/0.47  |- ~accessible_world skc14 $_253 \/ male $_253 skc11
% 0.19/0.47  |- ~accessible_world skc14 $_253 \/ male $_253 skc17
% 0.19/0.47  |- ~accessible_world skc9 $_253 \/ male $_253 skc11
% 0.19/0.47  |- ~accessible_world skc9 $_253 \/ male $_253 skc17
% 0.19/0.47  |- ~accessible_world skc9 $_260 \/ forename $_260 skc12
% 0.19/0.47  |- ~accessible_world skc9 $_260 \/ forename $_260 skc16
% 0.19/0.47  |- forename skc14 skc12
% 0.19/0.47  |- ~accessible_world skc14 $V \/ forename $V skc12
% 0.19/0.47  |- relname skc14 skc12
% 0.19/0.47  |- relation skc14 skc12
% 0.19/0.47  |- abstraction skc14 skc12
% 0.19/0.47  |- general skc14 skc12
% 0.19/0.47  |- nonhuman skc14 skc12
% 0.19/0.47  |- ~human skc14 skc12
% 0.19/0.47  |- forename skc14 skc16
% 0.19/0.47  |- ~accessible_world skc14 $V \/ forename $V skc16
% 0.19/0.47  |- relname skc14 skc16
% 0.19/0.47  |- relation skc14 skc16
% 0.19/0.47  |- abstraction skc14 skc16
% 0.19/0.47  |- general skc14 skc16
% 0.19/0.47  |- nonhuman skc14 skc16
% 0.19/0.47  |- ~human skc14 skc16
% 0.19/0.47  |- ~accessible_world skc14 $_267 \/ relname $_267 skc12
% 0.19/0.47  |- ~accessible_world skc14 $_267 \/ relname $_267 skc16
% 0.19/0.47  |- ~accessible_world skc9 $_267 \/ relname $_267 skc12
% 0.19/0.47  |- ~accessible_world skc9 $_267 \/ relname $_267 skc16
% 0.19/0.47  |- ~accessible_world skc14 $_274 \/ relation $_274 skc12
% 0.19/0.47  |- ~accessible_world skc14 $_274 \/ relation $_274 skc16
% 0.19/0.47  |- ~accessible_world skc9 $_274 \/ relation $_274 skc12
% 0.19/0.47  |- ~accessible_world skc9 $_274 \/ relation $_274 skc14
% 0.19/0.47  |- ~accessible_world skc9 $_274 \/ relation $_274 skc16
% 0.19/0.47  |- relation skc14 skc14
% 0.19/0.47  |- ~accessible_world skc14 $V \/ relation $V skc14
% 0.19/0.47  |- abstraction skc14 skc14
% 0.19/0.47  |- general skc14 skc14
% 0.19/0.47  |- nonhuman skc14 skc14
% 0.19/0.47  |- ~human skc14 skc14
% 0.19/0.47  |- ~abstraction skc9 $_284 \/ abstraction skc14 $_284
% 0.19/0.47  |- ~accessible_world skc14 $_287 \/ nonhuman $_287 skc12
% 0.19/0.47  |- ~accessible_world skc14 $_287 \/ nonhuman $_287 skc14
% 0.19/0.47  |- ~accessible_world skc14 $_287 \/ nonhuman $_287 skc16
% 0.19/0.47  |- ~accessible_world skc9 $_287 \/ nonhuman $_287 skc12
% 0.19/0.47  |- ~accessible_world skc9 $_287 \/ nonhuman $_287 skc14
% 0.19/0.47  |- ~accessible_world skc9 $_287 \/ nonhuman $_287 skc16
% 0.19/0.47  |- ~accessible_world skc14 $_296 \/ general $_296 skc12
% 0.19/0.47  |- ~accessible_world skc14 $_296 \/ general $_296 skc14
% 0.19/0.47  |- ~accessible_world skc14 $_296 \/ general $_296 skc16
% 0.19/0.47  |- ~accessible_world skc9 $_296 \/ general $_296 skc12
% 0.19/0.47  |- ~accessible_world skc9 $_296 \/ general $_296 skc14
% 0.19/0.47  |- ~accessible_world skc9 $_296 \/ general $_296 skc16
% 0.19/0.47  |- ~accessible_world skc9 $_305 \/ jules_forename $_305 skc12
% 0.19/0.47  |- jules_forename skc14 skc12
% 0.19/0.47  |- ~accessible_world skc14 $V \/ jules_forename $V skc12
% 0.19/0.47  |- ~accessible_world skc14 $_310 \/ smoke $_310 (skf1 $V)
% 0.19/0.47  |- ~accessible_world skc14 $_315 \/ present $_315 (skf1 $V)
% 0.19/0.47  |- ~accessible_world skc9 $_315 \/ present $_315 skc15
% 0.19/0.47  |- present skc14 skc15
% 0.19/0.47  |- ~accessible_world skc14 $V \/ present $V skc15
% 0.19/0.47  |- ~accessible_world skc9 $_322 \/ think_believe_consider $_322 skc15
% 0.19/0.47  |- think_believe_consider skc14 skc15
% 0.19/0.47  |- ~accessible_world skc14 $V \/ think_believe_consider $V skc15
% 0.19/0.47  |- ~accessible_world skc9 $_327 \/ proposition $_327 skc14
% 0.19/0.47  |- proposition skc14 skc14
% 0.19/0.47  |- ~accessible_world skc14 $V \/ proposition $V skc14
% 0.19/0.47  |- ~accessible_world skc9 $_332 \/ vincent_forename $_332 skc16
% 0.19/0.47  |- vincent_forename skc14 skc16
% 0.19/0.47  |- ~accessible_world skc14 $V \/ vincent_forename $V skc16
% 0.19/0.47  |- ~accessible_world skc9 $_337 \/ of $_337 skc12 skc11
% 0.19/0.47  |- ~accessible_world skc9 $_337 \/ of $_337 skc16 skc17
% 0.19/0.47  |- of skc14 skc12 skc11
% 0.19/0.47  |- ~accessible_world skc14 $V \/ of $V skc12 skc11
% 0.19/0.47  |- of skc14 skc16 skc17
% 0.19/0.47  |- ~accessible_world skc14 $V \/ of $V skc16 skc17
% 0.19/0.47  |- ~accessible_world skc14 $_345 \/ agent $_345 (skf1 skc11) skc11
% 0.19/0.47  |- ~accessible_world skc14 $_345 \/ agent $_345 (skf1 skc17) skc17
% 0.19/0.47  |- ~accessible_world skc9 $_345 \/ agent $_345 skc15 skc17
% 0.19/0.47  |- agent skc14 skc15 skc17
% 0.19/0.47  |- ~accessible_world skc14 $V \/ agent $V skc15 skc17
% 0.19/0.47  |- ~accessible_world skc9 $_353 \/ theme $_353 skc15 skc14
% 0.19/0.47  |- theme skc14 skc15 skc14
% 0.19/0.47  |- ~accessible_world skc14 $V \/ theme $V skc15 skc14
% 0.19/0.47  |- ~accessible_world skc9 $_359 \/ be $_359 skc10 skc11 skc11
% 0.19/0.47  |- be skc14 skc10 skc11 skc11
% 0.19/0.47  |- ~accessible_world skc14 $V \/ be $V skc10 skc11 skc11
% 0.19/0.47  |- ~forename skc14 $_367 \/ ~of skc14 $_367 skc11 \/ $_367 = skc12
% 0.19/0.47  |- ~forename skc14 $_367 \/ ~of skc14 $_367 skc17 \/ $_367 = skc16
% 0.19/0.47  |- ~forename skc9 $_367 \/ ~of skc9 $_367 skc11 \/ $_367 = skc12
% 0.19/0.47  |- ~forename skc9 $_367 \/ ~of skc9 $_367 skc17 \/ $_367 = skc16
% 0.19/0.47  |- ~agent skc14 skc15 $_377 \/ ~proposition skc14 $_375 \/
% 0.19/0.47     ~theme skc14 skc15 $_375 \/ skc14 = $_375
% 0.19/0.47  |- ~agent skc9 skc15 $_377 \/ ~proposition skc9 $_375 \/
% 0.19/0.47     ~theme skc9 skc15 $_375 \/ skc14 = $_375
% 0.19/0.47  |- ~agent skc14 $_386 $_387 \/ ~agent skc14 skc15 $_387 \/
% 0.19/0.47     ~proposition skc14 $_384 \/ ~theme skc14 $_386 $_384 \/
% 0.19/0.47     ~think_believe_consider skc14 $_386 \/ skc14 = $_384
% 0.19/0.47  |- ~agent skc9 $_386 $_387 \/ ~agent skc9 skc15 $_387 \/
% 0.19/0.47     ~proposition skc9 $_384 \/ ~theme skc9 $_386 $_384 \/
% 0.19/0.47     ~think_believe_consider skc9 $_386 \/ skc14 = $_384
% 0.19/0.47  SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.47  
%------------------------------------------------------------------------------