↑ Up

Metis---2.4.SAT-Sat.s

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

% Computer : n003.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:15 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.11  % Problem  : NLP132-1 : TPTP v8.1.0. Released v2.4.0.
% 0.10/0.12  % Command  : metis --show proof --show saturation %s
% 0.12/0.33  % Computer : n003.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 19:12:52 EDT 2022
% 0.12/0.33  % CPUTime  : 
% 0.12/0.33  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 skc42
% 0.12/0.38  |- actual_world skc12
% 0.12/0.38  |- city skc42 skc46 \/ ssSkC0
% 0.12/0.38  |- chevy skc42 skc46 \/ ssSkC0
% 0.12/0.38  |- ssSkC0 \/ white skc42 skc46
% 0.12/0.38  |- dirty skc42 skc46 \/ ssSkC0
% 0.12/0.38  |- old skc42 skc46 \/ ssSkC0
% 0.12/0.38  |- placename skc42 skc47 \/ ssSkC0
% 0.12/0.38  |- hollywood_placename skc42 skc47 \/ ssSkC0
% 0.12/0.38  |- event skc42 skc44 \/ ssSkC0
% 0.12/0.38  |- present skc42 skc44 \/ ssSkC0
% 0.12/0.38  |- barrel skc42 skc44 \/ ssSkC0
% 0.12/0.38  |- lonely skc42 skc45 \/ ssSkC0
% 0.12/0.38  |- ssSkC0 \/ street skc42 skc45
% 0.12/0.38  |- group skc42 skc43 \/ ssSkC0
% 0.12/0.38  |- ssSkC0 \/ two skc42 skc43
% 0.12/0.38  |- ssSkC0 \/ ssSkP0 skc43 skc42
% 0.12/0.38  |- ~ssSkC0 \/ event skc12 skc14
% 0.12/0.38  |- ~ssSkC0 \/ present skc12 skc14
% 0.12/0.38  |- ~ssSkC0 \/ barrel skc12 skc14
% 0.12/0.38  |- ~ssSkC0 \/ old skc12 skc17
% 0.12/0.38  |- ~ssSkC0 \/ dirty skc12 skc17
% 0.12/0.38  |- ~ssSkC0 \/ white skc12 skc17
% 0.12/0.38  |- ~ssSkC0 \/ chevy skc12 skc17
% 0.12/0.38  |- ~ssSkC0 \/ lonely skc12 skc15
% 0.12/0.38  |- ~ssSkC0 \/ street skc12 skc15
% 0.12/0.38  |- ~ssSkC0 \/ city skc12 skc15
% 0.12/0.38  |- ~ssSkC0 \/ hollywood_placename skc12 skc16
% 0.12/0.38  |- ~ssSkC0 \/ placename skc12 skc16
% 0.12/0.38  |- ~ssSkC0 \/ group skc12 skc13
% 0.12/0.38  |- ~ssSkC0 \/ two skc12 skc13
% 0.12/0.38  |- ~ssSkC0 \/ ssSkP1 skc13 skc12
% 0.12/0.38  |- agent skc42 skc44 skc46 \/ ssSkC0
% 0.12/0.38  |- in skc42 skc44 skc46 \/ ssSkC0
% 0.12/0.38  |- of skc42 skc47 skc46 \/ ssSkC0
% 0.12/0.38  |- down skc42 skc44 skc45 \/ ssSkC0
% 0.12/0.38  |- ~ssSkC0 \/ agent skc12 skc14 skc17
% 0.12/0.38  |- ~ssSkC0 \/ in skc12 skc14 skc15
% 0.12/0.38  |- ~ssSkC0 \/ down skc12 skc14 skc15
% 0.12/0.38  |- ~ssSkC0 \/ of skc12 skc16 skc15
% 0.12/0.38  |- frontseat $V (skf14 $V $W) \/ ssSkP0 $U $V
% 0.12/0.38  |- member $V (skf14 $V $U) $U \/ ssSkP0 $U $V
% 0.12/0.38  |- member $V (skf19 $V $U) $U \/ ssSkP1 $U $V
% 0.12/0.38  |- ~member skc42 $U skc43 \/ fellow skc42 $U \/ ssSkC0
% 0.12/0.38  |- ~member skc42 $U skc43 \/ ssSkC0 \/ young skc42 $U
% 0.12/0.38  |- ~member skc12 $U skc13 \/ ~ssSkC0 \/ fellow skc12 $U
% 0.12/0.38  |- ~member skc12 $U skc13 \/ ~ssSkC0 \/ young skc12 $U
% 0.12/0.38  |- ~member $U $V $W \/ ~ssSkP1 $W $U \/ state $U (skf16 $U $X)
% 0.12/0.38  |- ~member $U $V $W \/ ~ssSkP1 $W $U \/ frontseat $U (skf15 $U $X)
% 0.12/0.38  |- ~member $U $V $W \/ ~ssSkP1 $W $U \/ in $U (skf15 $U $X) (skf15 $U $X)
% 0.12/0.38  |- ~frontseat $U $V \/ ~member $U $V $W \/ ~ssSkP0 $W $U \/
% 0.12/0.38     state $U (skf11 $U $X)
% 0.12/0.38  |- ~member $U $V $W \/ ~ssSkP1 $W $U \/
% 0.12/0.38     be $U (skf16 $U $V) $V (skf15 $U $V)
% 0.12/0.38  |- ~frontseat $U $V \/ ~member $U $V $W \/ ~ssSkP0 $W $U \/
% 0.12/0.38     in $U (skf10 $V $U) $V
% 0.12/0.38  |- ~frontseat $U $V \/ ~member $U $V $W \/ ~ssSkP0 $W $U \/
% 0.12/0.38     be $U (skf11 $U $V) $V (skf10 $V $U)
% 0.12/0.39  |- ~be $U $X (skf14 $U $W) $V \/ ~in $U $V (skf14 $U $W) \/ ~state $U $X \/
% 0.12/0.39     ssSkP0 $Y $U
% 0.12/0.39  |- ~be $U $W (skf19 $U $X) $V \/ ~frontseat $U $V \/ ~in $U $V $V \/
% 0.12/0.39     ~state $U $W \/ ssSkP1 $Y $U
% 0.12/0.39  |- ~actual_world $U \/ ~agent $U $V $W \/ ~barrel $U $V \/ ~chevy $U $W \/
% 0.12/0.39     ~city $U $X \/ ~dirty $U $W \/ ~down $U $V $X \/ ~event $U $V \/
% 0.12/0.39     ~group $U $Z \/ ~hollywood_placename $U $Y \/ ~in $U $V $X \/
% 0.12/0.39     ~lonely $U $X \/ ~of $U $Y $X \/ ~old $U $W \/ ~placename $U $Y \/
% 0.12/0.39     ~present $U $V \/ ~ssSkP1 $Z $U \/ ~street $U $X \/ ~two $U $Z \/
% 0.12/0.39     ~white $U $W \/ member $U (skf21 $U $Z) $Z \/ ssSkC0
% 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 \/ ~ssSkC0 \/ ~ssSkP0 $Z $U \/ ~street $U $Y \/
% 0.12/0.39     ~two $U $Z \/ ~white $U $V \/ member $U (skf9 $U $Z) $Z
% 0.12/0.39  |- ~actual_world $U \/ ~agent $U $V $W \/ ~barrel $U $V \/ ~chevy $U $W \/
% 0.12/0.39     ~city $U $X \/ ~dirty $U $W \/ ~down $U $V $X \/ ~event $U $V \/
% 0.12/0.39     ~fellow $U (skf21 $U $Z) \/ ~group $U $X1 \/
% 0.12/0.39     ~hollywood_placename $U $Y \/ ~in $U $V $X \/ ~lonely $U $X \/
% 0.12/0.39     ~of $U $Y $X \/ ~old $U $W \/ ~placename $U $Y \/ ~present $U $V \/
% 0.12/0.39     ~ssSkP1 $X1 $U \/ ~street $U $X \/ ~two $U $X1 \/ ~white $U $W \/
% 0.12/0.39     ~young $U (skf21 $U $Z) \/ ssSkC0
% 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 (skf9 $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     ~ssSkC0 \/ ~ssSkP0 $X1 $U \/ ~street $U $Y \/ ~two $U $X1 \/
% 0.12/0.39     ~white $U $V \/ ~young $U (skf9 $U $Z)
% 0.12/0.39  |- ~ssSkC0 \/ fellow skc12 (skf14 skc12 skc13) \/ ssSkP0 skc13 skc12
% 0.12/0.39  |- ~ssSkC0 \/ ssSkP0 skc13 skc12 \/ young skc12 (skf14 skc12 skc13)
% 0.12/0.39  |- ssSkC0 \/ ssSkP1 skc43 skc42 \/ young skc42 (skf19 skc42 skc43)
% 0.12/0.39  |- fellow skc42 (skf19 skc42 skc43) \/ ssSkC0 \/ ssSkP1 skc43 skc42
% 0.12/0.39  |- ~ssSkP1 $_13 $_11 \/ ssSkP0 $_13 $_11 \/ state $_11 (skf16 $_11 $_14)
% 0.12/0.39  |- ~ssSkP1 $_20 $_18 \/ frontseat $_18 (skf15 $_18 $_21) \/
% 0.12/0.39     ssSkP0 $_20 $_18
% 0.12/0.39  |- ~ssSkP1 $_27 $_25 \/
% 0.12/0.39     be $_25 (skf16 $_25 (skf14 $_25 $_27)) (skf14 $_25 $_27)
% 0.12/0.39       (skf15 $_25 (skf14 $_25 $_27)) \/ ssSkP0 $_27 $_25
% 0.12/0.39  |- ~ssSkP1 $_32 $_30 \/ in $_30 (skf15 $_30 $_33) (skf15 $_30 $_33) \/
% 0.12/0.39     ssSkP0 $_32 $_30
% 0.12/0.39  |- ~frontseat $_37 (skf19 $_37 $_39) \/ ~ssSkP0 $_39 $_37 \/
% 0.12/0.39     in $_37 (skf10 (skf19 $_37 $_39) $_37) (skf19 $_37 $_39) \/
% 0.12/0.39     ssSkP1 $_39 $_37
% 0.12/0.39  |- ~frontseat $_42 (skf19 $_42 $_44) \/ ~ssSkP0 $_44 $_42 \/
% 0.12/0.39     ssSkP1 $_44 $_42 \/ state $_42 (skf11 $_42 $_45)
% 0.12/0.39  |- ~frontseat $_49 (skf19 $_49 $_51) \/ ~ssSkP0 $_51 $_49 \/
% 0.12/0.39     be $_49 (skf11 $_49 (skf19 $_49 $_51)) (skf19 $_49 $_51)
% 0.12/0.39       (skf10 (skf19 $_49 $_51) $_49) \/ ssSkP1 $_51 $_49
% 0.12/0.39  |- ~agent skc42 $_65 $_66 \/ ~barrel skc42 $_65 \/ ~chevy skc42 $_66 \/
% 0.12/0.39     ~city skc42 skc46 \/ ~dirty skc42 $_66 \/ ~down skc42 $_65 skc46 \/
% 0.12/0.39     ~event skc42 $_65 \/ ~group skc42 $_69 \/
% 0.12/0.39     ~hollywood_placename skc42 skc47 \/ ~in skc42 $_65 skc46 \/
% 0.12/0.39     ~lonely skc42 skc46 \/ ~old skc42 $_66 \/ ~placename skc42 skc47 \/
% 0.12/0.39     ~present skc42 $_65 \/ ~ssSkP1 $_69 skc42 \/ ~street skc42 skc46 \/
% 0.12/0.39     ~two skc42 $_69 \/ ~white skc42 $_66 \/
% 0.12/0.39     member skc42 (skf21 skc42 $_69) $_69 \/ ssSkC0
% 0.12/0.39  |- ~agent skc42 skc44 $_71 \/ ~barrel skc42 skc44 \/ ~chevy skc42 $_71 \/
% 0.12/0.39     ~city skc42 skc46 \/ ~dirty skc42 $_71 \/ ~down skc42 skc44 skc46 \/
% 0.12/0.39     ~event skc42 skc44 \/ ~group skc42 $_72 \/
% 0.12/0.39     ~hollywood_placename skc42 skc47 \/ ~lonely skc42 skc46 \/
% 0.12/0.39     ~old skc42 $_71 \/ ~placename skc42 skc47 \/ ~present skc42 skc44 \/
% 0.12/0.39     ~ssSkP1 $_72 skc42 \/ ~street skc42 skc46 \/ ~two skc42 $_72 \/
% 0.12/0.39     ~white skc42 $_71 \/ member skc42 (skf21 skc42 $_72) $_72 \/ ssSkC0
% 0.12/0.39  SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.39  
%------------------------------------------------------------------------------