PyRes---1.5.CSA-Sat.s

%------------------------------------------------------------------------------
% File     : PyRes---1.5
% Problem  : NLP116+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s

% Computer : n019.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  : 300s
% DateTime : Thu May  9 17:34:10 EDT 2024

% Result   : CounterSatisfiable 4.30s 4.49s
% Output   : Saturation 4.30s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12  % Problem  : NLP116+1 : TPTP v8.1.2. Released v2.4.0.
% 0.07/0.13  % Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34  % Computer : n019.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  : 300
% 0.13/0.34  % DateTime : Wed May  8 13:29:53 EDT 2024
% 0.13/0.34  % CPUTime  : 
% 4.30/4.49  % Version:  1.5
% 4.30/4.49  % SZS status CounterSatisfiable
% 4.30/4.49  % SZS output start Saturation
% 4.30/4.49  fof(co1,conjecture,(~(~(((?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(((((((((((((((street(U,V)&lonely(U,V))&of(U,W,X))&city(U,X))&hollywood_placename(U,W))&placename(U,W))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&event(U,Y))&agent(U,Y,X))&present(U,Y))&barrel(U,Y))&down(U,Y,V))&in(U,Y,X))))))))=>(?[Z]:(actual_world(Z)&(?[X1]:(?[X2]:(?[X3]:(?[X4]:(((((((((((((((of(Z,X1,X2)&city(Z,X2))&hollywood_placename(Z,X1))&placename(Z,X1))&street(Z,X2))&lonely(Z,X2))&chevy(Z,X3))&white(Z,X3))&dirty(Z,X3))&old(Z,X3))&event(Z,X4))&agent(Z,X4,X3))&present(Z,X4))&barrel(Z,X4))&down(Z,X4,X2))&in(Z,X4,X2)))))))))&((?[Z]:(actual_world(Z)&(?[X1]:(?[X2]:(?[X3]:(?[X4]:(((((((((((((((of(Z,X1,X2)&city(Z,X2))&hollywood_placename(Z,X1))&placename(Z,X1))&street(Z,X2))&lonely(Z,X2))&chevy(Z,X3))&white(Z,X3))&dirty(Z,X3))&old(Z,X3))&event(Z,X4))&agent(Z,X4,X3))&present(Z,X4))&barrel(Z,X4))&down(Z,X4,X2))&in(Z,X4,X2))))))))=>(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(((((((((((((((street(U,V)&lonely(U,V))&of(U,W,X))&city(U,X))&hollywood_placename(U,W))&placename(U,W))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&event(U,Y))&agent(U,Y,X))&present(U,Y))&barrel(U,Y))&down(U,Y,V))&in(U,Y,X)))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1)).
% 4.30/4.49  fof(c0,negated_conjecture,(~(~(~(((?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(((((((((((((((street(U,V)&lonely(U,V))&of(U,W,X))&city(U,X))&hollywood_placename(U,W))&placename(U,W))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&event(U,Y))&agent(U,Y,X))&present(U,Y))&barrel(U,Y))&down(U,Y,V))&in(U,Y,X))))))))=>(?[Z]:(actual_world(Z)&(?[X1]:(?[X2]:(?[X3]:(?[X4]:(((((((((((((((of(Z,X1,X2)&city(Z,X2))&hollywood_placename(Z,X1))&placename(Z,X1))&street(Z,X2))&lonely(Z,X2))&chevy(Z,X3))&white(Z,X3))&dirty(Z,X3))&old(Z,X3))&event(Z,X4))&agent(Z,X4,X3))&present(Z,X4))&barrel(Z,X4))&down(Z,X4,X2))&in(Z,X4,X2)))))))))&((?[Z]:(actual_world(Z)&(?[X1]:(?[X2]:(?[X3]:(?[X4]:(((((((((((((((of(Z,X1,X2)&city(Z,X2))&hollywood_placename(Z,X1))&placename(Z,X1))&street(Z,X2))&lonely(Z,X2))&chevy(Z,X3))&white(Z,X3))&dirty(Z,X3))&old(Z,X3))&event(Z,X4))&agent(Z,X4,X3))&present(Z,X4))&barrel(Z,X4))&down(Z,X4,X2))&in(Z,X4,X2))))))))=>(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(((((((((((((((street(U,V)&lonely(U,V))&of(U,W,X))&city(U,X))&hollywood_placename(U,W))&placename(U,W))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&event(U,Y))&agent(U,Y,X))&present(U,Y))&barrel(U,Y))&down(U,Y,V))&in(U,Y,X))))))))))))),inference(assume_negation,[status(cth)],[co1])).
% 4.30/4.49  fof(c1,negated_conjecture,(((?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(((((((((((((((street(U,V)&lonely(U,V))&of(U,W,X))&city(U,X))&hollywood_placename(U,W))&placename(U,W))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&event(U,Y))&agent(U,Y,X))&present(U,Y))&barrel(U,Y))&down(U,Y,V))&in(U,Y,X))))))))&(![Z]:(~actual_world(Z)|(![X1]:(![X2]:(![X3]:(![X4]:(((((((((((((((~of(Z,X1,X2)|~city(Z,X2))|~hollywood_placename(Z,X1))|~placename(Z,X1))|~street(Z,X2))|~lonely(Z,X2))|~chevy(Z,X3))|~white(Z,X3))|~dirty(Z,X3))|~old(Z,X3))|~event(Z,X4))|~agent(Z,X4,X3))|~present(Z,X4))|~barrel(Z,X4))|~down(Z,X4,X2))|~in(Z,X4,X2)))))))))|((?[Z]:(actual_world(Z)&(?[X1]:(?[X2]:(?[X3]:(?[X4]:(((((((((((((((of(Z,X1,X2)&city(Z,X2))&hollywood_placename(Z,X1))&placename(Z,X1))&street(Z,X2))&lonely(Z,X2))&chevy(Z,X3))&white(Z,X3))&dirty(Z,X3))&old(Z,X3))&event(Z,X4))&agent(Z,X4,X3))&present(Z,X4))&barrel(Z,X4))&down(Z,X4,X2))&in(Z,X4,X2))))))))&(![U]:(~actual_world(U)|(![V]:(![W]:(![X]:(![Y]:(((((((((((((((~street(U,V)|~lonely(U,V))|~of(U,W,X))|~city(U,X))|~hollywood_placename(U,W))|~placename(U,W))|~chevy(U,X))|~white(U,X))|~dirty(U,X))|~old(U,X))|~event(U,Y))|~agent(U,Y,X))|~present(U,Y))|~barrel(U,Y))|~down(U,Y,V))|~in(U,Y,X)))))))))),inference(fof_nnf,[status(thm)],[c0])).
% 4.30/4.49  fof(c2,negated_conjecture,(((?[X2]:(actual_world(X2)&(?[X3]:(?[X4]:(?[X5]:(?[X6]:(((((((((((((((street(X2,X3)&lonely(X2,X3))&of(X2,X4,X5))&city(X2,X5))&hollywood_placename(X2,X4))&placename(X2,X4))&chevy(X2,X5))&white(X2,X5))&dirty(X2,X5))&old(X2,X5))&event(X2,X6))&agent(X2,X6,X5))&present(X2,X6))&barrel(X2,X6))&down(X2,X6,X3))&in(X2,X6,X5))))))))&(![X7]:(~actual_world(X7)|(![X8]:(![X9]:(![X10]:(![X11]:(((((((((((((((~of(X7,X8,X9)|~city(X7,X9))|~hollywood_placename(X7,X8))|~placename(X7,X8))|~street(X7,X9))|~lonely(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~event(X7,X11))|~agent(X7,X11,X10))|~present(X7,X11))|~barrel(X7,X11))|~down(X7,X11,X9))|~in(X7,X11,X9)))))))))|((?[X12]:(actual_world(X12)&(?[X13]:(?[X14]:(?[X15]:(?[X16]:(((((((((((((((of(X12,X13,X14)&city(X12,X14))&hollywood_placename(X12,X13))&placename(X12,X13))&street(X12,X14))&lonely(X12,X14))&chevy(X12,X15))&white(X12,X15))&dirty(X12,X15))&old(X12,X15))&event(X12,X16))&agent(X12,X16,X15))&present(X12,X16))&barrel(X12,X16))&down(X12,X16,X14))&in(X12,X16,X14))))))))&(![X17]:(~actual_world(X17)|(![X18]:(![X19]:(![X20]:(![X21]:(((((((((((((((~street(X17,X18)|~lonely(X17,X18))|~of(X17,X19,X20))|~city(X17,X20))|~hollywood_placename(X17,X19))|~placename(X17,X19))|~chevy(X17,X20))|~white(X17,X20))|~dirty(X17,X20))|~old(X17,X20))|~event(X17,X21))|~agent(X17,X21,X20))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X18))|~in(X17,X21,X20)))))))))),inference(variable_rename,[status(thm)],[c1])).
% 4.30/4.49  fof(c4,negated_conjecture,(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(((actual_world(skolem0001)&(((((((((((((((street(skolem0001,skolem0002)&lonely(skolem0001,skolem0002))&of(skolem0001,skolem0003,skolem0004))&city(skolem0001,skolem0004))&hollywood_placename(skolem0001,skolem0003))&placename(skolem0001,skolem0003))&chevy(skolem0001,skolem0004))&white(skolem0001,skolem0004))&dirty(skolem0001,skolem0004))&old(skolem0001,skolem0004))&event(skolem0001,skolem0005))&agent(skolem0001,skolem0005,skolem0004))&present(skolem0001,skolem0005))&barrel(skolem0001,skolem0005))&down(skolem0001,skolem0005,skolem0002))&in(skolem0001,skolem0005,skolem0004)))&(~actual_world(X7)|(((((((((((((((~of(X7,X8,X9)|~city(X7,X9))|~hollywood_placename(X7,X8))|~placename(X7,X8))|~street(X7,X9))|~lonely(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~event(X7,X11))|~agent(X7,X11,X10))|~present(X7,X11))|~barrel(X7,X11))|~down(X7,X11,X9))|~in(X7,X11,X9))))|((actual_world(skolem0006)&(((((((((((((((of(skolem0006,skolem0007,skolem0008)&city(skolem0006,skolem0008))&hollywood_placename(skolem0006,skolem0007))&placename(skolem0006,skolem0007))&street(skolem0006,skolem0008))&lonely(skolem0006,skolem0008))&chevy(skolem0006,skolem0009))&white(skolem0006,skolem0009))&dirty(skolem0006,skolem0009))&old(skolem0006,skolem0009))&event(skolem0006,skolem0010))&agent(skolem0006,skolem0010,skolem0009))&present(skolem0006,skolem0010))&barrel(skolem0006,skolem0010))&down(skolem0006,skolem0010,skolem0008))&in(skolem0006,skolem0010,skolem0008)))&(~actual_world(X17)|(((((((((((((((~street(X17,X18)|~lonely(X17,X18))|~of(X17,X19,X20))|~city(X17,X20))|~hollywood_placename(X17,X19))|~placename(X17,X19))|~chevy(X17,X20))|~white(X17,X20))|~dirty(X17,X20))|~old(X17,X20))|~event(X17,X21))|~agent(X17,X21,X20))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X18))|~in(X17,X21,X20))))))))))))))),inference(shift_quantors,[status(thm)],[fof(c3,negated_conjecture,(((actual_world(skolem0001)&(((((((((((((((street(skolem0001,skolem0002)&lonely(skolem0001,skolem0002))&of(skolem0001,skolem0003,skolem0004))&city(skolem0001,skolem0004))&hollywood_placename(skolem0001,skolem0003))&placename(skolem0001,skolem0003))&chevy(skolem0001,skolem0004))&white(skolem0001,skolem0004))&dirty(skolem0001,skolem0004))&old(skolem0001,skolem0004))&event(skolem0001,skolem0005))&agent(skolem0001,skolem0005,skolem0004))&present(skolem0001,skolem0005))&barrel(skolem0001,skolem0005))&down(skolem0001,skolem0005,skolem0002))&in(skolem0001,skolem0005,skolem0004)))&(![X7]:(~actual_world(X7)|(![X8]:(![X9]:(![X10]:(![X11]:(((((((((((((((~of(X7,X8,X9)|~city(X7,X9))|~hollywood_placename(X7,X8))|~placename(X7,X8))|~street(X7,X9))|~lonely(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~event(X7,X11))|~agent(X7,X11,X10))|~present(X7,X11))|~barrel(X7,X11))|~down(X7,X11,X9))|~in(X7,X11,X9)))))))))|((actual_world(skolem0006)&(((((((((((((((of(skolem0006,skolem0007,skolem0008)&city(skolem0006,skolem0008))&hollywood_placename(skolem0006,skolem0007))&placename(skolem0006,skolem0007))&street(skolem0006,skolem0008))&lonely(skolem0006,skolem0008))&chevy(skolem0006,skolem0009))&white(skolem0006,skolem0009))&dirty(skolem0006,skolem0009))&old(skolem0006,skolem0009))&event(skolem0006,skolem0010))&agent(skolem0006,skolem0010,skolem0009))&present(skolem0006,skolem0010))&barrel(skolem0006,skolem0010))&down(skolem0006,skolem0010,skolem0008))&in(skolem0006,skolem0010,skolem0008)))&(![X17]:(~actual_world(X17)|(![X18]:(![X19]:(![X20]:(![X21]:(((((((((((((((~street(X17,X18)|~lonely(X17,X18))|~of(X17,X19,X20))|~city(X17,X20))|~hollywood_placename(X17,X19))|~placename(X17,X19))|~chevy(X17,X20))|~white(X17,X20))|~dirty(X17,X20))|~old(X17,X20))|~event(X17,X21))|~agent(X17,X21,X20))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X18))|~in(X17,X21,X20)))))))))),inference(skolemize,[status(esa)],[c2])).])).
% 4.30/4.50  fof(c5,negated_conjecture,(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(((((actual_world(skolem0001)|actual_world(skolem0006))&((((((((((((((((actual_world(skolem0001)|of(skolem0006,skolem0007,skolem0008))&(actual_world(skolem0001)|city(skolem0006,skolem0008)))&(actual_world(skolem0001)|hollywood_placename(skolem0006,skolem0007)))&(actual_world(skolem0001)|placename(skolem0006,skolem0007)))&(actual_world(skolem0001)|street(skolem0006,skolem0008)))&(actual_world(skolem0001)|lonely(skolem0006,skolem0008)))&(actual_world(skolem0001)|chevy(skolem0006,skolem0009)))&(actual_world(skolem0001)|white(skolem0006,skolem0009)))&(actual_world(skolem0001)|dirty(skolem0006,skolem0009)))&(actual_world(skolem0001)|old(skolem0006,skolem0009)))&(actual_world(skolem0001)|event(skolem0006,skolem0010)))&(actual_world(skolem0001)|agent(skolem0006,skolem0010,skolem0009)))&(actual_world(skolem0001)|present(skolem0006,skolem0010)))&(actual_world(skolem0001)|barrel(skolem0006,skolem0010)))&(actual_world(skolem0001)|down(skolem0006,skolem0010,skolem0008)))&(actual_world(skolem0001)|in(skolem0006,skolem0010,skolem0008))))&(actual_world(skolem0001)|(~actual_world(X17)|(((((((((((((((~street(X17,X18)|~lonely(X17,X18))|~of(X17,X19,X20))|~city(X17,X20))|~hollywood_placename(X17,X19))|~placename(X17,X19))|~chevy(X17,X20))|~white(X17,X20))|~dirty(X17,X20))|~old(X17,X20))|~event(X17,X21))|~agent(X17,X21,X20))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X18))|~in(X17,X21,X20)))))&((((((((((((((((((street(skolem0001,skolem0002)|actual_world(skolem0006))&((((((((((((((((street(skolem0001,skolem0002)|of(skolem0006,skolem0007,skolem0008))&(street(skolem0001,skolem0002)|city(skolem0006,skolem0008)))&(street(skolem0001,skolem0002)|hollywood_placename(skolem0006,skolem0007)))&(street(skolem0001,skolem0002)|placename(skolem0006,skolem0007)))&(street(skolem0001,skolem0002)|street(skolem0006,skolem0008)))&(street(skolem0001,skolem0002)|lonely(skolem0006,skolem0008)))&(street(skolem0001,skolem0002)|chevy(skolem0006,skolem0009)))&(street(skolem0001,skolem0002)|white(skolem0006,skolem0009)))&(street(skolem0001,skolem0002)|dirty(skolem0006,skolem0009)))&(street(skolem0001,skolem0002)|old(skolem0006,skolem0009)))&(street(skolem0001,skolem0002)|event(skolem0006,skolem0010)))&(street(skolem0001,skolem0002)|agent(skolem0006,skolem0010,skolem0009)))&(street(skolem0001,skolem0002)|present(skolem0006,skolem0010)))&(street(skolem0001,skolem0002)|barrel(skolem0006,skolem0010)))&(street(skolem0001,skolem0002)|down(skolem0006,skolem0010,skolem0008)))&(street(skolem0001,skolem0002)|in(skolem0006,skolem0010,skolem0008))))&(street(skolem0001,skolem0002)|(~actual_world(X17)|(((((((((((((((~street(X17,X18)|~lonely(X17,X18))|~of(X17,X19,X20))|~city(X17,X20))|~hollywood_placename(X17,X19))|~placename(X17,X19))|~chevy(X17,X20))|~white(X17,X20))|~dirty(X17,X20))|~old(X17,X20))|~event(X17,X21))|~agent(X17,X21,X20))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X18))|~in(X17,X21,X20)))))&(((lonely(skolem0001,skolem0002)|actual_world(skolem0006))&((((((((((((((((lonely(skolem0001,skolem0002)|of(skolem0006,skolem0007,skolem0008))&(lonely(skolem0001,skolem0002)|city(skolem0006,skolem0008)))&(lonely(skolem0001,skolem0002)|hollywood_placename(skolem0006,skolem0007)))&(lonely(skolem0001,skolem0002)|placename(skolem0006,skolem0007)))&(lonely(skolem0001,skolem0002)|street(skolem0006,skolem0008)))&(lonely(skolem0001,skolem0002)|lonely(skolem0006,skolem0008)))&(lonely(skolem0001,skolem0002)|chevy(skolem0006,skolem0009)))&(lonely(skolem0001,skolem0002)|white(skolem0006,skolem0009)))&(lonely(skolem0001,skolem0002)|dirty(skolem0006,skolem0009)))&(lonely(skolem0001,skolem0002)|old(skolem0006,skolem0009)))&(lonely(skolem0001,skolem0002)|event(skolem0006,skolem0010)))&(lonely(skolem0001,skolem0002)|agent(skolem0006,skolem0010,skolem0009)))&(lonely(skolem0001,skolem0002)|present(skolem0006,skolem0010)))&(lonely(skolem0001,skolem0002)|barrel(skolem0006,skolem0010)))&(lonely(skolem0001,skolem0002)|down(skolem0006,skolem0010,skolem0008)))&(lonely(skolem0001,skolem0002)|in(skolem0006,skolem0010,skolem0008))))&(lonely(skolem0001,skolem0002)|(~actual_world(X17)|(((((((((((((((~street(X17,X18)|~lonely(X17,X18))|~of(X17,X19,X20))|~city(X17,X20))|~hollywood_placename(X17,X19))|~placename(X17,X19))|~chevy(X17,X20))|~white(X17,X20))|~dirty(X17,X20))|~old(X17,X20))|~event(X17,X21))|~agent(X17,X21,X20))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X18))|~in(X17,X21,X20))))))&(((of(skolem0001,skolem0003,skolem0004)|actual_world(skolem0006))&((((((((((((((((of(skolem0001,skolem0003,skolem0004)|of(skolem0006,skolem0007,skolem0008))&(of(skolem0001,skolem0003,skolem0004)|city(skolem0006,skolem0008)))&(of(skolem0001,skolem0003,skolem0004)|hollywood_placename(skolem0006,skolem0007)))&(of(skolem0001,skolem0003,skolem0004)|placename(skolem0006,skolem0007)))&(of(skolem0001,skolem0003,skolem0004)|street(skolem0006,skolem0008)))&(of(skolem0001,skolem0003,skolem0004)|lonely(skolem0006,skolem0008)))&(of(skolem0001,skolem0003,skolem0004)|chevy(skolem0006,skolem0009)))&(of(skolem0001,skolem0003,skolem0004)|white(skolem0006,skolem0009)))&(of(skolem0001,skolem0003,skolem0004)|dirty(skolem0006,skolem0009)))&(of(skolem0001,skolem0003,skolem0004)|old(skolem0006,skolem0009)))&(of(skolem0001,skolem0003,skolem0004)|event(skolem0006,skolem0010)))&(of(skolem0001,skolem0003,skolem0004)|agent(skolem0006,skolem0010,skolem0009)))&(of(skolem0001,skolem0003,skolem0004)|present(skolem0006,skolem0010)))&(of(skolem0001,skolem0003,skolem0004)|barrel(skolem0006,skolem0010)))&(of(skolem0001,skolem0003,skolem0004)|down(skolem0006,skolem0010,skolem0008)))&(of(skolem0001,skolem0003,skolem0004)|in(skolem0006,skolem0010,skolem0008))))&(of(skolem0001,skolem0003,skolem0004)|(~actual_world(X17)|(((((((((((((((~street(X17,X18)|~lonely(X17,X18))|~of(X17,X19,X20))|~city(X17,X20))|~hollywood_placename(X17,X19))|~placename(X17,X19))|~chevy(X17,X20))|~white(X17,X20))|~dirty(X17,X20))|~old(X17,X20))|~event(X17,X21))|~agent(X17,X21,X20))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X18))|~in(X17,X21,X20))))))&(((city(skolem0001,skolem0004)|actual_world(skolem0006))&((((((((((((((((city(skolem0001,skolem0004)|of(skolem0006,skolem0007,skolem0008))&(city(skolem0001,skolem0004)|city(skolem0006,skolem0008)))&(city(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0007)))&(city(skolem0001,skolem0004)|placename(skolem0006,skolem0007)))&(city(skolem0001,skolem0004)|street(skolem0006,skolem0008)))&(city(skolem0001,skolem0004)|lonely(skolem0006,skolem0008)))&(city(skolem0001,skolem0004)|chevy(skolem0006,skolem0009)))&(city(skolem0001,skolem0004)|white(skolem0006,skolem0009)))&(city(skolem0001,skolem0004)|dirty(skolem0006,skolem0009)))&(city(skolem0001,skolem0004)|old(skolem0006,skolem0009)))&(city(skolem0001,skolem0004)|event(skolem0006,skolem0010)))&(city(skolem0001,skolem0004)|agent(skolem0006,skolem0010,skolem0009)))&(city(skolem0001,skolem0004)|present(skolem0006,skolem0010)))&(city(skolem0001,skolem0004)|barrel(skolem0006,skolem0010)))&(city(skolem0001,skolem0004)|down(skolem0006,skolem0010,skolem0008)))&(city(skolem0001,skolem0004)|in(skolem0006,skolem0010,skolem0008))))&(city(skolem0001,skolem0004)|(~actual_world(X17)|(((((((((((((((~street(X17,X18)|~lonely(X17,X18))|~of(X17,X19,X20))|~city(X17,X20))|~hollywood_placename(X17,X19))|~placename(X17,X19))|~chevy(X17,X20))|~white(X17,X20))|~dirty(X17,X20))|~old(X17,X20))|~event(X17,X21))|~agent(X17,X21,X20))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X18))|~in(X17,X21,X20))))))&(((hollywood_placename(skolem0001,skolem0003)|actual_world(skolem0006))&((((((((((((((((hollywood_placename(skolem0001,skolem0003)|of(skolem0006,skolem0007,skolem0008))&(hollywood_placename(skolem0001,skolem0003)|city(skolem0006,skolem0008)))&(hollywood_placename(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0007)))&(hollywood_placename(skolem0001,skolem0003)|placename(skolem0006,skolem0007)))&(hollywood_placename(skolem0001,skolem0003)|street(skolem0006,skolem0008)))&(hollywood_placename(skolem0001,skolem0003)|lonely(skolem0006,skolem0008)))&(hollywood_placename(skolem0001,skolem0003)|chevy(skolem0006,skolem0009)))&(hollywood_placename(skolem0001,skolem0003)|white(skolem0006,skolem0009)))&(hollywood_placename(skolem0001,skolem0003)|dirty(skolem0006,skolem0009)))&(hollywood_placename(skolem0001,skolem0003)|old(skolem0006,skolem0009)))&(hollywood_placename(skolem0001,skolem0003)|event(skolem0006,skolem0010)))&(hollywood_placename(skolem0001,skolem0003)|agent(skolem0006,skolem0010,skolem0009)))&(hollywood_placename(skolem0001,skolem0003)|present(skolem0006,skolem0010)))&(hollywood_placename(skolem0001,skolem0003)|barrel(skolem0006,skolem0010)))&(hollywood_placename(skolem0001,skolem0003)|down(skolem0006,skolem0010,skolem0008)))&(hollywood_placename(skolem0001,skolem0003)|in(skolem0006,skolem0010,skolem0008))))&(hollywood_placename(skolem0001,skolem0003)|(~actual_world(X17)|(((((((((((((((~street(X17,X18)|~lonely(X17,X18))|~of(X17,X19,X20))|~city(X17,X20))|~hollywood_placename(X17,X19))|~placename(X17,X19))|~chevy(X17,X20))|~white(X17,X20))|~dirty(X17,X20))|~old(X17,X20))|~event(X17,X21))|~agent(X17,X21,X20))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X18))|~in(X17,X21,X20))))))&(((placename(skolem0001,skolem0003)|actual_world(skolem0006))&((((((((((((((((placename(skolem0001,skolem0003)|of(skolem0006,skolem0007,skolem0008))&(placename(skolem0001,skolem0003)|city(skolem0006,skolem0008)))&(placename(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0007)))&(placename(skolem0001,skolem0003)|placename(skolem0006,skolem0007)))&(placename(skolem0001,skolem0003)|street(skolem0006,skolem0008)))&(placename(skolem0001,skolem0003)|lonely(skolem0006,skolem0008)))&(placename(skolem0001,skolem0003)|chevy(skolem0006,skolem0009)))&(placename(skolem0001,skolem0003)|white(skolem0006,skolem0009)))&(placename(skolem0001,skolem0003)|dirty(skolem0006,skolem0009)))&(placename(skolem0001,skolem0003)|old(skolem0006,skolem0009)))&(placename(skolem0001,skolem0003)|event(skolem0006,skolem0010)))&(placename(skolem0001,skolem0003)|agent(skolem0006,skolem0010,skolem0009)))&(placename(skolem0001,skolem0003)|present(skolem0006,skolem0010)))&(placename(skolem0001,skolem0003)|barrel(skolem0006,skolem0010)))&(placename(skolem0001,skolem0003)|down(skolem0006,skolem0010,skolem0008)))&(placename(skolem0001,skolem0003)|in(skolem0006,skolem0010,skolem0008))))&(placename(skolem0001,skolem0003)|(~actual_world(X17)|(((((((((((((((~street(X17,X18)|~lonely(X17,X18))|~of(X17,X19,X20))|~city(X17,X20))|~hollywood_placename(X17,X19))|~placename(X17,X19))|~chevy(X17,X20))|~white(X17,X20))|~dirty(X17,X20))|~old(X17,X20))|~event(X17,X21))|~agent(X17,X21,X20))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X18))|~in(X17,X21,X20))))))&(((chevy(skolem0001,skolem0004)|actual_world(skolem0006))&((((((((((((((((chevy(skolem0001,skolem0004)|of(skolem0006,skolem0007,skolem0008))&(chevy(skolem0001,skolem0004)|city(skolem0006,skolem0008)))&(chevy(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0007)))&(chevy(skolem0001,skolem0004)|placename(skolem0006,skolem0007)))&(chevy(skolem0001,skolem0004)|street(skolem0006,skolem0008)))&(chevy(skolem0001,skolem0004)|lonely(skolem0006,skolem0008)))&(chevy(skolem0001,skolem0004)|chevy(skolem0006,skolem0009)))&(chevy(skolem0001,skolem0004)|white(skolem0006,skolem0009)))&(chevy(skolem0001,skolem0004)|dirty(skolem0006,skolem0009)))&(chevy(skolem0001,skolem0004)|old(skolem0006,skolem0009)))&(chevy(skolem0001,skolem0004)|event(skolem0006,skolem0010)))&(chevy(skolem0001,skolem0004)|agent(skolem0006,skolem0010,skolem0009)))&(chevy(skolem0001,skolem0004)|present(skolem0006,skolem0010)))&(chevy(skolem0001,skolem0004)|barrel(skolem0006,skolem0010)))&(chevy(skolem0001,skolem0004)|down(skolem0006,skolem0010,skolem0008)))&(chevy(skolem0001,skolem0004)|in(skolem0006,skolem0010,skolem0008))))&(chevy(skolem0001,skolem0004)|(~actual_world(X17)|(((((((((((((((~street(X17,X18)|~lonely(X17,X18))|~of(X17,X19,X20))|~city(X17,X20))|~hollywood_placename(X17,X19))|~placename(X17,X19))|~chevy(X17,X20))|~white(X17,X20))|~dirty(X17,X20))|~old(X17,X20))|~event(X17,X21))|~agent(X17,X21,X20))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X18))|~in(X17,X21,X20))))))&(((white(skolem0001,skolem0004)|actual_world(skolem0006))&((((((((((((((((white(skolem0001,skolem0004)|of(skolem0006,skolem0007,skolem0008))&(white(skolem0001,skolem0004)|city(skolem0006,skolem0008)))&(white(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0007)))&(white(skolem0001,skolem0004)|placename(skolem0006,skolem0007)))&(white(skolem0001,skolem0004)|street(skolem0006,skolem0008)))&(white(skolem0001,skolem0004)|lonely(skolem0006,skolem0008)))&(white(skolem0001,skolem0004)|chevy(skolem0006,skolem0009)))&(white(skolem0001,skolem0004)|white(skolem0006,skolem0009)))&(white(skolem0001,skolem0004)|dirty(skolem0006,skolem0009)))&(white(skolem0001,skolem0004)|old(skolem0006,skolem0009)))&(white(skolem0001,skolem0004)|event(skolem0006,skolem0010)))&(white(skolem0001,skolem0004)|agent(skolem0006,skolem0010,skolem0009)))&(white(skolem0001,skolem0004)|present(skolem0006,skolem0010)))&(white(skolem0001,skolem0004)|barrel(skolem0006,skolem0010)))&(white(skolem0001,skolem0004)|down(skolem0006,skolem0010,skolem0008)))&(white(skolem0001,skolem0004)|in(skolem0006,skolem0010,skolem0008))))&(white(skolem0001,skolem0004)|(~actual_world(X17)|(((((((((((((((~street(X17,X18)|~lonely(X17,X18))|~of(X17,X19,X20))|~city(X17,X20))|~hollywood_placename(X17,X19))|~placename(X17,X19))|~chevy(X17,X20))|~white(X17,X20))|~dirty(X17,X20))|~old(X17,X20))|~event(X17,X21))|~agent(X17,X21,X20))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X18))|~in(X17,X21,X20))))))&(((dirty(skolem0001,skolem0004)|actual_world(skolem0006))&((((((((((((((((dirty(skolem0001,skolem0004)|of(skolem0006,skolem0007,skolem0008))&(dirty(skolem0001,skolem0004)|city(skolem0006,skolem0008)))&(dirty(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0007)))&(dirty(skolem0001,skolem0004)|placename(skolem0006,skolem0007)))&(dirty(skolem0001,skolem0004)|street(skolem0006,skolem0008)))&(dirty(skolem0001,skolem0004)|lonely(skolem0006,skolem0008)))&(dirty(skolem0001,skolem0004)|chevy(skolem0006,skolem0009)))&(dirty(skolem0001,skolem0004)|white(skolem0006,skolem0009)))&(dirty(skolem0001,skolem0004)|dirty(skolem0006,skolem0009)))&(dirty(skolem0001,skolem0004)|old(skolem0006,skolem0009)))&(dirty(skolem0001,skolem0004)|event(skolem0006,skolem0010)))&(dirty(skolem0001,skolem0004)|agent(skolem0006,skolem0010,skolem0009)))&(dirty(skolem0001,skolem0004)|present(skolem0006,skolem0010)))&(dirty(skolem0001,skolem0004)|barrel(skolem0006,skolem0010)))&(dirty(skolem0001,skolem0004)|down(skolem0006,skolem0010,skolem0008)))&(dirty(skolem0001,skolem0004)|in(skolem0006,skolem0010,skolem0008))))&(dirty(skolem0001,skolem0004)|(~actual_world(X17)|(((((((((((((((~street(X17,X18)|~lonely(X17,X18))|~of(X17,X19,X20))|~city(X17,X20))|~hollywood_placename(X17,X19))|~placename(X17,X19))|~chevy(X17,X20))|~white(X17,X20))|~dirty(X17,X20))|~old(X17,X20))|~event(X17,X21))|~agent(X17,X21,X20))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X18))|~in(X17,X21,X20))))))&(((old(skolem0001,skolem0004)|actual_world(skolem0006))&((((((((((((((((old(skolem0001,skolem0004)|of(skolem0006,skolem0007,skolem0008))&(old(skolem0001,skolem0004)|city(skolem0006,skolem0008)))&(old(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0007)))&(old(skolem0001,skolem0004)|placename(skolem0006,skolem0007)))&(old(skolem0001,skolem0004)|street(skolem0006,skolem0008)))&(old(skolem0001,skolem0004)|lonely(skolem0006,skolem0008)))&(old(skolem0001,skolem0004)|chevy(skolem0006,skolem0009)))&(old(skolem0001,skolem0004)|white(skolem0006,skolem0009)))&(old(skolem0001,skolem0004)|dirty(skolem0006,skolem0009)))&(old(skolem0001,skolem0004)|old(skolem0006,skolem0009)))&(old(skolem0001,skolem0004)|event(skolem0006,skolem0010)))&(old(skolem0001,skolem0004)|agent(skolem0006,skolem0010,skolem0009)))&(old(skolem0001,skolem0004)|present(skolem0006,skolem0010)))&(old(skolem0001,skolem0004)|barrel(skolem0006,skolem0010)))&(old(skolem0001,skolem0004)|down(skolem0006,skolem0010,skolem0008)))&(old(skolem0001,skolem0004)|in(skolem0006,skolem0010,skolem0008))))&(old(skolem0001,skolem0004)|(~actual_world(X17)|(((((((((((((((~street(X17,X18)|~lonely(X17,X18))|~of(X17,X19,X20))|~city(X17,X20))|~hollywood_placename(X17,X19))|~placename(X17,X19))|~chevy(X17,X20))|~white(X17,X20))|~dirty(X17,X20))|~old(X17,X20))|~event(X17,X21))|~agent(X17,X21,X20))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X18))|~in(X17,X21,X20))))))&(((event(skolem0001,skolem0005)|actual_world(skolem0006))&((((((((((((((((event(skolem0001,skolem0005)|of(skolem0006,skolem0007,skolem0008))&(event(skolem0001,skolem0005)|city(skolem0006,skolem0008)))&(event(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0007)))&(event(skolem0001,skolem0005)|placename(skolem0006,skolem0007)))&(event(skolem0001,skolem0005)|street(skolem0006,skolem0008)))&(event(skolem0001,skolem0005)|lonely(skolem0006,skolem0008)))&(event(skolem0001,skolem0005)|chevy(skolem0006,skolem0009)))&(event(skolem0001,skolem0005)|white(skolem0006,skolem0009)))&(event(skolem0001,skolem0005)|dirty(skolem0006,skolem0009)))&(event(skolem0001,skolem0005)|old(skolem0006,skolem0009)))&(event(skolem0001,skolem0005)|event(skolem0006,skolem0010)))&(event(skolem0001,skolem0005)|agent(skolem0006,skolem0010,skolem0009)))&(event(skolem0001,skolem0005)|present(skolem0006,skolem0010)))&(event(skolem0001,skolem0005)|barrel(skolem0006,skolem0010)))&(event(skolem0001,skolem0005)|down(skolem0006,skolem0010,skolem0008)))&(event(skolem0001,skolem0005)|in(skolem0006,skolem0010,skolem0008))))&(event(skolem0001,skolem0005)|(~actual_world(X17)|(((((((((((((((~street(X17,X18)|~lonely(X17,X18))|~of(X17,X19,X20))|~city(X17,X20))|~hollywood_placename(X17,X19))|~placename(X17,X19))|~chevy(X17,X20))|~white(X17,X20))|~dirty(X17,X20))|~old(X17,X20))|~event(X17,X21))|~agent(X17,X21,X20))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X18))|~in(X17,X21,X20))))))&(((agent(skolem0001,skolem0005,skolem0004)|actual_world(skolem0006))&((((((((((((((((agent(skolem0001,skolem0005,skolem0004)|of(skolem0006,skolem0007,skolem0008))&(agent(skolem0001,skolem0005,skolem0004)|city(skolem0006,skolem0008)))&(agent(skolem0001,skolem0005,skolem0004)|hollywood_placename(skolem0006,skolem0007)))&(agent(skolem0001,skolem0005,skolem0004)|placename(skolem0006,skolem0007)))&(agent(skolem0001,skolem0005,skolem0004)|street(skolem0006,skolem0008)))&(agent(skolem0001,skolem0005,skolem0004)|lonely(skolem0006,skolem0008)))&(agent(skolem0001,skolem0005,skolem0004)|chevy(skolem0006,skolem0009)))&(agent(skolem0001,skolem0005,skolem0004)|white(skolem0006,skolem0009)))&(agent(skolem0001,skolem0005,skolem0004)|dirty(skolem0006,skolem0009)))&(agent(skolem0001,skolem0005,skolem0004)|old(skolem0006,skolem0009)))&(agent(skolem0001,skolem0005,skolem0004)|event(skolem0006,skolem0010)))&(agent(skolem0001,skolem0005,skolem0004)|agent(skolem0006,skolem0010,skolem0009)))&(agent(skolem0001,skolem0005,skolem0004)|present(skolem0006,skolem0010)))&(agent(skolem0001,skolem0005,skolem0004)|barrel(skolem0006,skolem0010)))&(agent(skolem0001,skolem0005,skolem0004)|down(skolem0006,skolem0010,skolem0008)))&(agent(skolem0001,skolem0005,skolem0004)|in(skolem0006,skolem0010,skolem0008))))&(agent(skolem0001,skolem0005,skolem0004)|(~actual_world(X17)|(((((((((((((((~street(X17,X18)|~lonely(X17,X18))|~of(X17,X19,X20))|~city(X17,X20))|~hollywood_placename(X17,X19))|~placename(X17,X19))|~chevy(X17,X20))|~white(X17,X20))|~dirty(X17,X20))|~old(X17,X20))|~event(X17,X21))|~agent(X17,X21,X20))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X18))|~in(X17,X21,X20))))))&(((present(skolem0001,skolem0005)|actual_world(skolem0006))&((((((((((((((((present(skolem0001,skolem0005)|of(skolem0006,skolem0007,skolem0008))&(present(skolem0001,skolem0005)|city(skolem0006,skolem0008)))&(present(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0007)))&(present(skolem0001,skolem0005)|placename(skolem0006,skolem0007)))&(present(skolem0001,skolem0005)|street(skolem0006,skolem0008)))&(present(skolem0001,skolem0005)|lonely(skolem0006,skolem0008)))&(present(skolem0001,skolem0005)|chevy(skolem0006,skolem0009)))&(present(skolem0001,skolem0005)|white(skolem0006,skolem0009)))&(present(skolem0001,skolem0005)|dirty(skolem0006,skolem0009)))&(present(skolem0001,skolem0005)|old(skolem0006,skolem0009)))&(present(skolem0001,skolem0005)|event(skolem0006,skolem0010)))&(present(skolem0001,skolem0005)|agent(skolem0006,skolem0010,skolem0009)))&(present(skolem0001,skolem0005)|present(skolem0006,skolem0010)))&(present(skolem0001,skolem0005)|barrel(skolem0006,skolem0010)))&(present(skolem0001,skolem0005)|down(skolem0006,skolem0010,skolem0008)))&(present(skolem0001,skolem0005)|in(skolem0006,skolem0010,skolem0008))))&(present(skolem0001,skolem0005)|(~actual_world(X17)|(((((((((((((((~street(X17,X18)|~lonely(X17,X18))|~of(X17,X19,X20))|~city(X17,X20))|~hollywood_placename(X17,X19))|~placename(X17,X19))|~chevy(X17,X20))|~white(X17,X20))|~dirty(X17,X20))|~old(X17,X20))|~event(X17,X21))|~agent(X17,X21,X20))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X18))|~in(X17,X21,X20))))))&(((barrel(skolem0001,skolem0005)|actual_world(skolem0006))&((((((((((((((((barrel(skolem0001,skolem0005)|of(skolem0006,skolem0007,skolem0008))&(barrel(skolem0001,skolem0005)|city(skolem0006,skolem0008)))&(barrel(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0007)))&(barrel(skolem0001,skolem0005)|placename(skolem0006,skolem0007)))&(barrel(skolem0001,skolem0005)|street(skolem0006,skolem0008)))&(barrel(skolem0001,skolem0005)|lonely(skolem0006,skolem0008)))&(barrel(skolem0001,skolem0005)|chevy(skolem0006,skolem0009)))&(barrel(skolem0001,skolem0005)|white(skolem0006,skolem0009)))&(barrel(skolem0001,skolem0005)|dirty(skolem0006,skolem0009)))&(barrel(skolem0001,skolem0005)|old(skolem0006,skolem0009)))&(barrel(skolem0001,skolem0005)|event(skolem0006,skolem0010)))&(barrel(skolem0001,skolem0005)|agent(skolem0006,skolem0010,skolem0009)))&(barrel(skolem0001,skolem0005)|present(skolem0006,skolem0010)))&(barrel(skolem0001,skolem0005)|barrel(skolem0006,skolem0010)))&(barrel(skolem0001,skolem0005)|down(skolem0006,skolem0010,skolem0008)))&(barrel(skolem0001,skolem0005)|in(skolem0006,skolem0010,skolem0008))))&(barrel(skolem0001,skolem0005)|(~actual_world(X17)|(((((((((((((((~street(X17,X18)|~lonely(X17,X18))|~of(X17,X19,X20))|~city(X17,X20))|~hollywood_placename(X17,X19))|~placename(X17,X19))|~chevy(X17,X20))|~white(X17,X20))|~dirty(X17,X20))|~old(X17,X20))|~event(X17,X21))|~agent(X17,X21,X20))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X18))|~in(X17,X21,X20))))))&(((down(skolem0001,skolem0005,skolem0002)|actual_world(skolem0006))&((((((((((((((((down(skolem0001,skolem0005,skolem0002)|of(skolem0006,skolem0007,skolem0008))&(down(skolem0001,skolem0005,skolem0002)|city(skolem0006,skolem0008)))&(down(skolem0001,skolem0005,skolem0002)|hollywood_placename(skolem0006,skolem0007)))&(down(skolem0001,skolem0005,skolem0002)|placename(skolem0006,skolem0007)))&(down(skolem0001,skolem0005,skolem0002)|street(skolem0006,skolem0008)))&(down(skolem0001,skolem0005,skolem0002)|lonely(skolem0006,skolem0008)))&(down(skolem0001,skolem0005,skolem0002)|chevy(skolem0006,skolem0009)))&(down(skolem0001,skolem0005,skolem0002)|white(skolem0006,skolem0009)))&(down(skolem0001,skolem0005,skolem0002)|dirty(skolem0006,skolem0009)))&(down(skolem0001,skolem0005,skolem0002)|old(skolem0006,skolem0009)))&(down(skolem0001,skolem0005,skolem0002)|event(skolem0006,skolem0010)))&(down(skolem0001,skolem0005,skolem0002)|agent(skolem0006,skolem0010,skolem0009)))&(down(skolem0001,skolem0005,skolem0002)|present(skolem0006,skolem0010)))&(down(skolem0001,skolem0005,skolem0002)|barrel(skolem0006,skolem0010)))&(down(skolem0001,skolem0005,skolem0002)|down(skolem0006,skolem0010,skolem0008)))&(down(skolem0001,skolem0005,skolem0002)|in(skolem0006,skolem0010,skolem0008))))&(down(skolem0001,skolem0005,skolem0002)|(~actual_world(X17)|(((((((((((((((~street(X17,X18)|~lonely(X17,X18))|~of(X17,X19,X20))|~city(X17,X20))|~hollywood_placename(X17,X19))|~placename(X17,X19))|~chevy(X17,X20))|~white(X17,X20))|~dirty(X17,X20))|~old(X17,X20))|~event(X17,X21))|~agent(X17,X21,X20))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X18))|~in(X17,X21,X20))))))&(((in(skolem0001,skolem0005,skolem0004)|actual_world(skolem0006))&((((((((((((((((in(skolem0001,skolem0005,skolem0004)|of(skolem0006,skolem0007,skolem0008))&(in(skolem0001,skolem0005,skolem0004)|city(skolem0006,skolem0008)))&(in(skolem0001,skolem0005,skolem0004)|hollywood_placename(skolem0006,skolem0007)))&(in(skolem0001,skolem0005,skolem0004)|placename(skolem0006,skolem0007)))&(in(skolem0001,skolem0005,skolem0004)|street(skolem0006,skolem0008)))&(in(skolem0001,skolem0005,skolem0004)|lonely(skolem0006,skolem0008)))&(in(skolem0001,skolem0005,skolem0004)|chevy(skolem0006,skolem0009)))&(in(skolem0001,skolem0005,skolem0004)|white(skolem0006,skolem0009)))&(in(skolem0001,skolem0005,skolem0004)|dirty(skolem0006,skolem0009)))&(in(skolem0001,skolem0005,skolem0004)|old(skolem0006,skolem0009)))&(in(skolem0001,skolem0005,skolem0004)|event(skolem0006,skolem0010)))&(in(skolem0001,skolem0005,skolem0004)|agent(skolem0006,skolem0010,skolem0009)))&(in(skolem0001,skolem0005,skolem0004)|present(skolem0006,skolem0010)))&(in(skolem0001,skolem0005,skolem0004)|barrel(skolem0006,skolem0010)))&(in(skolem0001,skolem0005,skolem0004)|down(skolem0006,skolem0010,skolem0008)))&(in(skolem0001,skolem0005,skolem0004)|in(skolem0006,skolem0010,skolem0008))))&(in(skolem0001,skolem0005,skolem0004)|(~actual_world(X17)|(((((((((((((((~street(X17,X18)|~lonely(X17,X18))|~of(X17,X19,X20))|~city(X17,X20))|~hollywood_placename(X17,X19))|~placename(X17,X19))|~chevy(X17,X20))|~white(X17,X20))|~dirty(X17,X20))|~old(X17,X20))|~event(X17,X21))|~agent(X17,X21,X20))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X18))|~in(X17,X21,X20)))))))&((((~actual_world(X7)|(((((((((((((((~of(X7,X8,X9)|~city(X7,X9))|~hollywood_placename(X7,X8))|~placename(X7,X8))|~street(X7,X9))|~lonely(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~event(X7,X11))|~agent(X7,X11,X10))|~present(X7,X11))|~barrel(X7,X11))|~down(X7,X11,X9))|~in(X7,X11,X9)))|actual_world(skolem0006))&(((((((((((((((((~actual_world(X7)|(((((((((((((((~of(X7,X8,X9)|~city(X7,X9))|~hollywood_placename(X7,X8))|~placename(X7,X8))|~street(X7,X9))|~lonely(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~event(X7,X11))|~agent(X7,X11,X10))|~present(X7,X11))|~barrel(X7,X11))|~down(X7,X11,X9))|~in(X7,X11,X9)))|of(skolem0006,skolem0007,skolem0008))&((~actual_world(X7)|(((((((((((((((~of(X7,X8,X9)|~city(X7,X9))|~hollywood_placename(X7,X8))|~placename(X7,X8))|~street(X7,X9))|~lonely(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~event(X7,X11))|~agent(X7,X11,X10))|~present(X7,X11))|~barrel(X7,X11))|~down(X7,X11,X9))|~in(X7,X11,X9)))|city(skolem0006,skolem0008)))&((~actual_world(X7)|(((((((((((((((~of(X7,X8,X9)|~city(X7,X9))|~hollywood_placename(X7,X8))|~placename(X7,X8))|~street(X7,X9))|~lonely(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~event(X7,X11))|~agent(X7,X11,X10))|~present(X7,X11))|~barrel(X7,X11))|~down(X7,X11,X9))|~in(X7,X11,X9)))|hollywood_placename(skolem0006,skolem0007)))&((~actual_world(X7)|(((((((((((((((~of(X7,X8,X9)|~city(X7,X9))|~hollywood_placename(X7,X8))|~placename(X7,X8))|~street(X7,X9))|~lonely(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~event(X7,X11))|~agent(X7,X11,X10))|~present(X7,X11))|~barrel(X7,X11))|~down(X7,X11,X9))|~in(X7,X11,X9)))|placename(skolem0006,skolem0007)))&((~actual_world(X7)|(((((((((((((((~of(X7,X8,X9)|~city(X7,X9))|~hollywood_placename(X7,X8))|~placename(X7,X8))|~street(X7,X9))|~lonely(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~event(X7,X11))|~agent(X7,X11,X10))|~present(X7,X11))|~barrel(X7,X11))|~down(X7,X11,X9))|~in(X7,X11,X9)))|street(skolem0006,skolem0008)))&((~actual_world(X7)|(((((((((((((((~of(X7,X8,X9)|~city(X7,X9))|~hollywood_placename(X7,X8))|~placename(X7,X8))|~street(X7,X9))|~lonely(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~event(X7,X11))|~agent(X7,X11,X10))|~present(X7,X11))|~barrel(X7,X11))|~down(X7,X11,X9))|~in(X7,X11,X9)))|lonely(skolem0006,skolem0008)))&((~actual_world(X7)|(((((((((((((((~of(X7,X8,X9)|~city(X7,X9))|~hollywood_placename(X7,X8))|~placename(X7,X8))|~street(X7,X9))|~lonely(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~event(X7,X11))|~agent(X7,X11,X10))|~present(X7,X11))|~barrel(X7,X11))|~down(X7,X11,X9))|~in(X7,X11,X9)))|chevy(skolem0006,skolem0009)))&((~actual_world(X7)|(((((((((((((((~of(X7,X8,X9)|~city(X7,X9))|~hollywood_placename(X7,X8))|~placename(X7,X8))|~street(X7,X9))|~lonely(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~event(X7,X11))|~agent(X7,X11,X10))|~present(X7,X11))|~barrel(X7,X11))|~down(X7,X11,X9))|~in(X7,X11,X9)))|white(skolem0006,skolem0009)))&((~actual_world(X7)|(((((((((((((((~of(X7,X8,X9)|~city(X7,X9))|~hollywood_placename(X7,X8))|~placename(X7,X8))|~street(X7,X9))|~lonely(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~event(X7,X11))|~agent(X7,X11,X10))|~present(X7,X11))|~barrel(X7,X11))|~down(X7,X11,X9))|~in(X7,X11,X9)))|dirty(skolem0006,skolem0009)))&((~actual_world(X7)|(((((((((((((((~of(X7,X8,X9)|~city(X7,X9))|~hollywood_placename(X7,X8))|~placename(X7,X8))|~street(X7,X9))|~lonely(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~event(X7,X11))|~agent(X7,X11,X10))|~present(X7,X11))|~barrel(X7,X11))|~down(X7,X11,X9))|~in(X7,X11,X9)))|old(skolem0006,skolem0009)))&((~actual_world(X7)|(((((((((((((((~of(X7,X8,X9)|~city(X7,X9))|~hollywood_placename(X7,X8))|~placename(X7,X8))|~street(X7,X9))|~lonely(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~event(X7,X11))|~agent(X7,X11,X10))|~present(X7,X11))|~barrel(X7,X11))|~down(X7,X11,X9))|~in(X7,X11,X9)))|event(skolem0006,skolem0010)))&((~actual_world(X7)|(((((((((((((((~of(X7,X8,X9)|~city(X7,X9))|~hollywood_placename(X7,X8))|~placename(X7,X8))|~street(X7,X9))|~lonely(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~event(X7,X11))|~agent(X7,X11,X10))|~present(X7,X11))|~barrel(X7,X11))|~down(X7,X11,X9))|~in(X7,X11,X9)))|agent(skolem0006,skolem0010,skolem0009)))&((~actual_world(X7)|(((((((((((((((~of(X7,X8,X9)|~city(X7,X9))|~hollywood_placename(X7,X8))|~placename(X7,X8))|~street(X7,X9))|~lonely(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~event(X7,X11))|~agent(X7,X11,X10))|~present(X7,X11))|~barrel(X7,X11))|~down(X7,X11,X9))|~in(X7,X11,X9)))|present(skolem0006,skolem0010)))&((~actual_world(X7)|(((((((((((((((~of(X7,X8,X9)|~city(X7,X9))|~hollywood_placename(X7,X8))|~placename(X7,X8))|~street(X7,X9))|~lonely(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~event(X7,X11))|~agent(X7,X11,X10))|~present(X7,X11))|~barrel(X7,X11))|~down(X7,X11,X9))|~in(X7,X11,X9)))|barrel(skolem0006,skolem0010)))&((~actual_world(X7)|(((((((((((((((~of(X7,X8,X9)|~city(X7,X9))|~hollywood_placename(X7,X8))|~placename(X7,X8))|~street(X7,X9))|~lonely(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~event(X7,X11))|~agent(X7,X11,X10))|~present(X7,X11))|~barrel(X7,X11))|~down(X7,X11,X9))|~in(X7,X11,X9)))|down(skolem0006,skolem0010,skolem0008)))&((~actual_world(X7)|(((((((((((((((~of(X7,X8,X9)|~city(X7,X9))|~hollywood_placename(X7,X8))|~placename(X7,X8))|~street(X7,X9))|~lonely(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~event(X7,X11))|~agent(X7,X11,X10))|~present(X7,X11))|~barrel(X7,X11))|~down(X7,X11,X9))|~in(X7,X11,X9)))|in(skolem0006,skolem0010,skolem0008))))&((~actual_world(X7)|(((((((((((((((~of(X7,X8,X9)|~city(X7,X9))|~hollywood_placename(X7,X8))|~placename(X7,X8))|~street(X7,X9))|~lonely(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~event(X7,X11))|~agent(X7,X11,X10))|~present(X7,X11))|~barrel(X7,X11))|~down(X7,X11,X9))|~in(X7,X11,X9)))|(~actual_world(X17)|(((((((((((((((~street(X17,X18)|~lonely(X17,X18))|~of(X17,X19,X20))|~city(X17,X20))|~hollywood_placename(X17,X19))|~placename(X17,X19))|~chevy(X17,X20))|~white(X17,X20))|~dirty(X17,X20))|~old(X17,X20))|~event(X17,X21))|~agent(X17,X21,X20))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X18))|~in(X17,X21,X20)))))))))))))))),inference(distribute,[status(thm)],[c4])).
% 4.30/4.51  cnf(c288,negated_conjecture,down(skolem0001,skolem0005,skolem0002)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c329,negated_conjecture,~actual_world(X196)|~of(X196,X197,X199)|~city(X196,X199)|~hollywood_placename(X196,X197)|~placename(X196,X197)|~street(X196,X199)|~lonely(X196,X199)|~chevy(X196,X195)|~white(X196,X195)|~dirty(X196,X195)|~old(X196,X195)|~event(X196,X194)|~agent(X196,X194,X195)|~present(X196,X194)|~barrel(X196,X194)|~down(X196,X194,X199)|~in(X196,X194,X199)|~actual_world(X193)|~street(X193,X200)|~lonely(X193,X200)|~of(X193,X201,X192)|~city(X193,X192)|~hollywood_placename(X193,X201)|~placename(X193,X201)|~chevy(X193,X192)|~white(X193,X192)|~dirty(X193,X192)|~old(X193,X192)|~event(X193,X198)|~agent(X193,X198,X192)|~present(X193,X198)|~barrel(X193,X198)|~down(X193,X198,X200)|~in(X193,X198,X192),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c1486,plain,~actual_world(X2806)|~of(X2806,X2808,X2805)|~city(X2806,X2805)|~hollywood_placename(X2806,X2808)|~placename(X2806,X2808)|~street(X2806,X2805)|~lonely(X2806,X2805)|~chevy(X2806,X2807)|~white(X2806,X2807)|~dirty(X2806,X2807)|~old(X2806,X2807)|~event(X2806,X2803)|~agent(X2806,X2803,X2807)|~present(X2806,X2803)|~barrel(X2806,X2803)|~down(X2806,X2803,X2805)|~in(X2806,X2803,X2805)|~street(X2806,X2809)|~lonely(X2806,X2809)|~of(X2806,X2804,X2805)|~hollywood_placename(X2806,X2804)|~placename(X2806,X2804)|~chevy(X2806,X2805)|~white(X2806,X2805)|~dirty(X2806,X2805)|~old(X2806,X2805)|~agent(X2806,X2803,X2805)|~down(X2806,X2803,X2809),inference(factor,[status(thm)],[c329])).
% 4.30/4.51  cnf(c1810,plain,~actual_world(X2810)|~of(X2810,X2812,X2814)|~city(X2810,X2814)|~hollywood_placename(X2810,X2812)|~placename(X2810,X2812)|~street(X2810,X2814)|~lonely(X2810,X2814)|~chevy(X2810,X2815)|~white(X2810,X2815)|~dirty(X2810,X2815)|~old(X2810,X2815)|~event(X2810,X2811)|~agent(X2810,X2811,X2815)|~present(X2810,X2811)|~barrel(X2810,X2811)|~down(X2810,X2811,X2814)|~in(X2810,X2811,X2814)|~of(X2810,X2813,X2814)|~hollywood_placename(X2810,X2813)|~placename(X2810,X2813)|~chevy(X2810,X2814)|~white(X2810,X2814)|~dirty(X2810,X2814)|~old(X2810,X2814)|~agent(X2810,X2811,X2814),inference(factor,[status(thm)],[c1486])).
% 4.30/4.51  cnf(c1877,plain,~actual_world(skolem0006)|~of(skolem0006,X3218,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3218)|~placename(skolem0006,X3218)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3216)|~white(skolem0006,X3216)|~dirty(skolem0006,X3216)|~old(skolem0006,X3216)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3216)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~of(skolem0006,X3217,skolem0009)|~hollywood_placename(skolem0006,X3217)|~placename(skolem0006,X3217)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|down(skolem0001,skolem0005,skolem0002),inference(resolution,[status(thm)],[c1810, c288])).
% 4.30/4.51  cnf(c1965,plain,~actual_world(skolem0006)|~of(skolem0006,X3227,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3227)|~placename(skolem0006,X3227)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3226)|~white(skolem0006,X3226)|~dirty(skolem0006,X3226)|~old(skolem0006,X3226)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3226)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|down(skolem0001,skolem0005,skolem0002),inference(factor,[status(thm)],[c1877])).
% 4.30/4.51  cnf(c234,negated_conjecture,agent(skolem0001,skolem0005,skolem0004)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c1876,plain,~actual_world(skolem0006)|~of(skolem0006,X3213,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3213)|~placename(skolem0006,X3213)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3211)|~white(skolem0006,X3211)|~dirty(skolem0006,X3211)|~old(skolem0006,X3211)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3211)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~of(skolem0006,X3212,skolem0009)|~hollywood_placename(skolem0006,X3212)|~placename(skolem0006,X3212)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|agent(skolem0001,skolem0005,skolem0004),inference(resolution,[status(thm)],[c1810, c234])).
% 4.30/4.51  cnf(c1964,plain,~actual_world(skolem0006)|~of(skolem0006,X3215,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3215)|~placename(skolem0006,X3215)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3214)|~white(skolem0006,X3214)|~dirty(skolem0006,X3214)|~old(skolem0006,X3214)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3214)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|agent(skolem0001,skolem0005,skolem0004),inference(factor,[status(thm)],[c1876])).
% 4.30/4.51  cnf(c306,negated_conjecture,in(skolem0001,skolem0005,skolem0004)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c1862,plain,~actual_world(skolem0006)|~of(skolem0006,X3208,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3208)|~placename(skolem0006,X3208)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3206)|~white(skolem0006,X3206)|~dirty(skolem0006,X3206)|~old(skolem0006,X3206)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3206)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~of(skolem0006,X3207,skolem0009)|~hollywood_placename(skolem0006,X3207)|~placename(skolem0006,X3207)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|in(skolem0001,skolem0005,skolem0004),inference(resolution,[status(thm)],[c1810, c306])).
% 4.30/4.51  cnf(c1963,plain,~actual_world(skolem0006)|~of(skolem0006,X3209,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3209)|~placename(skolem0006,X3209)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3210)|~white(skolem0006,X3210)|~dirty(skolem0006,X3210)|~old(skolem0006,X3210)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3210)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|in(skolem0001,skolem0005,skolem0004),inference(factor,[status(thm)],[c1862])).
% 4.30/4.51  cnf(c72,negated_conjecture,of(skolem0001,skolem0003,skolem0004)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c1852,plain,~actual_world(skolem0006)|~of(skolem0006,X3196,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3196)|~placename(skolem0006,X3196)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3194)|~white(skolem0006,X3194)|~dirty(skolem0006,X3194)|~old(skolem0006,X3194)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3194)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~of(skolem0006,X3195,skolem0009)|~hollywood_placename(skolem0006,X3195)|~placename(skolem0006,X3195)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|of(skolem0001,skolem0003,skolem0004),inference(resolution,[status(thm)],[c1810, c72])).
% 4.30/4.51  cnf(c1962,plain,~actual_world(skolem0006)|~of(skolem0006,X3197,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3197)|~placename(skolem0006,X3197)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3198)|~white(skolem0006,X3198)|~dirty(skolem0006,X3198)|~old(skolem0006,X3198)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3198)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|of(skolem0001,skolem0003,skolem0004),inference(factor,[status(thm)],[c1852])).
% 4.30/4.51  cnf(c90,negated_conjecture,city(skolem0001,skolem0004)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c1879,plain,~actual_world(skolem0006)|~of(skolem0006,X3175,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3175)|~placename(skolem0006,X3175)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3173)|~white(skolem0006,X3173)|~dirty(skolem0006,X3173)|~old(skolem0006,X3173)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3173)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~of(skolem0006,X3174,skolem0009)|~hollywood_placename(skolem0006,X3174)|~placename(skolem0006,X3174)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|city(skolem0001,skolem0004),inference(resolution,[status(thm)],[c1810, c90])).
% 4.30/4.51  cnf(c1961,plain,~actual_world(skolem0006)|~of(skolem0006,X3177,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3177)|~placename(skolem0006,X3177)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3176)|~white(skolem0006,X3176)|~dirty(skolem0006,X3176)|~old(skolem0006,X3176)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3176)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|city(skolem0001,skolem0004),inference(factor,[status(thm)],[c1879])).
% 4.30/4.51  cnf(c216,negated_conjecture,event(skolem0001,skolem0005)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c1873,plain,~actual_world(skolem0006)|~of(skolem0006,X3157,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3157)|~placename(skolem0006,X3157)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3155)|~white(skolem0006,X3155)|~dirty(skolem0006,X3155)|~old(skolem0006,X3155)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3155)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~of(skolem0006,X3156,skolem0009)|~hollywood_placename(skolem0006,X3156)|~placename(skolem0006,X3156)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|event(skolem0001,skolem0005),inference(resolution,[status(thm)],[c1810, c216])).
% 4.30/4.51  cnf(c1960,plain,~actual_world(skolem0006)|~of(skolem0006,X3165,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3165)|~placename(skolem0006,X3165)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3166)|~white(skolem0006,X3166)|~dirty(skolem0006,X3166)|~old(skolem0006,X3166)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3166)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|event(skolem0001,skolem0005),inference(factor,[status(thm)],[c1873])).
% 4.30/4.51  cnf(c180,negated_conjecture,dirty(skolem0001,skolem0004)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c1869,plain,~actual_world(skolem0006)|~of(skolem0006,X3146,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3146)|~placename(skolem0006,X3146)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3144)|~white(skolem0006,X3144)|~dirty(skolem0006,X3144)|~old(skolem0006,X3144)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3144)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~of(skolem0006,X3145,skolem0009)|~hollywood_placename(skolem0006,X3145)|~placename(skolem0006,X3145)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|dirty(skolem0001,skolem0004),inference(resolution,[status(thm)],[c1810, c180])).
% 4.30/4.51  cnf(c1959,plain,~actual_world(skolem0006)|~of(skolem0006,X3148,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3148)|~placename(skolem0006,X3148)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3147)|~white(skolem0006,X3147)|~dirty(skolem0006,X3147)|~old(skolem0006,X3147)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3147)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|dirty(skolem0001,skolem0004),inference(factor,[status(thm)],[c1869])).
% 4.30/4.51  cnf(c144,negated_conjecture,chevy(skolem0001,skolem0004)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c1867,plain,~actual_world(skolem0006)|~of(skolem0006,X3131,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3131)|~placename(skolem0006,X3131)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3129)|~white(skolem0006,X3129)|~dirty(skolem0006,X3129)|~old(skolem0006,X3129)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3129)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~of(skolem0006,X3130,skolem0009)|~hollywood_placename(skolem0006,X3130)|~placename(skolem0006,X3130)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|chevy(skolem0001,skolem0004),inference(resolution,[status(thm)],[c1810, c144])).
% 4.30/4.51  cnf(c1958,plain,~actual_world(skolem0006)|~of(skolem0006,X3132,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3132)|~placename(skolem0006,X3132)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3133)|~white(skolem0006,X3133)|~dirty(skolem0006,X3133)|~old(skolem0006,X3133)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3133)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|chevy(skolem0001,skolem0004),inference(factor,[status(thm)],[c1867])).
% 4.30/4.51  cnf(c54,negated_conjecture,lonely(skolem0001,skolem0002)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c1866,plain,~actual_world(skolem0006)|~of(skolem0006,X3126,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3126)|~placename(skolem0006,X3126)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3124)|~white(skolem0006,X3124)|~dirty(skolem0006,X3124)|~old(skolem0006,X3124)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3124)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~of(skolem0006,X3125,skolem0009)|~hollywood_placename(skolem0006,X3125)|~placename(skolem0006,X3125)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|lonely(skolem0001,skolem0002),inference(resolution,[status(thm)],[c1810, c54])).
% 4.30/4.51  cnf(c1957,plain,~actual_world(skolem0006)|~of(skolem0006,X3128,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3128)|~placename(skolem0006,X3128)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3127)|~white(skolem0006,X3127)|~dirty(skolem0006,X3127)|~old(skolem0006,X3127)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3127)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|lonely(skolem0001,skolem0002),inference(factor,[status(thm)],[c1866])).
% 4.30/4.51  cnf(c162,negated_conjecture,white(skolem0001,skolem0004)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c1864,plain,~actual_world(skolem0006)|~of(skolem0006,X3111,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3111)|~placename(skolem0006,X3111)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3109)|~white(skolem0006,X3109)|~dirty(skolem0006,X3109)|~old(skolem0006,X3109)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3109)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~of(skolem0006,X3110,skolem0009)|~hollywood_placename(skolem0006,X3110)|~placename(skolem0006,X3110)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|white(skolem0001,skolem0004),inference(resolution,[status(thm)],[c1810, c162])).
% 4.30/4.51  cnf(c1956,plain,~actual_world(skolem0006)|~of(skolem0006,X3112,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3112)|~placename(skolem0006,X3112)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3113)|~white(skolem0006,X3113)|~dirty(skolem0006,X3113)|~old(skolem0006,X3113)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3113)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|white(skolem0001,skolem0004),inference(factor,[status(thm)],[c1864])).
% 4.30/4.51  cnf(c108,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c1863,plain,~actual_world(skolem0006)|~of(skolem0006,X3106,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3106)|~placename(skolem0006,X3106)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3104)|~white(skolem0006,X3104)|~dirty(skolem0006,X3104)|~old(skolem0006,X3104)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3104)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~of(skolem0006,X3105,skolem0009)|~hollywood_placename(skolem0006,X3105)|~placename(skolem0006,X3105)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|hollywood_placename(skolem0001,skolem0003),inference(resolution,[status(thm)],[c1810, c108])).
% 4.30/4.51  cnf(c1955,plain,~actual_world(skolem0006)|~of(skolem0006,X3108,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3108)|~placename(skolem0006,X3108)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3107)|~white(skolem0006,X3107)|~dirty(skolem0006,X3107)|~old(skolem0006,X3107)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3107)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|hollywood_placename(skolem0001,skolem0003),inference(factor,[status(thm)],[c1863])).
% 4.30/4.51  cnf(c252,negated_conjecture,present(skolem0001,skolem0005)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c1860,plain,~actual_world(skolem0006)|~of(skolem0006,X3091,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3091)|~placename(skolem0006,X3091)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3089)|~white(skolem0006,X3089)|~dirty(skolem0006,X3089)|~old(skolem0006,X3089)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3089)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~of(skolem0006,X3090,skolem0009)|~hollywood_placename(skolem0006,X3090)|~placename(skolem0006,X3090)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|present(skolem0001,skolem0005),inference(resolution,[status(thm)],[c1810, c252])).
% 4.30/4.51  cnf(c1954,plain,~actual_world(skolem0006)|~of(skolem0006,X3093,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3093)|~placename(skolem0006,X3093)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3092)|~white(skolem0006,X3092)|~dirty(skolem0006,X3092)|~old(skolem0006,X3092)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3092)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|present(skolem0001,skolem0005),inference(factor,[status(thm)],[c1860])).
% 4.30/4.51  cnf(c126,negated_conjecture,placename(skolem0001,skolem0003)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c1858,plain,~actual_world(skolem0006)|~of(skolem0006,X3076,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3076)|~placename(skolem0006,X3076)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3074)|~white(skolem0006,X3074)|~dirty(skolem0006,X3074)|~old(skolem0006,X3074)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3074)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~of(skolem0006,X3075,skolem0009)|~hollywood_placename(skolem0006,X3075)|~placename(skolem0006,X3075)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|placename(skolem0001,skolem0003),inference(resolution,[status(thm)],[c1810, c126])).
% 4.30/4.51  cnf(c1953,plain,~actual_world(skolem0006)|~of(skolem0006,X3085,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3085)|~placename(skolem0006,X3085)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3084)|~white(skolem0006,X3084)|~dirty(skolem0006,X3084)|~old(skolem0006,X3084)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3084)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|placename(skolem0001,skolem0003),inference(factor,[status(thm)],[c1858])).
% 4.30/4.51  cnf(c198,negated_conjecture,old(skolem0001,skolem0004)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c1857,plain,~actual_world(skolem0006)|~of(skolem0006,X3071,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3071)|~placename(skolem0006,X3071)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3069)|~white(skolem0006,X3069)|~dirty(skolem0006,X3069)|~old(skolem0006,X3069)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3069)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~of(skolem0006,X3070,skolem0009)|~hollywood_placename(skolem0006,X3070)|~placename(skolem0006,X3070)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|old(skolem0001,skolem0004),inference(resolution,[status(thm)],[c1810, c198])).
% 4.30/4.51  cnf(c1952,plain,~actual_world(skolem0006)|~of(skolem0006,X3073,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3073)|~placename(skolem0006,X3073)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3072)|~white(skolem0006,X3072)|~dirty(skolem0006,X3072)|~old(skolem0006,X3072)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3072)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|old(skolem0001,skolem0004),inference(factor,[status(thm)],[c1857])).
% 4.30/4.51  cnf(c36,negated_conjecture,street(skolem0001,skolem0002)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c1856,plain,~actual_world(skolem0006)|~of(skolem0006,X3066,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3066)|~placename(skolem0006,X3066)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3064)|~white(skolem0006,X3064)|~dirty(skolem0006,X3064)|~old(skolem0006,X3064)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3064)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~of(skolem0006,X3065,skolem0009)|~hollywood_placename(skolem0006,X3065)|~placename(skolem0006,X3065)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|street(skolem0001,skolem0002),inference(resolution,[status(thm)],[c1810, c36])).
% 4.30/4.51  cnf(c1951,plain,~actual_world(skolem0006)|~of(skolem0006,X3067,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3067)|~placename(skolem0006,X3067)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3068)|~white(skolem0006,X3068)|~dirty(skolem0006,X3068)|~old(skolem0006,X3068)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3068)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|street(skolem0001,skolem0002),inference(factor,[status(thm)],[c1856])).
% 4.30/4.51  cnf(c270,negated_conjecture,barrel(skolem0001,skolem0005)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c1850,plain,~actual_world(skolem0006)|~of(skolem0006,X3045,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3045)|~placename(skolem0006,X3045)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3043)|~white(skolem0006,X3043)|~dirty(skolem0006,X3043)|~old(skolem0006,X3043)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3043)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~of(skolem0006,X3044,skolem0009)|~hollywood_placename(skolem0006,X3044)|~placename(skolem0006,X3044)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|barrel(skolem0001,skolem0005),inference(resolution,[status(thm)],[c1810, c270])).
% 4.30/4.51  cnf(c1950,plain,~actual_world(skolem0006)|~of(skolem0006,X3046,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3046)|~placename(skolem0006,X3046)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3047)|~white(skolem0006,X3047)|~dirty(skolem0006,X3047)|~old(skolem0006,X3047)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3047)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|barrel(skolem0001,skolem0005),inference(factor,[status(thm)],[c1850])).
% 4.30/4.51  cnf(c18,negated_conjecture,actual_world(skolem0001)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c1849,plain,~actual_world(skolem0006)|~of(skolem0006,X3027,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3027)|~placename(skolem0006,X3027)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3025)|~white(skolem0006,X3025)|~dirty(skolem0006,X3025)|~old(skolem0006,X3025)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3025)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~of(skolem0006,X3026,skolem0009)|~hollywood_placename(skolem0006,X3026)|~placename(skolem0006,X3026)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|actual_world(skolem0001),inference(resolution,[status(thm)],[c1810, c18])).
% 4.30/4.51  cnf(c1949,plain,~actual_world(skolem0006)|~of(skolem0006,X3029,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3029)|~placename(skolem0006,X3029)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3028)|~white(skolem0006,X3028)|~dirty(skolem0006,X3028)|~old(skolem0006,X3028)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3028)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|actual_world(skolem0001),inference(factor,[status(thm)],[c1849])).
% 4.30/4.51  cnf(c1845,plain,~actual_world(X2818)|~of(X2818,X2817,X2820)|~city(X2818,X2820)|~hollywood_placename(X2818,X2817)|~placename(X2818,X2817)|~street(X2818,X2820)|~lonely(X2818,X2820)|~chevy(X2818,X2820)|~white(X2818,X2820)|~dirty(X2818,X2820)|~old(X2818,X2820)|~event(X2818,X2816)|~agent(X2818,X2816,X2820)|~present(X2818,X2816)|~barrel(X2818,X2816)|~down(X2818,X2816,X2820)|~in(X2818,X2816,X2820)|~of(X2818,X2819,X2820)|~hollywood_placename(X2818,X2819)|~placename(X2818,X2819),inference(factor,[status(thm)],[c1810])).
% 4.30/4.51  cnf(c1880,plain,~actual_world(X2821)|~of(X2821,X2822,X2824)|~city(X2821,X2824)|~hollywood_placename(X2821,X2822)|~placename(X2821,X2822)|~street(X2821,X2824)|~lonely(X2821,X2824)|~chevy(X2821,X2824)|~white(X2821,X2824)|~dirty(X2821,X2824)|~old(X2821,X2824)|~event(X2821,X2823)|~agent(X2821,X2823,X2824)|~present(X2821,X2823)|~barrel(X2821,X2823)|~down(X2821,X2823,X2824)|~in(X2821,X2823,X2824),inference(factor,[status(thm)],[c1845])).
% 4.30/4.51  cnf(c309,negated_conjecture,in(skolem0001,skolem0005,skolem0004)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c310,negated_conjecture,in(skolem0001,skolem0005,skolem0004)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c311,negated_conjecture,in(skolem0001,skolem0005,skolem0004)|~actual_world(X133)|~street(X133,X135)|~lonely(X133,X135)|~of(X133,X136,X132)|~city(X133,X132)|~hollywood_placename(X133,X136)|~placename(X133,X136)|~chevy(X133,X132)|~white(X133,X132)|~dirty(X133,X132)|~old(X133,X132)|~event(X133,X134)|~agent(X133,X134,X132)|~present(X133,X134)|~barrel(X133,X134)|~down(X133,X134,X135)|~in(X133,X134,X132),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c1083,plain,in(skolem0001,skolem0005,skolem0004)|~actual_world(skolem0006)|~street(skolem0006,X612)|~lonely(skolem0006,X612)|~of(skolem0006,X611,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X611)|~placename(skolem0006,X611)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,X612),inference(resolution,[status(thm)],[c311, c310])).
% 4.30/4.51  cnf(c1805,plain,in(skolem0001,skolem0005,skolem0004)|~actual_world(skolem0006)|~street(skolem0006,skolem0008)|~lonely(skolem0006,skolem0008)|~of(skolem0006,X613,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X613)|~placename(skolem0006,X613)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c1083, c309])).
% 4.30/4.51  cnf(c291,negated_conjecture,down(skolem0001,skolem0005,skolem0002)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c292,negated_conjecture,down(skolem0001,skolem0005,skolem0002)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c293,negated_conjecture,down(skolem0001,skolem0005,skolem0002)|~actual_world(X103)|~street(X103,X105)|~lonely(X103,X105)|~of(X103,X106,X102)|~city(X103,X102)|~hollywood_placename(X103,X106)|~placename(X103,X106)|~chevy(X103,X102)|~white(X103,X102)|~dirty(X103,X102)|~old(X103,X102)|~event(X103,X104)|~agent(X103,X104,X102)|~present(X103,X104)|~barrel(X103,X104)|~down(X103,X104,X105)|~in(X103,X104,X102),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c883,plain,down(skolem0001,skolem0005,skolem0002)|~actual_world(skolem0006)|~street(skolem0006,X582)|~lonely(skolem0006,X582)|~of(skolem0006,X581,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X581)|~placename(skolem0006,X581)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,X582),inference(resolution,[status(thm)],[c293, c292])).
% 4.30/4.51  cnf(c1789,plain,down(skolem0001,skolem0005,skolem0002)|~actual_world(skolem0006)|~street(skolem0006,skolem0008)|~lonely(skolem0006,skolem0008)|~of(skolem0006,X583,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X583)|~placename(skolem0006,X583)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c883, c291])).
% 4.30/4.51  cnf(c237,negated_conjecture,agent(skolem0001,skolem0005,skolem0004)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c238,negated_conjecture,agent(skolem0001,skolem0005,skolem0004)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c239,negated_conjecture,agent(skolem0001,skolem0005,skolem0004)|~actual_world(X83)|~street(X83,X85)|~lonely(X83,X85)|~of(X83,X86,X82)|~city(X83,X82)|~hollywood_placename(X83,X86)|~placename(X83,X86)|~chevy(X83,X82)|~white(X83,X82)|~dirty(X83,X82)|~old(X83,X82)|~event(X83,X84)|~agent(X83,X84,X82)|~present(X83,X84)|~barrel(X83,X84)|~down(X83,X84,X85)|~in(X83,X84,X82),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c528,plain,agent(skolem0001,skolem0005,skolem0004)|~actual_world(skolem0006)|~street(skolem0006,X519)|~lonely(skolem0006,X519)|~of(skolem0006,X520,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X520)|~placename(skolem0006,X520)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,X519),inference(resolution,[status(thm)],[c239, c238])).
% 4.30/4.51  cnf(c1762,plain,agent(skolem0001,skolem0005,skolem0004)|~actual_world(skolem0006)|~street(skolem0006,skolem0008)|~lonely(skolem0006,skolem0008)|~of(skolem0006,X521,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X521)|~placename(skolem0006,X521)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c528, c237])).
% 4.30/4.51  cnf(c75,negated_conjecture,of(skolem0001,skolem0003,skolem0004)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c76,negated_conjecture,of(skolem0001,skolem0003,skolem0004)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c77,negated_conjecture,of(skolem0001,skolem0003,skolem0004)|~actual_world(X38)|~street(X38,X40)|~lonely(X38,X40)|~of(X38,X41,X37)|~city(X38,X37)|~hollywood_placename(X38,X41)|~placename(X38,X41)|~chevy(X38,X37)|~white(X38,X37)|~dirty(X38,X37)|~old(X38,X37)|~event(X38,X39)|~agent(X38,X39,X37)|~present(X38,X39)|~barrel(X38,X39)|~down(X38,X39,X40)|~in(X38,X39,X37),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c345,plain,of(skolem0001,skolem0003,skolem0004)|~actual_world(skolem0006)|~street(skolem0006,X329)|~lonely(skolem0006,X329)|~of(skolem0006,X328,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X328)|~placename(skolem0006,X328)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,X329),inference(resolution,[status(thm)],[c77, c76])).
% 4.30/4.51  cnf(c1742,plain,of(skolem0001,skolem0003,skolem0004)|~actual_world(skolem0006)|~street(skolem0006,skolem0008)|~lonely(skolem0006,skolem0008)|~of(skolem0006,X330,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X330)|~placename(skolem0006,X330)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c345, c75])).
% 4.30/4.51  cnf(c328,negated_conjecture,~actual_world(X189)|~of(X189,X190,X191)|~city(X189,X191)|~hollywood_placename(X189,X190)|~placename(X189,X190)|~street(X189,X191)|~lonely(X189,X191)|~chevy(X189,X188)|~white(X189,X188)|~dirty(X189,X188)|~old(X189,X188)|~event(X189,X187)|~agent(X189,X187,X188)|~present(X189,X187)|~barrel(X189,X187)|~down(X189,X187,X191)|~in(X189,X187,X191)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c1465,plain,~actual_world(skolem0001)|~of(skolem0001,X324,skolem0004)|~city(skolem0001,skolem0004)|~hollywood_placename(skolem0001,X324)|~placename(skolem0001,X324)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,X323)|~white(skolem0001,X323)|~dirty(skolem0001,X323)|~old(skolem0001,X323)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X323)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,skolem0004)|in(skolem0006,skolem0010,skolem0008),inference(resolution,[status(thm)],[c328, c310])).
% 4.30/4.51  cnf(c327,negated_conjecture,~actual_world(X184)|~of(X184,X185,X186)|~city(X184,X186)|~hollywood_placename(X184,X185)|~placename(X184,X185)|~street(X184,X186)|~lonely(X184,X186)|~chevy(X184,X183)|~white(X184,X183)|~dirty(X184,X183)|~old(X184,X183)|~event(X184,X182)|~agent(X184,X182,X183)|~present(X184,X182)|~barrel(X184,X182)|~down(X184,X182,X186)|~in(X184,X182,X186)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c1450,plain,~actual_world(skolem0001)|~of(skolem0001,X322,skolem0004)|~city(skolem0001,skolem0004)|~hollywood_placename(skolem0001,X322)|~placename(skolem0001,X322)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,X321)|~white(skolem0001,X321)|~dirty(skolem0001,X321)|~old(skolem0001,X321)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X321)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,skolem0004)|down(skolem0006,skolem0010,skolem0008),inference(resolution,[status(thm)],[c327, c309])).
% 4.30/4.51  cnf(c324,negated_conjecture,~actual_world(X179)|~of(X179,X180,X181)|~city(X179,X181)|~hollywood_placename(X179,X180)|~placename(X179,X180)|~street(X179,X181)|~lonely(X179,X181)|~chevy(X179,X178)|~white(X179,X178)|~dirty(X179,X178)|~old(X179,X178)|~event(X179,X177)|~agent(X179,X177,X178)|~present(X179,X177)|~barrel(X179,X177)|~down(X179,X177,X181)|~in(X179,X177,X181)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c1405,plain,~actual_world(skolem0001)|~of(skolem0001,X317,skolem0004)|~city(skolem0001,skolem0004)|~hollywood_placename(skolem0001,X317)|~placename(skolem0001,X317)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,X318)|~white(skolem0001,X318)|~dirty(skolem0001,X318)|~old(skolem0001,X318)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X318)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,skolem0004)|agent(skolem0006,skolem0010,skolem0009),inference(resolution,[status(thm)],[c324, c306])).
% 4.30/4.51  cnf(c295,negated_conjecture,in(skolem0001,skolem0005,skolem0004)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c313,negated_conjecture,~actual_world(X164)|~of(X164,X165,X166)|~city(X164,X166)|~hollywood_placename(X164,X165)|~placename(X164,X165)|~street(X164,X166)|~lonely(X164,X166)|~chevy(X164,X163)|~white(X164,X163)|~dirty(X164,X163)|~old(X164,X163)|~event(X164,X162)|~agent(X164,X162,X163)|~present(X164,X162)|~barrel(X164,X162)|~down(X164,X162,X166)|~in(X164,X162,X166)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c1293,plain,~actual_world(skolem0001)|~of(skolem0001,X316,skolem0004)|~city(skolem0001,skolem0004)|~hollywood_placename(skolem0001,X316)|~placename(skolem0001,X316)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,X315)|~white(skolem0001,X315)|~dirty(skolem0001,X315)|~old(skolem0001,X315)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X315)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,skolem0004)|of(skolem0006,skolem0007,skolem0008),inference(resolution,[status(thm)],[c313, c295])).
% 4.30/4.51  cnf(c273,negated_conjecture,barrel(skolem0001,skolem0005)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c274,negated_conjecture,barrel(skolem0001,skolem0005)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c275,negated_conjecture,barrel(skolem0001,skolem0005)|~actual_world(X93)|~street(X93,X95)|~lonely(X93,X95)|~of(X93,X96,X92)|~city(X93,X92)|~hollywood_placename(X93,X96)|~placename(X93,X96)|~chevy(X93,X92)|~white(X93,X92)|~dirty(X93,X92)|~old(X93,X92)|~event(X93,X94)|~agent(X93,X94,X92)|~present(X93,X94)|~barrel(X93,X94)|~down(X93,X94,X95)|~in(X93,X94,X92),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c707,plain,barrel(skolem0001,skolem0005)|~actual_world(skolem0006)|~street(skolem0006,X308)|~lonely(skolem0006,X308)|~of(skolem0006,X307,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X307)|~placename(skolem0006,X307)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,X308),inference(resolution,[status(thm)],[c275, c274])).
% 4.30/4.51  cnf(c1740,plain,barrel(skolem0001,skolem0005)|~actual_world(skolem0006)|~street(skolem0006,skolem0008)|~lonely(skolem0006,skolem0008)|~of(skolem0006,X311,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X311)|~placename(skolem0006,X311)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c707, c273])).
% 4.30/4.51  cnf(c255,negated_conjecture,present(skolem0001,skolem0005)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c256,negated_conjecture,present(skolem0001,skolem0005)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c257,negated_conjecture,present(skolem0001,skolem0005)|~actual_world(X88)|~street(X88,X90)|~lonely(X88,X90)|~of(X88,X91,X87)|~city(X88,X87)|~hollywood_placename(X88,X91)|~placename(X88,X91)|~chevy(X88,X87)|~white(X88,X87)|~dirty(X88,X87)|~old(X88,X87)|~event(X88,X89)|~agent(X88,X89,X87)|~present(X88,X89)|~barrel(X88,X89)|~down(X88,X89,X90)|~in(X88,X89,X87),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c619,plain,present(skolem0001,skolem0005)|~actual_world(skolem0006)|~street(skolem0006,X304)|~lonely(skolem0006,X304)|~of(skolem0006,X303,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X303)|~placename(skolem0006,X303)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,X304),inference(resolution,[status(thm)],[c257, c256])).
% 4.30/4.51  cnf(c1710,plain,present(skolem0001,skolem0005)|~actual_world(skolem0006)|~street(skolem0006,skolem0008)|~lonely(skolem0006,skolem0008)|~of(skolem0006,X305,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X305)|~placename(skolem0006,X305)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c619, c255])).
% 4.30/4.51  cnf(c219,negated_conjecture,event(skolem0001,skolem0005)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c220,negated_conjecture,event(skolem0001,skolem0005)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c221,negated_conjecture,event(skolem0001,skolem0005)|~actual_world(X78)|~street(X78,X80)|~lonely(X78,X80)|~of(X78,X81,X77)|~city(X78,X77)|~hollywood_placename(X78,X81)|~placename(X78,X81)|~chevy(X78,X77)|~white(X78,X77)|~dirty(X78,X77)|~old(X78,X77)|~event(X78,X79)|~agent(X78,X79,X77)|~present(X78,X79)|~barrel(X78,X79)|~down(X78,X79,X80)|~in(X78,X79,X77),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c482,plain,event(skolem0001,skolem0005)|~actual_world(skolem0006)|~street(skolem0006,X298)|~lonely(skolem0006,X298)|~of(skolem0006,X297,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X297)|~placename(skolem0006,X297)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,X298),inference(resolution,[status(thm)],[c221, c220])).
% 4.30/4.51  cnf(c1707,plain,event(skolem0001,skolem0005)|~actual_world(skolem0006)|~street(skolem0006,skolem0008)|~lonely(skolem0006,skolem0008)|~of(skolem0006,X299,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X299)|~placename(skolem0006,X299)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c482, c219])).
% 4.30/4.51  cnf(c201,negated_conjecture,old(skolem0001,skolem0004)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c202,negated_conjecture,old(skolem0001,skolem0004)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c203,negated_conjecture,old(skolem0001,skolem0004)|~actual_world(X73)|~street(X73,X75)|~lonely(X73,X75)|~of(X73,X76,X72)|~city(X73,X72)|~hollywood_placename(X73,X76)|~placename(X73,X76)|~chevy(X73,X72)|~white(X73,X72)|~dirty(X73,X72)|~old(X73,X72)|~event(X73,X74)|~agent(X73,X74,X72)|~present(X73,X74)|~barrel(X73,X74)|~down(X73,X74,X75)|~in(X73,X74,X72),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.51  cnf(c466,plain,old(skolem0001,skolem0004)|~actual_world(skolem0006)|~street(skolem0006,X293)|~lonely(skolem0006,X293)|~of(skolem0006,X294,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X294)|~placename(skolem0006,X294)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,X293),inference(resolution,[status(thm)],[c203, c202])).
% 4.30/4.52  cnf(c1675,plain,old(skolem0001,skolem0004)|~actual_world(skolem0006)|~street(skolem0006,skolem0008)|~lonely(skolem0006,skolem0008)|~of(skolem0006,X295,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X295)|~placename(skolem0006,X295)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c466, c201])).
% 4.30/4.52  cnf(c183,negated_conjecture,dirty(skolem0001,skolem0004)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c184,negated_conjecture,dirty(skolem0001,skolem0004)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c185,negated_conjecture,dirty(skolem0001,skolem0004)|~actual_world(X68)|~street(X68,X70)|~lonely(X68,X70)|~of(X68,X71,X67)|~city(X68,X67)|~hollywood_placename(X68,X71)|~placename(X68,X71)|~chevy(X68,X67)|~white(X68,X67)|~dirty(X68,X67)|~old(X68,X67)|~event(X68,X69)|~agent(X68,X69,X67)|~present(X68,X69)|~barrel(X68,X69)|~down(X68,X69,X70)|~in(X68,X69,X67),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c447,plain,dirty(skolem0001,skolem0004)|~actual_world(skolem0006)|~street(skolem0006,X288)|~lonely(skolem0006,X288)|~of(skolem0006,X287,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X287)|~placename(skolem0006,X287)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,X288),inference(resolution,[status(thm)],[c185, c184])).
% 4.30/4.52  cnf(c1662,plain,dirty(skolem0001,skolem0004)|~actual_world(skolem0006)|~street(skolem0006,skolem0008)|~lonely(skolem0006,skolem0008)|~of(skolem0006,X289,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X289)|~placename(skolem0006,X289)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c447, c183])).
% 4.30/4.52  cnf(c165,negated_conjecture,white(skolem0001,skolem0004)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c166,negated_conjecture,white(skolem0001,skolem0004)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c167,negated_conjecture,white(skolem0001,skolem0004)|~actual_world(X63)|~street(X63,X65)|~lonely(X63,X65)|~of(X63,X66,X62)|~city(X63,X62)|~hollywood_placename(X63,X66)|~placename(X63,X66)|~chevy(X63,X62)|~white(X63,X62)|~dirty(X63,X62)|~old(X63,X62)|~event(X63,X64)|~agent(X63,X64,X62)|~present(X63,X64)|~barrel(X63,X64)|~down(X63,X64,X65)|~in(X63,X64,X62),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c427,plain,white(skolem0001,skolem0004)|~actual_world(skolem0006)|~street(skolem0006,X281)|~lonely(skolem0006,X281)|~of(skolem0006,X282,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X282)|~placename(skolem0006,X282)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,X281),inference(resolution,[status(thm)],[c167, c166])).
% 4.30/4.52  cnf(c1647,plain,white(skolem0001,skolem0004)|~actual_world(skolem0006)|~street(skolem0006,skolem0008)|~lonely(skolem0006,skolem0008)|~of(skolem0006,X285,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X285)|~placename(skolem0006,X285)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c427, c165])).
% 4.30/4.52  cnf(c147,negated_conjecture,chevy(skolem0001,skolem0004)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c148,negated_conjecture,chevy(skolem0001,skolem0004)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c149,negated_conjecture,chevy(skolem0001,skolem0004)|~actual_world(X58)|~street(X58,X60)|~lonely(X58,X60)|~of(X58,X61,X57)|~city(X58,X57)|~hollywood_placename(X58,X61)|~placename(X58,X61)|~chevy(X58,X57)|~white(X58,X57)|~dirty(X58,X57)|~old(X58,X57)|~event(X58,X59)|~agent(X58,X59,X57)|~present(X58,X59)|~barrel(X58,X59)|~down(X58,X59,X60)|~in(X58,X59,X57),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c393,plain,chevy(skolem0001,skolem0004)|~actual_world(skolem0006)|~street(skolem0006,X277)|~lonely(skolem0006,X277)|~of(skolem0006,X278,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X278)|~placename(skolem0006,X278)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,X277),inference(resolution,[status(thm)],[c149, c148])).
% 4.30/4.52  cnf(c1631,plain,chevy(skolem0001,skolem0004)|~actual_world(skolem0006)|~street(skolem0006,skolem0008)|~lonely(skolem0006,skolem0008)|~of(skolem0006,X279,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X279)|~placename(skolem0006,X279)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c393, c147])).
% 4.30/4.52  cnf(c129,negated_conjecture,placename(skolem0001,skolem0003)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c130,negated_conjecture,placename(skolem0001,skolem0003)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c131,negated_conjecture,placename(skolem0001,skolem0003)|~actual_world(X53)|~street(X53,X55)|~lonely(X53,X55)|~of(X53,X56,X52)|~city(X53,X52)|~hollywood_placename(X53,X56)|~placename(X53,X56)|~chevy(X53,X52)|~white(X53,X52)|~dirty(X53,X52)|~old(X53,X52)|~event(X53,X54)|~agent(X53,X54,X52)|~present(X53,X54)|~barrel(X53,X54)|~down(X53,X54,X55)|~in(X53,X54,X52),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c384,plain,placename(skolem0001,skolem0003)|~actual_world(skolem0006)|~street(skolem0006,X271)|~lonely(skolem0006,X271)|~of(skolem0006,X272,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X272)|~placename(skolem0006,X272)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,X271),inference(resolution,[status(thm)],[c131, c130])).
% 4.30/4.52  cnf(c1615,plain,placename(skolem0001,skolem0003)|~actual_world(skolem0006)|~street(skolem0006,skolem0008)|~lonely(skolem0006,skolem0008)|~of(skolem0006,X273,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X273)|~placename(skolem0006,X273)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c384, c129])).
% 4.30/4.52  cnf(c111,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c112,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c113,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|~actual_world(X48)|~street(X48,X50)|~lonely(X48,X50)|~of(X48,X51,X47)|~city(X48,X47)|~hollywood_placename(X48,X51)|~placename(X48,X51)|~chevy(X48,X47)|~white(X48,X47)|~dirty(X48,X47)|~old(X48,X47)|~event(X48,X49)|~agent(X48,X49,X47)|~present(X48,X49)|~barrel(X48,X49)|~down(X48,X49,X50)|~in(X48,X49,X47),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c367,plain,hollywood_placename(skolem0001,skolem0003)|~actual_world(skolem0006)|~street(skolem0006,X268)|~lonely(skolem0006,X268)|~of(skolem0006,X267,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X267)|~placename(skolem0006,X267)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,X268),inference(resolution,[status(thm)],[c113, c112])).
% 4.30/4.52  cnf(c1593,plain,hollywood_placename(skolem0001,skolem0003)|~actual_world(skolem0006)|~street(skolem0006,skolem0008)|~lonely(skolem0006,skolem0008)|~of(skolem0006,X269,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X269)|~placename(skolem0006,X269)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c367, c111])).
% 4.30/4.52  cnf(c93,negated_conjecture,city(skolem0001,skolem0004)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c94,negated_conjecture,city(skolem0001,skolem0004)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c95,negated_conjecture,city(skolem0001,skolem0004)|~actual_world(X43)|~street(X43,X45)|~lonely(X43,X45)|~of(X43,X46,X42)|~city(X43,X42)|~hollywood_placename(X43,X46)|~placename(X43,X46)|~chevy(X43,X42)|~white(X43,X42)|~dirty(X43,X42)|~old(X43,X42)|~event(X43,X44)|~agent(X43,X44,X42)|~present(X43,X44)|~barrel(X43,X44)|~down(X43,X44,X45)|~in(X43,X44,X42),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c354,plain,city(skolem0001,skolem0004)|~actual_world(skolem0006)|~street(skolem0006,X261)|~lonely(skolem0006,X261)|~of(skolem0006,X262,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X262)|~placename(skolem0006,X262)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,X261),inference(resolution,[status(thm)],[c95, c94])).
% 4.30/4.52  cnf(c1582,plain,city(skolem0001,skolem0004)|~actual_world(skolem0006)|~street(skolem0006,skolem0008)|~lonely(skolem0006,skolem0008)|~of(skolem0006,X263,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X263)|~placename(skolem0006,X263)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c354, c93])).
% 4.30/4.52  cnf(c57,negated_conjecture,lonely(skolem0001,skolem0002)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c58,negated_conjecture,lonely(skolem0001,skolem0002)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c59,negated_conjecture,lonely(skolem0001,skolem0002)|~actual_world(X33)|~street(X33,X35)|~lonely(X33,X35)|~of(X33,X36,X32)|~city(X33,X32)|~hollywood_placename(X33,X36)|~placename(X33,X36)|~chevy(X33,X32)|~white(X33,X32)|~dirty(X33,X32)|~old(X33,X32)|~event(X33,X34)|~agent(X33,X34,X32)|~present(X33,X34)|~barrel(X33,X34)|~down(X33,X34,X35)|~in(X33,X34,X32),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c338,plain,lonely(skolem0001,skolem0002)|~actual_world(skolem0006)|~street(skolem0006,X255)|~lonely(skolem0006,X255)|~of(skolem0006,X256,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X256)|~placename(skolem0006,X256)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,X255),inference(resolution,[status(thm)],[c59, c58])).
% 4.30/4.52  cnf(c1561,plain,lonely(skolem0001,skolem0002)|~actual_world(skolem0006)|~street(skolem0006,skolem0008)|~lonely(skolem0006,skolem0008)|~of(skolem0006,X259,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X259)|~placename(skolem0006,X259)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c338, c57])).
% 4.30/4.52  cnf(c308,negated_conjecture,in(skolem0001,skolem0005,skolem0004)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c326,negated_conjecture,~actual_world(X174)|~of(X174,X175,X176)|~city(X174,X176)|~hollywood_placename(X174,X175)|~placename(X174,X175)|~street(X174,X176)|~lonely(X174,X176)|~chevy(X174,X173)|~white(X174,X173)|~dirty(X174,X173)|~old(X174,X173)|~event(X174,X172)|~agent(X174,X172,X173)|~present(X174,X172)|~barrel(X174,X172)|~down(X174,X172,X176)|~in(X174,X172,X176)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c1365,plain,~actual_world(skolem0001)|~of(skolem0001,X237,skolem0004)|~city(skolem0001,skolem0004)|~hollywood_placename(skolem0001,X237)|~placename(skolem0001,X237)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,X236)|~white(skolem0001,X236)|~dirty(skolem0001,X236)|~old(skolem0001,X236)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X236)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,skolem0004)|barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c326, c308])).
% 4.30/4.52  cnf(c307,negated_conjecture,in(skolem0001,skolem0005,skolem0004)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c325,negated_conjecture,~actual_world(X169)|~of(X169,X170,X171)|~city(X169,X171)|~hollywood_placename(X169,X170)|~placename(X169,X170)|~street(X169,X171)|~lonely(X169,X171)|~chevy(X169,X168)|~white(X169,X168)|~dirty(X169,X168)|~old(X169,X168)|~event(X169,X167)|~agent(X169,X167,X168)|~present(X169,X167)|~barrel(X169,X167)|~down(X169,X167,X171)|~in(X169,X167,X171)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c1316,plain,~actual_world(skolem0001)|~of(skolem0001,X233,skolem0004)|~city(skolem0001,skolem0004)|~hollywood_placename(skolem0001,X233)|~placename(skolem0001,X233)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,X232)|~white(skolem0001,X232)|~dirty(skolem0001,X232)|~old(skolem0001,X232)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X232)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,skolem0004)|present(skolem0006,skolem0010),inference(resolution,[status(thm)],[c325, c307])).
% 4.30/4.52  cnf(c305,negated_conjecture,in(skolem0001,skolem0005,skolem0004)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c323,negated_conjecture,~actual_world(X159)|~of(X159,X160,X161)|~city(X159,X161)|~hollywood_placename(X159,X160)|~placename(X159,X160)|~street(X159,X161)|~lonely(X159,X161)|~chevy(X159,X158)|~white(X159,X158)|~dirty(X159,X158)|~old(X159,X158)|~event(X159,X157)|~agent(X159,X157,X158)|~present(X159,X157)|~barrel(X159,X157)|~down(X159,X157,X161)|~in(X159,X157,X161)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c1252,plain,~actual_world(skolem0001)|~of(skolem0001,X231,skolem0004)|~city(skolem0001,skolem0004)|~hollywood_placename(skolem0001,X231)|~placename(skolem0001,X231)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,X230)|~white(skolem0001,X230)|~dirty(skolem0001,X230)|~old(skolem0001,X230)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X230)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,skolem0004)|event(skolem0006,skolem0010),inference(resolution,[status(thm)],[c323, c305])).
% 4.30/4.52  cnf(c304,negated_conjecture,in(skolem0001,skolem0005,skolem0004)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c322,negated_conjecture,~actual_world(X154)|~of(X154,X155,X156)|~city(X154,X156)|~hollywood_placename(X154,X155)|~placename(X154,X155)|~street(X154,X156)|~lonely(X154,X156)|~chevy(X154,X153)|~white(X154,X153)|~dirty(X154,X153)|~old(X154,X153)|~event(X154,X152)|~agent(X154,X152,X153)|~present(X154,X152)|~barrel(X154,X152)|~down(X154,X152,X156)|~in(X154,X152,X156)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c1221,plain,~actual_world(skolem0001)|~of(skolem0001,X228,skolem0004)|~city(skolem0001,skolem0004)|~hollywood_placename(skolem0001,X228)|~placename(skolem0001,X228)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,X229)|~white(skolem0001,X229)|~dirty(skolem0001,X229)|~old(skolem0001,X229)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X229)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,skolem0004)|old(skolem0006,skolem0009),inference(resolution,[status(thm)],[c322, c304])).
% 4.30/4.52  cnf(c303,negated_conjecture,in(skolem0001,skolem0005,skolem0004)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c321,negated_conjecture,~actual_world(X149)|~of(X149,X150,X151)|~city(X149,X151)|~hollywood_placename(X149,X150)|~placename(X149,X150)|~street(X149,X151)|~lonely(X149,X151)|~chevy(X149,X148)|~white(X149,X148)|~dirty(X149,X148)|~old(X149,X148)|~event(X149,X147)|~agent(X149,X147,X148)|~present(X149,X147)|~barrel(X149,X147)|~down(X149,X147,X151)|~in(X149,X147,X151)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c1194,plain,~actual_world(skolem0001)|~of(skolem0001,X227,skolem0004)|~city(skolem0001,skolem0004)|~hollywood_placename(skolem0001,X227)|~placename(skolem0001,X227)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,X226)|~white(skolem0001,X226)|~dirty(skolem0001,X226)|~old(skolem0001,X226)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X226)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,skolem0004)|dirty(skolem0006,skolem0009),inference(resolution,[status(thm)],[c321, c303])).
% 4.30/4.52  cnf(c39,negated_conjecture,street(skolem0001,skolem0002)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c40,negated_conjecture,street(skolem0001,skolem0002)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c41,negated_conjecture,street(skolem0001,skolem0002)|~actual_world(X28)|~street(X28,X30)|~lonely(X28,X30)|~of(X28,X31,X27)|~city(X28,X27)|~hollywood_placename(X28,X31)|~placename(X28,X31)|~chevy(X28,X27)|~white(X28,X27)|~dirty(X28,X27)|~old(X28,X27)|~event(X28,X29)|~agent(X28,X29,X27)|~present(X28,X29)|~barrel(X28,X29)|~down(X28,X29,X30)|~in(X28,X29,X27),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c332,plain,street(skolem0001,skolem0002)|~actual_world(skolem0006)|~street(skolem0006,X224)|~lonely(skolem0006,X224)|~of(skolem0006,X223,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X223)|~placename(skolem0006,X223)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,X224),inference(resolution,[status(thm)],[c41, c40])).
% 4.30/4.52  cnf(c1552,plain,street(skolem0001,skolem0002)|~actual_world(skolem0006)|~street(skolem0006,skolem0008)|~lonely(skolem0006,skolem0008)|~of(skolem0006,X225,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X225)|~placename(skolem0006,X225)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c332, c39])).
% 4.30/4.52  cnf(c302,negated_conjecture,in(skolem0001,skolem0005,skolem0004)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c320,negated_conjecture,~actual_world(X144)|~of(X144,X145,X146)|~city(X144,X146)|~hollywood_placename(X144,X145)|~placename(X144,X145)|~street(X144,X146)|~lonely(X144,X146)|~chevy(X144,X143)|~white(X144,X143)|~dirty(X144,X143)|~old(X144,X143)|~event(X144,X142)|~agent(X144,X142,X143)|~present(X144,X142)|~barrel(X144,X142)|~down(X144,X142,X146)|~in(X144,X142,X146)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c1164,plain,~actual_world(skolem0001)|~of(skolem0001,X221,skolem0004)|~city(skolem0001,skolem0004)|~hollywood_placename(skolem0001,X221)|~placename(skolem0001,X221)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,X222)|~white(skolem0001,X222)|~dirty(skolem0001,X222)|~old(skolem0001,X222)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X222)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,skolem0004)|white(skolem0006,skolem0009),inference(resolution,[status(thm)],[c320, c302])).
% 4.30/4.52  cnf(c301,negated_conjecture,in(skolem0001,skolem0005,skolem0004)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c319,negated_conjecture,~actual_world(X139)|~of(X139,X140,X141)|~city(X139,X141)|~hollywood_placename(X139,X140)|~placename(X139,X140)|~street(X139,X141)|~lonely(X139,X141)|~chevy(X139,X138)|~white(X139,X138)|~dirty(X139,X138)|~old(X139,X138)|~event(X139,X137)|~agent(X139,X137,X138)|~present(X139,X137)|~barrel(X139,X137)|~down(X139,X137,X141)|~in(X139,X137,X141)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c1132,plain,~actual_world(skolem0001)|~of(skolem0001,X220,skolem0004)|~city(skolem0001,skolem0004)|~hollywood_placename(skolem0001,X220)|~placename(skolem0001,X220)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,X219)|~white(skolem0001,X219)|~dirty(skolem0001,X219)|~old(skolem0001,X219)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X219)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,skolem0004)|chevy(skolem0006,skolem0009),inference(resolution,[status(thm)],[c319, c301])).
% 4.30/4.52  cnf(c300,negated_conjecture,in(skolem0001,skolem0005,skolem0004)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c318,negated_conjecture,~actual_world(X129)|~of(X129,X130,X131)|~city(X129,X131)|~hollywood_placename(X129,X130)|~placename(X129,X130)|~street(X129,X131)|~lonely(X129,X131)|~chevy(X129,X128)|~white(X129,X128)|~dirty(X129,X128)|~old(X129,X128)|~event(X129,X127)|~agent(X129,X127,X128)|~present(X129,X127)|~barrel(X129,X127)|~down(X129,X127,X131)|~in(X129,X127,X131)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c1045,plain,~actual_world(skolem0001)|~of(skolem0001,X218,skolem0004)|~city(skolem0001,skolem0004)|~hollywood_placename(skolem0001,X218)|~placename(skolem0001,X218)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,X217)|~white(skolem0001,X217)|~dirty(skolem0001,X217)|~old(skolem0001,X217)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X217)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,skolem0004)|lonely(skolem0006,skolem0008),inference(resolution,[status(thm)],[c318, c300])).
% 4.30/4.52  cnf(c299,negated_conjecture,in(skolem0001,skolem0005,skolem0004)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c317,negated_conjecture,~actual_world(X124)|~of(X124,X125,X126)|~city(X124,X126)|~hollywood_placename(X124,X125)|~placename(X124,X125)|~street(X124,X126)|~lonely(X124,X126)|~chevy(X124,X123)|~white(X124,X123)|~dirty(X124,X123)|~old(X124,X123)|~event(X124,X122)|~agent(X124,X122,X123)|~present(X124,X122)|~barrel(X124,X122)|~down(X124,X122,X126)|~in(X124,X122,X126)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c1043,plain,~actual_world(skolem0001)|~of(skolem0001,X216,skolem0004)|~city(skolem0001,skolem0004)|~hollywood_placename(skolem0001,X216)|~placename(skolem0001,X216)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,X215)|~white(skolem0001,X215)|~dirty(skolem0001,X215)|~old(skolem0001,X215)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X215)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,skolem0004)|street(skolem0006,skolem0008),inference(resolution,[status(thm)],[c317, c299])).
% 4.30/4.52  cnf(c298,negated_conjecture,in(skolem0001,skolem0005,skolem0004)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c316,negated_conjecture,~actual_world(X119)|~of(X119,X120,X121)|~city(X119,X121)|~hollywood_placename(X119,X120)|~placename(X119,X120)|~street(X119,X121)|~lonely(X119,X121)|~chevy(X119,X118)|~white(X119,X118)|~dirty(X119,X118)|~old(X119,X118)|~event(X119,X117)|~agent(X119,X117,X118)|~present(X119,X117)|~barrel(X119,X117)|~down(X119,X117,X121)|~in(X119,X117,X121)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c1001,plain,~actual_world(skolem0001)|~of(skolem0001,X214,skolem0004)|~city(skolem0001,skolem0004)|~hollywood_placename(skolem0001,X214)|~placename(skolem0001,X214)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,X213)|~white(skolem0001,X213)|~dirty(skolem0001,X213)|~old(skolem0001,X213)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X213)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,skolem0004)|placename(skolem0006,skolem0007),inference(resolution,[status(thm)],[c316, c298])).
% 4.30/4.52  cnf(c297,negated_conjecture,in(skolem0001,skolem0005,skolem0004)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c315,negated_conjecture,~actual_world(X114)|~of(X114,X115,X116)|~city(X114,X116)|~hollywood_placename(X114,X115)|~placename(X114,X115)|~street(X114,X116)|~lonely(X114,X116)|~chevy(X114,X113)|~white(X114,X113)|~dirty(X114,X113)|~old(X114,X113)|~event(X114,X112)|~agent(X114,X112,X113)|~present(X114,X112)|~barrel(X114,X112)|~down(X114,X112,X116)|~in(X114,X112,X116)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c965,plain,~actual_world(skolem0001)|~of(skolem0001,X210,skolem0004)|~city(skolem0001,skolem0004)|~hollywood_placename(skolem0001,X210)|~placename(skolem0001,X210)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,X209)|~white(skolem0001,X209)|~dirty(skolem0001,X209)|~old(skolem0001,X209)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X209)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,skolem0004)|hollywood_placename(skolem0006,skolem0007),inference(resolution,[status(thm)],[c315, c297])).
% 4.30/4.52  cnf(c296,negated_conjecture,in(skolem0001,skolem0005,skolem0004)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c314,negated_conjecture,~actual_world(X109)|~of(X109,X110,X111)|~city(X109,X111)|~hollywood_placename(X109,X110)|~placename(X109,X110)|~street(X109,X111)|~lonely(X109,X111)|~chevy(X109,X108)|~white(X109,X108)|~dirty(X109,X108)|~old(X109,X108)|~event(X109,X107)|~agent(X109,X107,X108)|~present(X109,X107)|~barrel(X109,X107)|~down(X109,X107,X111)|~in(X109,X107,X111)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c938,plain,~actual_world(skolem0001)|~of(skolem0001,X208,skolem0004)|~city(skolem0001,skolem0004)|~hollywood_placename(skolem0001,X208)|~placename(skolem0001,X208)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,X207)|~white(skolem0001,X207)|~dirty(skolem0001,X207)|~old(skolem0001,X207)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X207)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,skolem0004)|city(skolem0006,skolem0008),inference(resolution,[status(thm)],[c314, c296])).
% 4.30/4.52  cnf(c21,negated_conjecture,actual_world(skolem0001)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c22,negated_conjecture,actual_world(skolem0001)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c23,negated_conjecture,actual_world(skolem0001)|~actual_world(X23)|~street(X23,X25)|~lonely(X23,X25)|~of(X23,X26,X22)|~city(X23,X22)|~hollywood_placename(X23,X26)|~placename(X23,X26)|~chevy(X23,X22)|~white(X23,X22)|~dirty(X23,X22)|~old(X23,X22)|~event(X23,X24)|~agent(X23,X24,X22)|~present(X23,X24)|~barrel(X23,X24)|~down(X23,X24,X25)|~in(X23,X24,X22),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c330,plain,actual_world(skolem0001)|~actual_world(skolem0006)|~street(skolem0006,X204)|~lonely(skolem0006,X204)|~of(skolem0006,X205,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X205)|~placename(skolem0006,X205)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,X204),inference(resolution,[status(thm)],[c23, c22])).
% 4.30/4.52  cnf(c1532,plain,actual_world(skolem0001)|~actual_world(skolem0006)|~street(skolem0006,skolem0008)|~lonely(skolem0006,skolem0008)|~of(skolem0006,X206,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X206)|~placename(skolem0006,X206)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c330, c21])).
% 4.30/4.52  cnf(c294,negated_conjecture,in(skolem0001,skolem0005,skolem0004)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c312,negated_conjecture,~actual_world(X99)|~of(X99,X100,X101)|~city(X99,X101)|~hollywood_placename(X99,X100)|~placename(X99,X100)|~street(X99,X101)|~lonely(X99,X101)|~chevy(X99,X98)|~white(X99,X98)|~dirty(X99,X98)|~old(X99,X98)|~event(X99,X97)|~agent(X99,X97,X98)|~present(X99,X97)|~barrel(X99,X97)|~down(X99,X97,X101)|~in(X99,X97,X101)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c843,plain,~actual_world(skolem0001)|~of(skolem0001,X202,skolem0004)|~city(skolem0001,skolem0004)|~hollywood_placename(skolem0001,X202)|~placename(skolem0001,X202)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,X203)|~white(skolem0001,X203)|~dirty(skolem0001,X203)|~old(skolem0001,X203)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X203)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,skolem0004)|actual_world(skolem0006),inference(resolution,[status(thm)],[c312, c294])).
% 4.30/4.52  cnf(c277,negated_conjecture,down(skolem0001,skolem0005,skolem0002)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c290,negated_conjecture,down(skolem0001,skolem0005,skolem0002)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c289,negated_conjecture,down(skolem0001,skolem0005,skolem0002)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c287,negated_conjecture,down(skolem0001,skolem0005,skolem0002)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c286,negated_conjecture,down(skolem0001,skolem0005,skolem0002)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c285,negated_conjecture,down(skolem0001,skolem0005,skolem0002)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c284,negated_conjecture,down(skolem0001,skolem0005,skolem0002)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c283,negated_conjecture,down(skolem0001,skolem0005,skolem0002)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c282,negated_conjecture,down(skolem0001,skolem0005,skolem0002)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c281,negated_conjecture,down(skolem0001,skolem0005,skolem0002)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c280,negated_conjecture,down(skolem0001,skolem0005,skolem0002)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c279,negated_conjecture,down(skolem0001,skolem0005,skolem0002)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c278,negated_conjecture,down(skolem0001,skolem0005,skolem0002)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c259,negated_conjecture,barrel(skolem0001,skolem0005)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c241,negated_conjecture,present(skolem0001,skolem0005)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c223,negated_conjecture,agent(skolem0001,skolem0005,skolem0004)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c236,negated_conjecture,agent(skolem0001,skolem0005,skolem0004)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c235,negated_conjecture,agent(skolem0001,skolem0005,skolem0004)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c233,negated_conjecture,agent(skolem0001,skolem0005,skolem0004)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c232,negated_conjecture,agent(skolem0001,skolem0005,skolem0004)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c231,negated_conjecture,agent(skolem0001,skolem0005,skolem0004)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c230,negated_conjecture,agent(skolem0001,skolem0005,skolem0004)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c229,negated_conjecture,agent(skolem0001,skolem0005,skolem0004)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c228,negated_conjecture,agent(skolem0001,skolem0005,skolem0004)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c227,negated_conjecture,agent(skolem0001,skolem0005,skolem0004)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c226,negated_conjecture,agent(skolem0001,skolem0005,skolem0004)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c225,negated_conjecture,agent(skolem0001,skolem0005,skolem0004)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c224,negated_conjecture,agent(skolem0001,skolem0005,skolem0004)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c205,negated_conjecture,event(skolem0001,skolem0005)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c187,negated_conjecture,old(skolem0001,skolem0004)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c169,negated_conjecture,dirty(skolem0001,skolem0004)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c151,negated_conjecture,white(skolem0001,skolem0004)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c133,negated_conjecture,chevy(skolem0001,skolem0004)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c115,negated_conjecture,placename(skolem0001,skolem0003)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c97,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c276,negated_conjecture,down(skolem0001,skolem0005,skolem0002)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c272,negated_conjecture,barrel(skolem0001,skolem0005)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c271,negated_conjecture,barrel(skolem0001,skolem0005)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c269,negated_conjecture,barrel(skolem0001,skolem0005)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c268,negated_conjecture,barrel(skolem0001,skolem0005)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c267,negated_conjecture,barrel(skolem0001,skolem0005)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c266,negated_conjecture,barrel(skolem0001,skolem0005)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c79,negated_conjecture,city(skolem0001,skolem0004)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c265,negated_conjecture,barrel(skolem0001,skolem0005)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c264,negated_conjecture,barrel(skolem0001,skolem0005)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c263,negated_conjecture,barrel(skolem0001,skolem0005)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c262,negated_conjecture,barrel(skolem0001,skolem0005)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c261,negated_conjecture,barrel(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c260,negated_conjecture,barrel(skolem0001,skolem0005)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c254,negated_conjecture,present(skolem0001,skolem0005)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c253,negated_conjecture,present(skolem0001,skolem0005)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c251,negated_conjecture,present(skolem0001,skolem0005)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c250,negated_conjecture,present(skolem0001,skolem0005)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c249,negated_conjecture,present(skolem0001,skolem0005)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c248,negated_conjecture,present(skolem0001,skolem0005)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c247,negated_conjecture,present(skolem0001,skolem0005)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c246,negated_conjecture,present(skolem0001,skolem0005)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c245,negated_conjecture,present(skolem0001,skolem0005)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c244,negated_conjecture,present(skolem0001,skolem0005)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c243,negated_conjecture,present(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c242,negated_conjecture,present(skolem0001,skolem0005)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c222,negated_conjecture,agent(skolem0001,skolem0005,skolem0004)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c218,negated_conjecture,event(skolem0001,skolem0005)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c74,negated_conjecture,of(skolem0001,skolem0003,skolem0004)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c217,negated_conjecture,event(skolem0001,skolem0005)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c215,negated_conjecture,event(skolem0001,skolem0005)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c214,negated_conjecture,event(skolem0001,skolem0005)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c213,negated_conjecture,event(skolem0001,skolem0005)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c212,negated_conjecture,event(skolem0001,skolem0005)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c73,negated_conjecture,of(skolem0001,skolem0003,skolem0004)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c211,negated_conjecture,event(skolem0001,skolem0005)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c210,negated_conjecture,event(skolem0001,skolem0005)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c209,negated_conjecture,event(skolem0001,skolem0005)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c208,negated_conjecture,event(skolem0001,skolem0005)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c207,negated_conjecture,event(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c206,negated_conjecture,event(skolem0001,skolem0005)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c200,negated_conjecture,old(skolem0001,skolem0004)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c199,negated_conjecture,old(skolem0001,skolem0004)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c197,negated_conjecture,old(skolem0001,skolem0004)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c196,negated_conjecture,old(skolem0001,skolem0004)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c71,negated_conjecture,of(skolem0001,skolem0003,skolem0004)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c195,negated_conjecture,old(skolem0001,skolem0004)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c194,negated_conjecture,old(skolem0001,skolem0004)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c193,negated_conjecture,old(skolem0001,skolem0004)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c192,negated_conjecture,old(skolem0001,skolem0004)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c191,negated_conjecture,old(skolem0001,skolem0004)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c70,negated_conjecture,of(skolem0001,skolem0003,skolem0004)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c190,negated_conjecture,old(skolem0001,skolem0004)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c189,negated_conjecture,old(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c188,negated_conjecture,old(skolem0001,skolem0004)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c182,negated_conjecture,dirty(skolem0001,skolem0004)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c181,negated_conjecture,dirty(skolem0001,skolem0004)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c69,negated_conjecture,of(skolem0001,skolem0003,skolem0004)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c179,negated_conjecture,dirty(skolem0001,skolem0004)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c178,negated_conjecture,dirty(skolem0001,skolem0004)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c177,negated_conjecture,dirty(skolem0001,skolem0004)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c176,negated_conjecture,dirty(skolem0001,skolem0004)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c175,negated_conjecture,dirty(skolem0001,skolem0004)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c68,negated_conjecture,of(skolem0001,skolem0003,skolem0004)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c174,negated_conjecture,dirty(skolem0001,skolem0004)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c173,negated_conjecture,dirty(skolem0001,skolem0004)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c172,negated_conjecture,dirty(skolem0001,skolem0004)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c171,negated_conjecture,dirty(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c170,negated_conjecture,dirty(skolem0001,skolem0004)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c67,negated_conjecture,of(skolem0001,skolem0003,skolem0004)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c164,negated_conjecture,white(skolem0001,skolem0004)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c163,negated_conjecture,white(skolem0001,skolem0004)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c161,negated_conjecture,white(skolem0001,skolem0004)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c160,negated_conjecture,white(skolem0001,skolem0004)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c159,negated_conjecture,white(skolem0001,skolem0004)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c66,negated_conjecture,of(skolem0001,skolem0003,skolem0004)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c158,negated_conjecture,white(skolem0001,skolem0004)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c157,negated_conjecture,white(skolem0001,skolem0004)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c156,negated_conjecture,white(skolem0001,skolem0004)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c155,negated_conjecture,white(skolem0001,skolem0004)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c154,negated_conjecture,white(skolem0001,skolem0004)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c65,negated_conjecture,of(skolem0001,skolem0003,skolem0004)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c153,negated_conjecture,white(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c152,negated_conjecture,white(skolem0001,skolem0004)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c146,negated_conjecture,chevy(skolem0001,skolem0004)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c145,negated_conjecture,chevy(skolem0001,skolem0004)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c143,negated_conjecture,chevy(skolem0001,skolem0004)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c64,negated_conjecture,of(skolem0001,skolem0003,skolem0004)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c142,negated_conjecture,chevy(skolem0001,skolem0004)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c141,negated_conjecture,chevy(skolem0001,skolem0004)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c140,negated_conjecture,chevy(skolem0001,skolem0004)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c139,negated_conjecture,chevy(skolem0001,skolem0004)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c138,negated_conjecture,chevy(skolem0001,skolem0004)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.52  cnf(c63,negated_conjecture,of(skolem0001,skolem0003,skolem0004)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c137,negated_conjecture,chevy(skolem0001,skolem0004)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c136,negated_conjecture,chevy(skolem0001,skolem0004)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c135,negated_conjecture,chevy(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c134,negated_conjecture,chevy(skolem0001,skolem0004)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c128,negated_conjecture,placename(skolem0001,skolem0003)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c62,negated_conjecture,of(skolem0001,skolem0003,skolem0004)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c127,negated_conjecture,placename(skolem0001,skolem0003)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c125,negated_conjecture,placename(skolem0001,skolem0003)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c124,negated_conjecture,placename(skolem0001,skolem0003)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c123,negated_conjecture,placename(skolem0001,skolem0003)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c122,negated_conjecture,placename(skolem0001,skolem0003)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c61,negated_conjecture,of(skolem0001,skolem0003,skolem0004)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c121,negated_conjecture,placename(skolem0001,skolem0003)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c120,negated_conjecture,placename(skolem0001,skolem0003)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c119,negated_conjecture,placename(skolem0001,skolem0003)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c118,negated_conjecture,placename(skolem0001,skolem0003)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c117,negated_conjecture,placename(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c116,negated_conjecture,placename(skolem0001,skolem0003)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c110,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c109,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c107,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c106,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c105,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c104,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c103,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c102,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c101,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c100,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c99,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c98,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c92,negated_conjecture,city(skolem0001,skolem0004)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c91,negated_conjecture,city(skolem0001,skolem0004)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c89,negated_conjecture,city(skolem0001,skolem0004)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c88,negated_conjecture,city(skolem0001,skolem0004)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c87,negated_conjecture,city(skolem0001,skolem0004)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c86,negated_conjecture,city(skolem0001,skolem0004)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c85,negated_conjecture,city(skolem0001,skolem0004)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c43,negated_conjecture,lonely(skolem0001,skolem0002)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c84,negated_conjecture,city(skolem0001,skolem0004)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c83,negated_conjecture,city(skolem0001,skolem0004)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c82,negated_conjecture,city(skolem0001,skolem0004)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c81,negated_conjecture,city(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c80,negated_conjecture,city(skolem0001,skolem0004)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c60,negated_conjecture,of(skolem0001,skolem0003,skolem0004)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c56,negated_conjecture,lonely(skolem0001,skolem0002)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c55,negated_conjecture,lonely(skolem0001,skolem0002)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c53,negated_conjecture,lonely(skolem0001,skolem0002)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c52,negated_conjecture,lonely(skolem0001,skolem0002)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c51,negated_conjecture,lonely(skolem0001,skolem0002)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c50,negated_conjecture,lonely(skolem0001,skolem0002)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c49,negated_conjecture,lonely(skolem0001,skolem0002)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c48,negated_conjecture,lonely(skolem0001,skolem0002)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c47,negated_conjecture,lonely(skolem0001,skolem0002)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c46,negated_conjecture,lonely(skolem0001,skolem0002)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c45,negated_conjecture,lonely(skolem0001,skolem0002)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c44,negated_conjecture,lonely(skolem0001,skolem0002)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c38,negated_conjecture,street(skolem0001,skolem0002)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c37,negated_conjecture,street(skolem0001,skolem0002)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c35,negated_conjecture,street(skolem0001,skolem0002)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c34,negated_conjecture,street(skolem0001,skolem0002)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c33,negated_conjecture,street(skolem0001,skolem0002)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c32,negated_conjecture,street(skolem0001,skolem0002)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c31,negated_conjecture,street(skolem0001,skolem0002)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c25,negated_conjecture,street(skolem0001,skolem0002)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c30,negated_conjecture,street(skolem0001,skolem0002)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c29,negated_conjecture,street(skolem0001,skolem0002)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c28,negated_conjecture,street(skolem0001,skolem0002)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c27,negated_conjecture,street(skolem0001,skolem0002)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c26,negated_conjecture,street(skolem0001,skolem0002)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c258,negated_conjecture,barrel(skolem0001,skolem0005)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c240,negated_conjecture,present(skolem0001,skolem0005)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c204,negated_conjecture,event(skolem0001,skolem0005)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c186,negated_conjecture,old(skolem0001,skolem0004)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c168,negated_conjecture,dirty(skolem0001,skolem0004)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c150,negated_conjecture,white(skolem0001,skolem0004)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c132,negated_conjecture,chevy(skolem0001,skolem0004)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c114,negated_conjecture,placename(skolem0001,skolem0003)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c96,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c78,negated_conjecture,city(skolem0001,skolem0004)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c42,negated_conjecture,lonely(skolem0001,skolem0002)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c24,negated_conjecture,street(skolem0001,skolem0002)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c20,negated_conjecture,actual_world(skolem0001)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c19,negated_conjecture,actual_world(skolem0001)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c17,negated_conjecture,actual_world(skolem0001)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c16,negated_conjecture,actual_world(skolem0001)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c15,negated_conjecture,actual_world(skolem0001)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c14,negated_conjecture,actual_world(skolem0001)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c13,negated_conjecture,actual_world(skolem0001)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c12,negated_conjecture,actual_world(skolem0001)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c7,negated_conjecture,actual_world(skolem0001)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c11,negated_conjecture,actual_world(skolem0001)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c10,negated_conjecture,actual_world(skolem0001)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c9,negated_conjecture,actual_world(skolem0001)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c8,negated_conjecture,actual_world(skolem0001)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  cnf(c6,negated_conjecture,actual_world(skolem0001)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.30/4.53  % SZS output end Saturation
% 4.30/4.53  
% 4.30/4.53  % Initial clauses    : 324
% 4.30/4.53  % Processed clauses  : 413
% 4.30/4.53  % Factors computed   : 21
% 4.30/4.53  % Resolvents computed: 1615
% 4.30/4.53  % Tautologies deleted: 306
% 4.30/4.53  % Forward subsumed   : 1241
% 4.30/4.53  % Backward subsumed  : 20
% 4.30/4.53  % -------- CPU Time ---------
% 4.30/4.53  % User time          : 4.139 s
% 4.30/4.53  % System time        : 0.025 s
% 4.30/4.53  % Total time         : 4.164 s
%------------------------------------------------------------------------------