%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : NLP199+1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n011.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:58 EDT 2022 % Result : CounterSatisfiable 0.48s 0.67s % Output : Saturation 0.53s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : NLP199+1 : TPTP v8.1.0. Released v2.4.0. % 0.06/0.12 % Command : metis --show proof --show saturation %s % 0.13/0.33 % Computer : n011.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Fri Jul 1 10:25:48 EDT 2022 % 0.13/0.33 % CPUTime : % 0.13/0.33 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.48/0.67 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.48/0.67 % 0.48/0.67 SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.48/0.67 |- actual_world skolemFOFtoCNF_U % 0.48/0.67 |- agent skolemFOFtoCNF_U skolemFOFtoCNF_X2 skolemFOFtoCNF_Y % 0.48/0.67 |- barrel skolemFOFtoCNF_U skolemFOFtoCNF_X2 % 0.48/0.67 |- be skolemFOFtoCNF_U skolemFOFtoCNF_X5 skolemFOFtoCNF_V skolemFOFtoCNF_X6 % 0.48/0.67 |- behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 skolemFOFtoCNF_X6 % 0.48/0.67 |- chevy skolemFOFtoCNF_U skolemFOFtoCNF_Y % 0.48/0.67 |- city skolemFOFtoCNF_U skolemFOFtoCNF_X1 % 0.48/0.67 |- dirty skolemFOFtoCNF_U skolemFOFtoCNF_Y % 0.48/0.67 |- down skolemFOFtoCNF_U skolemFOFtoCNF_X2 skolemFOFtoCNF_X1 % 0.48/0.67 |- event skolemFOFtoCNF_U skolemFOFtoCNF_X2 % 0.48/0.67 |- forename skolemFOFtoCNF_U skolemFOFtoCNF_W % 0.48/0.67 |- frontseat skolemFOFtoCNF_U skolemFOFtoCNF_X % 0.48/0.67 |- group skolemFOFtoCNF_U skolemFOFtoCNF_X3 % 0.48/0.67 |- group skolemFOFtoCNF_U skolemFOFtoCNF_X4 % 0.48/0.67 |- hollywood_placename skolemFOFtoCNF_U skolemFOFtoCNF_Z % 0.48/0.67 |- in skolemFOFtoCNF_U skolemFOFtoCNF_X2 skolemFOFtoCNF_X1 % 0.48/0.67 |- jules_forename skolemFOFtoCNF_U skolemFOFtoCNF_W % 0.48/0.67 |- lonely skolemFOFtoCNF_U skolemFOFtoCNF_X1 % 0.48/0.67 |- man skolemFOFtoCNF_U skolemFOFtoCNF_V % 0.48/0.67 |- of skolemFOFtoCNF_U skolemFOFtoCNF_W skolemFOFtoCNF_V % 0.48/0.67 |- of skolemFOFtoCNF_U skolemFOFtoCNF_Z skolemFOFtoCNF_X1 % 0.48/0.67 |- old skolemFOFtoCNF_U skolemFOFtoCNF_Y % 0.48/0.67 |- placename skolemFOFtoCNF_U skolemFOFtoCNF_Z % 0.48/0.67 |- present skolemFOFtoCNF_U skolemFOFtoCNF_X2 % 0.48/0.67 |- state skolemFOFtoCNF_U skolemFOFtoCNF_X5 % 0.48/0.67 |- street skolemFOFtoCNF_U skolemFOFtoCNF_X1 % 0.48/0.67 |- two skolemFOFtoCNF_U skolemFOFtoCNF_X3 % 0.48/0.67 |- wheel skolemFOFtoCNF_U skolemFOFtoCNF_X6 % 0.48/0.67 |- white skolemFOFtoCNF_U skolemFOFtoCNF_Y % 0.48/0.67 |- ~member skolemFOFtoCNF_U $X10 skolemFOFtoCNF_X3 \/ % 0.48/0.67 fellow skolemFOFtoCNF_U $X10 % 0.48/0.67 |- ~member skolemFOFtoCNF_U $X10 skolemFOFtoCNF_X3 \/ % 0.48/0.67 young skolemFOFtoCNF_U $X10 % 0.48/0.67 |- ~member skolemFOFtoCNF_U $X11 skolemFOFtoCNF_X4 \/ % 0.48/0.67 ~member skolemFOFtoCNF_U $X12 skolemFOFtoCNF_X3 \/ % 0.48/0.67 agent skolemFOFtoCNF_U (skolemFOFtoCNF_X13 $X11 $X12) $X12 % 0.48/0.67 |- ~member skolemFOFtoCNF_U $X11 skolemFOFtoCNF_X4 \/ % 0.48/0.67 ~member skolemFOFtoCNF_U $X12 skolemFOFtoCNF_X3 \/ % 0.48/0.67 event skolemFOFtoCNF_U (skolemFOFtoCNF_X13 $X11 $X12) % 0.48/0.67 |- ~member skolemFOFtoCNF_U $X11 skolemFOFtoCNF_X4 \/ % 0.48/0.67 ~member skolemFOFtoCNF_U $X12 skolemFOFtoCNF_X3 \/ % 0.48/0.67 nonreflexive skolemFOFtoCNF_U (skolemFOFtoCNF_X13 $X11 $X12) % 0.48/0.67 |- ~member skolemFOFtoCNF_U $X11 skolemFOFtoCNF_X4 \/ % 0.48/0.67 ~member skolemFOFtoCNF_U $X12 skolemFOFtoCNF_X3 \/ % 0.48/0.67 patient skolemFOFtoCNF_U (skolemFOFtoCNF_X13 $X11 $X12) $X11 % 0.48/0.67 |- ~member skolemFOFtoCNF_U $X11 skolemFOFtoCNF_X4 \/ % 0.48/0.67 ~member skolemFOFtoCNF_U $X12 skolemFOFtoCNF_X3 \/ % 0.48/0.67 present skolemFOFtoCNF_U (skolemFOFtoCNF_X13 $X11 $X12) % 0.48/0.67 |- ~member skolemFOFtoCNF_U $X11 skolemFOFtoCNF_X4 \/ % 0.48/0.67 ~member skolemFOFtoCNF_U $X12 skolemFOFtoCNF_X3 \/ % 0.48/0.67 wear skolemFOFtoCNF_U (skolemFOFtoCNF_X13 $X11 $X12) % 0.48/0.67 |- ~member skolemFOFtoCNF_U $X14 skolemFOFtoCNF_X4 \/ % 0.48/0.67 black skolemFOFtoCNF_U $X14 % 0.48/0.67 |- ~member skolemFOFtoCNF_U $X14 skolemFOFtoCNF_X4 \/ % 0.48/0.67 cheap skolemFOFtoCNF_U $X14 % 0.48/0.67 |- ~member skolemFOFtoCNF_U $X14 skolemFOFtoCNF_X4 \/ % 0.48/0.67 coat skolemFOFtoCNF_U $X14 % 0.48/0.67 |- ~member skolemFOFtoCNF_U $X7 skolemFOFtoCNF_X3 \/ % 0.48/0.67 be skolemFOFtoCNF_U (skolemFOFtoCNF_X8 $X7) $X7 (skolemFOFtoCNF_X9 $X7) % 0.48/0.67 |- ~member skolemFOFtoCNF_U $X7 skolemFOFtoCNF_X3 \/ % 0.48/0.67 in skolemFOFtoCNF_U (skolemFOFtoCNF_X9 $X7) skolemFOFtoCNF_X % 0.48/0.67 |- ~member skolemFOFtoCNF_U $X7 skolemFOFtoCNF_X3 \/ % 0.48/0.67 state skolemFOFtoCNF_U (skolemFOFtoCNF_X8 $X7) % 0.48/0.67 |- ~definitionFOFtoCNF_0 $X15 $X23 $X30 \/ member $X15 $X30 $X23 % 0.48/0.67 |- ~definitionFOFtoCNF_0 $X15 $X23 $X30 \/ ~fellow $X15 $X30 \/ % 0.48/0.67 ~young $X15 $X30 % 0.48/0.67 |- ~member $X15 $X30 $X23 \/ definitionFOFtoCNF_0 $X15 $X23 $X30 \/ % 0.48/0.67 fellow $X15 $X30 % 0.48/0.67 |- ~member $X15 $X30 $X23 \/ definitionFOFtoCNF_0 $X15 $X23 $X30 \/ % 0.48/0.67 young $X15 $X30 % 0.48/0.67 |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/ % 0.48/0.67 ~be $X15 $X25 $X16 $X26 \/ ~behind $X15 $X26 $X18 \/ ~chevy $X15 $X19 \/ % 0.48/0.67 ~city $X15 $X21 \/ ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ % 0.48/0.67 ~event $X15 $X22 \/ ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ % 0.48/0.67 ~group $X15 $X23 \/ ~group $X15 $X24 \/ % 0.48/0.67 ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/ % 0.48/0.67 ~jules_forename $X15 $X17 \/ ~lonely $X15 $X21 \/ ~man $X15 $X16 \/ % 0.48/0.67 ~of $X15 $X17 $X16 \/ ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ % 0.48/0.67 ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~state $X15 $X25 \/ % 0.48/0.67 ~street $X15 $X21 \/ ~two $X15 $X23 \/ ~wheel $X15 $X18 \/ % 0.48/0.67 ~white $X15 $X19 \/ % 0.48/0.67 definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/ % 0.48/0.67 member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23 \/ % 0.48/0.67 member $X15 (skolemFOFtoCNF_X31 $X15 $X23 $X24) $X24 \/ % 0.48/0.67 member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24 % 0.48/0.67 |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/ % 0.48/0.67 ~be $X15 $X25 $X16 $X26 \/ ~behind $X15 $X26 $X18 \/ ~chevy $X15 $X19 \/ % 0.48/0.67 ~city $X15 $X21 \/ ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ % 0.48/0.67 ~event $X15 $X22 \/ ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ % 0.48/0.67 ~group $X15 $X23 \/ ~group $X15 $X24 \/ % 0.48/0.67 ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/ % 0.48/0.67 ~jules_forename $X15 $X17 \/ ~lonely $X15 $X21 \/ ~man $X15 $X16 \/ % 0.48/0.67 ~of $X15 $X17 $X16 \/ ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ % 0.48/0.67 ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~state $X15 $X25 \/ % 0.48/0.67 ~street $X15 $X21 \/ ~two $X15 $X23 \/ ~wheel $X15 $X18 \/ % 0.48/0.67 ~white $X15 $X19 \/ % 0.48/0.67 definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/ % 0.48/0.67 member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23 \/ % 0.48/0.67 member $X15 (skolemFOFtoCNF_X32 $X15 $X23 $X24) $X23 \/ % 0.48/0.67 member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24 % 0.48/0.67 |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/ % 0.48/0.67 ~be $X15 $X25 $X16 $X26 \/ % 0.48/0.67 ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/ % 0.48/0.67 ~behind $X15 $X26 $X18 \/ ~chevy $X15 $X19 \/ ~city $X15 $X21 \/ % 0.48/0.67 ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/ % 0.48/0.67 ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/ % 0.48/0.67 ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/ % 0.48/0.67 ~in $X15 $X22 $X21 \/ ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X17 \/ % 0.48/0.67 ~lonely $X15 $X21 \/ ~man $X15 $X16 \/ ~of $X15 $X17 $X16 \/ % 0.48/0.67 ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ ~placename $X15 $X20 \/ % 0.48/0.67 ~present $X15 $X22 \/ ~state $X15 $X25 \/ ~state $X15 $X28 \/ % 0.48/0.67 ~street $X15 $X21 \/ ~two $X15 $X23 \/ ~wheel $X15 $X18 \/ % 0.48/0.67 ~white $X15 $X19 \/ % 0.48/0.67 definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/ % 0.48/0.67 member $X15 (skolemFOFtoCNF_X31 $X15 $X23 $X24) $X24 \/ % 0.48/0.67 member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24 % 0.48/0.67 |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/ % 0.48/0.67 ~be $X15 $X25 $X16 $X26 \/ % 0.48/0.67 ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/ % 0.48/0.67 ~behind $X15 $X26 $X18 \/ ~chevy $X15 $X19 \/ ~city $X15 $X21 \/ % 0.48/0.67 ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/ % 0.48/0.67 ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/ % 0.48/0.67 ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/ % 0.48/0.67 ~in $X15 $X22 $X21 \/ ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X17 \/ % 0.48/0.67 ~lonely $X15 $X21 \/ ~man $X15 $X16 \/ ~of $X15 $X17 $X16 \/ % 0.48/0.67 ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ ~placename $X15 $X20 \/ % 0.48/0.67 ~present $X15 $X22 \/ ~state $X15 $X25 \/ ~state $X15 $X28 \/ % 0.48/0.67 ~street $X15 $X21 \/ ~two $X15 $X23 \/ ~wheel $X15 $X18 \/ % 0.48/0.67 ~white $X15 $X19 \/ % 0.48/0.67 definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/ % 0.48/0.67 member $X15 (skolemFOFtoCNF_X32 $X15 $X23 $X24) $X23 \/ % 0.48/0.67 member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24 % 0.48/0.67 |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/ % 0.48/0.67 ~be $X15 $X25 $X16 $X26 \/ ~behind $X15 $X26 $X18 \/ % 0.48/0.67 ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ % 0.48/0.67 ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/ % 0.48/0.67 ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ % 0.48/0.67 ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/ % 0.48/0.67 ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/ % 0.48/0.67 ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/ % 0.48/0.67 ~in $X15 $X22 $X21 \/ ~jules_forename $X15 $X17 \/ ~lonely $X15 $X21 \/ % 0.48/0.67 ~man $X15 $X16 \/ ~of $X15 $X17 $X16 \/ ~of $X15 $X20 $X21 \/ % 0.48/0.67 ~old $X15 $X19 \/ ~placename $X15 $X20 \/ ~present $X15 $X22 \/ % 0.48/0.67 ~state $X15 $X25 \/ ~street $X15 $X21 \/ ~two $X15 $X23 \/ % 0.48/0.67 ~wheel $X15 $X18 \/ ~white $X15 $X19 \/ % 0.48/0.67 definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/ % 0.48/0.67 member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23 \/ % 0.48/0.67 member $X15 (skolemFOFtoCNF_X31 $X15 $X23 $X24) $X24 % 0.48/0.67 |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/ % 0.48/0.67 ~be $X15 $X25 $X16 $X26 \/ ~behind $X15 $X26 $X18 \/ % 0.48/0.67 ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ % 0.48/0.67 ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/ % 0.48/0.67 ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ % 0.48/0.67 ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/ % 0.48/0.67 ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/ % 0.48/0.67 ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/ % 0.48/0.67 ~in $X15 $X22 $X21 \/ ~jules_forename $X15 $X17 \/ ~lonely $X15 $X21 \/ % 0.48/0.67 ~man $X15 $X16 \/ ~of $X15 $X17 $X16 \/ ~of $X15 $X20 $X21 \/ % 0.48/0.67 ~old $X15 $X19 \/ ~placename $X15 $X20 \/ ~present $X15 $X22 \/ % 0.48/0.67 ~state $X15 $X25 \/ ~street $X15 $X21 \/ ~two $X15 $X23 \/ % 0.48/0.67 ~wheel $X15 $X18 \/ ~white $X15 $X19 \/ % 0.48/0.67 definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/ % 0.48/0.67 member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23 \/ % 0.48/0.67 member $X15 (skolemFOFtoCNF_X32 $X15 $X23 $X24) $X23 % 0.48/0.67 |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/ % 0.48/0.67 ~be $X15 $X25 $X16 $X26 \/ % 0.48/0.67 ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/ % 0.48/0.67 ~behind $X15 $X26 $X18 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ % 0.48/0.67 ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/ % 0.48/0.67 ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ % 0.48/0.67 ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/ % 0.48/0.67 ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/ % 0.48/0.67 ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/ % 0.48/0.67 ~in $X15 $X22 $X21 \/ ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X17 \/ % 0.48/0.67 ~lonely $X15 $X21 \/ ~man $X15 $X16 \/ ~of $X15 $X17 $X16 \/ % 0.48/0.67 ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ ~placename $X15 $X20 \/ % 0.48/0.67 ~present $X15 $X22 \/ ~state $X15 $X25 \/ ~state $X15 $X28 \/ % 0.48/0.67 ~street $X15 $X21 \/ ~two $X15 $X23 \/ ~wheel $X15 $X18 \/ % 0.48/0.67 ~white $X15 $X19 \/ % 0.48/0.67 definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/ % 0.48/0.67 member $X15 (skolemFOFtoCNF_X31 $X15 $X23 $X24) $X24 % 0.48/0.67 |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/ % 0.48/0.67 ~be $X15 $X25 $X16 $X26 \/ % 0.48/0.67 ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/ % 0.48/0.67 ~behind $X15 $X26 $X18 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ % 0.48/0.67 ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/ % 0.48/0.67 ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ % 0.48/0.67 ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/ % 0.48/0.67 ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/ % 0.48/0.67 ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/ % 0.48/0.67 ~in $X15 $X22 $X21 \/ ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X17 \/ % 0.48/0.67 ~lonely $X15 $X21 \/ ~man $X15 $X16 \/ ~of $X15 $X17 $X16 \/ % 0.48/0.67 ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ ~placename $X15 $X20 \/ % 0.48/0.67 ~present $X15 $X22 \/ ~state $X15 $X25 \/ ~state $X15 $X28 \/ % 0.48/0.67 ~street $X15 $X21 \/ ~two $X15 $X23 \/ ~wheel $X15 $X18 \/ % 0.48/0.67 ~white $X15 $X19 \/ % 0.48/0.67 definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/ % 0.48/0.67 member $X15 (skolemFOFtoCNF_X32 $X15 $X23 $X24) $X23 % 0.48/0.67 |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ % 0.48/0.67 ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/ % 0.48/0.67 ~barrel $X15 $X22 \/ ~be $X15 $X25 $X16 $X26 \/ % 0.48/0.67 ~behind $X15 $X26 $X18 \/ ~chevy $X15 $X19 \/ ~city $X15 $X21 \/ % 0.48/0.67 ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/ % 0.48/0.67 ~event $X15 $X33 \/ ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ % 0.48/0.67 ~group $X15 $X23 \/ ~group $X15 $X24 \/ % 0.48/0.67 ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/ % 0.48/0.67 ~jules_forename $X15 $X17 \/ ~lonely $X15 $X21 \/ ~man $X15 $X16 \/ % 0.48/0.67 ~nonreflexive $X15 $X33 \/ ~of $X15 $X17 $X16 \/ ~of $X15 $X20 $X21 \/ % 0.48/0.67 ~old $X15 $X19 \/ % 0.48/0.67 ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/ % 0.48/0.67 ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/ % 0.48/0.67 ~state $X15 $X25 \/ ~street $X15 $X21 \/ ~two $X15 $X23 \/ % 0.48/0.67 ~wear $X15 $X33 \/ ~wheel $X15 $X18 \/ ~white $X15 $X19 \/ % 0.48/0.67 definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/ % 0.48/0.67 member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23 \/ % 0.48/0.67 member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24 % 0.48/0.67 |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ % 0.48/0.67 ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/ % 0.48/0.67 ~barrel $X15 $X22 \/ ~be $X15 $X25 $X16 $X26 \/ % 0.48/0.67 ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/ % 0.48/0.67 ~behind $X15 $X26 $X18 \/ ~chevy $X15 $X19 \/ ~city $X15 $X21 \/ % 0.48/0.67 ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/ % 0.48/0.67 ~event $X15 $X33 \/ ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ % 0.48/0.67 ~group $X15 $X23 \/ ~group $X15 $X24 \/ % 0.48/0.67 ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/ % 0.48/0.67 ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X17 \/ ~lonely $X15 $X21 \/ % 0.48/0.67 ~man $X15 $X16 \/ ~nonreflexive $X15 $X33 \/ ~of $X15 $X17 $X16 \/ % 0.48/0.67 ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ % 0.48/0.67 ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/ % 0.48/0.67 ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/ % 0.48/0.67 ~state $X15 $X25 \/ ~state $X15 $X28 \/ ~street $X15 $X21 \/ % 0.48/0.67 ~two $X15 $X23 \/ ~wear $X15 $X33 \/ ~wheel $X15 $X18 \/ % 0.48/0.67 ~white $X15 $X19 \/ % 0.48/0.67 definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/ % 0.48/0.67 member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24 % 0.48/0.67 |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ % 0.48/0.67 ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/ % 0.48/0.67 ~barrel $X15 $X22 \/ ~be $X15 $X25 $X16 $X26 \/ % 0.48/0.67 ~behind $X15 $X26 $X18 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ % 0.48/0.67 ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/ % 0.48/0.67 ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ % 0.48/0.67 ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/ % 0.48/0.67 ~event $X15 $X33 \/ ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ % 0.48/0.67 ~group $X15 $X23 \/ ~group $X15 $X24 \/ % 0.48/0.67 ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/ % 0.48/0.67 ~jules_forename $X15 $X17 \/ ~lonely $X15 $X21 \/ ~man $X15 $X16 \/ % 0.48/0.67 ~nonreflexive $X15 $X33 \/ ~of $X15 $X17 $X16 \/ ~of $X15 $X20 $X21 \/ % 0.48/0.67 ~old $X15 $X19 \/ % 0.48/0.67 ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/ % 0.48/0.67 ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/ % 0.48/0.67 ~state $X15 $X25 \/ ~street $X15 $X21 \/ ~two $X15 $X23 \/ % 0.48/0.67 ~wear $X15 $X33 \/ ~wheel $X15 $X18 \/ ~white $X15 $X19 \/ % 0.48/0.67 definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/ % 0.48/0.67 member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23 % 0.48/0.67 |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ % 0.48/0.67 ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/ % 0.48/0.67 ~barrel $X15 $X22 \/ ~be $X15 $X25 $X16 $X26 \/ % 0.48/0.67 ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/ % 0.48/0.67 ~behind $X15 $X26 $X18 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ % 0.48/0.67 ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/ % 0.48/0.67 ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ % 0.48/0.67 ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/ % 0.48/0.67 ~event $X15 $X33 \/ ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ % 0.48/0.67 ~group $X15 $X23 \/ ~group $X15 $X24 \/ % 0.48/0.67 ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/ % 0.48/0.67 ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X17 \/ ~lonely $X15 $X21 \/ % 0.48/0.67 ~man $X15 $X16 \/ ~nonreflexive $X15 $X33 \/ ~of $X15 $X17 $X16 \/ % 0.48/0.67 ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ % 0.48/0.67 ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/ % 0.48/0.67 ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/ % 0.48/0.67 ~state $X15 $X25 \/ ~state $X15 $X28 \/ ~street $X15 $X21 \/ % 0.48/0.67 ~two $X15 $X23 \/ ~wear $X15 $X33 \/ ~wheel $X15 $X18 \/ % 0.48/0.67 ~white $X15 $X19 \/ % 0.48/0.67 definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) % 0.48/0.67 |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/ % 0.48/0.67 ~be $X15 $X25 $X21 $X26 \/ ~behind $X15 $X26 $X18 \/ ~chevy $X15 $X19 \/ % 0.48/0.67 ~city $X15 $X21 \/ ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ % 0.48/0.67 ~event $X15 $X22 \/ ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/ % 0.48/0.67 ~group $X15 $X23 \/ ~group $X15 $X24 \/ % 0.48/0.67 ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/ % 0.48/0.67 ~jules_forename $X15 $X20 \/ ~lonely $X15 $X21 \/ ~man $X15 $X21 \/ % 0.48/0.67 ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ ~placename $X15 $X20 \/ % 0.48/0.67 ~present $X15 $X22 \/ ~state $X15 $X25 \/ ~street $X15 $X21 \/ % 0.48/0.67 ~two $X15 $X23 \/ ~wheel $X15 $X18 \/ ~white $X15 $X19 \/ % 0.48/0.67 definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/ % 0.48/0.67 member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23 \/ % 0.48/0.67 member $X15 (skolemFOFtoCNF_X31 $X15 $X23 $X24) $X24 \/ % 0.48/0.67 member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24 % 0.48/0.67 |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/ % 0.48/0.67 ~be $X15 $X25 $X21 $X26 \/ ~behind $X15 $X26 $X18 \/ ~chevy $X15 $X19 \/ % 0.48/0.67 ~city $X15 $X21 \/ ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ % 0.48/0.67 ~event $X15 $X22 \/ ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/ % 0.48/0.67 ~group $X15 $X23 \/ ~group $X15 $X24 \/ % 0.48/0.67 ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/ % 0.48/0.67 ~jules_forename $X15 $X20 \/ ~lonely $X15 $X21 \/ ~man $X15 $X21 \/ % 0.48/0.67 ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ ~placename $X15 $X20 \/ % 0.48/0.67 ~present $X15 $X22 \/ ~state $X15 $X25 \/ ~street $X15 $X21 \/ % 0.48/0.67 ~two $X15 $X23 \/ ~wheel $X15 $X18 \/ ~white $X15 $X19 \/ % 0.48/0.67 definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/ % 0.48/0.67 member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23 \/ % 0.48/0.67 member $X15 (skolemFOFtoCNF_X32 $X15 $X23 $X24) $X23 \/ % 0.48/0.67 member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24 % 0.48/0.67 |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/ % 0.48/0.67 ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/ % 0.48/0.67 ~behind $X15 $X29 $X18 \/ ~chevy $X15 $X19 \/ ~city $X15 $X21 \/ % 0.48/0.67 ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/ % 0.48/0.67 ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/ % 0.48/0.67 ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/ % 0.48/0.67 ~in $X15 $X22 $X21 \/ ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X17 \/ % 0.48/0.67 ~lonely $X15 $X21 \/ ~man $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ % 0.48/0.67 ~of $X15 $X17 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ % 0.48/0.67 ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ ~placename $X15 $X20 \/ % 0.48/0.67 ~present $X15 $X22 \/ ~state $X15 $X28 \/ ~street $X15 $X21 \/ % 0.48/0.67 ~two $X15 $X23 \/ ~wheel $X15 $X18 \/ ~white $X15 $X19 \/ % 0.48/0.67 definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/ % 0.48/0.67 member $X15 (skolemFOFtoCNF_X31 $X15 $X23 $X24) $X24 \/ % 0.48/0.67 member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24 % 0.48/0.67 |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/ % 0.48/0.67 ~be $X15 $X25 $X21 $X26 \/ % 0.48/0.67 ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/ % 0.48/0.67 ~behind $X15 $X26 $X18 \/ ~chevy $X15 $X19 \/ ~city $X15 $X21 \/ % 0.48/0.67 ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/ % 0.48/0.67 ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/ % 0.48/0.67 ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/ % 0.48/0.67 ~in $X15 $X22 $X21 \/ ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X20 \/ % 0.48/0.67 ~lonely $X15 $X21 \/ ~man $X15 $X21 \/ ~of $X15 $X20 $X21 \/ % 0.48/0.67 ~old $X15 $X19 \/ ~placename $X15 $X20 \/ ~present $X15 $X22 \/ % 0.48/0.67 ~state $X15 $X25 \/ ~state $X15 $X28 \/ ~street $X15 $X21 \/ % 0.48/0.67 ~two $X15 $X23 \/ ~wheel $X15 $X18 \/ ~white $X15 $X19 \/ % 0.48/0.67 definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/ % 0.48/0.67 member $X15 (skolemFOFtoCNF_X31 $X15 $X23 $X24) $X24 \/ % 0.48/0.67 member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24 % 0.48/0.67 |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/ % 0.48/0.67 ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/ % 0.48/0.67 ~behind $X15 $X29 $X18 \/ ~chevy $X15 $X19 \/ % 0.48/0.67 ~city $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~dirty $X15 $X19 \/ % 0.48/0.67 ~down $X15 $X22 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ % 0.48/0.67 ~event $X15 $X22 \/ ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/ % 0.48/0.67 ~group $X15 $X23 \/ ~group $X15 $X24 \/ % 0.48/0.67 ~hollywood_placename $X15 $X20 \/ % 0.48/0.67 ~in $X15 $X22 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ % 0.48/0.67 ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X20 \/ % 0.48/0.67 ~lonely $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ % 0.48/0.67 ~man $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ % 0.48/0.67 ~of $X15 $X20 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~old $X15 $X19 \/ % 0.48/0.67 ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~state $X15 $X28 \/ % 0.48/0.67 ~street $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~two $X15 $X23 \/ % 0.48/0.67 ~wheel $X15 $X18 \/ ~white $X15 $X19 \/ % 0.48/0.67 definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/ % 0.48/0.67 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 $X18 \/ ~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 $X18 \/ ~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 $X21 $X26 \/ % 0.48/0.68 ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/ % 0.48/0.68 ~behind $X15 $X26 $X18 \/ ~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 $X18 \/ ~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 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/ % 0.48/0.68 ~behind $X15 $X29 $X18 \/ ~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 $X18 \/ ~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.53/0.68 |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/ % 0.53/0.68 ~be $X15 $X25 $X21 $X26 \/ ~behind $X15 $X26 $X18 \/ % 0.53/0.68 ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ % 0.53/0.68 ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/ % 0.53/0.68 ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ % 0.53/0.68 ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/ % 0.53/0.68 ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/ % 0.53/0.68 ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/ % 0.53/0.68 ~in $X15 $X22 $X21 \/ ~jules_forename $X15 $X20 \/ ~lonely $X15 $X21 \/ % 0.53/0.68 ~man $X15 $X21 \/ ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ % 0.53/0.68 ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~state $X15 $X25 \/ % 0.53/0.68 ~street $X15 $X21 \/ ~two $X15 $X23 \/ ~wheel $X15 $X18 \/ % 0.53/0.68 ~white $X15 $X19 \/ % 0.53/0.68 definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/ % 0.53/0.68 member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23 \/ % 0.53/0.68 member $X15 (skolemFOFtoCNF_X31 $X15 $X23 $X24) $X24 % 0.53/0.68 |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/ % 0.53/0.68 ~be $X15 $X25 $X21 $X26 \/ ~behind $X15 $X26 $X18 \/ % 0.53/0.68 ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ % 0.53/0.68 ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/ % 0.53/0.68 ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ % 0.53/0.68 ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/ % 0.53/0.68 ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/ % 0.53/0.68 ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/ % 0.53/0.68 ~in $X15 $X22 $X21 \/ ~jules_forename $X15 $X20 \/ ~lonely $X15 $X21 \/ % 0.53/0.68 ~man $X15 $X21 \/ ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ % 0.53/0.68 ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~state $X15 $X25 \/ % 0.53/0.68 ~street $X15 $X21 \/ ~two $X15 $X23 \/ ~wheel $X15 $X18 \/ % 0.53/0.68 ~white $X15 $X19 \/ % 0.53/0.68 definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/ % 0.53/0.68 member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23 \/ % 0.53/0.68 member $X15 (skolemFOFtoCNF_X32 $X15 $X23 $X24) $X23 % 0.53/0.68 |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/ % 0.53/0.68 ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/ % 0.53/0.68 ~behind $X15 $X29 $X18 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ % 0.53/0.68 ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/ % 0.53/0.68 ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ % 0.53/0.68 ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/ % 0.53/0.68 ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/ % 0.53/0.68 ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/ % 0.53/0.68 ~in $X15 $X22 $X21 \/ ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X17 \/ % 0.53/0.68 ~lonely $X15 $X21 \/ ~man $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ % 0.53/0.68 ~of $X15 $X17 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ % 0.53/0.68 ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ ~placename $X15 $X20 \/ % 0.53/0.68 ~present $X15 $X22 \/ ~state $X15 $X28 \/ ~street $X15 $X21 \/ % 0.53/0.68 ~two $X15 $X23 \/ ~wheel $X15 $X18 \/ ~white $X15 $X19 \/ % 0.53/0.68 definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/ % 0.53/0.68 member $X15 (skolemFOFtoCNF_X31 $X15 $X23 $X24) $X24 % 0.53/0.68 |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/ % 0.53/0.68 ~be $X15 $X25 $X21 $X26 \/ % 0.53/0.68 ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/ % 0.53/0.68 ~behind $X15 $X26 $X18 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ % 0.53/0.68 ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/ % 0.53/0.68 ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ % 0.53/0.68 ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/ % 0.53/0.68 ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/ % 0.53/0.68 ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/ % 0.53/0.68 ~in $X15 $X22 $X21 \/ ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X20 \/ % 0.53/0.68 ~lonely $X15 $X21 \/ ~man $X15 $X21 \/ ~of $X15 $X20 $X21 \/ % 0.53/0.68 ~old $X15 $X19 \/ ~placename $X15 $X20 \/ ~present $X15 $X22 \/ % 0.53/0.68 ~state $X15 $X25 \/ ~state $X15 $X28 \/ ~street $X15 $X21 \/ % 0.53/0.68 ~two $X15 $X23 \/ ~wheel $X15 $X18 \/ ~white $X15 $X19 \/ % 0.53/0.68 definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/ % 0.53/0.68 member $X15 (skolemFOFtoCNF_X31 $X15 $X23 $X24) $X24 % 0.53/0.68 |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/ % 0.53/0.68 ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/ % 0.53/0.68 ~behind $X15 $X29 $X18 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ % 0.53/0.68 ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/ % 0.53/0.68 ~city $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ % 0.53/0.68 ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~dirty $X15 $X19 \/ % 0.53/0.68 ~down $X15 $X22 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ % 0.53/0.68 ~event $X15 $X22 \/ ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/ % 0.53/0.68 ~group $X15 $X23 \/ ~group $X15 $X24 \/ % 0.53/0.68 ~hollywood_placename $X15 $X20 \/ % 0.53/0.68 ~in $X15 $X22 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ % 0.53/0.68 ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X20 \/ % 0.53/0.68 ~lonely $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ % 0.53/0.68 ~man $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ % 0.53/0.68 ~of $X15 $X20 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~old $X15 $X19 \/ % 0.53/0.68 ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~state $X15 $X28 \/ % 0.53/0.68 ~street $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~two $X15 $X23 \/ % 0.53/0.68 ~wheel $X15 $X18 \/ ~white $X15 $X19 \/ % 0.53/0.68 definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/ % 0.53/0.68 member $X15 (skolemFOFtoCNF_X31 $X15 $X23 $X24) $X24 % 0.53/0.68 |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/ % 0.53/0.68 ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/ % 0.53/0.68 ~behind $X15 $X29 $X18 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ % 0.53/0.68 ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/ % 0.53/0.68 ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ % 0.53/0.68 ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/ % 0.53/0.68 ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/ % 0.53/0.68 ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/ % 0.53/0.68 ~in $X15 $X22 $X21 \/ ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X17 \/ % 0.53/0.68 ~lonely $X15 $X21 \/ ~man $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ % 0.53/0.68 ~of $X15 $X17 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ % 0.53/0.68 ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ ~placename $X15 $X20 \/ % 0.53/0.68 ~present $X15 $X22 \/ ~state $X15 $X28 \/ ~street $X15 $X21 \/ % 0.53/0.68 ~two $X15 $X23 \/ ~wheel $X15 $X18 \/ ~white $X15 $X19 \/ % 0.53/0.68 definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/ % 0.53/0.68 member $X15 (skolemFOFtoCNF_X32 $X15 $X23 $X24) $X23 % 0.53/0.68 |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/ % 0.53/0.68 ~be $X15 $X25 $X21 $X26 \/ % 0.53/0.68 ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/ % 0.53/0.68 ~behind $X15 $X26 $X18 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ % 0.53/0.68 ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/ % 0.53/0.68 ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ % 0.53/0.68 ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/ % 0.53/0.68 ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/ % 0.53/0.68 ~group $X15 $X24 \/ ~hollywood_placename $X15 $X20 \/ % 0.53/0.68 ~in $X15 $X22 $X21 \/ ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X20 \/ % 0.53/0.68 ~lonely $X15 $X21 \/ ~man $X15 $X21 \/ ~of $X15 $X20 $X21 \/ % 0.53/0.68 ~old $X15 $X19 \/ ~placename $X15 $X20 \/ ~present $X15 $X22 \/ % 0.53/0.68 ~state $X15 $X25 \/ ~state $X15 $X28 \/ ~street $X15 $X21 \/ % 0.53/0.68 ~two $X15 $X23 \/ ~wheel $X15 $X18 \/ ~white $X15 $X19 \/ % 0.53/0.68 definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/ % 0.53/0.68 member $X15 (skolemFOFtoCNF_X32 $X15 $X23 $X24) $X23 % 0.53/0.68 |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ ~barrel $X15 $X22 \/ % 0.53/0.68 ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/ % 0.53/0.68 ~behind $X15 $X29 $X18 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ % 0.53/0.68 ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/ % 0.53/0.68 ~city $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ % 0.53/0.68 ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~dirty $X15 $X19 \/ % 0.53/0.68 ~down $X15 $X22 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ % 0.53/0.68 ~event $X15 $X22 \/ ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/ % 0.53/0.68 ~group $X15 $X23 \/ ~group $X15 $X24 \/ % 0.53/0.68 ~hollywood_placename $X15 $X20 \/ % 0.53/0.68 ~in $X15 $X22 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ % 0.53/0.68 ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X20 \/ % 0.53/0.68 ~lonely $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ % 0.53/0.68 ~man $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ % 0.53/0.68 ~of $X15 $X20 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~old $X15 $X19 \/ % 0.53/0.68 ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~state $X15 $X28 \/ % 0.53/0.68 ~street $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~two $X15 $X23 \/ % 0.53/0.68 ~wheel $X15 $X18 \/ ~white $X15 $X19 \/ % 0.53/0.68 definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/ % 0.53/0.68 member $X15 (skolemFOFtoCNF_X32 $X15 $X23 $X24) $X23 % 0.53/0.68 |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ % 0.53/0.68 ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/ % 0.53/0.68 ~barrel $X15 $X22 \/ ~be $X15 $X25 $X21 $X26 \/ % 0.53/0.68 ~behind $X15 $X26 $X18 \/ ~chevy $X15 $X19 \/ ~city $X15 $X21 \/ % 0.53/0.68 ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/ % 0.53/0.68 ~event $X15 $X33 \/ ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/ % 0.53/0.68 ~group $X15 $X23 \/ ~group $X15 $X24 \/ % 0.53/0.68 ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/ % 0.53/0.68 ~jules_forename $X15 $X20 \/ ~lonely $X15 $X21 \/ ~man $X15 $X21 \/ % 0.53/0.68 ~nonreflexive $X15 $X33 \/ ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ % 0.53/0.68 ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/ % 0.53/0.68 ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/ % 0.53/0.68 ~state $X15 $X25 \/ ~street $X15 $X21 \/ ~two $X15 $X23 \/ % 0.53/0.68 ~wear $X15 $X33 \/ ~wheel $X15 $X18 \/ ~white $X15 $X19 \/ % 0.53/0.68 definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/ % 0.53/0.68 member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23 \/ % 0.53/0.68 member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24 % 0.53/0.68 |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ % 0.53/0.68 ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/ % 0.53/0.68 ~barrel $X15 $X22 \/ % 0.53/0.68 ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/ % 0.53/0.68 ~behind $X15 $X29 $X18 \/ ~chevy $X15 $X19 \/ ~city $X15 $X21 \/ % 0.53/0.68 ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/ % 0.53/0.68 ~event $X15 $X33 \/ ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ % 0.53/0.68 ~group $X15 $X23 \/ ~group $X15 $X24 \/ % 0.53/0.68 ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/ % 0.53/0.68 ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X17 \/ ~lonely $X15 $X21 \/ % 0.53/0.68 ~man $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ % 0.53/0.68 ~nonreflexive $X15 $X33 \/ % 0.53/0.68 ~of $X15 $X17 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ % 0.53/0.68 ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ % 0.53/0.68 ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/ % 0.53/0.68 ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/ % 0.53/0.68 ~state $X15 $X28 \/ ~street $X15 $X21 \/ ~two $X15 $X23 \/ % 0.53/0.68 ~wear $X15 $X33 \/ ~wheel $X15 $X18 \/ ~white $X15 $X19 \/ % 0.53/0.68 definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/ % 0.53/0.68 member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24 % 0.53/0.68 |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ % 0.53/0.68 ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/ % 0.53/0.68 ~barrel $X15 $X22 \/ ~be $X15 $X25 $X21 $X26 \/ % 0.53/0.68 ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/ % 0.53/0.68 ~behind $X15 $X26 $X18 \/ ~chevy $X15 $X19 \/ ~city $X15 $X21 \/ % 0.53/0.68 ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/ % 0.53/0.68 ~event $X15 $X33 \/ ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/ % 0.53/0.68 ~group $X15 $X23 \/ ~group $X15 $X24 \/ % 0.53/0.68 ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/ % 0.53/0.68 ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X20 \/ ~lonely $X15 $X21 \/ % 0.53/0.68 ~man $X15 $X21 \/ ~nonreflexive $X15 $X33 \/ ~of $X15 $X20 $X21 \/ % 0.53/0.68 ~old $X15 $X19 \/ % 0.53/0.68 ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/ % 0.53/0.68 ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/ % 0.53/0.68 ~state $X15 $X25 \/ ~state $X15 $X28 \/ ~street $X15 $X21 \/ % 0.53/0.68 ~two $X15 $X23 \/ ~wear $X15 $X33 \/ ~wheel $X15 $X18 \/ % 0.53/0.68 ~white $X15 $X19 \/ % 0.53/0.68 definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/ % 0.53/0.68 member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24 % 0.53/0.68 |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ % 0.53/0.68 ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/ % 0.53/0.68 ~barrel $X15 $X22 \/ % 0.53/0.68 ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/ % 0.53/0.68 ~behind $X15 $X29 $X18 \/ ~chevy $X15 $X19 \/ % 0.53/0.68 ~city $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~dirty $X15 $X19 \/ % 0.53/0.68 ~down $X15 $X22 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ % 0.53/0.68 ~event $X15 $X22 \/ ~event $X15 $X33 \/ ~forename $X15 $X20 \/ % 0.53/0.68 ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/ ~group $X15 $X24 \/ % 0.53/0.68 ~hollywood_placename $X15 $X20 \/ % 0.53/0.68 ~in $X15 $X22 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ % 0.53/0.68 ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X20 \/ % 0.53/0.68 ~lonely $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ % 0.53/0.68 ~man $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ % 0.53/0.68 ~nonreflexive $X15 $X33 \/ % 0.53/0.68 ~of $X15 $X20 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~old $X15 $X19 \/ % 0.53/0.68 ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/ % 0.53/0.68 ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/ % 0.53/0.68 ~state $X15 $X28 \/ ~street $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ % 0.53/0.68 ~two $X15 $X23 \/ ~wear $X15 $X33 \/ ~wheel $X15 $X18 \/ % 0.53/0.68 ~white $X15 $X19 \/ % 0.53/0.68 definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/ % 0.53/0.68 member $X15 (skolemFOFtoCNF_X34 $X15 $X24) $X24 % 0.53/0.68 |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ % 0.53/0.68 ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/ % 0.53/0.68 ~barrel $X15 $X22 \/ ~be $X15 $X25 $X21 $X26 \/ % 0.53/0.68 ~behind $X15 $X26 $X18 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ % 0.53/0.68 ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/ % 0.53/0.68 ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ % 0.53/0.68 ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/ % 0.53/0.68 ~event $X15 $X33 \/ ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/ % 0.53/0.68 ~group $X15 $X23 \/ ~group $X15 $X24 \/ % 0.53/0.68 ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/ % 0.53/0.68 ~jules_forename $X15 $X20 \/ ~lonely $X15 $X21 \/ ~man $X15 $X21 \/ % 0.53/0.68 ~nonreflexive $X15 $X33 \/ ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ % 0.53/0.68 ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/ % 0.53/0.68 ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/ % 0.53/0.68 ~state $X15 $X25 \/ ~street $X15 $X21 \/ ~two $X15 $X23 \/ % 0.53/0.68 ~wear $X15 $X33 \/ ~wheel $X15 $X18 \/ ~white $X15 $X19 \/ % 0.53/0.68 definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) \/ % 0.53/0.68 member $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X23 % 0.53/0.68 |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ % 0.53/0.68 ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/ % 0.53/0.68 ~barrel $X15 $X22 \/ % 0.53/0.68 ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/ % 0.53/0.68 ~behind $X15 $X29 $X18 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ % 0.53/0.68 ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/ % 0.53/0.68 ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ % 0.53/0.68 ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/ % 0.53/0.68 ~event $X15 $X33 \/ ~forename $X15 $X17 \/ ~frontseat $X15 $X18 \/ % 0.53/0.68 ~group $X15 $X23 \/ ~group $X15 $X24 \/ % 0.53/0.68 ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/ % 0.53/0.68 ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X17 \/ ~lonely $X15 $X21 \/ % 0.53/0.68 ~man $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ % 0.53/0.68 ~nonreflexive $X15 $X33 \/ % 0.53/0.68 ~of $X15 $X17 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ % 0.53/0.68 ~of $X15 $X20 $X21 \/ ~old $X15 $X19 \/ % 0.53/0.68 ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/ % 0.53/0.68 ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/ % 0.53/0.68 ~state $X15 $X28 \/ ~street $X15 $X21 \/ ~two $X15 $X23 \/ % 0.53/0.68 ~wear $X15 $X33 \/ ~wheel $X15 $X18 \/ ~white $X15 $X19 \/ % 0.53/0.68 definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) % 0.53/0.68 |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ % 0.53/0.68 ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/ % 0.53/0.68 ~barrel $X15 $X22 \/ ~be $X15 $X25 $X21 $X26 \/ % 0.53/0.68 ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/ % 0.53/0.68 ~behind $X15 $X26 $X18 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ % 0.53/0.68 ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/ % 0.53/0.68 ~city $X15 $X21 \/ ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ % 0.53/0.68 ~dirty $X15 $X19 \/ ~down $X15 $X22 $X21 \/ ~event $X15 $X22 \/ % 0.53/0.68 ~event $X15 $X33 \/ ~forename $X15 $X20 \/ ~frontseat $X15 $X18 \/ % 0.53/0.68 ~group $X15 $X23 \/ ~group $X15 $X24 \/ % 0.53/0.68 ~hollywood_placename $X15 $X20 \/ ~in $X15 $X22 $X21 \/ % 0.53/0.68 ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X20 \/ ~lonely $X15 $X21 \/ % 0.53/0.68 ~man $X15 $X21 \/ ~nonreflexive $X15 $X33 \/ ~of $X15 $X20 $X21 \/ % 0.53/0.68 ~old $X15 $X19 \/ % 0.53/0.68 ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/ % 0.53/0.68 ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/ % 0.53/0.68 ~state $X15 $X25 \/ ~state $X15 $X28 \/ ~street $X15 $X21 \/ % 0.53/0.68 ~two $X15 $X23 \/ ~wear $X15 $X33 \/ ~wheel $X15 $X18 \/ % 0.53/0.68 ~white $X15 $X19 \/ % 0.53/0.68 definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) % 0.53/0.68 |- ~actual_world $X15 \/ ~agent $X15 $X22 $X19 \/ % 0.53/0.68 ~agent $X15 $X33 (skolemFOFtoCNF_X32 $X15 $X23 $X24) \/ % 0.53/0.68 ~barrel $X15 $X22 \/ % 0.53/0.68 ~be $X15 $X28 (skolemFOFtoCNF_X27 $X15 $X18 $X23) $X29 \/ % 0.53/0.68 ~behind $X15 $X29 $X18 \/ ~black $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ % 0.53/0.68 ~cheap $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~chevy $X15 $X19 \/ % 0.53/0.68 ~city $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ % 0.53/0.68 ~coat $X15 (skolemFOFtoCNF_X34 $X15 $X24) \/ ~dirty $X15 $X19 \/ % 0.53/0.68 ~down $X15 $X22 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ % 0.53/0.68 ~event $X15 $X22 \/ ~event $X15 $X33 \/ ~forename $X15 $X20 \/ % 0.53/0.68 ~frontseat $X15 $X18 \/ ~group $X15 $X23 \/ ~group $X15 $X24 \/ % 0.53/0.68 ~hollywood_placename $X15 $X20 \/ % 0.53/0.68 ~in $X15 $X22 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ % 0.53/0.68 ~in $X15 $X29 $X18 \/ ~jules_forename $X15 $X20 \/ % 0.53/0.68 ~lonely $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ % 0.53/0.68 ~man $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ % 0.53/0.68 ~nonreflexive $X15 $X33 \/ % 0.53/0.68 ~of $X15 $X20 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ ~old $X15 $X19 \/ % 0.53/0.68 ~patient $X15 $X33 (skolemFOFtoCNF_X31 $X15 $X23 $X24) \/ % 0.53/0.68 ~placename $X15 $X20 \/ ~present $X15 $X22 \/ ~present $X15 $X33 \/ % 0.53/0.68 ~state $X15 $X28 \/ ~street $X15 (skolemFOFtoCNF_X27 $X15 $X18 $X23) \/ % 0.53/0.68 ~two $X15 $X23 \/ ~wear $X15 $X33 \/ ~wheel $X15 $X18 \/ % 0.53/0.68 ~white $X15 $X19 \/ % 0.53/0.68 definitionFOFtoCNF_0 $X15 $X23 (skolemFOFtoCNF_X30 $X15 $X23) % 0.53/0.68 |- ~agent skolemFOFtoCNF_U $_45 $_43 \/ ~barrel skolemFOFtoCNF_U $_45 \/ % 0.53/0.68 ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_42 \/ % 0.53/0.68 ~chevy skolemFOFtoCNF_U $_43 \/ % 0.53/0.68 ~city skolemFOFtoCNF_U skolemFOFtoCNF_V \/ % 0.53/0.68 ~dirty skolemFOFtoCNF_U $_43 \/ % 0.53/0.68 ~down skolemFOFtoCNF_U $_45 skolemFOFtoCNF_V \/ % 0.53/0.68 ~event skolemFOFtoCNF_U $_45 \/ ~frontseat skolemFOFtoCNF_U $_42 \/ % 0.53/0.68 ~group skolemFOFtoCNF_U $_46 \/ ~group skolemFOFtoCNF_U $_47 \/ % 0.53/0.68 ~hollywood_placename skolemFOFtoCNF_U skolemFOFtoCNF_W \/ % 0.53/0.68 ~in skolemFOFtoCNF_U $_45 skolemFOFtoCNF_V \/ % 0.53/0.68 ~lonely skolemFOFtoCNF_U skolemFOFtoCNF_V \/ % 0.53/0.68 ~old skolemFOFtoCNF_U $_43 \/ % 0.53/0.68 ~placename skolemFOFtoCNF_U skolemFOFtoCNF_W \/ % 0.53/0.68 ~present skolemFOFtoCNF_U $_45 \/ % 0.53/0.68 ~street skolemFOFtoCNF_U skolemFOFtoCNF_V \/ % 0.53/0.68 ~two skolemFOFtoCNF_U $_46 \/ ~wheel skolemFOFtoCNF_U $_42 \/ % 0.53/0.68 ~white skolemFOFtoCNF_U $_43 \/ % 0.53/0.68 definitionFOFtoCNF_0 skolemFOFtoCNF_U $_46 % 0.53/0.68 (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_46) \/ % 0.53/0.68 member skolemFOFtoCNF_U (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_42 $_46) % 0.53/0.68 $_46 \/ % 0.53/0.68 member skolemFOFtoCNF_U (skolemFOFtoCNF_X31 skolemFOFtoCNF_U $_46 $_47) % 0.53/0.68 $_47 \/ % 0.53/0.68 member skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_47) $_47 % 0.53/0.68 |- ~agent skolemFOFtoCNF_U $_66 $_64 \/ ~barrel skolemFOFtoCNF_U $_66 \/ % 0.53/0.68 ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_63 \/ % 0.53/0.68 ~chevy skolemFOFtoCNF_U $_64 \/ % 0.53/0.68 ~city skolemFOFtoCNF_U skolemFOFtoCNF_V \/ % 0.53/0.68 ~dirty skolemFOFtoCNF_U $_64 \/ % 0.53/0.68 ~down skolemFOFtoCNF_U $_66 skolemFOFtoCNF_V \/ % 0.53/0.68 ~event skolemFOFtoCNF_U $_66 \/ ~frontseat skolemFOFtoCNF_U $_63 \/ % 0.53/0.68 ~group skolemFOFtoCNF_U $_67 \/ ~group skolemFOFtoCNF_U $_68 \/ % 0.53/0.68 ~hollywood_placename skolemFOFtoCNF_U skolemFOFtoCNF_W \/ % 0.53/0.68 ~in skolemFOFtoCNF_U $_66 skolemFOFtoCNF_V \/ % 0.53/0.68 ~lonely skolemFOFtoCNF_U skolemFOFtoCNF_V \/ % 0.53/0.68 ~old skolemFOFtoCNF_U $_64 \/ % 0.53/0.68 ~placename skolemFOFtoCNF_U skolemFOFtoCNF_W \/ % 0.53/0.68 ~present skolemFOFtoCNF_U $_66 \/ % 0.53/0.68 ~street skolemFOFtoCNF_U skolemFOFtoCNF_V \/ % 0.53/0.68 ~two skolemFOFtoCNF_U $_67 \/ ~wheel skolemFOFtoCNF_U $_63 \/ % 0.53/0.68 ~white skolemFOFtoCNF_U $_64 \/ % 0.53/0.68 definitionFOFtoCNF_0 skolemFOFtoCNF_U $_67 % 0.53/0.68 (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_67) \/ % 0.53/0.68 member skolemFOFtoCNF_U (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_63 $_67) % 0.53/0.68 $_67 \/ % 0.53/0.68 member skolemFOFtoCNF_U (skolemFOFtoCNF_X32 skolemFOFtoCNF_U $_67 $_68) % 0.53/0.68 $_67 \/ % 0.53/0.68 member skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_68) $_68 % 0.53/0.68 |- ~agent skolemFOFtoCNF_U $_97 $_94 \/ ~barrel skolemFOFtoCNF_U $_97 \/ % 0.53/0.68 ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_93 \/ % 0.53/0.68 ~black skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_99) \/ % 0.53/0.68 ~cheap skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_99) \/ % 0.53/0.68 ~chevy skolemFOFtoCNF_U $_94 \/ % 0.53/0.68 ~city skolemFOFtoCNF_U skolemFOFtoCNF_V \/ % 0.53/0.68 ~coat skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_99) \/ % 0.53/0.68 ~dirty skolemFOFtoCNF_U $_94 \/ % 0.53/0.68 ~down skolemFOFtoCNF_U $_97 skolemFOFtoCNF_V \/ % 0.53/0.68 ~event skolemFOFtoCNF_U $_97 \/ ~forename skolemFOFtoCNF_U $_95 \/ % 0.53/0.68 ~frontseat skolemFOFtoCNF_U $_93 \/ ~group skolemFOFtoCNF_U $_98 \/ % 0.53/0.68 ~group skolemFOFtoCNF_U $_99 \/ % 0.53/0.68 ~hollywood_placename skolemFOFtoCNF_U $_95 \/ % 0.53/0.68 ~in skolemFOFtoCNF_U $_97 skolemFOFtoCNF_V \/ % 0.53/0.68 ~jules_forename skolemFOFtoCNF_U $_95 \/ % 0.53/0.68 ~lonely skolemFOFtoCNF_U skolemFOFtoCNF_V \/ % 0.53/0.68 ~of skolemFOFtoCNF_U $_95 skolemFOFtoCNF_V \/ % 0.53/0.68 ~old skolemFOFtoCNF_U $_94 \/ ~placename skolemFOFtoCNF_U $_95 \/ % 0.53/0.68 ~present skolemFOFtoCNF_U $_97 \/ % 0.53/0.68 ~street skolemFOFtoCNF_U skolemFOFtoCNF_V \/ % 0.53/0.68 ~two skolemFOFtoCNF_U $_98 \/ ~wheel skolemFOFtoCNF_U $_93 \/ % 0.53/0.68 ~white skolemFOFtoCNF_U $_94 \/ % 0.53/0.68 definitionFOFtoCNF_0 skolemFOFtoCNF_U $_98 % 0.53/0.68 (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_98) \/ % 0.53/0.68 member skolemFOFtoCNF_U (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_93 $_98) % 0.53/0.68 $_98 \/ % 0.53/0.68 member skolemFOFtoCNF_U (skolemFOFtoCNF_X31 skolemFOFtoCNF_U $_98 $_99) % 0.53/0.68 $_99 % 0.53/0.68 |- ~agent skolemFOFtoCNF_U $_113 $_110 \/ ~barrel skolemFOFtoCNF_U $_113 \/ % 0.53/0.68 ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_109 \/ % 0.53/0.68 ~black skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_115) \/ % 0.53/0.68 ~cheap skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_115) \/ % 0.53/0.68 ~chevy skolemFOFtoCNF_U $_110 \/ % 0.53/0.68 ~city skolemFOFtoCNF_U skolemFOFtoCNF_V \/ % 0.53/0.68 ~coat skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_115) \/ % 0.53/0.68 ~dirty skolemFOFtoCNF_U $_110 \/ % 0.53/0.68 ~down skolemFOFtoCNF_U $_113 skolemFOFtoCNF_V \/ % 0.53/0.68 ~event skolemFOFtoCNF_U $_113 \/ ~forename skolemFOFtoCNF_U $_111 \/ % 0.53/0.68 ~frontseat skolemFOFtoCNF_U $_109 \/ ~group skolemFOFtoCNF_U $_114 \/ % 0.53/0.68 ~group skolemFOFtoCNF_U $_115 \/ % 0.53/0.68 ~hollywood_placename skolemFOFtoCNF_U $_111 \/ % 0.53/0.68 ~in skolemFOFtoCNF_U $_113 skolemFOFtoCNF_V \/ % 0.53/0.68 ~jules_forename skolemFOFtoCNF_U $_111 \/ % 0.53/0.68 ~lonely skolemFOFtoCNF_U skolemFOFtoCNF_V \/ % 0.53/0.68 ~of skolemFOFtoCNF_U $_111 skolemFOFtoCNF_V \/ % 0.53/0.68 ~old skolemFOFtoCNF_U $_110 \/ ~placename skolemFOFtoCNF_U $_111 \/ % 0.53/0.68 ~present skolemFOFtoCNF_U $_113 \/ % 0.53/0.68 ~street skolemFOFtoCNF_U skolemFOFtoCNF_V \/ % 0.53/0.68 ~two skolemFOFtoCNF_U $_114 \/ ~wheel skolemFOFtoCNF_U $_109 \/ % 0.53/0.68 ~white skolemFOFtoCNF_U $_110 \/ % 0.53/0.68 definitionFOFtoCNF_0 skolemFOFtoCNF_U $_114 % 0.53/0.68 (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_114) \/ % 0.53/0.68 member skolemFOFtoCNF_U % 0.53/0.68 (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_109 $_114) $_114 \/ % 0.53/0.68 member skolemFOFtoCNF_U % 0.53/0.68 (skolemFOFtoCNF_X32 skolemFOFtoCNF_U $_114 $_115) $_114 % 0.53/0.68 |- ~agent skolemFOFtoCNF_U $_181 $_178 \/ ~barrel skolemFOFtoCNF_U $_181 \/ % 0.53/0.68 ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_177 \/ % 0.53/0.68 ~chevy skolemFOFtoCNF_U $_178 \/ ~city skolemFOFtoCNF_U $_180 \/ % 0.53/0.68 ~dirty skolemFOFtoCNF_U $_178 \/ ~down skolemFOFtoCNF_U $_181 $_180 \/ % 0.53/0.68 ~event skolemFOFtoCNF_U $_181 \/ ~frontseat skolemFOFtoCNF_U $_177 \/ % 0.53/0.68 ~group skolemFOFtoCNF_U $_182 \/ ~group skolemFOFtoCNF_U $_183 \/ % 0.53/0.68 ~hollywood_placename skolemFOFtoCNF_U $_179 \/ % 0.53/0.68 ~in skolemFOFtoCNF_U $_181 $_180 \/ ~lonely skolemFOFtoCNF_U $_180 \/ % 0.53/0.68 ~of skolemFOFtoCNF_U $_179 $_180 \/ ~old skolemFOFtoCNF_U $_178 \/ % 0.53/0.68 ~placename skolemFOFtoCNF_U $_179 \/ ~present skolemFOFtoCNF_U $_181 \/ % 0.53/0.68 ~street skolemFOFtoCNF_U $_180 \/ ~two skolemFOFtoCNF_U $_182 \/ % 0.53/0.68 ~wheel skolemFOFtoCNF_U $_177 \/ ~white skolemFOFtoCNF_U $_178 \/ % 0.53/0.68 definitionFOFtoCNF_0 skolemFOFtoCNF_U $_182 % 0.53/0.68 (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_182) \/ % 0.53/0.68 member skolemFOFtoCNF_U % 0.53/0.68 (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_177 $_182) $_182 \/ % 0.53/0.68 member skolemFOFtoCNF_U % 0.53/0.68 (skolemFOFtoCNF_X31 skolemFOFtoCNF_U $_182 $_183) $_183 \/ % 0.53/0.68 member skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_183) % 0.53/0.68 $_183 % 0.53/0.69 |- ~agent skolemFOFtoCNF_U $_187 $_186 \/ ~barrel skolemFOFtoCNF_U $_187 \/ % 0.53/0.69 ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_185 \/ % 0.53/0.69 ~chevy skolemFOFtoCNF_U $_186 \/ ~dirty skolemFOFtoCNF_U $_186 \/ % 0.53/0.69 ~down skolemFOFtoCNF_U $_187 skolemFOFtoCNF_X1 \/ % 0.53/0.69 ~event skolemFOFtoCNF_U $_187 \/ ~frontseat skolemFOFtoCNF_U $_185 \/ % 0.53/0.69 ~group skolemFOFtoCNF_U $_188 \/ ~group skolemFOFtoCNF_U $_189 \/ % 0.53/0.69 ~in skolemFOFtoCNF_U $_187 skolemFOFtoCNF_X1 \/ % 0.53/0.69 ~old skolemFOFtoCNF_U $_186 \/ ~present skolemFOFtoCNF_U $_187 \/ % 0.53/0.69 ~two skolemFOFtoCNF_U $_188 \/ ~wheel skolemFOFtoCNF_U $_185 \/ % 0.53/0.69 ~white skolemFOFtoCNF_U $_186 \/ % 0.53/0.69 definitionFOFtoCNF_0 skolemFOFtoCNF_U $_188 % 0.53/0.69 (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_188) \/ % 0.53/0.69 member skolemFOFtoCNF_U % 0.53/0.69 (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_185 $_188) $_188 \/ % 0.53/0.69 member skolemFOFtoCNF_U % 0.53/0.69 (skolemFOFtoCNF_X31 skolemFOFtoCNF_U $_188 $_189) $_189 \/ % 0.53/0.69 member skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_189) % 0.53/0.69 $_189 % 0.53/0.69 |- ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X2 $_191 \/ % 0.53/0.69 ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_190 \/ % 0.53/0.69 ~chevy skolemFOFtoCNF_U $_191 \/ ~dirty skolemFOFtoCNF_U $_191 \/ % 0.53/0.69 ~frontseat skolemFOFtoCNF_U $_190 \/ ~group skolemFOFtoCNF_U $_193 \/ % 0.53/0.69 ~group skolemFOFtoCNF_U $_194 \/ ~old skolemFOFtoCNF_U $_191 \/ % 0.53/0.69 ~two skolemFOFtoCNF_U $_193 \/ ~wheel skolemFOFtoCNF_U $_190 \/ % 0.53/0.69 ~white skolemFOFtoCNF_U $_191 \/ % 0.53/0.69 definitionFOFtoCNF_0 skolemFOFtoCNF_U $_193 % 0.53/0.69 (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_193) \/ % 0.53/0.69 member skolemFOFtoCNF_U % 0.53/0.69 (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_190 $_193) $_193 \/ % 0.53/0.69 member skolemFOFtoCNF_U % 0.53/0.69 (skolemFOFtoCNF_X31 skolemFOFtoCNF_U $_193 $_194) $_194 \/ % 0.53/0.69 member skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_194) % 0.53/0.69 $_194 % 0.53/0.69 |- ~frontseat skolemFOFtoCNF_U skolemFOFtoCNF_X6 \/ % 0.53/0.69 ~group skolemFOFtoCNF_U $_200 \/ ~group skolemFOFtoCNF_U $_201 \/ % 0.53/0.69 ~two skolemFOFtoCNF_U $_200 \/ % 0.53/0.69 definitionFOFtoCNF_0 skolemFOFtoCNF_U $_200 % 0.53/0.69 (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_200) \/ % 0.53/0.69 member skolemFOFtoCNF_U % 0.53/0.69 (skolemFOFtoCNF_X27 skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_200) $_200 \/ % 0.53/0.69 member skolemFOFtoCNF_U % 0.53/0.69 (skolemFOFtoCNF_X31 skolemFOFtoCNF_U $_200 $_201) $_201 \/ % 0.53/0.69 member skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_201) % 0.53/0.69 $_201 % 0.53/0.69 |- ~frontseat skolemFOFtoCNF_U skolemFOFtoCNF_X6 \/ % 0.53/0.69 ~group skolemFOFtoCNF_U $_203 \/ % 0.53/0.69 definitionFOFtoCNF_0 skolemFOFtoCNF_U skolemFOFtoCNF_X3 % 0.53/0.69 (skolemFOFtoCNF_X30 skolemFOFtoCNF_U skolemFOFtoCNF_X3) \/ % 0.53/0.69 member skolemFOFtoCNF_U % 0.53/0.69 (skolemFOFtoCNF_X27 skolemFOFtoCNF_U skolemFOFtoCNF_X6 % 0.53/0.69 skolemFOFtoCNF_X3) skolemFOFtoCNF_X3 \/ % 0.53/0.69 member skolemFOFtoCNF_U % 0.53/0.69 (skolemFOFtoCNF_X31 skolemFOFtoCNF_U skolemFOFtoCNF_X3 $_203) $_203 \/ % 0.53/0.69 member skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_203) % 0.53/0.69 $_203 % 0.53/0.69 |- ~frontseat skolemFOFtoCNF_U skolemFOFtoCNF_X6 \/ % 0.53/0.69 definitionFOFtoCNF_0 skolemFOFtoCNF_U skolemFOFtoCNF_X3 % 0.53/0.69 (skolemFOFtoCNF_X30 skolemFOFtoCNF_U skolemFOFtoCNF_X3) \/ % 0.53/0.69 member skolemFOFtoCNF_U % 0.53/0.69 (skolemFOFtoCNF_X27 skolemFOFtoCNF_U skolemFOFtoCNF_X6 % 0.53/0.69 skolemFOFtoCNF_X3) skolemFOFtoCNF_X3 \/ % 0.53/0.69 member skolemFOFtoCNF_U % 0.53/0.69 (skolemFOFtoCNF_X31 skolemFOFtoCNF_U skolemFOFtoCNF_X3 % 0.53/0.69 skolemFOFtoCNF_X3) skolemFOFtoCNF_X3 \/ % 0.53/0.69 member skolemFOFtoCNF_U % 0.53/0.69 (skolemFOFtoCNF_X34 skolemFOFtoCNF_U skolemFOFtoCNF_X3) % 0.53/0.69 skolemFOFtoCNF_X3 % 0.53/0.69 |- ~frontseat skolemFOFtoCNF_U skolemFOFtoCNF_X6 \/ % 0.53/0.69 definitionFOFtoCNF_0 skolemFOFtoCNF_U skolemFOFtoCNF_X3 % 0.53/0.69 (skolemFOFtoCNF_X30 skolemFOFtoCNF_U skolemFOFtoCNF_X3) \/ % 0.53/0.69 member skolemFOFtoCNF_U % 0.53/0.69 (skolemFOFtoCNF_X27 skolemFOFtoCNF_U skolemFOFtoCNF_X6 % 0.53/0.69 skolemFOFtoCNF_X3) skolemFOFtoCNF_X3 \/ % 0.53/0.69 member skolemFOFtoCNF_U % 0.53/0.69 (skolemFOFtoCNF_X31 skolemFOFtoCNF_U skolemFOFtoCNF_X3 % 0.53/0.69 skolemFOFtoCNF_X4) skolemFOFtoCNF_X4 \/ % 0.53/0.69 member skolemFOFtoCNF_U % 0.53/0.69 (skolemFOFtoCNF_X34 skolemFOFtoCNF_U skolemFOFtoCNF_X4) % 0.53/0.69 skolemFOFtoCNF_X4 % 0.53/0.69 |- ~agent skolemFOFtoCNF_U $_229 $_226 \/ ~barrel skolemFOFtoCNF_U $_229 \/ % 0.53/0.69 ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_225 \/ % 0.53/0.69 ~chevy skolemFOFtoCNF_U $_226 \/ ~city skolemFOFtoCNF_U $_228 \/ % 0.53/0.69 ~dirty skolemFOFtoCNF_U $_226 \/ ~down skolemFOFtoCNF_U $_229 $_228 \/ % 0.53/0.69 ~event skolemFOFtoCNF_U $_229 \/ ~frontseat skolemFOFtoCNF_U $_225 \/ % 0.53/0.69 ~group skolemFOFtoCNF_U $_230 \/ ~group skolemFOFtoCNF_U $_231 \/ % 0.53/0.69 ~hollywood_placename skolemFOFtoCNF_U $_227 \/ % 0.53/0.69 ~in skolemFOFtoCNF_U $_229 $_228 \/ ~lonely skolemFOFtoCNF_U $_228 \/ % 0.53/0.69 ~of skolemFOFtoCNF_U $_227 $_228 \/ ~old skolemFOFtoCNF_U $_226 \/ % 0.53/0.69 ~placename skolemFOFtoCNF_U $_227 \/ ~present skolemFOFtoCNF_U $_229 \/ % 0.53/0.69 ~street skolemFOFtoCNF_U $_228 \/ ~two skolemFOFtoCNF_U $_230 \/ % 0.53/0.69 ~wheel skolemFOFtoCNF_U $_225 \/ ~white skolemFOFtoCNF_U $_226 \/ % 0.53/0.69 definitionFOFtoCNF_0 skolemFOFtoCNF_U $_230 % 0.53/0.69 (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_230) \/ % 0.53/0.69 member skolemFOFtoCNF_U % 0.53/0.69 (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_225 $_230) $_230 \/ % 0.53/0.69 member skolemFOFtoCNF_U % 0.53/0.69 (skolemFOFtoCNF_X32 skolemFOFtoCNF_U $_230 $_231) $_230 \/ % 0.53/0.69 member skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_231) % 0.53/0.69 $_231 % 0.53/0.69 |- ~agent skolemFOFtoCNF_U $_235 $_234 \/ ~barrel skolemFOFtoCNF_U $_235 \/ % 0.53/0.69 ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_233 \/ % 0.53/0.69 ~chevy skolemFOFtoCNF_U $_234 \/ ~dirty skolemFOFtoCNF_U $_234 \/ % 0.53/0.69 ~down skolemFOFtoCNF_U $_235 skolemFOFtoCNF_X1 \/ % 0.53/0.69 ~event skolemFOFtoCNF_U $_235 \/ ~frontseat skolemFOFtoCNF_U $_233 \/ % 0.53/0.69 ~group skolemFOFtoCNF_U $_236 \/ ~group skolemFOFtoCNF_U $_237 \/ % 0.53/0.69 ~in skolemFOFtoCNF_U $_235 skolemFOFtoCNF_X1 \/ % 0.53/0.69 ~old skolemFOFtoCNF_U $_234 \/ ~present skolemFOFtoCNF_U $_235 \/ % 0.53/0.69 ~two skolemFOFtoCNF_U $_236 \/ ~wheel skolemFOFtoCNF_U $_233 \/ % 0.53/0.69 ~white skolemFOFtoCNF_U $_234 \/ % 0.53/0.69 definitionFOFtoCNF_0 skolemFOFtoCNF_U $_236 % 0.53/0.69 (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_236) \/ % 0.53/0.69 member skolemFOFtoCNF_U % 0.53/0.69 (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_233 $_236) $_236 \/ % 0.53/0.69 member skolemFOFtoCNF_U % 0.53/0.69 (skolemFOFtoCNF_X32 skolemFOFtoCNF_U $_236 $_237) $_236 \/ % 0.53/0.69 member skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_237) % 0.53/0.69 $_237 % 0.53/0.69 |- ~agent skolemFOFtoCNF_U skolemFOFtoCNF_X2 $_239 \/ % 0.53/0.69 ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_238 \/ % 0.53/0.69 ~chevy skolemFOFtoCNF_U $_239 \/ ~dirty skolemFOFtoCNF_U $_239 \/ % 0.53/0.69 ~frontseat skolemFOFtoCNF_U $_238 \/ ~group skolemFOFtoCNF_U $_241 \/ % 0.53/0.69 ~group skolemFOFtoCNF_U $_242 \/ ~old skolemFOFtoCNF_U $_239 \/ % 0.53/0.69 ~two skolemFOFtoCNF_U $_241 \/ ~wheel skolemFOFtoCNF_U $_238 \/ % 0.53/0.69 ~white skolemFOFtoCNF_U $_239 \/ % 0.53/0.69 definitionFOFtoCNF_0 skolemFOFtoCNF_U $_241 % 0.53/0.69 (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_241) \/ % 0.53/0.69 member skolemFOFtoCNF_U % 0.53/0.69 (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_238 $_241) $_241 \/ % 0.53/0.69 member skolemFOFtoCNF_U % 0.53/0.69 (skolemFOFtoCNF_X32 skolemFOFtoCNF_U $_241 $_242) $_241 \/ % 0.53/0.69 member skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_242) % 0.53/0.69 $_242 % 0.53/0.69 |- ~frontseat skolemFOFtoCNF_U skolemFOFtoCNF_X6 \/ % 0.53/0.69 ~group skolemFOFtoCNF_U $_248 \/ ~group skolemFOFtoCNF_U $_249 \/ % 0.53/0.69 ~two skolemFOFtoCNF_U $_248 \/ % 0.53/0.69 definitionFOFtoCNF_0 skolemFOFtoCNF_U $_248 % 0.53/0.69 (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_248) \/ % 0.53/0.69 member skolemFOFtoCNF_U % 0.53/0.69 (skolemFOFtoCNF_X27 skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_248) $_248 \/ % 0.53/0.69 member skolemFOFtoCNF_U % 0.53/0.69 (skolemFOFtoCNF_X32 skolemFOFtoCNF_U $_248 $_249) $_248 \/ % 0.53/0.69 member skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_249) % 0.53/0.69 $_249 % 0.53/0.69 |- ~frontseat skolemFOFtoCNF_U skolemFOFtoCNF_X6 \/ % 0.53/0.69 ~group skolemFOFtoCNF_U $_251 \/ % 0.53/0.69 definitionFOFtoCNF_0 skolemFOFtoCNF_U skolemFOFtoCNF_X3 % 0.53/0.69 (skolemFOFtoCNF_X30 skolemFOFtoCNF_U skolemFOFtoCNF_X3) \/ % 0.53/0.69 member skolemFOFtoCNF_U % 0.53/0.69 (skolemFOFtoCNF_X27 skolemFOFtoCNF_U skolemFOFtoCNF_X6 % 0.53/0.69 skolemFOFtoCNF_X3) skolemFOFtoCNF_X3 \/ % 0.53/0.69 member skolemFOFtoCNF_U % 0.53/0.69 (skolemFOFtoCNF_X32 skolemFOFtoCNF_U skolemFOFtoCNF_X3 $_251) % 0.53/0.69 skolemFOFtoCNF_X3 \/ % 0.53/0.69 member skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_251) % 0.53/0.69 $_251 % 0.53/0.69 |- ~frontseat skolemFOFtoCNF_U skolemFOFtoCNF_X6 \/ % 0.53/0.69 definitionFOFtoCNF_0 skolemFOFtoCNF_U skolemFOFtoCNF_X3 % 0.53/0.69 (skolemFOFtoCNF_X30 skolemFOFtoCNF_U skolemFOFtoCNF_X3) \/ % 0.53/0.69 member skolemFOFtoCNF_U % 0.53/0.69 (skolemFOFtoCNF_X27 skolemFOFtoCNF_U skolemFOFtoCNF_X6 % 0.53/0.69 skolemFOFtoCNF_X3) skolemFOFtoCNF_X3 \/ % 0.53/0.69 member skolemFOFtoCNF_U % 0.53/0.69 (skolemFOFtoCNF_X32 skolemFOFtoCNF_U skolemFOFtoCNF_X3 % 0.53/0.69 skolemFOFtoCNF_X3) skolemFOFtoCNF_X3 \/ % 0.53/0.69 member skolemFOFtoCNF_U % 0.53/0.69 (skolemFOFtoCNF_X34 skolemFOFtoCNF_U skolemFOFtoCNF_X3) % 0.53/0.69 skolemFOFtoCNF_X3 % 0.53/0.69 |- ~frontseat skolemFOFtoCNF_U skolemFOFtoCNF_X6 \/ % 0.53/0.69 definitionFOFtoCNF_0 skolemFOFtoCNF_U skolemFOFtoCNF_X3 % 0.53/0.69 (skolemFOFtoCNF_X30 skolemFOFtoCNF_U skolemFOFtoCNF_X3) \/ % 0.53/0.69 member skolemFOFtoCNF_U % 0.53/0.69 (skolemFOFtoCNF_X27 skolemFOFtoCNF_U skolemFOFtoCNF_X6 % 0.53/0.69 skolemFOFtoCNF_X3) skolemFOFtoCNF_X3 \/ % 0.53/0.69 member skolemFOFtoCNF_U % 0.53/0.69 (skolemFOFtoCNF_X32 skolemFOFtoCNF_U skolemFOFtoCNF_X3 % 0.53/0.69 skolemFOFtoCNF_X4) skolemFOFtoCNF_X3 \/ % 0.53/0.69 member skolemFOFtoCNF_U % 0.53/0.69 (skolemFOFtoCNF_X34 skolemFOFtoCNF_U skolemFOFtoCNF_X4) % 0.53/0.69 skolemFOFtoCNF_X4 % 0.53/0.69 |- ~agent skolemFOFtoCNF_U $_313 $_310 \/ ~barrel skolemFOFtoCNF_U $_313 \/ % 0.53/0.69 ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_309 \/ % 0.53/0.69 ~black skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_315) \/ % 0.53/0.69 ~cheap skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_315) \/ % 0.53/0.69 ~chevy skolemFOFtoCNF_U $_310 \/ ~city skolemFOFtoCNF_U $_312 \/ % 0.53/0.69 ~coat skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_315) \/ % 0.53/0.69 ~dirty skolemFOFtoCNF_U $_310 \/ ~down skolemFOFtoCNF_U $_313 $_312 \/ % 0.53/0.69 ~event skolemFOFtoCNF_U $_313 \/ ~forename skolemFOFtoCNF_U $_308 \/ % 0.53/0.69 ~frontseat skolemFOFtoCNF_U $_309 \/ ~group skolemFOFtoCNF_U $_314 \/ % 0.53/0.69 ~group skolemFOFtoCNF_U $_315 \/ % 0.53/0.69 ~hollywood_placename skolemFOFtoCNF_U $_311 \/ % 0.53/0.69 ~in skolemFOFtoCNF_U $_313 $_312 \/ % 0.53/0.69 ~jules_forename skolemFOFtoCNF_U $_308 \/ % 0.53/0.69 ~lonely skolemFOFtoCNF_U $_312 \/ % 0.53/0.69 ~of skolemFOFtoCNF_U $_308 skolemFOFtoCNF_V \/ % 0.53/0.69 ~of skolemFOFtoCNF_U $_311 $_312 \/ ~old skolemFOFtoCNF_U $_310 \/ % 0.53/0.69 ~placename skolemFOFtoCNF_U $_311 \/ ~present skolemFOFtoCNF_U $_313 \/ % 0.53/0.69 ~street skolemFOFtoCNF_U $_312 \/ ~two skolemFOFtoCNF_U $_314 \/ % 0.53/0.69 ~wheel skolemFOFtoCNF_U $_309 \/ ~white skolemFOFtoCNF_U $_310 \/ % 0.53/0.69 definitionFOFtoCNF_0 skolemFOFtoCNF_U $_314 % 0.53/0.69 (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_314) \/ % 0.53/0.69 member skolemFOFtoCNF_U % 0.53/0.69 (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_309 $_314) $_314 \/ % 0.53/0.69 member skolemFOFtoCNF_U % 0.53/0.69 (skolemFOFtoCNF_X32 skolemFOFtoCNF_U $_314 $_315) $_314 % 0.53/0.69 |- ~agent skolemFOFtoCNF_U $_333 $_330 \/ ~barrel skolemFOFtoCNF_U $_333 \/ % 0.53/0.69 ~behind skolemFOFtoCNF_U skolemFOFtoCNF_X6 $_329 \/ % 0.53/0.69 ~black skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_335) \/ % 0.53/0.69 ~cheap skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_335) \/ % 0.53/0.69 ~chevy skolemFOFtoCNF_U $_330 \/ ~city skolemFOFtoCNF_U $_332 \/ % 0.53/0.69 ~coat skolemFOFtoCNF_U (skolemFOFtoCNF_X34 skolemFOFtoCNF_U $_335) \/ % 0.53/0.69 ~dirty skolemFOFtoCNF_U $_330 \/ ~down skolemFOFtoCNF_U $_333 $_332 \/ % 0.53/0.69 ~event skolemFOFtoCNF_U $_333 \/ ~forename skolemFOFtoCNF_U $_328 \/ % 0.53/0.69 ~frontseat skolemFOFtoCNF_U $_329 \/ ~group skolemFOFtoCNF_U $_334 \/ % 0.53/0.69 ~group skolemFOFtoCNF_U $_335 \/ % 0.53/0.69 ~hollywood_placename skolemFOFtoCNF_U $_331 \/ % 0.53/0.69 ~in skolemFOFtoCNF_U $_333 $_332 \/ % 0.53/0.69 ~jules_forename skolemFOFtoCNF_U $_328 \/ % 0.53/0.69 ~lonely skolemFOFtoCNF_U $_332 \/ % 0.53/0.69 ~of skolemFOFtoCNF_U $_328 skolemFOFtoCNF_V \/ % 0.53/0.69 ~of skolemFOFtoCNF_U $_331 $_332 \/ ~old skolemFOFtoCNF_U $_330 \/ % 0.53/0.69 ~placename skolemFOFtoCNF_U $_331 \/ ~present skolemFOFtoCNF_U $_333 \/ % 0.53/0.69 ~street skolemFOFtoCNF_U $_332 \/ ~two skolemFOFtoCNF_U $_334 \/ % 0.53/0.69 ~wheel skolemFOFtoCNF_U $_329 \/ ~white skolemFOFtoCNF_U $_330 \/ % 0.53/0.69 definitionFOFtoCNF_0 skolemFOFtoCNF_U $_334 % 0.53/0.69 (skolemFOFtoCNF_X30 skolemFOFtoCNF_U $_334) \/ % 0.53/0.69 member skolemFOFtoCNF_U % 0.53/0.69 (skolemFOFtoCNF_X27 skolemFOFtoCNF_U $_329 $_334) $_334 \/ % 0.53/0.69 member skolemFOFtoCNF_U % 0.53/0.69 (skolemFOFtoCNF_X31 skolemFOFtoCNF_U $_334 $_335) $_335 % 0.53/0.69 SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.53/0.69 %------------------------------------------------------------------------------