%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : NLP228-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n028.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:21 EDT 2022 % Result : Satisfiable 0.19s 0.42s % Output : Saturation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : NLP228-1 : TPTP v8.1.0. Released v2.4.0. % 0.10/0.13 % Command : metis --show proof --show saturation %s % 0.12/0.33 % Computer : n028.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Thu Jun 30 21:05:00 EDT 2022 % 0.12/0.34 % CPUTime : % 0.12/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.19/0.42 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.19/0.42 % 0.19/0.42 SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.19/0.42 |- ~state $U $V \/ eventuality $U $V % 0.19/0.42 |- ~eventuality $U $V \/ thing $U $V % 0.19/0.42 |- ~thing $U $V \/ singleton $U $V % 0.19/0.42 |- ~eventuality $U $V \/ specific $U $V % 0.19/0.42 |- ~eventuality $U $V \/ nonexistent $U $V % 0.19/0.42 |- ~eventuality $U $V \/ unisex $U $V % 0.19/0.42 |- ~state $U $V \/ event $U $V % 0.19/0.42 |- ~event $U $V \/ eventuality $U $V % 0.19/0.42 |- ~man $U $V \/ human_person $U $V % 0.19/0.42 |- ~human_person $U $V \/ organism $U $V % 0.19/0.42 |- ~organism $U $V \/ entity $U $V % 0.19/0.42 |- ~entity $U $V \/ thing $U $V % 0.19/0.42 |- ~entity $U $V \/ specific $U $V % 0.19/0.42 |- ~entity $U $V \/ existent $U $V % 0.19/0.42 |- ~organism $U $V \/ impartial $U $V % 0.19/0.42 |- ~organism $U $V \/ living $U $V % 0.19/0.42 |- ~human_person $U $V \/ human $U $V % 0.19/0.42 |- ~human_person $U $V \/ animate $U $V % 0.19/0.42 |- ~man $U $V \/ male $U $V % 0.19/0.42 |- ~forename $U $V \/ relname $U $V % 0.19/0.42 |- ~relname $U $V \/ relation $U $V % 0.19/0.42 |- ~relation $U $V \/ abstraction $U $V % 0.19/0.42 |- ~abstraction $U $V \/ thing $U $V % 0.19/0.42 |- ~abstraction $U $V \/ nonhuman $U $V % 0.19/0.42 |- ~abstraction $U $V \/ general $U $V % 0.19/0.42 |- ~abstraction $U $V \/ unisex $U $V % 0.19/0.42 |- ~jules_forename $U $V \/ forename $U $V % 0.19/0.42 |- ~smoke $U $V \/ event $U $V % 0.19/0.42 |- ~proposition $U $V \/ relation $U $V % 0.19/0.42 |- ~vincent_forename $U $V \/ forename $U $V % 0.19/0.42 |- ~male $U $V \/ ~unisex $U $V % 0.19/0.42 |- ~general $U $V \/ ~specific $U $V % 0.19/0.42 |- ~human $U $V \/ ~nonhuman $U $V % 0.19/0.42 |- ~existent $U $V \/ ~nonexistent $U $V % 0.19/0.42 |- ~be $U $V $W $X \/ $W = $X % 0.19/0.42 |- ~accessible_world $U $V \/ ~state $U $W \/ state $V $W % 0.19/0.42 |- ~accessible_world $U $V \/ ~eventuality $U $W \/ eventuality $V $W % 0.19/0.42 |- ~accessible_world $U $V \/ ~thing $U $W \/ thing $V $W % 0.19/0.42 |- ~accessible_world $U $V \/ ~singleton $U $W \/ singleton $V $W % 0.19/0.42 |- ~accessible_world $U $V \/ ~specific $U $W \/ specific $V $W % 0.19/0.43 |- ~accessible_world $U $V \/ ~nonexistent $U $W \/ nonexistent $V $W % 0.19/0.43 |- ~accessible_world $U $V \/ ~unisex $U $W \/ unisex $V $W % 0.19/0.43 |- ~accessible_world $U $V \/ ~event $U $W \/ event $V $W % 0.19/0.43 |- ~accessible_world $U $V \/ ~man $U $W \/ man $V $W % 0.19/0.43 |- ~accessible_world $U $V \/ ~human_person $U $W \/ human_person $V $W % 0.19/0.43 |- ~accessible_world $U $V \/ ~organism $U $W \/ organism $V $W % 0.19/0.43 |- ~accessible_world $U $V \/ ~entity $U $W \/ entity $V $W % 0.19/0.43 |- ~accessible_world $U $V \/ ~existent $U $W \/ existent $V $W % 0.19/0.43 |- ~accessible_world $U $V \/ ~impartial $U $W \/ impartial $V $W % 0.19/0.43 |- ~accessible_world $U $V \/ ~living $U $W \/ living $V $W % 0.19/0.43 |- ~accessible_world $U $V \/ ~human $U $W \/ human $V $W % 0.19/0.43 |- ~accessible_world $U $V \/ ~animate $U $W \/ animate $V $W % 0.19/0.43 |- ~accessible_world $U $V \/ ~male $U $W \/ male $V $W % 0.19/0.43 |- ~accessible_world $U $V \/ ~forename $U $W \/ forename $V $W % 0.19/0.43 |- ~accessible_world $U $V \/ ~relname $U $W \/ relname $V $W % 0.19/0.43 |- ~accessible_world $U $V \/ ~relation $U $W \/ relation $V $W % 0.19/0.43 |- ~abstraction $U $W \/ ~accessible_world $U $V \/ abstraction $V $W % 0.19/0.43 |- ~accessible_world $U $V \/ ~nonhuman $U $W \/ nonhuman $V $W % 0.19/0.43 |- ~accessible_world $U $V \/ ~general $U $W \/ general $V $W % 0.19/0.43 |- ~accessible_world $U $V \/ ~jules_forename $U $W \/ jules_forename $V $W % 0.19/0.43 |- ~accessible_world $U $V \/ ~smoke $U $W \/ smoke $V $W % 0.19/0.43 |- ~accessible_world $U $V \/ ~present $U $W \/ present $V $W % 0.19/0.43 |- ~accessible_world $U $V \/ ~think_believe_consider $U $W \/ % 0.19/0.43 think_believe_consider $V $W % 0.19/0.43 |- ~accessible_world $U $V \/ ~proposition $U $W \/ proposition $V $W % 0.19/0.43 |- ~accessible_world $U $V \/ ~vincent_forename $U $W \/ % 0.19/0.43 vincent_forename $V $W % 0.19/0.43 |- ~accessible_world $U $V \/ ~of $U $W $X \/ of $V $W $X % 0.19/0.43 |- ~accessible_world $U $V \/ ~agent $U $W $X \/ agent $V $W $X % 0.19/0.43 |- ~accessible_world $U $V \/ ~theme $U $W $X \/ theme $V $W $X % 0.19/0.43 |- ~accessible_world $U $V \/ ~be $U $W $X $Y \/ be $V $W $X $Y % 0.19/0.43 |- ~entity $U $X \/ ~forename $U $V \/ ~forename $U $W \/ ~of $U $V $X \/ % 0.19/0.43 ~of $U $W $X \/ $W = $V % 0.19/0.43 |- ~agent $U $X $Z \/ ~agent $U $Y $Z \/ ~proposition $U $V \/ % 0.19/0.43 ~proposition $U $W \/ ~theme $U $X $V \/ ~theme $U $Y $W \/ % 0.19/0.43 ~think_believe_consider $U $X \/ ~think_believe_consider $U $Y \/ % 0.19/0.43 $V = $W % 0.19/0.43 |- ~agent $U $Y $Z \/ ~proposition $U $V \/ ~proposition $U $W \/ % 0.19/0.43 ~theme $U $Y $V \/ ~theme $U $Y $W \/ ~think_believe_consider $U $Y \/ % 0.19/0.43 $V = $W % 0.19/0.43 |- actual_world skc5 % 0.19/0.43 |- man skc5 skc9 % 0.19/0.43 |- forename skc5 skc8 % 0.19/0.43 |- vincent_forename skc5 skc8 % 0.19/0.43 |- event skc5 skc7 % 0.19/0.43 |- present skc5 skc7 % 0.19/0.43 |- think_believe_consider skc5 skc7 % 0.19/0.43 |- accessible_world skc5 skc6 % 0.19/0.43 |- proposition skc5 skc6 % 0.19/0.43 |- of skc5 skc8 skc9 % 0.19/0.43 |- agent skc5 skc7 skc9 % 0.19/0.43 |- theme skc5 skc7 skc6 % 0.19/0.43 |- ~man skc6 $U \/ agent skc6 (skf2 $U) $U % 0.19/0.43 |- ~accessible_world $U $X \/ ~actual_world $U \/ ~agent $U $Y $X1 \/ % 0.19/0.43 ~be $U $V $X1 $W \/ ~event $U $Y \/ ~forename $U $X2 \/ % 0.19/0.43 ~forename $U $Z \/ ~jules_forename $U $X2 \/ ~man $U $W \/ % 0.19/0.43 ~man $U $X1 \/ ~of $U $X2 $X1 \/ ~of $U $Z $X1 \/ ~present $U $Y \/ % 0.19/0.43 ~proposition $U $X \/ ~state $U $V \/ ~theme $U $Y $X \/ % 0.19/0.43 ~think_believe_consider $U $Y \/ ~vincent_forename $U $Z \/ % 0.19/0.43 man $X (skf4 $X) % 0.19/0.43 |- ~accessible_world $U $X \/ ~actual_world $U \/ ~agent $U $Z $X2 \/ % 0.19/0.43 ~agent $X $Y (skf4 $X) \/ ~be $U $V $X2 $W \/ ~event $U $Z \/ % 0.19/0.43 ~event $X $Y \/ ~forename $U $X1 \/ ~forename $U $X3 \/ % 0.19/0.43 ~jules_forename $U $X3 \/ ~man $U $W \/ ~man $U $X2 \/ ~of $U $X1 $X2 \/ % 0.19/0.43 ~of $U $X3 $X2 \/ ~present $U $Z \/ ~present $X $Y \/ % 0.19/0.43 ~proposition $U $X \/ ~smoke $X $Y \/ ~state $U $V \/ ~theme $U $Z $X \/ % 0.19/0.43 ~think_believe_consider $U $Z \/ ~vincent_forename $U $X1 % 0.19/0.43 |- ~accessible_world $U $X \/ ~actual_world $U \/ ~agent $U $Y $X1 \/ % 0.19/0.43 ~be $U $V $X1 $W \/ ~event $U $Y \/ ~forename $U $Z \/ % 0.19/0.43 ~jules_forename $U $Z \/ ~man $U $W \/ ~man $U $X1 \/ ~of $U $Z $X1 \/ % 0.19/0.43 ~present $U $Y \/ ~proposition $U $X \/ ~state $U $V \/ % 0.19/0.43 ~theme $U $Y $X \/ ~think_believe_consider $U $Y \/ % 0.19/0.43 ~vincent_forename $U $Z \/ man $X (skf4 $X) % 0.19/0.43 |- ~accessible_world $X $X \/ ~actual_world $X \/ ~agent $X $Y (skf4 $X) \/ % 0.19/0.43 ~be $X $V (skf4 $X) $W \/ ~event $X $Y \/ ~forename $X $X1 \/ % 0.19/0.43 ~forename $X $X3 \/ ~jules_forename $X $X3 \/ ~man $X $W \/ % 0.19/0.43 ~man $X (skf4 $X) \/ ~of $X $X1 (skf4 $X) \/ ~of $X $X3 (skf4 $X) \/ % 0.19/0.43 ~present $X $Y \/ ~proposition $X $X \/ ~smoke $X $Y \/ ~state $X $V \/ % 0.19/0.43 ~theme $X $Y $X \/ ~think_believe_consider $X $Y \/ % 0.19/0.43 ~vincent_forename $X $X1 % 0.19/0.43 |- ~accessible_world $U $X \/ ~actual_world $U \/ ~agent $U $Z $X2 \/ % 0.19/0.43 ~agent $X $Y (skf4 $X) \/ ~be $U $V $X2 $W \/ ~event $U $Z \/ % 0.19/0.43 ~event $X $Y \/ ~forename $U $X3 \/ ~jules_forename $U $X3 \/ % 0.19/0.43 ~man $U $W \/ ~man $U $X2 \/ ~of $U $X3 $X2 \/ ~present $U $Z \/ % 0.19/0.43 ~present $X $Y \/ ~proposition $U $X \/ ~smoke $X $Y \/ ~state $U $V \/ % 0.19/0.43 ~theme $U $Z $X \/ ~think_believe_consider $U $Z \/ % 0.19/0.43 ~vincent_forename $U $X3 % 0.19/0.43 |- ~accessible_world $X $X \/ ~actual_world $X \/ ~agent $X $Y (skf4 $X) \/ % 0.19/0.43 ~be $X $V (skf4 $X) $W \/ ~event $X $Y \/ ~forename $X $X3 \/ % 0.19/0.43 ~jules_forename $X $X3 \/ ~man $X $W \/ ~man $X (skf4 $X) \/ % 0.19/0.43 ~of $X $X3 (skf4 $X) \/ ~present $X $Y \/ ~proposition $X $X \/ % 0.19/0.43 ~smoke $X $Y \/ ~state $X $V \/ ~theme $X $Y $X \/ % 0.19/0.43 ~think_believe_consider $X $Y \/ ~vincent_forename $X $X3 % 0.19/0.43 |- eventuality skc5 skc7 % 0.19/0.43 |- unisex skc5 skc7 % 0.19/0.43 |- nonexistent skc5 skc7 % 0.19/0.43 |- specific skc5 skc7 % 0.19/0.43 |- thing skc5 skc7 % 0.19/0.43 |- singleton skc5 skc7 % 0.19/0.43 |- human_person skc5 skc9 % 0.19/0.43 |- organism skc5 skc9 % 0.19/0.43 |- entity skc5 skc9 % 0.19/0.43 |- thing skc5 skc9 % 0.19/0.43 |- singleton skc5 skc9 % 0.19/0.43 |- specific skc5 skc9 % 0.19/0.43 |- existent skc5 skc9 % 0.19/0.43 |- impartial skc5 skc9 % 0.19/0.43 |- living skc5 skc9 % 0.19/0.43 |- human skc5 skc9 % 0.19/0.43 |- animate skc5 skc9 % 0.19/0.43 |- male skc5 skc9 % 0.19/0.43 |- relname skc5 skc8 % 0.19/0.43 |- relation skc5 skc8 % 0.19/0.43 |- abstraction skc5 skc8 % 0.19/0.43 |- thing skc5 skc8 % 0.19/0.43 |- singleton skc5 skc8 % 0.19/0.43 |- nonhuman skc5 skc8 % 0.19/0.43 |- general skc5 skc8 % 0.19/0.43 |- unisex skc5 skc8 % 0.19/0.43 |- relation skc5 skc6 % 0.19/0.43 |- abstraction skc5 skc6 % 0.19/0.43 |- unisex skc5 skc6 % 0.19/0.43 |- general skc5 skc6 % 0.19/0.43 |- nonhuman skc5 skc6 % 0.19/0.43 |- thing skc5 skc6 % 0.19/0.43 |- singleton skc5 skc6 % 0.19/0.43 |- ~male skc5 skc6 % 0.19/0.43 |- ~male skc5 skc7 % 0.19/0.43 |- ~male skc5 skc8 % 0.19/0.43 |- ~general skc5 skc7 % 0.19/0.43 |- ~general skc5 skc9 % 0.19/0.43 |- ~human skc5 skc6 % 0.19/0.43 |- ~human skc5 skc8 % 0.19/0.43 |- ~existent skc5 skc7 % 0.19/0.43 |- ~accessible_world skc5 $_83 \/ eventuality $_83 skc7 % 0.19/0.43 |- eventuality skc6 skc7 % 0.19/0.43 |- ~accessible_world skc6 $V \/ eventuality $V skc7 % 0.19/0.43 |- unisex skc6 skc7 % 0.19/0.43 |- nonexistent skc6 skc7 % 0.19/0.44 |- specific skc6 skc7 % 0.19/0.44 |- thing skc6 skc7 % 0.19/0.44 |- ~male skc6 skc7 % 0.19/0.44 |- ~existent skc6 skc7 % 0.19/0.44 |- singleton skc6 skc7 % 0.19/0.44 |- ~general skc6 skc7 % 0.19/0.44 |- ~accessible_world skc5 $_88 \/ thing $_88 skc6 % 0.19/0.44 |- ~accessible_world skc5 $_88 \/ thing $_88 skc7 % 0.19/0.44 |- ~accessible_world skc5 $_88 \/ thing $_88 skc8 % 0.19/0.44 |- ~accessible_world skc5 $_88 \/ thing $_88 skc9 % 0.19/0.44 |- ~accessible_world skc6 $_88 \/ thing $_88 skc7 % 0.19/0.44 |- thing skc6 skc8 % 0.19/0.44 |- ~accessible_world skc6 $V \/ thing $V skc8 % 0.19/0.44 |- singleton skc6 skc8 % 0.19/0.44 |- thing skc6 skc9 % 0.19/0.44 |- ~accessible_world skc6 $V \/ thing $V skc9 % 0.19/0.44 |- singleton skc6 skc9 % 0.19/0.44 |- thing skc6 skc6 % 0.19/0.44 |- ~accessible_world skc6 $V \/ thing $V skc6 % 0.19/0.44 |- singleton skc6 skc6 % 0.19/0.44 |- ~accessible_world skc5 $_99 \/ singleton $_99 skc6 % 0.19/0.44 |- ~accessible_world skc5 $_99 \/ singleton $_99 skc7 % 0.19/0.44 |- ~accessible_world skc5 $_99 \/ singleton $_99 skc8 % 0.19/0.44 |- ~accessible_world skc5 $_99 \/ singleton $_99 skc9 % 0.19/0.44 |- ~accessible_world skc6 $_99 \/ singleton $_99 skc6 % 0.19/0.44 |- ~accessible_world skc6 $_99 \/ singleton $_99 skc7 % 0.19/0.44 |- ~accessible_world skc6 $_99 \/ singleton $_99 skc8 % 0.19/0.44 |- ~accessible_world skc6 $_99 \/ singleton $_99 skc9 % 0.19/0.44 |- ~accessible_world skc5 $_110 \/ specific $_110 skc7 % 0.19/0.44 |- ~accessible_world skc5 $_110 \/ specific $_110 skc9 % 0.19/0.44 |- ~accessible_world skc6 $_110 \/ specific $_110 skc7 % 0.19/0.44 |- specific skc6 skc9 % 0.19/0.44 |- ~accessible_world skc6 $V \/ specific $V skc9 % 0.19/0.44 |- ~general skc6 skc9 % 0.19/0.44 |- ~accessible_world skc5 $_117 \/ nonexistent $_117 skc7 % 0.19/0.44 |- ~accessible_world skc6 $_117 \/ nonexistent $_117 skc7 % 0.19/0.44 |- ~accessible_world skc5 $_122 \/ unisex $_122 skc6 % 0.19/0.44 |- ~accessible_world skc5 $_122 \/ unisex $_122 skc7 % 0.19/0.44 |- ~accessible_world skc5 $_122 \/ unisex $_122 skc8 % 0.19/0.44 |- ~accessible_world skc6 $_122 \/ unisex $_122 skc7 % 0.19/0.44 |- unisex skc6 skc6 % 0.19/0.44 |- ~accessible_world skc6 $V \/ unisex $V skc6 % 0.19/0.44 |- ~male skc6 skc6 % 0.19/0.44 |- unisex skc6 skc8 % 0.19/0.44 |- ~accessible_world skc6 $V \/ unisex $V skc8 % 0.19/0.44 |- ~male skc6 skc8 % 0.19/0.44 |- ~accessible_world skc5 $_131 \/ event $_131 skc7 % 0.19/0.44 |- event skc6 skc7 % 0.19/0.44 |- ~accessible_world skc6 $V \/ event $V skc7 % 0.19/0.44 |- ~accessible_world skc5 $_136 \/ man $_136 skc9 % 0.19/0.44 |- man skc6 skc9 % 0.19/0.44 |- ~accessible_world skc6 $V \/ man $V skc9 % 0.19/0.44 |- male skc6 skc9 % 0.19/0.44 |- human_person skc6 skc9 % 0.19/0.44 |- event skc6 (skf2 $V) % 0.19/0.44 |- present skc6 (skf2 $V) % 0.19/0.44 |- smoke skc6 (skf2 $V) % 0.19/0.44 |- agent skc6 (skf2 skc9) skc9 % 0.19/0.44 |- animate skc6 skc9 % 0.19/0.44 |- human skc6 skc9 % 0.19/0.44 |- organism skc6 skc9 % 0.19/0.44 |- living skc6 skc9 % 0.19/0.44 |- impartial skc6 skc9 % 0.19/0.44 |- entity skc6 skc9 % 0.19/0.44 |- existent skc6 skc9 % 0.19/0.44 |- ~accessible_world skc6 $V \/ event $V (skf2 $_140) % 0.19/0.44 |- eventuality skc6 (skf2 $_140) % 0.19/0.44 |- ~accessible_world skc6 $V \/ eventuality $V (skf2 $_141) % 0.19/0.44 |- unisex skc6 (skf2 $_141) % 0.19/0.44 |- nonexistent skc6 (skf2 $_141) % 0.19/0.44 |- specific skc6 (skf2 $_141) % 0.19/0.44 |- thing skc6 (skf2 $_141) % 0.19/0.44 |- ~accessible_world skc6 $V \/ unisex $V (skf2 $_142) % 0.19/0.44 |- ~male skc6 (skf2 $_142) % 0.19/0.44 |- ~accessible_world skc6 $V \/ thing $V (skf2 $_144) % 0.19/0.44 |- singleton skc6 (skf2 $_144) % 0.19/0.44 |- ~accessible_world skc6 $V \/ singleton $V (skf2 $_145) % 0.19/0.44 |- ~accessible_world skc6 $V \/ nonexistent $V (skf2 $_146) % 0.19/0.44 |- ~existent skc6 (skf2 $_146) % 0.19/0.44 |- ~accessible_world skc6 $V \/ specific $V (skf2 $_148) % 0.19/0.44 |- ~general skc6 (skf2 $_148) % 0.19/0.44 |- ~accessible_world skc5 $_167 \/ human_person $_167 skc9 % 0.19/0.44 |- ~accessible_world skc6 $_167 \/ human_person $_167 skc9 % 0.19/0.44 |- ~accessible_world skc5 $_172 \/ organism $_172 skc9 % 0.19/0.44 |- ~accessible_world skc6 $_172 \/ organism $_172 skc9 % 0.19/0.44 |- ~accessible_world skc5 $_177 \/ entity $_177 skc9 % 0.19/0.44 |- ~accessible_world skc6 $_177 \/ entity $_177 skc9 % 0.19/0.44 |- ~accessible_world skc5 $_182 \/ existent $_182 skc9 % 0.19/0.44 |- ~accessible_world skc6 $_182 \/ existent $_182 skc9 % 0.19/0.44 |- ~accessible_world skc5 $_187 \/ impartial $_187 skc9 % 0.19/0.44 |- ~accessible_world skc6 $_187 \/ impartial $_187 skc9 % 0.19/0.44 |- ~accessible_world skc5 $_192 \/ living $_192 skc9 % 0.19/0.44 |- ~accessible_world skc6 $_192 \/ living $_192 skc9 % 0.19/0.44 |- ~accessible_world skc5 $_197 \/ human $_197 skc9 % 0.19/0.44 |- ~accessible_world skc6 $_197 \/ human $_197 skc9 % 0.19/0.44 |- ~accessible_world skc5 $_202 \/ animate $_202 skc9 % 0.19/0.44 |- ~accessible_world skc6 $_202 \/ animate $_202 skc9 % 0.19/0.44 |- ~accessible_world skc5 $_207 \/ male $_207 skc9 % 0.19/0.44 |- ~accessible_world skc6 $_207 \/ male $_207 skc9 % 0.19/0.44 |- ~accessible_world skc5 $_212 \/ forename $_212 skc8 % 0.19/0.44 |- forename skc6 skc8 % 0.19/0.44 |- ~accessible_world skc6 $V \/ forename $V skc8 % 0.19/0.44 |- relname skc6 skc8 % 0.19/0.44 |- relation skc6 skc8 % 0.19/0.44 |- abstraction skc6 skc8 % 0.19/0.44 |- general skc6 skc8 % 0.19/0.44 |- nonhuman skc6 skc8 % 0.19/0.44 |- ~human skc6 skc8 % 0.19/0.44 |- ~accessible_world skc5 $_217 \/ relname $_217 skc8 % 0.19/0.44 |- ~accessible_world skc6 $_217 \/ relname $_217 skc8 % 0.19/0.44 |- ~accessible_world skc5 $_222 \/ relation $_222 skc6 % 0.19/0.44 |- ~accessible_world skc5 $_222 \/ relation $_222 skc8 % 0.19/0.44 |- ~accessible_world skc6 $_222 \/ relation $_222 skc8 % 0.19/0.44 |- relation skc6 skc6 % 0.19/0.44 |- ~accessible_world skc6 $V \/ relation $V skc6 % 0.19/0.44 |- abstraction skc6 skc6 % 0.19/0.44 |- general skc6 skc6 % 0.19/0.44 |- nonhuman skc6 skc6 % 0.19/0.44 |- ~human skc6 skc6 % 0.19/0.44 |- ~abstraction skc5 $_230 \/ abstraction skc6 $_230 % 0.19/0.44 |- ~accessible_world skc5 $_233 \/ nonhuman $_233 skc6 % 0.19/0.44 |- ~accessible_world skc5 $_233 \/ nonhuman $_233 skc8 % 0.19/0.44 |- ~accessible_world skc6 $_233 \/ nonhuman $_233 skc6 % 0.19/0.44 |- ~accessible_world skc6 $_233 \/ nonhuman $_233 skc8 % 0.19/0.44 |- ~accessible_world skc5 $_240 \/ general $_240 skc6 % 0.19/0.44 |- ~accessible_world skc5 $_240 \/ general $_240 skc8 % 0.19/0.45 |- ~accessible_world skc6 $_240 \/ general $_240 skc6 % 0.19/0.45 |- ~accessible_world skc6 $_240 \/ general $_240 skc8 % 0.19/0.45 |- ~accessible_world skc6 $_250 \/ smoke $_250 (skf2 $V) % 0.19/0.45 |- ~accessible_world skc5 $_255 \/ present $_255 skc7 % 0.19/0.45 |- ~accessible_world skc6 $_255 \/ present $_255 (skf2 $V) % 0.19/0.45 |- present skc6 skc7 % 0.19/0.45 |- ~accessible_world skc6 $V \/ present $V skc7 % 0.19/0.45 |- ~accessible_world skc5 $_262 \/ think_believe_consider $_262 skc7 % 0.19/0.45 |- think_believe_consider skc6 skc7 % 0.19/0.45 |- ~accessible_world skc6 $V \/ think_believe_consider $V skc7 % 0.19/0.45 |- ~accessible_world skc5 $_267 \/ proposition $_267 skc6 % 0.19/0.45 |- proposition skc6 skc6 % 0.19/0.45 |- ~accessible_world skc6 $V \/ proposition $V skc6 % 0.19/0.45 |- ~accessible_world skc5 $_272 \/ vincent_forename $_272 skc8 % 0.19/0.45 |- vincent_forename skc6 skc8 % 0.19/0.45 |- ~accessible_world skc6 $V \/ vincent_forename $V skc8 % 0.19/0.45 |- ~accessible_world skc5 $_277 \/ of $_277 skc8 skc9 % 0.19/0.45 |- of skc6 skc8 skc9 % 0.19/0.45 |- ~accessible_world skc6 $V \/ of $V skc8 skc9 % 0.19/0.45 |- ~accessible_world skc5 $_283 \/ agent $_283 skc7 skc9 % 0.19/0.45 |- ~accessible_world skc6 $_283 \/ agent $_283 (skf2 skc9) skc9 % 0.19/0.45 |- agent skc6 skc7 skc9 % 0.19/0.45 |- ~accessible_world skc6 $V \/ agent $V skc7 skc9 % 0.19/0.45 |- ~accessible_world skc5 $_290 \/ theme $_290 skc7 skc6 % 0.19/0.45 |- theme skc6 skc7 skc6 % 0.19/0.45 |- ~accessible_world skc6 $V \/ theme $V skc7 skc6 % 0.19/0.45 |- ~forename skc5 $_302 \/ ~of skc5 $_302 skc9 \/ $_302 = skc8 % 0.19/0.45 |- ~forename skc6 $_302 \/ ~of skc6 $_302 skc9 \/ $_302 = skc8 % 0.19/0.45 |- ~agent skc5 skc7 $_310 \/ ~proposition skc5 $_308 \/ % 0.19/0.45 ~theme skc5 skc7 $_308 \/ skc6 = $_308 % 0.19/0.45 |- ~agent skc6 skc7 $_310 \/ ~proposition skc6 $_308 \/ % 0.19/0.45 ~theme skc6 skc7 $_308 \/ skc6 = $_308 % 0.19/0.45 |- ~agent skc5 $_319 $_320 \/ ~agent skc5 skc7 $_320 \/ % 0.19/0.45 ~proposition skc5 $_317 \/ ~theme skc5 $_319 $_317 \/ % 0.19/0.45 ~think_believe_consider skc5 $_319 \/ skc6 = $_317 % 0.19/0.45 |- ~agent skc6 $_319 $_320 \/ ~agent skc6 skc7 $_320 \/ % 0.19/0.45 ~proposition skc6 $_317 \/ ~theme skc6 $_319 $_317 \/ % 0.19/0.45 ~think_believe_consider skc6 $_319 \/ skc6 = $_317 % 0.19/0.45 SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.19/0.45 %------------------------------------------------------------------------------