↑ Up

Metis---2.4.CSA-Sat.s

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

% Computer : n007.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:54 EDT 2022

% Result   : CounterSatisfiable 0.47s 0.68s
% Output   : Saturation 0.52s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11  % Problem  : NLP192+1 : TPTP v8.1.0. Released v2.4.0.
% 0.06/0.12  % Command  : metis --show proof --show saturation %s
% 0.12/0.33  % Computer : n007.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 07:40:39 EDT 2022
% 0.12/0.33  % CPUTime  : 
% 0.12/0.34  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.47/0.68  % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.47/0.68  
% 0.47/0.68  SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.47/0.68  |- actual_world skolemFOFtoCNF_U
% 0.47/0.68  |- agent skolemFOFtoCNF_U skolemFOFtoCNF_X2 skolemFOFtoCNF_Y
% 0.47/0.68  |- barrel skolemFOFtoCNF_U skolemFOFtoCNF_X2
% 0.47/0.68  |- be skolemFOFtoCNF_U skolemFOFtoCNF_X5 skolemFOFtoCNF_V skolemFOFtoCNF_X6
% 0.47/0.68  |- behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 skolemFOFtoCNF_Y
% 0.47/0.68  |- chevy skolemFOFtoCNF_U skolemFOFtoCNF_Y
% 0.47/0.68  |- city skolemFOFtoCNF_U skolemFOFtoCNF_X1
% 0.47/0.68  |- dirty skolemFOFtoCNF_U skolemFOFtoCNF_Y
% 0.47/0.68  |- down skolemFOFtoCNF_U skolemFOFtoCNF_X2 skolemFOFtoCNF_X1
% 0.47/0.68  |- event skolemFOFtoCNF_U skolemFOFtoCNF_X2
% 0.47/0.68  |- forename skolemFOFtoCNF_U skolemFOFtoCNF_W
% 0.47/0.68  |- frontseat skolemFOFtoCNF_U skolemFOFtoCNF_X
% 0.47/0.68  |- group skolemFOFtoCNF_U skolemFOFtoCNF_X3
% 0.47/0.68  |- group skolemFOFtoCNF_U skolemFOFtoCNF_X4
% 0.47/0.68  |- hollywood_placename skolemFOFtoCNF_U skolemFOFtoCNF_Z
% 0.47/0.68  |- in skolemFOFtoCNF_U skolemFOFtoCNF_X2 skolemFOFtoCNF_X1
% 0.47/0.68  |- jules_forename skolemFOFtoCNF_U skolemFOFtoCNF_W
% 0.47/0.68  |- lonely skolemFOFtoCNF_U skolemFOFtoCNF_X1
% 0.47/0.68  |- man skolemFOFtoCNF_U skolemFOFtoCNF_V
% 0.47/0.68  |- of skolemFOFtoCNF_U skolemFOFtoCNF_W skolemFOFtoCNF_V
% 0.47/0.68  |- of skolemFOFtoCNF_U skolemFOFtoCNF_Z skolemFOFtoCNF_X1
% 0.47/0.68  |- old skolemFOFtoCNF_U skolemFOFtoCNF_Y
% 0.47/0.68  |- placename skolemFOFtoCNF_U skolemFOFtoCNF_Z
% 0.47/0.68  |- present skolemFOFtoCNF_U skolemFOFtoCNF_X2
% 0.47/0.68  |- state skolemFOFtoCNF_U skolemFOFtoCNF_X5
% 0.47/0.68  |- street skolemFOFtoCNF_U skolemFOFtoCNF_X1
% 0.47/0.68  |- two skolemFOFtoCNF_U skolemFOFtoCNF_X3
% 0.47/0.68  |- wheel skolemFOFtoCNF_U skolemFOFtoCNF_Y
% 0.47/0.68  |- white skolemFOFtoCNF_U skolemFOFtoCNF_Y
% 0.47/0.68  |- ~member skolemFOFtoCNF_U $X10 skolemFOFtoCNF_X3 \/
% 0.47/0.68     fellow skolemFOFtoCNF_U $X10
% 0.47/0.68  |- ~member skolemFOFtoCNF_U $X10 skolemFOFtoCNF_X3 \/
% 0.47/0.68     young skolemFOFtoCNF_U $X10
% 0.47/0.68  |- ~member skolemFOFtoCNF_U $X11 skolemFOFtoCNF_X4 \/
% 0.47/0.68     ~member skolemFOFtoCNF_U $X12 skolemFOFtoCNF_X3 \/
% 0.47/0.68     agent skolemFOFtoCNF_U (skolemFOFtoCNF_X13 $X11 $X12) $X12
% 0.47/0.68  |- ~member skolemFOFtoCNF_U $X11 skolemFOFtoCNF_X4 \/
% 0.47/0.68     ~member skolemFOFtoCNF_U $X12 skolemFOFtoCNF_X3 \/
% 0.47/0.68     event skolemFOFtoCNF_U (skolemFOFtoCNF_X13 $X11 $X12)
% 0.47/0.68  |- ~member skolemFOFtoCNF_U $X11 skolemFOFtoCNF_X4 \/
% 0.47/0.68     ~member skolemFOFtoCNF_U $X12 skolemFOFtoCNF_X3 \/
% 0.47/0.68     nonreflexive skolemFOFtoCNF_U (skolemFOFtoCNF_X13 $X11 $X12)
% 0.47/0.68  |- ~member skolemFOFtoCNF_U $X11 skolemFOFtoCNF_X4 \/
% 0.47/0.68     ~member skolemFOFtoCNF_U $X12 skolemFOFtoCNF_X3 \/
% 0.47/0.68     patient skolemFOFtoCNF_U (skolemFOFtoCNF_X13 $X11 $X12) $X11
% 0.47/0.68  |- ~member skolemFOFtoCNF_U $X11 skolemFOFtoCNF_X4 \/
% 0.47/0.68     ~member skolemFOFtoCNF_U $X12 skolemFOFtoCNF_X3 \/
% 0.47/0.68     present skolemFOFtoCNF_U (skolemFOFtoCNF_X13 $X11 $X12)
% 0.47/0.68  |- ~member skolemFOFtoCNF_U $X11 skolemFOFtoCNF_X4 \/
% 0.47/0.68     ~member skolemFOFtoCNF_U $X12 skolemFOFtoCNF_X3 \/
% 0.47/0.68     wear skolemFOFtoCNF_U (skolemFOFtoCNF_X13 $X11 $X12)
% 0.47/0.68  |- ~member skolemFOFtoCNF_U $X14 skolemFOFtoCNF_X4 \/
% 0.47/0.68     black skolemFOFtoCNF_U $X14
% 0.47/0.68  |- ~member skolemFOFtoCNF_U $X14 skolemFOFtoCNF_X4 \/
% 0.47/0.68     cheap skolemFOFtoCNF_U $X14
% 0.47/0.68  |- ~member skolemFOFtoCNF_U $X14 skolemFOFtoCNF_X4 \/
% 0.47/0.68     coat skolemFOFtoCNF_U $X14
% 0.47/0.68  |- ~member skolemFOFtoCNF_U $X7 skolemFOFtoCNF_X3 \/
% 0.47/0.68     be skolemFOFtoCNF_U (skolemFOFtoCNF_X8 $X7) $X7 (skolemFOFtoCNF_X9 $X7)
% 0.47/0.68  |- ~member skolemFOFtoCNF_U $X7 skolemFOFtoCNF_X3 \/
% 0.47/0.68     in skolemFOFtoCNF_U (skolemFOFtoCNF_X9 $X7) skolemFOFtoCNF_X
% 0.47/0.68  |- ~member skolemFOFtoCNF_U $X7 skolemFOFtoCNF_X3 \/
% 0.47/0.68     state skolemFOFtoCNF_U (skolemFOFtoCNF_X8 $X7)
% 0.47/0.68  |- ~definitionFOFtoCNF_0 $X15 $X23 $X30 \/ member $X15 $X30 $X23
% 0.47/0.68  |- ~definitionFOFtoCNF_0 $X15 $X23 $X30 \/ ~fellow $X15 $X30 \/
% 0.47/0.68     ~young $X15 $X30
% 0.47/0.68  |- ~member $X15 $X30 $X23 \/ definitionFOFtoCNF_0 $X15 $X23 $X30 \/
% 0.47/0.68     fellow $X15 $X30
% 0.47/0.68  |- ~member $X15 $X30 $X23 \/ definitionFOFtoCNF_0 $X15 $X23 $X30 \/
% 0.47/0.68     young $X15 $X30
% 0.47/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.47/0.68     ~be $X15 $X25 $X16 $X26 \/ ~behind $X15 $X26 $X21 \/ ~chevy $X15 $X19 \/
% 0.47/0.68     ~city $X15 $X21 \/ ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/
% 0.47/0.68     ~event $X15 $X22 \/ ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/
% 0.47/0.68     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.47/0.68     ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/
% 0.47/0.68     ~jules_forename $X15 $X17 \/ ~lonely $X15 $X21 \/ ~man $X15 $X16 \/
% 0.47/0.68     ~of $X15 $X17 $X16 \/ ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/
% 0.47/0.68     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~state $X15 $X25 \/
% 0.47/0.68     ~street $X15 $X21 \/ ~two $X15 $X23 \/ ~wheel $X15 $X21 \/
% 0.47/0.68     ~white $X15 $X19 \/
% 0.47/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.47/0.68     member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23 \/
% 0.47/0.68     member $X15 (skolemFOFtoCNF_X31 $X15 $X23 $X24) $X24 \/
% 0.47/0.68     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.47/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.47/0.68     ~be $X15 $X25 $X16 $X26 \/ ~behind $X15 $X26 $X21 \/ ~chevy $X15 $X19 \/
% 0.47/0.68     ~city $X15 $X21 \/ ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/
% 0.47/0.68     ~event $X15 $X22 \/ ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/
% 0.47/0.68     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.47/0.68     ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/
% 0.47/0.68     ~jules_forename $X15 $X17 \/ ~lonely $X15 $X21 \/ ~man $X15 $X16 \/
% 0.47/0.68     ~of $X15 $X17 $X16 \/ ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/
% 0.47/0.68     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~state $X15 $X25 \/
% 0.47/0.68     ~street $X15 $X21 \/ ~two $X15 $X23 \/ ~wheel $X15 $X21 \/
% 0.47/0.68     ~white $X15 $X19 \/
% 0.47/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.47/0.68     member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23 \/
% 0.47/0.68     member $X15 (skolemFOFtoCNF_X32 $X15 $X23 $X24) $X23 \/
% 0.47/0.68     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.47/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.47/0.68     ~be $X15 $X25 $X16 $X26 \/
% 0.47/0.68     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.47/0.68     ~behind $X15 $X26 $X21 \/ ~chevy $X15 $X19 \/ ~city $X15 $X21 \/
% 0.47/0.68     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.47/0.68     ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/
% 0.47/0.68     ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/
% 0.47/0.68     ~in $X15 $X22 $X21 \/ ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X17 \/
% 0.47/0.68     ~lonely $X15 $X21 \/ ~man $X15 $X16 \/ ~of $X15 $X17 $X16 \/
% 0.47/0.68     ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ ~placename $X15 $X20 \/
% 0.47/0.68     ~present $X15 $X22 \/ ~state $X15 $X25 \/ ~state $X15 $X28 \/
% 0.47/0.68     ~street $X15 $X21 \/ ~two $X15 $X23 \/ ~wheel $X15 $X21 \/
% 0.47/0.68     ~white $X15 $X19 \/
% 0.47/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.47/0.68     member $X15 (skolemFOFtoCNF_X31 $X15 $X23 $X24) $X24 \/
% 0.47/0.68     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.47/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.47/0.68     ~be $X15 $X25 $X16 $X26 \/
% 0.47/0.68     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.47/0.68     ~behind $X15 $X26 $X21 \/ ~chevy $X15 $X19 \/ ~city $X15 $X21 \/
% 0.47/0.68     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.47/0.68     ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/
% 0.47/0.68     ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/
% 0.47/0.68     ~in $X15 $X22 $X21 \/ ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X17 \/
% 0.47/0.68     ~lonely $X15 $X21 \/ ~man $X15 $X16 \/ ~of $X15 $X17 $X16 \/
% 0.47/0.68     ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ ~placename $X15 $X20 \/
% 0.47/0.68     ~present $X15 $X22 \/ ~state $X15 $X25 \/ ~state $X15 $X28 \/
% 0.47/0.68     ~street $X15 $X21 \/ ~two $X15 $X23 \/ ~wheel $X15 $X21 \/
% 0.47/0.68     ~white $X15 $X19 \/
% 0.47/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.47/0.68     member $X15 (skolemFOFtoCNF_X32 $X15 $X23 $X24) $X23 \/
% 0.47/0.68     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.52/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.52/0.68     ~be $X15 $X25 $X16 $X26 \/ ~behind $X15 $X26 $X21 \/
% 0.52/0.68     ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.52/0.68     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.52/0.68     ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.52/0.68     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.52/0.68     ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/
% 0.52/0.68     ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/
% 0.52/0.68     ~in $X15 $X22 $X21 \/ ~jules_forename $X15 $X17 \/ ~lonely $X15 $X21 \/
% 0.52/0.68     ~man $X15 $X16 \/ ~of $X15 $X17 $X16 \/ ~of $X15 $X20 $X21 \/
% 0.52/0.68     ~old $X15 $X19 \/ ~placename $X15 $X20 \/ ~present $X15 $X22 \/
% 0.52/0.68     ~state $X15 $X25 \/ ~street $X15 $X21 \/ ~two $X15 $X23 \/
% 0.52/0.68     ~wheel $X15 $X21 \/ ~white $X15 $X19 \/
% 0.52/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.52/0.68     member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23 \/
% 0.52/0.68     member $X15 (skolemFOFtoCNF_X31 $X15 $X23 $X24) $X24
% 0.52/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.52/0.68     ~be $X15 $X25 $X16 $X26 \/ ~behind $X15 $X26 $X21 \/
% 0.52/0.68     ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.52/0.68     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.52/0.68     ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.52/0.68     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.52/0.68     ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/
% 0.52/0.68     ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/
% 0.52/0.68     ~in $X15 $X22 $X21 \/ ~jules_forename $X15 $X17 \/ ~lonely $X15 $X21 \/
% 0.52/0.68     ~man $X15 $X16 \/ ~of $X15 $X17 $X16 \/ ~of $X15 $X20 $X21 \/
% 0.52/0.68     ~old $X15 $X19 \/ ~placename $X15 $X20 \/ ~present $X15 $X22 \/
% 0.52/0.68     ~state $X15 $X25 \/ ~street $X15 $X21 \/ ~two $X15 $X23 \/
% 0.52/0.68     ~wheel $X15 $X21 \/ ~white $X15 $X19 \/
% 0.52/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.52/0.68     member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23 \/
% 0.52/0.68     member $X15 (skolemFOFtoCNF_X32 $X15 $X23 $X24) $X23
% 0.52/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.52/0.68     ~be $X15 $X25 $X16 $X26 \/
% 0.52/0.68     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.52/0.68     ~behind $X15 $X26 $X21 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.52/0.68     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.52/0.68     ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.52/0.68     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.52/0.68     ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/
% 0.52/0.68     ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/
% 0.52/0.68     ~in $X15 $X22 $X21 \/ ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X17 \/
% 0.52/0.68     ~lonely $X15 $X21 \/ ~man $X15 $X16 \/ ~of $X15 $X17 $X16 \/
% 0.52/0.68     ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ ~placename $X15 $X20 \/
% 0.52/0.68     ~present $X15 $X22 \/ ~state $X15 $X25 \/ ~state $X15 $X28 \/
% 0.52/0.68     ~street $X15 $X21 \/ ~two $X15 $X23 \/ ~wheel $X15 $X21 \/
% 0.52/0.68     ~white $X15 $X19 \/
% 0.52/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.52/0.68     member $X15 (skolemFOFtoCNF_X31 $X15 $X23 $X24) $X24
% 0.52/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.52/0.68     ~be $X15 $X25 $X16 $X26 \/
% 0.52/0.68     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.52/0.68     ~behind $X15 $X26 $X21 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.52/0.68     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.52/0.68     ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.52/0.68     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.52/0.68     ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/
% 0.52/0.68     ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/
% 0.52/0.68     ~in $X15 $X22 $X21 \/ ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X17 \/
% 0.52/0.68     ~lonely $X15 $X21 \/ ~man $X15 $X16 \/ ~of $X15 $X17 $X16 \/
% 0.52/0.68     ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ ~placename $X15 $X20 \/
% 0.52/0.68     ~present $X15 $X22 \/ ~state $X15 $X25 \/ ~state $X15 $X28 \/
% 0.52/0.68     ~street $X15 $X21 \/ ~two $X15 $X23 \/ ~wheel $X15 $X21 \/
% 0.52/0.68     ~white $X15 $X19 \/
% 0.52/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.52/0.68     member $X15 (skolemFOFtoCNF_X32 $X15 $X23 $X24) $X23
% 0.52/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/
% 0.52/0.68     ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/
% 0.52/0.68     ~barrel $X15 $X22 \/ ~be $X15 $X25 $X16 $X26 \/
% 0.52/0.68     ~behind $X15 $X26 $X21 \/ ~chevy $X15 $X19 \/ ~city $X15 $X21 \/
% 0.52/0.68     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.52/0.68     ~event $X15 $X33 \/ ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/
% 0.52/0.68     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.52/0.68     ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/
% 0.52/0.68     ~jules_forename $X15 $X17 \/ ~lonely $X15 $X21 \/ ~man $X15 $X16 \/
% 0.52/0.68     ~nonreflexive $X15 $X33 \/ ~of $X15 $X17 $X16 \/ ~of $X15 $X20 $X21 \/
% 0.52/0.68     ~old $X15 $X19 \/
% 0.52/0.68     ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/
% 0.52/0.68     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/
% 0.52/0.68     ~state $X15 $X25 \/ ~street $X15 $X21 \/ ~two $X15 $X23 \/
% 0.52/0.68     ~wear $X15 $X33 \/ ~wheel $X15 $X21 \/ ~white $X15 $X19 \/
% 0.52/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.52/0.68     member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23 \/
% 0.52/0.68     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.52/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/
% 0.52/0.68     ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/
% 0.52/0.68     ~barrel $X15 $X22 \/ ~be $X15 $X25 $X16 $X26 \/
% 0.52/0.68     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.52/0.68     ~behind $X15 $X26 $X21 \/ ~chevy $X15 $X19 \/ ~city $X15 $X21 \/
% 0.52/0.68     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.52/0.68     ~event $X15 $X33 \/ ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/
% 0.52/0.68     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.52/0.68     ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/
% 0.52/0.68     ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X17 \/ ~lonely $X15 $X21 \/
% 0.52/0.68     ~man $X15 $X16 \/ ~nonreflexive $X15 $X33 \/ ~of $X15 $X17 $X16 \/
% 0.52/0.68     ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/
% 0.52/0.68     ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/
% 0.52/0.68     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/
% 0.52/0.68     ~state $X15 $X25 \/ ~state $X15 $X28 \/ ~street $X15 $X21 \/
% 0.52/0.68     ~two $X15 $X23 \/ ~wear $X15 $X33 \/ ~wheel $X15 $X21 \/
% 0.52/0.68     ~white $X15 $X19 \/
% 0.52/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.52/0.68     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.52/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/
% 0.52/0.68     ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/
% 0.52/0.68     ~barrel $X15 $X22 \/ ~be $X15 $X25 $X16 $X26 \/
% 0.52/0.68     ~behind $X15 $X26 $X21 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.52/0.68     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.52/0.68     ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.52/0.68     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.52/0.68     ~event $X15 $X33 \/ ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/
% 0.52/0.68     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.52/0.68     ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/
% 0.52/0.68     ~jules_forename $X15 $X17 \/ ~lonely $X15 $X21 \/ ~man $X15 $X16 \/
% 0.52/0.68     ~nonreflexive $X15 $X33 \/ ~of $X15 $X17 $X16 \/ ~of $X15 $X20 $X21 \/
% 0.52/0.68     ~old $X15 $X19 \/
% 0.52/0.68     ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/
% 0.52/0.68     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/
% 0.52/0.68     ~state $X15 $X25 \/ ~street $X15 $X21 \/ ~two $X15 $X23 \/
% 0.52/0.68     ~wear $X15 $X33 \/ ~wheel $X15 $X21 \/ ~white $X15 $X19 \/
% 0.52/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.52/0.68     member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23
% 0.52/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/
% 0.52/0.68     ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/
% 0.52/0.68     ~barrel $X15 $X22 \/ ~be $X15 $X25 $X16 $X26 \/
% 0.52/0.68     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.52/0.68     ~behind $X15 $X26 $X21 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.52/0.68     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.52/0.68     ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.52/0.68     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.52/0.68     ~event $X15 $X33 \/ ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/
% 0.52/0.68     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.52/0.68     ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/
% 0.52/0.68     ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X17 \/ ~lonely $X15 $X21 \/
% 0.52/0.68     ~man $X15 $X16 \/ ~nonreflexive $X15 $X33 \/ ~of $X15 $X17 $X16 \/
% 0.52/0.68     ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/
% 0.52/0.68     ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/
% 0.52/0.68     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/
% 0.52/0.68     ~state $X15 $X25 \/ ~state $X15 $X28 \/ ~street $X15 $X21 \/
% 0.52/0.68     ~two $X15 $X23 \/ ~wear $X15 $X33 \/ ~wheel $X15 $X21 \/
% 0.52/0.68     ~white $X15 $X19 \/
% 0.52/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23)
% 0.52/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.52/0.68     ~be $X15 $X25 $X21 $X26 \/ ~behind $X15 $X26 $X21 \/ ~chevy $X15 $X19 \/
% 0.52/0.68     ~city $X15 $X21 \/ ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/
% 0.52/0.68     ~event $X15 $X22 \/ ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/
% 0.52/0.68     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.52/0.68     ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/
% 0.52/0.68     ~jules_forename $X15 $X20 \/ ~lonely $X15 $X21 \/ ~man $X15 $X21 \/
% 0.52/0.68     ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ ~placename $X15 $X20 \/
% 0.52/0.68     ~present $X15 $X22 \/ ~state $X15 $X25 \/ ~street $X15 $X21 \/
% 0.52/0.68     ~two $X15 $X23 \/ ~wheel $X15 $X21 \/ ~white $X15 $X19 \/
% 0.52/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.52/0.68     member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23 \/
% 0.52/0.68     member $X15 (skolemFOFtoCNF_X31 $X15 $X23 $X24) $X24 \/
% 0.52/0.68     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.52/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.52/0.68     ~be $X15 $X25 $X21 $X26 \/ ~behind $X15 $X26 $X21 \/ ~chevy $X15 $X19 \/
% 0.52/0.68     ~city $X15 $X21 \/ ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/
% 0.52/0.68     ~event $X15 $X22 \/ ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/
% 0.52/0.68     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.52/0.68     ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/
% 0.52/0.68     ~jules_forename $X15 $X20 \/ ~lonely $X15 $X21 \/ ~man $X15 $X21 \/
% 0.52/0.68     ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ ~placename $X15 $X20 \/
% 0.52/0.68     ~present $X15 $X22 \/ ~state $X15 $X25 \/ ~street $X15 $X21 \/
% 0.52/0.68     ~two $X15 $X23 \/ ~wheel $X15 $X21 \/ ~white $X15 $X19 \/
% 0.52/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.52/0.68     member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23 \/
% 0.52/0.68     member $X15 (skolemFOFtoCNF_X32 $X15 $X23 $X24) $X23 \/
% 0.52/0.68     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.52/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.52/0.68     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.52/0.68     ~behind $X15 $X29 $X21 \/ ~chevy $X15 $X19 \/ ~city $X15 $X21 \/
% 0.52/0.68     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.52/0.68     ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/
% 0.52/0.68     ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/
% 0.52/0.68     ~in $X15 $X22 $X21 \/ ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X17 \/
% 0.52/0.68     ~lonely $X15 $X21 \/ ~man $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.68     ~of $X15 $X17 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.68     ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ ~placename $X15 $X20 \/
% 0.52/0.68     ~present $X15 $X22 \/ ~state $X15 $X28 \/ ~street $X15 $X21 \/
% 0.52/0.68     ~two $X15 $X23 \/ ~wheel $X15 $X21 \/ ~white $X15 $X19 \/
% 0.52/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.52/0.68     member $X15 (skolemFOFtoCNF_X31 $X15 $X23 $X24) $X24 \/
% 0.52/0.68     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.52/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.52/0.68     ~be $X15 $X25 $X21 $X26 \/
% 0.52/0.68     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.52/0.68     ~behind $X15 $X26 $X21 \/ ~chevy $X15 $X19 \/ ~city $X15 $X21 \/
% 0.52/0.68     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.52/0.68     ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/
% 0.52/0.68     ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/
% 0.52/0.68     ~in $X15 $X22 $X21 \/ ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X20 \/
% 0.52/0.68     ~lonely $X15 $X21 \/ ~man $X15 $X21 \/ ~of $X15 $X20 $X21 \/
% 0.52/0.68     ~old $X15 $X19 \/ ~placename $X15 $X20 \/ ~present $X15 $X22 \/
% 0.52/0.68     ~state $X15 $X25 \/ ~state $X15 $X28 \/ ~street $X15 $X21 \/
% 0.52/0.68     ~two $X15 $X23 \/ ~wheel $X15 $X21 \/ ~white $X15 $X19 \/
% 0.52/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.52/0.68     member $X15 (skolemFOFtoCNF_X31 $X15 $X23 $X24) $X24 \/
% 0.52/0.68     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.52/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.52/0.68     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.52/0.68     ~behind $X15 $X29 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.68     ~chevy $X15 $X19 \/ ~city $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.68     ~dirty $X15 $X19 \/
% 0.52/0.68     ~down $X15 $X22 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.68     ~event $X15 $X22 \/ ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/
% 0.52/0.68     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.52/0.68     ~hollywood_placename $X15 $X20 \/
% 0.52/0.68     ~in $X15 $X22 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.68     ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X20 \/
% 0.52/0.68     ~lonely $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.68     ~man $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.68     ~of $X15 $X20 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~old $X15 $X19 \/
% 0.52/0.68     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~state $X15 $X28 \/
% 0.52/0.68     ~street $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~two $X15 $X23 \/
% 0.52/0.68     ~wheel $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~white $X15 $X19 \/
% 0.52/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.52/0.68     member $X15 (skolemFOFtoCNF_X31 $X15 $X23 $X24) $X24 \/
% 0.52/0.68     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.52/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.52/0.68     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.52/0.68     ~behind $X15 $X29 $X21 \/ ~chevy $X15 $X19 \/ ~city $X15 $X21 \/
% 0.52/0.68     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.52/0.68     ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/
% 0.52/0.68     ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/
% 0.52/0.68     ~in $X15 $X22 $X21 \/ ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X17 \/
% 0.52/0.68     ~lonely $X15 $X21 \/ ~man $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.68     ~of $X15 $X17 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.68     ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ ~placename $X15 $X20 \/
% 0.52/0.68     ~present $X15 $X22 \/ ~state $X15 $X28 \/ ~street $X15 $X21 \/
% 0.52/0.68     ~two $X15 $X23 \/ ~wheel $X15 $X21 \/ ~white $X15 $X19 \/
% 0.52/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.52/0.68     member $X15 (skolemFOFtoCNF_X32 $X15 $X23 $X24) $X23 \/
% 0.52/0.68     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.52/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.52/0.69     ~be $X15 $X25 $X21 $X26 \/
% 0.52/0.69     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.52/0.69     ~behind $X15 $X26 $X21 \/ ~chevy $X15 $X19 \/ ~city $X15 $X21 \/
% 0.52/0.69     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.52/0.69     ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/
% 0.52/0.69     ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/
% 0.52/0.69     ~in $X15 $X22 $X21 \/ ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X20 \/
% 0.52/0.69     ~lonely $X15 $X21 \/ ~man $X15 $X21 \/ ~of $X15 $X20 $X21 \/
% 0.52/0.69     ~old $X15 $X19 \/ ~placename $X15 $X20 \/ ~present $X15 $X22 \/
% 0.52/0.69     ~state $X15 $X25 \/ ~state $X15 $X28 \/ ~street $X15 $X21 \/
% 0.52/0.69     ~two $X15 $X23 \/ ~wheel $X15 $X21 \/ ~white $X15 $X19 \/
% 0.52/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.52/0.69     member $X15 (skolemFOFtoCNF_X32 $X15 $X23 $X24) $X23 \/
% 0.52/0.69     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.52/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.52/0.69     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.52/0.69     ~behind $X15 $X29 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~chevy $X15 $X19 \/ ~city $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~dirty $X15 $X19 \/
% 0.52/0.69     ~down $X15 $X22 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~event $X15 $X22 \/ ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/
% 0.52/0.69     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.52/0.69     ~hollywood_placename $X15 $X20 \/
% 0.52/0.69     ~in $X15 $X22 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X20 \/
% 0.52/0.69     ~lonely $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~man $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~of $X15 $X20 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~old $X15 $X19 \/
% 0.52/0.69     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~state $X15 $X28 \/
% 0.52/0.69     ~street $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~two $X15 $X23 \/
% 0.52/0.69     ~wheel $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~white $X15 $X19 \/
% 0.52/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.52/0.69     member $X15 (skolemFOFtoCNF_X32 $X15 $X23 $X24) $X23 \/
% 0.52/0.69     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.52/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.52/0.69     ~be $X15 $X25 $X21 $X26 \/ ~behind $X15 $X26 $X21 \/
% 0.52/0.69     ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.52/0.69     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.52/0.69     ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.52/0.69     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.52/0.69     ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/
% 0.52/0.69     ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/
% 0.52/0.69     ~in $X15 $X22 $X21 \/ ~jules_forename $X15 $X20 \/ ~lonely $X15 $X21 \/
% 0.52/0.69     ~man $X15 $X21 \/ ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/
% 0.52/0.69     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~state $X15 $X25 \/
% 0.52/0.69     ~street $X15 $X21 \/ ~two $X15 $X23 \/ ~wheel $X15 $X21 \/
% 0.52/0.69     ~white $X15 $X19 \/
% 0.52/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.52/0.69     member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23 \/
% 0.52/0.69     member $X15 (skolemFOFtoCNF_X31 $X15 $X23 $X24) $X24
% 0.52/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.52/0.69     ~be $X15 $X25 $X21 $X26 \/ ~behind $X15 $X26 $X21 \/
% 0.52/0.69     ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.52/0.69     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.52/0.69     ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.52/0.69     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.52/0.69     ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/
% 0.52/0.69     ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/
% 0.52/0.69     ~in $X15 $X22 $X21 \/ ~jules_forename $X15 $X20 \/ ~lonely $X15 $X21 \/
% 0.52/0.69     ~man $X15 $X21 \/ ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/
% 0.52/0.69     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~state $X15 $X25 \/
% 0.52/0.69     ~street $X15 $X21 \/ ~two $X15 $X23 \/ ~wheel $X15 $X21 \/
% 0.52/0.69     ~white $X15 $X19 \/
% 0.52/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.52/0.69     member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23 \/
% 0.52/0.69     member $X15 (skolemFOFtoCNF_X32 $X15 $X23 $X24) $X23
% 0.52/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.52/0.69     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.52/0.69     ~behind $X15 $X29 $X21 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.52/0.69     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.52/0.69     ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.52/0.69     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.52/0.69     ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/
% 0.52/0.69     ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/
% 0.52/0.69     ~in $X15 $X22 $X21 \/ ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X17 \/
% 0.52/0.69     ~lonely $X15 $X21 \/ ~man $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~of $X15 $X17 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ ~placename $X15 $X20 \/
% 0.52/0.69     ~present $X15 $X22 \/ ~state $X15 $X28 \/ ~street $X15 $X21 \/
% 0.52/0.69     ~two $X15 $X23 \/ ~wheel $X15 $X21 \/ ~white $X15 $X19 \/
% 0.52/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.52/0.69     member $X15 (skolemFOFtoCNF_X31 $X15 $X23 $X24) $X24
% 0.52/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.52/0.69     ~be $X15 $X25 $X21 $X26 \/
% 0.52/0.69     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.52/0.69     ~behind $X15 $X26 $X21 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.52/0.69     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.52/0.69     ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.52/0.69     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.52/0.69     ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/
% 0.52/0.69     ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/
% 0.52/0.69     ~in $X15 $X22 $X21 \/ ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X20 \/
% 0.52/0.69     ~lonely $X15 $X21 \/ ~man $X15 $X21 \/ ~of $X15 $X20 $X21 \/
% 0.52/0.69     ~old $X15 $X19 \/ ~placename $X15 $X20 \/ ~present $X15 $X22 \/
% 0.52/0.69     ~state $X15 $X25 \/ ~state $X15 $X28 \/ ~street $X15 $X21 \/
% 0.52/0.69     ~two $X15 $X23 \/ ~wheel $X15 $X21 \/ ~white $X15 $X19 \/
% 0.52/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.52/0.69     member $X15 (skolemFOFtoCNF_X31 $X15 $X23 $X24) $X24
% 0.52/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.52/0.69     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.52/0.69     ~behind $X15 $X29 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.52/0.69     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.52/0.69     ~city $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~dirty $X15 $X19 \/
% 0.52/0.69     ~down $X15 $X22 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~event $X15 $X22 \/ ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/
% 0.52/0.69     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.52/0.69     ~hollywood_placename $X15 $X20 \/
% 0.52/0.69     ~in $X15 $X22 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X20 \/
% 0.52/0.69     ~lonely $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~man $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~of $X15 $X20 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~old $X15 $X19 \/
% 0.52/0.69     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~state $X15 $X28 \/
% 0.52/0.69     ~street $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~two $X15 $X23 \/
% 0.52/0.69     ~wheel $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~white $X15 $X19 \/
% 0.52/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.52/0.69     member $X15 (skolemFOFtoCNF_X31 $X15 $X23 $X24) $X24
% 0.52/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.52/0.69     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.52/0.69     ~behind $X15 $X29 $X21 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.52/0.69     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.52/0.69     ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.52/0.69     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.52/0.69     ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/
% 0.52/0.69     ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/
% 0.52/0.69     ~in $X15 $X22 $X21 \/ ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X17 \/
% 0.52/0.69     ~lonely $X15 $X21 \/ ~man $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~of $X15 $X17 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ ~placename $X15 $X20 \/
% 0.52/0.69     ~present $X15 $X22 \/ ~state $X15 $X28 \/ ~street $X15 $X21 \/
% 0.52/0.69     ~two $X15 $X23 \/ ~wheel $X15 $X21 \/ ~white $X15 $X19 \/
% 0.52/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.52/0.69     member $X15 (skolemFOFtoCNF_X32 $X15 $X23 $X24) $X23
% 0.52/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.52/0.69     ~be $X15 $X25 $X21 $X26 \/
% 0.52/0.69     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.52/0.69     ~behind $X15 $X26 $X21 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.52/0.69     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.52/0.69     ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.52/0.69     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.52/0.69     ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/
% 0.52/0.69     ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/
% 0.52/0.69     ~in $X15 $X22 $X21 \/ ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X20 \/
% 0.52/0.69     ~lonely $X15 $X21 \/ ~man $X15 $X21 \/ ~of $X15 $X20 $X21 \/
% 0.52/0.69     ~old $X15 $X19 \/ ~placename $X15 $X20 \/ ~present $X15 $X22 \/
% 0.52/0.69     ~state $X15 $X25 \/ ~state $X15 $X28 \/ ~street $X15 $X21 \/
% 0.52/0.69     ~two $X15 $X23 \/ ~wheel $X15 $X21 \/ ~white $X15 $X19 \/
% 0.52/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.52/0.69     member $X15 (skolemFOFtoCNF_X32 $X15 $X23 $X24) $X23
% 0.52/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.52/0.69     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.52/0.69     ~behind $X15 $X29 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.52/0.69     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.52/0.69     ~city $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~dirty $X15 $X19 \/
% 0.52/0.69     ~down $X15 $X22 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~event $X15 $X22 \/ ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/
% 0.52/0.69     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.52/0.69     ~hollywood_placename $X15 $X20 \/
% 0.52/0.69     ~in $X15 $X22 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X20 \/
% 0.52/0.69     ~lonely $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~man $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~of $X15 $X20 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~old $X15 $X19 \/
% 0.52/0.69     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~state $X15 $X28 \/
% 0.52/0.69     ~street $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~two $X15 $X23 \/
% 0.52/0.69     ~wheel $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~white $X15 $X19 \/
% 0.52/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.52/0.69     member $X15 (skolemFOFtoCNF_X32 $X15 $X23 $X24) $X23
% 0.52/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/
% 0.52/0.69     ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/
% 0.52/0.69     ~barrel $X15 $X22 \/ ~be $X15 $X25 $X21 $X26 \/
% 0.52/0.69     ~behind $X15 $X26 $X21 \/ ~chevy $X15 $X19 \/ ~city $X15 $X21 \/
% 0.52/0.69     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.52/0.69     ~event $X15 $X33 \/ ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/
% 0.52/0.69     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.52/0.69     ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/
% 0.52/0.69     ~jules_forename $X15 $X20 \/ ~lonely $X15 $X21 \/ ~man $X15 $X21 \/
% 0.52/0.69     ~nonreflexive $X15 $X33 \/ ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/
% 0.52/0.69     ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/
% 0.52/0.69     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/
% 0.52/0.69     ~state $X15 $X25 \/ ~street $X15 $X21 \/ ~two $X15 $X23 \/
% 0.52/0.69     ~wear $X15 $X33 \/ ~wheel $X15 $X21 \/ ~white $X15 $X19 \/
% 0.52/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.52/0.69     member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23 \/
% 0.52/0.69     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.52/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/
% 0.52/0.69     ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/
% 0.52/0.69     ~barrel $X15 $X22 \/
% 0.52/0.69     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.52/0.69     ~behind $X15 $X29 $X21 \/ ~chevy $X15 $X19 \/ ~city $X15 $X21 \/
% 0.52/0.69     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.52/0.69     ~event $X15 $X33 \/ ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/
% 0.52/0.69     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.52/0.69     ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/
% 0.52/0.69     ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X17 \/ ~lonely $X15 $X21 \/
% 0.52/0.69     ~man $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~nonreflexive $X15 $X33 \/
% 0.52/0.69     ~of $X15 $X17 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/
% 0.52/0.69     ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/
% 0.52/0.69     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/
% 0.52/0.69     ~state $X15 $X28 \/ ~street $X15 $X21 \/ ~two $X15 $X23 \/
% 0.52/0.69     ~wear $X15 $X33 \/ ~wheel $X15 $X21 \/ ~white $X15 $X19 \/
% 0.52/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.52/0.69     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.52/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/
% 0.52/0.69     ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/
% 0.52/0.69     ~barrel $X15 $X22 \/ ~be $X15 $X25 $X21 $X26 \/
% 0.52/0.69     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.52/0.69     ~behind $X15 $X26 $X21 \/ ~chevy $X15 $X19 \/ ~city $X15 $X21 \/
% 0.52/0.69     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.52/0.69     ~event $X15 $X33 \/ ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/
% 0.52/0.69     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.52/0.69     ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/
% 0.52/0.69     ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X20 \/ ~lonely $X15 $X21 \/
% 0.52/0.69     ~man $X15 $X21 \/ ~nonreflexive $X15 $X33 \/ ~of $X15 $X20 $X21 \/
% 0.52/0.69     ~old $X15 $X19 \/
% 0.52/0.69     ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/
% 0.52/0.69     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/
% 0.52/0.69     ~state $X15 $X25 \/ ~state $X15 $X28 \/ ~street $X15 $X21 \/
% 0.52/0.69     ~two $X15 $X23 \/ ~wear $X15 $X33 \/ ~wheel $X15 $X21 \/
% 0.52/0.69     ~white $X15 $X19 \/
% 0.52/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.52/0.69     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.52/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/
% 0.52/0.69     ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/
% 0.52/0.69     ~barrel $X15 $X22 \/
% 0.52/0.69     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.52/0.69     ~behind $X15 $X29 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~chevy $X15 $X19 \/ ~city $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~dirty $X15 $X19 \/
% 0.52/0.69     ~down $X15 $X22 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~event $X15 $X22 \/ ~event $X15 $X33 \/ ~forename $X15 $X20 \/
% 0.52/0.69     ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.52/0.69     ~hollywood_placename $X15 $X20 \/
% 0.52/0.69     ~in $X15 $X22 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X20 \/
% 0.52/0.69     ~lonely $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~man $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~nonreflexive $X15 $X33 \/
% 0.52/0.69     ~of $X15 $X20 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~old $X15 $X19 \/
% 0.52/0.69     ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/
% 0.52/0.69     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/
% 0.52/0.69     ~state $X15 $X28 \/ ~street $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~two $X15 $X23 \/ ~wear $X15 $X33 \/
% 0.52/0.69     ~wheel $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~white $X15 $X19 \/
% 0.52/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.52/0.69     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.52/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/
% 0.52/0.69     ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/
% 0.52/0.69     ~barrel $X15 $X22 \/ ~be $X15 $X25 $X21 $X26 \/
% 0.52/0.69     ~behind $X15 $X26 $X21 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.52/0.69     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.52/0.69     ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.52/0.69     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.52/0.69     ~event $X15 $X33 \/ ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/
% 0.52/0.69     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.52/0.69     ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/
% 0.52/0.69     ~jules_forename $X15 $X20 \/ ~lonely $X15 $X21 \/ ~man $X15 $X21 \/
% 0.52/0.69     ~nonreflexive $X15 $X33 \/ ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/
% 0.52/0.69     ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/
% 0.52/0.69     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/
% 0.52/0.69     ~state $X15 $X25 \/ ~street $X15 $X21 \/ ~two $X15 $X23 \/
% 0.52/0.69     ~wear $X15 $X33 \/ ~wheel $X15 $X21 \/ ~white $X15 $X19 \/
% 0.52/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.52/0.69     member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23
% 0.52/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/
% 0.52/0.69     ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/
% 0.52/0.69     ~barrel $X15 $X22 \/
% 0.52/0.69     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.52/0.69     ~behind $X15 $X29 $X21 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.52/0.69     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.52/0.69     ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.52/0.69     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.52/0.69     ~event $X15 $X33 \/ ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/
% 0.52/0.69     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.52/0.69     ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/
% 0.52/0.69     ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X17 \/ ~lonely $X15 $X21 \/
% 0.52/0.69     ~man $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~nonreflexive $X15 $X33 \/
% 0.52/0.69     ~of $X15 $X17 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/
% 0.52/0.69     ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/
% 0.52/0.69     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/
% 0.52/0.69     ~state $X15 $X28 \/ ~street $X15 $X21 \/ ~two $X15 $X23 \/
% 0.52/0.69     ~wear $X15 $X33 \/ ~wheel $X15 $X21 \/ ~white $X15 $X19 \/
% 0.52/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23)
% 0.52/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/
% 0.52/0.69     ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/
% 0.52/0.69     ~barrel $X15 $X22 \/ ~be $X15 $X25 $X21 $X26 \/
% 0.52/0.69     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.52/0.69     ~behind $X15 $X26 $X21 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.52/0.69     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.52/0.69     ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.52/0.69     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.52/0.69     ~event $X15 $X33 \/ ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/
% 0.52/0.69     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.52/0.69     ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/
% 0.52/0.69     ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X20 \/ ~lonely $X15 $X21 \/
% 0.52/0.69     ~man $X15 $X21 \/ ~nonreflexive $X15 $X33 \/ ~of $X15 $X20 $X21 \/
% 0.52/0.69     ~old $X15 $X19 \/
% 0.52/0.69     ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/
% 0.52/0.69     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/
% 0.52/0.69     ~state $X15 $X25 \/ ~state $X15 $X28 \/ ~street $X15 $X21 \/
% 0.52/0.69     ~two $X15 $X23 \/ ~wear $X15 $X33 \/ ~wheel $X15 $X21 \/
% 0.52/0.69     ~white $X15 $X19 \/
% 0.52/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23)
% 0.52/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/
% 0.52/0.69     ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/
% 0.52/0.69     ~barrel $X15 $X22 \/
% 0.52/0.69     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.52/0.69     ~behind $X15 $X29 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.52/0.69     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.52/0.69     ~city $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~dirty $X15 $X19 \/
% 0.52/0.69     ~down $X15 $X22 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~event $X15 $X22 \/ ~event $X15 $X33 \/ ~forename $X15 $X20 \/
% 0.52/0.69     ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.52/0.69     ~hollywood_placename $X15 $X20 \/
% 0.52/0.69     ~in $X15 $X22 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X20 \/
% 0.52/0.69     ~lonely $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~man $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~nonreflexive $X15 $X33 \/
% 0.52/0.69     ~of $X15 $X20 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~old $X15 $X19 \/
% 0.52/0.69     ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/
% 0.52/0.69     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/
% 0.52/0.69     ~state $X15 $X28 \/ ~street $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.52/0.69     ~two $X15 $X23 \/ ~wear $X15 $X33 \/
% 0.52/0.69     ~wheel $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~white $X15 $X19 \/
% 0.52/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23)
% 0.52/0.69  |- ~agent skolemFOFtoCNF_U $_45 $_43 \/ ~barrel skolemFOFtoCNF_U $_45 \/
% 0.52/0.69     ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 skolemFOFtoCNF_V \/
% 0.52/0.69     ~chevy skolemFOFtoCNF_U $_43 \/
% 0.52/0.69     ~city skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.52/0.69     ~dirty skolemFOFtoCNF_U $_43 \/
% 0.52/0.69     ~down skolemFOFtoCNF_U $_45 skolemFOFtoCNF_V \/
% 0.52/0.69     ~event skolemFOFtoCNF_U $_45 \/ ~frontseat skolemFOFtoCNF_U $_42 \/
% 0.52/0.69     ~group skolemFOFtoCNF_U $_46 \/ ~group skolemFOFtoCNF_U $_47 \/
% 0.52/0.69     ~hollywood_placename skolemFOFtoCNF_U skolemFOFtoCNF_W \/
% 0.52/0.69     ~in skolemFOFtoCNF_U $_45 skolemFOFtoCNF_V \/
% 0.52/0.69     ~lonely skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.52/0.69     ~old skolemFOFtoCNF_U $_43 \/
% 0.52/0.69     ~placename skolemFOFtoCNF_U skolemFOFtoCNF_W \/
% 0.52/0.69     ~present skolemFOFtoCNF_U $_45 \/
% 0.52/0.69     ~street skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.52/0.69     ~two skolemFOFtoCNF_U $_46 \/
% 0.52/0.69     ~wheel skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.52/0.69     ~white skolemFOFtoCNF_U $_43 \/
% 0.52/0.69     definitionFOFtoCNF_0 skolemFOFtoCNF_U $_46
% 0.52/0.69       (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_46) \/
% 0.52/0.69     member skolemFOFtoCNF_U (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_42 $_46)
% 0.52/0.69       $_46 \/
% 0.52/0.69     member skolemFOFtoCNF_U (skolemFOFtoCNF_X32 skolemFOFtoCNF_U $_46 $_47)
% 0.52/0.69       $_46 \/
% 0.52/0.69     member skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_47) $_47
% 0.52/0.69  |- ~agent skolemFOFtoCNF_U $_66 $_64 \/ ~barrel skolemFOFtoCNF_U $_66 \/
% 0.52/0.69     ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 skolemFOFtoCNF_V \/
% 0.52/0.69     ~chevy skolemFOFtoCNF_U $_64 \/
% 0.52/0.69     ~city skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.52/0.69     ~dirty skolemFOFtoCNF_U $_64 \/
% 0.52/0.69     ~down skolemFOFtoCNF_U $_66 skolemFOFtoCNF_V \/
% 0.52/0.69     ~event skolemFOFtoCNF_U $_66 \/ ~frontseat skolemFOFtoCNF_U $_63 \/
% 0.52/0.69     ~group skolemFOFtoCNF_U $_67 \/ ~group skolemFOFtoCNF_U $_68 \/
% 0.52/0.69     ~hollywood_placename skolemFOFtoCNF_U skolemFOFtoCNF_W \/
% 0.52/0.69     ~in skolemFOFtoCNF_U $_66 skolemFOFtoCNF_V \/
% 0.52/0.69     ~lonely skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.52/0.69     ~old skolemFOFtoCNF_U $_64 \/
% 0.52/0.69     ~placename skolemFOFtoCNF_U skolemFOFtoCNF_W \/
% 0.52/0.69     ~present skolemFOFtoCNF_U $_66 \/
% 0.52/0.69     ~street skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.52/0.69     ~two skolemFOFtoCNF_U $_67 \/
% 0.52/0.69     ~wheel skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.52/0.69     ~white skolemFOFtoCNF_U $_64 \/
% 0.52/0.69     definitionFOFtoCNF_0 skolemFOFtoCNF_U $_67
% 0.52/0.69       (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_67) \/
% 0.52/0.69     member skolemFOFtoCNF_U (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_63 $_67)
% 0.52/0.69       $_67 \/
% 0.52/0.69     member skolemFOFtoCNF_U (skolemFOFtoCNF_X31 skolemFOFtoCNF_U $_67 $_68)
% 0.52/0.69       $_68 \/
% 0.52/0.69     member skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_68) $_68
% 0.52/0.69  |- ~agent skolemFOFtoCNF_U $_97 $_94 \/ ~barrel skolemFOFtoCNF_U $_97 \/
% 0.52/0.69     ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 skolemFOFtoCNF_V \/
% 0.52/0.69     ~black skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_99) \/
% 0.52/0.69     ~cheap skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_99) \/
% 0.52/0.69     ~chevy skolemFOFtoCNF_U $_94 \/
% 0.52/0.69     ~city skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.52/0.69     ~coat skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_99) \/
% 0.52/0.69     ~dirty skolemFOFtoCNF_U $_94 \/
% 0.52/0.69     ~down skolemFOFtoCNF_U $_97 skolemFOFtoCNF_V \/
% 0.52/0.69     ~event skolemFOFtoCNF_U $_97 \/ ~forename skolemFOFtoCNF_U $_95 \/
% 0.52/0.69     ~frontseat skolemFOFtoCNF_U $_93 \/ ~group skolemFOFtoCNF_U $_98 \/
% 0.52/0.69     ~group skolemFOFtoCNF_U $_99 \/
% 0.52/0.69     ~hollywood_placename skolemFOFtoCNF_U $_95 \/
% 0.52/0.69     ~in skolemFOFtoCNF_U $_97 skolemFOFtoCNF_V \/
% 0.52/0.69     ~jules_forename skolemFOFtoCNF_U $_95 \/
% 0.52/0.69     ~lonely skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.52/0.69     ~of skolemFOFtoCNF_U $_95 skolemFOFtoCNF_V \/
% 0.52/0.69     ~old skolemFOFtoCNF_U $_94 \/ ~placename skolemFOFtoCNF_U $_95 \/
% 0.52/0.69     ~present skolemFOFtoCNF_U $_97 \/
% 0.52/0.69     ~street skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.52/0.69     ~two skolemFOFtoCNF_U $_98 \/
% 0.52/0.69     ~wheel skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.52/0.69     ~white skolemFOFtoCNF_U $_94 \/
% 0.52/0.69     definitionFOFtoCNF_0 skolemFOFtoCNF_U $_98
% 0.52/0.69       (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_98) \/
% 0.52/0.69     member skolemFOFtoCNF_U (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_93 $_98)
% 0.52/0.69       $_98 \/
% 0.52/0.69     member skolemFOFtoCNF_U (skolemFOFtoCNF_X31 skolemFOFtoCNF_U $_98 $_99)
% 0.52/0.69       $_99
% 0.52/0.69  |- ~agent skolemFOFtoCNF_U $_113 $_110 \/ ~barrel skolemFOFtoCNF_U $_113 \/
% 0.52/0.69     ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 skolemFOFtoCNF_V \/
% 0.52/0.69     ~black skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_115) \/
% 0.52/0.69     ~cheap skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_115) \/
% 0.52/0.69     ~chevy skolemFOFtoCNF_U $_110 \/
% 0.52/0.69     ~city skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.52/0.69     ~coat skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_115) \/
% 0.52/0.69     ~dirty skolemFOFtoCNF_U $_110 \/
% 0.52/0.69     ~down skolemFOFtoCNF_U $_113 skolemFOFtoCNF_V \/
% 0.52/0.69     ~event skolemFOFtoCNF_U $_113 \/ ~forename skolemFOFtoCNF_U $_111 \/
% 0.52/0.69     ~frontseat skolemFOFtoCNF_U $_109 \/ ~group skolemFOFtoCNF_U $_114 \/
% 0.52/0.69     ~group skolemFOFtoCNF_U $_115 \/
% 0.52/0.69     ~hollywood_placename skolemFOFtoCNF_U $_111 \/
% 0.52/0.69     ~in skolemFOFtoCNF_U $_113 skolemFOFtoCNF_V \/
% 0.52/0.69     ~jules_forename skolemFOFtoCNF_U $_111 \/
% 0.52/0.69     ~lonely skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.52/0.69     ~of skolemFOFtoCNF_U $_111 skolemFOFtoCNF_V \/
% 0.52/0.69     ~old skolemFOFtoCNF_U $_110 \/ ~placename skolemFOFtoCNF_U $_111 \/
% 0.52/0.69     ~present skolemFOFtoCNF_U $_113 \/
% 0.52/0.69     ~street skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.52/0.69     ~two skolemFOFtoCNF_U $_114 \/
% 0.52/0.69     ~wheel skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.52/0.69     ~white skolemFOFtoCNF_U $_110 \/
% 0.52/0.69     definitionFOFtoCNF_0 skolemFOFtoCNF_U $_114
% 0.52/0.69       (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_114) \/
% 0.52/0.69     member skolemFOFtoCNF_U
% 0.52/0.69       (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_109 $_114) $_114 \/
% 0.52/0.69     member skolemFOFtoCNF_U
% 0.52/0.69       (skolemFOFtoCNF_X32 skolemFOFtoCNF_U $_114 $_115) $_114
% 0.52/0.69  |- ~agent skolemFOFtoCNF_U $_163 $_160 \/ ~barrel skolemFOFtoCNF_U $_163 \/
% 0.52/0.69     ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_162 \/
% 0.52/0.69     ~chevy skolemFOFtoCNF_U $_160 \/ ~city skolemFOFtoCNF_U $_162 \/
% 0.52/0.69     ~dirty skolemFOFtoCNF_U $_160 \/ ~down skolemFOFtoCNF_U $_163 $_162 \/
% 0.52/0.69     ~event skolemFOFtoCNF_U $_163 \/ ~frontseat skolemFOFtoCNF_U $_159 \/
% 0.52/0.69     ~group skolemFOFtoCNF_U $_164 \/ ~group skolemFOFtoCNF_U $_165 \/
% 0.52/0.69     ~hollywood_placename skolemFOFtoCNF_U $_161 \/
% 0.52/0.69     ~in skolemFOFtoCNF_U $_163 $_162 \/ ~lonely skolemFOFtoCNF_U $_162 \/
% 0.52/0.69     ~of skolemFOFtoCNF_U $_161 $_162 \/ ~old skolemFOFtoCNF_U $_160 \/
% 0.52/0.69     ~placename skolemFOFtoCNF_U $_161 \/ ~present skolemFOFtoCNF_U $_163 \/
% 0.52/0.69     ~street skolemFOFtoCNF_U $_162 \/ ~two skolemFOFtoCNF_U $_164 \/
% 0.52/0.69     ~wheel skolemFOFtoCNF_U $_162 \/ ~white skolemFOFtoCNF_U $_160 \/
% 0.52/0.69     definitionFOFtoCNF_0 skolemFOFtoCNF_U $_164
% 0.52/0.69       (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_164) \/
% 0.52/0.69     member skolemFOFtoCNF_U
% 0.52/0.69       (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_159 $_164) $_164 \/
% 0.52/0.69     member skolemFOFtoCNF_U
% 0.52/0.69       (skolemFOFtoCNF_X31 skolemFOFtoCNF_U $_164 $_165) $_165 \/
% 0.52/0.69     member skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_165)
% 0.52/0.69       $_165
% 0.52/0.70  |- ~agent skolemFOFtoCNF_U $_169 $_168 \/ ~barrel skolemFOFtoCNF_U $_169 \/
% 0.52/0.70     ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 skolemFOFtoCNF_X1 \/
% 0.52/0.70     ~chevy skolemFOFtoCNF_U $_168 \/ ~dirty skolemFOFtoCNF_U $_168 \/
% 0.52/0.70     ~down skolemFOFtoCNF_U $_169 skolemFOFtoCNF_X1 \/
% 0.52/0.70     ~event skolemFOFtoCNF_U $_169 \/ ~frontseat skolemFOFtoCNF_U $_167 \/
% 0.52/0.70     ~group skolemFOFtoCNF_U $_170 \/ ~group skolemFOFtoCNF_U $_171 \/
% 0.52/0.70     ~in skolemFOFtoCNF_U $_169 skolemFOFtoCNF_X1 \/
% 0.52/0.70     ~old skolemFOFtoCNF_U $_168 \/ ~present skolemFOFtoCNF_U $_169 \/
% 0.52/0.70     ~two skolemFOFtoCNF_U $_170 \/
% 0.52/0.70     ~wheel skolemFOFtoCNF_U skolemFOFtoCNF_X1 \/
% 0.52/0.70     ~white skolemFOFtoCNF_U $_168 \/
% 0.52/0.70     definitionFOFtoCNF_0 skolemFOFtoCNF_U $_170
% 0.52/0.70       (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_170) \/
% 0.52/0.70     member skolemFOFtoCNF_U
% 0.52/0.70       (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_167 $_170) $_170 \/
% 0.52/0.70     member skolemFOFtoCNF_U
% 0.52/0.70       (skolemFOFtoCNF_X31 skolemFOFtoCNF_U $_170 $_171) $_171 \/
% 0.52/0.70     member skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_171)
% 0.52/0.70       $_171
% 0.52/0.70  |- ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X2 $_173 \/
% 0.52/0.70     ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 skolemFOFtoCNF_X1 \/
% 0.52/0.70     ~chevy skolemFOFtoCNF_U $_173 \/ ~dirty skolemFOFtoCNF_U $_173 \/
% 0.52/0.70     ~frontseat skolemFOFtoCNF_U $_172 \/ ~group skolemFOFtoCNF_U $_175 \/
% 0.52/0.70     ~group skolemFOFtoCNF_U $_176 \/ ~old skolemFOFtoCNF_U $_173 \/
% 0.52/0.70     ~two skolemFOFtoCNF_U $_175 \/
% 0.52/0.70     ~wheel skolemFOFtoCNF_U skolemFOFtoCNF_X1 \/
% 0.52/0.70     ~white skolemFOFtoCNF_U $_173 \/
% 0.52/0.70     definitionFOFtoCNF_0 skolemFOFtoCNF_U $_175
% 0.52/0.70       (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_175) \/
% 0.52/0.70     member skolemFOFtoCNF_U
% 0.52/0.70       (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_172 $_175) $_175 \/
% 0.52/0.70     member skolemFOFtoCNF_U
% 0.52/0.70       (skolemFOFtoCNF_X31 skolemFOFtoCNF_U $_175 $_176) $_176 \/
% 0.52/0.70     member skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_176)
% 0.52/0.70       $_176
% 0.52/0.70  |- ~agent skolemFOFtoCNF_U $_205 $_202 \/ ~barrel skolemFOFtoCNF_U $_205 \/
% 0.52/0.70     ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_204 \/
% 0.52/0.70     ~chevy skolemFOFtoCNF_U $_202 \/ ~city skolemFOFtoCNF_U $_204 \/
% 0.52/0.70     ~dirty skolemFOFtoCNF_U $_202 \/ ~down skolemFOFtoCNF_U $_205 $_204 \/
% 0.52/0.70     ~event skolemFOFtoCNF_U $_205 \/ ~frontseat skolemFOFtoCNF_U $_201 \/
% 0.52/0.70     ~group skolemFOFtoCNF_U $_206 \/ ~group skolemFOFtoCNF_U $_207 \/
% 0.52/0.70     ~hollywood_placename skolemFOFtoCNF_U $_203 \/
% 0.52/0.70     ~in skolemFOFtoCNF_U $_205 $_204 \/ ~lonely skolemFOFtoCNF_U $_204 \/
% 0.52/0.70     ~of skolemFOFtoCNF_U $_203 $_204 \/ ~old skolemFOFtoCNF_U $_202 \/
% 0.52/0.70     ~placename skolemFOFtoCNF_U $_203 \/ ~present skolemFOFtoCNF_U $_205 \/
% 0.52/0.70     ~street skolemFOFtoCNF_U $_204 \/ ~two skolemFOFtoCNF_U $_206 \/
% 0.52/0.70     ~wheel skolemFOFtoCNF_U $_204 \/ ~white skolemFOFtoCNF_U $_202 \/
% 0.52/0.70     definitionFOFtoCNF_0 skolemFOFtoCNF_U $_206
% 0.52/0.70       (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_206) \/
% 0.52/0.70     member skolemFOFtoCNF_U
% 0.52/0.70       (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_201 $_206) $_206 \/
% 0.52/0.70     member skolemFOFtoCNF_U
% 0.52/0.70       (skolemFOFtoCNF_X32 skolemFOFtoCNF_U $_206 $_207) $_206 \/
% 0.52/0.70     member skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_207)
% 0.52/0.70       $_207
% 0.52/0.70  |- ~agent skolemFOFtoCNF_U $_211 $_210 \/ ~barrel skolemFOFtoCNF_U $_211 \/
% 0.52/0.70     ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 skolemFOFtoCNF_X1 \/
% 0.52/0.70     ~chevy skolemFOFtoCNF_U $_210 \/ ~dirty skolemFOFtoCNF_U $_210 \/
% 0.52/0.70     ~down skolemFOFtoCNF_U $_211 skolemFOFtoCNF_X1 \/
% 0.52/0.70     ~event skolemFOFtoCNF_U $_211 \/ ~frontseat skolemFOFtoCNF_U $_209 \/
% 0.52/0.70     ~group skolemFOFtoCNF_U $_212 \/ ~group skolemFOFtoCNF_U $_213 \/
% 0.52/0.70     ~in skolemFOFtoCNF_U $_211 skolemFOFtoCNF_X1 \/
% 0.52/0.70     ~old skolemFOFtoCNF_U $_210 \/ ~present skolemFOFtoCNF_U $_211 \/
% 0.52/0.70     ~two skolemFOFtoCNF_U $_212 \/
% 0.52/0.70     ~wheel skolemFOFtoCNF_U skolemFOFtoCNF_X1 \/
% 0.52/0.70     ~white skolemFOFtoCNF_U $_210 \/
% 0.52/0.70     definitionFOFtoCNF_0 skolemFOFtoCNF_U $_212
% 0.52/0.70       (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_212) \/
% 0.52/0.70     member skolemFOFtoCNF_U
% 0.52/0.70       (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_209 $_212) $_212 \/
% 0.52/0.70     member skolemFOFtoCNF_U
% 0.52/0.70       (skolemFOFtoCNF_X32 skolemFOFtoCNF_U $_212 $_213) $_212 \/
% 0.52/0.70     member skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_213)
% 0.52/0.70       $_213
% 0.52/0.70  |- ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X2 $_215 \/
% 0.52/0.70     ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 skolemFOFtoCNF_X1 \/
% 0.52/0.70     ~chevy skolemFOFtoCNF_U $_215 \/ ~dirty skolemFOFtoCNF_U $_215 \/
% 0.52/0.70     ~frontseat skolemFOFtoCNF_U $_214 \/ ~group skolemFOFtoCNF_U $_217 \/
% 0.52/0.70     ~group skolemFOFtoCNF_U $_218 \/ ~old skolemFOFtoCNF_U $_215 \/
% 0.52/0.70     ~two skolemFOFtoCNF_U $_217 \/
% 0.52/0.70     ~wheel skolemFOFtoCNF_U skolemFOFtoCNF_X1 \/
% 0.52/0.70     ~white skolemFOFtoCNF_U $_215 \/
% 0.52/0.70     definitionFOFtoCNF_0 skolemFOFtoCNF_U $_217
% 0.52/0.70       (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_217) \/
% 0.52/0.70     member skolemFOFtoCNF_U
% 0.52/0.70       (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_214 $_217) $_217 \/
% 0.52/0.70     member skolemFOFtoCNF_U
% 0.52/0.70       (skolemFOFtoCNF_X32 skolemFOFtoCNF_U $_217 $_218) $_217 \/
% 0.52/0.70     member skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_218)
% 0.52/0.70       $_218
% 0.52/0.70  |- ~agent skolemFOFtoCNF_U $_301 $_298 \/ ~barrel skolemFOFtoCNF_U $_301 \/
% 0.52/0.70     ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_300 \/
% 0.52/0.70     ~black skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_303) \/
% 0.52/0.70     ~cheap skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_303) \/
% 0.52/0.70     ~chevy skolemFOFtoCNF_U $_298 \/ ~city skolemFOFtoCNF_U $_300 \/
% 0.52/0.70     ~coat skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_303) \/
% 0.52/0.70     ~dirty skolemFOFtoCNF_U $_298 \/ ~down skolemFOFtoCNF_U $_301 $_300 \/
% 0.52/0.70     ~event skolemFOFtoCNF_U $_301 \/ ~forename skolemFOFtoCNF_U $_296 \/
% 0.52/0.70     ~frontseat skolemFOFtoCNF_U $_297 \/ ~group skolemFOFtoCNF_U $_302 \/
% 0.52/0.70     ~group skolemFOFtoCNF_U $_303 \/
% 0.52/0.70     ~hollywood_placename skolemFOFtoCNF_U $_299 \/
% 0.52/0.70     ~in skolemFOFtoCNF_U $_301 $_300 \/
% 0.52/0.70     ~jules_forename skolemFOFtoCNF_U $_296 \/
% 0.52/0.70     ~lonely skolemFOFtoCNF_U $_300 \/
% 0.52/0.70     ~of skolemFOFtoCNF_U $_296 skolemFOFtoCNF_V \/
% 0.52/0.70     ~of skolemFOFtoCNF_U $_299 $_300 \/ ~old skolemFOFtoCNF_U $_298 \/
% 0.52/0.70     ~placename skolemFOFtoCNF_U $_299 \/ ~present skolemFOFtoCNF_U $_301 \/
% 0.52/0.70     ~street skolemFOFtoCNF_U $_300 \/ ~two skolemFOFtoCNF_U $_302 \/
% 0.52/0.70     ~wheel skolemFOFtoCNF_U $_300 \/ ~white skolemFOFtoCNF_U $_298 \/
% 0.52/0.70     definitionFOFtoCNF_0 skolemFOFtoCNF_U $_302
% 0.52/0.70       (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_302) \/
% 0.52/0.70     member skolemFOFtoCNF_U
% 0.52/0.70       (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_297 $_302) $_302 \/
% 0.52/0.70     member skolemFOFtoCNF_U
% 0.52/0.70       (skolemFOFtoCNF_X31 skolemFOFtoCNF_U $_302 $_303) $_303
% 0.52/0.70  |- ~agent skolemFOFtoCNF_U $_321 $_318 \/ ~barrel skolemFOFtoCNF_U $_321 \/
% 0.52/0.70     ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_320 \/
% 0.52/0.70     ~black skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_323) \/
% 0.52/0.70     ~cheap skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_323) \/
% 0.52/0.70     ~chevy skolemFOFtoCNF_U $_318 \/ ~city skolemFOFtoCNF_U $_320 \/
% 0.52/0.70     ~coat skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_323) \/
% 0.52/0.70     ~dirty skolemFOFtoCNF_U $_318 \/ ~down skolemFOFtoCNF_U $_321 $_320 \/
% 0.52/0.70     ~event skolemFOFtoCNF_U $_321 \/ ~forename skolemFOFtoCNF_U $_316 \/
% 0.52/0.70     ~frontseat skolemFOFtoCNF_U $_317 \/ ~group skolemFOFtoCNF_U $_322 \/
% 0.52/0.70     ~group skolemFOFtoCNF_U $_323 \/
% 0.52/0.70     ~hollywood_placename skolemFOFtoCNF_U $_319 \/
% 0.52/0.70     ~in skolemFOFtoCNF_U $_321 $_320 \/
% 0.52/0.70     ~jules_forename skolemFOFtoCNF_U $_316 \/
% 0.52/0.70     ~lonely skolemFOFtoCNF_U $_320 \/
% 0.52/0.70     ~of skolemFOFtoCNF_U $_316 skolemFOFtoCNF_V \/
% 0.52/0.70     ~of skolemFOFtoCNF_U $_319 $_320 \/ ~old skolemFOFtoCNF_U $_318 \/
% 0.52/0.70     ~placename skolemFOFtoCNF_U $_319 \/ ~present skolemFOFtoCNF_U $_321 \/
% 0.52/0.70     ~street skolemFOFtoCNF_U $_320 \/ ~two skolemFOFtoCNF_U $_322 \/
% 0.52/0.70     ~wheel skolemFOFtoCNF_U $_320 \/ ~white skolemFOFtoCNF_U $_318 \/
% 0.52/0.70     definitionFOFtoCNF_0 skolemFOFtoCNF_U $_322
% 0.52/0.70       (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_322) \/
% 0.52/0.70     member skolemFOFtoCNF_U
% 0.52/0.70       (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_317 $_322) $_322 \/
% 0.52/0.70     member skolemFOFtoCNF_U
% 0.52/0.70       (skolemFOFtoCNF_X32 skolemFOFtoCNF_U $_322 $_323) $_322
% 0.52/0.70  SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.52/0.70  
%------------------------------------------------------------------------------