↑ Up

Metis---2.4.CSA-Sat.s

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

% Computer : n014.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:42 EDT 2022

% Result   : CounterSatisfiable 0.18s 0.44s
% Output   : Saturation 0.18s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12  % Problem  : NLP008+1 : TPTP v8.1.0. Released v2.4.0.
% 0.06/0.12  % Command  : metis --show proof --show saturation %s
% 0.12/0.34  % Computer : n014.cluster.edu
% 0.12/0.34  % Model    : x86_64 x86_64
% 0.12/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34  % Memory   : 8042.1875MB
% 0.12/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34  % CPULimit : 300
% 0.12/0.34  % WCLimit  : 600
% 0.12/0.34  % DateTime : Thu Jun 30 22:14:26 EDT 2022
% 0.12/0.34  % CPUTime  : 
% 0.12/0.34  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.18/0.44  % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.44  
% 0.18/0.44  SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.44  |- ~(skolemFOFtoCNF_X20 = skolemFOFtoCNF_X21)
% 0.18/0.44  |- skolemFOFtoCNF_X20 = skolemFOFtoCNF_X23
% 0.18/0.44  |- skolemFOFtoCNF_X21 = skolemFOFtoCNF_X24
% 0.18/0.44  |- barrel skolemFOFtoCNF_X17 skolemFOFtoCNF_X18
% 0.18/0.44  |- car skolemFOFtoCNF_X18
% 0.18/0.44  |- chevy skolemFOFtoCNF_X18
% 0.18/0.44  |- city skolemFOFtoCNF_X16
% 0.18/0.44  |- dirty skolemFOFtoCNF_X18
% 0.18/0.44  |- down skolemFOFtoCNF_X17 skolemFOFtoCNF_X19
% 0.18/0.44  |- event skolemFOFtoCNF_X17
% 0.18/0.44  |- fellow skolemFOFtoCNF_X20
% 0.18/0.44  |- fellow skolemFOFtoCNF_X21
% 0.18/0.44  |- front skolemFOFtoCNF_X15
% 0.18/0.44  |- front skolemFOFtoCNF_X22
% 0.18/0.44  |- furniture skolemFOFtoCNF_X15
% 0.18/0.44  |- furniture skolemFOFtoCNF_X22
% 0.18/0.44  |- hollywood skolemFOFtoCNF_X16
% 0.18/0.44  |- in skolemFOFtoCNF_X17 skolemFOFtoCNF_X16
% 0.18/0.44  |- in skolemFOFtoCNF_X20 skolemFOFtoCNF_X22
% 0.18/0.44  |- in skolemFOFtoCNF_X21 skolemFOFtoCNF_X15
% 0.18/0.44  |- lonely skolemFOFtoCNF_X19
% 0.18/0.44  |- man skolemFOFtoCNF_X20
% 0.18/0.45  |- man skolemFOFtoCNF_X21
% 0.18/0.45  |- old skolemFOFtoCNF_X18
% 0.18/0.45  |- seat skolemFOFtoCNF_X15
% 0.18/0.45  |- seat skolemFOFtoCNF_X22
% 0.18/0.45  |- street skolemFOFtoCNF_X19
% 0.18/0.45  |- way skolemFOFtoCNF_X19
% 0.18/0.45  |- white skolemFOFtoCNF_X18
% 0.18/0.45  |- young skolemFOFtoCNF_X20
% 0.18/0.45  |- young skolemFOFtoCNF_X21
% 0.18/0.45  |- ~barrel $X27 $X29 \/ ~car $X29 \/ ~chevy $X29 \/ ~city $X26 \/
% 0.18/0.45     ~dirty $X29 \/ ~down $X27 $X28 \/ ~event $X27 \/ ~fellow $X33 \/
% 0.18/0.45     ~fellow $X34 \/ ~front $X25 \/ ~furniture $X25 \/ ~hollywood $X26 \/
% 0.18/0.45     ~in $X27 $X26 \/ ~in $X33 $X25 \/ ~in $X34 $X25 \/ ~lonely $X28 \/
% 0.18/0.45     ~man $X33 \/ ~man $X34 \/ ~old $X29 \/ ~seat $X25 \/ ~street $X28 \/
% 0.18/0.45     ~way $X28 \/ ~white $X29 \/ ~young $X33 \/ ~young $X34 \/ $X33 = $X34
% 0.18/0.45  |- ~barrel $X33 $X29 \/ ~car $X29 \/ ~chevy $X29 \/ ~city $X25 \/
% 0.18/0.45     ~dirty $X29 \/ ~down $X33 $X28 \/ ~event $X33 \/ ~fellow $X33 \/
% 0.18/0.45     ~fellow $X34 \/ ~front $X25 \/ ~furniture $X25 \/ ~hollywood $X25 \/
% 0.18/0.45     ~in $X33 $X25 \/ ~in $X34 $X25 \/ ~lonely $X28 \/ ~man $X33 \/
% 0.18/0.45     ~man $X34 \/ ~old $X29 \/ ~seat $X25 \/ ~street $X28 \/ ~way $X28 \/
% 0.18/0.45     ~white $X29 \/ ~young $X33 \/ ~young $X34 \/ $X33 = $X34
% 0.18/0.45  |- ~barrel skolemFOFtoCNF_X17 $_55 \/ ~car $_55 \/ ~chevy $_55 \/
% 0.18/0.45     ~dirty $_55 \/ ~down skolemFOFtoCNF_X17 $_54 \/ ~fellow $_57 \/
% 0.18/0.45     ~fellow skolemFOFtoCNF_X17 \/ ~front skolemFOFtoCNF_X16 \/
% 0.18/0.45     ~furniture skolemFOFtoCNF_X16 \/ ~in $_57 skolemFOFtoCNF_X16 \/
% 0.18/0.45     ~lonely $_54 \/ ~man $_57 \/ ~man skolemFOFtoCNF_X17 \/ ~old $_55 \/
% 0.18/0.45     ~seat skolemFOFtoCNF_X16 \/ ~street $_54 \/ ~way $_54 \/ ~white $_55 \/
% 0.18/0.45     ~young $_57 \/ ~young skolemFOFtoCNF_X17 \/ skolemFOFtoCNF_X17 = $_57
% 0.18/0.45  |- ~barrel skolemFOFtoCNF_X20 $_55 \/ ~car $_55 \/ ~chevy $_55 \/
% 0.18/0.45     ~city skolemFOFtoCNF_X22 \/ ~dirty $_55 \/
% 0.18/0.45     ~down skolemFOFtoCNF_X20 $_54 \/ ~event skolemFOFtoCNF_X20 \/
% 0.18/0.45     ~fellow $_57 \/ ~hollywood skolemFOFtoCNF_X22 \/
% 0.18/0.45     ~in $_57 skolemFOFtoCNF_X22 \/ ~lonely $_54 \/ ~man $_57 \/ ~old $_55 \/
% 0.18/0.45     ~street $_54 \/ ~way $_54 \/ ~white $_55 \/ ~young $_57 \/
% 0.18/0.45     skolemFOFtoCNF_X20 = $_57
% 0.18/0.45  |- ~barrel skolemFOFtoCNF_X21 $_55 \/ ~car $_55 \/ ~chevy $_55 \/
% 0.18/0.45     ~city skolemFOFtoCNF_X15 \/ ~dirty $_55 \/
% 0.18/0.45     ~down skolemFOFtoCNF_X21 $_54 \/ ~event skolemFOFtoCNF_X21 \/
% 0.18/0.45     ~fellow $_57 \/ ~hollywood skolemFOFtoCNF_X15 \/
% 0.18/0.45     ~in $_57 skolemFOFtoCNF_X15 \/ ~lonely $_54 \/ ~man $_57 \/ ~old $_55 \/
% 0.18/0.45     ~street $_54 \/ ~way $_54 \/ ~white $_55 \/ ~young $_57 \/
% 0.18/0.45     skolemFOFtoCNF_X21 = $_57
% 0.18/0.45  |- ~barrel $_56 $_55 \/ ~car $_55 \/ ~chevy $_55 \/ ~dirty $_55 \/
% 0.18/0.45     ~down $_56 $_54 \/ ~event $_56 \/ ~fellow $_56 \/
% 0.18/0.45     ~fellow skolemFOFtoCNF_X17 \/ ~front skolemFOFtoCNF_X16 \/
% 0.18/0.45     ~furniture skolemFOFtoCNF_X16 \/ ~in $_56 skolemFOFtoCNF_X16 \/
% 0.18/0.45     ~lonely $_54 \/ ~man $_56 \/ ~man skolemFOFtoCNF_X17 \/ ~old $_55 \/
% 0.18/0.45     ~seat skolemFOFtoCNF_X16 \/ ~street $_54 \/ ~way $_54 \/ ~white $_55 \/
% 0.18/0.45     ~young $_56 \/ ~young skolemFOFtoCNF_X17 \/ $_56 = skolemFOFtoCNF_X17
% 0.18/0.45  |- ~barrel $_56 $_55 \/ ~car $_55 \/ ~chevy $_55 \/
% 0.18/0.45     ~city skolemFOFtoCNF_X22 \/ ~dirty $_55 \/ ~down $_56 $_54 \/
% 0.18/0.45     ~event $_56 \/ ~fellow $_56 \/ ~hollywood skolemFOFtoCNF_X22 \/
% 0.18/0.45     ~in $_56 skolemFOFtoCNF_X22 \/ ~lonely $_54 \/ ~man $_56 \/ ~old $_55 \/
% 0.18/0.45     ~street $_54 \/ ~way $_54 \/ ~white $_55 \/ ~young $_56 \/
% 0.18/0.45     $_56 = skolemFOFtoCNF_X20
% 0.18/0.45  |- ~barrel $_56 $_55 \/ ~car $_55 \/ ~chevy $_55 \/
% 0.18/0.45     ~city skolemFOFtoCNF_X15 \/ ~dirty $_55 \/ ~down $_56 $_54 \/
% 0.18/0.45     ~event $_56 \/ ~fellow $_56 \/ ~hollywood skolemFOFtoCNF_X15 \/
% 0.18/0.45     ~in $_56 skolemFOFtoCNF_X15 \/ ~lonely $_54 \/ ~man $_56 \/ ~old $_55 \/
% 0.18/0.45     ~street $_54 \/ ~way $_54 \/ ~white $_55 \/ ~young $_56 \/
% 0.18/0.45     $_56 = skolemFOFtoCNF_X21
% 0.18/0.45  |- ~barrel skolemFOFtoCNF_X17 $_80 \/ ~car $_80 \/ ~chevy $_80 \/
% 0.18/0.45     ~dirty $_80 \/ ~down skolemFOFtoCNF_X17 $_79 \/ ~fellow $_81 \/
% 0.18/0.45     ~fellow $_82 \/ ~front $_76 \/ ~furniture $_76 \/ ~in $_81 $_76 \/
% 0.18/0.45     ~in $_82 $_76 \/ ~lonely $_79 \/ ~man $_81 \/ ~man $_82 \/ ~old $_80 \/
% 0.18/0.45     ~seat $_76 \/ ~street $_79 \/ ~way $_79 \/ ~white $_80 \/ ~young $_81 \/
% 0.18/0.45     ~young $_82 \/ $_81 = $_82
% 0.18/0.45  |- ~barrel skolemFOFtoCNF_X20 $_80 \/ ~car $_80 \/ ~chevy $_80 \/
% 0.18/0.45     ~city skolemFOFtoCNF_X22 \/ ~dirty $_80 \/
% 0.18/0.45     ~down skolemFOFtoCNF_X20 $_79 \/ ~event skolemFOFtoCNF_X20 \/
% 0.18/0.45     ~fellow $_81 \/ ~fellow $_82 \/ ~front $_76 \/ ~furniture $_76 \/
% 0.18/0.45     ~hollywood skolemFOFtoCNF_X22 \/ ~in $_81 $_76 \/ ~in $_82 $_76 \/
% 0.18/0.45     ~lonely $_79 \/ ~man $_81 \/ ~man $_82 \/ ~old $_80 \/ ~seat $_76 \/
% 0.18/0.45     ~street $_79 \/ ~way $_79 \/ ~white $_80 \/ ~young $_81 \/
% 0.18/0.45     ~young $_82 \/ $_81 = $_82
% 0.18/0.45  |- ~barrel skolemFOFtoCNF_X21 $_80 \/ ~car $_80 \/ ~chevy $_80 \/
% 0.18/0.45     ~city skolemFOFtoCNF_X15 \/ ~dirty $_80 \/
% 0.18/0.45     ~down skolemFOFtoCNF_X21 $_79 \/ ~event skolemFOFtoCNF_X21 \/
% 0.18/0.45     ~fellow $_81 \/ ~fellow $_82 \/ ~front $_76 \/ ~furniture $_76 \/
% 0.18/0.45     ~hollywood skolemFOFtoCNF_X15 \/ ~in $_81 $_76 \/ ~in $_82 $_76 \/
% 0.18/0.45     ~lonely $_79 \/ ~man $_81 \/ ~man $_82 \/ ~old $_80 \/ ~seat $_76 \/
% 0.18/0.45     ~street $_79 \/ ~way $_79 \/ ~white $_80 \/ ~young $_81 \/
% 0.18/0.45     ~young $_82 \/ $_81 = $_82
% 0.18/0.45  |- ~barrel $_78 $_80 \/ ~car $_80 \/ ~chevy $_80 \/ ~city $_77 \/
% 0.18/0.45     ~dirty $_80 \/ ~down $_78 $_79 \/ ~event $_78 \/ ~fellow $_82 \/
% 0.18/0.45     ~fellow skolemFOFtoCNF_X17 \/ ~front skolemFOFtoCNF_X16 \/
% 0.18/0.45     ~furniture skolemFOFtoCNF_X16 \/ ~hollywood $_77 \/ ~in $_78 $_77 \/
% 0.18/0.45     ~in $_82 skolemFOFtoCNF_X16 \/ ~lonely $_79 \/ ~man $_82 \/
% 0.18/0.45     ~man skolemFOFtoCNF_X17 \/ ~old $_80 \/ ~seat skolemFOFtoCNF_X16 \/
% 0.18/0.45     ~street $_79 \/ ~way $_79 \/ ~white $_80 \/ ~young $_82 \/
% 0.18/0.45     ~young skolemFOFtoCNF_X17 \/ skolemFOFtoCNF_X17 = $_82
% 0.18/0.45  |- ~barrel $_78 $_80 \/ ~car $_80 \/ ~chevy $_80 \/ ~city $_77 \/
% 0.18/0.45     ~dirty $_80 \/ ~down $_78 $_79 \/ ~event $_78 \/ ~fellow $_82 \/
% 0.18/0.45     ~hollywood $_77 \/ ~in $_78 $_77 \/ ~in $_82 skolemFOFtoCNF_X22 \/
% 0.18/0.45     ~lonely $_79 \/ ~man $_82 \/ ~old $_80 \/ ~street $_79 \/ ~way $_79 \/
% 0.18/0.45     ~white $_80 \/ ~young $_82 \/ skolemFOFtoCNF_X20 = $_82
% 0.18/0.45  |- ~barrel $_78 $_80 \/ ~car $_80 \/ ~chevy $_80 \/ ~city $_77 \/
% 0.18/0.45     ~dirty $_80 \/ ~down $_78 $_79 \/ ~event $_78 \/ ~fellow $_82 \/
% 0.18/0.45     ~hollywood $_77 \/ ~in $_78 $_77 \/ ~in $_82 skolemFOFtoCNF_X15 \/
% 0.18/0.45     ~lonely $_79 \/ ~man $_82 \/ ~old $_80 \/ ~street $_79 \/ ~way $_79 \/
% 0.18/0.45     ~white $_80 \/ ~young $_82 \/ skolemFOFtoCNF_X21 = $_82
% 0.18/0.45  |- ~barrel skolemFOFtoCNF_X17 $_86 \/ ~car $_86 \/ ~chevy $_86 \/
% 0.18/0.45     ~dirty $_86 \/ ~down skolemFOFtoCNF_X17 $_85 \/ ~fellow $_87 \/
% 0.18/0.45     ~in $_87 skolemFOFtoCNF_X22 \/ ~lonely $_85 \/ ~man $_87 \/ ~old $_86 \/
% 0.18/0.45     ~street $_85 \/ ~way $_85 \/ ~white $_86 \/ ~young $_87 \/
% 0.18/0.45     skolemFOFtoCNF_X20 = $_87
% 0.18/0.45  |- ~barrel skolemFOFtoCNF_X21 $_86 \/ ~car $_86 \/ ~chevy $_86 \/
% 0.18/0.45     ~city skolemFOFtoCNF_X15 \/ ~dirty $_86 \/
% 0.18/0.45     ~down skolemFOFtoCNF_X21 $_85 \/ ~event skolemFOFtoCNF_X21 \/
% 0.18/0.45     ~fellow $_87 \/ ~hollywood skolemFOFtoCNF_X15 \/
% 0.18/0.45     ~in $_87 skolemFOFtoCNF_X22 \/ ~lonely $_85 \/ ~man $_87 \/ ~old $_86 \/
% 0.18/0.45     ~street $_85 \/ ~way $_85 \/ ~white $_86 \/ ~young $_87 \/
% 0.18/0.45     skolemFOFtoCNF_X20 = $_87
% 0.18/0.45  |- ~barrel skolemFOFtoCNF_X17 $_97 \/ ~car $_97 \/ ~chevy $_97 \/
% 0.18/0.45     ~dirty $_97 \/ ~down skolemFOFtoCNF_X17 $_96 \/ ~fellow $_98 \/
% 0.18/0.45     ~in $_98 skolemFOFtoCNF_X15 \/ ~lonely $_96 \/ ~man $_98 \/ ~old $_97 \/
% 0.18/0.45     ~street $_96 \/ ~way $_96 \/ ~white $_97 \/ ~young $_98 \/
% 0.18/0.45     skolemFOFtoCNF_X21 = $_98
% 0.18/0.45  |- ~barrel skolemFOFtoCNF_X20 $_97 \/ ~car $_97 \/ ~chevy $_97 \/
% 0.18/0.45     ~city skolemFOFtoCNF_X22 \/ ~dirty $_97 \/
% 0.18/0.45     ~down skolemFOFtoCNF_X20 $_96 \/ ~event skolemFOFtoCNF_X20 \/
% 0.18/0.45     ~fellow $_98 \/ ~hollywood skolemFOFtoCNF_X22 \/
% 0.18/0.45     ~in $_98 skolemFOFtoCNF_X15 \/ ~lonely $_96 \/ ~man $_98 \/ ~old $_97 \/
% 0.18/0.45     ~street $_96 \/ ~way $_96 \/ ~white $_97 \/ ~young $_98 \/
% 0.18/0.45     skolemFOFtoCNF_X21 = $_98
% 0.18/0.45  |- ~barrel skolemFOFtoCNF_X20 $_112 \/ ~car $_112 \/ ~chevy $_112 \/
% 0.18/0.45     ~city skolemFOFtoCNF_X22 \/ ~dirty $_112 \/
% 0.18/0.45     ~down skolemFOFtoCNF_X20 $_111 \/ ~event skolemFOFtoCNF_X20 \/
% 0.18/0.45     ~fellow $_114 \/ ~fellow skolemFOFtoCNF_X17 \/
% 0.18/0.45     ~front skolemFOFtoCNF_X16 \/ ~furniture skolemFOFtoCNF_X16 \/
% 0.18/0.45     ~hollywood skolemFOFtoCNF_X22 \/ ~in $_114 skolemFOFtoCNF_X16 \/
% 0.18/0.45     ~lonely $_111 \/ ~man $_114 \/ ~man skolemFOFtoCNF_X17 \/ ~old $_112 \/
% 0.18/0.45     ~seat skolemFOFtoCNF_X16 \/ ~street $_111 \/ ~way $_111 \/
% 0.18/0.45     ~white $_112 \/ ~young $_114 \/ ~young skolemFOFtoCNF_X17 \/
% 0.18/0.45     skolemFOFtoCNF_X17 = $_114
% 0.18/0.45  |- ~barrel skolemFOFtoCNF_X21 $_121 \/ ~car $_121 \/ ~chevy $_121 \/
% 0.18/0.45     ~city skolemFOFtoCNF_X15 \/ ~dirty $_121 \/
% 0.18/0.45     ~down skolemFOFtoCNF_X21 $_120 \/ ~event skolemFOFtoCNF_X21 \/
% 0.18/0.45     ~fellow $_122 \/ ~fellow skolemFOFtoCNF_X17 \/
% 0.18/0.45     ~front skolemFOFtoCNF_X16 \/ ~furniture skolemFOFtoCNF_X16 \/
% 0.18/0.45     ~hollywood skolemFOFtoCNF_X15 \/ ~in $_122 skolemFOFtoCNF_X16 \/
% 0.18/0.45     ~lonely $_120 \/ ~man $_122 \/ ~man skolemFOFtoCNF_X17 \/ ~old $_121 \/
% 0.18/0.45     ~seat skolemFOFtoCNF_X16 \/ ~street $_120 \/ ~way $_120 \/
% 0.18/0.45     ~white $_121 \/ ~young $_122 \/ ~young skolemFOFtoCNF_X17 \/
% 0.18/0.45     skolemFOFtoCNF_X17 = $_122
% 0.18/0.45  SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.45  
%------------------------------------------------------------------------------