↑ Up

Metis---2.4.CSA-Sat.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : Metis---2.4
% Problem  : NLP195+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:15:56 EDT 2022

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

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12  % Problem  : NLP195+1 : TPTP v8.1.0. Released v2.4.0.
% 0.11/0.13  % Command  : metis --show proof --show saturation %s
% 0.13/0.34  % Computer : n014.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 : Fri Jul  1 06:38:56 EDT 2022
% 0.13/0.34  % CPUTime  : 
% 0.13/0.34  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.48/0.68  % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.48/0.68  
% 0.48/0.68  SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.48/0.68  |- actual_world skolemFOFtoCNF_U
% 0.48/0.68  |- agent skolemFOFtoCNF_U skolemFOFtoCNF_X2 skolemFOFtoCNF_Y
% 0.48/0.68  |- barrel skolemFOFtoCNF_U skolemFOFtoCNF_X2
% 0.48/0.68  |- be skolemFOFtoCNF_U skolemFOFtoCNF_X5 skolemFOFtoCNF_V skolemFOFtoCNF_X6
% 0.48/0.68  |- behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 skolemFOFtoCNF_X
% 0.48/0.68  |- chevy skolemFOFtoCNF_U skolemFOFtoCNF_Y
% 0.48/0.68  |- city skolemFOFtoCNF_U skolemFOFtoCNF_X1
% 0.48/0.68  |- dirty skolemFOFtoCNF_U skolemFOFtoCNF_Y
% 0.48/0.68  |- down skolemFOFtoCNF_U skolemFOFtoCNF_X2 skolemFOFtoCNF_X1
% 0.48/0.68  |- event skolemFOFtoCNF_U skolemFOFtoCNF_X2
% 0.48/0.68  |- forename skolemFOFtoCNF_U skolemFOFtoCNF_W
% 0.48/0.68  |- frontseat skolemFOFtoCNF_U skolemFOFtoCNF_X
% 0.48/0.68  |- group skolemFOFtoCNF_U skolemFOFtoCNF_X3
% 0.48/0.68  |- group skolemFOFtoCNF_U skolemFOFtoCNF_X4
% 0.48/0.68  |- hollywood_placename skolemFOFtoCNF_U skolemFOFtoCNF_Z
% 0.48/0.68  |- in skolemFOFtoCNF_U skolemFOFtoCNF_X2 skolemFOFtoCNF_X1
% 0.48/0.68  |- jules_forename skolemFOFtoCNF_U skolemFOFtoCNF_W
% 0.48/0.68  |- lonely skolemFOFtoCNF_U skolemFOFtoCNF_X1
% 0.48/0.68  |- man skolemFOFtoCNF_U skolemFOFtoCNF_V
% 0.48/0.68  |- of skolemFOFtoCNF_U skolemFOFtoCNF_W skolemFOFtoCNF_V
% 0.48/0.68  |- of skolemFOFtoCNF_U skolemFOFtoCNF_Z skolemFOFtoCNF_X1
% 0.48/0.68  |- old skolemFOFtoCNF_U skolemFOFtoCNF_Y
% 0.48/0.68  |- placename skolemFOFtoCNF_U skolemFOFtoCNF_Z
% 0.48/0.68  |- present skolemFOFtoCNF_U skolemFOFtoCNF_X2
% 0.48/0.68  |- state skolemFOFtoCNF_U skolemFOFtoCNF_X5
% 0.48/0.68  |- street skolemFOFtoCNF_U skolemFOFtoCNF_X1
% 0.48/0.68  |- two skolemFOFtoCNF_U skolemFOFtoCNF_X3
% 0.48/0.68  |- wheel skolemFOFtoCNF_U skolemFOFtoCNF_X
% 0.48/0.68  |- white skolemFOFtoCNF_U skolemFOFtoCNF_Y
% 0.48/0.68  |- ~member skolemFOFtoCNF_U $X10 skolemFOFtoCNF_X3 \/
% 0.48/0.68     fellow skolemFOFtoCNF_U $X10
% 0.48/0.68  |- ~member skolemFOFtoCNF_U $X10 skolemFOFtoCNF_X3 \/
% 0.48/0.68     young skolemFOFtoCNF_U $X10
% 0.48/0.68  |- ~member skolemFOFtoCNF_U $X11 skolemFOFtoCNF_X4 \/
% 0.48/0.68     ~member skolemFOFtoCNF_U $X12 skolemFOFtoCNF_X3 \/
% 0.48/0.68     agent skolemFOFtoCNF_U (skolemFOFtoCNF_X13 $X11 $X12) $X12
% 0.48/0.68  |- ~member skolemFOFtoCNF_U $X11 skolemFOFtoCNF_X4 \/
% 0.48/0.68     ~member skolemFOFtoCNF_U $X12 skolemFOFtoCNF_X3 \/
% 0.48/0.68     event skolemFOFtoCNF_U (skolemFOFtoCNF_X13 $X11 $X12)
% 0.48/0.68  |- ~member skolemFOFtoCNF_U $X11 skolemFOFtoCNF_X4 \/
% 0.48/0.68     ~member skolemFOFtoCNF_U $X12 skolemFOFtoCNF_X3 \/
% 0.48/0.68     nonreflexive skolemFOFtoCNF_U (skolemFOFtoCNF_X13 $X11 $X12)
% 0.48/0.68  |- ~member skolemFOFtoCNF_U $X11 skolemFOFtoCNF_X4 \/
% 0.48/0.68     ~member skolemFOFtoCNF_U $X12 skolemFOFtoCNF_X3 \/
% 0.48/0.68     patient skolemFOFtoCNF_U (skolemFOFtoCNF_X13 $X11 $X12) $X11
% 0.48/0.68  |- ~member skolemFOFtoCNF_U $X11 skolemFOFtoCNF_X4 \/
% 0.48/0.68     ~member skolemFOFtoCNF_U $X12 skolemFOFtoCNF_X3 \/
% 0.48/0.68     present skolemFOFtoCNF_U (skolemFOFtoCNF_X13 $X11 $X12)
% 0.48/0.68  |- ~member skolemFOFtoCNF_U $X11 skolemFOFtoCNF_X4 \/
% 0.48/0.68     ~member skolemFOFtoCNF_U $X12 skolemFOFtoCNF_X3 \/
% 0.48/0.68     wear skolemFOFtoCNF_U (skolemFOFtoCNF_X13 $X11 $X12)
% 0.48/0.68  |- ~member skolemFOFtoCNF_U $X14 skolemFOFtoCNF_X4 \/
% 0.48/0.68     black skolemFOFtoCNF_U $X14
% 0.48/0.68  |- ~member skolemFOFtoCNF_U $X14 skolemFOFtoCNF_X4 \/
% 0.48/0.68     cheap skolemFOFtoCNF_U $X14
% 0.48/0.68  |- ~member skolemFOFtoCNF_U $X14 skolemFOFtoCNF_X4 \/
% 0.48/0.68     coat skolemFOFtoCNF_U $X14
% 0.48/0.68  |- ~member skolemFOFtoCNF_U $X7 skolemFOFtoCNF_X3 \/
% 0.48/0.68     be skolemFOFtoCNF_U (skolemFOFtoCNF_X8 $X7) $X7 (skolemFOFtoCNF_X9 $X7)
% 0.48/0.68  |- ~member skolemFOFtoCNF_U $X7 skolemFOFtoCNF_X3 \/
% 0.48/0.68     in skolemFOFtoCNF_U (skolemFOFtoCNF_X9 $X7) skolemFOFtoCNF_X
% 0.48/0.68  |- ~member skolemFOFtoCNF_U $X7 skolemFOFtoCNF_X3 \/
% 0.48/0.68     state skolemFOFtoCNF_U (skolemFOFtoCNF_X8 $X7)
% 0.48/0.68  |- ~definitionFOFtoCNF_0 $X15 $X23 $X30 \/ member $X15 $X30 $X23
% 0.48/0.68  |- ~definitionFOFtoCNF_0 $X15 $X23 $X30 \/ ~fellow $X15 $X30 \/
% 0.48/0.68     ~young $X15 $X30
% 0.48/0.68  |- ~member $X15 $X30 $X23 \/ definitionFOFtoCNF_0 $X15 $X23 $X30 \/
% 0.48/0.68     fellow $X15 $X30
% 0.48/0.68  |- ~member $X15 $X30 $X23 \/ definitionFOFtoCNF_0 $X15 $X23 $X30 \/
% 0.48/0.68     young $X15 $X30
% 0.48/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.48/0.68     ~be $X15 $X25 $X16 $X26 \/ ~behind $X15 $X26 $X19 \/ ~chevy $X15 $X19 \/
% 0.48/0.68     ~city $X15 $X21 \/ ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/
% 0.48/0.68     ~event $X15 $X22 \/ ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/
% 0.48/0.68     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.48/0.68     ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/
% 0.48/0.68     ~jules_forename $X15 $X17 \/ ~lonely $X15 $X21 \/ ~man $X15 $X16 \/
% 0.48/0.68     ~of $X15 $X17 $X16 \/ ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/
% 0.48/0.68     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~state $X15 $X25 \/
% 0.48/0.68     ~street $X15 $X21 \/ ~two $X15 $X23 \/ ~wheel $X15 $X19 \/
% 0.48/0.68     ~white $X15 $X19 \/
% 0.48/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.48/0.68     member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23 \/
% 0.48/0.68     member $X15 (skolemFOFtoCNF_X31 $X15 $X23 $X24) $X24 \/
% 0.48/0.68     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.48/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.48/0.68     ~be $X15 $X25 $X16 $X26 \/ ~behind $X15 $X26 $X19 \/ ~chevy $X15 $X19 \/
% 0.48/0.68     ~city $X15 $X21 \/ ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/
% 0.48/0.68     ~event $X15 $X22 \/ ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/
% 0.48/0.68     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.48/0.68     ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/
% 0.48/0.68     ~jules_forename $X15 $X17 \/ ~lonely $X15 $X21 \/ ~man $X15 $X16 \/
% 0.48/0.68     ~of $X15 $X17 $X16 \/ ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/
% 0.48/0.68     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~state $X15 $X25 \/
% 0.48/0.68     ~street $X15 $X21 \/ ~two $X15 $X23 \/ ~wheel $X15 $X19 \/
% 0.48/0.68     ~white $X15 $X19 \/
% 0.48/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.48/0.68     member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23 \/
% 0.48/0.68     member $X15 (skolemFOFtoCNF_X32 $X15 $X23 $X24) $X23 \/
% 0.48/0.68     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.48/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.48/0.68     ~be $X15 $X25 $X16 $X26 \/
% 0.48/0.68     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.48/0.68     ~behind $X15 $X26 $X19 \/ ~chevy $X15 $X19 \/ ~city $X15 $X21 \/
% 0.48/0.68     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.48/0.68     ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/
% 0.48/0.68     ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/
% 0.48/0.68     ~in $X15 $X22 $X21 \/ ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X17 \/
% 0.48/0.68     ~lonely $X15 $X21 \/ ~man $X15 $X16 \/ ~of $X15 $X17 $X16 \/
% 0.48/0.68     ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ ~placename $X15 $X20 \/
% 0.48/0.68     ~present $X15 $X22 \/ ~state $X15 $X25 \/ ~state $X15 $X28 \/
% 0.48/0.68     ~street $X15 $X21 \/ ~two $X15 $X23 \/ ~wheel $X15 $X19 \/
% 0.48/0.68     ~white $X15 $X19 \/
% 0.48/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.48/0.68     member $X15 (skolemFOFtoCNF_X31 $X15 $X23 $X24) $X24 \/
% 0.48/0.68     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.48/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.48/0.68     ~be $X15 $X25 $X16 $X26 \/
% 0.48/0.68     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.48/0.68     ~behind $X15 $X26 $X19 \/ ~chevy $X15 $X19 \/ ~city $X15 $X21 \/
% 0.48/0.68     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.48/0.68     ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/
% 0.48/0.68     ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/
% 0.48/0.68     ~in $X15 $X22 $X21 \/ ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X17 \/
% 0.48/0.68     ~lonely $X15 $X21 \/ ~man $X15 $X16 \/ ~of $X15 $X17 $X16 \/
% 0.48/0.68     ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ ~placename $X15 $X20 \/
% 0.48/0.68     ~present $X15 $X22 \/ ~state $X15 $X25 \/ ~state $X15 $X28 \/
% 0.48/0.68     ~street $X15 $X21 \/ ~two $X15 $X23 \/ ~wheel $X15 $X19 \/
% 0.48/0.68     ~white $X15 $X19 \/
% 0.48/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.48/0.68     member $X15 (skolemFOFtoCNF_X32 $X15 $X23 $X24) $X23 \/
% 0.48/0.68     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.48/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.48/0.68     ~be $X15 $X25 $X16 $X26 \/ ~behind $X15 $X26 $X19 \/
% 0.48/0.68     ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.48/0.68     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.48/0.68     ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.48/0.68     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.48/0.68     ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/
% 0.48/0.68     ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/
% 0.48/0.68     ~in $X15 $X22 $X21 \/ ~jules_forename $X15 $X17 \/ ~lonely $X15 $X21 \/
% 0.48/0.68     ~man $X15 $X16 \/ ~of $X15 $X17 $X16 \/ ~of $X15 $X20 $X21 \/
% 0.48/0.68     ~old $X15 $X19 \/ ~placename $X15 $X20 \/ ~present $X15 $X22 \/
% 0.48/0.68     ~state $X15 $X25 \/ ~street $X15 $X21 \/ ~two $X15 $X23 \/
% 0.48/0.68     ~wheel $X15 $X19 \/ ~white $X15 $X19 \/
% 0.48/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.48/0.68     member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23 \/
% 0.48/0.68     member $X15 (skolemFOFtoCNF_X31 $X15 $X23 $X24) $X24
% 0.48/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.48/0.68     ~be $X15 $X25 $X16 $X26 \/ ~behind $X15 $X26 $X19 \/
% 0.48/0.68     ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.48/0.68     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.48/0.68     ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.48/0.68     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.48/0.68     ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/
% 0.48/0.68     ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/
% 0.48/0.68     ~in $X15 $X22 $X21 \/ ~jules_forename $X15 $X17 \/ ~lonely $X15 $X21 \/
% 0.48/0.68     ~man $X15 $X16 \/ ~of $X15 $X17 $X16 \/ ~of $X15 $X20 $X21 \/
% 0.48/0.68     ~old $X15 $X19 \/ ~placename $X15 $X20 \/ ~present $X15 $X22 \/
% 0.48/0.68     ~state $X15 $X25 \/ ~street $X15 $X21 \/ ~two $X15 $X23 \/
% 0.48/0.68     ~wheel $X15 $X19 \/ ~white $X15 $X19 \/
% 0.48/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.48/0.68     member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23 \/
% 0.48/0.68     member $X15 (skolemFOFtoCNF_X32 $X15 $X23 $X24) $X23
% 0.48/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.48/0.68     ~be $X15 $X25 $X16 $X26 \/
% 0.48/0.68     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.48/0.68     ~behind $X15 $X26 $X19 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.48/0.68     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.48/0.68     ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.48/0.68     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.48/0.68     ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/
% 0.48/0.68     ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/
% 0.48/0.68     ~in $X15 $X22 $X21 \/ ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X17 \/
% 0.48/0.68     ~lonely $X15 $X21 \/ ~man $X15 $X16 \/ ~of $X15 $X17 $X16 \/
% 0.48/0.68     ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ ~placename $X15 $X20 \/
% 0.48/0.68     ~present $X15 $X22 \/ ~state $X15 $X25 \/ ~state $X15 $X28 \/
% 0.48/0.68     ~street $X15 $X21 \/ ~two $X15 $X23 \/ ~wheel $X15 $X19 \/
% 0.48/0.68     ~white $X15 $X19 \/
% 0.48/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.48/0.68     member $X15 (skolemFOFtoCNF_X31 $X15 $X23 $X24) $X24
% 0.48/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.48/0.68     ~be $X15 $X25 $X16 $X26 \/
% 0.48/0.68     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.48/0.68     ~behind $X15 $X26 $X19 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.48/0.68     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.48/0.68     ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.48/0.68     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.48/0.68     ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/
% 0.48/0.68     ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/
% 0.48/0.68     ~in $X15 $X22 $X21 \/ ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X17 \/
% 0.48/0.68     ~lonely $X15 $X21 \/ ~man $X15 $X16 \/ ~of $X15 $X17 $X16 \/
% 0.48/0.68     ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ ~placename $X15 $X20 \/
% 0.48/0.68     ~present $X15 $X22 \/ ~state $X15 $X25 \/ ~state $X15 $X28 \/
% 0.48/0.68     ~street $X15 $X21 \/ ~two $X15 $X23 \/ ~wheel $X15 $X19 \/
% 0.48/0.68     ~white $X15 $X19 \/
% 0.48/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.48/0.68     member $X15 (skolemFOFtoCNF_X32 $X15 $X23 $X24) $X23
% 0.48/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/
% 0.48/0.68     ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/
% 0.48/0.68     ~barrel $X15 $X22 \/ ~be $X15 $X25 $X16 $X26 \/
% 0.48/0.68     ~behind $X15 $X26 $X19 \/ ~chevy $X15 $X19 \/ ~city $X15 $X21 \/
% 0.48/0.68     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.48/0.68     ~event $X15 $X33 \/ ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/
% 0.48/0.68     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.48/0.68     ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/
% 0.48/0.68     ~jules_forename $X15 $X17 \/ ~lonely $X15 $X21 \/ ~man $X15 $X16 \/
% 0.48/0.68     ~nonreflexive $X15 $X33 \/ ~of $X15 $X17 $X16 \/ ~of $X15 $X20 $X21 \/
% 0.48/0.68     ~old $X15 $X19 \/
% 0.48/0.68     ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/
% 0.48/0.68     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/
% 0.48/0.68     ~state $X15 $X25 \/ ~street $X15 $X21 \/ ~two $X15 $X23 \/
% 0.48/0.68     ~wear $X15 $X33 \/ ~wheel $X15 $X19 \/ ~white $X15 $X19 \/
% 0.48/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.48/0.68     member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23 \/
% 0.48/0.68     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.48/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/
% 0.48/0.68     ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/
% 0.48/0.68     ~barrel $X15 $X22 \/ ~be $X15 $X25 $X16 $X26 \/
% 0.48/0.68     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.48/0.68     ~behind $X15 $X26 $X19 \/ ~chevy $X15 $X19 \/ ~city $X15 $X21 \/
% 0.48/0.68     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.48/0.68     ~event $X15 $X33 \/ ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/
% 0.48/0.68     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.48/0.68     ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/
% 0.48/0.68     ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X17 \/ ~lonely $X15 $X21 \/
% 0.48/0.68     ~man $X15 $X16 \/ ~nonreflexive $X15 $X33 \/ ~of $X15 $X17 $X16 \/
% 0.48/0.68     ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/
% 0.48/0.68     ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/
% 0.48/0.68     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/
% 0.48/0.68     ~state $X15 $X25 \/ ~state $X15 $X28 \/ ~street $X15 $X21 \/
% 0.48/0.68     ~two $X15 $X23 \/ ~wear $X15 $X33 \/ ~wheel $X15 $X19 \/
% 0.48/0.68     ~white $X15 $X19 \/
% 0.48/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.48/0.68     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.48/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/
% 0.48/0.68     ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/
% 0.48/0.68     ~barrel $X15 $X22 \/ ~be $X15 $X25 $X16 $X26 \/
% 0.48/0.68     ~behind $X15 $X26 $X19 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.48/0.68     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.48/0.68     ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.48/0.68     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.48/0.68     ~event $X15 $X33 \/ ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/
% 0.48/0.68     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.48/0.68     ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/
% 0.48/0.68     ~jules_forename $X15 $X17 \/ ~lonely $X15 $X21 \/ ~man $X15 $X16 \/
% 0.48/0.68     ~nonreflexive $X15 $X33 \/ ~of $X15 $X17 $X16 \/ ~of $X15 $X20 $X21 \/
% 0.48/0.68     ~old $X15 $X19 \/
% 0.48/0.68     ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/
% 0.48/0.68     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/
% 0.48/0.68     ~state $X15 $X25 \/ ~street $X15 $X21 \/ ~two $X15 $X23 \/
% 0.48/0.68     ~wear $X15 $X33 \/ ~wheel $X15 $X19 \/ ~white $X15 $X19 \/
% 0.48/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.48/0.68     member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23
% 0.48/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/
% 0.48/0.68     ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/
% 0.48/0.68     ~barrel $X15 $X22 \/ ~be $X15 $X25 $X16 $X26 \/
% 0.48/0.68     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.48/0.68     ~behind $X15 $X26 $X19 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.48/0.68     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.48/0.68     ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.48/0.68     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.48/0.68     ~event $X15 $X33 \/ ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/
% 0.48/0.68     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.48/0.68     ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/
% 0.48/0.68     ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X17 \/ ~lonely $X15 $X21 \/
% 0.48/0.68     ~man $X15 $X16 \/ ~nonreflexive $X15 $X33 \/ ~of $X15 $X17 $X16 \/
% 0.48/0.68     ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/
% 0.48/0.68     ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/
% 0.48/0.68     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/
% 0.48/0.68     ~state $X15 $X25 \/ ~state $X15 $X28 \/ ~street $X15 $X21 \/
% 0.48/0.68     ~two $X15 $X23 \/ ~wear $X15 $X33 \/ ~wheel $X15 $X19 \/
% 0.48/0.68     ~white $X15 $X19 \/
% 0.48/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23)
% 0.48/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.48/0.68     ~be $X15 $X25 $X21 $X26 \/ ~behind $X15 $X26 $X19 \/ ~chevy $X15 $X19 \/
% 0.48/0.68     ~city $X15 $X21 \/ ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/
% 0.48/0.68     ~event $X15 $X22 \/ ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/
% 0.48/0.68     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.48/0.68     ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/
% 0.48/0.68     ~jules_forename $X15 $X20 \/ ~lonely $X15 $X21 \/ ~man $X15 $X21 \/
% 0.48/0.68     ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ ~placename $X15 $X20 \/
% 0.48/0.68     ~present $X15 $X22 \/ ~state $X15 $X25 \/ ~street $X15 $X21 \/
% 0.48/0.68     ~two $X15 $X23 \/ ~wheel $X15 $X19 \/ ~white $X15 $X19 \/
% 0.48/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.48/0.68     member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23 \/
% 0.48/0.68     member $X15 (skolemFOFtoCNF_X31 $X15 $X23 $X24) $X24 \/
% 0.48/0.68     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.48/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.48/0.68     ~be $X15 $X25 $X21 $X26 \/ ~behind $X15 $X26 $X19 \/ ~chevy $X15 $X19 \/
% 0.48/0.68     ~city $X15 $X21 \/ ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/
% 0.48/0.68     ~event $X15 $X22 \/ ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/
% 0.48/0.68     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.48/0.68     ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/
% 0.48/0.68     ~jules_forename $X15 $X20 \/ ~lonely $X15 $X21 \/ ~man $X15 $X21 \/
% 0.48/0.68     ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ ~placename $X15 $X20 \/
% 0.48/0.68     ~present $X15 $X22 \/ ~state $X15 $X25 \/ ~street $X15 $X21 \/
% 0.48/0.68     ~two $X15 $X23 \/ ~wheel $X15 $X19 \/ ~white $X15 $X19 \/
% 0.48/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.48/0.68     member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23 \/
% 0.48/0.68     member $X15 (skolemFOFtoCNF_X32 $X15 $X23 $X24) $X23 \/
% 0.48/0.68     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.48/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.48/0.68     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.48/0.68     ~behind $X15 $X29 $X19 \/ ~chevy $X15 $X19 \/ ~city $X15 $X21 \/
% 0.48/0.68     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.48/0.68     ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/
% 0.48/0.68     ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/
% 0.48/0.68     ~in $X15 $X22 $X21 \/ ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X17 \/
% 0.48/0.68     ~lonely $X15 $X21 \/ ~man $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.68     ~of $X15 $X17 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.68     ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ ~placename $X15 $X20 \/
% 0.48/0.68     ~present $X15 $X22 \/ ~state $X15 $X28 \/ ~street $X15 $X21 \/
% 0.48/0.68     ~two $X15 $X23 \/ ~wheel $X15 $X19 \/ ~white $X15 $X19 \/
% 0.48/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.48/0.68     member $X15 (skolemFOFtoCNF_X31 $X15 $X23 $X24) $X24 \/
% 0.48/0.68     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.48/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.48/0.68     ~be $X15 $X25 $X21 $X26 \/
% 0.48/0.68     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.48/0.68     ~behind $X15 $X26 $X19 \/ ~chevy $X15 $X19 \/ ~city $X15 $X21 \/
% 0.48/0.68     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.48/0.68     ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/
% 0.48/0.68     ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/
% 0.48/0.68     ~in $X15 $X22 $X21 \/ ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X20 \/
% 0.48/0.68     ~lonely $X15 $X21 \/ ~man $X15 $X21 \/ ~of $X15 $X20 $X21 \/
% 0.48/0.68     ~old $X15 $X19 \/ ~placename $X15 $X20 \/ ~present $X15 $X22 \/
% 0.48/0.68     ~state $X15 $X25 \/ ~state $X15 $X28 \/ ~street $X15 $X21 \/
% 0.48/0.68     ~two $X15 $X23 \/ ~wheel $X15 $X19 \/ ~white $X15 $X19 \/
% 0.48/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.48/0.68     member $X15 (skolemFOFtoCNF_X31 $X15 $X23 $X24) $X24 \/
% 0.48/0.68     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.48/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.48/0.68     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.48/0.68     ~behind $X15 $X29 $X19 \/ ~chevy $X15 $X19 \/
% 0.48/0.68     ~city $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~dirty $X15 $X19 \/
% 0.48/0.68     ~down $X15 $X22 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.68     ~event $X15 $X22 \/ ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/
% 0.48/0.68     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.48/0.68     ~hollywood_placename $X15 $X20 \/
% 0.48/0.68     ~in $X15 $X22 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.68     ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X20 \/
% 0.48/0.68     ~lonely $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.68     ~man $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.68     ~of $X15 $X20 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~old $X15 $X19 \/
% 0.48/0.68     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~state $X15 $X28 \/
% 0.48/0.68     ~street $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~two $X15 $X23 \/
% 0.48/0.68     ~wheel $X15 $X19 \/ ~white $X15 $X19 \/
% 0.48/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.48/0.68     member $X15 (skolemFOFtoCNF_X31 $X15 $X23 $X24) $X24 \/
% 0.48/0.68     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.48/0.68  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.48/0.68     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.48/0.68     ~behind $X15 $X29 $X19 \/ ~chevy $X15 $X19 \/ ~city $X15 $X21 \/
% 0.48/0.68     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.48/0.68     ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/
% 0.48/0.68     ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/
% 0.48/0.68     ~in $X15 $X22 $X21 \/ ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X17 \/
% 0.48/0.68     ~lonely $X15 $X21 \/ ~man $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.68     ~of $X15 $X17 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.68     ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ ~placename $X15 $X20 \/
% 0.48/0.68     ~present $X15 $X22 \/ ~state $X15 $X28 \/ ~street $X15 $X21 \/
% 0.48/0.68     ~two $X15 $X23 \/ ~wheel $X15 $X19 \/ ~white $X15 $X19 \/
% 0.48/0.68     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.48/0.68     member $X15 (skolemFOFtoCNF_X32 $X15 $X23 $X24) $X23 \/
% 0.48/0.68     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.48/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.48/0.69     ~be $X15 $X25 $X21 $X26 \/
% 0.48/0.69     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.48/0.69     ~behind $X15 $X26 $X19 \/ ~chevy $X15 $X19 \/ ~city $X15 $X21 \/
% 0.48/0.69     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.48/0.69     ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/
% 0.48/0.69     ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/
% 0.48/0.69     ~in $X15 $X22 $X21 \/ ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X20 \/
% 0.48/0.69     ~lonely $X15 $X21 \/ ~man $X15 $X21 \/ ~of $X15 $X20 $X21 \/
% 0.48/0.69     ~old $X15 $X19 \/ ~placename $X15 $X20 \/ ~present $X15 $X22 \/
% 0.48/0.69     ~state $X15 $X25 \/ ~state $X15 $X28 \/ ~street $X15 $X21 \/
% 0.48/0.69     ~two $X15 $X23 \/ ~wheel $X15 $X19 \/ ~white $X15 $X19 \/
% 0.48/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.48/0.69     member $X15 (skolemFOFtoCNF_X32 $X15 $X23 $X24) $X23 \/
% 0.48/0.69     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.48/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.48/0.69     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.48/0.69     ~behind $X15 $X29 $X19 \/ ~chevy $X15 $X19 \/
% 0.48/0.69     ~city $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~dirty $X15 $X19 \/
% 0.48/0.69     ~down $X15 $X22 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.69     ~event $X15 $X22 \/ ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/
% 0.48/0.69     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.48/0.69     ~hollywood_placename $X15 $X20 \/
% 0.48/0.69     ~in $X15 $X22 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.69     ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X20 \/
% 0.48/0.69     ~lonely $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.69     ~man $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.69     ~of $X15 $X20 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~old $X15 $X19 \/
% 0.48/0.69     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~state $X15 $X28 \/
% 0.48/0.69     ~street $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~two $X15 $X23 \/
% 0.48/0.69     ~wheel $X15 $X19 \/ ~white $X15 $X19 \/
% 0.48/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.48/0.69     member $X15 (skolemFOFtoCNF_X32 $X15 $X23 $X24) $X23 \/
% 0.48/0.69     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.48/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.48/0.69     ~be $X15 $X25 $X21 $X26 \/ ~behind $X15 $X26 $X19 \/
% 0.48/0.69     ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.48/0.69     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.48/0.69     ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.48/0.69     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.48/0.69     ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/
% 0.48/0.69     ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/
% 0.48/0.69     ~in $X15 $X22 $X21 \/ ~jules_forename $X15 $X20 \/ ~lonely $X15 $X21 \/
% 0.48/0.69     ~man $X15 $X21 \/ ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/
% 0.48/0.69     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~state $X15 $X25 \/
% 0.48/0.69     ~street $X15 $X21 \/ ~two $X15 $X23 \/ ~wheel $X15 $X19 \/
% 0.48/0.69     ~white $X15 $X19 \/
% 0.48/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.48/0.69     member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23 \/
% 0.48/0.69     member $X15 (skolemFOFtoCNF_X31 $X15 $X23 $X24) $X24
% 0.48/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.48/0.69     ~be $X15 $X25 $X21 $X26 \/ ~behind $X15 $X26 $X19 \/
% 0.48/0.69     ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.48/0.69     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.48/0.69     ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.48/0.69     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.48/0.69     ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/
% 0.48/0.69     ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/
% 0.48/0.69     ~in $X15 $X22 $X21 \/ ~jules_forename $X15 $X20 \/ ~lonely $X15 $X21 \/
% 0.48/0.69     ~man $X15 $X21 \/ ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/
% 0.48/0.69     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~state $X15 $X25 \/
% 0.48/0.69     ~street $X15 $X21 \/ ~two $X15 $X23 \/ ~wheel $X15 $X19 \/
% 0.48/0.69     ~white $X15 $X19 \/
% 0.48/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.48/0.69     member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23 \/
% 0.48/0.69     member $X15 (skolemFOFtoCNF_X32 $X15 $X23 $X24) $X23
% 0.48/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.48/0.69     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.48/0.69     ~behind $X15 $X29 $X19 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.48/0.69     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.48/0.69     ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.48/0.69     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.48/0.69     ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/
% 0.48/0.69     ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/
% 0.48/0.69     ~in $X15 $X22 $X21 \/ ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X17 \/
% 0.48/0.69     ~lonely $X15 $X21 \/ ~man $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.69     ~of $X15 $X17 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.69     ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ ~placename $X15 $X20 \/
% 0.48/0.69     ~present $X15 $X22 \/ ~state $X15 $X28 \/ ~street $X15 $X21 \/
% 0.48/0.69     ~two $X15 $X23 \/ ~wheel $X15 $X19 \/ ~white $X15 $X19 \/
% 0.48/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.48/0.69     member $X15 (skolemFOFtoCNF_X31 $X15 $X23 $X24) $X24
% 0.48/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.48/0.69     ~be $X15 $X25 $X21 $X26 \/
% 0.48/0.69     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.48/0.69     ~behind $X15 $X26 $X19 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.48/0.69     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.48/0.69     ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.48/0.69     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.48/0.69     ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/
% 0.48/0.69     ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/
% 0.48/0.69     ~in $X15 $X22 $X21 \/ ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X20 \/
% 0.48/0.69     ~lonely $X15 $X21 \/ ~man $X15 $X21 \/ ~of $X15 $X20 $X21 \/
% 0.48/0.69     ~old $X15 $X19 \/ ~placename $X15 $X20 \/ ~present $X15 $X22 \/
% 0.48/0.69     ~state $X15 $X25 \/ ~state $X15 $X28 \/ ~street $X15 $X21 \/
% 0.48/0.69     ~two $X15 $X23 \/ ~wheel $X15 $X19 \/ ~white $X15 $X19 \/
% 0.48/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.48/0.69     member $X15 (skolemFOFtoCNF_X31 $X15 $X23 $X24) $X24
% 0.48/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.48/0.69     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.48/0.69     ~behind $X15 $X29 $X19 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.48/0.69     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.48/0.69     ~city $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.69     ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~dirty $X15 $X19 \/
% 0.48/0.69     ~down $X15 $X22 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.69     ~event $X15 $X22 \/ ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/
% 0.48/0.69     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.48/0.69     ~hollywood_placename $X15 $X20 \/
% 0.48/0.69     ~in $X15 $X22 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.69     ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X20 \/
% 0.48/0.69     ~lonely $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.69     ~man $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.69     ~of $X15 $X20 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~old $X15 $X19 \/
% 0.48/0.69     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~state $X15 $X28 \/
% 0.48/0.69     ~street $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~two $X15 $X23 \/
% 0.48/0.69     ~wheel $X15 $X19 \/ ~white $X15 $X19 \/
% 0.48/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.48/0.69     member $X15 (skolemFOFtoCNF_X31 $X15 $X23 $X24) $X24
% 0.48/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.48/0.69     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.48/0.69     ~behind $X15 $X29 $X19 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.48/0.69     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.48/0.69     ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.48/0.69     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.48/0.69     ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/
% 0.48/0.69     ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/
% 0.48/0.69     ~in $X15 $X22 $X21 \/ ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X17 \/
% 0.48/0.69     ~lonely $X15 $X21 \/ ~man $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.69     ~of $X15 $X17 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.69     ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ ~placename $X15 $X20 \/
% 0.48/0.69     ~present $X15 $X22 \/ ~state $X15 $X28 \/ ~street $X15 $X21 \/
% 0.48/0.69     ~two $X15 $X23 \/ ~wheel $X15 $X19 \/ ~white $X15 $X19 \/
% 0.48/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.48/0.69     member $X15 (skolemFOFtoCNF_X32 $X15 $X23 $X24) $X23
% 0.48/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.48/0.69     ~be $X15 $X25 $X21 $X26 \/
% 0.48/0.69     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.48/0.69     ~behind $X15 $X26 $X19 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.48/0.69     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.48/0.69     ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.48/0.69     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.48/0.69     ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/
% 0.48/0.69     ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/
% 0.48/0.69     ~in $X15 $X22 $X21 \/ ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X20 \/
% 0.48/0.69     ~lonely $X15 $X21 \/ ~man $X15 $X21 \/ ~of $X15 $X20 $X21 \/
% 0.48/0.69     ~old $X15 $X19 \/ ~placename $X15 $X20 \/ ~present $X15 $X22 \/
% 0.48/0.69     ~state $X15 $X25 \/ ~state $X15 $X28 \/ ~street $X15 $X21 \/
% 0.48/0.69     ~two $X15 $X23 \/ ~wheel $X15 $X19 \/ ~white $X15 $X19 \/
% 0.48/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.48/0.69     member $X15 (skolemFOFtoCNF_X32 $X15 $X23 $X24) $X23
% 0.48/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/
% 0.48/0.69     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.48/0.69     ~behind $X15 $X29 $X19 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.48/0.69     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.48/0.69     ~city $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.69     ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~dirty $X15 $X19 \/
% 0.48/0.69     ~down $X15 $X22 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.69     ~event $X15 $X22 \/ ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/
% 0.48/0.69     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.48/0.69     ~hollywood_placename $X15 $X20 \/
% 0.48/0.69     ~in $X15 $X22 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.69     ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X20 \/
% 0.48/0.69     ~lonely $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.69     ~man $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.69     ~of $X15 $X20 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~old $X15 $X19 \/
% 0.48/0.69     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~state $X15 $X28 \/
% 0.48/0.69     ~street $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~two $X15 $X23 \/
% 0.48/0.69     ~wheel $X15 $X19 \/ ~white $X15 $X19 \/
% 0.48/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.48/0.69     member $X15 (skolemFOFtoCNF_X32 $X15 $X23 $X24) $X23
% 0.48/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/
% 0.48/0.69     ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/
% 0.48/0.69     ~barrel $X15 $X22 \/ ~be $X15 $X25 $X21 $X26 \/
% 0.48/0.69     ~behind $X15 $X26 $X19 \/ ~chevy $X15 $X19 \/ ~city $X15 $X21 \/
% 0.48/0.69     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.48/0.69     ~event $X15 $X33 \/ ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/
% 0.48/0.69     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.48/0.69     ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/
% 0.48/0.69     ~jules_forename $X15 $X20 \/ ~lonely $X15 $X21 \/ ~man $X15 $X21 \/
% 0.48/0.69     ~nonreflexive $X15 $X33 \/ ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/
% 0.48/0.69     ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/
% 0.48/0.69     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/
% 0.48/0.69     ~state $X15 $X25 \/ ~street $X15 $X21 \/ ~two $X15 $X23 \/
% 0.48/0.69     ~wear $X15 $X33 \/ ~wheel $X15 $X19 \/ ~white $X15 $X19 \/
% 0.48/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.48/0.69     member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23 \/
% 0.48/0.69     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.48/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/
% 0.48/0.69     ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/
% 0.48/0.69     ~barrel $X15 $X22 \/
% 0.48/0.69     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.48/0.69     ~behind $X15 $X29 $X19 \/ ~chevy $X15 $X19 \/ ~city $X15 $X21 \/
% 0.48/0.69     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.48/0.69     ~event $X15 $X33 \/ ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/
% 0.48/0.69     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.48/0.69     ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/
% 0.48/0.69     ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X17 \/ ~lonely $X15 $X21 \/
% 0.48/0.69     ~man $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.69     ~nonreflexive $X15 $X33 \/
% 0.48/0.69     ~of $X15 $X17 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.69     ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/
% 0.48/0.69     ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/
% 0.48/0.69     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/
% 0.48/0.69     ~state $X15 $X28 \/ ~street $X15 $X21 \/ ~two $X15 $X23 \/
% 0.48/0.69     ~wear $X15 $X33 \/ ~wheel $X15 $X19 \/ ~white $X15 $X19 \/
% 0.48/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.48/0.69     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.48/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/
% 0.48/0.69     ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/
% 0.48/0.69     ~barrel $X15 $X22 \/ ~be $X15 $X25 $X21 $X26 \/
% 0.48/0.69     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.48/0.69     ~behind $X15 $X26 $X19 \/ ~chevy $X15 $X19 \/ ~city $X15 $X21 \/
% 0.48/0.69     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.48/0.69     ~event $X15 $X33 \/ ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/
% 0.48/0.69     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.48/0.69     ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/
% 0.48/0.69     ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X20 \/ ~lonely $X15 $X21 \/
% 0.48/0.69     ~man $X15 $X21 \/ ~nonreflexive $X15 $X33 \/ ~of $X15 $X20 $X21 \/
% 0.48/0.69     ~old $X15 $X19 \/
% 0.48/0.69     ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/
% 0.48/0.69     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/
% 0.48/0.69     ~state $X15 $X25 \/ ~state $X15 $X28 \/ ~street $X15 $X21 \/
% 0.48/0.69     ~two $X15 $X23 \/ ~wear $X15 $X33 \/ ~wheel $X15 $X19 \/
% 0.48/0.69     ~white $X15 $X19 \/
% 0.48/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.48/0.69     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.48/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/
% 0.48/0.69     ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/
% 0.48/0.69     ~barrel $X15 $X22 \/
% 0.48/0.69     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.48/0.69     ~behind $X15 $X29 $X19 \/ ~chevy $X15 $X19 \/
% 0.48/0.69     ~city $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~dirty $X15 $X19 \/
% 0.48/0.69     ~down $X15 $X22 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.69     ~event $X15 $X22 \/ ~event $X15 $X33 \/ ~forename $X15 $X20 \/
% 0.48/0.69     ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.48/0.69     ~hollywood_placename $X15 $X20 \/
% 0.48/0.69     ~in $X15 $X22 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.69     ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X20 \/
% 0.48/0.69     ~lonely $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.69     ~man $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.69     ~nonreflexive $X15 $X33 \/
% 0.48/0.69     ~of $X15 $X20 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~old $X15 $X19 \/
% 0.48/0.69     ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/
% 0.48/0.69     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/
% 0.48/0.69     ~state $X15 $X28 \/ ~street $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.69     ~two $X15 $X23 \/ ~wear $X15 $X33 \/ ~wheel $X15 $X19 \/
% 0.48/0.69     ~white $X15 $X19 \/
% 0.48/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.48/0.69     member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24
% 0.48/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/
% 0.48/0.69     ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/
% 0.48/0.69     ~barrel $X15 $X22 \/ ~be $X15 $X25 $X21 $X26 \/
% 0.48/0.69     ~behind $X15 $X26 $X19 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.48/0.69     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.48/0.69     ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.48/0.69     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.48/0.69     ~event $X15 $X33 \/ ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/
% 0.48/0.69     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.48/0.69     ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/
% 0.48/0.69     ~jules_forename $X15 $X20 \/ ~lonely $X15 $X21 \/ ~man $X15 $X21 \/
% 0.48/0.69     ~nonreflexive $X15 $X33 \/ ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/
% 0.48/0.69     ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/
% 0.48/0.69     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/
% 0.48/0.69     ~state $X15 $X25 \/ ~street $X15 $X21 \/ ~two $X15 $X23 \/
% 0.48/0.69     ~wear $X15 $X33 \/ ~wheel $X15 $X19 \/ ~white $X15 $X19 \/
% 0.48/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/
% 0.48/0.69     member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23
% 0.48/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/
% 0.48/0.69     ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/
% 0.48/0.69     ~barrel $X15 $X22 \/
% 0.48/0.69     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.48/0.69     ~behind $X15 $X29 $X19 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.48/0.69     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.48/0.69     ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.48/0.69     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.48/0.69     ~event $X15 $X33 \/ ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/
% 0.48/0.69     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.48/0.69     ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/
% 0.48/0.69     ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X17 \/ ~lonely $X15 $X21 \/
% 0.48/0.69     ~man $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.69     ~nonreflexive $X15 $X33 \/
% 0.48/0.69     ~of $X15 $X17 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.69     ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/
% 0.48/0.69     ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/
% 0.48/0.69     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/
% 0.48/0.69     ~state $X15 $X28 \/ ~street $X15 $X21 \/ ~two $X15 $X23 \/
% 0.48/0.69     ~wear $X15 $X33 \/ ~wheel $X15 $X19 \/ ~white $X15 $X19 \/
% 0.48/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23)
% 0.48/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/
% 0.48/0.69     ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/
% 0.48/0.69     ~barrel $X15 $X22 \/ ~be $X15 $X25 $X21 $X26 \/
% 0.48/0.69     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.48/0.69     ~behind $X15 $X26 $X19 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.48/0.69     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.48/0.69     ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.48/0.69     ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/
% 0.48/0.69     ~event $X15 $X33 \/ ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/
% 0.48/0.69     ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.48/0.69     ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/
% 0.48/0.69     ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X20 \/ ~lonely $X15 $X21 \/
% 0.48/0.69     ~man $X15 $X21 \/ ~nonreflexive $X15 $X33 \/ ~of $X15 $X20 $X21 \/
% 0.48/0.69     ~old $X15 $X19 \/
% 0.48/0.69     ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/
% 0.48/0.69     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/
% 0.48/0.69     ~state $X15 $X25 \/ ~state $X15 $X28 \/ ~street $X15 $X21 \/
% 0.48/0.69     ~two $X15 $X23 \/ ~wear $X15 $X33 \/ ~wheel $X15 $X19 \/
% 0.48/0.69     ~white $X15 $X19 \/
% 0.48/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23)
% 0.48/0.69  |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/
% 0.48/0.69     ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/
% 0.48/0.69     ~barrel $X15 $X22 \/
% 0.48/0.69     ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/
% 0.48/0.69     ~behind $X15 $X29 $X19 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/
% 0.48/0.69     ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/
% 0.48/0.69     ~city $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.69     ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~dirty $X15 $X19 \/
% 0.48/0.69     ~down $X15 $X22 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.69     ~event $X15 $X22 \/ ~event $X15 $X33 \/ ~forename $X15 $X20 \/
% 0.48/0.69     ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/ ~group $X15 $X24 \/
% 0.48/0.69     ~hollywood_placename $X15 $X20 \/
% 0.48/0.69     ~in $X15 $X22 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.69     ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X20 \/
% 0.48/0.69     ~lonely $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.69     ~man $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.69     ~nonreflexive $X15 $X33 \/
% 0.48/0.69     ~of $X15 $X20 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~old $X15 $X19 \/
% 0.48/0.69     ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/
% 0.48/0.69     ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/
% 0.48/0.69     ~state $X15 $X28 \/ ~street $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/
% 0.48/0.69     ~two $X15 $X23 \/ ~wear $X15 $X33 \/ ~wheel $X15 $X19 \/
% 0.48/0.69     ~white $X15 $X19 \/
% 0.48/0.69     definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23)
% 0.48/0.69  |- ~agent skolemFOFtoCNF_U $_45 $_43 \/ ~barrel skolemFOFtoCNF_U $_45 \/
% 0.48/0.69     ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_43 \/
% 0.48/0.69     ~chevy skolemFOFtoCNF_U $_43 \/
% 0.48/0.69     ~city skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.48/0.69     ~dirty skolemFOFtoCNF_U $_43 \/
% 0.48/0.69     ~down skolemFOFtoCNF_U $_45 skolemFOFtoCNF_V \/
% 0.48/0.69     ~event skolemFOFtoCNF_U $_45 \/ ~frontseat skolemFOFtoCNF_U $_42 \/
% 0.48/0.69     ~group skolemFOFtoCNF_U $_46 \/ ~group skolemFOFtoCNF_U $_47 \/
% 0.48/0.69     ~hollywood_placename skolemFOFtoCNF_U skolemFOFtoCNF_W \/
% 0.48/0.69     ~in skolemFOFtoCNF_U $_45 skolemFOFtoCNF_V \/
% 0.48/0.69     ~lonely skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.48/0.69     ~old skolemFOFtoCNF_U $_43 \/
% 0.48/0.69     ~placename skolemFOFtoCNF_U skolemFOFtoCNF_W \/
% 0.48/0.69     ~present skolemFOFtoCNF_U $_45 \/
% 0.48/0.69     ~street skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.48/0.69     ~two skolemFOFtoCNF_U $_46 \/ ~wheel skolemFOFtoCNF_U $_43 \/
% 0.48/0.69     ~white skolemFOFtoCNF_U $_43 \/
% 0.48/0.69     definitionFOFtoCNF_0 skolemFOFtoCNF_U $_46
% 0.48/0.69       (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_46) \/
% 0.48/0.69     member skolemFOFtoCNF_U (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_42 $_46)
% 0.48/0.69       $_46 \/
% 0.48/0.69     member skolemFOFtoCNF_U (skolemFOFtoCNF_X32 skolemFOFtoCNF_U $_46 $_47)
% 0.48/0.69       $_46 \/
% 0.48/0.69     member skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_47) $_47
% 0.48/0.69  |- ~agent skolemFOFtoCNF_U $_66 $_64 \/ ~barrel skolemFOFtoCNF_U $_66 \/
% 0.48/0.69     ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_64 \/
% 0.48/0.69     ~chevy skolemFOFtoCNF_U $_64 \/
% 0.48/0.69     ~city skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.48/0.69     ~dirty skolemFOFtoCNF_U $_64 \/
% 0.48/0.69     ~down skolemFOFtoCNF_U $_66 skolemFOFtoCNF_V \/
% 0.48/0.69     ~event skolemFOFtoCNF_U $_66 \/ ~frontseat skolemFOFtoCNF_U $_63 \/
% 0.48/0.69     ~group skolemFOFtoCNF_U $_67 \/ ~group skolemFOFtoCNF_U $_68 \/
% 0.48/0.69     ~hollywood_placename skolemFOFtoCNF_U skolemFOFtoCNF_W \/
% 0.48/0.69     ~in skolemFOFtoCNF_U $_66 skolemFOFtoCNF_V \/
% 0.48/0.69     ~lonely skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.48/0.69     ~old skolemFOFtoCNF_U $_64 \/
% 0.48/0.69     ~placename skolemFOFtoCNF_U skolemFOFtoCNF_W \/
% 0.48/0.69     ~present skolemFOFtoCNF_U $_66 \/
% 0.48/0.69     ~street skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.48/0.69     ~two skolemFOFtoCNF_U $_67 \/ ~wheel skolemFOFtoCNF_U $_64 \/
% 0.48/0.69     ~white skolemFOFtoCNF_U $_64 \/
% 0.48/0.69     definitionFOFtoCNF_0 skolemFOFtoCNF_U $_67
% 0.48/0.69       (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_67) \/
% 0.48/0.69     member skolemFOFtoCNF_U (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_63 $_67)
% 0.48/0.69       $_67 \/
% 0.48/0.69     member skolemFOFtoCNF_U (skolemFOFtoCNF_X31 skolemFOFtoCNF_U $_67 $_68)
% 0.48/0.69       $_68 \/
% 0.48/0.69     member skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_68) $_68
% 0.48/0.69  |- ~agent skolemFOFtoCNF_U $_97 $_94 \/ ~barrel skolemFOFtoCNF_U $_97 \/
% 0.48/0.69     ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_94 \/
% 0.48/0.69     ~black skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_99) \/
% 0.48/0.69     ~cheap skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_99) \/
% 0.48/0.69     ~chevy skolemFOFtoCNF_U $_94 \/
% 0.48/0.69     ~city skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.48/0.69     ~coat skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_99) \/
% 0.48/0.69     ~dirty skolemFOFtoCNF_U $_94 \/
% 0.48/0.69     ~down skolemFOFtoCNF_U $_97 skolemFOFtoCNF_V \/
% 0.48/0.69     ~event skolemFOFtoCNF_U $_97 \/ ~forename skolemFOFtoCNF_U $_95 \/
% 0.48/0.69     ~frontseat skolemFOFtoCNF_U $_93 \/ ~group skolemFOFtoCNF_U $_98 \/
% 0.48/0.69     ~group skolemFOFtoCNF_U $_99 \/
% 0.48/0.69     ~hollywood_placename skolemFOFtoCNF_U $_95 \/
% 0.48/0.69     ~in skolemFOFtoCNF_U $_97 skolemFOFtoCNF_V \/
% 0.48/0.69     ~jules_forename skolemFOFtoCNF_U $_95 \/
% 0.48/0.69     ~lonely skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.48/0.69     ~of skolemFOFtoCNF_U $_95 skolemFOFtoCNF_V \/
% 0.48/0.69     ~old skolemFOFtoCNF_U $_94 \/ ~placename skolemFOFtoCNF_U $_95 \/
% 0.48/0.69     ~present skolemFOFtoCNF_U $_97 \/
% 0.48/0.69     ~street skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.48/0.69     ~two skolemFOFtoCNF_U $_98 \/ ~wheel skolemFOFtoCNF_U $_94 \/
% 0.48/0.69     ~white skolemFOFtoCNF_U $_94 \/
% 0.48/0.69     definitionFOFtoCNF_0 skolemFOFtoCNF_U $_98
% 0.48/0.69       (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_98) \/
% 0.48/0.69     member skolemFOFtoCNF_U (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_93 $_98)
% 0.48/0.69       $_98 \/
% 0.48/0.69     member skolemFOFtoCNF_U (skolemFOFtoCNF_X32 skolemFOFtoCNF_U $_98 $_99)
% 0.48/0.69       $_98
% 0.48/0.69  |- ~agent skolemFOFtoCNF_U $_113 $_110 \/ ~barrel skolemFOFtoCNF_U $_113 \/
% 0.48/0.69     ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_110 \/
% 0.48/0.69     ~black skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_115) \/
% 0.48/0.69     ~cheap skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_115) \/
% 0.48/0.69     ~chevy skolemFOFtoCNF_U $_110 \/
% 0.48/0.69     ~city skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.48/0.69     ~coat skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_115) \/
% 0.48/0.69     ~dirty skolemFOFtoCNF_U $_110 \/
% 0.48/0.69     ~down skolemFOFtoCNF_U $_113 skolemFOFtoCNF_V \/
% 0.48/0.69     ~event skolemFOFtoCNF_U $_113 \/ ~forename skolemFOFtoCNF_U $_111 \/
% 0.48/0.69     ~frontseat skolemFOFtoCNF_U $_109 \/ ~group skolemFOFtoCNF_U $_114 \/
% 0.48/0.69     ~group skolemFOFtoCNF_U $_115 \/
% 0.48/0.69     ~hollywood_placename skolemFOFtoCNF_U $_111 \/
% 0.48/0.69     ~in skolemFOFtoCNF_U $_113 skolemFOFtoCNF_V \/
% 0.48/0.69     ~jules_forename skolemFOFtoCNF_U $_111 \/
% 0.48/0.69     ~lonely skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.48/0.69     ~of skolemFOFtoCNF_U $_111 skolemFOFtoCNF_V \/
% 0.48/0.69     ~old skolemFOFtoCNF_U $_110 \/ ~placename skolemFOFtoCNF_U $_111 \/
% 0.48/0.69     ~present skolemFOFtoCNF_U $_113 \/
% 0.48/0.69     ~street skolemFOFtoCNF_U skolemFOFtoCNF_V \/
% 0.48/0.69     ~two skolemFOFtoCNF_U $_114 \/ ~wheel skolemFOFtoCNF_U $_110 \/
% 0.48/0.69     ~white skolemFOFtoCNF_U $_110 \/
% 0.48/0.69     definitionFOFtoCNF_0 skolemFOFtoCNF_U $_114
% 0.48/0.69       (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_114) \/
% 0.48/0.69     member skolemFOFtoCNF_U
% 0.48/0.69       (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_109 $_114) $_114 \/
% 0.48/0.69     member skolemFOFtoCNF_U
% 0.48/0.69       (skolemFOFtoCNF_X31 skolemFOFtoCNF_U $_114 $_115) $_115
% 0.48/0.69  |- ~agent skolemFOFtoCNF_U $_181 $_178 \/ ~barrel skolemFOFtoCNF_U $_181 \/
% 0.48/0.69     ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_178 \/
% 0.48/0.69     ~chevy skolemFOFtoCNF_U $_178 \/ ~city skolemFOFtoCNF_U $_180 \/
% 0.48/0.69     ~dirty skolemFOFtoCNF_U $_178 \/ ~down skolemFOFtoCNF_U $_181 $_180 \/
% 0.48/0.69     ~event skolemFOFtoCNF_U $_181 \/ ~frontseat skolemFOFtoCNF_U $_177 \/
% 0.48/0.69     ~group skolemFOFtoCNF_U $_182 \/ ~group skolemFOFtoCNF_U $_183 \/
% 0.48/0.69     ~hollywood_placename skolemFOFtoCNF_U $_179 \/
% 0.48/0.69     ~in skolemFOFtoCNF_U $_181 $_180 \/ ~lonely skolemFOFtoCNF_U $_180 \/
% 0.48/0.69     ~of skolemFOFtoCNF_U $_179 $_180 \/ ~old skolemFOFtoCNF_U $_178 \/
% 0.48/0.69     ~placename skolemFOFtoCNF_U $_179 \/ ~present skolemFOFtoCNF_U $_181 \/
% 0.48/0.69     ~street skolemFOFtoCNF_U $_180 \/ ~two skolemFOFtoCNF_U $_182 \/
% 0.48/0.69     ~wheel skolemFOFtoCNF_U $_178 \/ ~white skolemFOFtoCNF_U $_178 \/
% 0.48/0.69     definitionFOFtoCNF_0 skolemFOFtoCNF_U $_182
% 0.48/0.69       (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_182) \/
% 0.48/0.69     member skolemFOFtoCNF_U
% 0.48/0.69       (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_177 $_182) $_182 \/
% 0.48/0.69     member skolemFOFtoCNF_U
% 0.48/0.69       (skolemFOFtoCNF_X31 skolemFOFtoCNF_U $_182 $_183) $_183 \/
% 0.48/0.69     member skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_183)
% 0.48/0.69       $_183
% 0.48/0.69  |- ~agent skolemFOFtoCNF_U $_187 $_186 \/ ~barrel skolemFOFtoCNF_U $_187 \/
% 0.48/0.69     ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_186 \/
% 0.48/0.69     ~chevy skolemFOFtoCNF_U $_186 \/ ~dirty skolemFOFtoCNF_U $_186 \/
% 0.48/0.69     ~down skolemFOFtoCNF_U $_187 skolemFOFtoCNF_X1 \/
% 0.48/0.69     ~event skolemFOFtoCNF_U $_187 \/ ~frontseat skolemFOFtoCNF_U $_185 \/
% 0.48/0.69     ~group skolemFOFtoCNF_U $_188 \/ ~group skolemFOFtoCNF_U $_189 \/
% 0.48/0.69     ~in skolemFOFtoCNF_U $_187 skolemFOFtoCNF_X1 \/
% 0.48/0.69     ~old skolemFOFtoCNF_U $_186 \/ ~present skolemFOFtoCNF_U $_187 \/
% 0.48/0.69     ~two skolemFOFtoCNF_U $_188 \/ ~wheel skolemFOFtoCNF_U $_186 \/
% 0.48/0.69     ~white skolemFOFtoCNF_U $_186 \/
% 0.48/0.69     definitionFOFtoCNF_0 skolemFOFtoCNF_U $_188
% 0.48/0.69       (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_188) \/
% 0.48/0.69     member skolemFOFtoCNF_U
% 0.48/0.69       (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_185 $_188) $_188 \/
% 0.48/0.69     member skolemFOFtoCNF_U
% 0.48/0.69       (skolemFOFtoCNF_X31 skolemFOFtoCNF_U $_188 $_189) $_189 \/
% 0.48/0.69     member skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_189)
% 0.48/0.69       $_189
% 0.48/0.69  |- ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X2 $_191 \/
% 0.48/0.69     ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_191 \/
% 0.48/0.69     ~chevy skolemFOFtoCNF_U $_191 \/ ~dirty skolemFOFtoCNF_U $_191 \/
% 0.48/0.69     ~frontseat skolemFOFtoCNF_U $_190 \/ ~group skolemFOFtoCNF_U $_193 \/
% 0.48/0.69     ~group skolemFOFtoCNF_U $_194 \/ ~old skolemFOFtoCNF_U $_191 \/
% 0.48/0.69     ~two skolemFOFtoCNF_U $_193 \/ ~wheel skolemFOFtoCNF_U $_191 \/
% 0.48/0.69     ~white skolemFOFtoCNF_U $_191 \/
% 0.48/0.69     definitionFOFtoCNF_0 skolemFOFtoCNF_U $_193
% 0.48/0.69       (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_193) \/
% 0.48/0.69     member skolemFOFtoCNF_U
% 0.48/0.69       (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_190 $_193) $_193 \/
% 0.48/0.69     member skolemFOFtoCNF_U
% 0.48/0.69       (skolemFOFtoCNF_X31 skolemFOFtoCNF_U $_193 $_194) $_194 \/
% 0.48/0.69     member skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_194)
% 0.48/0.69       $_194
% 0.48/0.70  |- ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X2 skolemFOFtoCNF_X \/
% 0.48/0.70     ~chevy skolemFOFtoCNF_U skolemFOFtoCNF_X \/
% 0.48/0.70     ~dirty skolemFOFtoCNF_U skolemFOFtoCNF_X \/
% 0.48/0.70     ~frontseat skolemFOFtoCNF_U $_195 \/ ~group skolemFOFtoCNF_U $_197 \/
% 0.48/0.70     ~group skolemFOFtoCNF_U $_198 \/
% 0.48/0.70     ~old skolemFOFtoCNF_U skolemFOFtoCNF_X \/ ~two skolemFOFtoCNF_U $_197 \/
% 0.48/0.70     ~white skolemFOFtoCNF_U skolemFOFtoCNF_X \/
% 0.48/0.70     definitionFOFtoCNF_0 skolemFOFtoCNF_U $_197
% 0.48/0.70       (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_197) \/
% 0.48/0.70     member skolemFOFtoCNF_U
% 0.48/0.70       (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_195 $_197) $_197 \/
% 0.48/0.70     member skolemFOFtoCNF_U
% 0.48/0.70       (skolemFOFtoCNF_X31 skolemFOFtoCNF_U $_197 $_198) $_198 \/
% 0.48/0.70     member skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_198)
% 0.48/0.70       $_198
% 0.48/0.70  |- ~agent skolemFOFtoCNF_U $_226 $_223 \/ ~barrel skolemFOFtoCNF_U $_226 \/
% 0.48/0.70     ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_223 \/
% 0.48/0.70     ~chevy skolemFOFtoCNF_U $_223 \/ ~city skolemFOFtoCNF_U $_225 \/
% 0.48/0.70     ~dirty skolemFOFtoCNF_U $_223 \/ ~down skolemFOFtoCNF_U $_226 $_225 \/
% 0.48/0.70     ~event skolemFOFtoCNF_U $_226 \/ ~frontseat skolemFOFtoCNF_U $_222 \/
% 0.48/0.70     ~group skolemFOFtoCNF_U $_227 \/ ~group skolemFOFtoCNF_U $_228 \/
% 0.48/0.70     ~hollywood_placename skolemFOFtoCNF_U $_224 \/
% 0.48/0.70     ~in skolemFOFtoCNF_U $_226 $_225 \/ ~lonely skolemFOFtoCNF_U $_225 \/
% 0.48/0.70     ~of skolemFOFtoCNF_U $_224 $_225 \/ ~old skolemFOFtoCNF_U $_223 \/
% 0.48/0.70     ~placename skolemFOFtoCNF_U $_224 \/ ~present skolemFOFtoCNF_U $_226 \/
% 0.48/0.70     ~street skolemFOFtoCNF_U $_225 \/ ~two skolemFOFtoCNF_U $_227 \/
% 0.48/0.70     ~wheel skolemFOFtoCNF_U $_223 \/ ~white skolemFOFtoCNF_U $_223 \/
% 0.48/0.70     definitionFOFtoCNF_0 skolemFOFtoCNF_U $_227
% 0.48/0.70       (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_227) \/
% 0.48/0.70     member skolemFOFtoCNF_U
% 0.48/0.70       (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_222 $_227) $_227 \/
% 0.48/0.70     member skolemFOFtoCNF_U
% 0.48/0.70       (skolemFOFtoCNF_X32 skolemFOFtoCNF_U $_227 $_228) $_227 \/
% 0.48/0.70     member skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_228)
% 0.48/0.70       $_228
% 0.48/0.70  |- ~agent skolemFOFtoCNF_U $_232 $_231 \/ ~barrel skolemFOFtoCNF_U $_232 \/
% 0.48/0.70     ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_231 \/
% 0.48/0.70     ~chevy skolemFOFtoCNF_U $_231 \/ ~dirty skolemFOFtoCNF_U $_231 \/
% 0.48/0.70     ~down skolemFOFtoCNF_U $_232 skolemFOFtoCNF_X1 \/
% 0.48/0.70     ~event skolemFOFtoCNF_U $_232 \/ ~frontseat skolemFOFtoCNF_U $_230 \/
% 0.48/0.70     ~group skolemFOFtoCNF_U $_233 \/ ~group skolemFOFtoCNF_U $_234 \/
% 0.48/0.70     ~in skolemFOFtoCNF_U $_232 skolemFOFtoCNF_X1 \/
% 0.48/0.70     ~old skolemFOFtoCNF_U $_231 \/ ~present skolemFOFtoCNF_U $_232 \/
% 0.48/0.70     ~two skolemFOFtoCNF_U $_233 \/ ~wheel skolemFOFtoCNF_U $_231 \/
% 0.48/0.70     ~white skolemFOFtoCNF_U $_231 \/
% 0.48/0.70     definitionFOFtoCNF_0 skolemFOFtoCNF_U $_233
% 0.48/0.70       (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_233) \/
% 0.48/0.70     member skolemFOFtoCNF_U
% 0.48/0.70       (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_230 $_233) $_233 \/
% 0.48/0.70     member skolemFOFtoCNF_U
% 0.48/0.70       (skolemFOFtoCNF_X32 skolemFOFtoCNF_U $_233 $_234) $_233 \/
% 0.48/0.70     member skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_234)
% 0.48/0.70       $_234
% 0.48/0.70  |- ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X2 $_236 \/
% 0.48/0.70     ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_236 \/
% 0.48/0.70     ~chevy skolemFOFtoCNF_U $_236 \/ ~dirty skolemFOFtoCNF_U $_236 \/
% 0.48/0.70     ~frontseat skolemFOFtoCNF_U $_235 \/ ~group skolemFOFtoCNF_U $_238 \/
% 0.48/0.70     ~group skolemFOFtoCNF_U $_239 \/ ~old skolemFOFtoCNF_U $_236 \/
% 0.48/0.70     ~two skolemFOFtoCNF_U $_238 \/ ~wheel skolemFOFtoCNF_U $_236 \/
% 0.48/0.70     ~white skolemFOFtoCNF_U $_236 \/
% 0.48/0.70     definitionFOFtoCNF_0 skolemFOFtoCNF_U $_238
% 0.48/0.70       (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_238) \/
% 0.48/0.70     member skolemFOFtoCNF_U
% 0.48/0.70       (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_235 $_238) $_238 \/
% 0.48/0.70     member skolemFOFtoCNF_U
% 0.48/0.70       (skolemFOFtoCNF_X32 skolemFOFtoCNF_U $_238 $_239) $_238 \/
% 0.48/0.70     member skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_239)
% 0.48/0.70       $_239
% 0.48/0.70  |- ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X2 skolemFOFtoCNF_X \/
% 0.48/0.70     ~chevy skolemFOFtoCNF_U skolemFOFtoCNF_X \/
% 0.48/0.70     ~dirty skolemFOFtoCNF_U skolemFOFtoCNF_X \/
% 0.48/0.70     ~frontseat skolemFOFtoCNF_U $_240 \/ ~group skolemFOFtoCNF_U $_242 \/
% 0.48/0.70     ~group skolemFOFtoCNF_U $_243 \/
% 0.48/0.70     ~old skolemFOFtoCNF_U skolemFOFtoCNF_X \/ ~two skolemFOFtoCNF_U $_242 \/
% 0.48/0.70     ~white skolemFOFtoCNF_U skolemFOFtoCNF_X \/
% 0.48/0.70     definitionFOFtoCNF_0 skolemFOFtoCNF_U $_242
% 0.48/0.70       (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_242) \/
% 0.48/0.70     member skolemFOFtoCNF_U
% 0.48/0.70       (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_240 $_242) $_242 \/
% 0.48/0.70     member skolemFOFtoCNF_U
% 0.48/0.70       (skolemFOFtoCNF_X32 skolemFOFtoCNF_U $_242 $_243) $_242 \/
% 0.48/0.70     member skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_243)
% 0.48/0.70       $_243
% 0.48/0.70  |- ~agent skolemFOFtoCNF_U $_307 $_304 \/ ~barrel skolemFOFtoCNF_U $_307 \/
% 0.48/0.70     ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_304 \/
% 0.48/0.70     ~black skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_309) \/
% 0.48/0.70     ~cheap skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_309) \/
% 0.48/0.70     ~chevy skolemFOFtoCNF_U $_304 \/ ~city skolemFOFtoCNF_U $_306 \/
% 0.48/0.70     ~coat skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_309) \/
% 0.48/0.70     ~dirty skolemFOFtoCNF_U $_304 \/ ~down skolemFOFtoCNF_U $_307 $_306 \/
% 0.48/0.70     ~event skolemFOFtoCNF_U $_307 \/ ~forename skolemFOFtoCNF_U $_302 \/
% 0.48/0.70     ~frontseat skolemFOFtoCNF_U $_303 \/ ~group skolemFOFtoCNF_U $_308 \/
% 0.48/0.70     ~group skolemFOFtoCNF_U $_309 \/
% 0.48/0.70     ~hollywood_placename skolemFOFtoCNF_U $_305 \/
% 0.48/0.70     ~in skolemFOFtoCNF_U $_307 $_306 \/
% 0.48/0.70     ~jules_forename skolemFOFtoCNF_U $_302 \/
% 0.48/0.70     ~lonely skolemFOFtoCNF_U $_306 \/
% 0.48/0.70     ~of skolemFOFtoCNF_U $_302 skolemFOFtoCNF_V \/
% 0.48/0.70     ~of skolemFOFtoCNF_U $_305 $_306 \/ ~old skolemFOFtoCNF_U $_304 \/
% 0.48/0.70     ~placename skolemFOFtoCNF_U $_305 \/ ~present skolemFOFtoCNF_U $_307 \/
% 0.48/0.70     ~street skolemFOFtoCNF_U $_306 \/ ~two skolemFOFtoCNF_U $_308 \/
% 0.48/0.70     ~wheel skolemFOFtoCNF_U $_304 \/ ~white skolemFOFtoCNF_U $_304 \/
% 0.48/0.70     definitionFOFtoCNF_0 skolemFOFtoCNF_U $_308
% 0.48/0.70       (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_308) \/
% 0.48/0.70     member skolemFOFtoCNF_U
% 0.48/0.70       (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_303 $_308) $_308 \/
% 0.48/0.70     member skolemFOFtoCNF_U
% 0.48/0.70       (skolemFOFtoCNF_X32 skolemFOFtoCNF_U $_308 $_309) $_308
% 0.48/0.70  |- ~agent skolemFOFtoCNF_U $_327 $_324 \/ ~barrel skolemFOFtoCNF_U $_327 \/
% 0.48/0.70     ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_324 \/
% 0.48/0.70     ~black skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_329) \/
% 0.48/0.70     ~cheap skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_329) \/
% 0.48/0.70     ~chevy skolemFOFtoCNF_U $_324 \/ ~city skolemFOFtoCNF_U $_326 \/
% 0.48/0.70     ~coat skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_329) \/
% 0.48/0.70     ~dirty skolemFOFtoCNF_U $_324 \/ ~down skolemFOFtoCNF_U $_327 $_326 \/
% 0.48/0.70     ~event skolemFOFtoCNF_U $_327 \/ ~forename skolemFOFtoCNF_U $_322 \/
% 0.48/0.70     ~frontseat skolemFOFtoCNF_U $_323 \/ ~group skolemFOFtoCNF_U $_328 \/
% 0.48/0.70     ~group skolemFOFtoCNF_U $_329 \/
% 0.48/0.70     ~hollywood_placename skolemFOFtoCNF_U $_325 \/
% 0.48/0.70     ~in skolemFOFtoCNF_U $_327 $_326 \/
% 0.48/0.70     ~jules_forename skolemFOFtoCNF_U $_322 \/
% 0.48/0.70     ~lonely skolemFOFtoCNF_U $_326 \/
% 0.48/0.70     ~of skolemFOFtoCNF_U $_322 skolemFOFtoCNF_V \/
% 0.48/0.70     ~of skolemFOFtoCNF_U $_325 $_326 \/ ~old skolemFOFtoCNF_U $_324 \/
% 0.48/0.70     ~placename skolemFOFtoCNF_U $_325 \/ ~present skolemFOFtoCNF_U $_327 \/
% 0.48/0.70     ~street skolemFOFtoCNF_U $_326 \/ ~two skolemFOFtoCNF_U $_328 \/
% 0.48/0.70     ~wheel skolemFOFtoCNF_U $_324 \/ ~white skolemFOFtoCNF_U $_324 \/
% 0.48/0.70     definitionFOFtoCNF_0 skolemFOFtoCNF_U $_328
% 0.48/0.70       (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_328) \/
% 0.48/0.70     member skolemFOFtoCNF_U
% 0.48/0.70       (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_323 $_328) $_328 \/
% 0.48/0.70     member skolemFOFtoCNF_U
% 0.48/0.70       (skolemFOFtoCNF_X31 skolemFOFtoCNF_U $_328 $_329) $_329
% 0.48/0.70  SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.48/0.70  
%------------------------------------------------------------------------------