%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : NLP223-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n021.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:15 EDT 2022 % Result : Satisfiable 0.21s 0.42s % Output : Saturation 0.21s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : NLP223-1 : TPTP v8.1.0. Released v2.4.0. % 0.04/0.13 % Command : metis --show proof --show saturation %s % 0.14/0.34 % Computer : n021.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 600 % 0.14/0.34 % DateTime : Fri Jul 1 08:56:28 EDT 2022 % 0.14/0.34 % CPUTime : % 0.14/0.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.21/0.42 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.21/0.42 % 0.21/0.42 SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.21/0.42 |- actual_world skc27 % 0.21/0.42 |- actual_world skc16 % 0.21/0.42 |- proposition skc27 skc31 \/ ssSkC0 % 0.21/0.42 |- accessible_world skc27 skc31 \/ ssSkC0 % 0.21/0.42 |- ssSkC0 \/ think_believe_consider skc27 skc32 % 0.21/0.42 |- present skc27 skc32 \/ ssSkC0 % 0.21/0.42 |- event skc27 skc32 \/ ssSkC0 % 0.21/0.42 |- ssSkC0 \/ vincent_forename skc27 skc33 % 0.21/0.42 |- forename skc27 skc33 \/ ssSkC0 % 0.21/0.42 |- man skc27 skc34 \/ ssSkC0 % 0.21/0.42 |- ssSkC0 \/ state skc27 skc28 % 0.21/0.42 |- man skc27 skc29 \/ ssSkC0 % 0.21/0.42 |- forename skc27 skc30 \/ ssSkC0 % 0.21/0.42 |- jules_forename skc27 skc30 \/ ssSkC0 % 0.21/0.42 |- ~ssSkC0 \/ state skc16 skc17 % 0.21/0.42 |- ~ssSkC0 \/ man skc16 skc18 % 0.21/0.42 |- ~ssSkC0 \/ accessible_world skc16 skc19 % 0.21/0.42 |- ~ssSkC0 \/ proposition skc16 skc19 % 0.21/0.42 |- ~ssSkC0 \/ event skc16 skc20 % 0.21/0.42 |- ~ssSkC0 \/ present skc16 skc20 % 0.21/0.42 |- ~ssSkC0 \/ think_believe_consider skc16 skc20 % 0.21/0.42 |- ~ssSkC0 \/ forename skc16 skc21 % 0.21/0.42 |- ~ssSkC0 \/ vincent_forename skc16 skc21 % 0.21/0.42 |- ~ssSkC0 \/ man skc16 skc22 % 0.21/0.42 |- ~ssSkC0 \/ forename skc16 skc23 % 0.21/0.42 |- ~ssSkC0 \/ jules_forename skc16 skc23 % 0.21/0.42 |- ssSkC0 \/ theme skc27 skc32 skc31 % 0.21/0.42 |- agent skc27 skc32 skc34 \/ ssSkC0 % 0.21/0.42 |- of skc27 skc33 skc34 \/ ssSkC0 % 0.21/0.42 |- of skc27 skc30 skc29 \/ ssSkC0 % 0.21/0.42 |- ~ssSkC0 \/ theme skc16 skc20 skc19 % 0.21/0.42 |- ~ssSkC0 \/ of skc16 skc21 skc22 % 0.21/0.42 |- ~ssSkC0 \/ agent skc16 skc20 skc22 % 0.21/0.42 |- ~ssSkC0 \/ of skc16 skc23 skc22 % 0.21/0.42 |- be skc27 skc28 skc29 skc29 \/ ssSkC0 % 0.21/0.42 |- ~ssSkC0 \/ be skc16 skc17 skc22 skc18 % 0.21/0.42 |- ~man skc31 $U \/ event skc31 (skf11 $V) \/ ssSkC0 % 0.21/0.42 |- ~man skc31 $U \/ present skc31 (skf11 $V) \/ ssSkC0 % 0.21/0.42 |- ~man skc31 $U \/ smoke skc31 (skf11 $V) \/ ssSkC0 % 0.21/0.42 |- ~man skc19 $U \/ ~ssSkC0 \/ event skc19 (skf7 $V) % 0.21/0.42 |- ~man skc19 $U \/ ~ssSkC0 \/ present skc19 (skf7 $V) % 0.21/0.42 |- ~man skc19 $U \/ ~ssSkC0 \/ smoke skc19 (skf7 $V) % 0.21/0.42 |- ~man skc31 $U \/ agent skc31 (skf11 $U) $U \/ ssSkC0 % 0.21/0.42 |- ~man skc19 $U \/ ~ssSkC0 \/ agent skc19 (skf7 $U) $U % 0.21/0.42 |- ~accessible_world $U $X \/ ~actual_world $U \/ ~agent $U $Y $X1 \/ % 0.21/0.42 ~be $U $V $X1 $W \/ ~event $U $Y \/ ~forename $U $X2 \/ % 0.21/0.42 ~forename $U $Z \/ ~jules_forename $U $X2 \/ ~man $U $W \/ % 0.21/0.42 ~man $U $X1 \/ ~of $U $X2 $X1 \/ ~of $U $Z $X1 \/ ~present $U $Y \/ % 0.21/0.42 ~proposition $U $X \/ ~state $U $V \/ ~theme $U $Y $X \/ % 0.21/0.42 ~think_believe_consider $U $Y \/ ~vincent_forename $U $Z \/ % 0.21/0.42 man $X (skf13 $X) \/ ssSkC0 % 0.21/0.42 |- ~accessible_world $U $V \/ ~actual_world $U \/ ~agent $U $W $Y \/ % 0.21/0.42 ~be $U $Z $X1 $X1 \/ ~event $U $W \/ ~forename $U $X \/ % 0.21/0.42 ~forename $U $X2 \/ ~jules_forename $U $X2 \/ ~man $U $X1 \/ % 0.21/0.42 ~man $U $Y \/ ~of $U $X $Y \/ ~of $U $X2 $X1 \/ ~present $U $W \/ % 0.21/0.42 ~proposition $U $V \/ ~ssSkC0 \/ ~state $U $Z \/ ~theme $U $W $V \/ % 0.21/0.42 ~think_believe_consider $U $W \/ ~vincent_forename $U $X \/ % 0.21/0.42 man $V (skf9 $V) % 0.21/0.42 |- ~accessible_world $U $X \/ ~actual_world $U \/ ~agent $U $Z $X2 \/ % 0.21/0.42 ~agent $X $Y (skf13 $X) \/ ~be $U $V $X2 $W \/ ~event $U $Z \/ % 0.21/0.42 ~event $X $Y \/ ~forename $U $X1 \/ ~forename $U $X3 \/ % 0.21/0.42 ~jules_forename $U $X3 \/ ~man $U $W \/ ~man $U $X2 \/ ~of $U $X1 $X2 \/ % 0.21/0.42 ~of $U $X3 $X2 \/ ~present $U $Z \/ ~present $X $Y \/ % 0.21/0.42 ~proposition $U $X \/ ~smoke $X $Y \/ ~state $U $V \/ ~theme $U $Z $X \/ % 0.21/0.42 ~think_believe_consider $U $Z \/ ~vincent_forename $U $X1 \/ ssSkC0 % 0.21/0.42 |- ~accessible_world $U $V \/ ~actual_world $U \/ ~agent $U $X $Z \/ % 0.21/0.42 ~agent $V $W (skf9 $V) \/ ~be $U $X1 $X2 $X2 \/ ~event $U $X \/ % 0.21/0.42 ~event $V $W \/ ~forename $U $X3 \/ ~forename $U $Y \/ % 0.21/0.42 ~jules_forename $U $X3 \/ ~man $U $X2 \/ ~man $U $Z \/ ~of $U $X3 $X2 \/ % 0.21/0.42 ~of $U $Y $Z \/ ~present $U $X \/ ~present $V $W \/ % 0.21/0.42 ~proposition $U $V \/ ~smoke $V $W \/ ~ssSkC0 \/ ~state $U $X1 \/ % 0.21/0.42 ~theme $U $X $V \/ ~think_believe_consider $U $X \/ % 0.21/0.42 ~vincent_forename $U $Y % 0.21/0.42 |- ~accessible_world $U $X \/ ~actual_world $U \/ ~agent $U $Y $X1 \/ % 0.21/0.42 ~be $U $V $X1 $W \/ ~event $U $Y \/ ~forename $U $Z \/ % 0.21/0.42 ~jules_forename $U $Z \/ ~man $U $W \/ ~man $U $X1 \/ ~of $U $Z $X1 \/ % 0.21/0.42 ~present $U $Y \/ ~proposition $U $X \/ ~state $U $V \/ % 0.21/0.42 ~theme $U $Y $X \/ ~think_believe_consider $U $Y \/ % 0.21/0.42 ~vincent_forename $U $Z \/ man $X (skf13 $X) \/ ssSkC0 % 0.21/0.42 |- ~accessible_world $U $V \/ ~actual_world $U \/ ~agent $U $W $X1 \/ % 0.21/0.42 ~be $U $Z $X1 $X1 \/ ~event $U $W \/ ~forename $U $X2 \/ % 0.21/0.42 ~jules_forename $U $X2 \/ ~man $U $X1 \/ ~of $U $X2 $X1 \/ % 0.21/0.42 ~present $U $W \/ ~proposition $U $V \/ ~ssSkC0 \/ ~state $U $Z \/ % 0.21/0.42 ~theme $U $W $V \/ ~think_believe_consider $U $W \/ % 0.21/0.42 ~vincent_forename $U $X2 \/ man $V (skf9 $V) % 0.21/0.43 |- ~accessible_world $X $X \/ ~actual_world $X \/ % 0.21/0.43 ~agent $X $Y (skf13 $X) \/ ~be $X $V (skf13 $X) $W \/ ~event $X $Y \/ % 0.21/0.43 ~forename $X $X1 \/ ~forename $X $X3 \/ ~jules_forename $X $X3 \/ % 0.21/0.43 ~man $X $W \/ ~man $X (skf13 $X) \/ ~of $X $X1 (skf13 $X) \/ % 0.21/0.43 ~of $X $X3 (skf13 $X) \/ ~present $X $Y \/ ~proposition $X $X \/ % 0.21/0.43 ~smoke $X $Y \/ ~state $X $V \/ ~theme $X $Y $X \/ % 0.21/0.43 ~think_believe_consider $X $Y \/ ~vincent_forename $X $X1 \/ ssSkC0 % 0.21/0.43 |- ~accessible_world $U $X \/ ~actual_world $U \/ ~agent $U $Z $X2 \/ % 0.21/0.43 ~agent $X $Y (skf13 $X) \/ ~be $U $V $X2 $W \/ ~event $U $Z \/ % 0.21/0.43 ~event $X $Y \/ ~forename $U $X3 \/ ~jules_forename $U $X3 \/ % 0.21/0.43 ~man $U $W \/ ~man $U $X2 \/ ~of $U $X3 $X2 \/ ~present $U $Z \/ % 0.21/0.43 ~present $X $Y \/ ~proposition $U $X \/ ~smoke $X $Y \/ ~state $U $V \/ % 0.21/0.43 ~theme $U $Z $X \/ ~think_believe_consider $U $Z \/ % 0.21/0.43 ~vincent_forename $U $X3 \/ ssSkC0 % 0.21/0.43 |- ~accessible_world $X $X \/ ~actual_world $X \/ % 0.21/0.43 ~agent $X $Y (skf13 $X) \/ ~be $X $V (skf13 $X) $W \/ ~event $X $Y \/ % 0.21/0.43 ~forename $X $X3 \/ ~jules_forename $X $X3 \/ ~man $X $W \/ % 0.21/0.43 ~man $X (skf13 $X) \/ ~of $X $X3 (skf13 $X) \/ ~present $X $Y \/ % 0.21/0.43 ~proposition $X $X \/ ~smoke $X $Y \/ ~state $X $V \/ ~theme $X $Y $X \/ % 0.21/0.43 ~think_believe_consider $X $Y \/ ~vincent_forename $X $X3 \/ ssSkC0 % 0.21/0.43 |- ~accessible_world $V $V \/ ~actual_world $V \/ ~agent $V $W (skf9 $V) \/ % 0.21/0.43 ~be $V $X1 $X2 $X2 \/ ~event $V $W \/ ~forename $V $X3 \/ % 0.21/0.43 ~forename $V $Y \/ ~jules_forename $V $X3 \/ ~man $V $X2 \/ % 0.21/0.43 ~man $V (skf9 $V) \/ ~of $V $X3 $X2 \/ ~of $V $Y (skf9 $V) \/ % 0.21/0.43 ~present $V $W \/ ~proposition $V $V \/ ~smoke $V $W \/ ~ssSkC0 \/ % 0.21/0.43 ~state $V $X1 \/ ~theme $V $W $V \/ ~think_believe_consider $V $W \/ % 0.21/0.43 ~vincent_forename $V $Y % 0.21/0.43 |- ~accessible_world $U $V \/ ~actual_world $U \/ ~agent $U $X $Z \/ % 0.21/0.43 ~agent $V $W (skf9 $V) \/ ~be $U $X1 $Z $Z \/ ~event $U $X \/ % 0.21/0.43 ~event $V $W \/ ~forename $U $Y \/ ~jules_forename $U $Y \/ % 0.21/0.43 ~man $U $Z \/ ~of $U $Y $Z \/ ~present $U $X \/ ~present $V $W \/ % 0.21/0.43 ~proposition $U $V \/ ~smoke $V $W \/ ~ssSkC0 \/ ~state $U $X1 \/ % 0.21/0.43 ~theme $U $X $V \/ ~think_believe_consider $U $X \/ % 0.21/0.43 ~vincent_forename $U $Y % 0.21/0.43 |- ~accessible_world $V $V \/ ~actual_world $V \/ ~agent $V $W (skf9 $V) \/ % 0.21/0.43 ~be $V $X1 (skf9 $V) (skf9 $V) \/ ~event $V $W \/ ~forename $V $Y \/ % 0.21/0.43 ~jules_forename $V $Y \/ ~man $V (skf9 $V) \/ ~of $V $Y (skf9 $V) \/ % 0.21/0.43 ~present $V $W \/ ~proposition $V $V \/ ~smoke $V $W \/ ~ssSkC0 \/ % 0.21/0.43 ~state $V $X1 \/ ~theme $V $W $V \/ ~think_believe_consider $V $W \/ % 0.21/0.43 ~vincent_forename $V $Y % 0.21/0.43 |- ~accessible_world skc27 $_32 \/ ~agent skc27 $_34 skc29 \/ % 0.21/0.43 ~event skc27 $_34 \/ ~forename skc27 $_35 \/ % 0.21/0.43 ~jules_forename skc27 $_35 \/ ~man skc27 skc29 \/ % 0.21/0.43 ~of skc27 $_35 skc29 \/ ~present skc27 $_34 \/ % 0.21/0.43 ~proposition skc27 $_32 \/ ~state skc27 skc28 \/ % 0.21/0.43 ~theme skc27 $_34 $_32 \/ ~think_believe_consider skc27 $_34 \/ % 0.21/0.43 ~vincent_forename skc27 $_35 \/ man $_32 (skf13 $_32) \/ ssSkC0 % 0.21/0.43 |- ~accessible_world skc27 skc31 \/ ~agent skc27 skc32 skc29 \/ % 0.21/0.43 ~event skc27 skc32 \/ ~forename skc27 $_38 \/ % 0.21/0.43 ~jules_forename skc27 $_38 \/ ~man skc27 skc29 \/ % 0.21/0.43 ~of skc27 $_38 skc29 \/ ~present skc27 skc32 \/ % 0.21/0.43 ~proposition skc27 skc31 \/ ~state skc27 skc28 \/ % 0.21/0.43 ~think_believe_consider skc27 skc32 \/ ~vincent_forename skc27 $_38 \/ % 0.21/0.43 man skc31 (skf13 skc31) \/ ssSkC0 % 0.21/0.43 |- ~accessible_world skc27 skc31 \/ ~agent skc27 skc32 skc29 \/ % 0.21/0.43 ~event skc27 skc32 \/ ~forename skc27 skc30 \/ % 0.21/0.43 ~jules_forename skc27 skc30 \/ ~man skc27 skc29 \/ % 0.21/0.43 ~present skc27 skc32 \/ ~proposition skc27 skc31 \/ % 0.21/0.43 ~state skc27 skc28 \/ ~think_believe_consider skc27 skc32 \/ % 0.21/0.43 ~vincent_forename skc27 skc30 \/ man skc31 (skf13 skc31) \/ ssSkC0 % 0.21/0.43 |- ~accessible_world skc27 $_62 \/ ~agent skc27 $_65 skc29 \/ % 0.21/0.43 ~event skc27 $_65 \/ ~forename skc27 $_64 \/ ~forename skc27 $_66 \/ % 0.21/0.43 ~jules_forename skc27 $_64 \/ ~man skc27 skc29 \/ % 0.21/0.43 ~of skc27 $_64 skc29 \/ ~of skc27 $_66 skc29 \/ ~present skc27 $_65 \/ % 0.21/0.43 ~proposition skc27 $_62 \/ ~state skc27 skc28 \/ % 0.21/0.43 ~theme skc27 $_65 $_62 \/ ~think_believe_consider skc27 $_65 \/ % 0.21/0.43 ~vincent_forename skc27 $_66 \/ man $_62 (skf13 $_62) \/ ssSkC0 % 0.21/0.43 |- ~accessible_world skc27 skc31 \/ ~agent skc27 skc32 skc29 \/ % 0.21/0.43 ~event skc27 skc32 \/ ~forename skc27 $_68 \/ ~forename skc27 $_70 \/ % 0.21/0.43 ~jules_forename skc27 $_68 \/ ~man skc27 skc29 \/ % 0.21/0.43 ~of skc27 $_68 skc29 \/ ~of skc27 $_70 skc29 \/ ~present skc27 skc32 \/ % 0.21/0.43 ~proposition skc27 skc31 \/ ~state skc27 skc28 \/ % 0.21/0.43 ~think_believe_consider skc27 skc32 \/ ~vincent_forename skc27 $_70 \/ % 0.21/0.43 man skc31 (skf13 skc31) \/ ssSkC0 % 0.21/0.43 |- ~accessible_world skc27 skc31 \/ ~agent skc27 skc32 skc29 \/ % 0.21/0.43 ~event skc27 skc32 \/ ~forename skc27 $_72 \/ ~forename skc27 skc30 \/ % 0.21/0.43 ~jules_forename skc27 skc30 \/ ~man skc27 skc29 \/ % 0.21/0.43 ~of skc27 $_72 skc29 \/ ~present skc27 skc32 \/ % 0.21/0.43 ~proposition skc27 skc31 \/ ~state skc27 skc28 \/ % 0.21/0.43 ~think_believe_consider skc27 skc32 \/ ~vincent_forename skc27 $_72 \/ % 0.21/0.43 man skc31 (skf13 skc31) \/ ssSkC0 % 0.21/0.43 |- ~accessible_world skc27 skc31 \/ ~agent skc27 skc32 skc29 \/ % 0.21/0.43 ~event skc27 skc32 \/ ~forename skc27 $_71 \/ ~forename skc27 skc30 \/ % 0.21/0.43 ~jules_forename skc27 $_71 \/ ~man skc27 skc29 \/ % 0.21/0.43 ~of skc27 $_71 skc29 \/ ~present skc27 skc32 \/ % 0.21/0.43 ~proposition skc27 skc31 \/ ~state skc27 skc28 \/ % 0.21/0.43 ~think_believe_consider skc27 skc32 \/ ~vincent_forename skc27 skc30 \/ % 0.21/0.43 man skc31 (skf13 skc31) \/ ssSkC0 % 0.21/0.43 |- ~accessible_world skc27 $_86 \/ ~agent $_86 $_89 (skf13 $_86) \/ % 0.21/0.43 ~agent skc27 $_90 skc29 \/ ~event $_86 $_89 \/ ~event skc27 $_90 \/ % 0.21/0.43 ~forename skc27 $_88 \/ ~jules_forename skc27 $_88 \/ % 0.21/0.43 ~man skc27 skc29 \/ ~of skc27 $_88 skc29 \/ ~present $_86 $_89 \/ % 0.21/0.43 ~present skc27 $_90 \/ ~proposition skc27 $_86 \/ ~smoke $_86 $_89 \/ % 0.21/0.43 ~state skc27 skc28 \/ ~theme skc27 $_90 $_86 \/ % 0.21/0.43 ~think_believe_consider skc27 $_90 \/ ~vincent_forename skc27 $_88 \/ % 0.21/0.43 ssSkC0 % 0.21/0.43 |- ~accessible_world skc27 $_98 \/ ~agent $_98 $_102 (skf13 $_98) \/ % 0.21/0.43 ~agent skc27 $_103 skc29 \/ ~event $_98 $_102 \/ ~event skc27 $_103 \/ % 0.21/0.43 ~forename skc27 $_101 \/ ~forename skc27 $_99 \/ % 0.21/0.43 ~jules_forename skc27 $_101 \/ ~man skc27 skc29 \/ % 0.21/0.43 ~of skc27 $_101 skc29 \/ ~of skc27 $_99 skc29 \/ ~present $_98 $_102 \/ % 0.21/0.43 ~present skc27 $_103 \/ ~proposition skc27 $_98 \/ ~smoke $_98 $_102 \/ % 0.21/0.43 ~state skc27 skc28 \/ ~theme skc27 $_103 $_98 \/ % 0.21/0.43 ~think_believe_consider skc27 $_103 \/ ~vincent_forename skc27 $_99 \/ % 0.21/0.43 ssSkC0 % 0.21/0.43 SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.21/0.43 %------------------------------------------------------------------------------