%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : NLP138-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n018.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:15:19 EDT 2022 % Result : Satisfiable 0.12s 0.38s % Output : Saturation 0.12s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : NLP138-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 : n018.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 : Fri Jul 1 10:25:17 EDT 2022 % 0.12/0.33 % CPUTime : % 0.12/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.12/0.38 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.12/0.38 % 0.12/0.38 SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.12/0.38 |- actual_world skc33 % 0.12/0.38 |- actual_world skc13 % 0.12/0.38 |- old skc33 skc39 \/ ssSkC0 % 0.12/0.38 |- dirty skc33 skc39 \/ ssSkC0 % 0.12/0.38 |- ssSkC0 \/ white skc33 skc39 % 0.12/0.38 |- chevy skc33 skc39 \/ ssSkC0 % 0.12/0.38 |- barrel skc33 skc35 \/ ssSkC0 % 0.12/0.38 |- present skc33 skc35 \/ ssSkC0 % 0.12/0.38 |- event skc33 skc35 \/ ssSkC0 % 0.12/0.38 |- hollywood_placename skc33 skc37 \/ ssSkC0 % 0.12/0.38 |- placename skc33 skc37 \/ ssSkC0 % 0.12/0.38 |- city skc33 skc38 \/ ssSkC0 % 0.12/0.38 |- ssSkC0 \/ street skc33 skc36 % 0.12/0.38 |- lonely skc33 skc36 \/ ssSkC0 % 0.12/0.38 |- ssSkC0 \/ ssSkP0 skc34 skc33 % 0.12/0.38 |- ssSkC0 \/ two skc33 skc34 % 0.12/0.38 |- group skc33 skc34 \/ ssSkC0 % 0.12/0.38 |- ~ssSkC0 \/ city skc13 skc17 % 0.12/0.38 |- ~ssSkC0 \/ chevy skc13 skc17 % 0.12/0.38 |- ~ssSkC0 \/ white skc13 skc17 % 0.12/0.38 |- ~ssSkC0 \/ dirty skc13 skc17 % 0.12/0.38 |- ~ssSkC0 \/ old skc13 skc17 % 0.12/0.38 |- ~ssSkC0 \/ placename skc13 skc18 % 0.12/0.38 |- ~ssSkC0 \/ hollywood_placename skc13 skc18 % 0.12/0.38 |- ~ssSkC0 \/ event skc13 skc15 % 0.12/0.38 |- ~ssSkC0 \/ present skc13 skc15 % 0.12/0.38 |- ~ssSkC0 \/ barrel skc13 skc15 % 0.12/0.38 |- ~ssSkC0 \/ lonely skc13 skc16 % 0.12/0.38 |- ~ssSkC0 \/ street skc13 skc16 % 0.12/0.38 |- ~ssSkC0 \/ group skc13 skc14 % 0.12/0.38 |- ~ssSkC0 \/ two skc13 skc14 % 0.12/0.38 |- ~ssSkC0 \/ ssSkP0 skc14 skc13 % 0.12/0.38 |- agent skc33 skc35 skc39 \/ ssSkC0 % 0.12/0.38 |- in skc33 skc35 skc38 \/ ssSkC0 % 0.12/0.38 |- of skc33 skc37 skc38 \/ ssSkC0 % 0.12/0.38 |- down skc33 skc35 skc36 \/ ssSkC0 % 0.12/0.38 |- ~ssSkC0 \/ agent skc13 skc15 skc17 % 0.12/0.38 |- ~ssSkC0 \/ in skc13 skc15 skc17 % 0.12/0.38 |- ~ssSkC0 \/ of skc13 skc18 skc17 % 0.12/0.38 |- ~ssSkC0 \/ down skc13 skc15 skc16 % 0.12/0.38 |- frontseat $V (skf11 $V $W) \/ ssSkP0 $U $V % 0.12/0.38 |- member $V (skf11 $V $U) $U \/ ssSkP0 $U $V % 0.12/0.38 |- ~member skc33 $U skc34 \/ fellow skc33 $U \/ ssSkC0 % 0.12/0.38 |- ~member skc33 $U skc34 \/ ssSkC0 \/ young skc33 $U % 0.12/0.38 |- ~member skc13 $U skc14 \/ ~ssSkC0 \/ fellow skc13 $U % 0.12/0.38 |- ~member skc13 $U skc14 \/ ~ssSkC0 \/ young skc13 $U % 0.12/0.38 |- ~frontseat $U $V \/ ~member $U $V $W \/ ~ssSkP0 $W $U \/ % 0.12/0.38 state $U (skf8 $U $X) % 0.12/0.38 |- ~frontseat $U $V \/ ~member $U $V $W \/ ~ssSkP0 $W $U \/ % 0.12/0.38 in $U (skf7 $V $U) $V % 0.12/0.38 |- ~frontseat $U $V \/ ~member $U $V $W \/ ~ssSkP0 $W $U \/ % 0.12/0.38 be $U (skf8 $U $V) $V (skf7 $V $U) % 0.12/0.39 |- ~be $U $X (skf11 $U $W) $V \/ ~in $U $V (skf11 $U $W) \/ ~state $U $X \/ % 0.12/0.39 ssSkP0 $Y $U % 0.12/0.39 |- ~actual_world $U \/ ~agent $U $W $V \/ ~barrel $U $W \/ ~chevy $U $V \/ % 0.12/0.39 ~city $U $V \/ ~dirty $U $V \/ ~down $U $W $Y \/ ~event $U $W \/ % 0.12/0.39 ~group $U $Z \/ ~hollywood_placename $U $X \/ ~in $U $W $V \/ % 0.12/0.39 ~lonely $U $Y \/ ~of $U $X $V \/ ~old $U $V \/ ~placename $U $X \/ % 0.12/0.39 ~present $U $W \/ ~ssSkP0 $Z $U \/ ~street $U $Y \/ ~two $U $Z \/ % 0.12/0.39 ~white $U $V \/ member $U (skf13 $U $Z) $Z \/ ssSkC0 % 0.12/0.39 |- ~actual_world $U \/ ~agent $U $V $W \/ ~barrel $U $V \/ ~chevy $U $W \/ % 0.12/0.39 ~city $U $Y \/ ~dirty $U $W \/ ~down $U $V $Z \/ ~event $U $V \/ % 0.12/0.39 ~group $U $X1 \/ ~hollywood_placename $U $X \/ ~in $U $V $Y \/ % 0.12/0.39 ~lonely $U $Z \/ ~of $U $X $Y \/ ~old $U $W \/ ~placename $U $X \/ % 0.12/0.39 ~present $U $V \/ ~ssSkC0 \/ ~ssSkP0 $X1 $U \/ ~street $U $Z \/ % 0.12/0.39 ~two $U $X1 \/ ~white $U $W \/ member $U (skf6 $U $X1) $X1 % 0.12/0.39 |- ~actual_world $U \/ ~agent $U $W $V \/ ~barrel $U $W \/ ~chevy $U $V \/ % 0.12/0.39 ~city $U $V \/ ~dirty $U $V \/ ~down $U $W $Y \/ ~event $U $W \/ % 0.12/0.39 ~fellow $U (skf13 $U $Z) \/ ~group $U $X1 \/ % 0.12/0.39 ~hollywood_placename $U $X \/ ~in $U $W $V \/ ~lonely $U $Y \/ % 0.12/0.39 ~of $U $X $V \/ ~old $U $V \/ ~placename $U $X \/ ~present $U $W \/ % 0.12/0.39 ~ssSkP0 $X1 $U \/ ~street $U $Y \/ ~two $U $X1 \/ ~white $U $V \/ % 0.12/0.39 ~young $U (skf13 $U $Z) \/ ssSkC0 % 0.12/0.39 |- ~actual_world $U \/ ~agent $U $V $W \/ ~barrel $U $V \/ ~chevy $U $W \/ % 0.12/0.39 ~city $U $Y \/ ~dirty $U $W \/ ~down $U $V $Z \/ ~event $U $V \/ % 0.12/0.39 ~fellow $U (skf6 $U $X2) \/ ~group $U $X1 \/ % 0.12/0.39 ~hollywood_placename $U $X \/ ~in $U $V $Y \/ ~lonely $U $Z \/ % 0.12/0.39 ~of $U $X $Y \/ ~old $U $W \/ ~placename $U $X \/ ~present $U $V \/ % 0.12/0.39 ~ssSkC0 \/ ~ssSkP0 $X1 $U \/ ~street $U $Z \/ ~two $U $X1 \/ % 0.12/0.39 ~white $U $W \/ ~young $U (skf6 $U $X2) % 0.12/0.39 |- ~agent skc33 $_26 skc38 \/ ~barrel skc33 $_26 \/ ~chevy skc33 skc38 \/ % 0.12/0.39 ~city skc33 skc38 \/ ~dirty skc33 skc38 \/ ~down skc33 $_26 $_28 \/ % 0.12/0.39 ~event skc33 $_26 \/ ~group skc33 $_29 \/ % 0.12/0.39 ~hollywood_placename skc33 skc37 \/ ~in skc33 $_26 skc38 \/ % 0.12/0.39 ~lonely skc33 $_28 \/ ~old skc33 skc38 \/ ~placename skc33 skc37 \/ % 0.12/0.39 ~present skc33 $_26 \/ ~ssSkP0 $_29 skc33 \/ ~street skc33 $_28 \/ % 0.12/0.39 ~two skc33 $_29 \/ ~white skc33 skc38 \/ % 0.12/0.39 member skc33 (skf13 skc33 $_29) $_29 \/ ssSkC0 % 0.12/0.39 |- ~agent skc33 skc35 skc38 \/ ~barrel skc33 skc35 \/ ~chevy skc33 skc38 \/ % 0.12/0.39 ~city skc33 skc38 \/ ~dirty skc33 skc38 \/ ~down skc33 skc35 $_31 \/ % 0.12/0.39 ~event skc33 skc35 \/ ~group skc33 $_32 \/ % 0.12/0.39 ~hollywood_placename skc33 skc37 \/ ~lonely skc33 $_31 \/ % 0.12/0.39 ~old skc33 skc38 \/ ~placename skc33 skc37 \/ ~present skc33 skc35 \/ % 0.12/0.39 ~ssSkP0 $_32 skc33 \/ ~street skc33 $_31 \/ ~two skc33 $_32 \/ % 0.12/0.39 ~white skc33 skc38 \/ member skc33 (skf13 skc33 $_32) $_32 \/ ssSkC0 % 0.12/0.39 |- ~agent skc33 skc35 skc38 \/ ~barrel skc33 skc35 \/ ~chevy skc33 skc38 \/ % 0.12/0.39 ~city skc33 skc38 \/ ~dirty skc33 skc38 \/ ~event skc33 skc35 \/ % 0.12/0.39 ~group skc33 $_34 \/ ~hollywood_placename skc33 skc37 \/ % 0.12/0.39 ~lonely skc33 skc36 \/ ~old skc33 skc38 \/ ~placename skc33 skc37 \/ % 0.12/0.39 ~present skc33 skc35 \/ ~ssSkP0 $_34 skc33 \/ ~street skc33 skc36 \/ % 0.12/0.39 ~two skc33 $_34 \/ ~white skc33 skc38 \/ % 0.12/0.39 member skc33 (skf13 skc33 $_34) $_34 \/ ssSkC0 % 0.12/0.39 SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.12/0.39 %------------------------------------------------------------------------------