%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP118+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n023.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:11 EDT 2024
% Result : CounterSatisfiable 6.65s 6.86s
% Output : Saturation 6.73s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : NLP118+1 : TPTP v8.1.2. Released v2.4.0.
% 0.12/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n023.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 13:43:23 EDT 2024
% 0.13/0.35 % CPUTime :
% 6.65/6.86 % Version: 1.5
% 6.65/6.86 % SZS status CounterSatisfiable
% 6.65/6.86 % SZS output start Saturation
% 6.65/6.86 fof(co1,conjecture,(~(~(((?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(((((((((((((((of(U,W,V)&city(U,V))&hollywood_placename(U,W))&placename(U,W))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&street(U,Y))&lonely(U,Y))&event(U,Z))&agent(U,Z,X))&present(U,Z))&barrel(U,Z))&down(U,Z,Y))&in(U,Z,V)))))))))=>(?[X1]:(actual_world(X1)&(?[X2]:(?[X3]:(?[X4]:(?[X5]:(((((((((((((((of(X1,X2,X3)&city(X1,X3))&hollywood_placename(X1,X2))&placename(X1,X2))&street(X1,X3))&lonely(X1,X3))&chevy(X1,X4))&white(X1,X4))&dirty(X1,X4))&old(X1,X4))&event(X1,X5))&agent(X1,X5,X4))&present(X1,X5))&barrel(X1,X5))&down(X1,X5,X3))&in(X1,X5,X3)))))))))&((?[X1]:(actual_world(X1)&(?[X2]:(?[X3]:(?[X4]:(?[X5]:(((((((((((((((of(X1,X2,X3)&city(X1,X3))&hollywood_placename(X1,X2))&placename(X1,X2))&street(X1,X3))&lonely(X1,X3))&chevy(X1,X4))&white(X1,X4))&dirty(X1,X4))&old(X1,X4))&event(X1,X5))&agent(X1,X5,X4))&present(X1,X5))&barrel(X1,X5))&down(X1,X5,X3))&in(X1,X5,X3))))))))=>(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(((((((((((((((of(U,W,V)&city(U,V))&hollywood_placename(U,W))&placename(U,W))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&street(U,Y))&lonely(U,Y))&event(U,Z))&agent(U,Z,X))&present(U,Z))&barrel(U,Z))&down(U,Z,Y))&in(U,Z,V))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', co1)).
% 6.65/6.86 fof(c0,negated_conjecture,(~(~(~(((?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(((((((((((((((of(U,W,V)&city(U,V))&hollywood_placename(U,W))&placename(U,W))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&street(U,Y))&lonely(U,Y))&event(U,Z))&agent(U,Z,X))&present(U,Z))&barrel(U,Z))&down(U,Z,Y))&in(U,Z,V)))))))))=>(?[X1]:(actual_world(X1)&(?[X2]:(?[X3]:(?[X4]:(?[X5]:(((((((((((((((of(X1,X2,X3)&city(X1,X3))&hollywood_placename(X1,X2))&placename(X1,X2))&street(X1,X3))&lonely(X1,X3))&chevy(X1,X4))&white(X1,X4))&dirty(X1,X4))&old(X1,X4))&event(X1,X5))&agent(X1,X5,X4))&present(X1,X5))&barrel(X1,X5))&down(X1,X5,X3))&in(X1,X5,X3)))))))))&((?[X1]:(actual_world(X1)&(?[X2]:(?[X3]:(?[X4]:(?[X5]:(((((((((((((((of(X1,X2,X3)&city(X1,X3))&hollywood_placename(X1,X2))&placename(X1,X2))&street(X1,X3))&lonely(X1,X3))&chevy(X1,X4))&white(X1,X4))&dirty(X1,X4))&old(X1,X4))&event(X1,X5))&agent(X1,X5,X4))&present(X1,X5))&barrel(X1,X5))&down(X1,X5,X3))&in(X1,X5,X3))))))))=>(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(((((((((((((((of(U,W,V)&city(U,V))&hollywood_placename(U,W))&placename(U,W))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&street(U,Y))&lonely(U,Y))&event(U,Z))&agent(U,Z,X))&present(U,Z))&barrel(U,Z))&down(U,Z,Y))&in(U,Z,V)))))))))))))),inference(assume_negation,[status(cth)],[co1])).
% 6.65/6.86 fof(c1,negated_conjecture,(((?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(((((((((((((((of(U,W,V)&city(U,V))&hollywood_placename(U,W))&placename(U,W))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&street(U,Y))&lonely(U,Y))&event(U,Z))&agent(U,Z,X))&present(U,Z))&barrel(U,Z))&down(U,Z,Y))&in(U,Z,V)))))))))&(![X1]:(~actual_world(X1)|(![X2]:(![X3]:(![X4]:(![X5]:(((((((((((((((~of(X1,X2,X3)|~city(X1,X3))|~hollywood_placename(X1,X2))|~placename(X1,X2))|~street(X1,X3))|~lonely(X1,X3))|~chevy(X1,X4))|~white(X1,X4))|~dirty(X1,X4))|~old(X1,X4))|~event(X1,X5))|~agent(X1,X5,X4))|~present(X1,X5))|~barrel(X1,X5))|~down(X1,X5,X3))|~in(X1,X5,X3)))))))))|((?[X1]:(actual_world(X1)&(?[X2]:(?[X3]:(?[X4]:(?[X5]:(((((((((((((((of(X1,X2,X3)&city(X1,X3))&hollywood_placename(X1,X2))&placename(X1,X2))&street(X1,X3))&lonely(X1,X3))&chevy(X1,X4))&white(X1,X4))&dirty(X1,X4))&old(X1,X4))&event(X1,X5))&agent(X1,X5,X4))&present(X1,X5))&barrel(X1,X5))&down(X1,X5,X3))&in(X1,X5,X3))))))))&(![U]:(~actual_world(U)|(![V]:(![W]:(![X]:(![Y]:(![Z]:(((((((((((((((~of(U,W,V)|~city(U,V))|~hollywood_placename(U,W))|~placename(U,W))|~chevy(U,X))|~white(U,X))|~dirty(U,X))|~old(U,X))|~street(U,Y))|~lonely(U,Y))|~event(U,Z))|~agent(U,Z,X))|~present(U,Z))|~barrel(U,Z))|~down(U,Z,Y))|~in(U,Z,V))))))))))),inference(fof_nnf,[status(thm)],[c0])).
% 6.65/6.86 fof(c2,negated_conjecture,(((?[X2]:(actual_world(X2)&(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(((((((((((((((of(X2,X4,X3)&city(X2,X3))&hollywood_placename(X2,X4))&placename(X2,X4))&chevy(X2,X5))&white(X2,X5))&dirty(X2,X5))&old(X2,X5))&street(X2,X6))&lonely(X2,X6))&event(X2,X7))&agent(X2,X7,X5))&present(X2,X7))&barrel(X2,X7))&down(X2,X7,X6))&in(X2,X7,X3)))))))))&(![X8]:(~actual_world(X8)|(![X9]:(![X10]:(![X11]:(![X12]:(((((((((((((((~of(X8,X9,X10)|~city(X8,X10))|~hollywood_placename(X8,X9))|~placename(X8,X9))|~street(X8,X10))|~lonely(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~event(X8,X12))|~agent(X8,X12,X11))|~present(X8,X12))|~barrel(X8,X12))|~down(X8,X12,X10))|~in(X8,X12,X10)))))))))|((?[X13]:(actual_world(X13)&(?[X14]:(?[X15]:(?[X16]:(?[X17]:(((((((((((((((of(X13,X14,X15)&city(X13,X15))&hollywood_placename(X13,X14))&placename(X13,X14))&street(X13,X15))&lonely(X13,X15))&chevy(X13,X16))&white(X13,X16))&dirty(X13,X16))&old(X13,X16))&event(X13,X17))&agent(X13,X17,X16))&present(X13,X17))&barrel(X13,X17))&down(X13,X17,X15))&in(X13,X17,X15))))))))&(![X18]:(~actual_world(X18)|(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(((((((((((((((~of(X18,X20,X19)|~city(X18,X19))|~hollywood_placename(X18,X20))|~placename(X18,X20))|~chevy(X18,X21))|~white(X18,X21))|~dirty(X18,X21))|~old(X18,X21))|~street(X18,X22))|~lonely(X18,X22))|~event(X18,X23))|~agent(X18,X23,X21))|~present(X18,X23))|~barrel(X18,X23))|~down(X18,X23,X22))|~in(X18,X23,X19))))))))))),inference(variable_rename,[status(thm)],[c1])).
% 6.65/6.86 fof(c4,negated_conjecture,(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(((actual_world(skolem0001)&(((((((((((((((of(skolem0001,skolem0003,skolem0002)&city(skolem0001,skolem0002))&hollywood_placename(skolem0001,skolem0003))&placename(skolem0001,skolem0003))&chevy(skolem0001,skolem0004))&white(skolem0001,skolem0004))&dirty(skolem0001,skolem0004))&old(skolem0001,skolem0004))&street(skolem0001,skolem0005))&lonely(skolem0001,skolem0005))&event(skolem0001,skolem0006))&agent(skolem0001,skolem0006,skolem0004))&present(skolem0001,skolem0006))&barrel(skolem0001,skolem0006))&down(skolem0001,skolem0006,skolem0005))&in(skolem0001,skolem0006,skolem0002)))&(~actual_world(X8)|(((((((((((((((~of(X8,X9,X10)|~city(X8,X10))|~hollywood_placename(X8,X9))|~placename(X8,X9))|~street(X8,X10))|~lonely(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~event(X8,X12))|~agent(X8,X12,X11))|~present(X8,X12))|~barrel(X8,X12))|~down(X8,X12,X10))|~in(X8,X12,X10))))|((actual_world(skolem0007)&(((((((((((((((of(skolem0007,skolem0008,skolem0009)&city(skolem0007,skolem0009))&hollywood_placename(skolem0007,skolem0008))&placename(skolem0007,skolem0008))&street(skolem0007,skolem0009))&lonely(skolem0007,skolem0009))&chevy(skolem0007,skolem0010))&white(skolem0007,skolem0010))&dirty(skolem0007,skolem0010))&old(skolem0007,skolem0010))&event(skolem0007,skolem0011))&agent(skolem0007,skolem0011,skolem0010))&present(skolem0007,skolem0011))&barrel(skolem0007,skolem0011))&down(skolem0007,skolem0011,skolem0009))&in(skolem0007,skolem0011,skolem0009)))&(~actual_world(X18)|(((((((((((((((~of(X18,X20,X19)|~city(X18,X19))|~hollywood_placename(X18,X20))|~placename(X18,X20))|~chevy(X18,X21))|~white(X18,X21))|~dirty(X18,X21))|~old(X18,X21))|~street(X18,X22))|~lonely(X18,X22))|~event(X18,X23))|~agent(X18,X23,X21))|~present(X18,X23))|~barrel(X18,X23))|~down(X18,X23,X22))|~in(X18,X23,X19)))))))))))))))),inference(shift_quantors,[status(thm)],[fof(c3,negated_conjecture,(((actual_world(skolem0001)&(((((((((((((((of(skolem0001,skolem0003,skolem0002)&city(skolem0001,skolem0002))&hollywood_placename(skolem0001,skolem0003))&placename(skolem0001,skolem0003))&chevy(skolem0001,skolem0004))&white(skolem0001,skolem0004))&dirty(skolem0001,skolem0004))&old(skolem0001,skolem0004))&street(skolem0001,skolem0005))&lonely(skolem0001,skolem0005))&event(skolem0001,skolem0006))&agent(skolem0001,skolem0006,skolem0004))&present(skolem0001,skolem0006))&barrel(skolem0001,skolem0006))&down(skolem0001,skolem0006,skolem0005))&in(skolem0001,skolem0006,skolem0002)))&(![X8]:(~actual_world(X8)|(![X9]:(![X10]:(![X11]:(![X12]:(((((((((((((((~of(X8,X9,X10)|~city(X8,X10))|~hollywood_placename(X8,X9))|~placename(X8,X9))|~street(X8,X10))|~lonely(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~event(X8,X12))|~agent(X8,X12,X11))|~present(X8,X12))|~barrel(X8,X12))|~down(X8,X12,X10))|~in(X8,X12,X10)))))))))|((actual_world(skolem0007)&(((((((((((((((of(skolem0007,skolem0008,skolem0009)&city(skolem0007,skolem0009))&hollywood_placename(skolem0007,skolem0008))&placename(skolem0007,skolem0008))&street(skolem0007,skolem0009))&lonely(skolem0007,skolem0009))&chevy(skolem0007,skolem0010))&white(skolem0007,skolem0010))&dirty(skolem0007,skolem0010))&old(skolem0007,skolem0010))&event(skolem0007,skolem0011))&agent(skolem0007,skolem0011,skolem0010))&present(skolem0007,skolem0011))&barrel(skolem0007,skolem0011))&down(skolem0007,skolem0011,skolem0009))&in(skolem0007,skolem0011,skolem0009)))&(![X18]:(~actual_world(X18)|(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(((((((((((((((~of(X18,X20,X19)|~city(X18,X19))|~hollywood_placename(X18,X20))|~placename(X18,X20))|~chevy(X18,X21))|~white(X18,X21))|~dirty(X18,X21))|~old(X18,X21))|~street(X18,X22))|~lonely(X18,X22))|~event(X18,X23))|~agent(X18,X23,X21))|~present(X18,X23))|~barrel(X18,X23))|~down(X18,X23,X22))|~in(X18,X23,X19))))))))))),inference(skolemize,[status(esa)],[c2])).])).
% 6.65/6.87 fof(c5,negated_conjecture,(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(((((actual_world(skolem0001)|actual_world(skolem0007))&((((((((((((((((actual_world(skolem0001)|of(skolem0007,skolem0008,skolem0009))&(actual_world(skolem0001)|city(skolem0007,skolem0009)))&(actual_world(skolem0001)|hollywood_placename(skolem0007,skolem0008)))&(actual_world(skolem0001)|placename(skolem0007,skolem0008)))&(actual_world(skolem0001)|street(skolem0007,skolem0009)))&(actual_world(skolem0001)|lonely(skolem0007,skolem0009)))&(actual_world(skolem0001)|chevy(skolem0007,skolem0010)))&(actual_world(skolem0001)|white(skolem0007,skolem0010)))&(actual_world(skolem0001)|dirty(skolem0007,skolem0010)))&(actual_world(skolem0001)|old(skolem0007,skolem0010)))&(actual_world(skolem0001)|event(skolem0007,skolem0011)))&(actual_world(skolem0001)|agent(skolem0007,skolem0011,skolem0010)))&(actual_world(skolem0001)|present(skolem0007,skolem0011)))&(actual_world(skolem0001)|barrel(skolem0007,skolem0011)))&(actual_world(skolem0001)|down(skolem0007,skolem0011,skolem0009)))&(actual_world(skolem0001)|in(skolem0007,skolem0011,skolem0009))))&(actual_world(skolem0001)|(~actual_world(X18)|(((((((((((((((~of(X18,X20,X19)|~city(X18,X19))|~hollywood_placename(X18,X20))|~placename(X18,X20))|~chevy(X18,X21))|~white(X18,X21))|~dirty(X18,X21))|~old(X18,X21))|~street(X18,X22))|~lonely(X18,X22))|~event(X18,X23))|~agent(X18,X23,X21))|~present(X18,X23))|~barrel(X18,X23))|~down(X18,X23,X22))|~in(X18,X23,X19)))))&((((((((((((((((((of(skolem0001,skolem0003,skolem0002)|actual_world(skolem0007))&((((((((((((((((of(skolem0001,skolem0003,skolem0002)|of(skolem0007,skolem0008,skolem0009))&(of(skolem0001,skolem0003,skolem0002)|city(skolem0007,skolem0009)))&(of(skolem0001,skolem0003,skolem0002)|hollywood_placename(skolem0007,skolem0008)))&(of(skolem0001,skolem0003,skolem0002)|placename(skolem0007,skolem0008)))&(of(skolem0001,skolem0003,skolem0002)|street(skolem0007,skolem0009)))&(of(skolem0001,skolem0003,skolem0002)|lonely(skolem0007,skolem0009)))&(of(skolem0001,skolem0003,skolem0002)|chevy(skolem0007,skolem0010)))&(of(skolem0001,skolem0003,skolem0002)|white(skolem0007,skolem0010)))&(of(skolem0001,skolem0003,skolem0002)|dirty(skolem0007,skolem0010)))&(of(skolem0001,skolem0003,skolem0002)|old(skolem0007,skolem0010)))&(of(skolem0001,skolem0003,skolem0002)|event(skolem0007,skolem0011)))&(of(skolem0001,skolem0003,skolem0002)|agent(skolem0007,skolem0011,skolem0010)))&(of(skolem0001,skolem0003,skolem0002)|present(skolem0007,skolem0011)))&(of(skolem0001,skolem0003,skolem0002)|barrel(skolem0007,skolem0011)))&(of(skolem0001,skolem0003,skolem0002)|down(skolem0007,skolem0011,skolem0009)))&(of(skolem0001,skolem0003,skolem0002)|in(skolem0007,skolem0011,skolem0009))))&(of(skolem0001,skolem0003,skolem0002)|(~actual_world(X18)|(((((((((((((((~of(X18,X20,X19)|~city(X18,X19))|~hollywood_placename(X18,X20))|~placename(X18,X20))|~chevy(X18,X21))|~white(X18,X21))|~dirty(X18,X21))|~old(X18,X21))|~street(X18,X22))|~lonely(X18,X22))|~event(X18,X23))|~agent(X18,X23,X21))|~present(X18,X23))|~barrel(X18,X23))|~down(X18,X23,X22))|~in(X18,X23,X19)))))&(((city(skolem0001,skolem0002)|actual_world(skolem0007))&((((((((((((((((city(skolem0001,skolem0002)|of(skolem0007,skolem0008,skolem0009))&(city(skolem0001,skolem0002)|city(skolem0007,skolem0009)))&(city(skolem0001,skolem0002)|hollywood_placename(skolem0007,skolem0008)))&(city(skolem0001,skolem0002)|placename(skolem0007,skolem0008)))&(city(skolem0001,skolem0002)|street(skolem0007,skolem0009)))&(city(skolem0001,skolem0002)|lonely(skolem0007,skolem0009)))&(city(skolem0001,skolem0002)|chevy(skolem0007,skolem0010)))&(city(skolem0001,skolem0002)|white(skolem0007,skolem0010)))&(city(skolem0001,skolem0002)|dirty(skolem0007,skolem0010)))&(city(skolem0001,skolem0002)|old(skolem0007,skolem0010)))&(city(skolem0001,skolem0002)|event(skolem0007,skolem0011)))&(city(skolem0001,skolem0002)|agent(skolem0007,skolem0011,skolem0010)))&(city(skolem0001,skolem0002)|present(skolem0007,skolem0011)))&(city(skolem0001,skolem0002)|barrel(skolem0007,skolem0011)))&(city(skolem0001,skolem0002)|down(skolem0007,skolem0011,skolem0009)))&(city(skolem0001,skolem0002)|in(skolem0007,skolem0011,skolem0009))))&(city(skolem0001,skolem0002)|(~actual_world(X18)|(((((((((((((((~of(X18,X20,X19)|~city(X18,X19))|~hollywood_placename(X18,X20))|~placename(X18,X20))|~chevy(X18,X21))|~white(X18,X21))|~dirty(X18,X21))|~old(X18,X21))|~street(X18,X22))|~lonely(X18,X22))|~event(X18,X23))|~agent(X18,X23,X21))|~present(X18,X23))|~barrel(X18,X23))|~down(X18,X23,X22))|~in(X18,X23,X19))))))&(((hollywood_placename(skolem0001,skolem0003)|actual_world(skolem0007))&((((((((((((((((hollywood_placename(skolem0001,skolem0003)|of(skolem0007,skolem0008,skolem0009))&(hollywood_placename(skolem0001,skolem0003)|city(skolem0007,skolem0009)))&(hollywood_placename(skolem0001,skolem0003)|hollywood_placename(skolem0007,skolem0008)))&(hollywood_placename(skolem0001,skolem0003)|placename(skolem0007,skolem0008)))&(hollywood_placename(skolem0001,skolem0003)|street(skolem0007,skolem0009)))&(hollywood_placename(skolem0001,skolem0003)|lonely(skolem0007,skolem0009)))&(hollywood_placename(skolem0001,skolem0003)|chevy(skolem0007,skolem0010)))&(hollywood_placename(skolem0001,skolem0003)|white(skolem0007,skolem0010)))&(hollywood_placename(skolem0001,skolem0003)|dirty(skolem0007,skolem0010)))&(hollywood_placename(skolem0001,skolem0003)|old(skolem0007,skolem0010)))&(hollywood_placename(skolem0001,skolem0003)|event(skolem0007,skolem0011)))&(hollywood_placename(skolem0001,skolem0003)|agent(skolem0007,skolem0011,skolem0010)))&(hollywood_placename(skolem0001,skolem0003)|present(skolem0007,skolem0011)))&(hollywood_placename(skolem0001,skolem0003)|barrel(skolem0007,skolem0011)))&(hollywood_placename(skolem0001,skolem0003)|down(skolem0007,skolem0011,skolem0009)))&(hollywood_placename(skolem0001,skolem0003)|in(skolem0007,skolem0011,skolem0009))))&(hollywood_placename(skolem0001,skolem0003)|(~actual_world(X18)|(((((((((((((((~of(X18,X20,X19)|~city(X18,X19))|~hollywood_placename(X18,X20))|~placename(X18,X20))|~chevy(X18,X21))|~white(X18,X21))|~dirty(X18,X21))|~old(X18,X21))|~street(X18,X22))|~lonely(X18,X22))|~event(X18,X23))|~agent(X18,X23,X21))|~present(X18,X23))|~barrel(X18,X23))|~down(X18,X23,X22))|~in(X18,X23,X19))))))&(((placename(skolem0001,skolem0003)|actual_world(skolem0007))&((((((((((((((((placename(skolem0001,skolem0003)|of(skolem0007,skolem0008,skolem0009))&(placename(skolem0001,skolem0003)|city(skolem0007,skolem0009)))&(placename(skolem0001,skolem0003)|hollywood_placename(skolem0007,skolem0008)))&(placename(skolem0001,skolem0003)|placename(skolem0007,skolem0008)))&(placename(skolem0001,skolem0003)|street(skolem0007,skolem0009)))&(placename(skolem0001,skolem0003)|lonely(skolem0007,skolem0009)))&(placename(skolem0001,skolem0003)|chevy(skolem0007,skolem0010)))&(placename(skolem0001,skolem0003)|white(skolem0007,skolem0010)))&(placename(skolem0001,skolem0003)|dirty(skolem0007,skolem0010)))&(placename(skolem0001,skolem0003)|old(skolem0007,skolem0010)))&(placename(skolem0001,skolem0003)|event(skolem0007,skolem0011)))&(placename(skolem0001,skolem0003)|agent(skolem0007,skolem0011,skolem0010)))&(placename(skolem0001,skolem0003)|present(skolem0007,skolem0011)))&(placename(skolem0001,skolem0003)|barrel(skolem0007,skolem0011)))&(placename(skolem0001,skolem0003)|down(skolem0007,skolem0011,skolem0009)))&(placename(skolem0001,skolem0003)|in(skolem0007,skolem0011,skolem0009))))&(placename(skolem0001,skolem0003)|(~actual_world(X18)|(((((((((((((((~of(X18,X20,X19)|~city(X18,X19))|~hollywood_placename(X18,X20))|~placename(X18,X20))|~chevy(X18,X21))|~white(X18,X21))|~dirty(X18,X21))|~old(X18,X21))|~street(X18,X22))|~lonely(X18,X22))|~event(X18,X23))|~agent(X18,X23,X21))|~present(X18,X23))|~barrel(X18,X23))|~down(X18,X23,X22))|~in(X18,X23,X19))))))&(((chevy(skolem0001,skolem0004)|actual_world(skolem0007))&((((((((((((((((chevy(skolem0001,skolem0004)|of(skolem0007,skolem0008,skolem0009))&(chevy(skolem0001,skolem0004)|city(skolem0007,skolem0009)))&(chevy(skolem0001,skolem0004)|hollywood_placename(skolem0007,skolem0008)))&(chevy(skolem0001,skolem0004)|placename(skolem0007,skolem0008)))&(chevy(skolem0001,skolem0004)|street(skolem0007,skolem0009)))&(chevy(skolem0001,skolem0004)|lonely(skolem0007,skolem0009)))&(chevy(skolem0001,skolem0004)|chevy(skolem0007,skolem0010)))&(chevy(skolem0001,skolem0004)|white(skolem0007,skolem0010)))&(chevy(skolem0001,skolem0004)|dirty(skolem0007,skolem0010)))&(chevy(skolem0001,skolem0004)|old(skolem0007,skolem0010)))&(chevy(skolem0001,skolem0004)|event(skolem0007,skolem0011)))&(chevy(skolem0001,skolem0004)|agent(skolem0007,skolem0011,skolem0010)))&(chevy(skolem0001,skolem0004)|present(skolem0007,skolem0011)))&(chevy(skolem0001,skolem0004)|barrel(skolem0007,skolem0011)))&(chevy(skolem0001,skolem0004)|down(skolem0007,skolem0011,skolem0009)))&(chevy(skolem0001,skolem0004)|in(skolem0007,skolem0011,skolem0009))))&(chevy(skolem0001,skolem0004)|(~actual_world(X18)|(((((((((((((((~of(X18,X20,X19)|~city(X18,X19))|~hollywood_placename(X18,X20))|~placename(X18,X20))|~chevy(X18,X21))|~white(X18,X21))|~dirty(X18,X21))|~old(X18,X21))|~street(X18,X22))|~lonely(X18,X22))|~event(X18,X23))|~agent(X18,X23,X21))|~present(X18,X23))|~barrel(X18,X23))|~down(X18,X23,X22))|~in(X18,X23,X19))))))&(((white(skolem0001,skolem0004)|actual_world(skolem0007))&((((((((((((((((white(skolem0001,skolem0004)|of(skolem0007,skolem0008,skolem0009))&(white(skolem0001,skolem0004)|city(skolem0007,skolem0009)))&(white(skolem0001,skolem0004)|hollywood_placename(skolem0007,skolem0008)))&(white(skolem0001,skolem0004)|placename(skolem0007,skolem0008)))&(white(skolem0001,skolem0004)|street(skolem0007,skolem0009)))&(white(skolem0001,skolem0004)|lonely(skolem0007,skolem0009)))&(white(skolem0001,skolem0004)|chevy(skolem0007,skolem0010)))&(white(skolem0001,skolem0004)|white(skolem0007,skolem0010)))&(white(skolem0001,skolem0004)|dirty(skolem0007,skolem0010)))&(white(skolem0001,skolem0004)|old(skolem0007,skolem0010)))&(white(skolem0001,skolem0004)|event(skolem0007,skolem0011)))&(white(skolem0001,skolem0004)|agent(skolem0007,skolem0011,skolem0010)))&(white(skolem0001,skolem0004)|present(skolem0007,skolem0011)))&(white(skolem0001,skolem0004)|barrel(skolem0007,skolem0011)))&(white(skolem0001,skolem0004)|down(skolem0007,skolem0011,skolem0009)))&(white(skolem0001,skolem0004)|in(skolem0007,skolem0011,skolem0009))))&(white(skolem0001,skolem0004)|(~actual_world(X18)|(((((((((((((((~of(X18,X20,X19)|~city(X18,X19))|~hollywood_placename(X18,X20))|~placename(X18,X20))|~chevy(X18,X21))|~white(X18,X21))|~dirty(X18,X21))|~old(X18,X21))|~street(X18,X22))|~lonely(X18,X22))|~event(X18,X23))|~agent(X18,X23,X21))|~present(X18,X23))|~barrel(X18,X23))|~down(X18,X23,X22))|~in(X18,X23,X19))))))&(((dirty(skolem0001,skolem0004)|actual_world(skolem0007))&((((((((((((((((dirty(skolem0001,skolem0004)|of(skolem0007,skolem0008,skolem0009))&(dirty(skolem0001,skolem0004)|city(skolem0007,skolem0009)))&(dirty(skolem0001,skolem0004)|hollywood_placename(skolem0007,skolem0008)))&(dirty(skolem0001,skolem0004)|placename(skolem0007,skolem0008)))&(dirty(skolem0001,skolem0004)|street(skolem0007,skolem0009)))&(dirty(skolem0001,skolem0004)|lonely(skolem0007,skolem0009)))&(dirty(skolem0001,skolem0004)|chevy(skolem0007,skolem0010)))&(dirty(skolem0001,skolem0004)|white(skolem0007,skolem0010)))&(dirty(skolem0001,skolem0004)|dirty(skolem0007,skolem0010)))&(dirty(skolem0001,skolem0004)|old(skolem0007,skolem0010)))&(dirty(skolem0001,skolem0004)|event(skolem0007,skolem0011)))&(dirty(skolem0001,skolem0004)|agent(skolem0007,skolem0011,skolem0010)))&(dirty(skolem0001,skolem0004)|present(skolem0007,skolem0011)))&(dirty(skolem0001,skolem0004)|barrel(skolem0007,skolem0011)))&(dirty(skolem0001,skolem0004)|down(skolem0007,skolem0011,skolem0009)))&(dirty(skolem0001,skolem0004)|in(skolem0007,skolem0011,skolem0009))))&(dirty(skolem0001,skolem0004)|(~actual_world(X18)|(((((((((((((((~of(X18,X20,X19)|~city(X18,X19))|~hollywood_placename(X18,X20))|~placename(X18,X20))|~chevy(X18,X21))|~white(X18,X21))|~dirty(X18,X21))|~old(X18,X21))|~street(X18,X22))|~lonely(X18,X22))|~event(X18,X23))|~agent(X18,X23,X21))|~present(X18,X23))|~barrel(X18,X23))|~down(X18,X23,X22))|~in(X18,X23,X19))))))&(((old(skolem0001,skolem0004)|actual_world(skolem0007))&((((((((((((((((old(skolem0001,skolem0004)|of(skolem0007,skolem0008,skolem0009))&(old(skolem0001,skolem0004)|city(skolem0007,skolem0009)))&(old(skolem0001,skolem0004)|hollywood_placename(skolem0007,skolem0008)))&(old(skolem0001,skolem0004)|placename(skolem0007,skolem0008)))&(old(skolem0001,skolem0004)|street(skolem0007,skolem0009)))&(old(skolem0001,skolem0004)|lonely(skolem0007,skolem0009)))&(old(skolem0001,skolem0004)|chevy(skolem0007,skolem0010)))&(old(skolem0001,skolem0004)|white(skolem0007,skolem0010)))&(old(skolem0001,skolem0004)|dirty(skolem0007,skolem0010)))&(old(skolem0001,skolem0004)|old(skolem0007,skolem0010)))&(old(skolem0001,skolem0004)|event(skolem0007,skolem0011)))&(old(skolem0001,skolem0004)|agent(skolem0007,skolem0011,skolem0010)))&(old(skolem0001,skolem0004)|present(skolem0007,skolem0011)))&(old(skolem0001,skolem0004)|barrel(skolem0007,skolem0011)))&(old(skolem0001,skolem0004)|down(skolem0007,skolem0011,skolem0009)))&(old(skolem0001,skolem0004)|in(skolem0007,skolem0011,skolem0009))))&(old(skolem0001,skolem0004)|(~actual_world(X18)|(((((((((((((((~of(X18,X20,X19)|~city(X18,X19))|~hollywood_placename(X18,X20))|~placename(X18,X20))|~chevy(X18,X21))|~white(X18,X21))|~dirty(X18,X21))|~old(X18,X21))|~street(X18,X22))|~lonely(X18,X22))|~event(X18,X23))|~agent(X18,X23,X21))|~present(X18,X23))|~barrel(X18,X23))|~down(X18,X23,X22))|~in(X18,X23,X19))))))&(((street(skolem0001,skolem0005)|actual_world(skolem0007))&((((((((((((((((street(skolem0001,skolem0005)|of(skolem0007,skolem0008,skolem0009))&(street(skolem0001,skolem0005)|city(skolem0007,skolem0009)))&(street(skolem0001,skolem0005)|hollywood_placename(skolem0007,skolem0008)))&(street(skolem0001,skolem0005)|placename(skolem0007,skolem0008)))&(street(skolem0001,skolem0005)|street(skolem0007,skolem0009)))&(street(skolem0001,skolem0005)|lonely(skolem0007,skolem0009)))&(street(skolem0001,skolem0005)|chevy(skolem0007,skolem0010)))&(street(skolem0001,skolem0005)|white(skolem0007,skolem0010)))&(street(skolem0001,skolem0005)|dirty(skolem0007,skolem0010)))&(street(skolem0001,skolem0005)|old(skolem0007,skolem0010)))&(street(skolem0001,skolem0005)|event(skolem0007,skolem0011)))&(street(skolem0001,skolem0005)|agent(skolem0007,skolem0011,skolem0010)))&(street(skolem0001,skolem0005)|present(skolem0007,skolem0011)))&(street(skolem0001,skolem0005)|barrel(skolem0007,skolem0011)))&(street(skolem0001,skolem0005)|down(skolem0007,skolem0011,skolem0009)))&(street(skolem0001,skolem0005)|in(skolem0007,skolem0011,skolem0009))))&(street(skolem0001,skolem0005)|(~actual_world(X18)|(((((((((((((((~of(X18,X20,X19)|~city(X18,X19))|~hollywood_placename(X18,X20))|~placename(X18,X20))|~chevy(X18,X21))|~white(X18,X21))|~dirty(X18,X21))|~old(X18,X21))|~street(X18,X22))|~lonely(X18,X22))|~event(X18,X23))|~agent(X18,X23,X21))|~present(X18,X23))|~barrel(X18,X23))|~down(X18,X23,X22))|~in(X18,X23,X19))))))&(((lonely(skolem0001,skolem0005)|actual_world(skolem0007))&((((((((((((((((lonely(skolem0001,skolem0005)|of(skolem0007,skolem0008,skolem0009))&(lonely(skolem0001,skolem0005)|city(skolem0007,skolem0009)))&(lonely(skolem0001,skolem0005)|hollywood_placename(skolem0007,skolem0008)))&(lonely(skolem0001,skolem0005)|placename(skolem0007,skolem0008)))&(lonely(skolem0001,skolem0005)|street(skolem0007,skolem0009)))&(lonely(skolem0001,skolem0005)|lonely(skolem0007,skolem0009)))&(lonely(skolem0001,skolem0005)|chevy(skolem0007,skolem0010)))&(lonely(skolem0001,skolem0005)|white(skolem0007,skolem0010)))&(lonely(skolem0001,skolem0005)|dirty(skolem0007,skolem0010)))&(lonely(skolem0001,skolem0005)|old(skolem0007,skolem0010)))&(lonely(skolem0001,skolem0005)|event(skolem0007,skolem0011)))&(lonely(skolem0001,skolem0005)|agent(skolem0007,skolem0011,skolem0010)))&(lonely(skolem0001,skolem0005)|present(skolem0007,skolem0011)))&(lonely(skolem0001,skolem0005)|barrel(skolem0007,skolem0011)))&(lonely(skolem0001,skolem0005)|down(skolem0007,skolem0011,skolem0009)))&(lonely(skolem0001,skolem0005)|in(skolem0007,skolem0011,skolem0009))))&(lonely(skolem0001,skolem0005)|(~actual_world(X18)|(((((((((((((((~of(X18,X20,X19)|~city(X18,X19))|~hollywood_placename(X18,X20))|~placename(X18,X20))|~chevy(X18,X21))|~white(X18,X21))|~dirty(X18,X21))|~old(X18,X21))|~street(X18,X22))|~lonely(X18,X22))|~event(X18,X23))|~agent(X18,X23,X21))|~present(X18,X23))|~barrel(X18,X23))|~down(X18,X23,X22))|~in(X18,X23,X19))))))&(((event(skolem0001,skolem0006)|actual_world(skolem0007))&((((((((((((((((event(skolem0001,skolem0006)|of(skolem0007,skolem0008,skolem0009))&(event(skolem0001,skolem0006)|city(skolem0007,skolem0009)))&(event(skolem0001,skolem0006)|hollywood_placename(skolem0007,skolem0008)))&(event(skolem0001,skolem0006)|placename(skolem0007,skolem0008)))&(event(skolem0001,skolem0006)|street(skolem0007,skolem0009)))&(event(skolem0001,skolem0006)|lonely(skolem0007,skolem0009)))&(event(skolem0001,skolem0006)|chevy(skolem0007,skolem0010)))&(event(skolem0001,skolem0006)|white(skolem0007,skolem0010)))&(event(skolem0001,skolem0006)|dirty(skolem0007,skolem0010)))&(event(skolem0001,skolem0006)|old(skolem0007,skolem0010)))&(event(skolem0001,skolem0006)|event(skolem0007,skolem0011)))&(event(skolem0001,skolem0006)|agent(skolem0007,skolem0011,skolem0010)))&(event(skolem0001,skolem0006)|present(skolem0007,skolem0011)))&(event(skolem0001,skolem0006)|barrel(skolem0007,skolem0011)))&(event(skolem0001,skolem0006)|down(skolem0007,skolem0011,skolem0009)))&(event(skolem0001,skolem0006)|in(skolem0007,skolem0011,skolem0009))))&(event(skolem0001,skolem0006)|(~actual_world(X18)|(((((((((((((((~of(X18,X20,X19)|~city(X18,X19))|~hollywood_placename(X18,X20))|~placename(X18,X20))|~chevy(X18,X21))|~white(X18,X21))|~dirty(X18,X21))|~old(X18,X21))|~street(X18,X22))|~lonely(X18,X22))|~event(X18,X23))|~agent(X18,X23,X21))|~present(X18,X23))|~barrel(X18,X23))|~down(X18,X23,X22))|~in(X18,X23,X19))))))&(((agent(skolem0001,skolem0006,skolem0004)|actual_world(skolem0007))&((((((((((((((((agent(skolem0001,skolem0006,skolem0004)|of(skolem0007,skolem0008,skolem0009))&(agent(skolem0001,skolem0006,skolem0004)|city(skolem0007,skolem0009)))&(agent(skolem0001,skolem0006,skolem0004)|hollywood_placename(skolem0007,skolem0008)))&(agent(skolem0001,skolem0006,skolem0004)|placename(skolem0007,skolem0008)))&(agent(skolem0001,skolem0006,skolem0004)|street(skolem0007,skolem0009)))&(agent(skolem0001,skolem0006,skolem0004)|lonely(skolem0007,skolem0009)))&(agent(skolem0001,skolem0006,skolem0004)|chevy(skolem0007,skolem0010)))&(agent(skolem0001,skolem0006,skolem0004)|white(skolem0007,skolem0010)))&(agent(skolem0001,skolem0006,skolem0004)|dirty(skolem0007,skolem0010)))&(agent(skolem0001,skolem0006,skolem0004)|old(skolem0007,skolem0010)))&(agent(skolem0001,skolem0006,skolem0004)|event(skolem0007,skolem0011)))&(agent(skolem0001,skolem0006,skolem0004)|agent(skolem0007,skolem0011,skolem0010)))&(agent(skolem0001,skolem0006,skolem0004)|present(skolem0007,skolem0011)))&(agent(skolem0001,skolem0006,skolem0004)|barrel(skolem0007,skolem0011)))&(agent(skolem0001,skolem0006,skolem0004)|down(skolem0007,skolem0011,skolem0009)))&(agent(skolem0001,skolem0006,skolem0004)|in(skolem0007,skolem0011,skolem0009))))&(agent(skolem0001,skolem0006,skolem0004)|(~actual_world(X18)|(((((((((((((((~of(X18,X20,X19)|~city(X18,X19))|~hollywood_placename(X18,X20))|~placename(X18,X20))|~chevy(X18,X21))|~white(X18,X21))|~dirty(X18,X21))|~old(X18,X21))|~street(X18,X22))|~lonely(X18,X22))|~event(X18,X23))|~agent(X18,X23,X21))|~present(X18,X23))|~barrel(X18,X23))|~down(X18,X23,X22))|~in(X18,X23,X19))))))&(((present(skolem0001,skolem0006)|actual_world(skolem0007))&((((((((((((((((present(skolem0001,skolem0006)|of(skolem0007,skolem0008,skolem0009))&(present(skolem0001,skolem0006)|city(skolem0007,skolem0009)))&(present(skolem0001,skolem0006)|hollywood_placename(skolem0007,skolem0008)))&(present(skolem0001,skolem0006)|placename(skolem0007,skolem0008)))&(present(skolem0001,skolem0006)|street(skolem0007,skolem0009)))&(present(skolem0001,skolem0006)|lonely(skolem0007,skolem0009)))&(present(skolem0001,skolem0006)|chevy(skolem0007,skolem0010)))&(present(skolem0001,skolem0006)|white(skolem0007,skolem0010)))&(present(skolem0001,skolem0006)|dirty(skolem0007,skolem0010)))&(present(skolem0001,skolem0006)|old(skolem0007,skolem0010)))&(present(skolem0001,skolem0006)|event(skolem0007,skolem0011)))&(present(skolem0001,skolem0006)|agent(skolem0007,skolem0011,skolem0010)))&(present(skolem0001,skolem0006)|present(skolem0007,skolem0011)))&(present(skolem0001,skolem0006)|barrel(skolem0007,skolem0011)))&(present(skolem0001,skolem0006)|down(skolem0007,skolem0011,skolem0009)))&(present(skolem0001,skolem0006)|in(skolem0007,skolem0011,skolem0009))))&(present(skolem0001,skolem0006)|(~actual_world(X18)|(((((((((((((((~of(X18,X20,X19)|~city(X18,X19))|~hollywood_placename(X18,X20))|~placename(X18,X20))|~chevy(X18,X21))|~white(X18,X21))|~dirty(X18,X21))|~old(X18,X21))|~street(X18,X22))|~lonely(X18,X22))|~event(X18,X23))|~agent(X18,X23,X21))|~present(X18,X23))|~barrel(X18,X23))|~down(X18,X23,X22))|~in(X18,X23,X19))))))&(((barrel(skolem0001,skolem0006)|actual_world(skolem0007))&((((((((((((((((barrel(skolem0001,skolem0006)|of(skolem0007,skolem0008,skolem0009))&(barrel(skolem0001,skolem0006)|city(skolem0007,skolem0009)))&(barrel(skolem0001,skolem0006)|hollywood_placename(skolem0007,skolem0008)))&(barrel(skolem0001,skolem0006)|placename(skolem0007,skolem0008)))&(barrel(skolem0001,skolem0006)|street(skolem0007,skolem0009)))&(barrel(skolem0001,skolem0006)|lonely(skolem0007,skolem0009)))&(barrel(skolem0001,skolem0006)|chevy(skolem0007,skolem0010)))&(barrel(skolem0001,skolem0006)|white(skolem0007,skolem0010)))&(barrel(skolem0001,skolem0006)|dirty(skolem0007,skolem0010)))&(barrel(skolem0001,skolem0006)|old(skolem0007,skolem0010)))&(barrel(skolem0001,skolem0006)|event(skolem0007,skolem0011)))&(barrel(skolem0001,skolem0006)|agent(skolem0007,skolem0011,skolem0010)))&(barrel(skolem0001,skolem0006)|present(skolem0007,skolem0011)))&(barrel(skolem0001,skolem0006)|barrel(skolem0007,skolem0011)))&(barrel(skolem0001,skolem0006)|down(skolem0007,skolem0011,skolem0009)))&(barrel(skolem0001,skolem0006)|in(skolem0007,skolem0011,skolem0009))))&(barrel(skolem0001,skolem0006)|(~actual_world(X18)|(((((((((((((((~of(X18,X20,X19)|~city(X18,X19))|~hollywood_placename(X18,X20))|~placename(X18,X20))|~chevy(X18,X21))|~white(X18,X21))|~dirty(X18,X21))|~old(X18,X21))|~street(X18,X22))|~lonely(X18,X22))|~event(X18,X23))|~agent(X18,X23,X21))|~present(X18,X23))|~barrel(X18,X23))|~down(X18,X23,X22))|~in(X18,X23,X19))))))&(((down(skolem0001,skolem0006,skolem0005)|actual_world(skolem0007))&((((((((((((((((down(skolem0001,skolem0006,skolem0005)|of(skolem0007,skolem0008,skolem0009))&(down(skolem0001,skolem0006,skolem0005)|city(skolem0007,skolem0009)))&(down(skolem0001,skolem0006,skolem0005)|hollywood_placename(skolem0007,skolem0008)))&(down(skolem0001,skolem0006,skolem0005)|placename(skolem0007,skolem0008)))&(down(skolem0001,skolem0006,skolem0005)|street(skolem0007,skolem0009)))&(down(skolem0001,skolem0006,skolem0005)|lonely(skolem0007,skolem0009)))&(down(skolem0001,skolem0006,skolem0005)|chevy(skolem0007,skolem0010)))&(down(skolem0001,skolem0006,skolem0005)|white(skolem0007,skolem0010)))&(down(skolem0001,skolem0006,skolem0005)|dirty(skolem0007,skolem0010)))&(down(skolem0001,skolem0006,skolem0005)|old(skolem0007,skolem0010)))&(down(skolem0001,skolem0006,skolem0005)|event(skolem0007,skolem0011)))&(down(skolem0001,skolem0006,skolem0005)|agent(skolem0007,skolem0011,skolem0010)))&(down(skolem0001,skolem0006,skolem0005)|present(skolem0007,skolem0011)))&(down(skolem0001,skolem0006,skolem0005)|barrel(skolem0007,skolem0011)))&(down(skolem0001,skolem0006,skolem0005)|down(skolem0007,skolem0011,skolem0009)))&(down(skolem0001,skolem0006,skolem0005)|in(skolem0007,skolem0011,skolem0009))))&(down(skolem0001,skolem0006,skolem0005)|(~actual_world(X18)|(((((((((((((((~of(X18,X20,X19)|~city(X18,X19))|~hollywood_placename(X18,X20))|~placename(X18,X20))|~chevy(X18,X21))|~white(X18,X21))|~dirty(X18,X21))|~old(X18,X21))|~street(X18,X22))|~lonely(X18,X22))|~event(X18,X23))|~agent(X18,X23,X21))|~present(X18,X23))|~barrel(X18,X23))|~down(X18,X23,X22))|~in(X18,X23,X19))))))&(((in(skolem0001,skolem0006,skolem0002)|actual_world(skolem0007))&((((((((((((((((in(skolem0001,skolem0006,skolem0002)|of(skolem0007,skolem0008,skolem0009))&(in(skolem0001,skolem0006,skolem0002)|city(skolem0007,skolem0009)))&(in(skolem0001,skolem0006,skolem0002)|hollywood_placename(skolem0007,skolem0008)))&(in(skolem0001,skolem0006,skolem0002)|placename(skolem0007,skolem0008)))&(in(skolem0001,skolem0006,skolem0002)|street(skolem0007,skolem0009)))&(in(skolem0001,skolem0006,skolem0002)|lonely(skolem0007,skolem0009)))&(in(skolem0001,skolem0006,skolem0002)|chevy(skolem0007,skolem0010)))&(in(skolem0001,skolem0006,skolem0002)|white(skolem0007,skolem0010)))&(in(skolem0001,skolem0006,skolem0002)|dirty(skolem0007,skolem0010)))&(in(skolem0001,skolem0006,skolem0002)|old(skolem0007,skolem0010)))&(in(skolem0001,skolem0006,skolem0002)|event(skolem0007,skolem0011)))&(in(skolem0001,skolem0006,skolem0002)|agent(skolem0007,skolem0011,skolem0010)))&(in(skolem0001,skolem0006,skolem0002)|present(skolem0007,skolem0011)))&(in(skolem0001,skolem0006,skolem0002)|barrel(skolem0007,skolem0011)))&(in(skolem0001,skolem0006,skolem0002)|down(skolem0007,skolem0011,skolem0009)))&(in(skolem0001,skolem0006,skolem0002)|in(skolem0007,skolem0011,skolem0009))))&(in(skolem0001,skolem0006,skolem0002)|(~actual_world(X18)|(((((((((((((((~of(X18,X20,X19)|~city(X18,X19))|~hollywood_placename(X18,X20))|~placename(X18,X20))|~chevy(X18,X21))|~white(X18,X21))|~dirty(X18,X21))|~old(X18,X21))|~street(X18,X22))|~lonely(X18,X22))|~event(X18,X23))|~agent(X18,X23,X21))|~present(X18,X23))|~barrel(X18,X23))|~down(X18,X23,X22))|~in(X18,X23,X19)))))))&((((~actual_world(X8)|(((((((((((((((~of(X8,X9,X10)|~city(X8,X10))|~hollywood_placename(X8,X9))|~placename(X8,X9))|~street(X8,X10))|~lonely(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~event(X8,X12))|~agent(X8,X12,X11))|~present(X8,X12))|~barrel(X8,X12))|~down(X8,X12,X10))|~in(X8,X12,X10)))|actual_world(skolem0007))&(((((((((((((((((~actual_world(X8)|(((((((((((((((~of(X8,X9,X10)|~city(X8,X10))|~hollywood_placename(X8,X9))|~placename(X8,X9))|~street(X8,X10))|~lonely(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~event(X8,X12))|~agent(X8,X12,X11))|~present(X8,X12))|~barrel(X8,X12))|~down(X8,X12,X10))|~in(X8,X12,X10)))|of(skolem0007,skolem0008,skolem0009))&((~actual_world(X8)|(((((((((((((((~of(X8,X9,X10)|~city(X8,X10))|~hollywood_placename(X8,X9))|~placename(X8,X9))|~street(X8,X10))|~lonely(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~event(X8,X12))|~agent(X8,X12,X11))|~present(X8,X12))|~barrel(X8,X12))|~down(X8,X12,X10))|~in(X8,X12,X10)))|city(skolem0007,skolem0009)))&((~actual_world(X8)|(((((((((((((((~of(X8,X9,X10)|~city(X8,X10))|~hollywood_placename(X8,X9))|~placename(X8,X9))|~street(X8,X10))|~lonely(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~event(X8,X12))|~agent(X8,X12,X11))|~present(X8,X12))|~barrel(X8,X12))|~down(X8,X12,X10))|~in(X8,X12,X10)))|hollywood_placename(skolem0007,skolem0008)))&((~actual_world(X8)|(((((((((((((((~of(X8,X9,X10)|~city(X8,X10))|~hollywood_placename(X8,X9))|~placename(X8,X9))|~street(X8,X10))|~lonely(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~event(X8,X12))|~agent(X8,X12,X11))|~present(X8,X12))|~barrel(X8,X12))|~down(X8,X12,X10))|~in(X8,X12,X10)))|placename(skolem0007,skolem0008)))&((~actual_world(X8)|(((((((((((((((~of(X8,X9,X10)|~city(X8,X10))|~hollywood_placename(X8,X9))|~placename(X8,X9))|~street(X8,X10))|~lonely(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~event(X8,X12))|~agent(X8,X12,X11))|~present(X8,X12))|~barrel(X8,X12))|~down(X8,X12,X10))|~in(X8,X12,X10)))|street(skolem0007,skolem0009)))&((~actual_world(X8)|(((((((((((((((~of(X8,X9,X10)|~city(X8,X10))|~hollywood_placename(X8,X9))|~placename(X8,X9))|~street(X8,X10))|~lonely(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~event(X8,X12))|~agent(X8,X12,X11))|~present(X8,X12))|~barrel(X8,X12))|~down(X8,X12,X10))|~in(X8,X12,X10)))|lonely(skolem0007,skolem0009)))&((~actual_world(X8)|(((((((((((((((~of(X8,X9,X10)|~city(X8,X10))|~hollywood_placename(X8,X9))|~placename(X8,X9))|~street(X8,X10))|~lonely(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~event(X8,X12))|~agent(X8,X12,X11))|~present(X8,X12))|~barrel(X8,X12))|~down(X8,X12,X10))|~in(X8,X12,X10)))|chevy(skolem0007,skolem0010)))&((~actual_world(X8)|(((((((((((((((~of(X8,X9,X10)|~city(X8,X10))|~hollywood_placename(X8,X9))|~placename(X8,X9))|~street(X8,X10))|~lonely(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~event(X8,X12))|~agent(X8,X12,X11))|~present(X8,X12))|~barrel(X8,X12))|~down(X8,X12,X10))|~in(X8,X12,X10)))|white(skolem0007,skolem0010)))&((~actual_world(X8)|(((((((((((((((~of(X8,X9,X10)|~city(X8,X10))|~hollywood_placename(X8,X9))|~placename(X8,X9))|~street(X8,X10))|~lonely(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~event(X8,X12))|~agent(X8,X12,X11))|~present(X8,X12))|~barrel(X8,X12))|~down(X8,X12,X10))|~in(X8,X12,X10)))|dirty(skolem0007,skolem0010)))&((~actual_world(X8)|(((((((((((((((~of(X8,X9,X10)|~city(X8,X10))|~hollywood_placename(X8,X9))|~placename(X8,X9))|~street(X8,X10))|~lonely(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~event(X8,X12))|~agent(X8,X12,X11))|~present(X8,X12))|~barrel(X8,X12))|~down(X8,X12,X10))|~in(X8,X12,X10)))|old(skolem0007,skolem0010)))&((~actual_world(X8)|(((((((((((((((~of(X8,X9,X10)|~city(X8,X10))|~hollywood_placename(X8,X9))|~placename(X8,X9))|~street(X8,X10))|~lonely(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~event(X8,X12))|~agent(X8,X12,X11))|~present(X8,X12))|~barrel(X8,X12))|~down(X8,X12,X10))|~in(X8,X12,X10)))|event(skolem0007,skolem0011)))&((~actual_world(X8)|(((((((((((((((~of(X8,X9,X10)|~city(X8,X10))|~hollywood_placename(X8,X9))|~placename(X8,X9))|~street(X8,X10))|~lonely(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~event(X8,X12))|~agent(X8,X12,X11))|~present(X8,X12))|~barrel(X8,X12))|~down(X8,X12,X10))|~in(X8,X12,X10)))|agent(skolem0007,skolem0011,skolem0010)))&((~actual_world(X8)|(((((((((((((((~of(X8,X9,X10)|~city(X8,X10))|~hollywood_placename(X8,X9))|~placename(X8,X9))|~street(X8,X10))|~lonely(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~event(X8,X12))|~agent(X8,X12,X11))|~present(X8,X12))|~barrel(X8,X12))|~down(X8,X12,X10))|~in(X8,X12,X10)))|present(skolem0007,skolem0011)))&((~actual_world(X8)|(((((((((((((((~of(X8,X9,X10)|~city(X8,X10))|~hollywood_placename(X8,X9))|~placename(X8,X9))|~street(X8,X10))|~lonely(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~event(X8,X12))|~agent(X8,X12,X11))|~present(X8,X12))|~barrel(X8,X12))|~down(X8,X12,X10))|~in(X8,X12,X10)))|barrel(skolem0007,skolem0011)))&((~actual_world(X8)|(((((((((((((((~of(X8,X9,X10)|~city(X8,X10))|~hollywood_placename(X8,X9))|~placename(X8,X9))|~street(X8,X10))|~lonely(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~event(X8,X12))|~agent(X8,X12,X11))|~present(X8,X12))|~barrel(X8,X12))|~down(X8,X12,X10))|~in(X8,X12,X10)))|down(skolem0007,skolem0011,skolem0009)))&((~actual_world(X8)|(((((((((((((((~of(X8,X9,X10)|~city(X8,X10))|~hollywood_placename(X8,X9))|~placename(X8,X9))|~street(X8,X10))|~lonely(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~event(X8,X12))|~agent(X8,X12,X11))|~present(X8,X12))|~barrel(X8,X12))|~down(X8,X12,X10))|~in(X8,X12,X10)))|in(skolem0007,skolem0011,skolem0009))))&((~actual_world(X8)|(((((((((((((((~of(X8,X9,X10)|~city(X8,X10))|~hollywood_placename(X8,X9))|~placename(X8,X9))|~street(X8,X10))|~lonely(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~event(X8,X12))|~agent(X8,X12,X11))|~present(X8,X12))|~barrel(X8,X12))|~down(X8,X12,X10))|~in(X8,X12,X10)))|(~actual_world(X18)|(((((((((((((((~of(X18,X20,X19)|~city(X18,X19))|~hollywood_placename(X18,X20))|~placename(X18,X20))|~chevy(X18,X21))|~white(X18,X21))|~dirty(X18,X21))|~old(X18,X21))|~street(X18,X22))|~lonely(X18,X22))|~event(X18,X23))|~agent(X18,X23,X21))|~present(X18,X23))|~barrel(X18,X23))|~down(X18,X23,X22))|~in(X18,X23,X19))))))))))))))))),inference(distribute,[status(thm)],[c4])).
% 6.65/6.87 cnf(c294,negated_conjecture,in(skolem0001,skolem0006,skolem0002)|actual_world(skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c296,negated_conjecture,in(skolem0001,skolem0006,skolem0002)|city(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c297,negated_conjecture,in(skolem0001,skolem0006,skolem0002)|hollywood_placename(skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c298,negated_conjecture,in(skolem0001,skolem0006,skolem0002)|placename(skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c301,negated_conjecture,in(skolem0001,skolem0006,skolem0002)|chevy(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c302,negated_conjecture,in(skolem0001,skolem0006,skolem0002)|white(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c303,negated_conjecture,in(skolem0001,skolem0006,skolem0002)|dirty(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c304,negated_conjecture,in(skolem0001,skolem0006,skolem0002)|old(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c299,negated_conjecture,in(skolem0001,skolem0006,skolem0002)|street(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c300,negated_conjecture,in(skolem0001,skolem0006,skolem0002)|lonely(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c305,negated_conjecture,in(skolem0001,skolem0006,skolem0002)|event(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c307,negated_conjecture,in(skolem0001,skolem0006,skolem0002)|present(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c308,negated_conjecture,in(skolem0001,skolem0006,skolem0002)|barrel(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c295,negated_conjecture,in(skolem0001,skolem0006,skolem0002)|of(skolem0007,skolem0008,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c306,negated_conjecture,in(skolem0001,skolem0006,skolem0002)|agent(skolem0007,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c309,negated_conjecture,in(skolem0001,skolem0006,skolem0002)|down(skolem0007,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c310,negated_conjecture,in(skolem0001,skolem0006,skolem0002)|in(skolem0007,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c311,negated_conjecture,in(skolem0001,skolem0006,skolem0002)|~actual_world(X152)|~of(X152,X151,X153)|~city(X152,X153)|~hollywood_placename(X152,X151)|~placename(X152,X151)|~chevy(X152,X150)|~white(X152,X150)|~dirty(X152,X150)|~old(X152,X150)|~street(X152,X154)|~lonely(X152,X154)|~event(X152,X155)|~agent(X152,X155,X150)|~present(X152,X155)|~barrel(X152,X155)|~down(X152,X155,X154)|~in(X152,X155,X153),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c1107,plain,in(skolem0001,skolem0006,skolem0002)|~actual_world(skolem0007)|~of(skolem0007,X2109,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X2109)|~placename(skolem0007,X2109)|~chevy(skolem0007,X2107)|~white(skolem0007,X2107)|~dirty(skolem0007,X2107)|~old(skolem0007,X2107)|~street(skolem0007,X2108)|~lonely(skolem0007,X2108)|~event(skolem0007,skolem0011)|~agent(skolem0007,skolem0011,X2107)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011)|~down(skolem0007,skolem0011,X2108),inference(resolution,[status(thm)],[c311, c310])).
% 6.65/6.87 cnf(c4036,plain,in(skolem0001,skolem0006,skolem0002)|~actual_world(skolem0007)|~of(skolem0007,X2111,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X2111)|~placename(skolem0007,X2111)|~chevy(skolem0007,X2110)|~white(skolem0007,X2110)|~dirty(skolem0007,X2110)|~old(skolem0007,X2110)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~agent(skolem0007,skolem0011,X2110)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c1107, c309])).
% 6.65/6.87 cnf(c4037,plain,in(skolem0001,skolem0006,skolem0002)|~actual_world(skolem0007)|~of(skolem0007,X2115,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X2115)|~placename(skolem0007,X2115)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c4036, c306])).
% 6.65/6.87 cnf(c4038,plain,in(skolem0001,skolem0006,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c4037, c295])).
% 6.65/6.87 cnf(c4039,plain,in(skolem0001,skolem0006,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011),inference(resolution,[status(thm)],[c4038, c308])).
% 6.65/6.87 cnf(c4040,plain,in(skolem0001,skolem0006,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011),inference(resolution,[status(thm)],[c4039, c307])).
% 6.65/6.87 cnf(c4041,plain,in(skolem0001,skolem0006,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009),inference(resolution,[status(thm)],[c4040, c305])).
% 6.65/6.87 cnf(c4042,plain,in(skolem0001,skolem0006,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009),inference(resolution,[status(thm)],[c4041, c300])).
% 6.65/6.87 cnf(c4043,plain,in(skolem0001,skolem0006,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010),inference(resolution,[status(thm)],[c4042, c299])).
% 6.65/6.87 cnf(c4044,plain,in(skolem0001,skolem0006,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010),inference(resolution,[status(thm)],[c4043, c304])).
% 6.65/6.87 cnf(c4045,plain,in(skolem0001,skolem0006,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010),inference(resolution,[status(thm)],[c4044, c303])).
% 6.65/6.87 cnf(c4046,plain,in(skolem0001,skolem0006,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010),inference(resolution,[status(thm)],[c4045, c302])).
% 6.65/6.87 cnf(c4047,plain,in(skolem0001,skolem0006,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008),inference(resolution,[status(thm)],[c4046, c301])).
% 6.65/6.87 cnf(c4048,plain,in(skolem0001,skolem0006,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008),inference(resolution,[status(thm)],[c4047, c298])).
% 6.65/6.87 cnf(c4049,plain,in(skolem0001,skolem0006,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009),inference(resolution,[status(thm)],[c4048, c297])).
% 6.65/6.87 cnf(c4050,plain,in(skolem0001,skolem0006,skolem0002)|~actual_world(skolem0007),inference(resolution,[status(thm)],[c4049, c296])).
% 6.65/6.87 cnf(c4051,plain,in(skolem0001,skolem0006,skolem0002),inference(resolution,[status(thm)],[c4050, c294])).
% 6.65/6.87 cnf(c329,negated_conjecture,~actual_world(X214)|~of(X214,X213,X211)|~city(X214,X211)|~hollywood_placename(X214,X213)|~placename(X214,X213)|~street(X214,X211)|~lonely(X214,X211)|~chevy(X214,X221)|~white(X214,X221)|~dirty(X214,X221)|~old(X214,X221)|~event(X214,X216)|~agent(X214,X216,X221)|~present(X214,X216)|~barrel(X214,X216)|~down(X214,X216,X211)|~in(X214,X216,X211)|~actual_world(X217)|~of(X217,X215,X218)|~city(X217,X218)|~hollywood_placename(X217,X215)|~placename(X217,X215)|~chevy(X217,X212)|~white(X217,X212)|~dirty(X217,X212)|~old(X217,X212)|~street(X217,X219)|~lonely(X217,X219)|~event(X217,X220)|~agent(X217,X220,X212)|~present(X217,X220)|~barrel(X217,X220)|~down(X217,X220,X219)|~in(X217,X220,X218),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c1486,plain,~actual_world(X3771)|~of(X3771,X3778,X3773)|~city(X3771,X3773)|~hollywood_placename(X3771,X3778)|~placename(X3771,X3778)|~street(X3771,X3773)|~lonely(X3771,X3773)|~chevy(X3771,X3772)|~white(X3771,X3772)|~dirty(X3771,X3772)|~old(X3771,X3772)|~event(X3771,X3775)|~agent(X3771,X3775,X3772)|~present(X3771,X3775)|~barrel(X3771,X3775)|~down(X3771,X3775,X3773)|~in(X3771,X3775,X3773)|~of(X3771,X3776,X3773)|~hollywood_placename(X3771,X3776)|~placename(X3771,X3776)|~chevy(X3771,X3774)|~white(X3771,X3774)|~dirty(X3771,X3774)|~old(X3771,X3774)|~street(X3771,X3777)|~lonely(X3771,X3777)|~agent(X3771,X3775,X3774)|~down(X3771,X3775,X3777),inference(factor,[status(thm)],[c329])).
% 6.65/6.87 cnf(c4070,plain,~actual_world(X3785)|~of(X3785,X3784,X3779)|~city(X3785,X3779)|~hollywood_placename(X3785,X3784)|~placename(X3785,X3784)|~street(X3785,X3779)|~lonely(X3785,X3779)|~chevy(X3785,X3781)|~white(X3785,X3781)|~dirty(X3785,X3781)|~old(X3785,X3781)|~event(X3785,X3782)|~agent(X3785,X3782,X3781)|~present(X3785,X3782)|~barrel(X3785,X3782)|~down(X3785,X3782,X3779)|~in(X3785,X3782,X3779)|~of(X3785,X3783,X3779)|~hollywood_placename(X3785,X3783)|~placename(X3785,X3783)|~chevy(X3785,X3780)|~white(X3785,X3780)|~dirty(X3785,X3780)|~old(X3785,X3780)|~agent(X3785,X3782,X3780),inference(factor,[status(thm)],[c1486])).
% 6.65/6.87 cnf(c4072,plain,~actual_world(X3786)|~of(X3786,X3788,X3791)|~city(X3786,X3791)|~hollywood_placename(X3786,X3788)|~placename(X3786,X3788)|~street(X3786,X3791)|~lonely(X3786,X3791)|~chevy(X3786,X3787)|~white(X3786,X3787)|~dirty(X3786,X3787)|~old(X3786,X3787)|~event(X3786,X3789)|~agent(X3786,X3789,X3787)|~present(X3786,X3789)|~barrel(X3786,X3789)|~down(X3786,X3789,X3791)|~in(X3786,X3789,X3791)|~of(X3786,X3790,X3791)|~hollywood_placename(X3786,X3790)|~placename(X3786,X3790),inference(factor,[status(thm)],[c4070])).
% 6.65/6.87 cnf(c4074,plain,~actual_world(X3802)|~of(X3802,X3804,X3803)|~city(X3802,X3803)|~hollywood_placename(X3802,X3804)|~placename(X3802,X3804)|~street(X3802,X3803)|~lonely(X3802,X3803)|~chevy(X3802,X3801)|~white(X3802,X3801)|~dirty(X3802,X3801)|~old(X3802,X3801)|~event(X3802,X3800)|~agent(X3802,X3800,X3801)|~present(X3802,X3800)|~barrel(X3802,X3800)|~down(X3802,X3800,X3803)|~in(X3802,X3800,X3803),inference(factor,[status(thm)],[c4072])).
% 6.65/6.87 cnf(c4076,plain,~actual_world(skolem0001)|~of(skolem0001,X3806,skolem0002)|~city(skolem0001,skolem0002)|~hollywood_placename(skolem0001,X3806)|~placename(skolem0001,X3806)|~street(skolem0001,skolem0002)|~lonely(skolem0001,skolem0002)|~chevy(skolem0001,X3805)|~white(skolem0001,X3805)|~dirty(skolem0001,X3805)|~old(skolem0001,X3805)|~event(skolem0001,skolem0006)|~agent(skolem0001,skolem0006,X3805)|~present(skolem0001,skolem0006)|~barrel(skolem0001,skolem0006)|~down(skolem0001,skolem0006,skolem0002),inference(resolution,[status(thm)],[c4074, c4051])).
% 6.65/6.87 cnf(c276,negated_conjecture,down(skolem0001,skolem0006,skolem0005)|actual_world(skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c278,negated_conjecture,down(skolem0001,skolem0006,skolem0005)|city(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c279,negated_conjecture,down(skolem0001,skolem0006,skolem0005)|hollywood_placename(skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c280,negated_conjecture,down(skolem0001,skolem0006,skolem0005)|placename(skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c283,negated_conjecture,down(skolem0001,skolem0006,skolem0005)|chevy(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c284,negated_conjecture,down(skolem0001,skolem0006,skolem0005)|white(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c285,negated_conjecture,down(skolem0001,skolem0006,skolem0005)|dirty(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c286,negated_conjecture,down(skolem0001,skolem0006,skolem0005)|old(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c281,negated_conjecture,down(skolem0001,skolem0006,skolem0005)|street(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c282,negated_conjecture,down(skolem0001,skolem0006,skolem0005)|lonely(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c287,negated_conjecture,down(skolem0001,skolem0006,skolem0005)|event(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c289,negated_conjecture,down(skolem0001,skolem0006,skolem0005)|present(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c290,negated_conjecture,down(skolem0001,skolem0006,skolem0005)|barrel(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c277,negated_conjecture,down(skolem0001,skolem0006,skolem0005)|of(skolem0007,skolem0008,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c288,negated_conjecture,down(skolem0001,skolem0006,skolem0005)|agent(skolem0007,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c291,negated_conjecture,down(skolem0001,skolem0006,skolem0005)|down(skolem0007,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c292,negated_conjecture,down(skolem0001,skolem0006,skolem0005)|in(skolem0007,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c293,negated_conjecture,down(skolem0001,skolem0006,skolem0005)|~actual_world(X121)|~of(X121,X120,X122)|~city(X121,X122)|~hollywood_placename(X121,X120)|~placename(X121,X120)|~chevy(X121,X119)|~white(X121,X119)|~dirty(X121,X119)|~old(X121,X119)|~street(X121,X123)|~lonely(X121,X123)|~event(X121,X124)|~agent(X121,X124,X119)|~present(X121,X124)|~barrel(X121,X124)|~down(X121,X124,X123)|~in(X121,X124,X122),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c875,plain,down(skolem0001,skolem0006,skolem0005)|~actual_world(skolem0007)|~of(skolem0007,X2085,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X2085)|~placename(skolem0007,X2085)|~chevy(skolem0007,X2083)|~white(skolem0007,X2083)|~dirty(skolem0007,X2083)|~old(skolem0007,X2083)|~street(skolem0007,X2084)|~lonely(skolem0007,X2084)|~event(skolem0007,skolem0011)|~agent(skolem0007,skolem0011,X2083)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011)|~down(skolem0007,skolem0011,X2084),inference(resolution,[status(thm)],[c293, c292])).
% 6.65/6.87 cnf(c4005,plain,down(skolem0001,skolem0006,skolem0005)|~actual_world(skolem0007)|~of(skolem0007,X2086,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X2086)|~placename(skolem0007,X2086)|~chevy(skolem0007,X2087)|~white(skolem0007,X2087)|~dirty(skolem0007,X2087)|~old(skolem0007,X2087)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~agent(skolem0007,skolem0011,X2087)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c875, c291])).
% 6.65/6.87 cnf(c4006,plain,down(skolem0001,skolem0006,skolem0005)|~actual_world(skolem0007)|~of(skolem0007,X2088,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X2088)|~placename(skolem0007,X2088)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c4005, c288])).
% 6.65/6.87 cnf(c4009,plain,down(skolem0001,skolem0006,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c4006, c277])).
% 6.65/6.87 cnf(c4010,plain,down(skolem0001,skolem0006,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011),inference(resolution,[status(thm)],[c4009, c290])).
% 6.65/6.87 cnf(c4013,plain,down(skolem0001,skolem0006,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011),inference(resolution,[status(thm)],[c4010, c289])).
% 6.65/6.87 cnf(c4015,plain,down(skolem0001,skolem0006,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009),inference(resolution,[status(thm)],[c4013, c287])).
% 6.65/6.87 cnf(c4016,plain,down(skolem0001,skolem0006,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009),inference(resolution,[status(thm)],[c4015, c282])).
% 6.65/6.87 cnf(c4018,plain,down(skolem0001,skolem0006,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010),inference(resolution,[status(thm)],[c4016, c281])).
% 6.65/6.87 cnf(c4021,plain,down(skolem0001,skolem0006,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010),inference(resolution,[status(thm)],[c4018, c286])).
% 6.65/6.87 cnf(c4022,plain,down(skolem0001,skolem0006,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010),inference(resolution,[status(thm)],[c4021, c285])).
% 6.65/6.87 cnf(c4024,plain,down(skolem0001,skolem0006,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010),inference(resolution,[status(thm)],[c4022, c284])).
% 6.65/6.87 cnf(c4027,plain,down(skolem0001,skolem0006,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008),inference(resolution,[status(thm)],[c4024, c283])).
% 6.65/6.87 cnf(c4028,plain,down(skolem0001,skolem0006,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008),inference(resolution,[status(thm)],[c4027, c280])).
% 6.65/6.87 cnf(c4030,plain,down(skolem0001,skolem0006,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009),inference(resolution,[status(thm)],[c4028, c279])).
% 6.65/6.87 cnf(c4032,plain,down(skolem0001,skolem0006,skolem0005)|~actual_world(skolem0007),inference(resolution,[status(thm)],[c4030, c278])).
% 6.65/6.87 cnf(c4035,plain,down(skolem0001,skolem0006,skolem0005),inference(resolution,[status(thm)],[c4032, c276])).
% 6.65/6.87 cnf(c222,negated_conjecture,agent(skolem0001,skolem0006,skolem0004)|actual_world(skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c224,negated_conjecture,agent(skolem0001,skolem0006,skolem0004)|city(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c225,negated_conjecture,agent(skolem0001,skolem0006,skolem0004)|hollywood_placename(skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c226,negated_conjecture,agent(skolem0001,skolem0006,skolem0004)|placename(skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c229,negated_conjecture,agent(skolem0001,skolem0006,skolem0004)|chevy(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c230,negated_conjecture,agent(skolem0001,skolem0006,skolem0004)|white(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c231,negated_conjecture,agent(skolem0001,skolem0006,skolem0004)|dirty(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c232,negated_conjecture,agent(skolem0001,skolem0006,skolem0004)|old(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c227,negated_conjecture,agent(skolem0001,skolem0006,skolem0004)|street(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c228,negated_conjecture,agent(skolem0001,skolem0006,skolem0004)|lonely(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c233,negated_conjecture,agent(skolem0001,skolem0006,skolem0004)|event(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c235,negated_conjecture,agent(skolem0001,skolem0006,skolem0004)|present(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c236,negated_conjecture,agent(skolem0001,skolem0006,skolem0004)|barrel(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c223,negated_conjecture,agent(skolem0001,skolem0006,skolem0004)|of(skolem0007,skolem0008,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c234,negated_conjecture,agent(skolem0001,skolem0006,skolem0004)|agent(skolem0007,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c237,negated_conjecture,agent(skolem0001,skolem0006,skolem0004)|down(skolem0007,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c238,negated_conjecture,agent(skolem0001,skolem0006,skolem0004)|in(skolem0007,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c239,negated_conjecture,agent(skolem0001,skolem0006,skolem0004)|~actual_world(X98)|~of(X98,X97,X99)|~city(X98,X99)|~hollywood_placename(X98,X97)|~placename(X98,X97)|~chevy(X98,X96)|~white(X98,X96)|~dirty(X98,X96)|~old(X98,X96)|~street(X98,X100)|~lonely(X98,X100)|~event(X98,X101)|~agent(X98,X101,X96)|~present(X98,X101)|~barrel(X98,X101)|~down(X98,X101,X100)|~in(X98,X101,X99),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c526,plain,agent(skolem0001,skolem0006,skolem0004)|~actual_world(skolem0007)|~of(skolem0007,X826,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X826)|~placename(skolem0007,X826)|~chevy(skolem0007,X827)|~white(skolem0007,X827)|~dirty(skolem0007,X827)|~old(skolem0007,X827)|~street(skolem0007,X825)|~lonely(skolem0007,X825)|~event(skolem0007,skolem0011)|~agent(skolem0007,skolem0011,X827)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011)|~down(skolem0007,skolem0011,X825),inference(resolution,[status(thm)],[c239, c238])).
% 6.65/6.87 cnf(c2844,plain,agent(skolem0001,skolem0006,skolem0004)|~actual_world(skolem0007)|~of(skolem0007,X1537,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X1537)|~placename(skolem0007,X1537)|~chevy(skolem0007,X1536)|~white(skolem0007,X1536)|~dirty(skolem0007,X1536)|~old(skolem0007,X1536)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~agent(skolem0007,skolem0011,X1536)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c526, c237])).
% 6.65/6.87 cnf(c3959,plain,agent(skolem0001,skolem0006,skolem0004)|~actual_world(skolem0007)|~of(skolem0007,X1538,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X1538)|~placename(skolem0007,X1538)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c2844, c234])).
% 6.65/6.87 cnf(c3962,plain,agent(skolem0001,skolem0006,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c3959, c223])).
% 6.65/6.87 cnf(c3965,plain,agent(skolem0001,skolem0006,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011),inference(resolution,[status(thm)],[c3962, c236])).
% 6.65/6.87 cnf(c3969,plain,agent(skolem0001,skolem0006,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011),inference(resolution,[status(thm)],[c3965, c235])).
% 6.65/6.87 cnf(c3973,plain,agent(skolem0001,skolem0006,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009),inference(resolution,[status(thm)],[c3969, c233])).
% 6.65/6.87 cnf(c3975,plain,agent(skolem0001,skolem0006,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009),inference(resolution,[status(thm)],[c3973, c228])).
% 6.65/6.87 cnf(c3979,plain,agent(skolem0001,skolem0006,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3975, c227])).
% 6.65/6.87 cnf(c3980,plain,agent(skolem0001,skolem0006,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3979, c232])).
% 6.65/6.87 cnf(c3985,plain,agent(skolem0001,skolem0006,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3980, c231])).
% 6.65/6.87 cnf(c3986,plain,agent(skolem0001,skolem0006,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3985, c230])).
% 6.65/6.87 cnf(c3989,plain,agent(skolem0001,skolem0006,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008),inference(resolution,[status(thm)],[c3986, c229])).
% 6.65/6.87 cnf(c3993,plain,agent(skolem0001,skolem0006,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008),inference(resolution,[status(thm)],[c3989, c226])).
% 6.65/6.87 cnf(c3995,plain,agent(skolem0001,skolem0006,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009),inference(resolution,[status(thm)],[c3993, c225])).
% 6.65/6.87 cnf(c3999,plain,agent(skolem0001,skolem0006,skolem0004)|~actual_world(skolem0007),inference(resolution,[status(thm)],[c3995, c224])).
% 6.65/6.87 cnf(c4003,plain,agent(skolem0001,skolem0006,skolem0004),inference(resolution,[status(thm)],[c3999, c222])).
% 6.65/6.87 cnf(c24,negated_conjecture,of(skolem0001,skolem0003,skolem0002)|actual_world(skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c26,negated_conjecture,of(skolem0001,skolem0003,skolem0002)|city(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c27,negated_conjecture,of(skolem0001,skolem0003,skolem0002)|hollywood_placename(skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c28,negated_conjecture,of(skolem0001,skolem0003,skolem0002)|placename(skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c31,negated_conjecture,of(skolem0001,skolem0003,skolem0002)|chevy(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c32,negated_conjecture,of(skolem0001,skolem0003,skolem0002)|white(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c33,negated_conjecture,of(skolem0001,skolem0003,skolem0002)|dirty(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c34,negated_conjecture,of(skolem0001,skolem0003,skolem0002)|old(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c29,negated_conjecture,of(skolem0001,skolem0003,skolem0002)|street(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c30,negated_conjecture,of(skolem0001,skolem0003,skolem0002)|lonely(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c35,negated_conjecture,of(skolem0001,skolem0003,skolem0002)|event(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c37,negated_conjecture,of(skolem0001,skolem0003,skolem0002)|present(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c38,negated_conjecture,of(skolem0001,skolem0003,skolem0002)|barrel(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c25,negated_conjecture,of(skolem0001,skolem0003,skolem0002)|of(skolem0007,skolem0008,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c36,negated_conjecture,of(skolem0001,skolem0003,skolem0002)|agent(skolem0007,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c39,negated_conjecture,of(skolem0001,skolem0003,skolem0002)|down(skolem0007,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c40,negated_conjecture,of(skolem0001,skolem0003,skolem0002)|in(skolem0007,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.87 cnf(c41,negated_conjecture,of(skolem0001,skolem0003,skolem0002)|~actual_world(X32)|~of(X32,X31,X33)|~city(X32,X33)|~hollywood_placename(X32,X31)|~placename(X32,X31)|~chevy(X32,X30)|~white(X32,X30)|~dirty(X32,X30)|~old(X32,X30)|~street(X32,X34)|~lonely(X32,X34)|~event(X32,X35)|~agent(X32,X35,X30)|~present(X32,X35)|~barrel(X32,X35)|~down(X32,X35,X34)|~in(X32,X35,X33),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c332,plain,of(skolem0001,skolem0003,skolem0002)|~actual_world(skolem0007)|~of(skolem0007,X232,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X232)|~placename(skolem0007,X232)|~chevy(skolem0007,X233)|~white(skolem0007,X233)|~dirty(skolem0007,X233)|~old(skolem0007,X233)|~street(skolem0007,X231)|~lonely(skolem0007,X231)|~event(skolem0007,skolem0011)|~agent(skolem0007,skolem0011,X233)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011)|~down(skolem0007,skolem0011,X231),inference(resolution,[status(thm)],[c41, c40])).
% 6.65/6.88 cnf(c1699,plain,of(skolem0001,skolem0003,skolem0002)|~actual_world(skolem0007)|~of(skolem0007,X1501,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X1501)|~placename(skolem0007,X1501)|~chevy(skolem0007,X1500)|~white(skolem0007,X1500)|~dirty(skolem0007,X1500)|~old(skolem0007,X1500)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~agent(skolem0007,skolem0011,X1500)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c332, c39])).
% 6.65/6.88 cnf(c3899,plain,of(skolem0001,skolem0003,skolem0002)|~actual_world(skolem0007)|~of(skolem0007,X1502,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X1502)|~placename(skolem0007,X1502)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c1699, c36])).
% 6.65/6.88 cnf(c3904,plain,of(skolem0001,skolem0003,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c3899, c25])).
% 6.65/6.88 cnf(c3910,plain,of(skolem0001,skolem0003,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011),inference(resolution,[status(thm)],[c3904, c38])).
% 6.65/6.88 cnf(c3912,plain,of(skolem0001,skolem0003,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011),inference(resolution,[status(thm)],[c3910, c37])).
% 6.65/6.88 cnf(c3917,plain,of(skolem0001,skolem0003,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009),inference(resolution,[status(thm)],[c3912, c35])).
% 6.65/6.88 cnf(c3920,plain,of(skolem0001,skolem0003,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009),inference(resolution,[status(thm)],[c3917, c30])).
% 6.65/6.88 cnf(c3926,plain,of(skolem0001,skolem0003,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3920, c29])).
% 6.65/6.88 cnf(c3929,plain,of(skolem0001,skolem0003,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3926, c34])).
% 6.65/6.88 cnf(c3933,plain,of(skolem0001,skolem0003,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3929, c33])).
% 6.65/6.88 cnf(c3937,plain,of(skolem0001,skolem0003,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3933, c32])).
% 6.65/6.88 cnf(c3939,plain,of(skolem0001,skolem0003,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008),inference(resolution,[status(thm)],[c3937, c31])).
% 6.65/6.88 cnf(c3943,plain,of(skolem0001,skolem0003,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008),inference(resolution,[status(thm)],[c3939, c28])).
% 6.65/6.88 cnf(c3949,plain,of(skolem0001,skolem0003,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009),inference(resolution,[status(thm)],[c3943, c27])).
% 6.65/6.88 cnf(c3953,plain,of(skolem0001,skolem0003,skolem0002)|~actual_world(skolem0007),inference(resolution,[status(thm)],[c3949, c26])).
% 6.65/6.88 cnf(c3955,plain,of(skolem0001,skolem0003,skolem0002),inference(resolution,[status(thm)],[c3953, c24])).
% 6.65/6.88 cnf(c258,negated_conjecture,barrel(skolem0001,skolem0006)|actual_world(skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c260,negated_conjecture,barrel(skolem0001,skolem0006)|city(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c261,negated_conjecture,barrel(skolem0001,skolem0006)|hollywood_placename(skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c262,negated_conjecture,barrel(skolem0001,skolem0006)|placename(skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c265,negated_conjecture,barrel(skolem0001,skolem0006)|chevy(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c266,negated_conjecture,barrel(skolem0001,skolem0006)|white(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c267,negated_conjecture,barrel(skolem0001,skolem0006)|dirty(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c268,negated_conjecture,barrel(skolem0001,skolem0006)|old(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c263,negated_conjecture,barrel(skolem0001,skolem0006)|street(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c264,negated_conjecture,barrel(skolem0001,skolem0006)|lonely(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c269,negated_conjecture,barrel(skolem0001,skolem0006)|event(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c271,negated_conjecture,barrel(skolem0001,skolem0006)|present(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c272,negated_conjecture,barrel(skolem0001,skolem0006)|barrel(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c259,negated_conjecture,barrel(skolem0001,skolem0006)|of(skolem0007,skolem0008,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c270,negated_conjecture,barrel(skolem0001,skolem0006)|agent(skolem0007,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c273,negated_conjecture,barrel(skolem0001,skolem0006)|down(skolem0007,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c274,negated_conjecture,barrel(skolem0001,skolem0006)|in(skolem0007,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c275,negated_conjecture,barrel(skolem0001,skolem0006)|~actual_world(X110)|~of(X110,X109,X111)|~city(X110,X111)|~hollywood_placename(X110,X109)|~placename(X110,X109)|~chevy(X110,X108)|~white(X110,X108)|~dirty(X110,X108)|~old(X110,X108)|~street(X110,X112)|~lonely(X110,X112)|~event(X110,X113)|~agent(X110,X113,X108)|~present(X110,X113)|~barrel(X110,X113)|~down(X110,X113,X112)|~in(X110,X113,X111),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c712,plain,barrel(skolem0001,skolem0006)|~actual_world(skolem0007)|~of(skolem0007,X1406,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X1406)|~placename(skolem0007,X1406)|~chevy(skolem0007,X1405)|~white(skolem0007,X1405)|~dirty(skolem0007,X1405)|~old(skolem0007,X1405)|~street(skolem0007,X1404)|~lonely(skolem0007,X1404)|~event(skolem0007,skolem0011)|~agent(skolem0007,skolem0011,X1405)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011)|~down(skolem0007,skolem0011,X1404),inference(resolution,[status(thm)],[c275, c274])).
% 6.65/6.88 cnf(c3823,plain,barrel(skolem0001,skolem0006)|~actual_world(skolem0007)|~of(skolem0007,X1435,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X1435)|~placename(skolem0007,X1435)|~chevy(skolem0007,X1434)|~white(skolem0007,X1434)|~dirty(skolem0007,X1434)|~old(skolem0007,X1434)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~agent(skolem0007,skolem0011,X1434)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c712, c273])).
% 6.65/6.88 cnf(c3824,plain,barrel(skolem0001,skolem0006)|~actual_world(skolem0007)|~of(skolem0007,X1436,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X1436)|~placename(skolem0007,X1436)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c3823, c270])).
% 6.65/6.88 cnf(c3831,plain,barrel(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c3824, c259])).
% 6.65/6.88 cnf(c3834,plain,barrel(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011),inference(resolution,[status(thm)],[c3831, c272])).
% 6.65/6.88 cnf(c3841,plain,barrel(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011),inference(resolution,[status(thm)],[c3834, c271])).
% 6.65/6.88 cnf(c3845,plain,barrel(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009),inference(resolution,[status(thm)],[c3841, c269])).
% 6.65/6.88 cnf(c3852,plain,barrel(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009),inference(resolution,[status(thm)],[c3845, c264])).
% 6.65/6.88 cnf(c3854,plain,barrel(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3852, c263])).
% 6.65/6.88 cnf(c3861,plain,barrel(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3854, c268])).
% 6.65/6.88 cnf(c3864,plain,barrel(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3861, c267])).
% 6.65/6.88 cnf(c3870,plain,barrel(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3864, c266])).
% 6.65/6.88 cnf(c3877,plain,barrel(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008),inference(resolution,[status(thm)],[c3870, c265])).
% 6.65/6.88 cnf(c3880,plain,barrel(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008),inference(resolution,[status(thm)],[c3877, c262])).
% 6.65/6.88 cnf(c3884,plain,barrel(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009),inference(resolution,[status(thm)],[c3880, c261])).
% 6.65/6.88 cnf(c3889,plain,barrel(skolem0001,skolem0006)|~actual_world(skolem0007),inference(resolution,[status(thm)],[c3884, c260])).
% 6.65/6.88 cnf(c3896,plain,barrel(skolem0001,skolem0006),inference(resolution,[status(thm)],[c3889, c258])).
% 6.65/6.88 cnf(c240,negated_conjecture,present(skolem0001,skolem0006)|actual_world(skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c242,negated_conjecture,present(skolem0001,skolem0006)|city(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c243,negated_conjecture,present(skolem0001,skolem0006)|hollywood_placename(skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c244,negated_conjecture,present(skolem0001,skolem0006)|placename(skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c247,negated_conjecture,present(skolem0001,skolem0006)|chevy(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c248,negated_conjecture,present(skolem0001,skolem0006)|white(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c249,negated_conjecture,present(skolem0001,skolem0006)|dirty(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c250,negated_conjecture,present(skolem0001,skolem0006)|old(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c245,negated_conjecture,present(skolem0001,skolem0006)|street(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c246,negated_conjecture,present(skolem0001,skolem0006)|lonely(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c251,negated_conjecture,present(skolem0001,skolem0006)|event(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c253,negated_conjecture,present(skolem0001,skolem0006)|present(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c254,negated_conjecture,present(skolem0001,skolem0006)|barrel(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c241,negated_conjecture,present(skolem0001,skolem0006)|of(skolem0007,skolem0008,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c252,negated_conjecture,present(skolem0001,skolem0006)|agent(skolem0007,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c255,negated_conjecture,present(skolem0001,skolem0006)|down(skolem0007,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c256,negated_conjecture,present(skolem0001,skolem0006)|in(skolem0007,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c257,negated_conjecture,present(skolem0001,skolem0006)|~actual_world(X104)|~of(X104,X103,X105)|~city(X104,X105)|~hollywood_placename(X104,X103)|~placename(X104,X103)|~chevy(X104,X102)|~white(X104,X102)|~dirty(X104,X102)|~old(X104,X102)|~street(X104,X106)|~lonely(X104,X106)|~event(X104,X107)|~agent(X104,X107,X102)|~present(X104,X107)|~barrel(X104,X107)|~down(X104,X107,X106)|~in(X104,X107,X105),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c621,plain,present(skolem0001,skolem0006)|~actual_world(skolem0007)|~of(skolem0007,X1121,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X1121)|~placename(skolem0007,X1121)|~chevy(skolem0007,X1119)|~white(skolem0007,X1119)|~dirty(skolem0007,X1119)|~old(skolem0007,X1119)|~street(skolem0007,X1120)|~lonely(skolem0007,X1120)|~event(skolem0007,skolem0011)|~agent(skolem0007,skolem0011,X1119)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011)|~down(skolem0007,skolem0011,X1120),inference(resolution,[status(thm)],[c257, c256])).
% 6.65/6.88 cnf(c3368,plain,present(skolem0001,skolem0006)|~actual_world(skolem0007)|~of(skolem0007,X1372,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X1372)|~placename(skolem0007,X1372)|~chevy(skolem0007,X1371)|~white(skolem0007,X1371)|~dirty(skolem0007,X1371)|~old(skolem0007,X1371)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~agent(skolem0007,skolem0011,X1371)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c621, c255])).
% 6.65/6.88 cnf(c3730,plain,present(skolem0001,skolem0006)|~actual_world(skolem0007)|~of(skolem0007,X1376,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X1376)|~placename(skolem0007,X1376)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c3368, c252])).
% 6.65/6.88 cnf(c3738,plain,present(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c3730, c241])).
% 6.65/6.88 cnf(c3741,plain,present(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011),inference(resolution,[status(thm)],[c3738, c254])).
% 6.65/6.88 cnf(c3750,plain,present(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011),inference(resolution,[status(thm)],[c3741, c253])).
% 6.65/6.88 cnf(c3754,plain,present(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009),inference(resolution,[status(thm)],[c3750, c251])).
% 6.65/6.88 cnf(c3761,plain,present(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009),inference(resolution,[status(thm)],[c3754, c246])).
% 6.65/6.88 cnf(c3768,plain,present(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3761, c245])).
% 6.65/6.88 cnf(c3771,plain,present(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3768, c250])).
% 6.65/6.88 cnf(c3782,plain,present(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3771, c249])).
% 6.65/6.88 cnf(c3783,plain,present(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3782, c248])).
% 6.65/6.88 cnf(c3791,plain,present(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008),inference(resolution,[status(thm)],[c3783, c247])).
% 6.65/6.88 cnf(c3795,plain,present(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008),inference(resolution,[status(thm)],[c3791, c244])).
% 6.65/6.88 cnf(c3805,plain,present(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009),inference(resolution,[status(thm)],[c3795, c243])).
% 6.65/6.88 cnf(c3810,plain,present(skolem0001,skolem0006)|~actual_world(skolem0007),inference(resolution,[status(thm)],[c3805, c242])).
% 6.65/6.88 cnf(c3816,plain,present(skolem0001,skolem0006),inference(resolution,[status(thm)],[c3810, c240])).
% 6.65/6.88 cnf(c204,negated_conjecture,event(skolem0001,skolem0006)|actual_world(skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c206,negated_conjecture,event(skolem0001,skolem0006)|city(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c207,negated_conjecture,event(skolem0001,skolem0006)|hollywood_placename(skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c208,negated_conjecture,event(skolem0001,skolem0006)|placename(skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c211,negated_conjecture,event(skolem0001,skolem0006)|chevy(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c212,negated_conjecture,event(skolem0001,skolem0006)|white(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c213,negated_conjecture,event(skolem0001,skolem0006)|dirty(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c214,negated_conjecture,event(skolem0001,skolem0006)|old(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c209,negated_conjecture,event(skolem0001,skolem0006)|street(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c210,negated_conjecture,event(skolem0001,skolem0006)|lonely(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c215,negated_conjecture,event(skolem0001,skolem0006)|event(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c217,negated_conjecture,event(skolem0001,skolem0006)|present(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c218,negated_conjecture,event(skolem0001,skolem0006)|barrel(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c205,negated_conjecture,event(skolem0001,skolem0006)|of(skolem0007,skolem0008,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c216,negated_conjecture,event(skolem0001,skolem0006)|agent(skolem0007,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c219,negated_conjecture,event(skolem0001,skolem0006)|down(skolem0007,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c220,negated_conjecture,event(skolem0001,skolem0006)|in(skolem0007,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c221,negated_conjecture,event(skolem0001,skolem0006)|~actual_world(X92)|~of(X92,X91,X93)|~city(X92,X93)|~hollywood_placename(X92,X91)|~placename(X92,X91)|~chevy(X92,X90)|~white(X92,X90)|~dirty(X92,X90)|~old(X92,X90)|~street(X92,X94)|~lonely(X92,X94)|~event(X92,X95)|~agent(X92,X95,X90)|~present(X92,X95)|~barrel(X92,X95)|~down(X92,X95,X94)|~in(X92,X95,X93),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c478,plain,event(skolem0001,skolem0006)|~actual_world(skolem0007)|~of(skolem0007,X678,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X678)|~placename(skolem0007,X678)|~chevy(skolem0007,X679)|~white(skolem0007,X679)|~dirty(skolem0007,X679)|~old(skolem0007,X679)|~street(skolem0007,X680)|~lonely(skolem0007,X680)|~event(skolem0007,skolem0011)|~agent(skolem0007,skolem0011,X679)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011)|~down(skolem0007,skolem0011,X680),inference(resolution,[status(thm)],[c221, c220])).
% 6.65/6.88 cnf(c2644,plain,event(skolem0001,skolem0006)|~actual_world(skolem0007)|~of(skolem0007,X1302,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X1302)|~placename(skolem0007,X1302)|~chevy(skolem0007,X1303)|~white(skolem0007,X1303)|~dirty(skolem0007,X1303)|~old(skolem0007,X1303)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~agent(skolem0007,skolem0011,X1303)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c478, c219])).
% 6.65/6.88 cnf(c3629,plain,event(skolem0001,skolem0006)|~actual_world(skolem0007)|~of(skolem0007,X1304,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X1304)|~placename(skolem0007,X1304)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c2644, c216])).
% 6.65/6.88 cnf(c3633,plain,event(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c3629, c205])).
% 6.65/6.88 cnf(c3640,plain,event(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011),inference(resolution,[status(thm)],[c3633, c218])).
% 6.65/6.88 cnf(c3649,plain,event(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011),inference(resolution,[status(thm)],[c3640, c217])).
% 6.65/6.88 cnf(c3655,plain,event(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009),inference(resolution,[status(thm)],[c3649, c215])).
% 6.65/6.88 cnf(c3665,plain,event(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009),inference(resolution,[status(thm)],[c3655, c210])).
% 6.65/6.88 cnf(c3667,plain,event(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3665, c209])).
% 6.65/6.88 cnf(c3677,plain,event(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3667, c214])).
% 6.65/6.88 cnf(c3682,plain,event(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3677, c213])).
% 6.65/6.88 cnf(c3690,plain,event(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3682, c212])).
% 6.65/6.88 cnf(c3700,plain,event(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008),inference(resolution,[status(thm)],[c3690, c211])).
% 6.65/6.88 cnf(c3704,plain,event(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008),inference(resolution,[status(thm)],[c3700, c208])).
% 6.65/6.88 cnf(c3710,plain,event(skolem0001,skolem0006)|~actual_world(skolem0007)|~city(skolem0007,skolem0009),inference(resolution,[status(thm)],[c3704, c207])).
% 6.65/6.88 cnf(c3717,plain,event(skolem0001,skolem0006)|~actual_world(skolem0007),inference(resolution,[status(thm)],[c3710, c206])).
% 6.65/6.88 cnf(c3723,plain,event(skolem0001,skolem0006),inference(resolution,[status(thm)],[c3717, c204])).
% 6.65/6.88 cnf(c186,negated_conjecture,lonely(skolem0001,skolem0005)|actual_world(skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c188,negated_conjecture,lonely(skolem0001,skolem0005)|city(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c189,negated_conjecture,lonely(skolem0001,skolem0005)|hollywood_placename(skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c190,negated_conjecture,lonely(skolem0001,skolem0005)|placename(skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c193,negated_conjecture,lonely(skolem0001,skolem0005)|chevy(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c194,negated_conjecture,lonely(skolem0001,skolem0005)|white(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c195,negated_conjecture,lonely(skolem0001,skolem0005)|dirty(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c196,negated_conjecture,lonely(skolem0001,skolem0005)|old(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c191,negated_conjecture,lonely(skolem0001,skolem0005)|street(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c192,negated_conjecture,lonely(skolem0001,skolem0005)|lonely(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c197,negated_conjecture,lonely(skolem0001,skolem0005)|event(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c199,negated_conjecture,lonely(skolem0001,skolem0005)|present(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c200,negated_conjecture,lonely(skolem0001,skolem0005)|barrel(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c187,negated_conjecture,lonely(skolem0001,skolem0005)|of(skolem0007,skolem0008,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c198,negated_conjecture,lonely(skolem0001,skolem0005)|agent(skolem0007,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c201,negated_conjecture,lonely(skolem0001,skolem0005)|down(skolem0007,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c202,negated_conjecture,lonely(skolem0001,skolem0005)|in(skolem0007,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c203,negated_conjecture,lonely(skolem0001,skolem0005)|~actual_world(X86)|~of(X86,X85,X87)|~city(X86,X87)|~hollywood_placename(X86,X85)|~placename(X86,X85)|~chevy(X86,X84)|~white(X86,X84)|~dirty(X86,X84)|~old(X86,X84)|~street(X86,X88)|~lonely(X86,X88)|~event(X86,X89)|~agent(X86,X89,X84)|~present(X86,X89)|~barrel(X86,X89)|~down(X86,X89,X88)|~in(X86,X89,X87),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c469,plain,lonely(skolem0001,skolem0005)|~actual_world(skolem0007)|~of(skolem0007,X652,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X652)|~placename(skolem0007,X652)|~chevy(skolem0007,X651)|~white(skolem0007,X651)|~dirty(skolem0007,X651)|~old(skolem0007,X651)|~street(skolem0007,X653)|~lonely(skolem0007,X653)|~event(skolem0007,skolem0011)|~agent(skolem0007,skolem0011,X651)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011)|~down(skolem0007,skolem0011,X653),inference(resolution,[status(thm)],[c203, c202])).
% 6.65/6.88 cnf(c2634,plain,lonely(skolem0001,skolem0005)|~actual_world(skolem0007)|~of(skolem0007,X1234,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X1234)|~placename(skolem0007,X1234)|~chevy(skolem0007,X1233)|~white(skolem0007,X1233)|~dirty(skolem0007,X1233)|~old(skolem0007,X1233)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~agent(skolem0007,skolem0011,X1233)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c469, c201])).
% 6.65/6.88 cnf(c3505,plain,lonely(skolem0001,skolem0005)|~actual_world(skolem0007)|~of(skolem0007,X1235,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X1235)|~placename(skolem0007,X1235)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c2634, c198])).
% 6.65/6.88 cnf(c3514,plain,lonely(skolem0001,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c3505, c187])).
% 6.65/6.88 cnf(c3525,plain,lonely(skolem0001,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011),inference(resolution,[status(thm)],[c3514, c200])).
% 6.65/6.88 cnf(c3535,plain,lonely(skolem0001,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011),inference(resolution,[status(thm)],[c3525, c199])).
% 6.65/6.88 cnf(c3541,plain,lonely(skolem0001,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009),inference(resolution,[status(thm)],[c3535, c197])).
% 6.65/6.88 cnf(c3548,plain,lonely(skolem0001,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009),inference(resolution,[status(thm)],[c3541, c192])).
% 6.65/6.88 cnf(c3552,plain,lonely(skolem0001,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3548, c191])).
% 6.65/6.88 cnf(c3563,plain,lonely(skolem0001,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3552, c196])).
% 6.65/6.88 cnf(c3571,plain,lonely(skolem0001,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3563, c195])).
% 6.65/6.88 cnf(c3580,plain,lonely(skolem0001,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3571, c194])).
% 6.65/6.88 cnf(c3588,plain,lonely(skolem0001,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008),inference(resolution,[status(thm)],[c3580, c193])).
% 6.65/6.88 cnf(c3596,plain,lonely(skolem0001,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008),inference(resolution,[status(thm)],[c3588, c190])).
% 6.65/6.88 cnf(c3607,plain,lonely(skolem0001,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009),inference(resolution,[status(thm)],[c3596, c189])).
% 6.65/6.88 cnf(c3615,plain,lonely(skolem0001,skolem0005)|~actual_world(skolem0007),inference(resolution,[status(thm)],[c3607, c188])).
% 6.65/6.88 cnf(c3623,plain,lonely(skolem0001,skolem0005),inference(resolution,[status(thm)],[c3615, c186])).
% 6.65/6.88 cnf(c168,negated_conjecture,street(skolem0001,skolem0005)|actual_world(skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c170,negated_conjecture,street(skolem0001,skolem0005)|city(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c171,negated_conjecture,street(skolem0001,skolem0005)|hollywood_placename(skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c172,negated_conjecture,street(skolem0001,skolem0005)|placename(skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c175,negated_conjecture,street(skolem0001,skolem0005)|chevy(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.65/6.88 cnf(c176,negated_conjecture,street(skolem0001,skolem0005)|white(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.88 cnf(c177,negated_conjecture,street(skolem0001,skolem0005)|dirty(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.88 cnf(c178,negated_conjecture,street(skolem0001,skolem0005)|old(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.88 cnf(c173,negated_conjecture,street(skolem0001,skolem0005)|street(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.88 cnf(c174,negated_conjecture,street(skolem0001,skolem0005)|lonely(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.88 cnf(c179,negated_conjecture,street(skolem0001,skolem0005)|event(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.88 cnf(c181,negated_conjecture,street(skolem0001,skolem0005)|present(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.88 cnf(c182,negated_conjecture,street(skolem0001,skolem0005)|barrel(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.88 cnf(c169,negated_conjecture,street(skolem0001,skolem0005)|of(skolem0007,skolem0008,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.88 cnf(c180,negated_conjecture,street(skolem0001,skolem0005)|agent(skolem0007,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.88 cnf(c183,negated_conjecture,street(skolem0001,skolem0005)|down(skolem0007,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.88 cnf(c184,negated_conjecture,street(skolem0001,skolem0005)|in(skolem0007,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.88 cnf(c185,negated_conjecture,street(skolem0001,skolem0005)|~actual_world(X80)|~of(X80,X79,X81)|~city(X80,X81)|~hollywood_placename(X80,X79)|~placename(X80,X79)|~chevy(X80,X78)|~white(X80,X78)|~dirty(X80,X78)|~old(X80,X78)|~street(X80,X82)|~lonely(X80,X82)|~event(X80,X83)|~agent(X80,X83,X78)|~present(X80,X83)|~barrel(X80,X83)|~down(X80,X83,X82)|~in(X80,X83,X81),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.88 cnf(c441,plain,street(skolem0001,skolem0005)|~actual_world(skolem0007)|~of(skolem0007,X565,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X565)|~placename(skolem0007,X565)|~chevy(skolem0007,X566)|~white(skolem0007,X566)|~dirty(skolem0007,X566)|~old(skolem0007,X566)|~street(skolem0007,X564)|~lonely(skolem0007,X564)|~event(skolem0007,skolem0011)|~agent(skolem0007,skolem0011,X566)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011)|~down(skolem0007,skolem0011,X564),inference(resolution,[status(thm)],[c185, c184])).
% 6.73/6.88 cnf(c2391,plain,street(skolem0001,skolem0005)|~actual_world(skolem0007)|~of(skolem0007,X1153,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X1153)|~placename(skolem0007,X1153)|~chevy(skolem0007,X1152)|~white(skolem0007,X1152)|~dirty(skolem0007,X1152)|~old(skolem0007,X1152)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~agent(skolem0007,skolem0011,X1152)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c441, c183])).
% 6.73/6.88 cnf(c3376,plain,street(skolem0001,skolem0005)|~actual_world(skolem0007)|~of(skolem0007,X1157,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X1157)|~placename(skolem0007,X1157)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c2391, c180])).
% 6.73/6.88 cnf(c3385,plain,street(skolem0001,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c3376, c169])).
% 6.73/6.88 cnf(c3390,plain,street(skolem0001,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011),inference(resolution,[status(thm)],[c3385, c182])).
% 6.73/6.88 cnf(c3398,plain,street(skolem0001,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011),inference(resolution,[status(thm)],[c3390, c181])).
% 6.73/6.88 cnf(c3405,plain,street(skolem0001,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009),inference(resolution,[status(thm)],[c3398, c179])).
% 6.73/6.88 cnf(c3415,plain,street(skolem0001,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009),inference(resolution,[status(thm)],[c3405, c174])).
% 6.73/6.88 cnf(c3427,plain,street(skolem0001,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3415, c173])).
% 6.73/6.88 cnf(c3434,plain,street(skolem0001,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3427, c178])).
% 6.73/6.88 cnf(c3446,plain,street(skolem0001,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3434, c177])).
% 6.73/6.88 cnf(c3455,plain,street(skolem0001,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3446, c176])).
% 6.73/6.88 cnf(c3467,plain,street(skolem0001,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008),inference(resolution,[status(thm)],[c3455, c175])).
% 6.73/6.88 cnf(c3473,plain,street(skolem0001,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008),inference(resolution,[status(thm)],[c3467, c172])).
% 6.73/6.88 cnf(c3477,plain,street(skolem0001,skolem0005)|~actual_world(skolem0007)|~city(skolem0007,skolem0009),inference(resolution,[status(thm)],[c3473, c171])).
% 6.73/6.88 cnf(c3494,plain,street(skolem0001,skolem0005)|~actual_world(skolem0007),inference(resolution,[status(thm)],[c3477, c170])).
% 6.73/6.88 cnf(c3499,plain,street(skolem0001,skolem0005),inference(resolution,[status(thm)],[c3494, c168])).
% 6.73/6.88 cnf(c150,negated_conjecture,old(skolem0001,skolem0004)|actual_world(skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.88 cnf(c152,negated_conjecture,old(skolem0001,skolem0004)|city(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.88 cnf(c153,negated_conjecture,old(skolem0001,skolem0004)|hollywood_placename(skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.88 cnf(c154,negated_conjecture,old(skolem0001,skolem0004)|placename(skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c157,negated_conjecture,old(skolem0001,skolem0004)|chevy(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c158,negated_conjecture,old(skolem0001,skolem0004)|white(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c159,negated_conjecture,old(skolem0001,skolem0004)|dirty(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c160,negated_conjecture,old(skolem0001,skolem0004)|old(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c155,negated_conjecture,old(skolem0001,skolem0004)|street(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c156,negated_conjecture,old(skolem0001,skolem0004)|lonely(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c161,negated_conjecture,old(skolem0001,skolem0004)|event(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c163,negated_conjecture,old(skolem0001,skolem0004)|present(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c164,negated_conjecture,old(skolem0001,skolem0004)|barrel(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c151,negated_conjecture,old(skolem0001,skolem0004)|of(skolem0007,skolem0008,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c162,negated_conjecture,old(skolem0001,skolem0004)|agent(skolem0007,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c165,negated_conjecture,old(skolem0001,skolem0004)|down(skolem0007,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c166,negated_conjecture,old(skolem0001,skolem0004)|in(skolem0007,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c167,negated_conjecture,old(skolem0001,skolem0004)|~actual_world(X74)|~of(X74,X73,X75)|~city(X74,X75)|~hollywood_placename(X74,X73)|~placename(X74,X73)|~chevy(X74,X72)|~white(X74,X72)|~dirty(X74,X72)|~old(X74,X72)|~street(X74,X76)|~lonely(X74,X76)|~event(X74,X77)|~agent(X74,X77,X72)|~present(X74,X77)|~barrel(X74,X77)|~down(X74,X77,X76)|~in(X74,X77,X75),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c419,plain,old(skolem0001,skolem0004)|~actual_world(skolem0007)|~of(skolem0007,X495,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X495)|~placename(skolem0007,X495)|~chevy(skolem0007,X497)|~white(skolem0007,X497)|~dirty(skolem0007,X497)|~old(skolem0007,X497)|~street(skolem0007,X496)|~lonely(skolem0007,X496)|~event(skolem0007,skolem0011)|~agent(skolem0007,skolem0011,X497)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011)|~down(skolem0007,skolem0011,X496),inference(resolution,[status(thm)],[c167, c166])).
% 6.73/6.89 cnf(c2150,plain,old(skolem0001,skolem0004)|~actual_world(skolem0007)|~of(skolem0007,X1066,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X1066)|~placename(skolem0007,X1066)|~chevy(skolem0007,X1065)|~white(skolem0007,X1065)|~dirty(skolem0007,X1065)|~old(skolem0007,X1065)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~agent(skolem0007,skolem0011,X1065)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c419, c165])).
% 6.73/6.89 cnf(c3207,plain,old(skolem0001,skolem0004)|~actual_world(skolem0007)|~of(skolem0007,X1067,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X1067)|~placename(skolem0007,X1067)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c2150, c162])).
% 6.73/6.89 cnf(c3218,plain,old(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c3207, c151])).
% 6.73/6.89 cnf(c3230,plain,old(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011),inference(resolution,[status(thm)],[c3218, c164])).
% 6.73/6.89 cnf(c3234,plain,old(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011),inference(resolution,[status(thm)],[c3230, c163])).
% 6.73/6.89 cnf(c3243,plain,old(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009),inference(resolution,[status(thm)],[c3234, c161])).
% 6.73/6.89 cnf(c3259,plain,old(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009),inference(resolution,[status(thm)],[c3243, c156])).
% 6.73/6.89 cnf(c3268,plain,old(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3259, c155])).
% 6.73/6.89 cnf(c3274,plain,old(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3268, c160])).
% 6.73/6.89 cnf(c3289,plain,old(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3274, c159])).
% 6.73/6.89 cnf(c3296,plain,old(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3289, c158])).
% 6.73/6.89 cnf(c3305,plain,old(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008),inference(resolution,[status(thm)],[c3296, c157])).
% 6.73/6.89 cnf(c3314,plain,old(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008),inference(resolution,[status(thm)],[c3305, c154])).
% 6.73/6.89 cnf(c3329,plain,old(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009),inference(resolution,[status(thm)],[c3314, c153])).
% 6.73/6.89 cnf(c3338,plain,old(skolem0001,skolem0004)|~actual_world(skolem0007),inference(resolution,[status(thm)],[c3329, c152])).
% 6.73/6.89 cnf(c3347,plain,old(skolem0001,skolem0004),inference(resolution,[status(thm)],[c3338, c150])).
% 6.73/6.89 cnf(c132,negated_conjecture,dirty(skolem0001,skolem0004)|actual_world(skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c134,negated_conjecture,dirty(skolem0001,skolem0004)|city(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c135,negated_conjecture,dirty(skolem0001,skolem0004)|hollywood_placename(skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c136,negated_conjecture,dirty(skolem0001,skolem0004)|placename(skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c139,negated_conjecture,dirty(skolem0001,skolem0004)|chevy(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c140,negated_conjecture,dirty(skolem0001,skolem0004)|white(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c141,negated_conjecture,dirty(skolem0001,skolem0004)|dirty(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c142,negated_conjecture,dirty(skolem0001,skolem0004)|old(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c137,negated_conjecture,dirty(skolem0001,skolem0004)|street(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c138,negated_conjecture,dirty(skolem0001,skolem0004)|lonely(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c143,negated_conjecture,dirty(skolem0001,skolem0004)|event(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c145,negated_conjecture,dirty(skolem0001,skolem0004)|present(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c146,negated_conjecture,dirty(skolem0001,skolem0004)|barrel(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c133,negated_conjecture,dirty(skolem0001,skolem0004)|of(skolem0007,skolem0008,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c144,negated_conjecture,dirty(skolem0001,skolem0004)|agent(skolem0007,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c147,negated_conjecture,dirty(skolem0001,skolem0004)|down(skolem0007,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c148,negated_conjecture,dirty(skolem0001,skolem0004)|in(skolem0007,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c149,negated_conjecture,dirty(skolem0001,skolem0004)|~actual_world(X68)|~of(X68,X67,X69)|~city(X68,X69)|~hollywood_placename(X68,X67)|~placename(X68,X67)|~chevy(X68,X66)|~white(X68,X66)|~dirty(X68,X66)|~old(X68,X66)|~street(X68,X70)|~lonely(X68,X70)|~event(X68,X71)|~agent(X68,X71,X66)|~present(X68,X71)|~barrel(X68,X71)|~down(X68,X71,X70)|~in(X68,X71,X69),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c396,plain,dirty(skolem0001,skolem0004)|~actual_world(skolem0007)|~of(skolem0007,X426,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X426)|~placename(skolem0007,X426)|~chevy(skolem0007,X427)|~white(skolem0007,X427)|~dirty(skolem0007,X427)|~old(skolem0007,X427)|~street(skolem0007,X428)|~lonely(skolem0007,X428)|~event(skolem0007,skolem0011)|~agent(skolem0007,skolem0011,X427)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011)|~down(skolem0007,skolem0011,X428),inference(resolution,[status(thm)],[c149, c148])).
% 6.73/6.89 cnf(c2139,plain,dirty(skolem0001,skolem0004)|~actual_world(skolem0007)|~of(skolem0007,X972,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X972)|~placename(skolem0007,X972)|~chevy(skolem0007,X973)|~white(skolem0007,X973)|~dirty(skolem0007,X973)|~old(skolem0007,X973)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~agent(skolem0007,skolem0011,X973)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c396, c147])).
% 6.73/6.89 cnf(c3036,plain,dirty(skolem0001,skolem0004)|~actual_world(skolem0007)|~of(skolem0007,X974,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X974)|~placename(skolem0007,X974)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c2139, c144])).
% 6.73/6.89 cnf(c3049,plain,dirty(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c3036, c133])).
% 6.73/6.89 cnf(c3061,plain,dirty(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011),inference(resolution,[status(thm)],[c3049, c146])).
% 6.73/6.89 cnf(c3071,plain,dirty(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011),inference(resolution,[status(thm)],[c3061, c145])).
% 6.73/6.89 cnf(c3084,plain,dirty(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009),inference(resolution,[status(thm)],[c3071, c143])).
% 6.73/6.89 cnf(c3099,plain,dirty(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009),inference(resolution,[status(thm)],[c3084, c138])).
% 6.73/6.89 cnf(c3106,plain,dirty(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3099, c137])).
% 6.73/6.89 cnf(c3121,plain,dirty(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3106, c142])).
% 6.73/6.89 cnf(c3127,plain,dirty(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3121, c141])).
% 6.73/6.89 cnf(c3139,plain,dirty(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010),inference(resolution,[status(thm)],[c3127, c140])).
% 6.73/6.89 cnf(c3156,plain,dirty(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008),inference(resolution,[status(thm)],[c3139, c139])).
% 6.73/6.89 cnf(c3163,plain,dirty(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008),inference(resolution,[status(thm)],[c3156, c136])).
% 6.73/6.89 cnf(c3178,plain,dirty(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009),inference(resolution,[status(thm)],[c3163, c135])).
% 6.73/6.89 cnf(c3188,plain,dirty(skolem0001,skolem0004)|~actual_world(skolem0007),inference(resolution,[status(thm)],[c3178, c134])).
% 6.73/6.89 cnf(c3192,plain,dirty(skolem0001,skolem0004),inference(resolution,[status(thm)],[c3188, c132])).
% 6.73/6.89 cnf(c114,negated_conjecture,white(skolem0001,skolem0004)|actual_world(skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c116,negated_conjecture,white(skolem0001,skolem0004)|city(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c117,negated_conjecture,white(skolem0001,skolem0004)|hollywood_placename(skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c118,negated_conjecture,white(skolem0001,skolem0004)|placename(skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c121,negated_conjecture,white(skolem0001,skolem0004)|chevy(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c122,negated_conjecture,white(skolem0001,skolem0004)|white(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c123,negated_conjecture,white(skolem0001,skolem0004)|dirty(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c124,negated_conjecture,white(skolem0001,skolem0004)|old(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c119,negated_conjecture,white(skolem0001,skolem0004)|street(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c120,negated_conjecture,white(skolem0001,skolem0004)|lonely(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c125,negated_conjecture,white(skolem0001,skolem0004)|event(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c127,negated_conjecture,white(skolem0001,skolem0004)|present(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c128,negated_conjecture,white(skolem0001,skolem0004)|barrel(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c115,negated_conjecture,white(skolem0001,skolem0004)|of(skolem0007,skolem0008,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c126,negated_conjecture,white(skolem0001,skolem0004)|agent(skolem0007,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c129,negated_conjecture,white(skolem0001,skolem0004)|down(skolem0007,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c130,negated_conjecture,white(skolem0001,skolem0004)|in(skolem0007,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c131,negated_conjecture,white(skolem0001,skolem0004)|~actual_world(X62)|~of(X62,X61,X63)|~city(X62,X63)|~hollywood_placename(X62,X61)|~placename(X62,X61)|~chevy(X62,X60)|~white(X62,X60)|~dirty(X62,X60)|~old(X62,X60)|~street(X62,X64)|~lonely(X62,X64)|~event(X62,X65)|~agent(X62,X65,X60)|~present(X62,X65)|~barrel(X62,X65)|~down(X62,X65,X64)|~in(X62,X65,X63),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c378,plain,white(skolem0001,skolem0004)|~actual_world(skolem0007)|~of(skolem0007,X370,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X370)|~placename(skolem0007,X370)|~chevy(skolem0007,X371)|~white(skolem0007,X371)|~dirty(skolem0007,X371)|~old(skolem0007,X371)|~street(skolem0007,X369)|~lonely(skolem0007,X369)|~event(skolem0007,skolem0011)|~agent(skolem0007,skolem0011,X371)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011)|~down(skolem0007,skolem0011,X369),inference(resolution,[status(thm)],[c131, c130])).
% 6.73/6.89 cnf(c1887,plain,white(skolem0001,skolem0004)|~actual_world(skolem0007)|~of(skolem0007,X868,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X868)|~placename(skolem0007,X868)|~chevy(skolem0007,X867)|~white(skolem0007,X867)|~dirty(skolem0007,X867)|~old(skolem0007,X867)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~agent(skolem0007,skolem0011,X867)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c378, c129])).
% 6.73/6.89 cnf(c2867,plain,white(skolem0001,skolem0004)|~actual_world(skolem0007)|~of(skolem0007,X869,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X869)|~placename(skolem0007,X869)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c1887, c126])).
% 6.73/6.89 cnf(c2870,plain,white(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c2867, c115])).
% 6.73/6.89 cnf(c2886,plain,white(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011),inference(resolution,[status(thm)],[c2870, c128])).
% 6.73/6.89 cnf(c2903,plain,white(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011),inference(resolution,[status(thm)],[c2886, c127])).
% 6.73/6.89 cnf(c2913,plain,white(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009),inference(resolution,[status(thm)],[c2903, c125])).
% 6.73/6.89 cnf(c2919,plain,white(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009),inference(resolution,[status(thm)],[c2913, c120])).
% 6.73/6.89 cnf(c2932,plain,white(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010),inference(resolution,[status(thm)],[c2919, c119])).
% 6.73/6.89 cnf(c2943,plain,white(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010),inference(resolution,[status(thm)],[c2932, c124])).
% 6.73/6.89 cnf(c2957,plain,white(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010),inference(resolution,[status(thm)],[c2943, c123])).
% 6.73/6.89 cnf(c2973,plain,white(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010),inference(resolution,[status(thm)],[c2957, c122])).
% 6.73/6.89 cnf(c2986,plain,white(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008),inference(resolution,[status(thm)],[c2973, c121])).
% 6.73/6.89 cnf(c2997,plain,white(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008),inference(resolution,[status(thm)],[c2986, c118])).
% 6.73/6.89 cnf(c3008,plain,white(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009),inference(resolution,[status(thm)],[c2997, c117])).
% 6.73/6.89 cnf(c3016,plain,white(skolem0001,skolem0004)|~actual_world(skolem0007),inference(resolution,[status(thm)],[c3008, c116])).
% 6.73/6.89 cnf(c3026,plain,white(skolem0001,skolem0004),inference(resolution,[status(thm)],[c3016, c114])).
% 6.73/6.89 cnf(c96,negated_conjecture,chevy(skolem0001,skolem0004)|actual_world(skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c98,negated_conjecture,chevy(skolem0001,skolem0004)|city(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c99,negated_conjecture,chevy(skolem0001,skolem0004)|hollywood_placename(skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c100,negated_conjecture,chevy(skolem0001,skolem0004)|placename(skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c103,negated_conjecture,chevy(skolem0001,skolem0004)|chevy(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c104,negated_conjecture,chevy(skolem0001,skolem0004)|white(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c105,negated_conjecture,chevy(skolem0001,skolem0004)|dirty(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c106,negated_conjecture,chevy(skolem0001,skolem0004)|old(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c101,negated_conjecture,chevy(skolem0001,skolem0004)|street(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c102,negated_conjecture,chevy(skolem0001,skolem0004)|lonely(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c107,negated_conjecture,chevy(skolem0001,skolem0004)|event(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c109,negated_conjecture,chevy(skolem0001,skolem0004)|present(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c110,negated_conjecture,chevy(skolem0001,skolem0004)|barrel(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c97,negated_conjecture,chevy(skolem0001,skolem0004)|of(skolem0007,skolem0008,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c108,negated_conjecture,chevy(skolem0001,skolem0004)|agent(skolem0007,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c111,negated_conjecture,chevy(skolem0001,skolem0004)|down(skolem0007,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c112,negated_conjecture,chevy(skolem0001,skolem0004)|in(skolem0007,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c113,negated_conjecture,chevy(skolem0001,skolem0004)|~actual_world(X56)|~of(X56,X55,X57)|~city(X56,X57)|~hollywood_placename(X56,X55)|~placename(X56,X55)|~chevy(X56,X54)|~white(X56,X54)|~dirty(X56,X54)|~old(X56,X54)|~street(X56,X58)|~lonely(X56,X58)|~event(X56,X59)|~agent(X56,X59,X54)|~present(X56,X59)|~barrel(X56,X59)|~down(X56,X59,X58)|~in(X56,X59,X57),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c370,plain,chevy(skolem0001,skolem0004)|~actual_world(skolem0007)|~of(skolem0007,X347,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X347)|~placename(skolem0007,X347)|~chevy(skolem0007,X345)|~white(skolem0007,X345)|~dirty(skolem0007,X345)|~old(skolem0007,X345)|~street(skolem0007,X346)|~lonely(skolem0007,X346)|~event(skolem0007,skolem0011)|~agent(skolem0007,skolem0011,X345)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011)|~down(skolem0007,skolem0011,X346),inference(resolution,[status(thm)],[c113, c112])).
% 6.73/6.89 cnf(c1867,plain,chevy(skolem0001,skolem0004)|~actual_world(skolem0007)|~of(skolem0007,X757,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X757)|~placename(skolem0007,X757)|~chevy(skolem0007,X756)|~white(skolem0007,X756)|~dirty(skolem0007,X756)|~old(skolem0007,X756)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~agent(skolem0007,skolem0011,X756)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c370, c111])).
% 6.73/6.89 cnf(c2649,plain,chevy(skolem0001,skolem0004)|~actual_world(skolem0007)|~of(skolem0007,X758,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X758)|~placename(skolem0007,X758)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c1867, c108])).
% 6.73/6.89 cnf(c2663,plain,chevy(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c2649, c97])).
% 6.73/6.89 cnf(c2685,plain,chevy(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011),inference(resolution,[status(thm)],[c2663, c110])).
% 6.73/6.89 cnf(c2700,plain,chevy(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011),inference(resolution,[status(thm)],[c2685, c109])).
% 6.73/6.89 cnf(c2701,plain,chevy(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009),inference(resolution,[status(thm)],[c2700, c107])).
% 6.73/6.89 cnf(c2718,plain,chevy(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009),inference(resolution,[status(thm)],[c2701, c102])).
% 6.73/6.89 cnf(c2733,plain,chevy(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010),inference(resolution,[status(thm)],[c2718, c101])).
% 6.73/6.89 cnf(c2744,plain,chevy(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010),inference(resolution,[status(thm)],[c2733, c106])).
% 6.73/6.89 cnf(c2762,plain,chevy(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010),inference(resolution,[status(thm)],[c2744, c105])).
% 6.73/6.89 cnf(c2766,plain,chevy(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010),inference(resolution,[status(thm)],[c2762, c104])).
% 6.73/6.89 cnf(c2779,plain,chevy(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008),inference(resolution,[status(thm)],[c2766, c103])).
% 6.73/6.89 cnf(c2792,plain,chevy(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008),inference(resolution,[status(thm)],[c2779, c100])).
% 6.73/6.89 cnf(c2808,plain,chevy(skolem0001,skolem0004)|~actual_world(skolem0007)|~city(skolem0007,skolem0009),inference(resolution,[status(thm)],[c2792, c99])).
% 6.73/6.89 cnf(c2823,plain,chevy(skolem0001,skolem0004)|~actual_world(skolem0007),inference(resolution,[status(thm)],[c2808, c98])).
% 6.73/6.89 cnf(c2835,plain,chevy(skolem0001,skolem0004),inference(resolution,[status(thm)],[c2823, c96])).
% 6.73/6.89 cnf(c78,negated_conjecture,placename(skolem0001,skolem0003)|actual_world(skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c80,negated_conjecture,placename(skolem0001,skolem0003)|city(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c81,negated_conjecture,placename(skolem0001,skolem0003)|hollywood_placename(skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c82,negated_conjecture,placename(skolem0001,skolem0003)|placename(skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c85,negated_conjecture,placename(skolem0001,skolem0003)|chevy(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c86,negated_conjecture,placename(skolem0001,skolem0003)|white(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c87,negated_conjecture,placename(skolem0001,skolem0003)|dirty(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c88,negated_conjecture,placename(skolem0001,skolem0003)|old(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c83,negated_conjecture,placename(skolem0001,skolem0003)|street(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c84,negated_conjecture,placename(skolem0001,skolem0003)|lonely(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c89,negated_conjecture,placename(skolem0001,skolem0003)|event(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c91,negated_conjecture,placename(skolem0001,skolem0003)|present(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c92,negated_conjecture,placename(skolem0001,skolem0003)|barrel(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c79,negated_conjecture,placename(skolem0001,skolem0003)|of(skolem0007,skolem0008,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c90,negated_conjecture,placename(skolem0001,skolem0003)|agent(skolem0007,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c93,negated_conjecture,placename(skolem0001,skolem0003)|down(skolem0007,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c94,negated_conjecture,placename(skolem0001,skolem0003)|in(skolem0007,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c95,negated_conjecture,placename(skolem0001,skolem0003)|~actual_world(X50)|~of(X50,X49,X51)|~city(X50,X51)|~hollywood_placename(X50,X49)|~placename(X50,X49)|~chevy(X50,X48)|~white(X50,X48)|~dirty(X50,X48)|~old(X50,X48)|~street(X50,X52)|~lonely(X50,X52)|~event(X50,X53)|~agent(X50,X53,X48)|~present(X50,X53)|~barrel(X50,X53)|~down(X50,X53,X52)|~in(X50,X53,X51),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c355,plain,placename(skolem0001,skolem0003)|~actual_world(skolem0007)|~of(skolem0007,X302,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X302)|~placename(skolem0007,X302)|~chevy(skolem0007,X301)|~white(skolem0007,X301)|~dirty(skolem0007,X301)|~old(skolem0007,X301)|~street(skolem0007,X300)|~lonely(skolem0007,X300)|~event(skolem0007,skolem0011)|~agent(skolem0007,skolem0011,X301)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011)|~down(skolem0007,skolem0011,X300),inference(resolution,[status(thm)],[c95, c94])).
% 6.73/6.89 cnf(c1844,plain,placename(skolem0001,skolem0003)|~actual_world(skolem0007)|~of(skolem0007,X637,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X637)|~placename(skolem0007,X637)|~chevy(skolem0007,X636)|~white(skolem0007,X636)|~dirty(skolem0007,X636)|~old(skolem0007,X636)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~agent(skolem0007,skolem0011,X636)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c355, c93])).
% 6.73/6.89 cnf(c2404,plain,placename(skolem0001,skolem0003)|~actual_world(skolem0007)|~of(skolem0007,X638,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X638)|~placename(skolem0007,X638)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c1844, c90])).
% 6.73/6.89 cnf(c2419,plain,placename(skolem0001,skolem0003)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c2404, c79])).
% 6.73/6.89 cnf(c2436,plain,placename(skolem0001,skolem0003)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011),inference(resolution,[status(thm)],[c2419, c92])).
% 6.73/6.89 cnf(c2453,plain,placename(skolem0001,skolem0003)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011),inference(resolution,[status(thm)],[c2436, c91])).
% 6.73/6.89 cnf(c2472,plain,placename(skolem0001,skolem0003)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009),inference(resolution,[status(thm)],[c2453, c89])).
% 6.73/6.89 cnf(c2496,plain,placename(skolem0001,skolem0003)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009),inference(resolution,[status(thm)],[c2472, c84])).
% 6.73/6.89 cnf(c2509,plain,placename(skolem0001,skolem0003)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010),inference(resolution,[status(thm)],[c2496, c83])).
% 6.73/6.89 cnf(c2516,plain,placename(skolem0001,skolem0003)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010),inference(resolution,[status(thm)],[c2509, c88])).
% 6.73/6.89 cnf(c2534,plain,placename(skolem0001,skolem0003)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010),inference(resolution,[status(thm)],[c2516, c87])).
% 6.73/6.89 cnf(c2539,plain,placename(skolem0001,skolem0003)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010),inference(resolution,[status(thm)],[c2534, c86])).
% 6.73/6.89 cnf(c2566,plain,placename(skolem0001,skolem0003)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008),inference(resolution,[status(thm)],[c2539, c85])).
% 6.73/6.89 cnf(c2570,plain,placename(skolem0001,skolem0003)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008),inference(resolution,[status(thm)],[c2566, c82])).
% 6.73/6.89 cnf(c2586,plain,placename(skolem0001,skolem0003)|~actual_world(skolem0007)|~city(skolem0007,skolem0009),inference(resolution,[status(thm)],[c2570, c81])).
% 6.73/6.89 cnf(c2602,plain,placename(skolem0001,skolem0003)|~actual_world(skolem0007),inference(resolution,[status(thm)],[c2586, c80])).
% 6.73/6.89 cnf(c2620,plain,placename(skolem0001,skolem0003),inference(resolution,[status(thm)],[c2602, c78])).
% 6.73/6.89 cnf(c60,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|actual_world(skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.89 cnf(c62,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|city(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c63,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|hollywood_placename(skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c64,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|placename(skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c67,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|chevy(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c68,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|white(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c69,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|dirty(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c70,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|old(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c65,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|street(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c66,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|lonely(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c71,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|event(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c73,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|present(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c74,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|barrel(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c61,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|of(skolem0007,skolem0008,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c72,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|agent(skolem0007,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c75,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|down(skolem0007,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c76,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|in(skolem0007,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c77,negated_conjecture,hollywood_placename(skolem0001,skolem0003)|~actual_world(X44)|~of(X44,X43,X45)|~city(X44,X45)|~hollywood_placename(X44,X43)|~placename(X44,X43)|~chevy(X44,X42)|~white(X44,X42)|~dirty(X44,X42)|~old(X44,X42)|~street(X44,X46)|~lonely(X44,X46)|~event(X44,X47)|~agent(X44,X47,X42)|~present(X44,X47)|~barrel(X44,X47)|~down(X44,X47,X46)|~in(X44,X47,X45),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c343,plain,hollywood_placename(skolem0001,skolem0003)|~actual_world(skolem0007)|~of(skolem0007,X264,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X264)|~placename(skolem0007,X264)|~chevy(skolem0007,X266)|~white(skolem0007,X266)|~dirty(skolem0007,X266)|~old(skolem0007,X266)|~street(skolem0007,X265)|~lonely(skolem0007,X265)|~event(skolem0007,skolem0011)|~agent(skolem0007,skolem0011,X266)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011)|~down(skolem0007,skolem0011,X265),inference(resolution,[status(thm)],[c77, c76])).
% 6.73/6.90 cnf(c1826,plain,hollywood_placename(skolem0001,skolem0003)|~actual_world(skolem0007)|~of(skolem0007,X507,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X507)|~placename(skolem0007,X507)|~chevy(skolem0007,X508)|~white(skolem0007,X508)|~dirty(skolem0007,X508)|~old(skolem0007,X508)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~agent(skolem0007,skolem0011,X508)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c343, c75])).
% 6.73/6.90 cnf(c2166,plain,hollywood_placename(skolem0001,skolem0003)|~actual_world(skolem0007)|~of(skolem0007,X509,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X509)|~placename(skolem0007,X509)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c1826, c72])).
% 6.73/6.90 cnf(c2184,plain,hollywood_placename(skolem0001,skolem0003)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c2166, c61])).
% 6.73/6.90 cnf(c2204,plain,hollywood_placename(skolem0001,skolem0003)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011),inference(resolution,[status(thm)],[c2184, c74])).
% 6.73/6.90 cnf(c2208,plain,hollywood_placename(skolem0001,skolem0003)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011),inference(resolution,[status(thm)],[c2204, c73])).
% 6.73/6.90 cnf(c2224,plain,hollywood_placename(skolem0001,skolem0003)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009),inference(resolution,[status(thm)],[c2208, c71])).
% 6.73/6.90 cnf(c2242,plain,hollywood_placename(skolem0001,skolem0003)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009),inference(resolution,[status(thm)],[c2224, c66])).
% 6.73/6.90 cnf(c2260,plain,hollywood_placename(skolem0001,skolem0003)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010),inference(resolution,[status(thm)],[c2242, c65])).
% 6.73/6.90 cnf(c2272,plain,hollywood_placename(skolem0001,skolem0003)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010),inference(resolution,[status(thm)],[c2260, c70])).
% 6.73/6.90 cnf(c2291,plain,hollywood_placename(skolem0001,skolem0003)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010),inference(resolution,[status(thm)],[c2272, c69])).
% 6.73/6.90 cnf(c2302,plain,hollywood_placename(skolem0001,skolem0003)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010),inference(resolution,[status(thm)],[c2291, c68])).
% 6.73/6.90 cnf(c2314,plain,hollywood_placename(skolem0001,skolem0003)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008),inference(resolution,[status(thm)],[c2302, c67])).
% 6.73/6.90 cnf(c2328,plain,hollywood_placename(skolem0001,skolem0003)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008),inference(resolution,[status(thm)],[c2314, c64])).
% 6.73/6.90 cnf(c2349,plain,hollywood_placename(skolem0001,skolem0003)|~actual_world(skolem0007)|~city(skolem0007,skolem0009),inference(resolution,[status(thm)],[c2328, c63])).
% 6.73/6.90 cnf(c2365,plain,hollywood_placename(skolem0001,skolem0003)|~actual_world(skolem0007),inference(resolution,[status(thm)],[c2349, c62])).
% 6.73/6.90 cnf(c2374,plain,hollywood_placename(skolem0001,skolem0003),inference(resolution,[status(thm)],[c2365, c60])).
% 6.73/6.90 cnf(c42,negated_conjecture,city(skolem0001,skolem0002)|actual_world(skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c44,negated_conjecture,city(skolem0001,skolem0002)|city(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c45,negated_conjecture,city(skolem0001,skolem0002)|hollywood_placename(skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c46,negated_conjecture,city(skolem0001,skolem0002)|placename(skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c49,negated_conjecture,city(skolem0001,skolem0002)|chevy(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c50,negated_conjecture,city(skolem0001,skolem0002)|white(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c51,negated_conjecture,city(skolem0001,skolem0002)|dirty(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c52,negated_conjecture,city(skolem0001,skolem0002)|old(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c47,negated_conjecture,city(skolem0001,skolem0002)|street(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c48,negated_conjecture,city(skolem0001,skolem0002)|lonely(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c53,negated_conjecture,city(skolem0001,skolem0002)|event(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c55,negated_conjecture,city(skolem0001,skolem0002)|present(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c56,negated_conjecture,city(skolem0001,skolem0002)|barrel(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c43,negated_conjecture,city(skolem0001,skolem0002)|of(skolem0007,skolem0008,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c54,negated_conjecture,city(skolem0001,skolem0002)|agent(skolem0007,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c57,negated_conjecture,city(skolem0001,skolem0002)|down(skolem0007,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c58,negated_conjecture,city(skolem0001,skolem0002)|in(skolem0007,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c59,negated_conjecture,city(skolem0001,skolem0002)|~actual_world(X38)|~of(X38,X37,X39)|~city(X38,X39)|~hollywood_placename(X38,X37)|~placename(X38,X37)|~chevy(X38,X36)|~white(X38,X36)|~dirty(X38,X36)|~old(X38,X36)|~street(X38,X40)|~lonely(X38,X40)|~event(X38,X41)|~agent(X38,X41,X36)|~present(X38,X41)|~barrel(X38,X41)|~down(X38,X41,X40)|~in(X38,X41,X39),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c338,plain,city(skolem0001,skolem0002)|~actual_world(skolem0007)|~of(skolem0007,X250,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X250)|~placename(skolem0007,X250)|~chevy(skolem0007,X251)|~white(skolem0007,X251)|~dirty(skolem0007,X251)|~old(skolem0007,X251)|~street(skolem0007,X249)|~lonely(skolem0007,X249)|~event(skolem0007,skolem0011)|~agent(skolem0007,skolem0011,X251)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011)|~down(skolem0007,skolem0011,X249),inference(resolution,[status(thm)],[c59, c58])).
% 6.73/6.90 cnf(c1816,plain,city(skolem0001,skolem0002)|~actual_world(skolem0007)|~of(skolem0007,X372,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X372)|~placename(skolem0007,X372)|~chevy(skolem0007,X373)|~white(skolem0007,X373)|~dirty(skolem0007,X373)|~old(skolem0007,X373)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~agent(skolem0007,skolem0011,X373)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c338, c57])).
% 6.73/6.90 cnf(c1901,plain,city(skolem0001,skolem0002)|~actual_world(skolem0007)|~of(skolem0007,X374,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X374)|~placename(skolem0007,X374)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c1816, c54])).
% 6.73/6.90 cnf(c1909,plain,city(skolem0001,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c1901, c43])).
% 6.73/6.90 cnf(c1935,plain,city(skolem0001,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011),inference(resolution,[status(thm)],[c1909, c56])).
% 6.73/6.90 cnf(c1940,plain,city(skolem0001,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011),inference(resolution,[status(thm)],[c1935, c55])).
% 6.73/6.90 cnf(c1958,plain,city(skolem0001,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009),inference(resolution,[status(thm)],[c1940, c53])).
% 6.73/6.90 cnf(c1985,plain,city(skolem0001,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009),inference(resolution,[status(thm)],[c1958, c48])).
% 6.73/6.90 cnf(c1991,plain,city(skolem0001,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010),inference(resolution,[status(thm)],[c1985, c47])).
% 6.73/6.90 cnf(c2003,plain,city(skolem0001,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010),inference(resolution,[status(thm)],[c1991, c52])).
% 6.73/6.90 cnf(c2021,plain,city(skolem0001,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010),inference(resolution,[status(thm)],[c2003, c51])).
% 6.73/6.90 cnf(c2044,plain,city(skolem0001,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010),inference(resolution,[status(thm)],[c2021, c50])).
% 6.73/6.90 cnf(c2057,plain,city(skolem0001,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008),inference(resolution,[status(thm)],[c2044, c49])).
% 6.73/6.90 cnf(c2075,plain,city(skolem0001,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008),inference(resolution,[status(thm)],[c2057, c46])).
% 6.73/6.90 cnf(c2096,plain,city(skolem0001,skolem0002)|~actual_world(skolem0007)|~city(skolem0007,skolem0009),inference(resolution,[status(thm)],[c2075, c45])).
% 6.73/6.90 cnf(c2110,plain,city(skolem0001,skolem0002)|~actual_world(skolem0007),inference(resolution,[status(thm)],[c2096, c44])).
% 6.73/6.90 cnf(c2118,plain,city(skolem0001,skolem0002),inference(resolution,[status(thm)],[c2110, c42])).
% 6.73/6.90 cnf(c6,negated_conjecture,actual_world(skolem0001)|actual_world(skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c8,negated_conjecture,actual_world(skolem0001)|city(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c9,negated_conjecture,actual_world(skolem0001)|hollywood_placename(skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c10,negated_conjecture,actual_world(skolem0001)|placename(skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c13,negated_conjecture,actual_world(skolem0001)|chevy(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c14,negated_conjecture,actual_world(skolem0001)|white(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c15,negated_conjecture,actual_world(skolem0001)|dirty(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c16,negated_conjecture,actual_world(skolem0001)|old(skolem0007,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c11,negated_conjecture,actual_world(skolem0001)|street(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c12,negated_conjecture,actual_world(skolem0001)|lonely(skolem0007,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c17,negated_conjecture,actual_world(skolem0001)|event(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c19,negated_conjecture,actual_world(skolem0001)|present(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c20,negated_conjecture,actual_world(skolem0001)|barrel(skolem0007,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c7,negated_conjecture,actual_world(skolem0001)|of(skolem0007,skolem0008,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c18,negated_conjecture,actual_world(skolem0001)|agent(skolem0007,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c21,negated_conjecture,actual_world(skolem0001)|down(skolem0007,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c22,negated_conjecture,actual_world(skolem0001)|in(skolem0007,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c23,negated_conjecture,actual_world(skolem0001)|~actual_world(X26)|~of(X26,X25,X27)|~city(X26,X27)|~hollywood_placename(X26,X25)|~placename(X26,X25)|~chevy(X26,X24)|~white(X26,X24)|~dirty(X26,X24)|~old(X26,X24)|~street(X26,X28)|~lonely(X26,X28)|~event(X26,X29)|~agent(X26,X29,X24)|~present(X26,X29)|~barrel(X26,X29)|~down(X26,X29,X28)|~in(X26,X29,X27),inference(split_conjunct,[status(thm)],[c5])).
% 6.73/6.90 cnf(c330,plain,actual_world(skolem0001)|~actual_world(skolem0007)|~of(skolem0007,X224,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X224)|~placename(skolem0007,X224)|~chevy(skolem0007,X222)|~white(skolem0007,X222)|~dirty(skolem0007,X222)|~old(skolem0007,X222)|~street(skolem0007,X223)|~lonely(skolem0007,X223)|~event(skolem0007,skolem0011)|~agent(skolem0007,skolem0011,X222)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011)|~down(skolem0007,skolem0011,X223),inference(resolution,[status(thm)],[c23, c22])).
% 6.73/6.90 cnf(c1527,plain,actual_world(skolem0001)|~actual_world(skolem0007)|~of(skolem0007,X226,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X226)|~placename(skolem0007,X226)|~chevy(skolem0007,X225)|~white(skolem0007,X225)|~dirty(skolem0007,X225)|~old(skolem0007,X225)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~agent(skolem0007,skolem0011,X225)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c330, c21])).
% 6.73/6.90 cnf(c1547,plain,actual_world(skolem0001)|~actual_world(skolem0007)|~of(skolem0007,X227,skolem0009)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,X227)|~placename(skolem0007,X227)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c1527, c18])).
% 6.73/6.90 cnf(c1561,plain,actual_world(skolem0001)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011)|~barrel(skolem0007,skolem0011),inference(resolution,[status(thm)],[c1547, c7])).
% 6.73/6.90 cnf(c1581,plain,actual_world(skolem0001)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011)|~present(skolem0007,skolem0011),inference(resolution,[status(thm)],[c1561, c20])).
% 6.73/6.90 cnf(c1601,plain,actual_world(skolem0001)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009)|~event(skolem0007,skolem0011),inference(resolution,[status(thm)],[c1581, c19])).
% 6.73/6.90 cnf(c1607,plain,actual_world(skolem0001)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009)|~lonely(skolem0007,skolem0009),inference(resolution,[status(thm)],[c1601, c17])).
% 6.73/6.90 cnf(c1638,plain,actual_world(skolem0001)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010)|~street(skolem0007,skolem0009),inference(resolution,[status(thm)],[c1607, c12])).
% 6.73/6.90 cnf(c1647,plain,actual_world(skolem0001)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010)|~old(skolem0007,skolem0010),inference(resolution,[status(thm)],[c1638, c11])).
% 6.73/6.90 cnf(c1660,plain,actual_world(skolem0001)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010)|~dirty(skolem0007,skolem0010),inference(resolution,[status(thm)],[c1647, c16])).
% 6.73/6.90 cnf(c1682,plain,actual_world(skolem0001)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010)|~white(skolem0007,skolem0010),inference(resolution,[status(thm)],[c1660, c15])).
% 6.73/6.90 cnf(c1719,plain,actual_world(skolem0001)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008)|~chevy(skolem0007,skolem0010),inference(resolution,[status(thm)],[c1682, c14])).
% 6.73/6.90 cnf(c1741,plain,actual_world(skolem0001)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008)|~placename(skolem0007,skolem0008),inference(resolution,[status(thm)],[c1719, c13])).
% 6.73/6.90 cnf(c1753,plain,actual_world(skolem0001)|~actual_world(skolem0007)|~city(skolem0007,skolem0009)|~hollywood_placename(skolem0007,skolem0008),inference(resolution,[status(thm)],[c1741, c10])).
% 6.73/6.90 cnf(c1759,plain,actual_world(skolem0001)|~actual_world(skolem0007)|~city(skolem0007,skolem0009),inference(resolution,[status(thm)],[c1753, c9])).
% 6.73/6.90 cnf(c1792,plain,actual_world(skolem0001)|~actual_world(skolem0007),inference(resolution,[status(thm)],[c1759, c8])).
% 6.73/6.90 cnf(c1799,plain,actual_world(skolem0001),inference(resolution,[status(thm)],[c1792, c6])).
% 6.73/6.90 % SZS output end Saturation
% 6.73/6.90
% 6.73/6.90 % Initial clauses : 324
% 6.73/6.90 % Processed clauses : 637
% 6.73/6.90 % Factors computed : 4
% 6.73/6.90 % Resolvents computed: 3743
% 6.73/6.90 % Tautologies deleted: 221
% 6.73/6.90 % Forward subsumed : 3213
% 6.73/6.90 % Backward subsumed : 618
% 6.73/6.90 % -------- CPU Time ---------
% 6.73/6.90 % User time : 6.520 s
% 6.73/6.90 % System time : 0.030 s
% 6.73/6.90 % Total time : 6.550 s
%------------------------------------------------------------------------------