%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : NLP226-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n026.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:18 EDT 2022 % Result : Satisfiable 0.18s 0.42s % Output : Saturation 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : NLP226-1 : TPTP v8.1.0. Released v2.4.0. % 0.12/0.12 % Command : metis --show proof --show saturation %s % 0.12/0.33 % Computer : n026.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 17:32:04 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.18/0.42 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.18/0.42 % 0.18/0.42 SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.18/0.42 |- ~state $U $V \/ eventuality $U $V % 0.18/0.42 |- ~eventuality $U $V \/ thing $U $V % 0.18/0.42 |- ~thing $U $V \/ singleton $U $V % 0.18/0.42 |- ~eventuality $U $V \/ specific $U $V % 0.18/0.42 |- ~eventuality $U $V \/ nonexistent $U $V % 0.18/0.42 |- ~eventuality $U $V \/ unisex $U $V % 0.18/0.42 |- ~state $U $V \/ event $U $V % 0.18/0.42 |- ~event $U $V \/ eventuality $U $V % 0.18/0.42 |- ~man $U $V \/ human_person $U $V % 0.18/0.42 |- ~human_person $U $V \/ organism $U $V % 0.18/0.42 |- ~organism $U $V \/ entity $U $V % 0.18/0.42 |- ~entity $U $V \/ thing $U $V % 0.18/0.42 |- ~entity $U $V \/ specific $U $V % 0.18/0.42 |- ~entity $U $V \/ existent $U $V % 0.18/0.42 |- ~organism $U $V \/ impartial $U $V % 0.18/0.42 |- ~organism $U $V \/ living $U $V % 0.18/0.42 |- ~human_person $U $V \/ human $U $V % 0.18/0.42 |- ~human_person $U $V \/ animate $U $V % 0.18/0.42 |- ~man $U $V \/ male $U $V % 0.18/0.42 |- ~forename $U $V \/ relname $U $V % 0.18/0.42 |- ~relname $U $V \/ relation $U $V % 0.18/0.42 |- ~relation $U $V \/ abstraction $U $V % 0.18/0.42 |- ~abstraction $U $V \/ thing $U $V % 0.18/0.42 |- ~abstraction $U $V \/ nonhuman $U $V % 0.18/0.42 |- ~abstraction $U $V \/ general $U $V % 0.18/0.42 |- ~abstraction $U $V \/ unisex $U $V % 0.18/0.42 |- ~jules_forename $U $V \/ forename $U $V % 0.18/0.42 |- ~smoke $U $V \/ event $U $V % 0.18/0.43 |- ~proposition $U $V \/ relation $U $V % 0.18/0.43 |- ~vincent_forename $U $V \/ forename $U $V % 0.18/0.43 |- ~male $U $V \/ ~unisex $U $V % 0.18/0.43 |- ~general $U $V \/ ~specific $U $V % 0.18/0.43 |- ~human $U $V \/ ~nonhuman $U $V % 0.18/0.43 |- ~existent $U $V \/ ~nonexistent $U $V % 0.18/0.43 |- ~be $U $V $W $X \/ $W = $X % 0.18/0.43 |- ~accessible_world $U $V \/ ~state $U $W \/ state $V $W % 0.18/0.43 |- ~accessible_world $U $V \/ ~eventuality $U $W \/ eventuality $V $W % 0.18/0.43 |- ~accessible_world $U $V \/ ~thing $U $W \/ thing $V $W % 0.18/0.43 |- ~accessible_world $U $V \/ ~singleton $U $W \/ singleton $V $W % 0.18/0.43 |- ~accessible_world $U $V \/ ~specific $U $W \/ specific $V $W % 0.18/0.43 |- ~accessible_world $U $V \/ ~nonexistent $U $W \/ nonexistent $V $W % 0.18/0.43 |- ~accessible_world $U $V \/ ~unisex $U $W \/ unisex $V $W % 0.18/0.43 |- ~accessible_world $U $V \/ ~event $U $W \/ event $V $W % 0.18/0.43 |- ~accessible_world $U $V \/ ~man $U $W \/ man $V $W % 0.18/0.43 |- ~accessible_world $U $V \/ ~human_person $U $W \/ human_person $V $W % 0.18/0.43 |- ~accessible_world $U $V \/ ~organism $U $W \/ organism $V $W % 0.18/0.43 |- ~accessible_world $U $V \/ ~entity $U $W \/ entity $V $W % 0.18/0.43 |- ~accessible_world $U $V \/ ~existent $U $W \/ existent $V $W % 0.18/0.43 |- ~accessible_world $U $V \/ ~impartial $U $W \/ impartial $V $W % 0.18/0.43 |- ~accessible_world $U $V \/ ~living $U $W \/ living $V $W % 0.18/0.43 |- ~accessible_world $U $V \/ ~human $U $W \/ human $V $W % 0.18/0.43 |- ~accessible_world $U $V \/ ~animate $U $W \/ animate $V $W % 0.18/0.43 |- ~accessible_world $U $V \/ ~male $U $W \/ male $V $W % 0.18/0.43 |- ~accessible_world $U $V \/ ~forename $U $W \/ forename $V $W % 0.18/0.43 |- ~accessible_world $U $V \/ ~relname $U $W \/ relname $V $W % 0.18/0.43 |- ~accessible_world $U $V \/ ~relation $U $W \/ relation $V $W % 0.18/0.43 |- ~abstraction $U $W \/ ~accessible_world $U $V \/ abstraction $V $W % 0.18/0.43 |- ~accessible_world $U $V \/ ~nonhuman $U $W \/ nonhuman $V $W % 0.18/0.43 |- ~accessible_world $U $V \/ ~general $U $W \/ general $V $W % 0.18/0.43 |- ~accessible_world $U $V \/ ~jules_forename $U $W \/ jules_forename $V $W % 0.18/0.43 |- ~accessible_world $U $V \/ ~smoke $U $W \/ smoke $V $W % 0.18/0.43 |- ~accessible_world $U $V \/ ~present $U $W \/ present $V $W % 0.18/0.43 |- ~accessible_world $U $V \/ ~think_believe_consider $U $W \/ % 0.18/0.43 think_believe_consider $V $W % 0.18/0.43 |- ~accessible_world $U $V \/ ~proposition $U $W \/ proposition $V $W % 0.18/0.43 |- ~accessible_world $U $V \/ ~vincent_forename $U $W \/ % 0.18/0.43 vincent_forename $V $W % 0.18/0.43 |- ~accessible_world $U $V \/ ~of $U $W $X \/ of $V $W $X % 0.18/0.43 |- ~accessible_world $U $V \/ ~agent $U $W $X \/ agent $V $W $X % 0.18/0.43 |- ~accessible_world $U $V \/ ~theme $U $W $X \/ theme $V $W $X % 0.18/0.43 |- ~accessible_world $U $V \/ ~be $U $W $X $Y \/ be $V $W $X $Y % 0.18/0.43 |- ~entity $U $X \/ ~forename $U $V \/ ~forename $U $W \/ ~of $U $V $X \/ % 0.18/0.43 ~of $U $W $X \/ $W = $V % 0.18/0.43 |- ~agent $U $X $Z \/ ~agent $U $Y $Z \/ ~proposition $U $V \/ % 0.18/0.43 ~proposition $U $W \/ ~theme $U $X $V \/ ~theme $U $Y $W \/ % 0.18/0.43 ~think_believe_consider $U $X \/ ~think_believe_consider $U $Y \/ % 0.18/0.43 $V = $W % 0.18/0.43 |- ~agent $U $Y $Z \/ ~proposition $U $V \/ ~proposition $U $W \/ % 0.18/0.43 ~theme $U $Y $V \/ ~theme $U $Y $W \/ ~think_believe_consider $U $Y \/ % 0.18/0.43 $V = $W % 0.18/0.43 |- actual_world skc8 % 0.18/0.43 |- man skc8 skc15 % 0.18/0.43 |- forename skc8 skc14 % 0.18/0.43 |- vincent_forename skc8 skc14 % 0.18/0.43 |- event skc8 skc13 % 0.18/0.43 |- present skc8 skc13 % 0.18/0.43 |- think_believe_consider skc8 skc13 % 0.18/0.43 |- jules_forename skc8 skc11 % 0.18/0.43 |- forename skc8 skc11 % 0.18/0.43 |- man skc8 skc10 % 0.18/0.43 |- state skc8 skc9 % 0.18/0.43 |- accessible_world skc8 skc12 % 0.18/0.43 |- proposition skc8 skc12 % 0.18/0.43 |- of skc8 skc14 skc15 % 0.18/0.43 |- agent skc8 skc13 skc15 % 0.18/0.43 |- theme skc8 skc13 skc12 % 0.18/0.43 |- of skc8 skc11 skc10 % 0.18/0.43 |- be skc8 skc9 skc10 skc10 % 0.18/0.43 |- ~man skc12 $U \/ agent skc12 (skf1 $U) $U % 0.18/0.43 |- eventuality skc8 skc9 % 0.18/0.43 |- thing skc8 skc9 % 0.18/0.43 |- singleton skc8 skc9 % 0.18/0.43 |- specific skc8 skc9 % 0.18/0.43 |- nonexistent skc8 skc9 % 0.18/0.43 |- unisex skc8 skc9 % 0.18/0.43 |- event skc8 skc9 % 0.18/0.43 |- eventuality skc8 skc13 % 0.18/0.43 |- unisex skc8 skc13 % 0.18/0.43 |- nonexistent skc8 skc13 % 0.18/0.43 |- specific skc8 skc13 % 0.18/0.43 |- thing skc8 skc13 % 0.18/0.43 |- singleton skc8 skc13 % 0.18/0.43 |- human_person skc8 skc10 % 0.18/0.43 |- human_person skc8 skc15 % 0.18/0.43 |- organism skc8 skc10 % 0.18/0.43 |- organism skc8 skc15 % 0.18/0.43 |- entity skc8 skc10 % 0.18/0.43 |- entity skc8 skc15 % 0.18/0.43 |- thing skc8 skc10 % 0.18/0.43 |- thing skc8 skc15 % 0.18/0.43 |- singleton skc8 skc15 % 0.18/0.43 |- singleton skc8 skc10 % 0.18/0.43 |- specific skc8 skc10 % 0.18/0.43 |- specific skc8 skc15 % 0.18/0.43 |- existent skc8 skc10 % 0.18/0.43 |- existent skc8 skc15 % 0.18/0.43 |- impartial skc8 skc10 % 0.18/0.43 |- impartial skc8 skc15 % 0.18/0.43 |- living skc8 skc10 % 0.18/0.43 |- living skc8 skc15 % 0.18/0.43 |- human skc8 skc10 % 0.18/0.43 |- human skc8 skc15 % 0.18/0.43 |- animate skc8 skc10 % 0.18/0.43 |- animate skc8 skc15 % 0.18/0.43 |- male skc8 skc10 % 0.18/0.43 |- male skc8 skc15 % 0.18/0.43 |- relname skc8 skc11 % 0.18/0.43 |- relname skc8 skc14 % 0.18/0.43 |- relation skc8 skc11 % 0.18/0.43 |- relation skc8 skc14 % 0.18/0.43 |- abstraction skc8 skc11 % 0.18/0.43 |- abstraction skc8 skc14 % 0.18/0.43 |- thing skc8 skc11 % 0.18/0.43 |- thing skc8 skc14 % 0.18/0.43 |- singleton skc8 skc14 % 0.18/0.43 |- singleton skc8 skc11 % 0.18/0.43 |- nonhuman skc8 skc11 % 0.18/0.43 |- nonhuman skc8 skc14 % 0.18/0.43 |- general skc8 skc11 % 0.18/0.43 |- general skc8 skc14 % 0.18/0.43 |- unisex skc8 skc11 % 0.18/0.43 |- unisex skc8 skc14 % 0.18/0.43 |- relation skc8 skc12 % 0.18/0.43 |- abstraction skc8 skc12 % 0.18/0.44 |- unisex skc8 skc12 % 0.18/0.44 |- general skc8 skc12 % 0.18/0.44 |- nonhuman skc8 skc12 % 0.18/0.44 |- thing skc8 skc12 % 0.18/0.44 |- singleton skc8 skc12 % 0.18/0.44 |- ~male skc8 skc11 % 0.18/0.44 |- ~male skc8 skc12 % 0.18/0.44 |- ~male skc8 skc13 % 0.18/0.44 |- ~male skc8 skc14 % 0.18/0.44 |- ~male skc8 skc9 % 0.18/0.44 |- ~general skc8 skc10 % 0.18/0.44 |- ~general skc8 skc13 % 0.18/0.44 |- ~general skc8 skc15 % 0.18/0.44 |- ~general skc8 skc9 % 0.18/0.44 |- ~human skc8 skc11 % 0.18/0.44 |- ~human skc8 skc12 % 0.18/0.44 |- ~human skc8 skc14 % 0.18/0.44 |- ~existent skc8 skc13 % 0.18/0.44 |- ~existent skc8 skc9 % 0.18/0.44 |- ~accessible_world skc8 $_80 \/ state $_80 skc9 % 0.18/0.44 |- state skc12 skc9 % 0.18/0.44 |- ~accessible_world skc12 $V \/ state $V skc9 % 0.18/0.44 |- event skc12 skc9 % 0.18/0.44 |- eventuality skc12 skc9 % 0.18/0.44 |- unisex skc12 skc9 % 0.18/0.44 |- nonexistent skc12 skc9 % 0.18/0.44 |- specific skc12 skc9 % 0.18/0.44 |- thing skc12 skc9 % 0.18/0.44 |- ~male skc12 skc9 % 0.18/0.44 |- ~general skc12 skc9 % 0.18/0.44 |- ~existent skc12 skc9 % 0.18/0.44 |- singleton skc12 skc9 % 0.18/0.44 |- ~accessible_world skc12 $_85 \/ eventuality $_85 skc9 % 0.18/0.44 |- ~accessible_world skc8 $_85 \/ eventuality $_85 skc13 % 0.18/0.44 |- ~accessible_world skc8 $_85 \/ eventuality $_85 skc9 % 0.18/0.44 |- eventuality skc12 skc13 % 0.18/0.44 |- ~accessible_world skc12 $V \/ eventuality $V skc13 % 0.18/0.44 |- unisex skc12 skc13 % 0.18/0.44 |- nonexistent skc12 skc13 % 0.18/0.44 |- specific skc12 skc13 % 0.18/0.44 |- thing skc12 skc13 % 0.18/0.44 |- ~male skc12 skc13 % 0.18/0.44 |- singleton skc12 skc13 % 0.18/0.44 |- ~existent skc12 skc13 % 0.18/0.44 |- ~general skc12 skc13 % 0.18/0.44 |- ~accessible_world skc12 $_92 \/ thing $_92 skc13 % 0.18/0.44 |- ~accessible_world skc12 $_92 \/ thing $_92 skc9 % 0.18/0.44 |- ~accessible_world skc8 $_92 \/ thing $_92 skc10 % 0.18/0.44 |- ~accessible_world skc8 $_92 \/ thing $_92 skc11 % 0.18/0.44 |- ~accessible_world skc8 $_92 \/ thing $_92 skc12 % 0.18/0.44 |- ~accessible_world skc8 $_92 \/ thing $_92 skc13 % 0.18/0.44 |- ~accessible_world skc8 $_92 \/ thing $_92 skc14 % 0.18/0.44 |- ~accessible_world skc8 $_92 \/ thing $_92 skc15 % 0.18/0.44 |- ~accessible_world skc8 $_92 \/ thing $_92 skc9 % 0.18/0.44 |- thing skc12 skc11 % 0.18/0.44 |- ~accessible_world skc12 $V \/ thing $V skc11 % 0.18/0.44 |- singleton skc12 skc11 % 0.18/0.44 |- thing skc12 skc12 % 0.18/0.44 |- ~accessible_world skc12 $V \/ thing $V skc12 % 0.18/0.44 |- singleton skc12 skc12 % 0.18/0.44 |- thing skc12 skc14 % 0.18/0.44 |- ~accessible_world skc12 $V \/ thing $V skc14 % 0.18/0.44 |- singleton skc12 skc14 % 0.18/0.44 |- thing skc12 skc15 % 0.18/0.44 |- ~accessible_world skc12 $V \/ thing $V skc15 % 0.18/0.44 |- singleton skc12 skc15 % 0.18/0.44 |- thing skc12 skc10 % 0.18/0.44 |- ~accessible_world skc12 $V \/ thing $V skc10 % 0.18/0.44 |- singleton skc12 skc10 % 0.18/0.44 |- ~accessible_world skc12 $_109 \/ singleton $_109 skc10 % 0.18/0.44 |- ~accessible_world skc12 $_109 \/ singleton $_109 skc11 % 0.18/0.44 |- ~accessible_world skc12 $_109 \/ singleton $_109 skc12 % 0.18/0.44 |- ~accessible_world skc12 $_109 \/ singleton $_109 skc13 % 0.18/0.44 |- ~accessible_world skc12 $_109 \/ singleton $_109 skc14 % 0.18/0.44 |- ~accessible_world skc12 $_109 \/ singleton $_109 skc15 % 0.18/0.44 |- ~accessible_world skc12 $_109 \/ singleton $_109 skc9 % 0.18/0.44 |- ~accessible_world skc8 $_109 \/ singleton $_109 skc10 % 0.18/0.44 |- ~accessible_world skc8 $_109 \/ singleton $_109 skc11 % 0.18/0.44 |- ~accessible_world skc8 $_109 \/ singleton $_109 skc12 % 0.18/0.44 |- ~accessible_world skc8 $_109 \/ singleton $_109 skc13 % 0.18/0.44 |- ~accessible_world skc8 $_109 \/ singleton $_109 skc14 % 0.18/0.44 |- ~accessible_world skc8 $_109 \/ singleton $_109 skc15 % 0.18/0.44 |- ~accessible_world skc8 $_109 \/ singleton $_109 skc9 % 0.18/0.44 |- ~accessible_world skc12 $_126 \/ specific $_126 skc13 % 0.18/0.44 |- ~accessible_world skc12 $_126 \/ specific $_126 skc9 % 0.18/0.44 |- ~accessible_world skc8 $_126 \/ specific $_126 skc10 % 0.18/0.44 |- ~accessible_world skc8 $_126 \/ specific $_126 skc13 % 0.18/0.44 |- ~accessible_world skc8 $_126 \/ specific $_126 skc15 % 0.18/0.44 |- ~accessible_world skc8 $_126 \/ specific $_126 skc9 % 0.18/0.44 |- specific skc12 skc15 % 0.18/0.44 |- ~accessible_world skc12 $V \/ specific $V skc15 % 0.18/0.44 |- ~general skc12 skc15 % 0.18/0.44 |- specific skc12 skc10 % 0.18/0.44 |- ~accessible_world skc12 $V \/ specific $V skc10 % 0.18/0.44 |- ~general skc12 skc10 % 0.18/0.44 |- ~accessible_world skc12 $_137 \/ nonexistent $_137 skc13 % 0.18/0.44 |- ~accessible_world skc12 $_137 \/ nonexistent $_137 skc9 % 0.18/0.44 |- ~accessible_world skc8 $_137 \/ nonexistent $_137 skc13 % 0.18/0.44 |- ~accessible_world skc8 $_137 \/ nonexistent $_137 skc9 % 0.18/0.44 |- ~accessible_world skc12 $_144 \/ unisex $_144 skc13 % 0.18/0.44 |- ~accessible_world skc12 $_144 \/ unisex $_144 skc9 % 0.18/0.44 |- ~accessible_world skc8 $_144 \/ unisex $_144 skc11 % 0.18/0.44 |- ~accessible_world skc8 $_144 \/ unisex $_144 skc12 % 0.18/0.44 |- ~accessible_world skc8 $_144 \/ unisex $_144 skc13 % 0.18/0.44 |- ~accessible_world skc8 $_144 \/ unisex $_144 skc14 % 0.18/0.44 |- ~accessible_world skc8 $_144 \/ unisex $_144 skc9 % 0.18/0.44 |- unisex skc12 skc11 % 0.18/0.44 |- ~accessible_world skc12 $V \/ unisex $V skc11 % 0.18/0.44 |- ~male skc12 skc11 % 0.18/0.44 |- unisex skc12 skc12 % 0.18/0.44 |- ~accessible_world skc12 $V \/ unisex $V skc12 % 0.18/0.44 |- ~male skc12 skc12 % 0.18/0.44 |- unisex skc12 skc14 % 0.18/0.44 |- ~accessible_world skc12 $V \/ unisex $V skc14 % 0.18/0.44 |- ~male skc12 skc14 % 0.18/0.44 |- ~accessible_world skc12 $_157 \/ event $_157 skc9 % 0.18/0.44 |- ~accessible_world skc8 $_157 \/ event $_157 skc13 % 0.18/0.44 |- ~accessible_world skc8 $_157 \/ event $_157 skc9 % 0.18/0.44 |- event skc12 skc13 % 0.18/0.44 |- ~accessible_world skc12 $V \/ event $V skc13 % 0.18/0.44 |- ~accessible_world skc8 $_164 \/ man $_164 skc10 % 0.18/0.44 |- ~accessible_world skc8 $_164 \/ man $_164 skc15 % 0.18/0.44 |- man skc12 skc15 % 0.18/0.45 |- ~accessible_world skc12 $V \/ man $V skc15 % 0.18/0.45 |- male skc12 skc15 % 0.18/0.45 |- human_person skc12 skc15 % 0.18/0.45 |- event skc12 (skf1 $V) % 0.18/0.45 |- present skc12 (skf1 $V) % 0.18/0.45 |- smoke skc12 (skf1 $V) % 0.18/0.45 |- agent skc12 (skf1 skc15) skc15 % 0.18/0.45 |- animate skc12 skc15 % 0.18/0.45 |- human skc12 skc15 % 0.18/0.45 |- organism skc12 skc15 % 0.18/0.45 |- living skc12 skc15 % 0.18/0.45 |- impartial skc12 skc15 % 0.18/0.45 |- entity skc12 skc15 % 0.18/0.45 |- existent skc12 skc15 % 0.18/0.45 |- ~accessible_world skc12 $V \/ event $V (skf1 $_169) % 0.18/0.45 |- eventuality skc12 (skf1 $_169) % 0.18/0.45 |- ~accessible_world skc12 $V \/ eventuality $V (skf1 $_170) % 0.18/0.45 |- unisex skc12 (skf1 $_170) % 0.18/0.45 |- nonexistent skc12 (skf1 $_170) % 0.18/0.45 |- specific skc12 (skf1 $_170) % 0.18/0.45 |- thing skc12 (skf1 $_170) % 0.18/0.45 |- ~accessible_world skc12 $V \/ specific $V (skf1 $_171) % 0.18/0.45 |- ~general skc12 (skf1 $_171) % 0.18/0.45 |- ~accessible_world skc12 $V \/ unisex $V (skf1 $_172) % 0.18/0.45 |- ~male skc12 (skf1 $_172) % 0.18/0.45 |- ~accessible_world skc12 $V \/ nonexistent $V (skf1 $_174) % 0.18/0.45 |- ~existent skc12 (skf1 $_174) % 0.18/0.45 |- ~accessible_world skc12 $V \/ thing $V (skf1 $_176) % 0.18/0.45 |- singleton skc12 (skf1 $_176) % 0.18/0.45 |- ~accessible_world skc12 $V \/ singleton $V (skf1 $_177) % 0.18/0.45 |- man skc12 skc10 % 0.18/0.45 |- ~accessible_world skc12 $V \/ man $V skc10 % 0.18/0.45 |- male skc12 skc10 % 0.18/0.45 |- human_person skc12 skc10 % 0.18/0.45 |- agent skc12 (skf1 skc10) skc10 % 0.18/0.45 |- animate skc12 skc10 % 0.18/0.45 |- human skc12 skc10 % 0.18/0.45 |- organism skc12 skc10 % 0.18/0.45 |- living skc12 skc10 % 0.18/0.45 |- impartial skc12 skc10 % 0.18/0.45 |- entity skc12 skc10 % 0.18/0.45 |- existent skc12 skc10 % 0.18/0.45 |- ~accessible_world skc12 $_197 \/ human_person $_197 skc10 % 0.18/0.45 |- ~accessible_world skc12 $_197 \/ human_person $_197 skc15 % 0.18/0.45 |- ~accessible_world skc8 $_197 \/ human_person $_197 skc10 % 0.18/0.45 |- ~accessible_world skc8 $_197 \/ human_person $_197 skc15 % 0.18/0.45 |- ~accessible_world skc12 $_204 \/ organism $_204 skc10 % 0.18/0.45 |- ~accessible_world skc12 $_204 \/ organism $_204 skc15 % 0.18/0.45 |- ~accessible_world skc8 $_204 \/ organism $_204 skc10 % 0.18/0.45 |- ~accessible_world skc8 $_204 \/ organism $_204 skc15 % 0.18/0.45 |- ~accessible_world skc12 $_211 \/ entity $_211 skc10 % 0.18/0.45 |- ~accessible_world skc12 $_211 \/ entity $_211 skc15 % 0.18/0.45 |- ~accessible_world skc8 $_211 \/ entity $_211 skc10 % 0.18/0.45 |- ~accessible_world skc8 $_211 \/ entity $_211 skc15 % 0.18/0.45 |- ~accessible_world skc12 $_218 \/ existent $_218 skc10 % 0.18/0.45 |- ~accessible_world skc12 $_218 \/ existent $_218 skc15 % 0.18/0.45 |- ~accessible_world skc8 $_218 \/ existent $_218 skc10 % 0.18/0.45 |- ~accessible_world skc8 $_218 \/ existent $_218 skc15 % 0.18/0.45 |- ~accessible_world skc12 $_225 \/ impartial $_225 skc10 % 0.18/0.45 |- ~accessible_world skc12 $_225 \/ impartial $_225 skc15 % 0.18/0.45 |- ~accessible_world skc8 $_225 \/ impartial $_225 skc10 % 0.18/0.45 |- ~accessible_world skc8 $_225 \/ impartial $_225 skc15 % 0.18/0.45 |- ~accessible_world skc12 $_232 \/ living $_232 skc10 % 0.18/0.45 |- ~accessible_world skc12 $_232 \/ living $_232 skc15 % 0.18/0.45 |- ~accessible_world skc8 $_232 \/ living $_232 skc10 % 0.18/0.45 |- ~accessible_world skc8 $_232 \/ living $_232 skc15 % 0.18/0.45 |- ~accessible_world skc12 $_239 \/ human $_239 skc10 % 0.18/0.45 |- ~accessible_world skc12 $_239 \/ human $_239 skc15 % 0.18/0.45 |- ~accessible_world skc8 $_239 \/ human $_239 skc10 % 0.18/0.45 |- ~accessible_world skc8 $_239 \/ human $_239 skc15 % 0.18/0.45 |- ~accessible_world skc12 $_246 \/ animate $_246 skc10 % 0.18/0.45 |- ~accessible_world skc12 $_246 \/ animate $_246 skc15 % 0.18/0.45 |- ~accessible_world skc8 $_246 \/ animate $_246 skc10 % 0.18/0.45 |- ~accessible_world skc8 $_246 \/ animate $_246 skc15 % 0.18/0.45 |- ~accessible_world skc12 $_253 \/ male $_253 skc10 % 0.18/0.45 |- ~accessible_world skc12 $_253 \/ male $_253 skc15 % 0.18/0.45 |- ~accessible_world skc8 $_253 \/ male $_253 skc10 % 0.18/0.45 |- ~accessible_world skc8 $_253 \/ male $_253 skc15 % 0.18/0.45 |- ~accessible_world skc8 $_260 \/ forename $_260 skc11 % 0.18/0.45 |- ~accessible_world skc8 $_260 \/ forename $_260 skc14 % 0.18/0.45 |- forename skc12 skc14 % 0.18/0.45 |- ~accessible_world skc12 $V \/ forename $V skc14 % 0.18/0.45 |- relname skc12 skc14 % 0.18/0.45 |- relation skc12 skc14 % 0.18/0.45 |- abstraction skc12 skc14 % 0.18/0.45 |- general skc12 skc14 % 0.18/0.45 |- nonhuman skc12 skc14 % 0.18/0.45 |- ~human skc12 skc14 % 0.18/0.45 |- forename skc12 skc11 % 0.18/0.45 |- ~accessible_world skc12 $V \/ forename $V skc11 % 0.18/0.45 |- relname skc12 skc11 % 0.18/0.45 |- relation skc12 skc11 % 0.18/0.45 |- abstraction skc12 skc11 % 0.18/0.45 |- general skc12 skc11 % 0.18/0.45 |- nonhuman skc12 skc11 % 0.18/0.45 |- ~human skc12 skc11 % 0.18/0.45 |- ~accessible_world skc12 $_267 \/ relname $_267 skc11 % 0.18/0.45 |- ~accessible_world skc12 $_267 \/ relname $_267 skc14 % 0.18/0.45 |- ~accessible_world skc8 $_267 \/ relname $_267 skc11 % 0.18/0.45 |- ~accessible_world skc8 $_267 \/ relname $_267 skc14 % 0.18/0.45 |- ~accessible_world skc12 $_274 \/ relation $_274 skc11 % 0.18/0.45 |- ~accessible_world skc12 $_274 \/ relation $_274 skc14 % 0.18/0.45 |- ~accessible_world skc8 $_274 \/ relation $_274 skc11 % 0.18/0.45 |- ~accessible_world skc8 $_274 \/ relation $_274 skc12 % 0.18/0.45 |- ~accessible_world skc8 $_274 \/ relation $_274 skc14 % 0.18/0.45 |- relation skc12 skc12 % 0.18/0.45 |- ~accessible_world skc12 $V \/ relation $V skc12 % 0.18/0.45 |- abstraction skc12 skc12 % 0.18/0.45 |- general skc12 skc12 % 0.18/0.45 |- nonhuman skc12 skc12 % 0.18/0.45 |- ~human skc12 skc12 % 0.18/0.45 |- ~abstraction skc8 $_284 \/ abstraction skc12 $_284 % 0.18/0.45 |- ~accessible_world skc12 $_287 \/ nonhuman $_287 skc11 % 0.18/0.45 |- ~accessible_world skc12 $_287 \/ nonhuman $_287 skc12 % 0.18/0.45 |- ~accessible_world skc12 $_287 \/ nonhuman $_287 skc14 % 0.18/0.45 |- ~accessible_world skc8 $_287 \/ nonhuman $_287 skc11 % 0.18/0.45 |- ~accessible_world skc8 $_287 \/ nonhuman $_287 skc12 % 0.18/0.45 |- ~accessible_world skc8 $_287 \/ nonhuman $_287 skc14 % 0.18/0.45 |- ~accessible_world skc12 $_296 \/ general $_296 skc11 % 0.18/0.45 |- ~accessible_world skc12 $_296 \/ general $_296 skc12 % 0.18/0.45 |- ~accessible_world skc12 $_296 \/ general $_296 skc14 % 0.18/0.45 |- ~accessible_world skc8 $_296 \/ general $_296 skc11 % 0.18/0.45 |- ~accessible_world skc8 $_296 \/ general $_296 skc12 % 0.18/0.45 |- ~accessible_world skc8 $_296 \/ general $_296 skc14 % 0.18/0.45 |- ~accessible_world skc8 $_305 \/ jules_forename $_305 skc11 % 0.18/0.45 |- jules_forename skc12 skc11 % 0.18/0.45 |- ~accessible_world skc12 $V \/ jules_forename $V skc11 % 0.18/0.45 |- ~accessible_world skc12 $_310 \/ smoke $_310 (skf1 $V) % 0.18/0.46 |- ~accessible_world skc12 $_315 \/ present $_315 (skf1 $V) % 0.18/0.46 |- ~accessible_world skc8 $_315 \/ present $_315 skc13 % 0.18/0.46 |- present skc12 skc13 % 0.18/0.46 |- ~accessible_world skc12 $V \/ present $V skc13 % 0.18/0.46 |- ~accessible_world skc8 $_322 \/ think_believe_consider $_322 skc13 % 0.18/0.46 |- think_believe_consider skc12 skc13 % 0.18/0.46 |- ~accessible_world skc12 $V \/ think_believe_consider $V skc13 % 0.18/0.46 |- ~accessible_world skc8 $_327 \/ proposition $_327 skc12 % 0.18/0.46 |- proposition skc12 skc12 % 0.18/0.46 |- ~accessible_world skc12 $V \/ proposition $V skc12 % 0.18/0.46 |- ~accessible_world skc8 $_332 \/ vincent_forename $_332 skc14 % 0.18/0.46 |- vincent_forename skc12 skc14 % 0.18/0.46 |- ~accessible_world skc12 $V \/ vincent_forename $V skc14 % 0.18/0.46 |- ~accessible_world skc8 $_337 \/ of $_337 skc11 skc10 % 0.18/0.46 |- ~accessible_world skc8 $_337 \/ of $_337 skc14 skc15 % 0.18/0.46 |- of skc12 skc14 skc15 % 0.18/0.46 |- ~accessible_world skc12 $V \/ of $V skc14 skc15 % 0.18/0.46 |- of skc12 skc11 skc10 % 0.18/0.46 |- ~accessible_world skc12 $V \/ of $V skc11 skc10 % 0.18/0.46 |- ~accessible_world skc12 $_345 \/ agent $_345 (skf1 skc10) skc10 % 0.18/0.46 |- ~accessible_world skc12 $_345 \/ agent $_345 (skf1 skc15) skc15 % 0.18/0.46 |- ~accessible_world skc8 $_345 \/ agent $_345 skc13 skc15 % 0.18/0.46 |- agent skc12 skc13 skc15 % 0.18/0.46 |- ~accessible_world skc12 $V \/ agent $V skc13 skc15 % 0.18/0.46 |- ~accessible_world skc8 $_353 \/ theme $_353 skc13 skc12 % 0.18/0.46 |- theme skc12 skc13 skc12 % 0.18/0.46 |- ~accessible_world skc12 $V \/ theme $V skc13 skc12 % 0.18/0.46 |- ~accessible_world skc8 $_359 \/ be $_359 skc9 skc10 skc10 % 0.18/0.46 |- be skc12 skc9 skc10 skc10 % 0.18/0.46 |- ~accessible_world skc12 $V \/ be $V skc9 skc10 skc10 % 0.18/0.46 |- ~forename skc12 $_367 \/ ~of skc12 $_367 skc10 \/ $_367 = skc11 % 0.18/0.46 |- ~forename skc12 $_367 \/ ~of skc12 $_367 skc15 \/ $_367 = skc14 % 0.18/0.46 |- ~forename skc8 $_367 \/ ~of skc8 $_367 skc10 \/ $_367 = skc11 % 0.18/0.46 |- ~forename skc8 $_367 \/ ~of skc8 $_367 skc15 \/ $_367 = skc14 % 0.18/0.46 |- ~agent skc12 skc13 $_377 \/ ~proposition skc12 $_375 \/ % 0.18/0.46 ~theme skc12 skc13 $_375 \/ skc12 = $_375 % 0.18/0.46 |- ~agent skc8 skc13 $_377 \/ ~proposition skc8 $_375 \/ % 0.18/0.46 ~theme skc8 skc13 $_375 \/ skc12 = $_375 % 0.18/0.46 |- ~agent skc12 $_386 $_387 \/ ~agent skc12 skc13 $_387 \/ % 0.18/0.46 ~proposition skc12 $_384 \/ ~theme skc12 $_386 $_384 \/ % 0.18/0.46 ~think_believe_consider skc12 $_386 \/ skc12 = $_384 % 0.18/0.46 |- ~agent skc8 $_386 $_387 \/ ~agent skc8 skc13 $_387 \/ % 0.18/0.46 ~proposition skc8 $_384 \/ ~theme skc8 $_386 $_384 \/ % 0.18/0.46 ~think_believe_consider skc8 $_386 \/ skc12 = $_384 % 0.18/0.46 SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.18/0.46 %------------------------------------------------------------------------------