↑ Up

Metis---2.4.SAT-Sat.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : Metis---2.4
% Problem  : NLP137-1 : TPTP v8.1.0. Released v2.4.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : metis --show proof --show saturation %s

% Computer : n017.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:18 EDT 2022

% Result   : Satisfiable 0.19s 0.38s
% Output   : Saturation 0.19s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12  % Problem  : NLP137-1 : TPTP v8.1.0. Released v2.4.0.
% 0.04/0.13  % Command  : metis --show proof --show saturation %s
% 0.12/0.33  % Computer : n017.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 01:17:39 EDT 2022
% 0.12/0.34  % CPUTime  : 
% 0.12/0.34  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.19/0.38  % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.38  
% 0.19/0.38  SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.38  |- actual_world skc43
% 0.19/0.38  |- actual_world skc13
% 0.19/0.38  |- old skc43 skc49 \/ ssSkC0
% 0.19/0.38  |- dirty skc43 skc49 \/ ssSkC0
% 0.19/0.38  |- ssSkC0 \/ white skc43 skc49
% 0.19/0.38  |- chevy skc43 skc49 \/ ssSkC0
% 0.19/0.38  |- barrel skc43 skc45 \/ ssSkC0
% 0.19/0.38  |- present skc43 skc45 \/ ssSkC0
% 0.19/0.38  |- event skc43 skc45 \/ ssSkC0
% 0.19/0.38  |- hollywood_placename skc43 skc47 \/ ssSkC0
% 0.19/0.38  |- placename skc43 skc47 \/ ssSkC0
% 0.19/0.39  |- city skc43 skc48 \/ ssSkC0
% 0.19/0.39  |- ssSkC0 \/ street skc43 skc46
% 0.19/0.39  |- lonely skc43 skc46 \/ ssSkC0
% 0.19/0.39  |- ssSkC0 \/ ssSkP0 skc44 skc43
% 0.19/0.39  |- ssSkC0 \/ two skc43 skc44
% 0.19/0.39  |- group skc43 skc44 \/ ssSkC0
% 0.19/0.39  |- ~ssSkC0 \/ event skc13 skc15
% 0.19/0.39  |- ~ssSkC0 \/ present skc13 skc15
% 0.19/0.39  |- ~ssSkC0 \/ barrel skc13 skc15
% 0.19/0.39  |- ~ssSkC0 \/ old skc13 skc18
% 0.19/0.39  |- ~ssSkC0 \/ dirty skc13 skc18
% 0.19/0.39  |- ~ssSkC0 \/ white skc13 skc18
% 0.19/0.39  |- ~ssSkC0 \/ chevy skc13 skc18
% 0.19/0.39  |- ~ssSkC0 \/ lonely skc13 skc16
% 0.19/0.39  |- ~ssSkC0 \/ street skc13 skc16
% 0.19/0.39  |- ~ssSkC0 \/ city skc13 skc16
% 0.19/0.39  |- ~ssSkC0 \/ hollywood_placename skc13 skc17
% 0.19/0.39  |- ~ssSkC0 \/ placename skc13 skc17
% 0.19/0.39  |- ~ssSkC0 \/ group skc13 skc14
% 0.19/0.39  |- ~ssSkC0 \/ two skc13 skc14
% 0.19/0.39  |- ~ssSkC0 \/ ssSkP1 skc14 skc13
% 0.19/0.39  |- agent skc43 skc45 skc49 \/ ssSkC0
% 0.19/0.39  |- in skc43 skc45 skc48 \/ ssSkC0
% 0.19/0.39  |- of skc43 skc47 skc48 \/ ssSkC0
% 0.19/0.39  |- down skc43 skc45 skc46 \/ ssSkC0
% 0.19/0.39  |- ~ssSkC0 \/ agent skc13 skc15 skc18
% 0.19/0.39  |- ~ssSkC0 \/ in skc13 skc15 skc16
% 0.19/0.39  |- ~ssSkC0 \/ down skc13 skc15 skc16
% 0.19/0.39  |- ~ssSkC0 \/ of skc13 skc17 skc16
% 0.19/0.39  |- frontseat $V (skf14 $V $W) \/ ssSkP0 $U $V
% 0.19/0.39  |- member $V (skf14 $V $U) $U \/ ssSkP0 $U $V
% 0.19/0.39  |- member $V (skf19 $V $U) $U \/ ssSkP1 $U $V
% 0.19/0.39  |- ~member skc43 $U skc44 \/ fellow skc43 $U \/ ssSkC0
% 0.19/0.39  |- ~member skc43 $U skc44 \/ ssSkC0 \/ young skc43 $U
% 0.19/0.39  |- ~member skc13 $U skc14 \/ ~ssSkC0 \/ fellow skc13 $U
% 0.19/0.39  |- ~member skc13 $U skc14 \/ ~ssSkC0 \/ young skc13 $U
% 0.19/0.39  |- ~member $U $V $W \/ ~ssSkP1 $W $U \/ state $U (skf16 $U $X)
% 0.19/0.39  |- ~member $U $V $W \/ ~ssSkP1 $W $U \/ frontseat $U (skf15 $U $X)
% 0.19/0.39  |- ~member $U $V $W \/ ~ssSkP1 $W $U \/ in $U (skf15 $U $X) (skf15 $U $X)
% 0.19/0.39  |- ~frontseat $U $V \/ ~member $U $V $W \/ ~ssSkP0 $W $U \/
% 0.19/0.39     state $U (skf11 $U $X)
% 0.19/0.39  |- ~member $U $V $W \/ ~ssSkP1 $W $U \/
% 0.19/0.39     be $U (skf16 $U $V) $V (skf15 $U $V)
% 0.19/0.39  |- ~frontseat $U $V \/ ~member $U $V $W \/ ~ssSkP0 $W $U \/
% 0.19/0.39     in $U (skf10 $V $U) $V
% 0.19/0.39  |- ~frontseat $U $V \/ ~member $U $V $W \/ ~ssSkP0 $W $U \/
% 0.19/0.39     be $U (skf11 $U $V) $V (skf10 $V $U)
% 0.19/0.39  |- ~be $U $X (skf14 $U $W) $V \/ ~in $U $V (skf14 $U $W) \/ ~state $U $X \/
% 0.19/0.39     ssSkP0 $Y $U
% 0.19/0.39  |- ~be $U $W (skf19 $U $X) $V \/ ~frontseat $U $V \/ ~in $U $V $V \/
% 0.19/0.39     ~state $U $W \/ ssSkP1 $Y $U
% 0.19/0.39  |- ~actual_world $U \/ ~agent $U $V $W \/ ~barrel $U $V \/ ~chevy $U $W \/
% 0.19/0.39     ~city $U $X \/ ~dirty $U $W \/ ~down $U $V $X \/ ~event $U $V \/
% 0.19/0.39     ~group $U $Z \/ ~hollywood_placename $U $Y \/ ~in $U $V $X \/
% 0.19/0.39     ~lonely $U $X \/ ~of $U $Y $X \/ ~old $U $W \/ ~placename $U $Y \/
% 0.19/0.39     ~present $U $V \/ ~ssSkP1 $Z $U \/ ~street $U $X \/ ~two $U $Z \/
% 0.19/0.39     ~white $U $W \/ member $U (skf21 $U $Z) $Z \/ ssSkC0
% 0.19/0.39  |- ~actual_world $U \/ ~agent $U $V $W \/ ~barrel $U $V \/ ~chevy $U $W \/
% 0.19/0.39     ~city $U $Y \/ ~dirty $U $W \/ ~down $U $V $Z \/ ~event $U $V \/
% 0.19/0.39     ~group $U $X1 \/ ~hollywood_placename $U $X \/ ~in $U $V $Y \/
% 0.19/0.39     ~lonely $U $Z \/ ~of $U $X $Y \/ ~old $U $W \/ ~placename $U $X \/
% 0.19/0.39     ~present $U $V \/ ~ssSkC0 \/ ~ssSkP0 $X1 $U \/ ~street $U $Z \/
% 0.19/0.39     ~two $U $X1 \/ ~white $U $W \/ member $U (skf9 $U $X1) $X1
% 0.19/0.39  |- ~actual_world $U \/ ~agent $U $V $W \/ ~barrel $U $V \/ ~chevy $U $W \/
% 0.19/0.39     ~city $U $X \/ ~dirty $U $W \/ ~down $U $V $X \/ ~event $U $V \/
% 0.19/0.39     ~fellow $U (skf21 $U $Z) \/ ~group $U $X1 \/
% 0.19/0.39     ~hollywood_placename $U $Y \/ ~in $U $V $X \/ ~lonely $U $X \/
% 0.19/0.39     ~of $U $Y $X \/ ~old $U $W \/ ~placename $U $Y \/ ~present $U $V \/
% 0.19/0.39     ~ssSkP1 $X1 $U \/ ~street $U $X \/ ~two $U $X1 \/ ~white $U $W \/
% 0.19/0.39     ~young $U (skf21 $U $Z) \/ ssSkC0
% 0.19/0.39  |- ~actual_world $U \/ ~agent $U $V $W \/ ~barrel $U $V \/ ~chevy $U $W \/
% 0.19/0.39     ~city $U $Y \/ ~dirty $U $W \/ ~down $U $V $Z \/ ~event $U $V \/
% 0.19/0.39     ~fellow $U (skf9 $U $X2) \/ ~group $U $X1 \/
% 0.19/0.39     ~hollywood_placename $U $X \/ ~in $U $V $Y \/ ~lonely $U $Z \/
% 0.19/0.39     ~of $U $X $Y \/ ~old $U $W \/ ~placename $U $X \/ ~present $U $V \/
% 0.19/0.39     ~ssSkC0 \/ ~ssSkP0 $X1 $U \/ ~street $U $Z \/ ~two $U $X1 \/
% 0.19/0.39     ~white $U $W \/ ~young $U (skf9 $U $X2)
% 0.19/0.39  |- ~ssSkC0 \/ ssSkP0 skc14 skc13 \/ young skc13 (skf14 skc13 skc14)
% 0.19/0.39  |- ~ssSkC0 \/ fellow skc13 (skf14 skc13 skc14) \/ ssSkP0 skc14 skc13
% 0.19/0.39  |- ssSkC0 \/ ssSkP1 skc44 skc43 \/ young skc43 (skf19 skc43 skc44)
% 0.19/0.39  |- fellow skc43 (skf19 skc43 skc44) \/ ssSkC0 \/ ssSkP1 skc44 skc43
% 0.19/0.39  |- ~ssSkP1 $_13 $_11 \/ ssSkP0 $_13 $_11 \/ state $_11 (skf16 $_11 $_14)
% 0.19/0.39  |- ~ssSkP1 $_20 $_18 \/ frontseat $_18 (skf15 $_18 $_21) \/
% 0.19/0.39     ssSkP0 $_20 $_18
% 0.19/0.39  |- ~ssSkP1 $_27 $_25 \/
% 0.19/0.39     be $_25 (skf16 $_25 (skf14 $_25 $_27)) (skf14 $_25 $_27)
% 0.19/0.39       (skf15 $_25 (skf14 $_25 $_27)) \/ ssSkP0 $_27 $_25
% 0.19/0.39  |- ~ssSkP1 $_32 $_30 \/ in $_30 (skf15 $_30 $_33) (skf15 $_30 $_33) \/
% 0.19/0.39     ssSkP0 $_32 $_30
% 0.19/0.39  |- ~frontseat $_37 (skf19 $_37 $_39) \/ ~ssSkP0 $_39 $_37 \/
% 0.19/0.39     in $_37 (skf10 (skf19 $_37 $_39) $_37) (skf19 $_37 $_39) \/
% 0.19/0.39     ssSkP1 $_39 $_37
% 0.19/0.39  |- ~frontseat $_42 (skf19 $_42 $_44) \/ ~ssSkP0 $_44 $_42 \/
% 0.19/0.39     ssSkP1 $_44 $_42 \/ state $_42 (skf11 $_42 $_45)
% 0.19/0.39  |- ~frontseat $_49 (skf19 $_49 $_51) \/ ~ssSkP0 $_51 $_49 \/
% 0.19/0.39     be $_49 (skf11 $_49 (skf19 $_49 $_51)) (skf19 $_49 $_51)
% 0.19/0.39       (skf10 (skf19 $_49 $_51) $_49) \/ ssSkP1 $_51 $_49
% 0.19/0.39  |- ~agent skc43 $_65 $_66 \/ ~barrel skc43 $_65 \/ ~chevy skc43 $_66 \/
% 0.19/0.39     ~city skc43 skc48 \/ ~dirty skc43 $_66 \/ ~down skc43 $_65 skc48 \/
% 0.19/0.39     ~event skc43 $_65 \/ ~group skc43 $_69 \/
% 0.19/0.39     ~hollywood_placename skc43 skc47 \/ ~in skc43 $_65 skc48 \/
% 0.19/0.39     ~lonely skc43 skc48 \/ ~old skc43 $_66 \/ ~placename skc43 skc47 \/
% 0.19/0.39     ~present skc43 $_65 \/ ~ssSkP1 $_69 skc43 \/ ~street skc43 skc48 \/
% 0.19/0.39     ~two skc43 $_69 \/ ~white skc43 $_66 \/
% 0.19/0.39     member skc43 (skf21 skc43 $_69) $_69 \/ ssSkC0
% 0.19/0.39  |- ~agent skc43 skc45 $_71 \/ ~barrel skc43 skc45 \/ ~chevy skc43 $_71 \/
% 0.19/0.39     ~city skc43 skc48 \/ ~dirty skc43 $_71 \/ ~down skc43 skc45 skc48 \/
% 0.19/0.39     ~event skc43 skc45 \/ ~group skc43 $_72 \/
% 0.19/0.39     ~hollywood_placename skc43 skc47 \/ ~lonely skc43 skc48 \/
% 0.19/0.39     ~old skc43 $_71 \/ ~placename skc43 skc47 \/ ~present skc43 skc45 \/
% 0.19/0.39     ~ssSkP1 $_72 skc43 \/ ~street skc43 skc48 \/ ~two skc43 $_72 \/
% 0.19/0.39     ~white skc43 $_71 \/ member skc43 (skf21 skc43 $_72) $_72 \/ ssSkC0
% 0.19/0.39  SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.39  
%------------------------------------------------------------------------------