↑ Up

Metis---2.4.CSA-Sat.s

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

% Computer : n029.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:39 EDT 2022

% Result   : CounterSatisfiable 0.19s 0.45s
% Output   : Saturation 0.19s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12  % Problem  : NLP005+1 : TPTP v8.1.0. Released v2.4.0.
% 0.07/0.13  % Command  : metis --show proof --show saturation %s
% 0.13/0.34  % Computer : n029.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 : Thu Jun 30 19:47:08 EDT 2022
% 0.13/0.34  % CPUTime  : 
% 0.13/0.35  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.19/0.45  % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.45  
% 0.19/0.45  SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.45  |- ~(skolemFOFtoCNF_X22 = skolemFOFtoCNF_X23)
% 0.19/0.45  |- skolemFOFtoCNF_X22 = skolemFOFtoCNF_X25
% 0.19/0.45  |- skolemFOFtoCNF_X23 = skolemFOFtoCNF_X26
% 0.19/0.45  |- barrel skolemFOFtoCNF_X19 skolemFOFtoCNF_X21
% 0.19/0.45  |- car skolemFOFtoCNF_X21
% 0.19/0.45  |- chevy skolemFOFtoCNF_X21
% 0.19/0.45  |- city skolemFOFtoCNF_X18
% 0.19/0.45  |- dirty skolemFOFtoCNF_X21
% 0.19/0.45  |- down skolemFOFtoCNF_X19 skolemFOFtoCNF_X20
% 0.19/0.45  |- event skolemFOFtoCNF_X19
% 0.19/0.45  |- fellow skolemFOFtoCNF_X22
% 0.19/0.45  |- fellow skolemFOFtoCNF_X23
% 0.19/0.45  |- front skolemFOFtoCNF_X16
% 0.19/0.45  |- front skolemFOFtoCNF_X17
% 0.19/0.45  |- furniture skolemFOFtoCNF_X16
% 0.19/0.45  |- furniture skolemFOFtoCNF_X17
% 0.19/0.45  |- hollywood skolemFOFtoCNF_X18
% 0.19/0.45  |- in skolemFOFtoCNF_X19 skolemFOFtoCNF_X18
% 0.19/0.45  |- in skolemFOFtoCNF_X22 skolemFOFtoCNF_X16
% 0.19/0.45  |- in skolemFOFtoCNF_X23 skolemFOFtoCNF_X17
% 0.19/0.45  |- lonely skolemFOFtoCNF_X20
% 0.19/0.45  |- man skolemFOFtoCNF_X22
% 0.19/0.45  |- man skolemFOFtoCNF_X23
% 0.19/0.45  |- old skolemFOFtoCNF_X21
% 0.19/0.45  |- seat skolemFOFtoCNF_X16
% 0.19/0.45  |- seat skolemFOFtoCNF_X17
% 0.19/0.45  |- street skolemFOFtoCNF_X20
% 0.19/0.45  |- way skolemFOFtoCNF_X20
% 0.19/0.45  |- white skolemFOFtoCNF_X21
% 0.19/0.45  |- young skolemFOFtoCNF_X22
% 0.19/0.45  |- young skolemFOFtoCNF_X23
% 0.19/0.45  |- ~barrel $X29 $X30 \/ ~car $X30 \/ ~chevy $X30 \/ ~city $X28 \/
% 0.19/0.45     ~dirty $X30 \/ ~down $X29 $X31 \/ ~event $X29 \/ ~fellow $X35 \/
% 0.19/0.45     ~fellow $X36 \/ ~front $X27 \/ ~furniture $X27 \/ ~hollywood $X28 \/
% 0.19/0.45     ~in $X29 $X28 \/ ~in $X35 $X27 \/ ~in $X36 $X27 \/ ~lonely $X31 \/
% 0.19/0.45     ~man $X35 \/ ~man $X36 \/ ~old $X30 \/ ~seat $X27 \/ ~street $X31 \/
% 0.19/0.45     ~way $X31 \/ ~white $X30 \/ ~young $X35 \/ ~young $X36 \/ $X35 = $X36
% 0.19/0.45  |- ~barrel $X35 $X30 \/ ~car $X30 \/ ~chevy $X30 \/ ~city $X27 \/
% 0.19/0.45     ~dirty $X30 \/ ~down $X35 $X31 \/ ~event $X35 \/ ~fellow $X35 \/
% 0.19/0.45     ~fellow $X36 \/ ~front $X27 \/ ~furniture $X27 \/ ~hollywood $X27 \/
% 0.19/0.45     ~in $X35 $X27 \/ ~in $X36 $X27 \/ ~lonely $X31 \/ ~man $X35 \/
% 0.19/0.45     ~man $X36 \/ ~old $X30 \/ ~seat $X27 \/ ~street $X31 \/ ~way $X31 \/
% 0.19/0.45     ~white $X30 \/ ~young $X35 \/ ~young $X36 \/ $X35 = $X36
% 0.19/0.45  |- ~barrel skolemFOFtoCNF_X19 $_54 \/ ~car $_54 \/ ~chevy $_54 \/
% 0.19/0.45     ~dirty $_54 \/ ~down skolemFOFtoCNF_X19 $_55 \/ ~fellow $_57 \/
% 0.19/0.45     ~fellow skolemFOFtoCNF_X19 \/ ~front skolemFOFtoCNF_X18 \/
% 0.19/0.45     ~furniture skolemFOFtoCNF_X18 \/ ~in $_57 skolemFOFtoCNF_X18 \/
% 0.19/0.45     ~lonely $_55 \/ ~man $_57 \/ ~man skolemFOFtoCNF_X19 \/ ~old $_54 \/
% 0.19/0.45     ~seat skolemFOFtoCNF_X18 \/ ~street $_55 \/ ~way $_55 \/ ~white $_54 \/
% 0.19/0.45     ~young $_57 \/ ~young skolemFOFtoCNF_X19 \/ skolemFOFtoCNF_X19 = $_57
% 0.19/0.45  |- ~barrel skolemFOFtoCNF_X22 $_54 \/ ~car $_54 \/ ~chevy $_54 \/
% 0.19/0.45     ~city skolemFOFtoCNF_X16 \/ ~dirty $_54 \/
% 0.19/0.45     ~down skolemFOFtoCNF_X22 $_55 \/ ~event skolemFOFtoCNF_X22 \/
% 0.19/0.45     ~fellow $_57 \/ ~hollywood skolemFOFtoCNF_X16 \/
% 0.19/0.45     ~in $_57 skolemFOFtoCNF_X16 \/ ~lonely $_55 \/ ~man $_57 \/ ~old $_54 \/
% 0.19/0.45     ~street $_55 \/ ~way $_55 \/ ~white $_54 \/ ~young $_57 \/
% 0.19/0.45     skolemFOFtoCNF_X22 = $_57
% 0.19/0.45  |- ~barrel skolemFOFtoCNF_X23 $_54 \/ ~car $_54 \/ ~chevy $_54 \/
% 0.19/0.45     ~city skolemFOFtoCNF_X17 \/ ~dirty $_54 \/
% 0.19/0.45     ~down skolemFOFtoCNF_X23 $_55 \/ ~event skolemFOFtoCNF_X23 \/
% 0.19/0.45     ~fellow $_57 \/ ~hollywood skolemFOFtoCNF_X17 \/
% 0.19/0.45     ~in $_57 skolemFOFtoCNF_X17 \/ ~lonely $_55 \/ ~man $_57 \/ ~old $_54 \/
% 0.19/0.45     ~street $_55 \/ ~way $_55 \/ ~white $_54 \/ ~young $_57 \/
% 0.19/0.45     skolemFOFtoCNF_X23 = $_57
% 0.19/0.45  |- ~barrel $_56 $_54 \/ ~car $_54 \/ ~chevy $_54 \/ ~dirty $_54 \/
% 0.19/0.45     ~down $_56 $_55 \/ ~event $_56 \/ ~fellow $_56 \/
% 0.19/0.45     ~fellow skolemFOFtoCNF_X19 \/ ~front skolemFOFtoCNF_X18 \/
% 0.19/0.45     ~furniture skolemFOFtoCNF_X18 \/ ~in $_56 skolemFOFtoCNF_X18 \/
% 0.19/0.45     ~lonely $_55 \/ ~man $_56 \/ ~man skolemFOFtoCNF_X19 \/ ~old $_54 \/
% 0.19/0.45     ~seat skolemFOFtoCNF_X18 \/ ~street $_55 \/ ~way $_55 \/ ~white $_54 \/
% 0.19/0.45     ~young $_56 \/ ~young skolemFOFtoCNF_X19 \/ $_56 = skolemFOFtoCNF_X19
% 0.19/0.45  |- ~barrel $_56 $_54 \/ ~car $_54 \/ ~chevy $_54 \/
% 0.19/0.45     ~city skolemFOFtoCNF_X16 \/ ~dirty $_54 \/ ~down $_56 $_55 \/
% 0.19/0.45     ~event $_56 \/ ~fellow $_56 \/ ~hollywood skolemFOFtoCNF_X16 \/
% 0.19/0.45     ~in $_56 skolemFOFtoCNF_X16 \/ ~lonely $_55 \/ ~man $_56 \/ ~old $_54 \/
% 0.19/0.45     ~street $_55 \/ ~way $_55 \/ ~white $_54 \/ ~young $_56 \/
% 0.19/0.45     $_56 = skolemFOFtoCNF_X22
% 0.19/0.45  |- ~barrel $_56 $_54 \/ ~car $_54 \/ ~chevy $_54 \/
% 0.19/0.45     ~city skolemFOFtoCNF_X17 \/ ~dirty $_54 \/ ~down $_56 $_55 \/
% 0.19/0.45     ~event $_56 \/ ~fellow $_56 \/ ~hollywood skolemFOFtoCNF_X17 \/
% 0.19/0.45     ~in $_56 skolemFOFtoCNF_X17 \/ ~lonely $_55 \/ ~man $_56 \/ ~old $_54 \/
% 0.19/0.45     ~street $_55 \/ ~way $_55 \/ ~white $_54 \/ ~young $_56 \/
% 0.19/0.45     $_56 = skolemFOFtoCNF_X23
% 0.19/0.45  |- ~barrel skolemFOFtoCNF_X19 $_79 \/ ~car $_79 \/ ~chevy $_79 \/
% 0.19/0.45     ~dirty $_79 \/ ~down skolemFOFtoCNF_X19 $_80 \/ ~fellow $_81 \/
% 0.19/0.45     ~fellow $_82 \/ ~front $_76 \/ ~furniture $_76 \/ ~in $_81 $_76 \/
% 0.19/0.45     ~in $_82 $_76 \/ ~lonely $_80 \/ ~man $_81 \/ ~man $_82 \/ ~old $_79 \/
% 0.19/0.45     ~seat $_76 \/ ~street $_80 \/ ~way $_80 \/ ~white $_79 \/ ~young $_81 \/
% 0.19/0.45     ~young $_82 \/ $_81 = $_82
% 0.19/0.45  |- ~barrel skolemFOFtoCNF_X22 $_79 \/ ~car $_79 \/ ~chevy $_79 \/
% 0.19/0.45     ~city skolemFOFtoCNF_X16 \/ ~dirty $_79 \/
% 0.19/0.45     ~down skolemFOFtoCNF_X22 $_80 \/ ~event skolemFOFtoCNF_X22 \/
% 0.19/0.45     ~fellow $_81 \/ ~fellow $_82 \/ ~front $_76 \/ ~furniture $_76 \/
% 0.19/0.45     ~hollywood skolemFOFtoCNF_X16 \/ ~in $_81 $_76 \/ ~in $_82 $_76 \/
% 0.19/0.45     ~lonely $_80 \/ ~man $_81 \/ ~man $_82 \/ ~old $_79 \/ ~seat $_76 \/
% 0.19/0.45     ~street $_80 \/ ~way $_80 \/ ~white $_79 \/ ~young $_81 \/
% 0.19/0.45     ~young $_82 \/ $_81 = $_82
% 0.19/0.45  |- ~barrel skolemFOFtoCNF_X23 $_79 \/ ~car $_79 \/ ~chevy $_79 \/
% 0.19/0.45     ~city skolemFOFtoCNF_X17 \/ ~dirty $_79 \/
% 0.19/0.45     ~down skolemFOFtoCNF_X23 $_80 \/ ~event skolemFOFtoCNF_X23 \/
% 0.19/0.45     ~fellow $_81 \/ ~fellow $_82 \/ ~front $_76 \/ ~furniture $_76 \/
% 0.19/0.45     ~hollywood skolemFOFtoCNF_X17 \/ ~in $_81 $_76 \/ ~in $_82 $_76 \/
% 0.19/0.45     ~lonely $_80 \/ ~man $_81 \/ ~man $_82 \/ ~old $_79 \/ ~seat $_76 \/
% 0.19/0.45     ~street $_80 \/ ~way $_80 \/ ~white $_79 \/ ~young $_81 \/
% 0.19/0.45     ~young $_82 \/ $_81 = $_82
% 0.19/0.45  |- ~barrel $_78 $_79 \/ ~car $_79 \/ ~chevy $_79 \/ ~city $_77 \/
% 0.19/0.45     ~dirty $_79 \/ ~down $_78 $_80 \/ ~event $_78 \/ ~fellow $_82 \/
% 0.19/0.45     ~fellow skolemFOFtoCNF_X19 \/ ~front skolemFOFtoCNF_X18 \/
% 0.19/0.45     ~furniture skolemFOFtoCNF_X18 \/ ~hollywood $_77 \/ ~in $_78 $_77 \/
% 0.19/0.45     ~in $_82 skolemFOFtoCNF_X18 \/ ~lonely $_80 \/ ~man $_82 \/
% 0.19/0.45     ~man skolemFOFtoCNF_X19 \/ ~old $_79 \/ ~seat skolemFOFtoCNF_X18 \/
% 0.19/0.45     ~street $_80 \/ ~way $_80 \/ ~white $_79 \/ ~young $_82 \/
% 0.19/0.45     ~young skolemFOFtoCNF_X19 \/ skolemFOFtoCNF_X19 = $_82
% 0.19/0.46  |- ~barrel $_78 $_79 \/ ~car $_79 \/ ~chevy $_79 \/ ~city $_77 \/
% 0.19/0.46     ~dirty $_79 \/ ~down $_78 $_80 \/ ~event $_78 \/ ~fellow $_82 \/
% 0.19/0.46     ~hollywood $_77 \/ ~in $_78 $_77 \/ ~in $_82 skolemFOFtoCNF_X16 \/
% 0.19/0.46     ~lonely $_80 \/ ~man $_82 \/ ~old $_79 \/ ~street $_80 \/ ~way $_80 \/
% 0.19/0.46     ~white $_79 \/ ~young $_82 \/ skolemFOFtoCNF_X22 = $_82
% 0.19/0.46  |- ~barrel $_78 $_79 \/ ~car $_79 \/ ~chevy $_79 \/ ~city $_77 \/
% 0.19/0.46     ~dirty $_79 \/ ~down $_78 $_80 \/ ~event $_78 \/ ~fellow $_82 \/
% 0.19/0.46     ~hollywood $_77 \/ ~in $_78 $_77 \/ ~in $_82 skolemFOFtoCNF_X17 \/
% 0.19/0.46     ~lonely $_80 \/ ~man $_82 \/ ~old $_79 \/ ~street $_80 \/ ~way $_80 \/
% 0.19/0.46     ~white $_79 \/ ~young $_82 \/ skolemFOFtoCNF_X23 = $_82
% 0.19/0.46  |- ~barrel skolemFOFtoCNF_X19 $_85 \/ ~car $_85 \/ ~chevy $_85 \/
% 0.19/0.46     ~dirty $_85 \/ ~down skolemFOFtoCNF_X19 $_86 \/ ~fellow $_87 \/
% 0.19/0.46     ~in $_87 skolemFOFtoCNF_X16 \/ ~lonely $_86 \/ ~man $_87 \/ ~old $_85 \/
% 0.19/0.46     ~street $_86 \/ ~way $_86 \/ ~white $_85 \/ ~young $_87 \/
% 0.19/0.46     skolemFOFtoCNF_X22 = $_87
% 0.19/0.46  |- ~barrel skolemFOFtoCNF_X23 $_85 \/ ~car $_85 \/ ~chevy $_85 \/
% 0.19/0.46     ~city skolemFOFtoCNF_X17 \/ ~dirty $_85 \/
% 0.19/0.46     ~down skolemFOFtoCNF_X23 $_86 \/ ~event skolemFOFtoCNF_X23 \/
% 0.19/0.46     ~fellow $_87 \/ ~hollywood skolemFOFtoCNF_X17 \/
% 0.19/0.46     ~in $_87 skolemFOFtoCNF_X16 \/ ~lonely $_86 \/ ~man $_87 \/ ~old $_85 \/
% 0.19/0.46     ~street $_86 \/ ~way $_86 \/ ~white $_85 \/ ~young $_87 \/
% 0.19/0.46     skolemFOFtoCNF_X22 = $_87
% 0.19/0.46  |- ~barrel skolemFOFtoCNF_X19 $_96 \/ ~car $_96 \/ ~chevy $_96 \/
% 0.19/0.46     ~dirty $_96 \/ ~down skolemFOFtoCNF_X19 $_97 \/ ~fellow $_98 \/
% 0.19/0.46     ~in $_98 skolemFOFtoCNF_X17 \/ ~lonely $_97 \/ ~man $_98 \/ ~old $_96 \/
% 0.19/0.46     ~street $_97 \/ ~way $_97 \/ ~white $_96 \/ ~young $_98 \/
% 0.19/0.46     skolemFOFtoCNF_X23 = $_98
% 0.19/0.46  |- ~barrel skolemFOFtoCNF_X22 $_96 \/ ~car $_96 \/ ~chevy $_96 \/
% 0.19/0.46     ~city skolemFOFtoCNF_X16 \/ ~dirty $_96 \/
% 0.19/0.46     ~down skolemFOFtoCNF_X22 $_97 \/ ~event skolemFOFtoCNF_X22 \/
% 0.19/0.46     ~fellow $_98 \/ ~hollywood skolemFOFtoCNF_X16 \/
% 0.19/0.46     ~in $_98 skolemFOFtoCNF_X17 \/ ~lonely $_97 \/ ~man $_98 \/ ~old $_96 \/
% 0.19/0.46     ~street $_97 \/ ~way $_97 \/ ~white $_96 \/ ~young $_98 \/
% 0.19/0.46     skolemFOFtoCNF_X23 = $_98
% 0.19/0.46  |- ~barrel skolemFOFtoCNF_X22 $_111 \/ ~car $_111 \/ ~chevy $_111 \/
% 0.19/0.46     ~city skolemFOFtoCNF_X16 \/ ~dirty $_111 \/
% 0.19/0.46     ~down skolemFOFtoCNF_X22 $_112 \/ ~event skolemFOFtoCNF_X22 \/
% 0.19/0.46     ~fellow $_114 \/ ~fellow skolemFOFtoCNF_X19 \/
% 0.19/0.46     ~front skolemFOFtoCNF_X18 \/ ~furniture skolemFOFtoCNF_X18 \/
% 0.19/0.46     ~hollywood skolemFOFtoCNF_X16 \/ ~in $_114 skolemFOFtoCNF_X18 \/
% 0.19/0.46     ~lonely $_112 \/ ~man $_114 \/ ~man skolemFOFtoCNF_X19 \/ ~old $_111 \/
% 0.19/0.46     ~seat skolemFOFtoCNF_X18 \/ ~street $_112 \/ ~way $_112 \/
% 0.19/0.46     ~white $_111 \/ ~young $_114 \/ ~young skolemFOFtoCNF_X19 \/
% 0.19/0.46     skolemFOFtoCNF_X19 = $_114
% 0.19/0.46  |- ~barrel skolemFOFtoCNF_X23 $_120 \/ ~car $_120 \/ ~chevy $_120 \/
% 0.19/0.46     ~city skolemFOFtoCNF_X17 \/ ~dirty $_120 \/
% 0.19/0.46     ~down skolemFOFtoCNF_X23 $_121 \/ ~event skolemFOFtoCNF_X23 \/
% 0.19/0.46     ~fellow $_122 \/ ~fellow skolemFOFtoCNF_X19 \/
% 0.19/0.46     ~front skolemFOFtoCNF_X18 \/ ~furniture skolemFOFtoCNF_X18 \/
% 0.19/0.46     ~hollywood skolemFOFtoCNF_X17 \/ ~in $_122 skolemFOFtoCNF_X18 \/
% 0.19/0.46     ~lonely $_121 \/ ~man $_122 \/ ~man skolemFOFtoCNF_X19 \/ ~old $_120 \/
% 0.19/0.46     ~seat skolemFOFtoCNF_X18 \/ ~street $_121 \/ ~way $_121 \/
% 0.19/0.46     ~white $_120 \/ ~young $_122 \/ ~young skolemFOFtoCNF_X19 \/
% 0.19/0.46     skolemFOFtoCNF_X19 = $_122
% 0.19/0.46  SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.46  
%------------------------------------------------------------------------------