%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : NLP006-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n020.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:13:40 EDT 2022 % Result : Satisfiable 0.20s 0.41s % Output : Saturation 0.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NLP006-1 : TPTP v8.1.0. Released v2.4.0. % 0.03/0.13 % Command : metis --show proof --show saturation %s % 0.13/0.34 % Computer : n020.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Fri Jul 1 00:58:30 EDT 2022 % 0.13/0.34 % CPUTime : % 0.13/0.35 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.20/0.41 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.20/0.41 % 0.20/0.41 SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.20/0.41 |- city skc29 % 0.20/0.41 |- event skc28 % 0.20/0.41 |- old skc27 % 0.20/0.41 |- street skc26 % 0.20/0.41 |- front skc25 % 0.20/0.41 |- seat skc24 % 0.20/0.41 |- fellow skc23 % 0.20/0.41 |- young skc22 % 0.20/0.41 |- city skc21 % 0.20/0.41 |- event skc20 % 0.20/0.41 |- old skc19 % 0.20/0.41 |- street skc18 % 0.20/0.41 |- seat skc17 % 0.20/0.41 |- young skc16 % 0.20/0.41 |- fellow skc15 % 0.20/0.41 |- lonely skc26 \/ ssSkC0 % 0.20/0.41 |- ssSkC0 \/ way skc26 % 0.20/0.41 |- chevy skc27 \/ ssSkC0 % 0.20/0.41 |- car skc27 \/ ssSkC0 % 0.20/0.41 |- ssSkC0 \/ white skc27 % 0.20/0.41 |- dirty skc27 \/ ssSkC0 % 0.20/0.41 |- hollywood skc29 \/ ssSkC0 % 0.20/0.41 |- seat skc25 \/ ssSkC0 % 0.20/0.41 |- furniture skc25 \/ ssSkC0 % 0.20/0.41 |- fellow skc22 \/ ssSkC0 % 0.20/0.41 |- man skc22 \/ ssSkC0 % 0.20/0.41 |- front skc24 \/ ssSkC0 % 0.20/0.41 |- furniture skc24 \/ ssSkC0 % 0.20/0.41 |- ssSkC0 \/ young skc23 % 0.20/0.41 |- man skc23 \/ ssSkC0 % 0.20/0.41 |- ~ssSkC0 \/ lonely skc18 % 0.20/0.41 |- ~ssSkC0 \/ way skc18 % 0.20/0.41 |- ~ssSkC0 \/ chevy skc19 % 0.20/0.41 |- ~ssSkC0 \/ car skc19 % 0.20/0.41 |- ~ssSkC0 \/ white skc19 % 0.20/0.41 |- ~ssSkC0 \/ dirty skc19 % 0.20/0.41 |- ~ssSkC0 \/ hollywood skc21 % 0.20/0.41 |- ~ssSkC0 \/ young skc15 % 0.20/0.41 |- ~ssSkC0 \/ man skc15 % 0.20/0.41 |- ~ssSkC0 \/ fellow skc16 % 0.20/0.41 |- ~ssSkC0 \/ man skc16 % 0.20/0.41 |- ~ssSkC0 \/ front skc17 % 0.20/0.41 |- ~ssSkC0 \/ furniture skc17 % 0.20/0.41 |- down skc28 skc26 \/ ssSkC0 % 0.20/0.41 |- barrel skc28 skc27 \/ ssSkC0 % 0.20/0.41 |- in skc28 skc29 \/ ssSkC0 % 0.20/0.41 |- in skc22 skc25 \/ ssSkC0 % 0.20/0.41 |- in skc23 skc24 \/ ssSkC0 % 0.20/0.41 |- ~ssSkC0 \/ down skc20 skc18 % 0.20/0.41 |- ~ssSkC0 \/ barrel skc20 skc19 % 0.20/0.41 |- ~ssSkC0 \/ in skc20 skc21 % 0.20/0.41 |- ~ssSkC0 \/ in skc15 skc17 % 0.20/0.41 |- ~ssSkC0 \/ in skc16 skc17 % 0.20/0.41 |- ~(skc23 = skc22) \/ ssSkC0 % 0.20/0.41 |- ~(skc16 = skc15) \/ ~ssSkC0 % 0.20/0.41 |- ~barrel $W $V \/ ~car $V \/ ~chevy $V \/ ~city $X \/ ~dirty $V \/ % 0.20/0.41 ~down $W $U \/ ~event $W \/ ~fellow $Y \/ ~fellow $Z \/ ~front $X1 \/ % 0.20/0.41 ~furniture $X1 \/ ~hollywood $X \/ ~in $W $X \/ ~in $Y $X1 \/ % 0.20/0.41 ~in $Z $X1 \/ ~lonely $U \/ ~man $Y \/ ~man $Z \/ ~old $V \/ % 0.20/0.41 ~seat $X1 \/ ~street $U \/ ~way $U \/ ~white $V \/ ~young $Y \/ % 0.20/0.41 ~young $Z \/ $Z = $Y \/ ssSkC0 % 0.20/0.41 |- ~barrel $W $V \/ ~car $V \/ ~chevy $V \/ ~city $X \/ ~dirty $V \/ % 0.20/0.41 ~down $W $U \/ ~event $W \/ ~fellow $X1 \/ ~fellow $Z \/ ~front $X2 \/ % 0.20/0.41 ~front $Y \/ ~furniture $X2 \/ ~furniture $Y \/ ~hollywood $X \/ % 0.20/0.41 ~in $W $X \/ ~in $X1 $X2 \/ ~in $Z $Y \/ ~lonely $U \/ ~man $X1 \/ % 0.20/0.41 ~man $Z \/ ~old $V \/ ~seat $X2 \/ ~seat $Y \/ ~ssSkC0 \/ ~street $U \/ % 0.20/0.41 ~way $U \/ ~white $V \/ ~young $X1 \/ ~young $Z \/ $X1 = $Z % 0.20/0.41 |- ~barrel $Y $V \/ ~car $V \/ ~chevy $V \/ ~city $X1 \/ ~dirty $V \/ % 0.20/0.41 ~down $Y $U \/ ~event $Y \/ ~fellow $Y \/ ~fellow $Z \/ ~front $X1 \/ % 0.20/0.41 ~furniture $X1 \/ ~hollywood $X1 \/ ~in $Y $X1 \/ ~in $Z $X1 \/ % 0.20/0.41 ~lonely $U \/ ~man $Y \/ ~man $Z \/ ~old $V \/ ~seat $X1 \/ % 0.20/0.41 ~street $U \/ ~way $U \/ ~white $V \/ ~young $Y \/ ~young $Z \/ % 0.20/0.41 $Z = $Y \/ ssSkC0 % 0.20/0.41 |- ~barrel $X1 $V \/ ~car $V \/ ~chevy $V \/ ~city $X2 \/ ~dirty $V \/ % 0.20/0.41 ~down $X1 $U \/ ~event $X1 \/ ~fellow $X1 \/ ~fellow $Z \/ ~front $X2 \/ % 0.20/0.41 ~front $Y \/ ~furniture $X2 \/ ~furniture $Y \/ ~hollywood $X2 \/ % 0.20/0.41 ~in $X1 $X2 \/ ~in $Z $Y \/ ~lonely $U \/ ~man $X1 \/ ~man $Z \/ % 0.20/0.41 ~old $V \/ ~seat $X2 \/ ~seat $Y \/ ~ssSkC0 \/ ~street $U \/ ~way $U \/ % 0.20/0.41 ~white $V \/ ~young $X1 \/ ~young $Z \/ $X1 = $Z % 0.20/0.41 |- ~barrel skc22 $_1 \/ ~car $_1 \/ ~chevy $_1 \/ ~city skc25 \/ % 0.20/0.41 ~dirty $_1 \/ ~down skc22 $_0 \/ ~event skc22 \/ ~fellow $_4 \/ % 0.20/0.41 ~fellow skc22 \/ ~furniture skc25 \/ ~hollywood skc25 \/ % 0.20/0.41 ~in $_4 skc25 \/ ~lonely $_0 \/ ~man $_4 \/ ~man skc22 \/ ~old $_1 \/ % 0.20/0.41 ~seat skc25 \/ ~street $_0 \/ ~way $_0 \/ ~white $_1 \/ ~young $_4 \/ % 0.20/0.41 $_4 = skc22 \/ ssSkC0 % 0.20/0.41 |- ~barrel skc23 $_1 \/ ~car $_1 \/ ~chevy $_1 \/ ~city skc24 \/ % 0.20/0.41 ~dirty $_1 \/ ~down skc23 $_0 \/ ~event skc23 \/ ~fellow $_4 \/ % 0.20/0.41 ~front skc24 \/ ~furniture skc24 \/ ~hollywood skc24 \/ ~in $_4 skc24 \/ % 0.20/0.41 ~lonely $_0 \/ ~man $_4 \/ ~man skc23 \/ ~old $_1 \/ ~street $_0 \/ % 0.20/0.41 ~way $_0 \/ ~white $_1 \/ ~young $_4 \/ ~young skc23 \/ $_4 = skc23 \/ % 0.20/0.41 ssSkC0 % 0.20/0.41 |- ~barrel skc28 $_1 \/ ~car $_1 \/ ~chevy $_1 \/ ~dirty $_1 \/ % 0.20/0.41 ~down skc28 $_0 \/ ~fellow $_4 \/ ~fellow skc28 \/ ~front skc29 \/ % 0.20/0.41 ~furniture skc29 \/ ~hollywood skc29 \/ ~in $_4 skc29 \/ ~lonely $_0 \/ % 0.20/0.41 ~man $_4 \/ ~man skc28 \/ ~old $_1 \/ ~seat skc29 \/ ~street $_0 \/ % 0.20/0.41 ~way $_0 \/ ~white $_1 \/ ~young $_4 \/ ~young skc28 \/ $_4 = skc28 \/ % 0.20/0.41 ssSkC0 % 0.20/0.41 |- ~barrel $_3 $_1 \/ ~car $_1 \/ ~chevy $_1 \/ ~city skc25 \/ % 0.20/0.41 ~dirty $_1 \/ ~down $_3 $_0 \/ ~event $_3 \/ ~fellow $_3 \/ % 0.20/0.41 ~fellow skc22 \/ ~furniture skc25 \/ ~hollywood skc25 \/ % 0.20/0.41 ~in $_3 skc25 \/ ~lonely $_0 \/ ~man $_3 \/ ~man skc22 \/ ~old $_1 \/ % 0.20/0.41 ~seat skc25 \/ ~street $_0 \/ ~way $_0 \/ ~white $_1 \/ ~young $_3 \/ % 0.20/0.41 skc22 = $_3 \/ ssSkC0 % 0.20/0.41 |- ~barrel $_3 $_1 \/ ~car $_1 \/ ~chevy $_1 \/ ~city skc24 \/ % 0.20/0.41 ~dirty $_1 \/ ~down $_3 $_0 \/ ~event $_3 \/ ~fellow $_3 \/ % 0.20/0.41 ~front skc24 \/ ~furniture skc24 \/ ~hollywood skc24 \/ ~in $_3 skc24 \/ % 0.20/0.41 ~lonely $_0 \/ ~man $_3 \/ ~man skc23 \/ ~old $_1 \/ ~street $_0 \/ % 0.20/0.41 ~way $_0 \/ ~white $_1 \/ ~young $_3 \/ ~young skc23 \/ skc23 = $_3 \/ % 0.20/0.41 ssSkC0 % 0.20/0.42 |- ~barrel $_3 $_1 \/ ~car $_1 \/ ~chevy $_1 \/ ~dirty $_1 \/ % 0.20/0.42 ~down $_3 $_0 \/ ~event $_3 \/ ~fellow $_3 \/ ~fellow skc28 \/ % 0.20/0.42 ~front skc29 \/ ~furniture skc29 \/ ~hollywood skc29 \/ ~in $_3 skc29 \/ % 0.20/0.42 ~lonely $_0 \/ ~man $_3 \/ ~man skc28 \/ ~old $_1 \/ ~seat skc29 \/ % 0.20/0.42 ~street $_0 \/ ~way $_0 \/ ~white $_1 \/ ~young $_3 \/ ~young skc28 \/ % 0.20/0.42 skc28 = $_3 \/ ssSkC0 % 0.20/0.42 |- ~barrel skc22 $_30 \/ ~car $_30 \/ ~chevy $_30 \/ ~city skc25 \/ % 0.20/0.42 ~dirty $_30 \/ ~down skc22 $_29 \/ ~event skc22 \/ ~fellow $_34 \/ % 0.20/0.42 ~fellow $_35 \/ ~front $_33 \/ ~furniture $_33 \/ ~hollywood skc25 \/ % 0.20/0.42 ~in $_34 $_33 \/ ~in $_35 $_33 \/ ~lonely $_29 \/ ~man $_34 \/ % 0.20/0.42 ~man $_35 \/ ~old $_30 \/ ~seat $_33 \/ ~street $_29 \/ ~way $_29 \/ % 0.20/0.42 ~white $_30 \/ ~young $_34 \/ ~young $_35 \/ $_35 = $_34 \/ ssSkC0 % 0.20/0.42 |- ~barrel skc23 $_30 \/ ~car $_30 \/ ~chevy $_30 \/ ~city skc24 \/ % 0.20/0.42 ~dirty $_30 \/ ~down skc23 $_29 \/ ~event skc23 \/ ~fellow $_34 \/ % 0.20/0.42 ~fellow $_35 \/ ~front $_33 \/ ~furniture $_33 \/ ~hollywood skc24 \/ % 0.20/0.42 ~in $_34 $_33 \/ ~in $_35 $_33 \/ ~lonely $_29 \/ ~man $_34 \/ % 0.20/0.42 ~man $_35 \/ ~old $_30 \/ ~seat $_33 \/ ~street $_29 \/ ~way $_29 \/ % 0.20/0.42 ~white $_30 \/ ~young $_34 \/ ~young $_35 \/ $_35 = $_34 \/ ssSkC0 % 0.20/0.42 |- ~barrel skc28 $_30 \/ ~car $_30 \/ ~chevy $_30 \/ ~dirty $_30 \/ % 0.20/0.42 ~down skc28 $_29 \/ ~fellow $_34 \/ ~fellow $_35 \/ ~front $_33 \/ % 0.20/0.42 ~furniture $_33 \/ ~hollywood skc29 \/ ~in $_34 $_33 \/ ~in $_35 $_33 \/ % 0.20/0.42 ~lonely $_29 \/ ~man $_34 \/ ~man $_35 \/ ~old $_30 \/ ~seat $_33 \/ % 0.20/0.42 ~street $_29 \/ ~way $_29 \/ ~white $_30 \/ ~young $_34 \/ % 0.20/0.42 ~young $_35 \/ $_35 = $_34 \/ ssSkC0 % 0.20/0.42 |- ~barrel $_31 $_30 \/ ~car $_30 \/ ~chevy $_30 \/ ~city $_32 \/ % 0.20/0.42 ~dirty $_30 \/ ~down $_31 $_29 \/ ~event $_31 \/ ~fellow $_35 \/ % 0.20/0.42 ~fellow skc22 \/ ~furniture skc25 \/ ~hollywood $_32 \/ ~in $_31 $_32 \/ % 0.20/0.42 ~in $_35 skc25 \/ ~lonely $_29 \/ ~man $_35 \/ ~man skc22 \/ % 0.20/0.42 ~old $_30 \/ ~seat skc25 \/ ~street $_29 \/ ~way $_29 \/ ~white $_30 \/ % 0.20/0.42 ~young $_35 \/ $_35 = skc22 \/ ssSkC0 % 0.20/0.42 |- ~barrel $_31 $_30 \/ ~car $_30 \/ ~chevy $_30 \/ ~city $_32 \/ % 0.20/0.42 ~dirty $_30 \/ ~down $_31 $_29 \/ ~event $_31 \/ ~fellow $_35 \/ % 0.20/0.42 ~front skc24 \/ ~furniture skc24 \/ ~hollywood $_32 \/ ~in $_31 $_32 \/ % 0.20/0.42 ~in $_35 skc24 \/ ~lonely $_29 \/ ~man $_35 \/ ~man skc23 \/ % 0.20/0.42 ~old $_30 \/ ~street $_29 \/ ~way $_29 \/ ~white $_30 \/ ~young $_35 \/ % 0.20/0.42 ~young skc23 \/ $_35 = skc23 \/ ssSkC0 % 0.20/0.42 |- ~barrel $_31 $_30 \/ ~car $_30 \/ ~chevy $_30 \/ ~city $_32 \/ % 0.20/0.42 ~dirty $_30 \/ ~down $_31 $_29 \/ ~event $_31 \/ ~fellow $_35 \/ % 0.20/0.42 ~fellow skc28 \/ ~front skc29 \/ ~furniture skc29 \/ ~hollywood $_32 \/ % 0.20/0.42 ~in $_31 $_32 \/ ~in $_35 skc29 \/ ~lonely $_29 \/ ~man $_35 \/ % 0.20/0.42 ~man skc28 \/ ~old $_30 \/ ~seat skc29 \/ ~street $_29 \/ ~way $_29 \/ % 0.20/0.42 ~white $_30 \/ ~young $_35 \/ ~young skc28 \/ $_35 = skc28 \/ ssSkC0 % 0.20/0.42 |- ~barrel skc22 $_37 \/ ~car $_37 \/ ~chevy $_37 \/ ~city skc25 \/ % 0.20/0.42 ~dirty $_37 \/ ~down skc22 $_36 \/ ~event skc22 \/ ~fellow $_40 \/ % 0.20/0.42 ~front skc24 \/ ~furniture skc24 \/ ~hollywood skc25 \/ % 0.20/0.42 ~in $_40 skc24 \/ ~lonely $_36 \/ ~man $_40 \/ ~man skc23 \/ % 0.20/0.42 ~old $_37 \/ ~street $_36 \/ ~way $_36 \/ ~white $_37 \/ ~young $_40 \/ % 0.20/0.42 ~young skc23 \/ $_40 = skc23 \/ ssSkC0 % 0.20/0.42 |- ~barrel skc28 $_37 \/ ~car $_37 \/ ~chevy $_37 \/ ~dirty $_37 \/ % 0.20/0.42 ~down skc28 $_36 \/ ~fellow $_40 \/ ~front skc24 \/ ~furniture skc24 \/ % 0.20/0.42 ~hollywood skc29 \/ ~in $_40 skc24 \/ ~lonely $_36 \/ ~man $_40 \/ % 0.20/0.42 ~man skc23 \/ ~old $_37 \/ ~street $_36 \/ ~way $_36 \/ ~white $_37 \/ % 0.20/0.42 ~young $_40 \/ ~young skc23 \/ $_40 = skc23 \/ ssSkC0 % 0.20/0.42 |- ~barrel skc23 $_48 \/ ~car $_48 \/ ~chevy $_48 \/ ~city skc24 \/ % 0.20/0.42 ~dirty $_48 \/ ~down skc23 $_47 \/ ~event skc23 \/ ~fellow $_51 \/ % 0.20/0.42 ~fellow skc22 \/ ~furniture skc25 \/ ~hollywood skc24 \/ % 0.20/0.42 ~in $_51 skc25 \/ ~lonely $_47 \/ ~man $_51 \/ ~man skc22 \/ % 0.20/0.42 ~old $_48 \/ ~seat skc25 \/ ~street $_47 \/ ~way $_47 \/ ~white $_48 \/ % 0.20/0.42 ~young $_51 \/ $_51 = skc22 \/ ssSkC0 % 0.20/0.42 |- ~barrel skc28 $_48 \/ ~car $_48 \/ ~chevy $_48 \/ ~dirty $_48 \/ % 0.20/0.42 ~down skc28 $_47 \/ ~fellow $_51 \/ ~fellow skc22 \/ ~furniture skc25 \/ % 0.20/0.42 ~hollywood skc29 \/ ~in $_51 skc25 \/ ~lonely $_47 \/ ~man $_51 \/ % 0.20/0.42 ~man skc22 \/ ~old $_48 \/ ~seat skc25 \/ ~street $_47 \/ ~way $_47 \/ % 0.20/0.42 ~white $_48 \/ ~young $_51 \/ $_51 = skc22 \/ ssSkC0 % 0.20/0.42 |- ~barrel skc23 $_64 \/ ~car $_64 \/ ~chevy $_64 \/ ~city skc24 \/ % 0.20/0.42 ~dirty $_64 \/ ~down skc23 $_63 \/ ~event skc23 \/ ~fellow $_67 \/ % 0.20/0.42 ~fellow skc28 \/ ~front skc29 \/ ~furniture skc29 \/ ~hollywood skc24 \/ % 0.20/0.42 ~in $_67 skc29 \/ ~lonely $_63 \/ ~man $_67 \/ ~man skc28 \/ % 0.20/0.42 ~old $_64 \/ ~seat skc29 \/ ~street $_63 \/ ~way $_63 \/ ~white $_64 \/ % 0.20/0.42 ~young $_67 \/ ~young skc28 \/ $_67 = skc28 \/ ssSkC0 % 0.20/0.42 |- ~barrel skc22 $_72 \/ ~car $_72 \/ ~chevy $_72 \/ ~city skc25 \/ % 0.20/0.42 ~dirty $_72 \/ ~down skc22 $_71 \/ ~event skc22 \/ ~fellow $_75 \/ % 0.20/0.42 ~fellow skc28 \/ ~front skc29 \/ ~furniture skc29 \/ ~hollywood skc25 \/ % 0.20/0.42 ~in $_75 skc29 \/ ~lonely $_71 \/ ~man $_75 \/ ~man skc28 \/ % 0.20/0.42 ~old $_72 \/ ~seat skc29 \/ ~street $_71 \/ ~way $_71 \/ ~white $_72 \/ % 0.20/0.42 ~young $_75 \/ ~young skc28 \/ $_75 = skc28 \/ ssSkC0 % 0.20/0.42 SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.20/0.42 %------------------------------------------------------------------------------