PyRes---1.5.CSA-Sat.s

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

% Computer : n015.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:12 EDT 2024

% Result   : CounterSatisfiable 4.52s 4.69s
% Output   : Saturation 4.52s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13  % Problem  : NLP121+1 : TPTP v8.1.2. Released v2.4.0.
% 0.07/0.14  % Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36  % Computer : n015.cluster.edu
% 0.14/0.36  % Model    : x86_64 x86_64
% 0.14/0.36  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36  % Memory   : 8042.1875MB
% 0.14/0.36  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36  % CPULimit : 300
% 0.14/0.36  % WCLimit  : 300
% 0.14/0.36  % DateTime : Wed May  8 13:36:38 EDT 2024
% 0.14/0.36  % CPUTime  : 
% 4.52/4.69  % Version:  1.5
% 4.52/4.69  % SZS status CounterSatisfiable
% 4.52/4.69  % SZS output start Saturation
% 4.52/4.69  fof(co1,conjecture,(~(~(((?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(((((((((((((((of(U,V,W)&city(U,W))&hollywood_placename(U,V))&placename(U,V))&chevy(U,W))&white(U,W))&dirty(U,W))&old(U,W))&street(U,X))&lonely(U,X))&event(U,Y))&agent(U,Y,W))&present(U,Y))&barrel(U,Y))&down(U,Y,X))&in(U,Y,W))))))))=>(?[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]:(((((((((((((((of(U,V,W)&city(U,W))&hollywood_placename(U,V))&placename(U,V))&chevy(U,W))&white(U,W))&dirty(U,W))&old(U,W))&street(U,X))&lonely(U,X))&event(U,Y))&agent(U,Y,W))&present(U,Y))&barrel(U,Y))&down(U,Y,X))&in(U,Y,W)))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1)).
% 4.52/4.69  fof(c0,negated_conjecture,(~(~(~(((?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(((((((((((((((of(U,V,W)&city(U,W))&hollywood_placename(U,V))&placename(U,V))&chevy(U,W))&white(U,W))&dirty(U,W))&old(U,W))&street(U,X))&lonely(U,X))&event(U,Y))&agent(U,Y,W))&present(U,Y))&barrel(U,Y))&down(U,Y,X))&in(U,Y,W))))))))=>(?[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]:(((((((((((((((of(U,V,W)&city(U,W))&hollywood_placename(U,V))&placename(U,V))&chevy(U,W))&white(U,W))&dirty(U,W))&old(U,W))&street(U,X))&lonely(U,X))&event(U,Y))&agent(U,Y,W))&present(U,Y))&barrel(U,Y))&down(U,Y,X))&in(U,Y,W))))))))))))),inference(assume_negation,[status(cth)],[co1])).
% 4.52/4.69  fof(c1,negated_conjecture,(((?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(((((((((((((((of(U,V,W)&city(U,W))&hollywood_placename(U,V))&placename(U,V))&chevy(U,W))&white(U,W))&dirty(U,W))&old(U,W))&street(U,X))&lonely(U,X))&event(U,Y))&agent(U,Y,W))&present(U,Y))&barrel(U,Y))&down(U,Y,X))&in(U,Y,W))))))))&(![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]:(((((((((((((((~of(U,V,W)|~city(U,W))|~hollywood_placename(U,V))|~placename(U,V))|~chevy(U,W))|~white(U,W))|~dirty(U,W))|~old(U,W))|~street(U,X))|~lonely(U,X))|~event(U,Y))|~agent(U,Y,W))|~present(U,Y))|~barrel(U,Y))|~down(U,Y,X))|~in(U,Y,W)))))))))),inference(fof_nnf,[status(thm)],[c0])).
% 4.52/4.69  fof(c2,negated_conjecture,(((?[X2]:(actual_world(X2)&(?[X3]:(?[X4]:(?[X5]:(?[X6]:(((((((((((((((of(X2,X3,X4)&city(X2,X4))&hollywood_placename(X2,X3))&placename(X2,X3))&chevy(X2,X4))&white(X2,X4))&dirty(X2,X4))&old(X2,X4))&street(X2,X5))&lonely(X2,X5))&event(X2,X6))&agent(X2,X6,X4))&present(X2,X6))&barrel(X2,X6))&down(X2,X6,X5))&in(X2,X6,X4))))))))&(![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]:(((((((((((((((~of(X17,X18,X19)|~city(X17,X19))|~hollywood_placename(X17,X18))|~placename(X17,X18))|~chevy(X17,X19))|~white(X17,X19))|~dirty(X17,X19))|~old(X17,X19))|~street(X17,X20))|~lonely(X17,X20))|~event(X17,X21))|~agent(X17,X21,X19))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X20))|~in(X17,X21,X19)))))))))),inference(variable_rename,[status(thm)],[c1])).
% 4.52/4.69  fof(c4,negated_conjecture,(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(((actual_world(skolem0001)&(((((((((((((((of(skolem0001,skolem0002,skolem0003)&city(skolem0001,skolem0003))&hollywood_placename(skolem0001,skolem0002))&placename(skolem0001,skolem0002))&chevy(skolem0001,skolem0003))&white(skolem0001,skolem0003))&dirty(skolem0001,skolem0003))&old(skolem0001,skolem0003))&street(skolem0001,skolem0004))&lonely(skolem0001,skolem0004))&event(skolem0001,skolem0005))&agent(skolem0001,skolem0005,skolem0003))&present(skolem0001,skolem0005))&barrel(skolem0001,skolem0005))&down(skolem0001,skolem0005,skolem0004))&in(skolem0001,skolem0005,skolem0003)))&(~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)|(((((((((((((((~of(X17,X18,X19)|~city(X17,X19))|~hollywood_placename(X17,X18))|~placename(X17,X18))|~chevy(X17,X19))|~white(X17,X19))|~dirty(X17,X19))|~old(X17,X19))|~street(X17,X20))|~lonely(X17,X20))|~event(X17,X21))|~agent(X17,X21,X19))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X20))|~in(X17,X21,X19))))))))))))))),inference(shift_quantors,[status(thm)],[fof(c3,negated_conjecture,(((actual_world(skolem0001)&(((((((((((((((of(skolem0001,skolem0002,skolem0003)&city(skolem0001,skolem0003))&hollywood_placename(skolem0001,skolem0002))&placename(skolem0001,skolem0002))&chevy(skolem0001,skolem0003))&white(skolem0001,skolem0003))&dirty(skolem0001,skolem0003))&old(skolem0001,skolem0003))&street(skolem0001,skolem0004))&lonely(skolem0001,skolem0004))&event(skolem0001,skolem0005))&agent(skolem0001,skolem0005,skolem0003))&present(skolem0001,skolem0005))&barrel(skolem0001,skolem0005))&down(skolem0001,skolem0005,skolem0004))&in(skolem0001,skolem0005,skolem0003)))&(![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]:(((((((((((((((~of(X17,X18,X19)|~city(X17,X19))|~hollywood_placename(X17,X18))|~placename(X17,X18))|~chevy(X17,X19))|~white(X17,X19))|~dirty(X17,X19))|~old(X17,X19))|~street(X17,X20))|~lonely(X17,X20))|~event(X17,X21))|~agent(X17,X21,X19))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X20))|~in(X17,X21,X19)))))))))),inference(skolemize,[status(esa)],[c2])).])).
% 4.52/4.70  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)|(((((((((((((((~of(X17,X18,X19)|~city(X17,X19))|~hollywood_placename(X17,X18))|~placename(X17,X18))|~chevy(X17,X19))|~white(X17,X19))|~dirty(X17,X19))|~old(X17,X19))|~street(X17,X20))|~lonely(X17,X20))|~event(X17,X21))|~agent(X17,X21,X19))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X20))|~in(X17,X21,X19)))))&((((((((((((((((((of(skolem0001,skolem0002,skolem0003)|actual_world(skolem0006))&((((((((((((((((of(skolem0001,skolem0002,skolem0003)|of(skolem0006,skolem0007,skolem0008))&(of(skolem0001,skolem0002,skolem0003)|city(skolem0006,skolem0008)))&(of(skolem0001,skolem0002,skolem0003)|hollywood_placename(skolem0006,skolem0007)))&(of(skolem0001,skolem0002,skolem0003)|placename(skolem0006,skolem0007)))&(of(skolem0001,skolem0002,skolem0003)|street(skolem0006,skolem0008)))&(of(skolem0001,skolem0002,skolem0003)|lonely(skolem0006,skolem0008)))&(of(skolem0001,skolem0002,skolem0003)|chevy(skolem0006,skolem0009)))&(of(skolem0001,skolem0002,skolem0003)|white(skolem0006,skolem0009)))&(of(skolem0001,skolem0002,skolem0003)|dirty(skolem0006,skolem0009)))&(of(skolem0001,skolem0002,skolem0003)|old(skolem0006,skolem0009)))&(of(skolem0001,skolem0002,skolem0003)|event(skolem0006,skolem0010)))&(of(skolem0001,skolem0002,skolem0003)|agent(skolem0006,skolem0010,skolem0009)))&(of(skolem0001,skolem0002,skolem0003)|present(skolem0006,skolem0010)))&(of(skolem0001,skolem0002,skolem0003)|barrel(skolem0006,skolem0010)))&(of(skolem0001,skolem0002,skolem0003)|down(skolem0006,skolem0010,skolem0008)))&(of(skolem0001,skolem0002,skolem0003)|in(skolem0006,skolem0010,skolem0008))))&(of(skolem0001,skolem0002,skolem0003)|(~actual_world(X17)|(((((((((((((((~of(X17,X18,X19)|~city(X17,X19))|~hollywood_placename(X17,X18))|~placename(X17,X18))|~chevy(X17,X19))|~white(X17,X19))|~dirty(X17,X19))|~old(X17,X19))|~street(X17,X20))|~lonely(X17,X20))|~event(X17,X21))|~agent(X17,X21,X19))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X20))|~in(X17,X21,X19)))))&(((city(skolem0001,skolem0003)|actual_world(skolem0006))&((((((((((((((((city(skolem0001,skolem0003)|of(skolem0006,skolem0007,skolem0008))&(city(skolem0001,skolem0003)|city(skolem0006,skolem0008)))&(city(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0007)))&(city(skolem0001,skolem0003)|placename(skolem0006,skolem0007)))&(city(skolem0001,skolem0003)|street(skolem0006,skolem0008)))&(city(skolem0001,skolem0003)|lonely(skolem0006,skolem0008)))&(city(skolem0001,skolem0003)|chevy(skolem0006,skolem0009)))&(city(skolem0001,skolem0003)|white(skolem0006,skolem0009)))&(city(skolem0001,skolem0003)|dirty(skolem0006,skolem0009)))&(city(skolem0001,skolem0003)|old(skolem0006,skolem0009)))&(city(skolem0001,skolem0003)|event(skolem0006,skolem0010)))&(city(skolem0001,skolem0003)|agent(skolem0006,skolem0010,skolem0009)))&(city(skolem0001,skolem0003)|present(skolem0006,skolem0010)))&(city(skolem0001,skolem0003)|barrel(skolem0006,skolem0010)))&(city(skolem0001,skolem0003)|down(skolem0006,skolem0010,skolem0008)))&(city(skolem0001,skolem0003)|in(skolem0006,skolem0010,skolem0008))))&(city(skolem0001,skolem0003)|(~actual_world(X17)|(((((((((((((((~of(X17,X18,X19)|~city(X17,X19))|~hollywood_placename(X17,X18))|~placename(X17,X18))|~chevy(X17,X19))|~white(X17,X19))|~dirty(X17,X19))|~old(X17,X19))|~street(X17,X20))|~lonely(X17,X20))|~event(X17,X21))|~agent(X17,X21,X19))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X20))|~in(X17,X21,X19))))))&(((hollywood_placename(skolem0001,skolem0002)|actual_world(skolem0006))&((((((((((((((((hollywood_placename(skolem0001,skolem0002)|of(skolem0006,skolem0007,skolem0008))&(hollywood_placename(skolem0001,skolem0002)|city(skolem0006,skolem0008)))&(hollywood_placename(skolem0001,skolem0002)|hollywood_placename(skolem0006,skolem0007)))&(hollywood_placename(skolem0001,skolem0002)|placename(skolem0006,skolem0007)))&(hollywood_placename(skolem0001,skolem0002)|street(skolem0006,skolem0008)))&(hollywood_placename(skolem0001,skolem0002)|lonely(skolem0006,skolem0008)))&(hollywood_placename(skolem0001,skolem0002)|chevy(skolem0006,skolem0009)))&(hollywood_placename(skolem0001,skolem0002)|white(skolem0006,skolem0009)))&(hollywood_placename(skolem0001,skolem0002)|dirty(skolem0006,skolem0009)))&(hollywood_placename(skolem0001,skolem0002)|old(skolem0006,skolem0009)))&(hollywood_placename(skolem0001,skolem0002)|event(skolem0006,skolem0010)))&(hollywood_placename(skolem0001,skolem0002)|agent(skolem0006,skolem0010,skolem0009)))&(hollywood_placename(skolem0001,skolem0002)|present(skolem0006,skolem0010)))&(hollywood_placename(skolem0001,skolem0002)|barrel(skolem0006,skolem0010)))&(hollywood_placename(skolem0001,skolem0002)|down(skolem0006,skolem0010,skolem0008)))&(hollywood_placename(skolem0001,skolem0002)|in(skolem0006,skolem0010,skolem0008))))&(hollywood_placename(skolem0001,skolem0002)|(~actual_world(X17)|(((((((((((((((~of(X17,X18,X19)|~city(X17,X19))|~hollywood_placename(X17,X18))|~placename(X17,X18))|~chevy(X17,X19))|~white(X17,X19))|~dirty(X17,X19))|~old(X17,X19))|~street(X17,X20))|~lonely(X17,X20))|~event(X17,X21))|~agent(X17,X21,X19))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X20))|~in(X17,X21,X19))))))&(((placename(skolem0001,skolem0002)|actual_world(skolem0006))&((((((((((((((((placename(skolem0001,skolem0002)|of(skolem0006,skolem0007,skolem0008))&(placename(skolem0001,skolem0002)|city(skolem0006,skolem0008)))&(placename(skolem0001,skolem0002)|hollywood_placename(skolem0006,skolem0007)))&(placename(skolem0001,skolem0002)|placename(skolem0006,skolem0007)))&(placename(skolem0001,skolem0002)|street(skolem0006,skolem0008)))&(placename(skolem0001,skolem0002)|lonely(skolem0006,skolem0008)))&(placename(skolem0001,skolem0002)|chevy(skolem0006,skolem0009)))&(placename(skolem0001,skolem0002)|white(skolem0006,skolem0009)))&(placename(skolem0001,skolem0002)|dirty(skolem0006,skolem0009)))&(placename(skolem0001,skolem0002)|old(skolem0006,skolem0009)))&(placename(skolem0001,skolem0002)|event(skolem0006,skolem0010)))&(placename(skolem0001,skolem0002)|agent(skolem0006,skolem0010,skolem0009)))&(placename(skolem0001,skolem0002)|present(skolem0006,skolem0010)))&(placename(skolem0001,skolem0002)|barrel(skolem0006,skolem0010)))&(placename(skolem0001,skolem0002)|down(skolem0006,skolem0010,skolem0008)))&(placename(skolem0001,skolem0002)|in(skolem0006,skolem0010,skolem0008))))&(placename(skolem0001,skolem0002)|(~actual_world(X17)|(((((((((((((((~of(X17,X18,X19)|~city(X17,X19))|~hollywood_placename(X17,X18))|~placename(X17,X18))|~chevy(X17,X19))|~white(X17,X19))|~dirty(X17,X19))|~old(X17,X19))|~street(X17,X20))|~lonely(X17,X20))|~event(X17,X21))|~agent(X17,X21,X19))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X20))|~in(X17,X21,X19))))))&(((chevy(skolem0001,skolem0003)|actual_world(skolem0006))&((((((((((((((((chevy(skolem0001,skolem0003)|of(skolem0006,skolem0007,skolem0008))&(chevy(skolem0001,skolem0003)|city(skolem0006,skolem0008)))&(chevy(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0007)))&(chevy(skolem0001,skolem0003)|placename(skolem0006,skolem0007)))&(chevy(skolem0001,skolem0003)|street(skolem0006,skolem0008)))&(chevy(skolem0001,skolem0003)|lonely(skolem0006,skolem0008)))&(chevy(skolem0001,skolem0003)|chevy(skolem0006,skolem0009)))&(chevy(skolem0001,skolem0003)|white(skolem0006,skolem0009)))&(chevy(skolem0001,skolem0003)|dirty(skolem0006,skolem0009)))&(chevy(skolem0001,skolem0003)|old(skolem0006,skolem0009)))&(chevy(skolem0001,skolem0003)|event(skolem0006,skolem0010)))&(chevy(skolem0001,skolem0003)|agent(skolem0006,skolem0010,skolem0009)))&(chevy(skolem0001,skolem0003)|present(skolem0006,skolem0010)))&(chevy(skolem0001,skolem0003)|barrel(skolem0006,skolem0010)))&(chevy(skolem0001,skolem0003)|down(skolem0006,skolem0010,skolem0008)))&(chevy(skolem0001,skolem0003)|in(skolem0006,skolem0010,skolem0008))))&(chevy(skolem0001,skolem0003)|(~actual_world(X17)|(((((((((((((((~of(X17,X18,X19)|~city(X17,X19))|~hollywood_placename(X17,X18))|~placename(X17,X18))|~chevy(X17,X19))|~white(X17,X19))|~dirty(X17,X19))|~old(X17,X19))|~street(X17,X20))|~lonely(X17,X20))|~event(X17,X21))|~agent(X17,X21,X19))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X20))|~in(X17,X21,X19))))))&(((white(skolem0001,skolem0003)|actual_world(skolem0006))&((((((((((((((((white(skolem0001,skolem0003)|of(skolem0006,skolem0007,skolem0008))&(white(skolem0001,skolem0003)|city(skolem0006,skolem0008)))&(white(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0007)))&(white(skolem0001,skolem0003)|placename(skolem0006,skolem0007)))&(white(skolem0001,skolem0003)|street(skolem0006,skolem0008)))&(white(skolem0001,skolem0003)|lonely(skolem0006,skolem0008)))&(white(skolem0001,skolem0003)|chevy(skolem0006,skolem0009)))&(white(skolem0001,skolem0003)|white(skolem0006,skolem0009)))&(white(skolem0001,skolem0003)|dirty(skolem0006,skolem0009)))&(white(skolem0001,skolem0003)|old(skolem0006,skolem0009)))&(white(skolem0001,skolem0003)|event(skolem0006,skolem0010)))&(white(skolem0001,skolem0003)|agent(skolem0006,skolem0010,skolem0009)))&(white(skolem0001,skolem0003)|present(skolem0006,skolem0010)))&(white(skolem0001,skolem0003)|barrel(skolem0006,skolem0010)))&(white(skolem0001,skolem0003)|down(skolem0006,skolem0010,skolem0008)))&(white(skolem0001,skolem0003)|in(skolem0006,skolem0010,skolem0008))))&(white(skolem0001,skolem0003)|(~actual_world(X17)|(((((((((((((((~of(X17,X18,X19)|~city(X17,X19))|~hollywood_placename(X17,X18))|~placename(X17,X18))|~chevy(X17,X19))|~white(X17,X19))|~dirty(X17,X19))|~old(X17,X19))|~street(X17,X20))|~lonely(X17,X20))|~event(X17,X21))|~agent(X17,X21,X19))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X20))|~in(X17,X21,X19))))))&(((dirty(skolem0001,skolem0003)|actual_world(skolem0006))&((((((((((((((((dirty(skolem0001,skolem0003)|of(skolem0006,skolem0007,skolem0008))&(dirty(skolem0001,skolem0003)|city(skolem0006,skolem0008)))&(dirty(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0007)))&(dirty(skolem0001,skolem0003)|placename(skolem0006,skolem0007)))&(dirty(skolem0001,skolem0003)|street(skolem0006,skolem0008)))&(dirty(skolem0001,skolem0003)|lonely(skolem0006,skolem0008)))&(dirty(skolem0001,skolem0003)|chevy(skolem0006,skolem0009)))&(dirty(skolem0001,skolem0003)|white(skolem0006,skolem0009)))&(dirty(skolem0001,skolem0003)|dirty(skolem0006,skolem0009)))&(dirty(skolem0001,skolem0003)|old(skolem0006,skolem0009)))&(dirty(skolem0001,skolem0003)|event(skolem0006,skolem0010)))&(dirty(skolem0001,skolem0003)|agent(skolem0006,skolem0010,skolem0009)))&(dirty(skolem0001,skolem0003)|present(skolem0006,skolem0010)))&(dirty(skolem0001,skolem0003)|barrel(skolem0006,skolem0010)))&(dirty(skolem0001,skolem0003)|down(skolem0006,skolem0010,skolem0008)))&(dirty(skolem0001,skolem0003)|in(skolem0006,skolem0010,skolem0008))))&(dirty(skolem0001,skolem0003)|(~actual_world(X17)|(((((((((((((((~of(X17,X18,X19)|~city(X17,X19))|~hollywood_placename(X17,X18))|~placename(X17,X18))|~chevy(X17,X19))|~white(X17,X19))|~dirty(X17,X19))|~old(X17,X19))|~street(X17,X20))|~lonely(X17,X20))|~event(X17,X21))|~agent(X17,X21,X19))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X20))|~in(X17,X21,X19))))))&(((old(skolem0001,skolem0003)|actual_world(skolem0006))&((((((((((((((((old(skolem0001,skolem0003)|of(skolem0006,skolem0007,skolem0008))&(old(skolem0001,skolem0003)|city(skolem0006,skolem0008)))&(old(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0007)))&(old(skolem0001,skolem0003)|placename(skolem0006,skolem0007)))&(old(skolem0001,skolem0003)|street(skolem0006,skolem0008)))&(old(skolem0001,skolem0003)|lonely(skolem0006,skolem0008)))&(old(skolem0001,skolem0003)|chevy(skolem0006,skolem0009)))&(old(skolem0001,skolem0003)|white(skolem0006,skolem0009)))&(old(skolem0001,skolem0003)|dirty(skolem0006,skolem0009)))&(old(skolem0001,skolem0003)|old(skolem0006,skolem0009)))&(old(skolem0001,skolem0003)|event(skolem0006,skolem0010)))&(old(skolem0001,skolem0003)|agent(skolem0006,skolem0010,skolem0009)))&(old(skolem0001,skolem0003)|present(skolem0006,skolem0010)))&(old(skolem0001,skolem0003)|barrel(skolem0006,skolem0010)))&(old(skolem0001,skolem0003)|down(skolem0006,skolem0010,skolem0008)))&(old(skolem0001,skolem0003)|in(skolem0006,skolem0010,skolem0008))))&(old(skolem0001,skolem0003)|(~actual_world(X17)|(((((((((((((((~of(X17,X18,X19)|~city(X17,X19))|~hollywood_placename(X17,X18))|~placename(X17,X18))|~chevy(X17,X19))|~white(X17,X19))|~dirty(X17,X19))|~old(X17,X19))|~street(X17,X20))|~lonely(X17,X20))|~event(X17,X21))|~agent(X17,X21,X19))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X20))|~in(X17,X21,X19))))))&(((street(skolem0001,skolem0004)|actual_world(skolem0006))&((((((((((((((((street(skolem0001,skolem0004)|of(skolem0006,skolem0007,skolem0008))&(street(skolem0001,skolem0004)|city(skolem0006,skolem0008)))&(street(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0007)))&(street(skolem0001,skolem0004)|placename(skolem0006,skolem0007)))&(street(skolem0001,skolem0004)|street(skolem0006,skolem0008)))&(street(skolem0001,skolem0004)|lonely(skolem0006,skolem0008)))&(street(skolem0001,skolem0004)|chevy(skolem0006,skolem0009)))&(street(skolem0001,skolem0004)|white(skolem0006,skolem0009)))&(street(skolem0001,skolem0004)|dirty(skolem0006,skolem0009)))&(street(skolem0001,skolem0004)|old(skolem0006,skolem0009)))&(street(skolem0001,skolem0004)|event(skolem0006,skolem0010)))&(street(skolem0001,skolem0004)|agent(skolem0006,skolem0010,skolem0009)))&(street(skolem0001,skolem0004)|present(skolem0006,skolem0010)))&(street(skolem0001,skolem0004)|barrel(skolem0006,skolem0010)))&(street(skolem0001,skolem0004)|down(skolem0006,skolem0010,skolem0008)))&(street(skolem0001,skolem0004)|in(skolem0006,skolem0010,skolem0008))))&(street(skolem0001,skolem0004)|(~actual_world(X17)|(((((((((((((((~of(X17,X18,X19)|~city(X17,X19))|~hollywood_placename(X17,X18))|~placename(X17,X18))|~chevy(X17,X19))|~white(X17,X19))|~dirty(X17,X19))|~old(X17,X19))|~street(X17,X20))|~lonely(X17,X20))|~event(X17,X21))|~agent(X17,X21,X19))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X20))|~in(X17,X21,X19))))))&(((lonely(skolem0001,skolem0004)|actual_world(skolem0006))&((((((((((((((((lonely(skolem0001,skolem0004)|of(skolem0006,skolem0007,skolem0008))&(lonely(skolem0001,skolem0004)|city(skolem0006,skolem0008)))&(lonely(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0007)))&(lonely(skolem0001,skolem0004)|placename(skolem0006,skolem0007)))&(lonely(skolem0001,skolem0004)|street(skolem0006,skolem0008)))&(lonely(skolem0001,skolem0004)|lonely(skolem0006,skolem0008)))&(lonely(skolem0001,skolem0004)|chevy(skolem0006,skolem0009)))&(lonely(skolem0001,skolem0004)|white(skolem0006,skolem0009)))&(lonely(skolem0001,skolem0004)|dirty(skolem0006,skolem0009)))&(lonely(skolem0001,skolem0004)|old(skolem0006,skolem0009)))&(lonely(skolem0001,skolem0004)|event(skolem0006,skolem0010)))&(lonely(skolem0001,skolem0004)|agent(skolem0006,skolem0010,skolem0009)))&(lonely(skolem0001,skolem0004)|present(skolem0006,skolem0010)))&(lonely(skolem0001,skolem0004)|barrel(skolem0006,skolem0010)))&(lonely(skolem0001,skolem0004)|down(skolem0006,skolem0010,skolem0008)))&(lonely(skolem0001,skolem0004)|in(skolem0006,skolem0010,skolem0008))))&(lonely(skolem0001,skolem0004)|(~actual_world(X17)|(((((((((((((((~of(X17,X18,X19)|~city(X17,X19))|~hollywood_placename(X17,X18))|~placename(X17,X18))|~chevy(X17,X19))|~white(X17,X19))|~dirty(X17,X19))|~old(X17,X19))|~street(X17,X20))|~lonely(X17,X20))|~event(X17,X21))|~agent(X17,X21,X19))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X20))|~in(X17,X21,X19))))))&(((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)|(((((((((((((((~of(X17,X18,X19)|~city(X17,X19))|~hollywood_placename(X17,X18))|~placename(X17,X18))|~chevy(X17,X19))|~white(X17,X19))|~dirty(X17,X19))|~old(X17,X19))|~street(X17,X20))|~lonely(X17,X20))|~event(X17,X21))|~agent(X17,X21,X19))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X20))|~in(X17,X21,X19))))))&(((agent(skolem0001,skolem0005,skolem0003)|actual_world(skolem0006))&((((((((((((((((agent(skolem0001,skolem0005,skolem0003)|of(skolem0006,skolem0007,skolem0008))&(agent(skolem0001,skolem0005,skolem0003)|city(skolem0006,skolem0008)))&(agent(skolem0001,skolem0005,skolem0003)|hollywood_placename(skolem0006,skolem0007)))&(agent(skolem0001,skolem0005,skolem0003)|placename(skolem0006,skolem0007)))&(agent(skolem0001,skolem0005,skolem0003)|street(skolem0006,skolem0008)))&(agent(skolem0001,skolem0005,skolem0003)|lonely(skolem0006,skolem0008)))&(agent(skolem0001,skolem0005,skolem0003)|chevy(skolem0006,skolem0009)))&(agent(skolem0001,skolem0005,skolem0003)|white(skolem0006,skolem0009)))&(agent(skolem0001,skolem0005,skolem0003)|dirty(skolem0006,skolem0009)))&(agent(skolem0001,skolem0005,skolem0003)|old(skolem0006,skolem0009)))&(agent(skolem0001,skolem0005,skolem0003)|event(skolem0006,skolem0010)))&(agent(skolem0001,skolem0005,skolem0003)|agent(skolem0006,skolem0010,skolem0009)))&(agent(skolem0001,skolem0005,skolem0003)|present(skolem0006,skolem0010)))&(agent(skolem0001,skolem0005,skolem0003)|barrel(skolem0006,skolem0010)))&(agent(skolem0001,skolem0005,skolem0003)|down(skolem0006,skolem0010,skolem0008)))&(agent(skolem0001,skolem0005,skolem0003)|in(skolem0006,skolem0010,skolem0008))))&(agent(skolem0001,skolem0005,skolem0003)|(~actual_world(X17)|(((((((((((((((~of(X17,X18,X19)|~city(X17,X19))|~hollywood_placename(X17,X18))|~placename(X17,X18))|~chevy(X17,X19))|~white(X17,X19))|~dirty(X17,X19))|~old(X17,X19))|~street(X17,X20))|~lonely(X17,X20))|~event(X17,X21))|~agent(X17,X21,X19))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X20))|~in(X17,X21,X19))))))&(((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)|(((((((((((((((~of(X17,X18,X19)|~city(X17,X19))|~hollywood_placename(X17,X18))|~placename(X17,X18))|~chevy(X17,X19))|~white(X17,X19))|~dirty(X17,X19))|~old(X17,X19))|~street(X17,X20))|~lonely(X17,X20))|~event(X17,X21))|~agent(X17,X21,X19))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X20))|~in(X17,X21,X19))))))&(((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)|(((((((((((((((~of(X17,X18,X19)|~city(X17,X19))|~hollywood_placename(X17,X18))|~placename(X17,X18))|~chevy(X17,X19))|~white(X17,X19))|~dirty(X17,X19))|~old(X17,X19))|~street(X17,X20))|~lonely(X17,X20))|~event(X17,X21))|~agent(X17,X21,X19))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X20))|~in(X17,X21,X19))))))&(((down(skolem0001,skolem0005,skolem0004)|actual_world(skolem0006))&((((((((((((((((down(skolem0001,skolem0005,skolem0004)|of(skolem0006,skolem0007,skolem0008))&(down(skolem0001,skolem0005,skolem0004)|city(skolem0006,skolem0008)))&(down(skolem0001,skolem0005,skolem0004)|hollywood_placename(skolem0006,skolem0007)))&(down(skolem0001,skolem0005,skolem0004)|placename(skolem0006,skolem0007)))&(down(skolem0001,skolem0005,skolem0004)|street(skolem0006,skolem0008)))&(down(skolem0001,skolem0005,skolem0004)|lonely(skolem0006,skolem0008)))&(down(skolem0001,skolem0005,skolem0004)|chevy(skolem0006,skolem0009)))&(down(skolem0001,skolem0005,skolem0004)|white(skolem0006,skolem0009)))&(down(skolem0001,skolem0005,skolem0004)|dirty(skolem0006,skolem0009)))&(down(skolem0001,skolem0005,skolem0004)|old(skolem0006,skolem0009)))&(down(skolem0001,skolem0005,skolem0004)|event(skolem0006,skolem0010)))&(down(skolem0001,skolem0005,skolem0004)|agent(skolem0006,skolem0010,skolem0009)))&(down(skolem0001,skolem0005,skolem0004)|present(skolem0006,skolem0010)))&(down(skolem0001,skolem0005,skolem0004)|barrel(skolem0006,skolem0010)))&(down(skolem0001,skolem0005,skolem0004)|down(skolem0006,skolem0010,skolem0008)))&(down(skolem0001,skolem0005,skolem0004)|in(skolem0006,skolem0010,skolem0008))))&(down(skolem0001,skolem0005,skolem0004)|(~actual_world(X17)|(((((((((((((((~of(X17,X18,X19)|~city(X17,X19))|~hollywood_placename(X17,X18))|~placename(X17,X18))|~chevy(X17,X19))|~white(X17,X19))|~dirty(X17,X19))|~old(X17,X19))|~street(X17,X20))|~lonely(X17,X20))|~event(X17,X21))|~agent(X17,X21,X19))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X20))|~in(X17,X21,X19))))))&(((in(skolem0001,skolem0005,skolem0003)|actual_world(skolem0006))&((((((((((((((((in(skolem0001,skolem0005,skolem0003)|of(skolem0006,skolem0007,skolem0008))&(in(skolem0001,skolem0005,skolem0003)|city(skolem0006,skolem0008)))&(in(skolem0001,skolem0005,skolem0003)|hollywood_placename(skolem0006,skolem0007)))&(in(skolem0001,skolem0005,skolem0003)|placename(skolem0006,skolem0007)))&(in(skolem0001,skolem0005,skolem0003)|street(skolem0006,skolem0008)))&(in(skolem0001,skolem0005,skolem0003)|lonely(skolem0006,skolem0008)))&(in(skolem0001,skolem0005,skolem0003)|chevy(skolem0006,skolem0009)))&(in(skolem0001,skolem0005,skolem0003)|white(skolem0006,skolem0009)))&(in(skolem0001,skolem0005,skolem0003)|dirty(skolem0006,skolem0009)))&(in(skolem0001,skolem0005,skolem0003)|old(skolem0006,skolem0009)))&(in(skolem0001,skolem0005,skolem0003)|event(skolem0006,skolem0010)))&(in(skolem0001,skolem0005,skolem0003)|agent(skolem0006,skolem0010,skolem0009)))&(in(skolem0001,skolem0005,skolem0003)|present(skolem0006,skolem0010)))&(in(skolem0001,skolem0005,skolem0003)|barrel(skolem0006,skolem0010)))&(in(skolem0001,skolem0005,skolem0003)|down(skolem0006,skolem0010,skolem0008)))&(in(skolem0001,skolem0005,skolem0003)|in(skolem0006,skolem0010,skolem0008))))&(in(skolem0001,skolem0005,skolem0003)|(~actual_world(X17)|(((((((((((((((~of(X17,X18,X19)|~city(X17,X19))|~hollywood_placename(X17,X18))|~placename(X17,X18))|~chevy(X17,X19))|~white(X17,X19))|~dirty(X17,X19))|~old(X17,X19))|~street(X17,X20))|~lonely(X17,X20))|~event(X17,X21))|~agent(X17,X21,X19))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X20))|~in(X17,X21,X19)))))))&((((~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)|(((((((((((((((~of(X17,X18,X19)|~city(X17,X19))|~hollywood_placename(X17,X18))|~placename(X17,X18))|~chevy(X17,X19))|~white(X17,X19))|~dirty(X17,X19))|~old(X17,X19))|~street(X17,X20))|~lonely(X17,X20))|~event(X17,X21))|~agent(X17,X21,X19))|~present(X17,X21))|~barrel(X17,X21))|~down(X17,X21,X20))|~in(X17,X21,X19)))))))))))))))),inference(distribute,[status(thm)],[c4])).
% 4.52/4.70  cnf(c288,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.70  cnf(c329,negated_conjecture,~actual_world(X192)|~of(X192,X201,X200)|~city(X192,X200)|~hollywood_placename(X192,X201)|~placename(X192,X201)|~street(X192,X200)|~lonely(X192,X200)|~chevy(X192,X199)|~white(X192,X199)|~dirty(X192,X199)|~old(X192,X199)|~event(X192,X195)|~agent(X192,X195,X199)|~present(X192,X195)|~barrel(X192,X195)|~down(X192,X195,X200)|~in(X192,X195,X200)|~actual_world(X197)|~of(X197,X194,X193)|~city(X197,X193)|~hollywood_placename(X197,X194)|~placename(X197,X194)|~chevy(X197,X193)|~white(X197,X193)|~dirty(X197,X193)|~old(X197,X193)|~street(X197,X196)|~lonely(X197,X196)|~event(X197,X198)|~agent(X197,X198,X193)|~present(X197,X198)|~barrel(X197,X198)|~down(X197,X198,X196)|~in(X197,X198,X193),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.70  cnf(c1486,plain,~actual_world(X2808)|~of(X2808,X2805,X2803)|~city(X2808,X2803)|~hollywood_placename(X2808,X2805)|~placename(X2808,X2805)|~street(X2808,X2803)|~lonely(X2808,X2803)|~chevy(X2808,X2804)|~white(X2808,X2804)|~dirty(X2808,X2804)|~old(X2808,X2804)|~event(X2808,X2807)|~agent(X2808,X2807,X2804)|~present(X2808,X2807)|~barrel(X2808,X2807)|~down(X2808,X2807,X2803)|~in(X2808,X2807,X2803)|~of(X2808,X2806,X2803)|~hollywood_placename(X2808,X2806)|~placename(X2808,X2806)|~chevy(X2808,X2803)|~white(X2808,X2803)|~dirty(X2808,X2803)|~old(X2808,X2803)|~street(X2808,X2809)|~lonely(X2808,X2809)|~agent(X2808,X2807,X2803)|~down(X2808,X2807,X2809),inference(factor,[status(thm)],[c329])).
% 4.52/4.70  cnf(c1810,plain,~actual_world(X2815)|~of(X2815,X2810,X2811)|~city(X2815,X2811)|~hollywood_placename(X2815,X2810)|~placename(X2815,X2810)|~street(X2815,X2811)|~lonely(X2815,X2811)|~chevy(X2815,X2814)|~white(X2815,X2814)|~dirty(X2815,X2814)|~old(X2815,X2814)|~event(X2815,X2812)|~agent(X2815,X2812,X2814)|~present(X2815,X2812)|~barrel(X2815,X2812)|~down(X2815,X2812,X2811)|~in(X2815,X2812,X2811)|~of(X2815,X2813,X2811)|~hollywood_placename(X2815,X2813)|~placename(X2815,X2813)|~chevy(X2815,X2811)|~white(X2815,X2811)|~dirty(X2815,X2811)|~old(X2815,X2811)|~agent(X2815,X2812,X2811),inference(factor,[status(thm)],[c1486])).
% 4.52/4.70  cnf(c1877,plain,~actual_world(skolem0006)|~of(skolem0006,X3217,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3217)|~placename(skolem0006,X3217)|~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,X3218,skolem0009)|~hollywood_placename(skolem0006,X3218)|~placename(skolem0006,X3218)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|down(skolem0001,skolem0005,skolem0004),inference(resolution,[status(thm)],[c1810, c288])).
% 4.52/4.70  cnf(c1965,plain,~actual_world(skolem0006)|~of(skolem0006,X3226,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3226)|~placename(skolem0006,X3226)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3227)|~white(skolem0006,X3227)|~dirty(skolem0006,X3227)|~old(skolem0006,X3227)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3227)|~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,skolem0004),inference(factor,[status(thm)],[c1877])).
% 4.52/4.70  cnf(c234,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.70  cnf(c1876,plain,~actual_world(skolem0006)|~of(skolem0006,X3212,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3212)|~placename(skolem0006,X3212)|~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,X3213,skolem0009)|~hollywood_placename(skolem0006,X3213)|~placename(skolem0006,X3213)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|agent(skolem0001,skolem0005,skolem0003),inference(resolution,[status(thm)],[c1810, c234])).
% 4.52/4.70  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,skolem0003),inference(factor,[status(thm)],[c1876])).
% 4.52/4.70  cnf(c306,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.70  cnf(c1863,plain,~actual_world(skolem0006)|~of(skolem0006,X3207,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3207)|~placename(skolem0006,X3207)|~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,X3208,skolem0009)|~hollywood_placename(skolem0006,X3208)|~placename(skolem0006,X3208)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|in(skolem0001,skolem0005,skolem0003),inference(resolution,[status(thm)],[c1810, c306])).
% 4.52/4.70  cnf(c1963,plain,~actual_world(skolem0006)|~of(skolem0006,X3210,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3210)|~placename(skolem0006,X3210)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3209)|~white(skolem0006,X3209)|~dirty(skolem0006,X3209)|~old(skolem0006,X3209)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3209)|~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,skolem0003),inference(factor,[status(thm)],[c1863])).
% 4.52/4.70  cnf(c36,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.70  cnf(c1853,plain,~actual_world(skolem0006)|~of(skolem0006,X3195,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3195)|~placename(skolem0006,X3195)|~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,X3196,skolem0009)|~hollywood_placename(skolem0006,X3196)|~placename(skolem0006,X3196)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|of(skolem0001,skolem0002,skolem0003),inference(resolution,[status(thm)],[c1810, c36])).
% 4.52/4.70  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,skolem0002,skolem0003),inference(factor,[status(thm)],[c1853])).
% 4.52/4.70  cnf(c90,negated_conjecture,placename(skolem0001,skolem0002)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.70  cnf(c1879,plain,~actual_world(skolem0006)|~of(skolem0006,X3174,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3174)|~placename(skolem0006,X3174)|~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,X3175,skolem0009)|~hollywood_placename(skolem0006,X3175)|~placename(skolem0006,X3175)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|placename(skolem0001,skolem0002),inference(resolution,[status(thm)],[c1810, c90])).
% 4.52/4.70  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)|placename(skolem0001,skolem0002),inference(factor,[status(thm)],[c1879])).
% 4.52/4.70  cnf(c216,negated_conjecture,event(skolem0001,skolem0005)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.70  cnf(c1873,plain,~actual_world(skolem0006)|~of(skolem0006,X3156,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3156)|~placename(skolem0006,X3156)|~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,X3157,skolem0009)|~hollywood_placename(skolem0006,X3157)|~placename(skolem0006,X3157)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|event(skolem0001,skolem0005),inference(resolution,[status(thm)],[c1810, c216])).
% 4.52/4.70  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.52/4.70  cnf(c72,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.70  cnf(c1871,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)|~of(skolem0006,X3149,skolem0009)|~hollywood_placename(skolem0006,X3149)|~placename(skolem0006,X3149)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|hollywood_placename(skolem0001,skolem0002),inference(resolution,[status(thm)],[c1810, c72])).
% 4.52/4.70  cnf(c1959,plain,~actual_world(skolem0006)|~of(skolem0006,X3151,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3151)|~placename(skolem0006,X3151)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3150)|~white(skolem0006,X3150)|~dirty(skolem0006,X3150)|~old(skolem0006,X3150)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3150)|~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,skolem0002),inference(factor,[status(thm)],[c1871])).
% 4.52/4.70  cnf(c180,negated_conjecture,street(skolem0001,skolem0004)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.70  cnf(c1869,plain,~actual_world(skolem0006)|~of(skolem0006,X3133,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3133)|~placename(skolem0006,X3133)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3132)|~white(skolem0006,X3132)|~dirty(skolem0006,X3132)|~old(skolem0006,X3132)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3132)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~of(skolem0006,X3134,skolem0009)|~hollywood_placename(skolem0006,X3134)|~placename(skolem0006,X3134)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|street(skolem0001,skolem0004),inference(resolution,[status(thm)],[c1810, c180])).
% 4.52/4.70  cnf(c1958,plain,~actual_world(skolem0006)|~of(skolem0006,X3135,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3135)|~placename(skolem0006,X3135)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3136)|~white(skolem0006,X3136)|~dirty(skolem0006,X3136)|~old(skolem0006,X3136)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3136)|~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,skolem0004),inference(factor,[status(thm)],[c1869])).
% 4.52/4.70  cnf(c144,negated_conjecture,dirty(skolem0001,skolem0003)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.70  cnf(c1867,plain,~actual_world(skolem0006)|~of(skolem0006,X3125,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3125)|~placename(skolem0006,X3125)|~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,X3126,skolem0009)|~hollywood_placename(skolem0006,X3126)|~placename(skolem0006,X3126)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|dirty(skolem0001,skolem0003),inference(resolution,[status(thm)],[c1810, c144])).
% 4.52/4.70  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)|dirty(skolem0001,skolem0003),inference(factor,[status(thm)],[c1867])).
% 4.52/4.70  cnf(c162,negated_conjecture,old(skolem0001,skolem0003)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.70  cnf(c1865,plain,~actual_world(skolem0006)|~of(skolem0006,X3110,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3110)|~placename(skolem0006,X3110)|~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,X3111,skolem0009)|~hollywood_placename(skolem0006,X3111)|~placename(skolem0006,X3111)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|old(skolem0001,skolem0003),inference(resolution,[status(thm)],[c1810, c162])).
% 4.52/4.70  cnf(c1956,plain,~actual_world(skolem0006)|~of(skolem0006,X3113,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3113)|~placename(skolem0006,X3113)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3112)|~white(skolem0006,X3112)|~dirty(skolem0006,X3112)|~old(skolem0006,X3112)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3112)|~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,skolem0003),inference(factor,[status(thm)],[c1865])).
% 4.52/4.70  cnf(c108,negated_conjecture,chevy(skolem0001,skolem0003)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.70  cnf(c1864,plain,~actual_world(skolem0006)|~of(skolem0006,X3105,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3105)|~placename(skolem0006,X3105)|~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,X3106,skolem0009)|~hollywood_placename(skolem0006,X3106)|~placename(skolem0006,X3106)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|chevy(skolem0001,skolem0003),inference(resolution,[status(thm)],[c1810, c108])).
% 4.52/4.70  cnf(c1955,plain,~actual_world(skolem0006)|~of(skolem0006,X3107,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3107)|~placename(skolem0006,X3107)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3108)|~white(skolem0006,X3108)|~dirty(skolem0006,X3108)|~old(skolem0006,X3108)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3108)|~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,skolem0003),inference(factor,[status(thm)],[c1864])).
% 4.52/4.70  cnf(c252,negated_conjecture,present(skolem0001,skolem0005)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.70  cnf(c1861,plain,~actual_world(skolem0006)|~of(skolem0006,X3090,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3090)|~placename(skolem0006,X3090)|~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,X3091,skolem0009)|~hollywood_placename(skolem0006,X3091)|~placename(skolem0006,X3091)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|present(skolem0001,skolem0005),inference(resolution,[status(thm)],[c1810, c252])).
% 4.52/4.70  cnf(c1954,plain,~actual_world(skolem0006)|~of(skolem0006,X3092,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3092)|~placename(skolem0006,X3092)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3093)|~white(skolem0006,X3093)|~dirty(skolem0006,X3093)|~old(skolem0006,X3093)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3093)|~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)],[c1861])).
% 4.52/4.70  cnf(c126,negated_conjecture,white(skolem0001,skolem0003)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.70  cnf(c1859,plain,~actual_world(skolem0006)|~of(skolem0006,X3075,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3075)|~placename(skolem0006,X3075)|~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,X3076,skolem0009)|~hollywood_placename(skolem0006,X3076)|~placename(skolem0006,X3076)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|white(skolem0001,skolem0003),inference(resolution,[status(thm)],[c1810, c126])).
% 4.52/4.70  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)|white(skolem0001,skolem0003),inference(factor,[status(thm)],[c1859])).
% 4.52/4.70  cnf(c198,negated_conjecture,lonely(skolem0001,skolem0004)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.70  cnf(c1858,plain,~actual_world(skolem0006)|~of(skolem0006,X3070,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3070)|~placename(skolem0006,X3070)|~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,X3071,skolem0009)|~hollywood_placename(skolem0006,X3071)|~placename(skolem0006,X3071)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|lonely(skolem0001,skolem0004),inference(resolution,[status(thm)],[c1810, c198])).
% 4.52/4.71  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)|lonely(skolem0001,skolem0004),inference(factor,[status(thm)],[c1858])).
% 4.52/4.71  cnf(c270,negated_conjecture,barrel(skolem0001,skolem0005)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c1851,plain,~actual_world(skolem0006)|~of(skolem0006,X3049,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3049)|~placename(skolem0006,X3049)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3048)|~white(skolem0006,X3048)|~dirty(skolem0006,X3048)|~old(skolem0006,X3048)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3048)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,skolem0009)|~in(skolem0006,skolem0010,skolem0009)|~of(skolem0006,X3050,skolem0009)|~hollywood_placename(skolem0006,X3050)|~placename(skolem0006,X3050)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|barrel(skolem0001,skolem0005),inference(resolution,[status(thm)],[c1810, c270])).
% 4.52/4.71  cnf(c1951,plain,~actual_world(skolem0006)|~of(skolem0006,X3051,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3051)|~placename(skolem0006,X3051)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3052)|~white(skolem0006,X3052)|~dirty(skolem0006,X3052)|~old(skolem0006,X3052)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3052)|~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)],[c1851])).
% 4.52/4.71  cnf(c54,negated_conjecture,city(skolem0001,skolem0003)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c1847,plain,~actual_world(skolem0006)|~of(skolem0006,X3044,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3044)|~placename(skolem0006,X3044)|~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,X3045,skolem0009)|~hollywood_placename(skolem0006,X3045)|~placename(skolem0006,X3045)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|city(skolem0001,skolem0003),inference(resolution,[status(thm)],[c1810, c54])).
% 4.52/4.71  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)|city(skolem0001,skolem0003),inference(factor,[status(thm)],[c1847])).
% 4.52/4.71  cnf(c18,negated_conjecture,actual_world(skolem0001)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c1850,plain,~actual_world(skolem0006)|~of(skolem0006,X3026,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3026)|~placename(skolem0006,X3026)|~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,X3027,skolem0009)|~hollywood_placename(skolem0006,X3027)|~placename(skolem0006,X3027)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009)|actual_world(skolem0001),inference(resolution,[status(thm)],[c1810, c18])).
% 4.52/4.71  cnf(c1949,plain,~actual_world(skolem0006)|~of(skolem0006,X3028,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3028)|~placename(skolem0006,X3028)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3029)|~white(skolem0006,X3029)|~dirty(skolem0006,X3029)|~old(skolem0006,X3029)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,X3029)|~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)],[c1850])).
% 4.52/4.71  cnf(c1845,plain,~actual_world(X2816)|~of(X2816,X2820,X2818)|~city(X2816,X2818)|~hollywood_placename(X2816,X2820)|~placename(X2816,X2820)|~street(X2816,X2818)|~lonely(X2816,X2818)|~chevy(X2816,X2818)|~white(X2816,X2818)|~dirty(X2816,X2818)|~old(X2816,X2818)|~event(X2816,X2819)|~agent(X2816,X2819,X2818)|~present(X2816,X2819)|~barrel(X2816,X2819)|~down(X2816,X2819,X2818)|~in(X2816,X2819,X2818)|~of(X2816,X2817,X2818)|~hollywood_placename(X2816,X2817)|~placename(X2816,X2817),inference(factor,[status(thm)],[c1810])).
% 4.52/4.71  cnf(c1880,plain,~actual_world(X2821)|~of(X2821,X2823,X2822)|~city(X2821,X2822)|~hollywood_placename(X2821,X2823)|~placename(X2821,X2823)|~street(X2821,X2822)|~lonely(X2821,X2822)|~chevy(X2821,X2822)|~white(X2821,X2822)|~dirty(X2821,X2822)|~old(X2821,X2822)|~event(X2821,X2824)|~agent(X2821,X2824,X2822)|~present(X2821,X2824)|~barrel(X2821,X2824)|~down(X2821,X2824,X2822)|~in(X2821,X2824,X2822),inference(factor,[status(thm)],[c1845])).
% 4.52/4.71  cnf(c309,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c310,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c311,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|~actual_world(X136)|~of(X136,X133,X132)|~city(X136,X132)|~hollywood_placename(X136,X133)|~placename(X136,X133)|~chevy(X136,X132)|~white(X136,X132)|~dirty(X136,X132)|~old(X136,X132)|~street(X136,X135)|~lonely(X136,X135)|~event(X136,X134)|~agent(X136,X134,X132)|~present(X136,X134)|~barrel(X136,X134)|~down(X136,X134,X135)|~in(X136,X134,X132),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c1083,plain,in(skolem0001,skolem0005,skolem0003)|~actual_world(skolem0006)|~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)|~street(skolem0006,X614)|~lonely(skolem0006,X614)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,X614),inference(resolution,[status(thm)],[c311, c310])).
% 4.52/4.71  cnf(c1806,plain,in(skolem0001,skolem0005,skolem0003)|~actual_world(skolem0006)|~of(skolem0006,X615,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X615)|~placename(skolem0006,X615)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~street(skolem0006,skolem0008)|~lonely(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c1083, c309])).
% 4.52/4.71  cnf(c291,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c292,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c293,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|~actual_world(X106)|~of(X106,X103,X102)|~city(X106,X102)|~hollywood_placename(X106,X103)|~placename(X106,X103)|~chevy(X106,X102)|~white(X106,X102)|~dirty(X106,X102)|~old(X106,X102)|~street(X106,X105)|~lonely(X106,X105)|~event(X106,X104)|~agent(X106,X104,X102)|~present(X106,X104)|~barrel(X106,X104)|~down(X106,X104,X105)|~in(X106,X104,X102),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c884,plain,down(skolem0001,skolem0005,skolem0004)|~actual_world(skolem0006)|~of(skolem0006,X584,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X584)|~placename(skolem0006,X584)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~street(skolem0006,X583)|~lonely(skolem0006,X583)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,X583),inference(resolution,[status(thm)],[c293, c292])).
% 4.52/4.71  cnf(c1790,plain,down(skolem0001,skolem0005,skolem0004)|~actual_world(skolem0006)|~of(skolem0006,X585,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X585)|~placename(skolem0006,X585)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~street(skolem0006,skolem0008)|~lonely(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c884, c291])).
% 4.52/4.71  cnf(c237,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c238,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c239,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|~actual_world(X86)|~of(X86,X83,X82)|~city(X86,X82)|~hollywood_placename(X86,X83)|~placename(X86,X83)|~chevy(X86,X82)|~white(X86,X82)|~dirty(X86,X82)|~old(X86,X82)|~street(X86,X85)|~lonely(X86,X85)|~event(X86,X84)|~agent(X86,X84,X82)|~present(X86,X84)|~barrel(X86,X84)|~down(X86,X84,X85)|~in(X86,X84,X82),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c526,plain,agent(skolem0001,skolem0005,skolem0003)|~actual_world(skolem0006)|~of(skolem0006,X522,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X522)|~placename(skolem0006,X522)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~street(skolem0006,X521)|~lonely(skolem0006,X521)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,X521),inference(resolution,[status(thm)],[c239, c238])).
% 4.52/4.71  cnf(c1763,plain,agent(skolem0001,skolem0005,skolem0003)|~actual_world(skolem0006)|~of(skolem0006,X523,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X523)|~placename(skolem0006,X523)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~street(skolem0006,skolem0008)|~lonely(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c526, c237])).
% 4.52/4.71  cnf(c328,negated_conjecture,~actual_world(X187)|~of(X187,X191,X190)|~city(X187,X190)|~hollywood_placename(X187,X191)|~placename(X187,X191)|~street(X187,X190)|~lonely(X187,X190)|~chevy(X187,X189)|~white(X187,X189)|~dirty(X187,X189)|~old(X187,X189)|~event(X187,X188)|~agent(X187,X188,X189)|~present(X187,X188)|~barrel(X187,X188)|~down(X187,X188,X190)|~in(X187,X188,X190)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c1466,plain,~actual_world(skolem0001)|~of(skolem0001,X327,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X327)|~placename(skolem0001,X327)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,X326)|~white(skolem0001,X326)|~dirty(skolem0001,X326)|~old(skolem0001,X326)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X326)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,skolem0003)|in(skolem0006,skolem0010,skolem0008),inference(resolution,[status(thm)],[c328, c310])).
% 4.52/4.71  cnf(c327,negated_conjecture,~actual_world(X182)|~of(X182,X186,X185)|~city(X182,X185)|~hollywood_placename(X182,X186)|~placename(X182,X186)|~street(X182,X185)|~lonely(X182,X185)|~chevy(X182,X184)|~white(X182,X184)|~dirty(X182,X184)|~old(X182,X184)|~event(X182,X183)|~agent(X182,X183,X184)|~present(X182,X183)|~barrel(X182,X183)|~down(X182,X183,X185)|~in(X182,X183,X185)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c1450,plain,~actual_world(skolem0001)|~of(skolem0001,X325,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X325)|~placename(skolem0001,X325)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,X324)|~white(skolem0001,X324)|~dirty(skolem0001,X324)|~old(skolem0001,X324)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X324)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,skolem0003)|down(skolem0006,skolem0010,skolem0008),inference(resolution,[status(thm)],[c327, c309])).
% 4.52/4.71  cnf(c324,negated_conjecture,~actual_world(X177)|~of(X177,X181,X180)|~city(X177,X180)|~hollywood_placename(X177,X181)|~placename(X177,X181)|~street(X177,X180)|~lonely(X177,X180)|~chevy(X177,X179)|~white(X177,X179)|~dirty(X177,X179)|~old(X177,X179)|~event(X177,X178)|~agent(X177,X178,X179)|~present(X177,X178)|~barrel(X177,X178)|~down(X177,X178,X180)|~in(X177,X178,X180)|agent(skolem0006,skolem0010,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c1407,plain,~actual_world(skolem0001)|~of(skolem0001,X323,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X323)|~placename(skolem0001,X323)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,X322)|~white(skolem0001,X322)|~dirty(skolem0001,X322)|~old(skolem0001,X322)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X322)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,skolem0003)|agent(skolem0006,skolem0010,skolem0009),inference(resolution,[status(thm)],[c324, c306])).
% 4.52/4.71  cnf(c295,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c313,negated_conjecture,~actual_world(X162)|~of(X162,X166,X165)|~city(X162,X165)|~hollywood_placename(X162,X166)|~placename(X162,X166)|~street(X162,X165)|~lonely(X162,X165)|~chevy(X162,X164)|~white(X162,X164)|~dirty(X162,X164)|~old(X162,X164)|~event(X162,X163)|~agent(X162,X163,X164)|~present(X162,X163)|~barrel(X162,X163)|~down(X162,X163,X165)|~in(X162,X163,X165)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c1294,plain,~actual_world(skolem0001)|~of(skolem0001,X321,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X321)|~placename(skolem0001,X321)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,X320)|~white(skolem0001,X320)|~dirty(skolem0001,X320)|~old(skolem0001,X320)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X320)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,skolem0003)|of(skolem0006,skolem0007,skolem0008),inference(resolution,[status(thm)],[c313, c295])).
% 4.52/4.71  cnf(c273,negated_conjecture,barrel(skolem0001,skolem0005)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c274,negated_conjecture,barrel(skolem0001,skolem0005)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c275,negated_conjecture,barrel(skolem0001,skolem0005)|~actual_world(X96)|~of(X96,X93,X92)|~city(X96,X92)|~hollywood_placename(X96,X93)|~placename(X96,X93)|~chevy(X96,X92)|~white(X96,X92)|~dirty(X96,X92)|~old(X96,X92)|~street(X96,X95)|~lonely(X96,X95)|~event(X96,X94)|~agent(X96,X94,X92)|~present(X96,X94)|~barrel(X96,X94)|~down(X96,X94,X95)|~in(X96,X94,X92),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c709,plain,barrel(skolem0001,skolem0005)|~actual_world(skolem0006)|~of(skolem0006,X313,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X313)|~placename(skolem0006,X313)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~street(skolem0006,X312)|~lonely(skolem0006,X312)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,X312),inference(resolution,[status(thm)],[c275, c274])).
% 4.52/4.71  cnf(c1757,plain,barrel(skolem0001,skolem0005)|~actual_world(skolem0006)|~of(skolem0006,X314,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X314)|~placename(skolem0006,X314)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~street(skolem0006,skolem0008)|~lonely(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c709, c273])).
% 4.52/4.71  cnf(c255,negated_conjecture,present(skolem0001,skolem0005)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c256,negated_conjecture,present(skolem0001,skolem0005)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c257,negated_conjecture,present(skolem0001,skolem0005)|~actual_world(X91)|~of(X91,X88,X87)|~city(X91,X87)|~hollywood_placename(X91,X88)|~placename(X91,X88)|~chevy(X91,X87)|~white(X91,X87)|~dirty(X91,X87)|~old(X91,X87)|~street(X91,X90)|~lonely(X91,X90)|~event(X91,X89)|~agent(X91,X89,X87)|~present(X91,X89)|~barrel(X91,X89)|~down(X91,X89,X90)|~in(X91,X89,X87),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c619,plain,present(skolem0001,skolem0005)|~actual_world(skolem0006)|~of(skolem0006,X306,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X306)|~placename(skolem0006,X306)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~street(skolem0006,X307)|~lonely(skolem0006,X307)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,X307),inference(resolution,[status(thm)],[c257, c256])).
% 4.52/4.71  cnf(c1728,plain,present(skolem0001,skolem0005)|~actual_world(skolem0006)|~of(skolem0006,X308,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X308)|~placename(skolem0006,X308)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~street(skolem0006,skolem0008)|~lonely(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c619, c255])).
% 4.52/4.71  cnf(c219,negated_conjecture,event(skolem0001,skolem0005)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c220,negated_conjecture,event(skolem0001,skolem0005)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c221,negated_conjecture,event(skolem0001,skolem0005)|~actual_world(X81)|~of(X81,X78,X77)|~city(X81,X77)|~hollywood_placename(X81,X78)|~placename(X81,X78)|~chevy(X81,X77)|~white(X81,X77)|~dirty(X81,X77)|~old(X81,X77)|~street(X81,X80)|~lonely(X81,X80)|~event(X81,X79)|~agent(X81,X79,X77)|~present(X81,X79)|~barrel(X81,X79)|~down(X81,X79,X80)|~in(X81,X79,X77),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c482,plain,event(skolem0001,skolem0005)|~actual_world(skolem0006)|~of(skolem0006,X302,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X302)|~placename(skolem0006,X302)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~street(skolem0006,X303)|~lonely(skolem0006,X303)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,X303),inference(resolution,[status(thm)],[c221, c220])).
% 4.52/4.71  cnf(c1724,plain,event(skolem0001,skolem0005)|~actual_world(skolem0006)|~of(skolem0006,X304,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X304)|~placename(skolem0006,X304)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~street(skolem0006,skolem0008)|~lonely(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c482, c219])).
% 4.52/4.71  cnf(c201,negated_conjecture,lonely(skolem0001,skolem0004)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c202,negated_conjecture,lonely(skolem0001,skolem0004)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c203,negated_conjecture,lonely(skolem0001,skolem0004)|~actual_world(X76)|~of(X76,X73,X72)|~city(X76,X72)|~hollywood_placename(X76,X73)|~placename(X76,X73)|~chevy(X76,X72)|~white(X76,X72)|~dirty(X76,X72)|~old(X76,X72)|~street(X76,X75)|~lonely(X76,X75)|~event(X76,X74)|~agent(X76,X74,X72)|~present(X76,X74)|~barrel(X76,X74)|~down(X76,X74,X75)|~in(X76,X74,X72),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c465,plain,lonely(skolem0001,skolem0004)|~actual_world(skolem0006)|~of(skolem0006,X296,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X296)|~placename(skolem0006,X296)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~street(skolem0006,X297)|~lonely(skolem0006,X297)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,X297),inference(resolution,[status(thm)],[c203, c202])).
% 4.52/4.71  cnf(c1693,plain,lonely(skolem0001,skolem0004)|~actual_world(skolem0006)|~of(skolem0006,X298,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X298)|~placename(skolem0006,X298)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~street(skolem0006,skolem0008)|~lonely(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c465, c201])).
% 4.52/4.71  cnf(c183,negated_conjecture,street(skolem0001,skolem0004)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c184,negated_conjecture,street(skolem0001,skolem0004)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c185,negated_conjecture,street(skolem0001,skolem0004)|~actual_world(X71)|~of(X71,X68,X67)|~city(X71,X67)|~hollywood_placename(X71,X68)|~placename(X71,X68)|~chevy(X71,X67)|~white(X71,X67)|~dirty(X71,X67)|~old(X71,X67)|~street(X71,X70)|~lonely(X71,X70)|~event(X71,X69)|~agent(X71,X69,X67)|~present(X71,X69)|~barrel(X71,X69)|~down(X71,X69,X70)|~in(X71,X69,X67),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c447,plain,street(skolem0001,skolem0004)|~actual_world(skolem0006)|~of(skolem0006,X291,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X291)|~placename(skolem0006,X291)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~street(skolem0006,X290)|~lonely(skolem0006,X290)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,X290),inference(resolution,[status(thm)],[c185, c184])).
% 4.52/4.71  cnf(c1681,plain,street(skolem0001,skolem0004)|~actual_world(skolem0006)|~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)|~street(skolem0006,skolem0008)|~lonely(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c447, c183])).
% 4.52/4.71  cnf(c165,negated_conjecture,old(skolem0001,skolem0003)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c166,negated_conjecture,old(skolem0001,skolem0003)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c167,negated_conjecture,old(skolem0001,skolem0003)|~actual_world(X66)|~of(X66,X63,X62)|~city(X66,X62)|~hollywood_placename(X66,X63)|~placename(X66,X63)|~chevy(X66,X62)|~white(X66,X62)|~dirty(X66,X62)|~old(X66,X62)|~street(X66,X65)|~lonely(X66,X65)|~event(X66,X64)|~agent(X66,X64,X62)|~present(X66,X64)|~barrel(X66,X64)|~down(X66,X64,X65)|~in(X66,X64,X62),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c427,plain,old(skolem0001,skolem0003)|~actual_world(skolem0006)|~of(skolem0006,X286,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X286)|~placename(skolem0006,X286)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~street(skolem0006,X287)|~lonely(skolem0006,X287)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,X287),inference(resolution,[status(thm)],[c167, c166])).
% 4.52/4.71  cnf(c1665,plain,old(skolem0001,skolem0003)|~actual_world(skolem0006)|~of(skolem0006,X288,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X288)|~placename(skolem0006,X288)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~street(skolem0006,skolem0008)|~lonely(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c427, c165])).
% 4.52/4.71  cnf(c147,negated_conjecture,dirty(skolem0001,skolem0003)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c148,negated_conjecture,dirty(skolem0001,skolem0003)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c149,negated_conjecture,dirty(skolem0001,skolem0003)|~actual_world(X61)|~of(X61,X58,X57)|~city(X61,X57)|~hollywood_placename(X61,X58)|~placename(X61,X58)|~chevy(X61,X57)|~white(X61,X57)|~dirty(X61,X57)|~old(X61,X57)|~street(X61,X60)|~lonely(X61,X60)|~event(X61,X59)|~agent(X61,X59,X57)|~present(X61,X59)|~barrel(X61,X59)|~down(X61,X59,X60)|~in(X61,X59,X57),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c393,plain,dirty(skolem0001,skolem0003)|~actual_world(skolem0006)|~of(skolem0006,X281,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X281)|~placename(skolem0006,X281)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~street(skolem0006,X280)|~lonely(skolem0006,X280)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,X280),inference(resolution,[status(thm)],[c149, c148])).
% 4.52/4.71  cnf(c1649,plain,dirty(skolem0001,skolem0003)|~actual_world(skolem0006)|~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)|~street(skolem0006,skolem0008)|~lonely(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c393, c147])).
% 4.52/4.71  cnf(c129,negated_conjecture,white(skolem0001,skolem0003)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c130,negated_conjecture,white(skolem0001,skolem0003)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c131,negated_conjecture,white(skolem0001,skolem0003)|~actual_world(X56)|~of(X56,X53,X52)|~city(X56,X52)|~hollywood_placename(X56,X53)|~placename(X56,X53)|~chevy(X56,X52)|~white(X56,X52)|~dirty(X56,X52)|~old(X56,X52)|~street(X56,X55)|~lonely(X56,X55)|~event(X56,X54)|~agent(X56,X54,X52)|~present(X56,X54)|~barrel(X56,X54)|~down(X56,X54,X55)|~in(X56,X54,X52),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c383,plain,white(skolem0001,skolem0003)|~actual_world(skolem0006)|~of(skolem0006,X277,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X277)|~placename(skolem0006,X277)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~street(skolem0006,X276)|~lonely(skolem0006,X276)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,X276),inference(resolution,[status(thm)],[c131, c130])).
% 4.52/4.71  cnf(c1633,plain,white(skolem0001,skolem0003)|~actual_world(skolem0006)|~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)|~street(skolem0006,skolem0008)|~lonely(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c383, c129])).
% 4.52/4.71  cnf(c111,negated_conjecture,chevy(skolem0001,skolem0003)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c112,negated_conjecture,chevy(skolem0001,skolem0003)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c113,negated_conjecture,chevy(skolem0001,skolem0003)|~actual_world(X51)|~of(X51,X48,X47)|~city(X51,X47)|~hollywood_placename(X51,X48)|~placename(X51,X48)|~chevy(X51,X47)|~white(X51,X47)|~dirty(X51,X47)|~old(X51,X47)|~street(X51,X50)|~lonely(X51,X50)|~event(X51,X49)|~agent(X51,X49,X47)|~present(X51,X49)|~barrel(X51,X49)|~down(X51,X49,X50)|~in(X51,X49,X47),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c367,plain,chevy(skolem0001,skolem0003)|~actual_world(skolem0006)|~of(skolem0006,X271,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X271)|~placename(skolem0006,X271)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~street(skolem0006,X270)|~lonely(skolem0006,X270)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,X270),inference(resolution,[status(thm)],[c113, c112])).
% 4.52/4.71  cnf(c1611,plain,chevy(skolem0001,skolem0003)|~actual_world(skolem0006)|~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)|~street(skolem0006,skolem0008)|~lonely(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c367, c111])).
% 4.52/4.71  cnf(c93,negated_conjecture,placename(skolem0001,skolem0002)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c94,negated_conjecture,placename(skolem0001,skolem0002)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c95,negated_conjecture,placename(skolem0001,skolem0002)|~actual_world(X46)|~of(X46,X43,X42)|~city(X46,X42)|~hollywood_placename(X46,X43)|~placename(X46,X43)|~chevy(X46,X42)|~white(X46,X42)|~dirty(X46,X42)|~old(X46,X42)|~street(X46,X45)|~lonely(X46,X45)|~event(X46,X44)|~agent(X46,X44,X42)|~present(X46,X44)|~barrel(X46,X44)|~down(X46,X44,X45)|~in(X46,X44,X42),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c355,plain,placename(skolem0001,skolem0002)|~actual_world(skolem0006)|~of(skolem0006,X264,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X264)|~placename(skolem0006,X264)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~street(skolem0006,X265)|~lonely(skolem0006,X265)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,X265),inference(resolution,[status(thm)],[c95, c94])).
% 4.52/4.71  cnf(c1600,plain,placename(skolem0001,skolem0002)|~actual_world(skolem0006)|~of(skolem0006,X268,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X268)|~placename(skolem0006,X268)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~street(skolem0006,skolem0008)|~lonely(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c355, c93])).
% 4.52/4.71  cnf(c75,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c76,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c77,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|~actual_world(X41)|~of(X41,X38,X37)|~city(X41,X37)|~hollywood_placename(X41,X38)|~placename(X41,X38)|~chevy(X41,X37)|~white(X41,X37)|~dirty(X41,X37)|~old(X41,X37)|~street(X41,X40)|~lonely(X41,X40)|~event(X41,X39)|~agent(X41,X39,X37)|~present(X41,X39)|~barrel(X41,X39)|~down(X41,X39,X40)|~in(X41,X39,X37),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c345,plain,hollywood_placename(skolem0001,skolem0002)|~actual_world(skolem0006)|~of(skolem0006,X260,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X260)|~placename(skolem0006,X260)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~street(skolem0006,X261)|~lonely(skolem0006,X261)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,X261),inference(resolution,[status(thm)],[c77, c76])).
% 4.52/4.71  cnf(c1578,plain,hollywood_placename(skolem0001,skolem0002)|~actual_world(skolem0006)|~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)|~street(skolem0006,skolem0008)|~lonely(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c345, c75])).
% 4.52/4.71  cnf(c57,negated_conjecture,city(skolem0001,skolem0003)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c58,negated_conjecture,city(skolem0001,skolem0003)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c59,negated_conjecture,city(skolem0001,skolem0003)|~actual_world(X36)|~of(X36,X33,X32)|~city(X36,X32)|~hollywood_placename(X36,X33)|~placename(X36,X33)|~chevy(X36,X32)|~white(X36,X32)|~dirty(X36,X32)|~old(X36,X32)|~street(X36,X35)|~lonely(X36,X35)|~event(X36,X34)|~agent(X36,X34,X32)|~present(X36,X34)|~barrel(X36,X34)|~down(X36,X34,X35)|~in(X36,X34,X32),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c337,plain,city(skolem0001,skolem0003)|~actual_world(skolem0006)|~of(skolem0006,X254,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X254)|~placename(skolem0006,X254)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~street(skolem0006,X255)|~lonely(skolem0006,X255)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,X255),inference(resolution,[status(thm)],[c59, c58])).
% 4.52/4.71  cnf(c1555,plain,city(skolem0001,skolem0003)|~actual_world(skolem0006)|~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)|~street(skolem0006,skolem0008)|~lonely(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c337, c57])).
% 4.52/4.71  cnf(c39,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c40,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c41,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|~actual_world(X31)|~of(X31,X28,X27)|~city(X31,X27)|~hollywood_placename(X31,X28)|~placename(X31,X28)|~chevy(X31,X27)|~white(X31,X27)|~dirty(X31,X27)|~old(X31,X27)|~street(X31,X30)|~lonely(X31,X30)|~event(X31,X29)|~agent(X31,X29,X27)|~present(X31,X29)|~barrel(X31,X29)|~down(X31,X29,X30)|~in(X31,X29,X27),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c333,plain,of(skolem0001,skolem0002,skolem0003)|~actual_world(skolem0006)|~of(skolem0006,X236,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X236)|~placename(skolem0006,X236)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~street(skolem0006,X235)|~lonely(skolem0006,X235)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,X235),inference(resolution,[status(thm)],[c41, c40])).
% 4.52/4.71  cnf(c1539,plain,of(skolem0001,skolem0002,skolem0003)|~actual_world(skolem0006)|~of(skolem0006,X237,skolem0008)|~city(skolem0006,skolem0008)|~hollywood_placename(skolem0006,X237)|~placename(skolem0006,X237)|~chevy(skolem0006,skolem0008)|~white(skolem0006,skolem0008)|~dirty(skolem0006,skolem0008)|~old(skolem0006,skolem0008)|~street(skolem0006,skolem0008)|~lonely(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c333, c39])).
% 4.52/4.71  cnf(c308,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c326,negated_conjecture,~actual_world(X172)|~of(X172,X176,X175)|~city(X172,X175)|~hollywood_placename(X172,X176)|~placename(X172,X176)|~street(X172,X175)|~lonely(X172,X175)|~chevy(X172,X174)|~white(X172,X174)|~dirty(X172,X174)|~old(X172,X174)|~event(X172,X173)|~agent(X172,X173,X174)|~present(X172,X173)|~barrel(X172,X173)|~down(X172,X173,X175)|~in(X172,X173,X175)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c1366,plain,~actual_world(skolem0001)|~of(skolem0001,X233,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X233)|~placename(skolem0001,X233)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,X234)|~white(skolem0001,X234)|~dirty(skolem0001,X234)|~old(skolem0001,X234)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X234)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,skolem0003)|barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c326, c308])).
% 4.52/4.71  cnf(c307,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c325,negated_conjecture,~actual_world(X167)|~of(X167,X171,X170)|~city(X167,X170)|~hollywood_placename(X167,X171)|~placename(X167,X171)|~street(X167,X170)|~lonely(X167,X170)|~chevy(X167,X169)|~white(X167,X169)|~dirty(X167,X169)|~old(X167,X169)|~event(X167,X168)|~agent(X167,X168,X169)|~present(X167,X168)|~barrel(X167,X168)|~down(X167,X168,X170)|~in(X167,X168,X170)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c1316,plain,~actual_world(skolem0001)|~of(skolem0001,X231,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X231)|~placename(skolem0001,X231)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~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,skolem0003)|present(skolem0006,skolem0010),inference(resolution,[status(thm)],[c325, c307])).
% 4.52/4.71  cnf(c305,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c323,negated_conjecture,~actual_world(X157)|~of(X157,X161,X160)|~city(X157,X160)|~hollywood_placename(X157,X161)|~placename(X157,X161)|~street(X157,X160)|~lonely(X157,X160)|~chevy(X157,X159)|~white(X157,X159)|~dirty(X157,X159)|~old(X157,X159)|~event(X157,X158)|~agent(X157,X158,X159)|~present(X157,X158)|~barrel(X157,X158)|~down(X157,X158,X160)|~in(X157,X158,X160)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c1252,plain,~actual_world(skolem0001)|~of(skolem0001,X229,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X229)|~placename(skolem0001,X229)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~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,skolem0003)|event(skolem0006,skolem0010),inference(resolution,[status(thm)],[c323, c305])).
% 4.52/4.71  cnf(c304,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c322,negated_conjecture,~actual_world(X152)|~of(X152,X156,X155)|~city(X152,X155)|~hollywood_placename(X152,X156)|~placename(X152,X156)|~street(X152,X155)|~lonely(X152,X155)|~chevy(X152,X154)|~white(X152,X154)|~dirty(X152,X154)|~old(X152,X154)|~event(X152,X153)|~agent(X152,X153,X154)|~present(X152,X153)|~barrel(X152,X153)|~down(X152,X153,X155)|~in(X152,X153,X155)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c1222,plain,~actual_world(skolem0001)|~of(skolem0001,X227,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X227)|~placename(skolem0001,X227)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,X228)|~white(skolem0001,X228)|~dirty(skolem0001,X228)|~old(skolem0001,X228)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X228)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,skolem0003)|old(skolem0006,skolem0009),inference(resolution,[status(thm)],[c322, c304])).
% 4.52/4.71  cnf(c303,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c321,negated_conjecture,~actual_world(X147)|~of(X147,X151,X150)|~city(X147,X150)|~hollywood_placename(X147,X151)|~placename(X147,X151)|~street(X147,X150)|~lonely(X147,X150)|~chevy(X147,X149)|~white(X147,X149)|~dirty(X147,X149)|~old(X147,X149)|~event(X147,X148)|~agent(X147,X148,X149)|~present(X147,X148)|~barrel(X147,X148)|~down(X147,X148,X150)|~in(X147,X148,X150)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c1195,plain,~actual_world(skolem0001)|~of(skolem0001,X226,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X226)|~placename(skolem0001,X226)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,X225)|~white(skolem0001,X225)|~dirty(skolem0001,X225)|~old(skolem0001,X225)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X225)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,skolem0003)|dirty(skolem0006,skolem0009),inference(resolution,[status(thm)],[c321, c303])).
% 4.52/4.71  cnf(c302,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c320,negated_conjecture,~actual_world(X142)|~of(X142,X146,X145)|~city(X142,X145)|~hollywood_placename(X142,X146)|~placename(X142,X146)|~street(X142,X145)|~lonely(X142,X145)|~chevy(X142,X144)|~white(X142,X144)|~dirty(X142,X144)|~old(X142,X144)|~event(X142,X143)|~agent(X142,X143,X144)|~present(X142,X143)|~barrel(X142,X143)|~down(X142,X143,X145)|~in(X142,X143,X145)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c1166,plain,~actual_world(skolem0001)|~of(skolem0001,X222,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X222)|~placename(skolem0001,X222)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,X221)|~white(skolem0001,X221)|~dirty(skolem0001,X221)|~old(skolem0001,X221)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X221)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,skolem0003)|white(skolem0006,skolem0009),inference(resolution,[status(thm)],[c320, c302])).
% 4.52/4.71  cnf(c301,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c319,negated_conjecture,~actual_world(X137)|~of(X137,X141,X140)|~city(X137,X140)|~hollywood_placename(X137,X141)|~placename(X137,X141)|~street(X137,X140)|~lonely(X137,X140)|~chevy(X137,X139)|~white(X137,X139)|~dirty(X137,X139)|~old(X137,X139)|~event(X137,X138)|~agent(X137,X138,X139)|~present(X137,X138)|~barrel(X137,X138)|~down(X137,X138,X140)|~in(X137,X138,X140)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c1134,plain,~actual_world(skolem0001)|~of(skolem0001,X219,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X219)|~placename(skolem0001,X219)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,X220)|~white(skolem0001,X220)|~dirty(skolem0001,X220)|~old(skolem0001,X220)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X220)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,skolem0003)|chevy(skolem0006,skolem0009),inference(resolution,[status(thm)],[c319, c301])).
% 4.52/4.71  cnf(c300,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c318,negated_conjecture,~actual_world(X127)|~of(X127,X131,X130)|~city(X127,X130)|~hollywood_placename(X127,X131)|~placename(X127,X131)|~street(X127,X130)|~lonely(X127,X130)|~chevy(X127,X129)|~white(X127,X129)|~dirty(X127,X129)|~old(X127,X129)|~event(X127,X128)|~agent(X127,X128,X129)|~present(X127,X128)|~barrel(X127,X128)|~down(X127,X128,X130)|~in(X127,X128,X130)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.71  cnf(c1045,plain,~actual_world(skolem0001)|~of(skolem0001,X218,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X218)|~placename(skolem0001,X218)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~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,skolem0003)|lonely(skolem0006,skolem0008),inference(resolution,[status(thm)],[c318, c300])).
% 4.52/4.71  cnf(c299,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c317,negated_conjecture,~actual_world(X122)|~of(X122,X126,X125)|~city(X122,X125)|~hollywood_placename(X122,X126)|~placename(X122,X126)|~street(X122,X125)|~lonely(X122,X125)|~chevy(X122,X124)|~white(X122,X124)|~dirty(X122,X124)|~old(X122,X124)|~event(X122,X123)|~agent(X122,X123,X124)|~present(X122,X123)|~barrel(X122,X123)|~down(X122,X123,X125)|~in(X122,X123,X125)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c1043,plain,~actual_world(skolem0001)|~of(skolem0001,X215,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X215)|~placename(skolem0001,X215)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,X216)|~white(skolem0001,X216)|~dirty(skolem0001,X216)|~old(skolem0001,X216)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X216)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,skolem0003)|street(skolem0006,skolem0008),inference(resolution,[status(thm)],[c317, c299])).
% 4.52/4.72  cnf(c298,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c316,negated_conjecture,~actual_world(X117)|~of(X117,X121,X120)|~city(X117,X120)|~hollywood_placename(X117,X121)|~placename(X117,X121)|~street(X117,X120)|~lonely(X117,X120)|~chevy(X117,X119)|~white(X117,X119)|~dirty(X117,X119)|~old(X117,X119)|~event(X117,X118)|~agent(X117,X118,X119)|~present(X117,X118)|~barrel(X117,X118)|~down(X117,X118,X120)|~in(X117,X118,X120)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c1003,plain,~actual_world(skolem0001)|~of(skolem0001,X214,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X214)|~placename(skolem0001,X214)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~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,skolem0003)|placename(skolem0006,skolem0007),inference(resolution,[status(thm)],[c316, c298])).
% 4.52/4.72  cnf(c297,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c315,negated_conjecture,~actual_world(X112)|~of(X112,X116,X115)|~city(X112,X115)|~hollywood_placename(X112,X116)|~placename(X112,X116)|~street(X112,X115)|~lonely(X112,X115)|~chevy(X112,X114)|~white(X112,X114)|~dirty(X112,X114)|~old(X112,X114)|~event(X112,X113)|~agent(X112,X113,X114)|~present(X112,X113)|~barrel(X112,X113)|~down(X112,X113,X115)|~in(X112,X113,X115)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c967,plain,~actual_world(skolem0001)|~of(skolem0001,X209,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X209)|~placename(skolem0001,X209)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,X210)|~white(skolem0001,X210)|~dirty(skolem0001,X210)|~old(skolem0001,X210)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X210)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,skolem0003)|hollywood_placename(skolem0006,skolem0007),inference(resolution,[status(thm)],[c315, c297])).
% 4.52/4.72  cnf(c296,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c314,negated_conjecture,~actual_world(X107)|~of(X107,X111,X110)|~city(X107,X110)|~hollywood_placename(X107,X111)|~placename(X107,X111)|~street(X107,X110)|~lonely(X107,X110)|~chevy(X107,X109)|~white(X107,X109)|~dirty(X107,X109)|~old(X107,X109)|~event(X107,X108)|~agent(X107,X108,X109)|~present(X107,X108)|~barrel(X107,X108)|~down(X107,X108,X110)|~in(X107,X108,X110)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c938,plain,~actual_world(skolem0001)|~of(skolem0001,X208,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X208)|~placename(skolem0001,X208)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~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,skolem0003)|city(skolem0006,skolem0008),inference(resolution,[status(thm)],[c314, c296])).
% 4.52/4.72  cnf(c21,negated_conjecture,actual_world(skolem0001)|down(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c22,negated_conjecture,actual_world(skolem0001)|in(skolem0006,skolem0010,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c23,negated_conjecture,actual_world(skolem0001)|~actual_world(X26)|~of(X26,X23,X22)|~city(X26,X22)|~hollywood_placename(X26,X23)|~placename(X26,X23)|~chevy(X26,X22)|~white(X26,X22)|~dirty(X26,X22)|~old(X26,X22)|~street(X26,X25)|~lonely(X26,X25)|~event(X26,X24)|~agent(X26,X24,X22)|~present(X26,X24)|~barrel(X26,X24)|~down(X26,X24,X25)|~in(X26,X24,X22),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c330,plain,actual_world(skolem0001)|~actual_world(skolem0006)|~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)|~street(skolem0006,X204)|~lonely(skolem0006,X204)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010)|~down(skolem0006,skolem0010,X204),inference(resolution,[status(thm)],[c23, c22])).
% 4.52/4.72  cnf(c1533,plain,actual_world(skolem0001)|~actual_world(skolem0006)|~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)|~street(skolem0006,skolem0008)|~lonely(skolem0006,skolem0008)|~event(skolem0006,skolem0010)|~agent(skolem0006,skolem0010,skolem0008)|~present(skolem0006,skolem0010)|~barrel(skolem0006,skolem0010),inference(resolution,[status(thm)],[c330, c21])).
% 4.52/4.72  cnf(c294,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c312,negated_conjecture,~actual_world(X97)|~of(X97,X101,X100)|~city(X97,X100)|~hollywood_placename(X97,X101)|~placename(X97,X101)|~street(X97,X100)|~lonely(X97,X100)|~chevy(X97,X99)|~white(X97,X99)|~dirty(X97,X99)|~old(X97,X99)|~event(X97,X98)|~agent(X97,X98,X99)|~present(X97,X98)|~barrel(X97,X98)|~down(X97,X98,X100)|~in(X97,X98,X100)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c843,plain,~actual_world(skolem0001)|~of(skolem0001,X202,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X202)|~placename(skolem0001,X202)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~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,skolem0003)|actual_world(skolem0006),inference(resolution,[status(thm)],[c312, c294])).
% 4.52/4.72  cnf(c277,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c290,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c289,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c287,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c286,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c285,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c284,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c283,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c282,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c281,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c280,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c279,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c278,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c259,negated_conjecture,barrel(skolem0001,skolem0005)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c241,negated_conjecture,present(skolem0001,skolem0005)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c223,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c236,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c235,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c233,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c232,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c231,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c230,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c229,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c228,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c227,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c226,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c225,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c224,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c205,negated_conjecture,event(skolem0001,skolem0005)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c187,negated_conjecture,lonely(skolem0001,skolem0004)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c169,negated_conjecture,street(skolem0001,skolem0004)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c151,negated_conjecture,old(skolem0001,skolem0003)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c133,negated_conjecture,dirty(skolem0001,skolem0003)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c115,negated_conjecture,white(skolem0001,skolem0003)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c97,negated_conjecture,chevy(skolem0001,skolem0003)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c276,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c272,negated_conjecture,barrel(skolem0001,skolem0005)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c271,negated_conjecture,barrel(skolem0001,skolem0005)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c269,negated_conjecture,barrel(skolem0001,skolem0005)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c268,negated_conjecture,barrel(skolem0001,skolem0005)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c267,negated_conjecture,barrel(skolem0001,skolem0005)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c266,negated_conjecture,barrel(skolem0001,skolem0005)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c79,negated_conjecture,placename(skolem0001,skolem0002)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c265,negated_conjecture,barrel(skolem0001,skolem0005)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c264,negated_conjecture,barrel(skolem0001,skolem0005)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c263,negated_conjecture,barrel(skolem0001,skolem0005)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c262,negated_conjecture,barrel(skolem0001,skolem0005)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c261,negated_conjecture,barrel(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c260,negated_conjecture,barrel(skolem0001,skolem0005)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c254,negated_conjecture,present(skolem0001,skolem0005)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c253,negated_conjecture,present(skolem0001,skolem0005)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c251,negated_conjecture,present(skolem0001,skolem0005)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c250,negated_conjecture,present(skolem0001,skolem0005)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c249,negated_conjecture,present(skolem0001,skolem0005)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c248,negated_conjecture,present(skolem0001,skolem0005)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c247,negated_conjecture,present(skolem0001,skolem0005)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c246,negated_conjecture,present(skolem0001,skolem0005)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c245,negated_conjecture,present(skolem0001,skolem0005)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c244,negated_conjecture,present(skolem0001,skolem0005)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c243,negated_conjecture,present(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c242,negated_conjecture,present(skolem0001,skolem0005)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c222,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c218,negated_conjecture,event(skolem0001,skolem0005)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c217,negated_conjecture,event(skolem0001,skolem0005)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c215,negated_conjecture,event(skolem0001,skolem0005)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c214,negated_conjecture,event(skolem0001,skolem0005)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c213,negated_conjecture,event(skolem0001,skolem0005)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c212,negated_conjecture,event(skolem0001,skolem0005)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c61,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c211,negated_conjecture,event(skolem0001,skolem0005)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c210,negated_conjecture,event(skolem0001,skolem0005)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c209,negated_conjecture,event(skolem0001,skolem0005)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c208,negated_conjecture,event(skolem0001,skolem0005)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c207,negated_conjecture,event(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c206,negated_conjecture,event(skolem0001,skolem0005)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c200,negated_conjecture,lonely(skolem0001,skolem0004)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c199,negated_conjecture,lonely(skolem0001,skolem0004)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c197,negated_conjecture,lonely(skolem0001,skolem0004)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c196,negated_conjecture,lonely(skolem0001,skolem0004)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c195,negated_conjecture,lonely(skolem0001,skolem0004)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c194,negated_conjecture,lonely(skolem0001,skolem0004)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c193,negated_conjecture,lonely(skolem0001,skolem0004)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c192,negated_conjecture,lonely(skolem0001,skolem0004)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c191,negated_conjecture,lonely(skolem0001,skolem0004)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c190,negated_conjecture,lonely(skolem0001,skolem0004)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c189,negated_conjecture,lonely(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c188,negated_conjecture,lonely(skolem0001,skolem0004)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c182,negated_conjecture,street(skolem0001,skolem0004)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c181,negated_conjecture,street(skolem0001,skolem0004)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c179,negated_conjecture,street(skolem0001,skolem0004)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c178,negated_conjecture,street(skolem0001,skolem0004)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c177,negated_conjecture,street(skolem0001,skolem0004)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c176,negated_conjecture,street(skolem0001,skolem0004)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c175,negated_conjecture,street(skolem0001,skolem0004)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c43,negated_conjecture,city(skolem0001,skolem0003)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c174,negated_conjecture,street(skolem0001,skolem0004)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c173,negated_conjecture,street(skolem0001,skolem0004)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c172,negated_conjecture,street(skolem0001,skolem0004)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c171,negated_conjecture,street(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c170,negated_conjecture,street(skolem0001,skolem0004)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c164,negated_conjecture,old(skolem0001,skolem0003)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c163,negated_conjecture,old(skolem0001,skolem0003)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c161,negated_conjecture,old(skolem0001,skolem0003)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c160,negated_conjecture,old(skolem0001,skolem0003)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c159,negated_conjecture,old(skolem0001,skolem0003)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c158,negated_conjecture,old(skolem0001,skolem0003)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c157,negated_conjecture,old(skolem0001,skolem0003)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c156,negated_conjecture,old(skolem0001,skolem0003)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c155,negated_conjecture,old(skolem0001,skolem0003)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c154,negated_conjecture,old(skolem0001,skolem0003)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c153,negated_conjecture,old(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c152,negated_conjecture,old(skolem0001,skolem0003)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c146,negated_conjecture,dirty(skolem0001,skolem0003)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c145,negated_conjecture,dirty(skolem0001,skolem0003)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c143,negated_conjecture,dirty(skolem0001,skolem0003)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c38,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c142,negated_conjecture,dirty(skolem0001,skolem0003)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c141,negated_conjecture,dirty(skolem0001,skolem0003)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c140,negated_conjecture,dirty(skolem0001,skolem0003)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c139,negated_conjecture,dirty(skolem0001,skolem0003)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c138,negated_conjecture,dirty(skolem0001,skolem0003)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c37,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c137,negated_conjecture,dirty(skolem0001,skolem0003)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c136,negated_conjecture,dirty(skolem0001,skolem0003)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c135,negated_conjecture,dirty(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c134,negated_conjecture,dirty(skolem0001,skolem0003)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c128,negated_conjecture,white(skolem0001,skolem0003)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c127,negated_conjecture,white(skolem0001,skolem0003)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c125,negated_conjecture,white(skolem0001,skolem0003)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c124,negated_conjecture,white(skolem0001,skolem0003)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c123,negated_conjecture,white(skolem0001,skolem0003)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c122,negated_conjecture,white(skolem0001,skolem0003)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c35,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c121,negated_conjecture,white(skolem0001,skolem0003)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c120,negated_conjecture,white(skolem0001,skolem0003)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c119,negated_conjecture,white(skolem0001,skolem0003)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c118,negated_conjecture,white(skolem0001,skolem0003)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c117,negated_conjecture,white(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c34,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c116,negated_conjecture,white(skolem0001,skolem0003)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c110,negated_conjecture,chevy(skolem0001,skolem0003)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c109,negated_conjecture,chevy(skolem0001,skolem0003)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c107,negated_conjecture,chevy(skolem0001,skolem0003)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c106,negated_conjecture,chevy(skolem0001,skolem0003)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c33,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c105,negated_conjecture,chevy(skolem0001,skolem0003)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c104,negated_conjecture,chevy(skolem0001,skolem0003)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c103,negated_conjecture,chevy(skolem0001,skolem0003)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c102,negated_conjecture,chevy(skolem0001,skolem0003)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c101,negated_conjecture,chevy(skolem0001,skolem0003)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c32,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c100,negated_conjecture,chevy(skolem0001,skolem0003)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c99,negated_conjecture,chevy(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c98,negated_conjecture,chevy(skolem0001,skolem0003)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c92,negated_conjecture,placename(skolem0001,skolem0002)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c91,negated_conjecture,placename(skolem0001,skolem0002)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c31,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c89,negated_conjecture,placename(skolem0001,skolem0002)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c88,negated_conjecture,placename(skolem0001,skolem0002)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c87,negated_conjecture,placename(skolem0001,skolem0002)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c86,negated_conjecture,placename(skolem0001,skolem0002)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c85,negated_conjecture,placename(skolem0001,skolem0002)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c30,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c84,negated_conjecture,placename(skolem0001,skolem0002)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c83,negated_conjecture,placename(skolem0001,skolem0002)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c82,negated_conjecture,placename(skolem0001,skolem0002)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c81,negated_conjecture,placename(skolem0001,skolem0002)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c80,negated_conjecture,placename(skolem0001,skolem0002)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c29,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c74,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c73,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c71,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c70,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c69,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c28,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c68,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c67,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c66,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c65,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c64,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c27,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c63,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c62,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c56,negated_conjecture,city(skolem0001,skolem0003)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c55,negated_conjecture,city(skolem0001,skolem0003)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c53,negated_conjecture,city(skolem0001,skolem0003)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c26,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c52,negated_conjecture,city(skolem0001,skolem0003)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c51,negated_conjecture,city(skolem0001,skolem0003)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c50,negated_conjecture,city(skolem0001,skolem0003)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c49,negated_conjecture,city(skolem0001,skolem0003)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c48,negated_conjecture,city(skolem0001,skolem0003)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c25,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c47,negated_conjecture,city(skolem0001,skolem0003)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c46,negated_conjecture,city(skolem0001,skolem0003)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c45,negated_conjecture,city(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c44,negated_conjecture,city(skolem0001,skolem0003)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c24,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c258,negated_conjecture,barrel(skolem0001,skolem0005)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c240,negated_conjecture,present(skolem0001,skolem0005)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c204,negated_conjecture,event(skolem0001,skolem0005)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c186,negated_conjecture,lonely(skolem0001,skolem0004)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c168,negated_conjecture,street(skolem0001,skolem0004)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c150,negated_conjecture,old(skolem0001,skolem0003)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c132,negated_conjecture,dirty(skolem0001,skolem0003)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c114,negated_conjecture,white(skolem0001,skolem0003)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c96,negated_conjecture,chevy(skolem0001,skolem0003)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c78,negated_conjecture,placename(skolem0001,skolem0002)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c60,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c42,negated_conjecture,city(skolem0001,skolem0003)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c20,negated_conjecture,actual_world(skolem0001)|barrel(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c19,negated_conjecture,actual_world(skolem0001)|present(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c17,negated_conjecture,actual_world(skolem0001)|event(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c16,negated_conjecture,actual_world(skolem0001)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c15,negated_conjecture,actual_world(skolem0001)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c14,negated_conjecture,actual_world(skolem0001)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c13,negated_conjecture,actual_world(skolem0001)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c12,negated_conjecture,actual_world(skolem0001)|lonely(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c7,negated_conjecture,actual_world(skolem0001)|of(skolem0006,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c11,negated_conjecture,actual_world(skolem0001)|street(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c10,negated_conjecture,actual_world(skolem0001)|placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c9,negated_conjecture,actual_world(skolem0001)|hollywood_placename(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c8,negated_conjecture,actual_world(skolem0001)|city(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  cnf(c6,negated_conjecture,actual_world(skolem0001)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 4.52/4.72  % SZS output end Saturation
% 4.52/4.72  
% 4.52/4.72  % Initial clauses    : 324
% 4.52/4.72  % Processed clauses  : 413
% 4.52/4.72  % Factors computed   : 21
% 4.52/4.72  % Resolvents computed: 1615
% 4.52/4.72  % Tautologies deleted: 306
% 4.52/4.72  % Forward subsumed   : 1241
% 4.52/4.72  % Backward subsumed  : 20
% 4.52/4.72  % -------- CPU Time ---------
% 4.52/4.72  % User time          : 4.344 s
% 4.52/4.72  % System time        : 0.017 s
% 4.52/4.72  % Total time         : 4.361 s
%------------------------------------------------------------------------------