%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP120+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:34:12 EDT 2024
% Result : CounterSatisfiable 6.96s 7.12s
% Output : Saturation 6.98s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : NLP120+1 : TPTP v8.1.2. Released v2.4.0.
% 0.11/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.32 % Computer : n026.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.32 % DateTime : Wed May 8 13:41:08 EDT 2024
% 0.12/0.32 % CPUTime :
% 6.96/7.12 % Version: 1.5
% 6.96/7.12 % SZS status CounterSatisfiable
% 6.96/7.12 % SZS output start Saturation
% 6.96/7.12 fof(co1,conjecture,(~(~(((?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(((((((((((((((of(U,V,W)&city(U,W))&hollywood_placename(U,V))&placename(U,V))&chevy(U,W))&white(U,W))&dirty(U,W))&old(U,W))&street(U,X))&lonely(U,X))&event(U,Y))&agent(U,Y,W))&present(U,Y))&barrel(U,Y))&down(U,Y,X))&in(U,Y,W))))))))=>(?[Z]:(actual_world(Z)&(?[X1]:(?[X2]:(?[X3]:(?[X4]:(?[X5]:(((((((((((((((of(Z,X2,X1)&city(Z,X1))&hollywood_placename(Z,X2))&placename(Z,X2))&street(Z,X3))&lonely(Z,X3))&chevy(Z,X4))&white(Z,X4))&dirty(Z,X4))&old(Z,X4))&event(Z,X5))&agent(Z,X5,X4))&present(Z,X5))&barrel(Z,X5))&down(Z,X5,X3))&in(Z,X5,X1))))))))))&((?[Z]:(actual_world(Z)&(?[X1]:(?[X2]:(?[X3]:(?[X4]:(?[X5]:(((((((((((((((of(Z,X2,X1)&city(Z,X1))&hollywood_placename(Z,X2))&placename(Z,X2))&street(Z,X3))&lonely(Z,X3))&chevy(Z,X4))&white(Z,X4))&dirty(Z,X4))&old(Z,X4))&event(Z,X5))&agent(Z,X5,X4))&present(Z,X5))&barrel(Z,X5))&down(Z,X5,X3))&in(Z,X5,X1)))))))))=>(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(((((((((((((((of(U,V,W)&city(U,W))&hollywood_placename(U,V))&placename(U,V))&chevy(U,W))&white(U,W))&dirty(U,W))&old(U,W))&street(U,X))&lonely(U,X))&event(U,Y))&agent(U,Y,W))&present(U,Y))&barrel(U,Y))&down(U,Y,X))&in(U,Y,W)))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1)).
% 6.96/7.12 fof(c0,negated_conjecture,(~(~(~(((?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(((((((((((((((of(U,V,W)&city(U,W))&hollywood_placename(U,V))&placename(U,V))&chevy(U,W))&white(U,W))&dirty(U,W))&old(U,W))&street(U,X))&lonely(U,X))&event(U,Y))&agent(U,Y,W))&present(U,Y))&barrel(U,Y))&down(U,Y,X))&in(U,Y,W))))))))=>(?[Z]:(actual_world(Z)&(?[X1]:(?[X2]:(?[X3]:(?[X4]:(?[X5]:(((((((((((((((of(Z,X2,X1)&city(Z,X1))&hollywood_placename(Z,X2))&placename(Z,X2))&street(Z,X3))&lonely(Z,X3))&chevy(Z,X4))&white(Z,X4))&dirty(Z,X4))&old(Z,X4))&event(Z,X5))&agent(Z,X5,X4))&present(Z,X5))&barrel(Z,X5))&down(Z,X5,X3))&in(Z,X5,X1))))))))))&((?[Z]:(actual_world(Z)&(?[X1]:(?[X2]:(?[X3]:(?[X4]:(?[X5]:(((((((((((((((of(Z,X2,X1)&city(Z,X1))&hollywood_placename(Z,X2))&placename(Z,X2))&street(Z,X3))&lonely(Z,X3))&chevy(Z,X4))&white(Z,X4))&dirty(Z,X4))&old(Z,X4))&event(Z,X5))&agent(Z,X5,X4))&present(Z,X5))&barrel(Z,X5))&down(Z,X5,X3))&in(Z,X5,X1)))))))))=>(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(((((((((((((((of(U,V,W)&city(U,W))&hollywood_placename(U,V))&placename(U,V))&chevy(U,W))&white(U,W))&dirty(U,W))&old(U,W))&street(U,X))&lonely(U,X))&event(U,Y))&agent(U,Y,W))&present(U,Y))&barrel(U,Y))&down(U,Y,X))&in(U,Y,W))))))))))))),inference(assume_negation,[status(cth)],[co1])).
% 6.96/7.12 fof(c1,negated_conjecture,(((?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(((((((((((((((of(U,V,W)&city(U,W))&hollywood_placename(U,V))&placename(U,V))&chevy(U,W))&white(U,W))&dirty(U,W))&old(U,W))&street(U,X))&lonely(U,X))&event(U,Y))&agent(U,Y,W))&present(U,Y))&barrel(U,Y))&down(U,Y,X))&in(U,Y,W))))))))&(![Z]:(~actual_world(Z)|(![X1]:(![X2]:(![X3]:(![X4]:(![X5]:(((((((((((((((~of(Z,X2,X1)|~city(Z,X1))|~hollywood_placename(Z,X2))|~placename(Z,X2))|~street(Z,X3))|~lonely(Z,X3))|~chevy(Z,X4))|~white(Z,X4))|~dirty(Z,X4))|~old(Z,X4))|~event(Z,X5))|~agent(Z,X5,X4))|~present(Z,X5))|~barrel(Z,X5))|~down(Z,X5,X3))|~in(Z,X5,X1))))))))))|((?[Z]:(actual_world(Z)&(?[X1]:(?[X2]:(?[X3]:(?[X4]:(?[X5]:(((((((((((((((of(Z,X2,X1)&city(Z,X1))&hollywood_placename(Z,X2))&placename(Z,X2))&street(Z,X3))&lonely(Z,X3))&chevy(Z,X4))&white(Z,X4))&dirty(Z,X4))&old(Z,X4))&event(Z,X5))&agent(Z,X5,X4))&present(Z,X5))&barrel(Z,X5))&down(Z,X5,X3))&in(Z,X5,X1)))))))))&(![U]:(~actual_world(U)|(![V]:(![W]:(![X]:(![Y]:(((((((((((((((~of(U,V,W)|~city(U,W))|~hollywood_placename(U,V))|~placename(U,V))|~chevy(U,W))|~white(U,W))|~dirty(U,W))|~old(U,W))|~street(U,X))|~lonely(U,X))|~event(U,Y))|~agent(U,Y,W))|~present(U,Y))|~barrel(U,Y))|~down(U,Y,X))|~in(U,Y,W)))))))))),inference(fof_nnf,[status(thm)],[c0])).
% 6.96/7.12 fof(c2,negated_conjecture,(((?[X2]:(actual_world(X2)&(?[X3]:(?[X4]:(?[X5]:(?[X6]:(((((((((((((((of(X2,X3,X4)&city(X2,X4))&hollywood_placename(X2,X3))&placename(X2,X3))&chevy(X2,X4))&white(X2,X4))&dirty(X2,X4))&old(X2,X4))&street(X2,X5))&lonely(X2,X5))&event(X2,X6))&agent(X2,X6,X4))&present(X2,X6))&barrel(X2,X6))&down(X2,X6,X5))&in(X2,X6,X4))))))))&(![X7]:(~actual_world(X7)|(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~street(X7,X10))|~lonely(X7,X10))|~chevy(X7,X11))|~white(X7,X11))|~dirty(X7,X11))|~old(X7,X11))|~event(X7,X12))|~agent(X7,X12,X11))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X10))|~in(X7,X12,X8))))))))))|((?[X13]:(actual_world(X13)&(?[X14]:(?[X15]:(?[X16]:(?[X17]:(?[X18]:(((((((((((((((of(X13,X15,X14)&city(X13,X14))&hollywood_placename(X13,X15))&placename(X13,X15))&street(X13,X16))&lonely(X13,X16))&chevy(X13,X17))&white(X13,X17))&dirty(X13,X17))&old(X13,X17))&event(X13,X18))&agent(X13,X18,X17))&present(X13,X18))&barrel(X13,X18))&down(X13,X18,X16))&in(X13,X18,X14)))))))))&(![X19]:(~actual_world(X19)|(![X20]:(![X21]:(![X22]:(![X23]:(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21)))))))))),inference(variable_rename,[status(thm)],[c1])).
% 6.96/7.12 fof(c4,negated_conjecture,(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(((actual_world(skolem0001)&(((((((((((((((of(skolem0001,skolem0002,skolem0003)&city(skolem0001,skolem0003))&hollywood_placename(skolem0001,skolem0002))&placename(skolem0001,skolem0002))&chevy(skolem0001,skolem0003))&white(skolem0001,skolem0003))&dirty(skolem0001,skolem0003))&old(skolem0001,skolem0003))&street(skolem0001,skolem0004))&lonely(skolem0001,skolem0004))&event(skolem0001,skolem0005))&agent(skolem0001,skolem0005,skolem0003))&present(skolem0001,skolem0005))&barrel(skolem0001,skolem0005))&down(skolem0001,skolem0005,skolem0004))&in(skolem0001,skolem0005,skolem0003)))&(~actual_world(X7)|(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~street(X7,X10))|~lonely(X7,X10))|~chevy(X7,X11))|~white(X7,X11))|~dirty(X7,X11))|~old(X7,X11))|~event(X7,X12))|~agent(X7,X12,X11))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X10))|~in(X7,X12,X8))))|((actual_world(skolem0006)&(((((((((((((((of(skolem0006,skolem0008,skolem0007)&city(skolem0006,skolem0007))&hollywood_placename(skolem0006,skolem0008))&placename(skolem0006,skolem0008))&street(skolem0006,skolem0009))&lonely(skolem0006,skolem0009))&chevy(skolem0006,skolem0010))&white(skolem0006,skolem0010))&dirty(skolem0006,skolem0010))&old(skolem0006,skolem0010))&event(skolem0006,skolem0011))&agent(skolem0006,skolem0011,skolem0010))&present(skolem0006,skolem0011))&barrel(skolem0006,skolem0011))&down(skolem0006,skolem0011,skolem0009))&in(skolem0006,skolem0011,skolem0007)))&(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21)))))))))))))))),inference(shift_quantors,[status(thm)],[fof(c3,negated_conjecture,(((actual_world(skolem0001)&(((((((((((((((of(skolem0001,skolem0002,skolem0003)&city(skolem0001,skolem0003))&hollywood_placename(skolem0001,skolem0002))&placename(skolem0001,skolem0002))&chevy(skolem0001,skolem0003))&white(skolem0001,skolem0003))&dirty(skolem0001,skolem0003))&old(skolem0001,skolem0003))&street(skolem0001,skolem0004))&lonely(skolem0001,skolem0004))&event(skolem0001,skolem0005))&agent(skolem0001,skolem0005,skolem0003))&present(skolem0001,skolem0005))&barrel(skolem0001,skolem0005))&down(skolem0001,skolem0005,skolem0004))&in(skolem0001,skolem0005,skolem0003)))&(![X7]:(~actual_world(X7)|(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~street(X7,X10))|~lonely(X7,X10))|~chevy(X7,X11))|~white(X7,X11))|~dirty(X7,X11))|~old(X7,X11))|~event(X7,X12))|~agent(X7,X12,X11))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X10))|~in(X7,X12,X8))))))))))|((actual_world(skolem0006)&(((((((((((((((of(skolem0006,skolem0008,skolem0007)&city(skolem0006,skolem0007))&hollywood_placename(skolem0006,skolem0008))&placename(skolem0006,skolem0008))&street(skolem0006,skolem0009))&lonely(skolem0006,skolem0009))&chevy(skolem0006,skolem0010))&white(skolem0006,skolem0010))&dirty(skolem0006,skolem0010))&old(skolem0006,skolem0010))&event(skolem0006,skolem0011))&agent(skolem0006,skolem0011,skolem0010))&present(skolem0006,skolem0011))&barrel(skolem0006,skolem0011))&down(skolem0006,skolem0011,skolem0009))&in(skolem0006,skolem0011,skolem0007)))&(![X19]:(~actual_world(X19)|(![X20]:(![X21]:(![X22]:(![X23]:(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21)))))))))),inference(skolemize,[status(esa)],[c2])).])).
% 6.96/7.13 fof(c5,negated_conjecture,(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(((((actual_world(skolem0001)|actual_world(skolem0006))&((((((((((((((((actual_world(skolem0001)|of(skolem0006,skolem0008,skolem0007))&(actual_world(skolem0001)|city(skolem0006,skolem0007)))&(actual_world(skolem0001)|hollywood_placename(skolem0006,skolem0008)))&(actual_world(skolem0001)|placename(skolem0006,skolem0008)))&(actual_world(skolem0001)|street(skolem0006,skolem0009)))&(actual_world(skolem0001)|lonely(skolem0006,skolem0009)))&(actual_world(skolem0001)|chevy(skolem0006,skolem0010)))&(actual_world(skolem0001)|white(skolem0006,skolem0010)))&(actual_world(skolem0001)|dirty(skolem0006,skolem0010)))&(actual_world(skolem0001)|old(skolem0006,skolem0010)))&(actual_world(skolem0001)|event(skolem0006,skolem0011)))&(actual_world(skolem0001)|agent(skolem0006,skolem0011,skolem0010)))&(actual_world(skolem0001)|present(skolem0006,skolem0011)))&(actual_world(skolem0001)|barrel(skolem0006,skolem0011)))&(actual_world(skolem0001)|down(skolem0006,skolem0011,skolem0009)))&(actual_world(skolem0001)|in(skolem0006,skolem0011,skolem0007))))&(actual_world(skolem0001)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21)))))&((((((((((((((((((of(skolem0001,skolem0002,skolem0003)|actual_world(skolem0006))&((((((((((((((((of(skolem0001,skolem0002,skolem0003)|of(skolem0006,skolem0008,skolem0007))&(of(skolem0001,skolem0002,skolem0003)|city(skolem0006,skolem0007)))&(of(skolem0001,skolem0002,skolem0003)|hollywood_placename(skolem0006,skolem0008)))&(of(skolem0001,skolem0002,skolem0003)|placename(skolem0006,skolem0008)))&(of(skolem0001,skolem0002,skolem0003)|street(skolem0006,skolem0009)))&(of(skolem0001,skolem0002,skolem0003)|lonely(skolem0006,skolem0009)))&(of(skolem0001,skolem0002,skolem0003)|chevy(skolem0006,skolem0010)))&(of(skolem0001,skolem0002,skolem0003)|white(skolem0006,skolem0010)))&(of(skolem0001,skolem0002,skolem0003)|dirty(skolem0006,skolem0010)))&(of(skolem0001,skolem0002,skolem0003)|old(skolem0006,skolem0010)))&(of(skolem0001,skolem0002,skolem0003)|event(skolem0006,skolem0011)))&(of(skolem0001,skolem0002,skolem0003)|agent(skolem0006,skolem0011,skolem0010)))&(of(skolem0001,skolem0002,skolem0003)|present(skolem0006,skolem0011)))&(of(skolem0001,skolem0002,skolem0003)|barrel(skolem0006,skolem0011)))&(of(skolem0001,skolem0002,skolem0003)|down(skolem0006,skolem0011,skolem0009)))&(of(skolem0001,skolem0002,skolem0003)|in(skolem0006,skolem0011,skolem0007))))&(of(skolem0001,skolem0002,skolem0003)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21)))))&(((city(skolem0001,skolem0003)|actual_world(skolem0006))&((((((((((((((((city(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007))&(city(skolem0001,skolem0003)|city(skolem0006,skolem0007)))&(city(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008)))&(city(skolem0001,skolem0003)|placename(skolem0006,skolem0008)))&(city(skolem0001,skolem0003)|street(skolem0006,skolem0009)))&(city(skolem0001,skolem0003)|lonely(skolem0006,skolem0009)))&(city(skolem0001,skolem0003)|chevy(skolem0006,skolem0010)))&(city(skolem0001,skolem0003)|white(skolem0006,skolem0010)))&(city(skolem0001,skolem0003)|dirty(skolem0006,skolem0010)))&(city(skolem0001,skolem0003)|old(skolem0006,skolem0010)))&(city(skolem0001,skolem0003)|event(skolem0006,skolem0011)))&(city(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0010)))&(city(skolem0001,skolem0003)|present(skolem0006,skolem0011)))&(city(skolem0001,skolem0003)|barrel(skolem0006,skolem0011)))&(city(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0009)))&(city(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007))))&(city(skolem0001,skolem0003)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21))))))&(((hollywood_placename(skolem0001,skolem0002)|actual_world(skolem0006))&((((((((((((((((hollywood_placename(skolem0001,skolem0002)|of(skolem0006,skolem0008,skolem0007))&(hollywood_placename(skolem0001,skolem0002)|city(skolem0006,skolem0007)))&(hollywood_placename(skolem0001,skolem0002)|hollywood_placename(skolem0006,skolem0008)))&(hollywood_placename(skolem0001,skolem0002)|placename(skolem0006,skolem0008)))&(hollywood_placename(skolem0001,skolem0002)|street(skolem0006,skolem0009)))&(hollywood_placename(skolem0001,skolem0002)|lonely(skolem0006,skolem0009)))&(hollywood_placename(skolem0001,skolem0002)|chevy(skolem0006,skolem0010)))&(hollywood_placename(skolem0001,skolem0002)|white(skolem0006,skolem0010)))&(hollywood_placename(skolem0001,skolem0002)|dirty(skolem0006,skolem0010)))&(hollywood_placename(skolem0001,skolem0002)|old(skolem0006,skolem0010)))&(hollywood_placename(skolem0001,skolem0002)|event(skolem0006,skolem0011)))&(hollywood_placename(skolem0001,skolem0002)|agent(skolem0006,skolem0011,skolem0010)))&(hollywood_placename(skolem0001,skolem0002)|present(skolem0006,skolem0011)))&(hollywood_placename(skolem0001,skolem0002)|barrel(skolem0006,skolem0011)))&(hollywood_placename(skolem0001,skolem0002)|down(skolem0006,skolem0011,skolem0009)))&(hollywood_placename(skolem0001,skolem0002)|in(skolem0006,skolem0011,skolem0007))))&(hollywood_placename(skolem0001,skolem0002)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21))))))&(((placename(skolem0001,skolem0002)|actual_world(skolem0006))&((((((((((((((((placename(skolem0001,skolem0002)|of(skolem0006,skolem0008,skolem0007))&(placename(skolem0001,skolem0002)|city(skolem0006,skolem0007)))&(placename(skolem0001,skolem0002)|hollywood_placename(skolem0006,skolem0008)))&(placename(skolem0001,skolem0002)|placename(skolem0006,skolem0008)))&(placename(skolem0001,skolem0002)|street(skolem0006,skolem0009)))&(placename(skolem0001,skolem0002)|lonely(skolem0006,skolem0009)))&(placename(skolem0001,skolem0002)|chevy(skolem0006,skolem0010)))&(placename(skolem0001,skolem0002)|white(skolem0006,skolem0010)))&(placename(skolem0001,skolem0002)|dirty(skolem0006,skolem0010)))&(placename(skolem0001,skolem0002)|old(skolem0006,skolem0010)))&(placename(skolem0001,skolem0002)|event(skolem0006,skolem0011)))&(placename(skolem0001,skolem0002)|agent(skolem0006,skolem0011,skolem0010)))&(placename(skolem0001,skolem0002)|present(skolem0006,skolem0011)))&(placename(skolem0001,skolem0002)|barrel(skolem0006,skolem0011)))&(placename(skolem0001,skolem0002)|down(skolem0006,skolem0011,skolem0009)))&(placename(skolem0001,skolem0002)|in(skolem0006,skolem0011,skolem0007))))&(placename(skolem0001,skolem0002)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21))))))&(((chevy(skolem0001,skolem0003)|actual_world(skolem0006))&((((((((((((((((chevy(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007))&(chevy(skolem0001,skolem0003)|city(skolem0006,skolem0007)))&(chevy(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008)))&(chevy(skolem0001,skolem0003)|placename(skolem0006,skolem0008)))&(chevy(skolem0001,skolem0003)|street(skolem0006,skolem0009)))&(chevy(skolem0001,skolem0003)|lonely(skolem0006,skolem0009)))&(chevy(skolem0001,skolem0003)|chevy(skolem0006,skolem0010)))&(chevy(skolem0001,skolem0003)|white(skolem0006,skolem0010)))&(chevy(skolem0001,skolem0003)|dirty(skolem0006,skolem0010)))&(chevy(skolem0001,skolem0003)|old(skolem0006,skolem0010)))&(chevy(skolem0001,skolem0003)|event(skolem0006,skolem0011)))&(chevy(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0010)))&(chevy(skolem0001,skolem0003)|present(skolem0006,skolem0011)))&(chevy(skolem0001,skolem0003)|barrel(skolem0006,skolem0011)))&(chevy(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0009)))&(chevy(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007))))&(chevy(skolem0001,skolem0003)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21))))))&(((white(skolem0001,skolem0003)|actual_world(skolem0006))&((((((((((((((((white(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007))&(white(skolem0001,skolem0003)|city(skolem0006,skolem0007)))&(white(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008)))&(white(skolem0001,skolem0003)|placename(skolem0006,skolem0008)))&(white(skolem0001,skolem0003)|street(skolem0006,skolem0009)))&(white(skolem0001,skolem0003)|lonely(skolem0006,skolem0009)))&(white(skolem0001,skolem0003)|chevy(skolem0006,skolem0010)))&(white(skolem0001,skolem0003)|white(skolem0006,skolem0010)))&(white(skolem0001,skolem0003)|dirty(skolem0006,skolem0010)))&(white(skolem0001,skolem0003)|old(skolem0006,skolem0010)))&(white(skolem0001,skolem0003)|event(skolem0006,skolem0011)))&(white(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0010)))&(white(skolem0001,skolem0003)|present(skolem0006,skolem0011)))&(white(skolem0001,skolem0003)|barrel(skolem0006,skolem0011)))&(white(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0009)))&(white(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007))))&(white(skolem0001,skolem0003)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21))))))&(((dirty(skolem0001,skolem0003)|actual_world(skolem0006))&((((((((((((((((dirty(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007))&(dirty(skolem0001,skolem0003)|city(skolem0006,skolem0007)))&(dirty(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008)))&(dirty(skolem0001,skolem0003)|placename(skolem0006,skolem0008)))&(dirty(skolem0001,skolem0003)|street(skolem0006,skolem0009)))&(dirty(skolem0001,skolem0003)|lonely(skolem0006,skolem0009)))&(dirty(skolem0001,skolem0003)|chevy(skolem0006,skolem0010)))&(dirty(skolem0001,skolem0003)|white(skolem0006,skolem0010)))&(dirty(skolem0001,skolem0003)|dirty(skolem0006,skolem0010)))&(dirty(skolem0001,skolem0003)|old(skolem0006,skolem0010)))&(dirty(skolem0001,skolem0003)|event(skolem0006,skolem0011)))&(dirty(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0010)))&(dirty(skolem0001,skolem0003)|present(skolem0006,skolem0011)))&(dirty(skolem0001,skolem0003)|barrel(skolem0006,skolem0011)))&(dirty(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0009)))&(dirty(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007))))&(dirty(skolem0001,skolem0003)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21))))))&(((old(skolem0001,skolem0003)|actual_world(skolem0006))&((((((((((((((((old(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007))&(old(skolem0001,skolem0003)|city(skolem0006,skolem0007)))&(old(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008)))&(old(skolem0001,skolem0003)|placename(skolem0006,skolem0008)))&(old(skolem0001,skolem0003)|street(skolem0006,skolem0009)))&(old(skolem0001,skolem0003)|lonely(skolem0006,skolem0009)))&(old(skolem0001,skolem0003)|chevy(skolem0006,skolem0010)))&(old(skolem0001,skolem0003)|white(skolem0006,skolem0010)))&(old(skolem0001,skolem0003)|dirty(skolem0006,skolem0010)))&(old(skolem0001,skolem0003)|old(skolem0006,skolem0010)))&(old(skolem0001,skolem0003)|event(skolem0006,skolem0011)))&(old(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0010)))&(old(skolem0001,skolem0003)|present(skolem0006,skolem0011)))&(old(skolem0001,skolem0003)|barrel(skolem0006,skolem0011)))&(old(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0009)))&(old(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007))))&(old(skolem0001,skolem0003)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21))))))&(((street(skolem0001,skolem0004)|actual_world(skolem0006))&((((((((((((((((street(skolem0001,skolem0004)|of(skolem0006,skolem0008,skolem0007))&(street(skolem0001,skolem0004)|city(skolem0006,skolem0007)))&(street(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0008)))&(street(skolem0001,skolem0004)|placename(skolem0006,skolem0008)))&(street(skolem0001,skolem0004)|street(skolem0006,skolem0009)))&(street(skolem0001,skolem0004)|lonely(skolem0006,skolem0009)))&(street(skolem0001,skolem0004)|chevy(skolem0006,skolem0010)))&(street(skolem0001,skolem0004)|white(skolem0006,skolem0010)))&(street(skolem0001,skolem0004)|dirty(skolem0006,skolem0010)))&(street(skolem0001,skolem0004)|old(skolem0006,skolem0010)))&(street(skolem0001,skolem0004)|event(skolem0006,skolem0011)))&(street(skolem0001,skolem0004)|agent(skolem0006,skolem0011,skolem0010)))&(street(skolem0001,skolem0004)|present(skolem0006,skolem0011)))&(street(skolem0001,skolem0004)|barrel(skolem0006,skolem0011)))&(street(skolem0001,skolem0004)|down(skolem0006,skolem0011,skolem0009)))&(street(skolem0001,skolem0004)|in(skolem0006,skolem0011,skolem0007))))&(street(skolem0001,skolem0004)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21))))))&(((lonely(skolem0001,skolem0004)|actual_world(skolem0006))&((((((((((((((((lonely(skolem0001,skolem0004)|of(skolem0006,skolem0008,skolem0007))&(lonely(skolem0001,skolem0004)|city(skolem0006,skolem0007)))&(lonely(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0008)))&(lonely(skolem0001,skolem0004)|placename(skolem0006,skolem0008)))&(lonely(skolem0001,skolem0004)|street(skolem0006,skolem0009)))&(lonely(skolem0001,skolem0004)|lonely(skolem0006,skolem0009)))&(lonely(skolem0001,skolem0004)|chevy(skolem0006,skolem0010)))&(lonely(skolem0001,skolem0004)|white(skolem0006,skolem0010)))&(lonely(skolem0001,skolem0004)|dirty(skolem0006,skolem0010)))&(lonely(skolem0001,skolem0004)|old(skolem0006,skolem0010)))&(lonely(skolem0001,skolem0004)|event(skolem0006,skolem0011)))&(lonely(skolem0001,skolem0004)|agent(skolem0006,skolem0011,skolem0010)))&(lonely(skolem0001,skolem0004)|present(skolem0006,skolem0011)))&(lonely(skolem0001,skolem0004)|barrel(skolem0006,skolem0011)))&(lonely(skolem0001,skolem0004)|down(skolem0006,skolem0011,skolem0009)))&(lonely(skolem0001,skolem0004)|in(skolem0006,skolem0011,skolem0007))))&(lonely(skolem0001,skolem0004)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21))))))&(((event(skolem0001,skolem0005)|actual_world(skolem0006))&((((((((((((((((event(skolem0001,skolem0005)|of(skolem0006,skolem0008,skolem0007))&(event(skolem0001,skolem0005)|city(skolem0006,skolem0007)))&(event(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0008)))&(event(skolem0001,skolem0005)|placename(skolem0006,skolem0008)))&(event(skolem0001,skolem0005)|street(skolem0006,skolem0009)))&(event(skolem0001,skolem0005)|lonely(skolem0006,skolem0009)))&(event(skolem0001,skolem0005)|chevy(skolem0006,skolem0010)))&(event(skolem0001,skolem0005)|white(skolem0006,skolem0010)))&(event(skolem0001,skolem0005)|dirty(skolem0006,skolem0010)))&(event(skolem0001,skolem0005)|old(skolem0006,skolem0010)))&(event(skolem0001,skolem0005)|event(skolem0006,skolem0011)))&(event(skolem0001,skolem0005)|agent(skolem0006,skolem0011,skolem0010)))&(event(skolem0001,skolem0005)|present(skolem0006,skolem0011)))&(event(skolem0001,skolem0005)|barrel(skolem0006,skolem0011)))&(event(skolem0001,skolem0005)|down(skolem0006,skolem0011,skolem0009)))&(event(skolem0001,skolem0005)|in(skolem0006,skolem0011,skolem0007))))&(event(skolem0001,skolem0005)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21))))))&(((agent(skolem0001,skolem0005,skolem0003)|actual_world(skolem0006))&((((((((((((((((agent(skolem0001,skolem0005,skolem0003)|of(skolem0006,skolem0008,skolem0007))&(agent(skolem0001,skolem0005,skolem0003)|city(skolem0006,skolem0007)))&(agent(skolem0001,skolem0005,skolem0003)|hollywood_placename(skolem0006,skolem0008)))&(agent(skolem0001,skolem0005,skolem0003)|placename(skolem0006,skolem0008)))&(agent(skolem0001,skolem0005,skolem0003)|street(skolem0006,skolem0009)))&(agent(skolem0001,skolem0005,skolem0003)|lonely(skolem0006,skolem0009)))&(agent(skolem0001,skolem0005,skolem0003)|chevy(skolem0006,skolem0010)))&(agent(skolem0001,skolem0005,skolem0003)|white(skolem0006,skolem0010)))&(agent(skolem0001,skolem0005,skolem0003)|dirty(skolem0006,skolem0010)))&(agent(skolem0001,skolem0005,skolem0003)|old(skolem0006,skolem0010)))&(agent(skolem0001,skolem0005,skolem0003)|event(skolem0006,skolem0011)))&(agent(skolem0001,skolem0005,skolem0003)|agent(skolem0006,skolem0011,skolem0010)))&(agent(skolem0001,skolem0005,skolem0003)|present(skolem0006,skolem0011)))&(agent(skolem0001,skolem0005,skolem0003)|barrel(skolem0006,skolem0011)))&(agent(skolem0001,skolem0005,skolem0003)|down(skolem0006,skolem0011,skolem0009)))&(agent(skolem0001,skolem0005,skolem0003)|in(skolem0006,skolem0011,skolem0007))))&(agent(skolem0001,skolem0005,skolem0003)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21))))))&(((present(skolem0001,skolem0005)|actual_world(skolem0006))&((((((((((((((((present(skolem0001,skolem0005)|of(skolem0006,skolem0008,skolem0007))&(present(skolem0001,skolem0005)|city(skolem0006,skolem0007)))&(present(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0008)))&(present(skolem0001,skolem0005)|placename(skolem0006,skolem0008)))&(present(skolem0001,skolem0005)|street(skolem0006,skolem0009)))&(present(skolem0001,skolem0005)|lonely(skolem0006,skolem0009)))&(present(skolem0001,skolem0005)|chevy(skolem0006,skolem0010)))&(present(skolem0001,skolem0005)|white(skolem0006,skolem0010)))&(present(skolem0001,skolem0005)|dirty(skolem0006,skolem0010)))&(present(skolem0001,skolem0005)|old(skolem0006,skolem0010)))&(present(skolem0001,skolem0005)|event(skolem0006,skolem0011)))&(present(skolem0001,skolem0005)|agent(skolem0006,skolem0011,skolem0010)))&(present(skolem0001,skolem0005)|present(skolem0006,skolem0011)))&(present(skolem0001,skolem0005)|barrel(skolem0006,skolem0011)))&(present(skolem0001,skolem0005)|down(skolem0006,skolem0011,skolem0009)))&(present(skolem0001,skolem0005)|in(skolem0006,skolem0011,skolem0007))))&(present(skolem0001,skolem0005)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21))))))&(((barrel(skolem0001,skolem0005)|actual_world(skolem0006))&((((((((((((((((barrel(skolem0001,skolem0005)|of(skolem0006,skolem0008,skolem0007))&(barrel(skolem0001,skolem0005)|city(skolem0006,skolem0007)))&(barrel(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0008)))&(barrel(skolem0001,skolem0005)|placename(skolem0006,skolem0008)))&(barrel(skolem0001,skolem0005)|street(skolem0006,skolem0009)))&(barrel(skolem0001,skolem0005)|lonely(skolem0006,skolem0009)))&(barrel(skolem0001,skolem0005)|chevy(skolem0006,skolem0010)))&(barrel(skolem0001,skolem0005)|white(skolem0006,skolem0010)))&(barrel(skolem0001,skolem0005)|dirty(skolem0006,skolem0010)))&(barrel(skolem0001,skolem0005)|old(skolem0006,skolem0010)))&(barrel(skolem0001,skolem0005)|event(skolem0006,skolem0011)))&(barrel(skolem0001,skolem0005)|agent(skolem0006,skolem0011,skolem0010)))&(barrel(skolem0001,skolem0005)|present(skolem0006,skolem0011)))&(barrel(skolem0001,skolem0005)|barrel(skolem0006,skolem0011)))&(barrel(skolem0001,skolem0005)|down(skolem0006,skolem0011,skolem0009)))&(barrel(skolem0001,skolem0005)|in(skolem0006,skolem0011,skolem0007))))&(barrel(skolem0001,skolem0005)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21))))))&(((down(skolem0001,skolem0005,skolem0004)|actual_world(skolem0006))&((((((((((((((((down(skolem0001,skolem0005,skolem0004)|of(skolem0006,skolem0008,skolem0007))&(down(skolem0001,skolem0005,skolem0004)|city(skolem0006,skolem0007)))&(down(skolem0001,skolem0005,skolem0004)|hollywood_placename(skolem0006,skolem0008)))&(down(skolem0001,skolem0005,skolem0004)|placename(skolem0006,skolem0008)))&(down(skolem0001,skolem0005,skolem0004)|street(skolem0006,skolem0009)))&(down(skolem0001,skolem0005,skolem0004)|lonely(skolem0006,skolem0009)))&(down(skolem0001,skolem0005,skolem0004)|chevy(skolem0006,skolem0010)))&(down(skolem0001,skolem0005,skolem0004)|white(skolem0006,skolem0010)))&(down(skolem0001,skolem0005,skolem0004)|dirty(skolem0006,skolem0010)))&(down(skolem0001,skolem0005,skolem0004)|old(skolem0006,skolem0010)))&(down(skolem0001,skolem0005,skolem0004)|event(skolem0006,skolem0011)))&(down(skolem0001,skolem0005,skolem0004)|agent(skolem0006,skolem0011,skolem0010)))&(down(skolem0001,skolem0005,skolem0004)|present(skolem0006,skolem0011)))&(down(skolem0001,skolem0005,skolem0004)|barrel(skolem0006,skolem0011)))&(down(skolem0001,skolem0005,skolem0004)|down(skolem0006,skolem0011,skolem0009)))&(down(skolem0001,skolem0005,skolem0004)|in(skolem0006,skolem0011,skolem0007))))&(down(skolem0001,skolem0005,skolem0004)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21))))))&(((in(skolem0001,skolem0005,skolem0003)|actual_world(skolem0006))&((((((((((((((((in(skolem0001,skolem0005,skolem0003)|of(skolem0006,skolem0008,skolem0007))&(in(skolem0001,skolem0005,skolem0003)|city(skolem0006,skolem0007)))&(in(skolem0001,skolem0005,skolem0003)|hollywood_placename(skolem0006,skolem0008)))&(in(skolem0001,skolem0005,skolem0003)|placename(skolem0006,skolem0008)))&(in(skolem0001,skolem0005,skolem0003)|street(skolem0006,skolem0009)))&(in(skolem0001,skolem0005,skolem0003)|lonely(skolem0006,skolem0009)))&(in(skolem0001,skolem0005,skolem0003)|chevy(skolem0006,skolem0010)))&(in(skolem0001,skolem0005,skolem0003)|white(skolem0006,skolem0010)))&(in(skolem0001,skolem0005,skolem0003)|dirty(skolem0006,skolem0010)))&(in(skolem0001,skolem0005,skolem0003)|old(skolem0006,skolem0010)))&(in(skolem0001,skolem0005,skolem0003)|event(skolem0006,skolem0011)))&(in(skolem0001,skolem0005,skolem0003)|agent(skolem0006,skolem0011,skolem0010)))&(in(skolem0001,skolem0005,skolem0003)|present(skolem0006,skolem0011)))&(in(skolem0001,skolem0005,skolem0003)|barrel(skolem0006,skolem0011)))&(in(skolem0001,skolem0005,skolem0003)|down(skolem0006,skolem0011,skolem0009)))&(in(skolem0001,skolem0005,skolem0003)|in(skolem0006,skolem0011,skolem0007))))&(in(skolem0001,skolem0005,skolem0003)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21)))))))&((((~actual_world(X7)|(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~street(X7,X10))|~lonely(X7,X10))|~chevy(X7,X11))|~white(X7,X11))|~dirty(X7,X11))|~old(X7,X11))|~event(X7,X12))|~agent(X7,X12,X11))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X10))|~in(X7,X12,X8)))|actual_world(skolem0006))&(((((((((((((((((~actual_world(X7)|(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~street(X7,X10))|~lonely(X7,X10))|~chevy(X7,X11))|~white(X7,X11))|~dirty(X7,X11))|~old(X7,X11))|~event(X7,X12))|~agent(X7,X12,X11))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X10))|~in(X7,X12,X8)))|of(skolem0006,skolem0008,skolem0007))&((~actual_world(X7)|(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~street(X7,X10))|~lonely(X7,X10))|~chevy(X7,X11))|~white(X7,X11))|~dirty(X7,X11))|~old(X7,X11))|~event(X7,X12))|~agent(X7,X12,X11))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X10))|~in(X7,X12,X8)))|city(skolem0006,skolem0007)))&((~actual_world(X7)|(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~street(X7,X10))|~lonely(X7,X10))|~chevy(X7,X11))|~white(X7,X11))|~dirty(X7,X11))|~old(X7,X11))|~event(X7,X12))|~agent(X7,X12,X11))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X10))|~in(X7,X12,X8)))|hollywood_placename(skolem0006,skolem0008)))&((~actual_world(X7)|(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~street(X7,X10))|~lonely(X7,X10))|~chevy(X7,X11))|~white(X7,X11))|~dirty(X7,X11))|~old(X7,X11))|~event(X7,X12))|~agent(X7,X12,X11))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X10))|~in(X7,X12,X8)))|placename(skolem0006,skolem0008)))&((~actual_world(X7)|(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~street(X7,X10))|~lonely(X7,X10))|~chevy(X7,X11))|~white(X7,X11))|~dirty(X7,X11))|~old(X7,X11))|~event(X7,X12))|~agent(X7,X12,X11))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X10))|~in(X7,X12,X8)))|street(skolem0006,skolem0009)))&((~actual_world(X7)|(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~street(X7,X10))|~lonely(X7,X10))|~chevy(X7,X11))|~white(X7,X11))|~dirty(X7,X11))|~old(X7,X11))|~event(X7,X12))|~agent(X7,X12,X11))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X10))|~in(X7,X12,X8)))|lonely(skolem0006,skolem0009)))&((~actual_world(X7)|(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~street(X7,X10))|~lonely(X7,X10))|~chevy(X7,X11))|~white(X7,X11))|~dirty(X7,X11))|~old(X7,X11))|~event(X7,X12))|~agent(X7,X12,X11))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X10))|~in(X7,X12,X8)))|chevy(skolem0006,skolem0010)))&((~actual_world(X7)|(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~street(X7,X10))|~lonely(X7,X10))|~chevy(X7,X11))|~white(X7,X11))|~dirty(X7,X11))|~old(X7,X11))|~event(X7,X12))|~agent(X7,X12,X11))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X10))|~in(X7,X12,X8)))|white(skolem0006,skolem0010)))&((~actual_world(X7)|(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~street(X7,X10))|~lonely(X7,X10))|~chevy(X7,X11))|~white(X7,X11))|~dirty(X7,X11))|~old(X7,X11))|~event(X7,X12))|~agent(X7,X12,X11))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X10))|~in(X7,X12,X8)))|dirty(skolem0006,skolem0010)))&((~actual_world(X7)|(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~street(X7,X10))|~lonely(X7,X10))|~chevy(X7,X11))|~white(X7,X11))|~dirty(X7,X11))|~old(X7,X11))|~event(X7,X12))|~agent(X7,X12,X11))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X10))|~in(X7,X12,X8)))|old(skolem0006,skolem0010)))&((~actual_world(X7)|(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~street(X7,X10))|~lonely(X7,X10))|~chevy(X7,X11))|~white(X7,X11))|~dirty(X7,X11))|~old(X7,X11))|~event(X7,X12))|~agent(X7,X12,X11))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X10))|~in(X7,X12,X8)))|event(skolem0006,skolem0011)))&((~actual_world(X7)|(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~street(X7,X10))|~lonely(X7,X10))|~chevy(X7,X11))|~white(X7,X11))|~dirty(X7,X11))|~old(X7,X11))|~event(X7,X12))|~agent(X7,X12,X11))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X10))|~in(X7,X12,X8)))|agent(skolem0006,skolem0011,skolem0010)))&((~actual_world(X7)|(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~street(X7,X10))|~lonely(X7,X10))|~chevy(X7,X11))|~white(X7,X11))|~dirty(X7,X11))|~old(X7,X11))|~event(X7,X12))|~agent(X7,X12,X11))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X10))|~in(X7,X12,X8)))|present(skolem0006,skolem0011)))&((~actual_world(X7)|(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~street(X7,X10))|~lonely(X7,X10))|~chevy(X7,X11))|~white(X7,X11))|~dirty(X7,X11))|~old(X7,X11))|~event(X7,X12))|~agent(X7,X12,X11))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X10))|~in(X7,X12,X8)))|barrel(skolem0006,skolem0011)))&((~actual_world(X7)|(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~street(X7,X10))|~lonely(X7,X10))|~chevy(X7,X11))|~white(X7,X11))|~dirty(X7,X11))|~old(X7,X11))|~event(X7,X12))|~agent(X7,X12,X11))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X10))|~in(X7,X12,X8)))|down(skolem0006,skolem0011,skolem0009)))&((~actual_world(X7)|(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~street(X7,X10))|~lonely(X7,X10))|~chevy(X7,X11))|~white(X7,X11))|~dirty(X7,X11))|~old(X7,X11))|~event(X7,X12))|~agent(X7,X12,X11))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X10))|~in(X7,X12,X8)))|in(skolem0006,skolem0011,skolem0007))))&((~actual_world(X7)|(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~street(X7,X10))|~lonely(X7,X10))|~chevy(X7,X11))|~white(X7,X11))|~dirty(X7,X11))|~old(X7,X11))|~event(X7,X12))|~agent(X7,X12,X11))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X10))|~in(X7,X12,X8)))|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21))))))))))))))))),inference(distribute,[status(thm)],[c4])).
% 6.96/7.13 cnf(c18,negated_conjecture,actual_world(skolem0001)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c54,negated_conjecture,city(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c72,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c90,negated_conjecture,placename(skolem0001,skolem0002)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c180,negated_conjecture,street(skolem0001,skolem0004)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c198,negated_conjecture,lonely(skolem0001,skolem0004)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c108,negated_conjecture,chevy(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c126,negated_conjecture,white(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c144,negated_conjecture,dirty(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c162,negated_conjecture,old(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c216,negated_conjecture,event(skolem0001,skolem0005)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c252,negated_conjecture,present(skolem0001,skolem0005)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c270,negated_conjecture,barrel(skolem0001,skolem0005)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c36,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c234,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c288,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c306,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c324,negated_conjecture,~actual_world(X195)|~of(X195,X196,X198)|~city(X195,X198)|~hollywood_placename(X195,X196)|~placename(X195,X196)|~street(X195,X193)|~lonely(X195,X193)|~chevy(X195,X197)|~white(X195,X197)|~dirty(X195,X197)|~old(X195,X197)|~event(X195,X194)|~agent(X195,X194,X197)|~present(X195,X194)|~barrel(X195,X194)|~down(X195,X194,X193)|~in(X195,X194,X198)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c1408,plain,~actual_world(skolem0001)|~of(skolem0001,X1548,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1548)|~placename(skolem0001,X1548)|~street(skolem0001,X1546)|~lonely(skolem0001,X1546)|~chevy(skolem0001,X1547)|~white(skolem0001,X1547)|~dirty(skolem0001,X1547)|~old(skolem0001,X1547)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1547)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X1546)|agent(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c324, c306])).
% 6.96/7.13 cnf(c4164,plain,~actual_world(skolem0001)|~of(skolem0001,X1549,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1549)|~placename(skolem0001,X1549)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,X1550)|~white(skolem0001,X1550)|~dirty(skolem0001,X1550)|~old(skolem0001,X1550)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1550)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|agent(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c1408, c288])).
% 6.96/7.13 cnf(c4167,plain,~actual_world(skolem0001)|~of(skolem0001,X1551,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1551)|~placename(skolem0001,X1551)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|agent(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c4164, c234])).
% 6.96/7.13 cnf(c4168,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|agent(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c4167, c36])).
% 6.96/7.13 cnf(c4171,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|agent(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c4168, c270])).
% 6.96/7.13 cnf(c4176,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|agent(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c4171, c252])).
% 6.96/7.13 cnf(c4178,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c4176, c216])).
% 6.96/7.13 cnf(c4182,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c4178, c162])).
% 6.96/7.13 cnf(c4184,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c4182, c144])).
% 6.96/7.13 cnf(c4186,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c4184, c126])).
% 6.96/7.13 cnf(c4189,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|agent(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c4186, c108])).
% 6.96/7.13 cnf(c4192,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|agent(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c4189, c198])).
% 6.96/7.13 cnf(c4195,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|agent(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c4192, c180])).
% 6.96/7.13 cnf(c4199,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|agent(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c4195, c90])).
% 6.96/7.13 cnf(c4201,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c4199, c72])).
% 6.96/7.13 cnf(c4204,plain,~actual_world(skolem0001)|agent(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c4201, c54])).
% 6.96/7.13 cnf(c4209,plain,agent(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c4204, c18])).
% 6.96/7.13 cnf(c329,negated_conjecture,~actual_world(X214)|~of(X214,X215,X221)|~city(X214,X221)|~hollywood_placename(X214,X215)|~placename(X214,X215)|~street(X214,X212)|~lonely(X214,X212)|~chevy(X214,X216)|~white(X214,X216)|~dirty(X214,X216)|~old(X214,X216)|~event(X214,X213)|~agent(X214,X213,X216)|~present(X214,X213)|~barrel(X214,X213)|~down(X214,X213,X212)|~in(X214,X213,X221)|~actual_world(X219)|~of(X219,X217,X211)|~city(X219,X211)|~hollywood_placename(X219,X217)|~placename(X219,X217)|~chevy(X219,X211)|~white(X219,X211)|~dirty(X219,X211)|~old(X219,X211)|~street(X219,X220)|~lonely(X219,X220)|~event(X219,X218)|~agent(X219,X218,X211)|~present(X219,X218)|~barrel(X219,X218)|~down(X219,X218,X220)|~in(X219,X218,X211),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c1486,plain,~actual_world(X3882)|~of(X3882,X3884,X3881)|~city(X3882,X3881)|~hollywood_placename(X3882,X3884)|~placename(X3882,X3884)|~street(X3882,X3878)|~lonely(X3882,X3878)|~chevy(X3882,X3880)|~white(X3882,X3880)|~dirty(X3882,X3880)|~old(X3882,X3880)|~event(X3882,X3883)|~agent(X3882,X3883,X3880)|~present(X3882,X3883)|~barrel(X3882,X3883)|~down(X3882,X3883,X3878)|~in(X3882,X3883,X3881)|~of(X3882,X3877,X3881)|~hollywood_placename(X3882,X3877)|~placename(X3882,X3877)|~chevy(X3882,X3881)|~white(X3882,X3881)|~dirty(X3882,X3881)|~old(X3882,X3881)|~street(X3882,X3879)|~lonely(X3882,X3879)|~agent(X3882,X3883,X3881)|~down(X3882,X3883,X3879),inference(factor,[status(thm)],[c329])).
% 6.96/7.13 cnf(c4294,plain,~actual_world(X3901)|~of(X3901,X3906,X3904)|~city(X3901,X3904)|~hollywood_placename(X3901,X3906)|~placename(X3901,X3906)|~street(X3901,X3905)|~lonely(X3901,X3905)|~chevy(X3901,X3902)|~white(X3901,X3902)|~dirty(X3901,X3902)|~old(X3901,X3902)|~event(X3901,X3903)|~agent(X3901,X3903,X3902)|~present(X3901,X3903)|~barrel(X3901,X3903)|~down(X3901,X3903,X3905)|~in(X3901,X3903,X3904)|~of(X3901,X3900,X3904)|~hollywood_placename(X3901,X3900)|~placename(X3901,X3900)|~chevy(X3901,X3904)|~white(X3901,X3904)|~dirty(X3901,X3904)|~old(X3901,X3904)|~agent(X3901,X3903,X3904),inference(factor,[status(thm)],[c1486])).
% 6.96/7.13 cnf(c4297,plain,~actual_world(skolem0006)|~of(skolem0006,X4008,skolem0010)|~city(skolem0006,skolem0010)|~hollywood_placename(skolem0006,X4008)|~placename(skolem0006,X4008)|~street(skolem0006,X4011)|~lonely(skolem0006,X4011)|~chevy(skolem0006,X4009)|~white(skolem0006,X4009)|~dirty(skolem0006,X4009)|~old(skolem0006,X4009)|~event(skolem0006,skolem0011)|~agent(skolem0006,skolem0011,X4009)|~present(skolem0006,skolem0011)|~barrel(skolem0006,skolem0011)|~down(skolem0006,skolem0011,X4011)|~in(skolem0006,skolem0011,skolem0010)|~of(skolem0006,X4010,skolem0010)|~hollywood_placename(skolem0006,X4010)|~placename(skolem0006,X4010)|~chevy(skolem0006,skolem0010)|~white(skolem0006,skolem0010)|~dirty(skolem0006,skolem0010)|~old(skolem0006,skolem0010),inference(resolution,[status(thm)],[c4294, c4209])).
% 6.96/7.13 cnf(c4302,plain,~actual_world(skolem0006)|~of(skolem0006,X4013,skolem0010)|~city(skolem0006,skolem0010)|~hollywood_placename(skolem0006,X4013)|~placename(skolem0006,X4013)|~street(skolem0006,X4012)|~lonely(skolem0006,X4012)|~chevy(skolem0006,X4014)|~white(skolem0006,X4014)|~dirty(skolem0006,X4014)|~old(skolem0006,X4014)|~event(skolem0006,skolem0011)|~agent(skolem0006,skolem0011,X4014)|~present(skolem0006,skolem0011)|~barrel(skolem0006,skolem0011)|~down(skolem0006,skolem0011,X4012)|~in(skolem0006,skolem0011,skolem0010)|~chevy(skolem0006,skolem0010)|~white(skolem0006,skolem0010)|~dirty(skolem0006,skolem0010)|~old(skolem0006,skolem0010),inference(factor,[status(thm)],[c4297])).
% 6.96/7.13 cnf(c21,negated_conjecture,actual_world(skolem0001)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c57,negated_conjecture,city(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c75,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c93,negated_conjecture,placename(skolem0001,skolem0002)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c183,negated_conjecture,street(skolem0001,skolem0004)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c201,negated_conjecture,lonely(skolem0001,skolem0004)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c111,negated_conjecture,chevy(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c129,negated_conjecture,white(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c147,negated_conjecture,dirty(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c165,negated_conjecture,old(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c219,negated_conjecture,event(skolem0001,skolem0005)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c255,negated_conjecture,present(skolem0001,skolem0005)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c273,negated_conjecture,barrel(skolem0001,skolem0005)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c39,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c237,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c291,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c309,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c327,negated_conjecture,~actual_world(X201)|~of(X201,X202,X204)|~city(X201,X204)|~hollywood_placename(X201,X202)|~placename(X201,X202)|~street(X201,X199)|~lonely(X201,X199)|~chevy(X201,X203)|~white(X201,X203)|~dirty(X201,X203)|~old(X201,X203)|~event(X201,X200)|~agent(X201,X200,X203)|~present(X201,X200)|~barrel(X201,X200)|~down(X201,X200,X199)|~in(X201,X200,X204)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c1436,plain,~actual_world(skolem0001)|~of(skolem0001,X1572,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1572)|~placename(skolem0001,X1572)|~street(skolem0001,X1571)|~lonely(skolem0001,X1571)|~chevy(skolem0001,X1570)|~white(skolem0001,X1570)|~dirty(skolem0001,X1570)|~old(skolem0001,X1570)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1570)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X1571)|down(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c327, c309])).
% 6.96/7.13 cnf(c4210,plain,~actual_world(skolem0001)|~of(skolem0001,X1573,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1573)|~placename(skolem0001,X1573)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,X1574)|~white(skolem0001,X1574)|~dirty(skolem0001,X1574)|~old(skolem0001,X1574)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1574)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|down(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c1436, c291])).
% 6.96/7.13 cnf(c4212,plain,~actual_world(skolem0001)|~of(skolem0001,X1575,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1575)|~placename(skolem0001,X1575)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|down(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c4210, c237])).
% 6.96/7.13 cnf(c4215,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|down(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c4212, c39])).
% 6.96/7.13 cnf(c4217,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|down(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c4215, c273])).
% 6.96/7.13 cnf(c4219,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|down(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c4217, c255])).
% 6.96/7.13 cnf(c4221,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c4219, c219])).
% 6.96/7.13 cnf(c4223,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c4221, c165])).
% 6.96/7.13 cnf(c4224,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c4223, c147])).
% 6.96/7.13 cnf(c4227,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c4224, c129])).
% 6.96/7.13 cnf(c4229,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|down(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c4227, c111])).
% 6.96/7.13 cnf(c4231,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|down(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c4229, c201])).
% 6.96/7.13 cnf(c4233,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|down(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c4231, c183])).
% 6.96/7.13 cnf(c4235,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|down(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c4233, c93])).
% 6.96/7.13 cnf(c4236,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c4235, c75])).
% 6.96/7.13 cnf(c4239,plain,~actual_world(skolem0001)|down(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c4236, c57])).
% 6.96/7.13 cnf(c4241,plain,down(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c4239, c21])).
% 6.96/7.13 cnf(c22,negated_conjecture,actual_world(skolem0001)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c58,negated_conjecture,city(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c76,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c94,negated_conjecture,placename(skolem0001,skolem0002)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c184,negated_conjecture,street(skolem0001,skolem0004)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c202,negated_conjecture,lonely(skolem0001,skolem0004)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c112,negated_conjecture,chevy(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c130,negated_conjecture,white(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c148,negated_conjecture,dirty(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c166,negated_conjecture,old(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c220,negated_conjecture,event(skolem0001,skolem0005)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c256,negated_conjecture,present(skolem0001,skolem0005)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c274,negated_conjecture,barrel(skolem0001,skolem0005)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c40,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c238,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c292,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c310,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c328,negated_conjecture,~actual_world(X207)|~of(X207,X208,X210)|~city(X207,X210)|~hollywood_placename(X207,X208)|~placename(X207,X208)|~street(X207,X205)|~lonely(X207,X205)|~chevy(X207,X209)|~white(X207,X209)|~dirty(X207,X209)|~old(X207,X209)|~event(X207,X206)|~agent(X207,X206,X209)|~present(X207,X206)|~barrel(X207,X206)|~down(X207,X206,X205)|~in(X207,X206,X210)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.96/7.13 cnf(c1463,plain,~actual_world(skolem0001)|~of(skolem0001,X1608,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1608)|~placename(skolem0001,X1608)|~street(skolem0001,X1607)|~lonely(skolem0001,X1607)|~chevy(skolem0001,X1609)|~white(skolem0001,X1609)|~dirty(skolem0001,X1609)|~old(skolem0001,X1609)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1609)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X1607)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c328, c310])).
% 6.98/7.13 cnf(c4257,plain,~actual_world(skolem0001)|~of(skolem0001,X1610,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1610)|~placename(skolem0001,X1610)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,X1611)|~white(skolem0001,X1611)|~dirty(skolem0001,X1611)|~old(skolem0001,X1611)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1611)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c1463, c292])).
% 6.98/7.13 cnf(c4258,plain,~actual_world(skolem0001)|~of(skolem0001,X1612,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1612)|~placename(skolem0001,X1612)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c4257, c238])).
% 6.98/7.13 cnf(c4259,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c4258, c40])).
% 6.98/7.13 cnf(c4260,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c4259, c274])).
% 6.98/7.13 cnf(c4261,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c4260, c256])).
% 6.98/7.13 cnf(c4262,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c4261, c220])).
% 6.98/7.13 cnf(c4263,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c4262, c166])).
% 6.98/7.13 cnf(c4264,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c4263, c148])).
% 6.98/7.13 cnf(c4265,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c4264, c130])).
% 6.98/7.13 cnf(c4266,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c4265, c112])).
% 6.98/7.13 cnf(c4267,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c4266, c202])).
% 6.98/7.13 cnf(c4268,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c4267, c184])).
% 6.98/7.13 cnf(c4269,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c4268, c94])).
% 6.98/7.13 cnf(c4270,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c4269, c76])).
% 6.98/7.13 cnf(c4271,plain,~actual_world(skolem0001)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c4270, c58])).
% 6.98/7.13 cnf(c4272,plain,in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c4271, c22])).
% 6.98/7.13 cnf(c4296,plain,~actual_world(X3911)|~of(X3911,X3912,X3908)|~city(X3911,X3908)|~hollywood_placename(X3911,X3912)|~placename(X3911,X3912)|~street(X3911,X3907)|~lonely(X3911,X3907)|~chevy(X3911,X3908)|~white(X3911,X3908)|~dirty(X3911,X3908)|~old(X3911,X3908)|~event(X3911,X3910)|~agent(X3911,X3910,X3908)|~present(X3911,X3910)|~barrel(X3911,X3910)|~down(X3911,X3910,X3907)|~in(X3911,X3910,X3908)|~of(X3911,X3909,X3908)|~hollywood_placename(X3911,X3909)|~placename(X3911,X3909),inference(factor,[status(thm)],[c4294])).
% 6.98/7.13 cnf(c4298,plain,~actual_world(X3913)|~of(X3913,X3916,X3917)|~city(X3913,X3917)|~hollywood_placename(X3913,X3916)|~placename(X3913,X3916)|~street(X3913,X3915)|~lonely(X3913,X3915)|~chevy(X3913,X3917)|~white(X3913,X3917)|~dirty(X3913,X3917)|~old(X3913,X3917)|~event(X3913,X3914)|~agent(X3913,X3914,X3917)|~present(X3913,X3914)|~barrel(X3913,X3914)|~down(X3913,X3914,X3915)|~in(X3913,X3914,X3917),inference(factor,[status(thm)],[c4296])).
% 6.98/7.13 cnf(c4300,plain,~actual_world(skolem0006)|~of(skolem0006,X3927,skolem0007)|~city(skolem0006,skolem0007)|~hollywood_placename(skolem0006,X3927)|~placename(skolem0006,X3927)|~street(skolem0006,X3926)|~lonely(skolem0006,X3926)|~chevy(skolem0006,skolem0007)|~white(skolem0006,skolem0007)|~dirty(skolem0006,skolem0007)|~old(skolem0006,skolem0007)|~event(skolem0006,skolem0011)|~agent(skolem0006,skolem0011,skolem0007)|~present(skolem0006,skolem0011)|~barrel(skolem0006,skolem0011)|~down(skolem0006,skolem0011,X3926),inference(resolution,[status(thm)],[c4298, c4272])).
% 6.98/7.13 cnf(c4301,plain,~actual_world(skolem0006)|~of(skolem0006,X3928,skolem0007)|~city(skolem0006,skolem0007)|~hollywood_placename(skolem0006,X3928)|~placename(skolem0006,X3928)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,skolem0007)|~white(skolem0006,skolem0007)|~dirty(skolem0006,skolem0007)|~old(skolem0006,skolem0007)|~event(skolem0006,skolem0011)|~agent(skolem0006,skolem0011,skolem0007)|~present(skolem0006,skolem0011)|~barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4300, c4241])).
% 6.98/7.13 cnf(c7,negated_conjecture,actual_world(skolem0001)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.13 cnf(c43,negated_conjecture,city(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.13 cnf(c61,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.13 cnf(c79,negated_conjecture,placename(skolem0001,skolem0002)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.13 cnf(c169,negated_conjecture,street(skolem0001,skolem0004)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.13 cnf(c187,negated_conjecture,lonely(skolem0001,skolem0004)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.13 cnf(c97,negated_conjecture,chevy(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.13 cnf(c115,negated_conjecture,white(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.13 cnf(c133,negated_conjecture,dirty(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.13 cnf(c151,negated_conjecture,old(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.13 cnf(c205,negated_conjecture,event(skolem0001,skolem0005)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.13 cnf(c241,negated_conjecture,present(skolem0001,skolem0005)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.13 cnf(c259,negated_conjecture,barrel(skolem0001,skolem0005)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.13 cnf(c25,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.13 cnf(c223,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.13 cnf(c277,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.13 cnf(c295,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.13 cnf(c313,negated_conjecture,~actual_world(X177)|~of(X177,X178,X180)|~city(X177,X180)|~hollywood_placename(X177,X178)|~placename(X177,X178)|~street(X177,X175)|~lonely(X177,X175)|~chevy(X177,X179)|~white(X177,X179)|~dirty(X177,X179)|~old(X177,X179)|~event(X177,X176)|~agent(X177,X176,X179)|~present(X177,X176)|~barrel(X177,X176)|~down(X177,X176,X175)|~in(X177,X176,X180)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.13 cnf(c1286,plain,~actual_world(skolem0001)|~of(skolem0001,X1517,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1517)|~placename(skolem0001,X1517)|~street(skolem0001,X1516)|~lonely(skolem0001,X1516)|~chevy(skolem0001,X1518)|~white(skolem0001,X1518)|~dirty(skolem0001,X1518)|~old(skolem0001,X1518)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1518)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X1516)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c313, c295])).
% 6.98/7.13 cnf(c4101,plain,~actual_world(skolem0001)|~of(skolem0001,X1520,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1520)|~placename(skolem0001,X1520)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,X1519)|~white(skolem0001,X1519)|~dirty(skolem0001,X1519)|~old(skolem0001,X1519)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1519)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c1286, c277])).
% 6.98/7.13 cnf(c4105,plain,~actual_world(skolem0001)|~of(skolem0001,X1521,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1521)|~placename(skolem0001,X1521)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c4101, c223])).
% 6.98/7.13 cnf(c4107,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c4105, c25])).
% 6.98/7.13 cnf(c4111,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c4107, c259])).
% 6.98/7.13 cnf(c4114,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c4111, c241])).
% 6.98/7.13 cnf(c4118,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c4114, c205])).
% 6.98/7.13 cnf(c4123,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c4118, c151])).
% 6.98/7.13 cnf(c4126,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c4123, c133])).
% 6.98/7.13 cnf(c4130,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c4126, c115])).
% 6.98/7.13 cnf(c4135,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c4130, c97])).
% 6.98/7.13 cnf(c4140,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c4135, c187])).
% 6.98/7.13 cnf(c4143,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c4140, c169])).
% 6.98/7.13 cnf(c4148,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c4143, c79])).
% 6.98/7.13 cnf(c4151,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c4148, c61])).
% 6.98/7.13 cnf(c4157,plain,~actual_world(skolem0001)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c4151, c43])).
% 6.98/7.13 cnf(c4158,plain,of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c4157, c7])).
% 6.98/7.13 cnf(c20,negated_conjecture,actual_world(skolem0001)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c56,negated_conjecture,city(skolem0001,skolem0003)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c74,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c92,negated_conjecture,placename(skolem0001,skolem0002)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c182,negated_conjecture,street(skolem0001,skolem0004)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c200,negated_conjecture,lonely(skolem0001,skolem0004)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c110,negated_conjecture,chevy(skolem0001,skolem0003)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c128,negated_conjecture,white(skolem0001,skolem0003)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c146,negated_conjecture,dirty(skolem0001,skolem0003)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c164,negated_conjecture,old(skolem0001,skolem0003)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c218,negated_conjecture,event(skolem0001,skolem0005)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c254,negated_conjecture,present(skolem0001,skolem0005)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c272,negated_conjecture,barrel(skolem0001,skolem0005)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c38,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c236,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c290,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c308,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c326,negated_conjecture,~actual_world(X189)|~of(X189,X190,X192)|~city(X189,X192)|~hollywood_placename(X189,X190)|~placename(X189,X190)|~street(X189,X187)|~lonely(X189,X187)|~chevy(X189,X191)|~white(X189,X191)|~dirty(X189,X191)|~old(X189,X191)|~event(X189,X188)|~agent(X189,X188,X191)|~present(X189,X188)|~barrel(X189,X188)|~down(X189,X188,X187)|~in(X189,X188,X192)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c1366,plain,~actual_world(skolem0001)|~of(skolem0001,X1227,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1227)|~placename(skolem0001,X1227)|~street(skolem0001,X1226)|~lonely(skolem0001,X1226)|~chevy(skolem0001,X1225)|~white(skolem0001,X1225)|~dirty(skolem0001,X1225)|~old(skolem0001,X1225)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1225)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X1226)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c326, c308])).
% 6.98/7.14 cnf(c4018,plain,~actual_world(skolem0001)|~of(skolem0001,X1228,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1228)|~placename(skolem0001,X1228)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,X1229)|~white(skolem0001,X1229)|~dirty(skolem0001,X1229)|~old(skolem0001,X1229)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1229)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c1366, c290])).
% 6.98/7.14 cnf(c4024,plain,~actual_world(skolem0001)|~of(skolem0001,X1232,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1232)|~placename(skolem0001,X1232)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4018, c236])).
% 6.98/7.14 cnf(c4031,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4024, c38])).
% 6.98/7.14 cnf(c4035,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4031, c272])).
% 6.98/7.14 cnf(c4040,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4035, c254])).
% 6.98/7.14 cnf(c4043,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4040, c218])).
% 6.98/7.14 cnf(c4048,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4043, c164])).
% 6.98/7.14 cnf(c4054,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4048, c146])).
% 6.98/7.14 cnf(c4061,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4054, c128])).
% 6.98/7.14 cnf(c4065,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4061, c110])).
% 6.98/7.14 cnf(c4072,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4065, c200])).
% 6.98/7.14 cnf(c4077,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4072, c182])).
% 6.98/7.14 cnf(c4079,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4077, c92])).
% 6.98/7.14 cnf(c4085,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4079, c74])).
% 6.98/7.14 cnf(c4092,plain,~actual_world(skolem0001)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4085, c56])).
% 6.98/7.14 cnf(c4095,plain,barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4092, c20])).
% 6.98/7.14 cnf(c19,negated_conjecture,actual_world(skolem0001)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c55,negated_conjecture,city(skolem0001,skolem0003)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c73,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c91,negated_conjecture,placename(skolem0001,skolem0002)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c181,negated_conjecture,street(skolem0001,skolem0004)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c199,negated_conjecture,lonely(skolem0001,skolem0004)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c109,negated_conjecture,chevy(skolem0001,skolem0003)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c127,negated_conjecture,white(skolem0001,skolem0003)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c145,negated_conjecture,dirty(skolem0001,skolem0003)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c163,negated_conjecture,old(skolem0001,skolem0003)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c217,negated_conjecture,event(skolem0001,skolem0005)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c253,negated_conjecture,present(skolem0001,skolem0005)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c271,negated_conjecture,barrel(skolem0001,skolem0005)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c37,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c235,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c289,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c307,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c325,negated_conjecture,~actual_world(X183)|~of(X183,X184,X186)|~city(X183,X186)|~hollywood_placename(X183,X184)|~placename(X183,X184)|~street(X183,X181)|~lonely(X183,X181)|~chevy(X183,X185)|~white(X183,X185)|~dirty(X183,X185)|~old(X183,X185)|~event(X183,X182)|~agent(X183,X182,X185)|~present(X183,X182)|~barrel(X183,X182)|~down(X183,X182,X181)|~in(X183,X182,X186)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c1342,plain,~actual_world(skolem0001)|~of(skolem0001,X1184,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1184)|~placename(skolem0001,X1184)|~street(skolem0001,X1185)|~lonely(skolem0001,X1185)|~chevy(skolem0001,X1186)|~white(skolem0001,X1186)|~dirty(skolem0001,X1186)|~old(skolem0001,X1186)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1186)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X1185)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c325, c307])).
% 6.98/7.14 cnf(c3925,plain,~actual_world(skolem0001)|~of(skolem0001,X1188,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1188)|~placename(skolem0001,X1188)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,X1187)|~white(skolem0001,X1187)|~dirty(skolem0001,X1187)|~old(skolem0001,X1187)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1187)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c1342, c289])).
% 6.98/7.14 cnf(c3930,plain,~actual_world(skolem0001)|~of(skolem0001,X1189,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1189)|~placename(skolem0001,X1189)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3925, c235])).
% 6.98/7.14 cnf(c3938,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3930, c37])).
% 6.98/7.14 cnf(c3943,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3938, c271])).
% 6.98/7.14 cnf(c3947,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3943, c253])).
% 6.98/7.14 cnf(c3954,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3947, c217])).
% 6.98/7.14 cnf(c3958,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3954, c163])).
% 6.98/7.14 cnf(c3965,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3958, c145])).
% 6.98/7.14 cnf(c3970,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3965, c127])).
% 6.98/7.14 cnf(c3976,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3970, c109])).
% 6.98/7.14 cnf(c3982,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3976, c199])).
% 6.98/7.14 cnf(c3992,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3982, c181])).
% 6.98/7.14 cnf(c3995,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3992, c91])).
% 6.98/7.14 cnf(c4001,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3995, c73])).
% 6.98/7.14 cnf(c4010,plain,~actual_world(skolem0001)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4001, c55])).
% 6.98/7.14 cnf(c4014,plain,present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4010, c19])).
% 6.98/7.14 cnf(c17,negated_conjecture,actual_world(skolem0001)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c53,negated_conjecture,city(skolem0001,skolem0003)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c71,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c89,negated_conjecture,placename(skolem0001,skolem0002)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c179,negated_conjecture,street(skolem0001,skolem0004)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c197,negated_conjecture,lonely(skolem0001,skolem0004)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c107,negated_conjecture,chevy(skolem0001,skolem0003)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c125,negated_conjecture,white(skolem0001,skolem0003)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c143,negated_conjecture,dirty(skolem0001,skolem0003)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c161,negated_conjecture,old(skolem0001,skolem0003)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c215,negated_conjecture,event(skolem0001,skolem0005)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c251,negated_conjecture,present(skolem0001,skolem0005)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c269,negated_conjecture,barrel(skolem0001,skolem0005)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c35,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c233,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c287,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c305,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c323,negated_conjecture,~actual_world(X171)|~of(X171,X172,X174)|~city(X171,X174)|~hollywood_placename(X171,X172)|~placename(X171,X172)|~street(X171,X169)|~lonely(X171,X169)|~chevy(X171,X173)|~white(X171,X173)|~dirty(X171,X173)|~old(X171,X173)|~event(X171,X170)|~agent(X171,X170,X173)|~present(X171,X170)|~barrel(X171,X170)|~down(X171,X170,X169)|~in(X171,X170,X174)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c1276,plain,~actual_world(skolem0001)|~of(skolem0001,X1135,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1135)|~placename(skolem0001,X1135)|~street(skolem0001,X1134)|~lonely(skolem0001,X1134)|~chevy(skolem0001,X1136)|~white(skolem0001,X1136)|~dirty(skolem0001,X1136)|~old(skolem0001,X1136)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1136)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X1134)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c323, c305])).
% 6.98/7.14 cnf(c3799,plain,~actual_world(skolem0001)|~of(skolem0001,X1138,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1138)|~placename(skolem0001,X1138)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,X1137)|~white(skolem0001,X1137)|~dirty(skolem0001,X1137)|~old(skolem0001,X1137)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1137)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c1276, c287])).
% 6.98/7.14 cnf(c3803,plain,~actual_world(skolem0001)|~of(skolem0001,X1139,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1139)|~placename(skolem0001,X1139)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3799, c233])).
% 6.98/7.14 cnf(c3808,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3803, c35])).
% 6.98/7.14 cnf(c3817,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3808, c269])).
% 6.98/7.14 cnf(c3824,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3817, c251])).
% 6.98/7.14 cnf(c3829,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3824, c215])).
% 6.98/7.14 cnf(c3835,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3829, c161])).
% 6.98/7.14 cnf(c3843,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3835, c143])).
% 6.98/7.14 cnf(c3851,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3843, c125])).
% 6.98/7.14 cnf(c3858,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3851, c107])).
% 6.98/7.14 cnf(c3867,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3858, c197])).
% 6.98/7.14 cnf(c3871,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3867, c179])).
% 6.98/7.14 cnf(c3881,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3871, c89])).
% 6.98/7.14 cnf(c3886,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3881, c71])).
% 6.98/7.14 cnf(c3895,plain,~actual_world(skolem0001)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3886, c53])).
% 6.98/7.14 cnf(c3901,plain,event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3895, c17])).
% 6.98/7.14 cnf(c16,negated_conjecture,actual_world(skolem0001)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c52,negated_conjecture,city(skolem0001,skolem0003)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c70,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c88,negated_conjecture,placename(skolem0001,skolem0002)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c178,negated_conjecture,street(skolem0001,skolem0004)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c196,negated_conjecture,lonely(skolem0001,skolem0004)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c106,negated_conjecture,chevy(skolem0001,skolem0003)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c124,negated_conjecture,white(skolem0001,skolem0003)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c142,negated_conjecture,dirty(skolem0001,skolem0003)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c160,negated_conjecture,old(skolem0001,skolem0003)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c214,negated_conjecture,event(skolem0001,skolem0005)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c250,negated_conjecture,present(skolem0001,skolem0005)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c268,negated_conjecture,barrel(skolem0001,skolem0005)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c34,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c232,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c286,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c304,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c322,negated_conjecture,~actual_world(X165)|~of(X165,X166,X168)|~city(X165,X168)|~hollywood_placename(X165,X166)|~placename(X165,X166)|~street(X165,X163)|~lonely(X165,X163)|~chevy(X165,X167)|~white(X165,X167)|~dirty(X165,X167)|~old(X165,X167)|~event(X165,X164)|~agent(X165,X164,X167)|~present(X165,X164)|~barrel(X165,X164)|~down(X165,X164,X163)|~in(X165,X164,X168)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c1215,plain,~actual_world(skolem0001)|~of(skolem0001,X1078,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1078)|~placename(skolem0001,X1078)|~street(skolem0001,X1079)|~lonely(skolem0001,X1079)|~chevy(skolem0001,X1077)|~white(skolem0001,X1077)|~dirty(skolem0001,X1077)|~old(skolem0001,X1077)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1077)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X1079)|old(skolem0006,skolem0010),inference(resolution,[status(thm)],[c322, c304])).
% 6.98/7.14 cnf(c3665,plain,~actual_world(skolem0001)|~of(skolem0001,X1083,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1083)|~placename(skolem0001,X1083)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,X1082)|~white(skolem0001,X1082)|~dirty(skolem0001,X1082)|~old(skolem0001,X1082)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1082)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|old(skolem0006,skolem0010),inference(resolution,[status(thm)],[c1215, c286])).
% 6.98/7.14 cnf(c3673,plain,~actual_world(skolem0001)|~of(skolem0001,X1084,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1084)|~placename(skolem0001,X1084)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|old(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3665, c232])).
% 6.98/7.14 cnf(c3685,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|old(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3673, c34])).
% 6.98/7.14 cnf(c3691,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|old(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3685, c268])).
% 6.98/7.14 cnf(c3702,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|old(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3691, c250])).
% 6.98/7.14 cnf(c3707,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|old(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3702, c214])).
% 6.98/7.14 cnf(c3713,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|old(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3707, c160])).
% 6.98/7.14 cnf(c3727,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|old(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3713, c142])).
% 6.98/7.14 cnf(c3732,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|old(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3727, c124])).
% 6.98/7.14 cnf(c3744,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|old(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3732, c106])).
% 6.98/7.14 cnf(c3748,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|old(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3744, c196])).
% 6.98/7.14 cnf(c3759,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|old(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3748, c178])).
% 6.98/7.14 cnf(c3763,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|old(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3759, c88])).
% 6.98/7.14 cnf(c3770,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|old(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3763, c70])).
% 6.98/7.14 cnf(c3783,plain,~actual_world(skolem0001)|old(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3770, c52])).
% 6.98/7.14 cnf(c3785,plain,old(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3783, c16])).
% 6.98/7.14 cnf(c15,negated_conjecture,actual_world(skolem0001)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c51,negated_conjecture,city(skolem0001,skolem0003)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c69,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c87,negated_conjecture,placename(skolem0001,skolem0002)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c177,negated_conjecture,street(skolem0001,skolem0004)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c195,negated_conjecture,lonely(skolem0001,skolem0004)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c105,negated_conjecture,chevy(skolem0001,skolem0003)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c123,negated_conjecture,white(skolem0001,skolem0003)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c141,negated_conjecture,dirty(skolem0001,skolem0003)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c159,negated_conjecture,old(skolem0001,skolem0003)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c213,negated_conjecture,event(skolem0001,skolem0005)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c249,negated_conjecture,present(skolem0001,skolem0005)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c267,negated_conjecture,barrel(skolem0001,skolem0005)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c33,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c231,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c285,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c303,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c321,negated_conjecture,~actual_world(X159)|~of(X159,X160,X162)|~city(X159,X162)|~hollywood_placename(X159,X160)|~placename(X159,X160)|~street(X159,X157)|~lonely(X159,X157)|~chevy(X159,X161)|~white(X159,X161)|~dirty(X159,X161)|~old(X159,X161)|~event(X159,X158)|~agent(X159,X158,X161)|~present(X159,X158)|~barrel(X159,X158)|~down(X159,X158,X157)|~in(X159,X158,X162)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c1190,plain,~actual_world(skolem0001)|~of(skolem0001,X1017,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1017)|~placename(skolem0001,X1017)|~street(skolem0001,X1016)|~lonely(skolem0001,X1016)|~chevy(skolem0001,X1015)|~white(skolem0001,X1015)|~dirty(skolem0001,X1015)|~old(skolem0001,X1015)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1015)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X1016)|dirty(skolem0006,skolem0010),inference(resolution,[status(thm)],[c321, c303])).
% 6.98/7.14 cnf(c3523,plain,~actual_world(skolem0001)|~of(skolem0001,X1018,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1018)|~placename(skolem0001,X1018)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,X1019)|~white(skolem0001,X1019)|~dirty(skolem0001,X1019)|~old(skolem0001,X1019)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1019)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|dirty(skolem0006,skolem0010),inference(resolution,[status(thm)],[c1190, c285])).
% 6.98/7.14 cnf(c3533,plain,~actual_world(skolem0001)|~of(skolem0001,X1020,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1020)|~placename(skolem0001,X1020)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|dirty(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3523, c231])).
% 6.98/7.14 cnf(c3543,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|dirty(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3533, c33])).
% 6.98/7.14 cnf(c3554,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|dirty(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3543, c267])).
% 6.98/7.14 cnf(c3564,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|dirty(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3554, c249])).
% 6.98/7.14 cnf(c3567,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|dirty(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3564, c213])).
% 6.98/7.14 cnf(c3580,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|dirty(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3567, c159])).
% 6.98/7.14 cnf(c3589,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|dirty(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3580, c141])).
% 6.98/7.14 cnf(c3596,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|dirty(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3589, c123])).
% 6.98/7.14 cnf(c3607,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|dirty(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3596, c105])).
% 6.98/7.14 cnf(c3612,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|dirty(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3607, c195])).
% 6.98/7.14 cnf(c3620,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|dirty(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3612, c177])).
% 6.98/7.14 cnf(c3634,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|dirty(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3620, c87])).
% 6.98/7.14 cnf(c3638,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|dirty(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3634, c69])).
% 6.98/7.14 cnf(c3655,plain,~actual_world(skolem0001)|dirty(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3638, c51])).
% 6.98/7.14 cnf(c3659,plain,dirty(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3655, c15])).
% 6.98/7.14 cnf(c14,negated_conjecture,actual_world(skolem0001)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c50,negated_conjecture,city(skolem0001,skolem0003)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c68,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c86,negated_conjecture,placename(skolem0001,skolem0002)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c176,negated_conjecture,street(skolem0001,skolem0004)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c194,negated_conjecture,lonely(skolem0001,skolem0004)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c104,negated_conjecture,chevy(skolem0001,skolem0003)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c122,negated_conjecture,white(skolem0001,skolem0003)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c140,negated_conjecture,dirty(skolem0001,skolem0003)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c158,negated_conjecture,old(skolem0001,skolem0003)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c212,negated_conjecture,event(skolem0001,skolem0005)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c248,negated_conjecture,present(skolem0001,skolem0005)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c266,negated_conjecture,barrel(skolem0001,skolem0005)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c32,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c230,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c284,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c302,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c320,negated_conjecture,~actual_world(X153)|~of(X153,X154,X156)|~city(X153,X156)|~hollywood_placename(X153,X154)|~placename(X153,X154)|~street(X153,X151)|~lonely(X153,X151)|~chevy(X153,X155)|~white(X153,X155)|~dirty(X153,X155)|~old(X153,X155)|~event(X153,X152)|~agent(X153,X152,X155)|~present(X153,X152)|~barrel(X153,X152)|~down(X153,X152,X151)|~in(X153,X152,X156)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c1160,plain,~actual_world(skolem0001)|~of(skolem0001,X946,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X946)|~placename(skolem0001,X946)|~street(skolem0001,X944)|~lonely(skolem0001,X944)|~chevy(skolem0001,X945)|~white(skolem0001,X945)|~dirty(skolem0001,X945)|~old(skolem0001,X945)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X945)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X944)|white(skolem0006,skolem0010),inference(resolution,[status(thm)],[c320, c302])).
% 6.98/7.14 cnf(c3361,plain,~actual_world(skolem0001)|~of(skolem0001,X947,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X947)|~placename(skolem0001,X947)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,X948)|~white(skolem0001,X948)|~dirty(skolem0001,X948)|~old(skolem0001,X948)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X948)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|white(skolem0006,skolem0010),inference(resolution,[status(thm)],[c1160, c284])).
% 6.98/7.14 cnf(c3375,plain,~actual_world(skolem0001)|~of(skolem0001,X951,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X951)|~placename(skolem0001,X951)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|white(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3361, c230])).
% 6.98/7.14 cnf(c3386,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|white(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3375, c32])).
% 6.98/7.14 cnf(c3396,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|white(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3386, c266])).
% 6.98/7.14 cnf(c3409,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|white(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3396, c248])).
% 6.98/7.14 cnf(c3412,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|white(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3409, c212])).
% 6.98/7.14 cnf(c3421,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|white(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3412, c158])).
% 6.98/7.14 cnf(c3435,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|white(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3421, c140])).
% 6.98/7.14 cnf(c3450,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|white(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3435, c122])).
% 6.98/7.14 cnf(c3453,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|white(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3450, c104])).
% 6.98/7.14 cnf(c3470,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|white(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3453, c194])).
% 6.98/7.14 cnf(c3478,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|white(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3470, c176])).
% 6.98/7.14 cnf(c3483,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|white(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3478, c86])).
% 6.98/7.14 cnf(c3498,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|white(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3483, c68])).
% 6.98/7.14 cnf(c3507,plain,~actual_world(skolem0001)|white(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3498, c50])).
% 6.98/7.14 cnf(c3511,plain,white(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3507, c14])).
% 6.98/7.14 cnf(c13,negated_conjecture,actual_world(skolem0001)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c49,negated_conjecture,city(skolem0001,skolem0003)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.14 cnf(c67,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c85,negated_conjecture,placename(skolem0001,skolem0002)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c175,negated_conjecture,street(skolem0001,skolem0004)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c193,negated_conjecture,lonely(skolem0001,skolem0004)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c103,negated_conjecture,chevy(skolem0001,skolem0003)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c121,negated_conjecture,white(skolem0001,skolem0003)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c139,negated_conjecture,dirty(skolem0001,skolem0003)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c157,negated_conjecture,old(skolem0001,skolem0003)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c211,negated_conjecture,event(skolem0001,skolem0005)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c247,negated_conjecture,present(skolem0001,skolem0005)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c265,negated_conjecture,barrel(skolem0001,skolem0005)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c31,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c229,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c283,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c301,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c319,negated_conjecture,~actual_world(X147)|~of(X147,X148,X150)|~city(X147,X150)|~hollywood_placename(X147,X148)|~placename(X147,X148)|~street(X147,X145)|~lonely(X147,X145)|~chevy(X147,X149)|~white(X147,X149)|~dirty(X147,X149)|~old(X147,X149)|~event(X147,X146)|~agent(X147,X146,X149)|~present(X147,X146)|~barrel(X147,X146)|~down(X147,X146,X145)|~in(X147,X146,X150)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c1131,plain,~actual_world(skolem0001)|~of(skolem0001,X868,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X868)|~placename(skolem0001,X868)|~street(skolem0001,X869)|~lonely(skolem0001,X869)|~chevy(skolem0001,X870)|~white(skolem0001,X870)|~dirty(skolem0001,X870)|~old(skolem0001,X870)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X870)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X869)|chevy(skolem0006,skolem0010),inference(resolution,[status(thm)],[c319, c301])).
% 6.98/7.15 cnf(c3172,plain,~actual_world(skolem0001)|~of(skolem0001,X872,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X872)|~placename(skolem0001,X872)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,X871)|~white(skolem0001,X871)|~dirty(skolem0001,X871)|~old(skolem0001,X871)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X871)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|chevy(skolem0006,skolem0010),inference(resolution,[status(thm)],[c1131, c283])).
% 6.98/7.15 cnf(c3187,plain,~actual_world(skolem0001)|~of(skolem0001,X873,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X873)|~placename(skolem0001,X873)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|chevy(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3172, c229])).
% 6.98/7.15 cnf(c3197,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|chevy(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3187, c31])).
% 6.98/7.15 cnf(c3209,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|chevy(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3197, c265])).
% 6.98/7.15 cnf(c3219,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|chevy(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3209, c247])).
% 6.98/7.15 cnf(c3227,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|chevy(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3219, c211])).
% 6.98/7.15 cnf(c3236,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|chevy(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3227, c157])).
% 6.98/7.15 cnf(c3247,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|chevy(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3236, c139])).
% 6.98/7.15 cnf(c3262,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|chevy(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3247, c121])).
% 6.98/7.15 cnf(c3273,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|chevy(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3262, c103])).
% 6.98/7.15 cnf(c3278,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|chevy(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3273, c193])).
% 6.98/7.15 cnf(c3289,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|chevy(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3278, c175])).
% 6.98/7.15 cnf(c3303,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|chevy(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3289, c85])).
% 6.98/7.15 cnf(c3320,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|chevy(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3303, c67])).
% 6.98/7.15 cnf(c3328,plain,~actual_world(skolem0001)|chevy(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3320, c49])).
% 6.98/7.15 cnf(c3333,plain,chevy(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3328, c13])).
% 6.98/7.15 cnf(c12,negated_conjecture,actual_world(skolem0001)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c48,negated_conjecture,city(skolem0001,skolem0003)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c66,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c84,negated_conjecture,placename(skolem0001,skolem0002)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c174,negated_conjecture,street(skolem0001,skolem0004)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c192,negated_conjecture,lonely(skolem0001,skolem0004)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c102,negated_conjecture,chevy(skolem0001,skolem0003)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c120,negated_conjecture,white(skolem0001,skolem0003)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c138,negated_conjecture,dirty(skolem0001,skolem0003)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c156,negated_conjecture,old(skolem0001,skolem0003)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c210,negated_conjecture,event(skolem0001,skolem0005)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c246,negated_conjecture,present(skolem0001,skolem0005)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c264,negated_conjecture,barrel(skolem0001,skolem0005)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c30,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c228,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c282,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c300,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c318,negated_conjecture,~actual_world(X136)|~of(X136,X137,X139)|~city(X136,X139)|~hollywood_placename(X136,X137)|~placename(X136,X137)|~street(X136,X134)|~lonely(X136,X134)|~chevy(X136,X138)|~white(X136,X138)|~dirty(X136,X138)|~old(X136,X138)|~event(X136,X135)|~agent(X136,X135,X138)|~present(X136,X135)|~barrel(X136,X135)|~down(X136,X135,X134)|~in(X136,X135,X139)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c1047,plain,~actual_world(skolem0001)|~of(skolem0001,X784,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X784)|~placename(skolem0001,X784)|~street(skolem0001,X783)|~lonely(skolem0001,X783)|~chevy(skolem0001,X785)|~white(skolem0001,X785)|~dirty(skolem0001,X785)|~old(skolem0001,X785)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X785)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X783)|lonely(skolem0006,skolem0009),inference(resolution,[status(thm)],[c318, c300])).
% 6.98/7.15 cnf(c2982,plain,~actual_world(skolem0001)|~of(skolem0001,X786,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X786)|~placename(skolem0001,X786)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,X787)|~white(skolem0001,X787)|~dirty(skolem0001,X787)|~old(skolem0001,X787)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X787)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|lonely(skolem0006,skolem0009),inference(resolution,[status(thm)],[c1047, c282])).
% 6.98/7.15 cnf(c2990,plain,~actual_world(skolem0001)|~of(skolem0001,X788,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X788)|~placename(skolem0001,X788)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|lonely(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2982, c228])).
% 6.98/7.15 cnf(c3008,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|lonely(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2990, c30])).
% 6.98/7.15 cnf(c3020,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|lonely(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3008, c264])).
% 6.98/7.15 cnf(c3030,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|lonely(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3020, c246])).
% 6.98/7.15 cnf(c3043,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|lonely(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3030, c210])).
% 6.98/7.15 cnf(c3048,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|lonely(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3043, c156])).
% 6.98/7.15 cnf(c3064,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|lonely(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3048, c138])).
% 6.98/7.15 cnf(c3078,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|lonely(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3064, c120])).
% 6.98/7.15 cnf(c3084,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|lonely(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3078, c102])).
% 6.98/7.15 cnf(c3103,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|lonely(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3084, c192])).
% 6.98/7.15 cnf(c3108,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|lonely(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3103, c174])).
% 6.98/7.15 cnf(c3127,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|lonely(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3108, c84])).
% 6.98/7.15 cnf(c3138,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|lonely(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3127, c66])).
% 6.98/7.15 cnf(c3148,plain,~actual_world(skolem0001)|lonely(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3138, c48])).
% 6.98/7.15 cnf(c3156,plain,lonely(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3148, c12])).
% 6.98/7.15 cnf(c11,negated_conjecture,actual_world(skolem0001)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c47,negated_conjecture,city(skolem0001,skolem0003)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c65,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c83,negated_conjecture,placename(skolem0001,skolem0002)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c173,negated_conjecture,street(skolem0001,skolem0004)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c191,negated_conjecture,lonely(skolem0001,skolem0004)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c101,negated_conjecture,chevy(skolem0001,skolem0003)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c119,negated_conjecture,white(skolem0001,skolem0003)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c137,negated_conjecture,dirty(skolem0001,skolem0003)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c155,negated_conjecture,old(skolem0001,skolem0003)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c209,negated_conjecture,event(skolem0001,skolem0005)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c245,negated_conjecture,present(skolem0001,skolem0005)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c263,negated_conjecture,barrel(skolem0001,skolem0005)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c29,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c227,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c281,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c299,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c317,negated_conjecture,~actual_world(X130)|~of(X130,X131,X133)|~city(X130,X133)|~hollywood_placename(X130,X131)|~placename(X130,X131)|~street(X130,X128)|~lonely(X130,X128)|~chevy(X130,X132)|~white(X130,X132)|~dirty(X130,X132)|~old(X130,X132)|~event(X130,X129)|~agent(X130,X129,X132)|~present(X130,X129)|~barrel(X130,X129)|~down(X130,X129,X128)|~in(X130,X129,X133)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c1035,plain,~actual_world(skolem0001)|~of(skolem0001,X693,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X693)|~placename(skolem0001,X693)|~street(skolem0001,X692)|~lonely(skolem0001,X692)|~chevy(skolem0001,X691)|~white(skolem0001,X691)|~dirty(skolem0001,X691)|~old(skolem0001,X691)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X691)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X692)|street(skolem0006,skolem0009),inference(resolution,[status(thm)],[c317, c299])).
% 6.98/7.15 cnf(c2752,plain,~actual_world(skolem0001)|~of(skolem0001,X696,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X696)|~placename(skolem0001,X696)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,X697)|~white(skolem0001,X697)|~dirty(skolem0001,X697)|~old(skolem0001,X697)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X697)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|street(skolem0006,skolem0009),inference(resolution,[status(thm)],[c1035, c281])).
% 6.98/7.15 cnf(c2771,plain,~actual_world(skolem0001)|~of(skolem0001,X698,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X698)|~placename(skolem0001,X698)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|street(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2752, c227])).
% 6.98/7.15 cnf(c2784,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|street(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2771, c29])).
% 6.98/7.15 cnf(c2798,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|street(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2784, c263])).
% 6.98/7.15 cnf(c2808,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|street(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2798, c245])).
% 6.98/7.15 cnf(c2820,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|street(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2808, c209])).
% 6.98/7.15 cnf(c2832,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|street(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2820, c155])).
% 6.98/7.15 cnf(c2851,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|street(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2832, c137])).
% 6.98/7.15 cnf(c2860,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|street(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2851, c119])).
% 6.98/7.15 cnf(c2869,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|street(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2860, c101])).
% 6.98/7.15 cnf(c2891,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|street(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2869, c191])).
% 6.98/7.15 cnf(c2898,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|street(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2891, c173])).
% 6.98/7.15 cnf(c2917,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|street(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2898, c83])).
% 6.98/7.15 cnf(c2928,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|street(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2917, c65])).
% 6.98/7.15 cnf(c2933,plain,~actual_world(skolem0001)|street(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2928, c47])).
% 6.98/7.15 cnf(c2953,plain,street(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2933, c11])).
% 6.98/7.15 cnf(c10,negated_conjecture,actual_world(skolem0001)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c46,negated_conjecture,city(skolem0001,skolem0003)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c64,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c82,negated_conjecture,placename(skolem0001,skolem0002)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c172,negated_conjecture,street(skolem0001,skolem0004)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c190,negated_conjecture,lonely(skolem0001,skolem0004)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c100,negated_conjecture,chevy(skolem0001,skolem0003)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c118,negated_conjecture,white(skolem0001,skolem0003)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c136,negated_conjecture,dirty(skolem0001,skolem0003)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c154,negated_conjecture,old(skolem0001,skolem0003)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c208,negated_conjecture,event(skolem0001,skolem0005)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c244,negated_conjecture,present(skolem0001,skolem0005)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c262,negated_conjecture,barrel(skolem0001,skolem0005)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c28,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c226,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c280,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c298,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c316,negated_conjecture,~actual_world(X124)|~of(X124,X125,X127)|~city(X124,X127)|~hollywood_placename(X124,X125)|~placename(X124,X125)|~street(X124,X122)|~lonely(X124,X122)|~chevy(X124,X126)|~white(X124,X126)|~dirty(X124,X126)|~old(X124,X126)|~event(X124,X123)|~agent(X124,X123,X126)|~present(X124,X123)|~barrel(X124,X123)|~down(X124,X123,X122)|~in(X124,X123,X127)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c999,plain,~actual_world(skolem0001)|~of(skolem0001,X594,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X594)|~placename(skolem0001,X594)|~street(skolem0001,X595)|~lonely(skolem0001,X595)|~chevy(skolem0001,X596)|~white(skolem0001,X596)|~dirty(skolem0001,X596)|~old(skolem0001,X596)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X596)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X595)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c316, c298])).
% 6.98/7.15 cnf(c2515,plain,~actual_world(skolem0001)|~of(skolem0001,X598,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X598)|~placename(skolem0001,X598)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,X597)|~white(skolem0001,X597)|~dirty(skolem0001,X597)|~old(skolem0001,X597)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X597)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c999, c280])).
% 6.98/7.15 cnf(c2532,plain,~actual_world(skolem0001)|~of(skolem0001,X599,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X599)|~placename(skolem0001,X599)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2515, c226])).
% 6.98/7.15 cnf(c2551,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2532, c28])).
% 6.98/7.15 cnf(c2559,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2551, c262])).
% 6.98/7.15 cnf(c2595,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2559, c244])).
% 6.98/7.15 cnf(c2600,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2595, c208])).
% 6.98/7.15 cnf(c2616,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2600, c154])).
% 6.98/7.15 cnf(c2634,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2616, c136])).
% 6.98/7.15 cnf(c2641,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2634, c118])).
% 6.98/7.15 cnf(c2661,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2641, c100])).
% 6.98/7.15 cnf(c2667,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2661, c190])).
% 6.98/7.15 cnf(c2681,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2667, c172])).
% 6.98/7.15 cnf(c2698,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2681, c82])).
% 6.98/7.15 cnf(c2715,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2698, c64])).
% 6.98/7.15 cnf(c2724,plain,~actual_world(skolem0001)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2715, c46])).
% 6.98/7.15 cnf(c2741,plain,placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2724, c10])).
% 6.98/7.15 cnf(c9,negated_conjecture,actual_world(skolem0001)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c45,negated_conjecture,city(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c63,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c81,negated_conjecture,placename(skolem0001,skolem0002)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c171,negated_conjecture,street(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c189,negated_conjecture,lonely(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c99,negated_conjecture,chevy(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c117,negated_conjecture,white(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c135,negated_conjecture,dirty(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c153,negated_conjecture,old(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c207,negated_conjecture,event(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c243,negated_conjecture,present(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c261,negated_conjecture,barrel(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c27,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c225,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c279,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c297,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c315,negated_conjecture,~actual_world(X118)|~of(X118,X119,X121)|~city(X118,X121)|~hollywood_placename(X118,X119)|~placename(X118,X119)|~street(X118,X116)|~lonely(X118,X116)|~chevy(X118,X120)|~white(X118,X120)|~dirty(X118,X120)|~old(X118,X120)|~event(X118,X117)|~agent(X118,X117,X120)|~present(X118,X117)|~barrel(X118,X117)|~down(X118,X117,X116)|~in(X118,X117,X121)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c963,plain,~actual_world(skolem0001)|~of(skolem0001,X490,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X490)|~placename(skolem0001,X490)|~street(skolem0001,X488)|~lonely(skolem0001,X488)|~chevy(skolem0001,X489)|~white(skolem0001,X489)|~dirty(skolem0001,X489)|~old(skolem0001,X489)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X489)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X488)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c315, c297])).
% 6.98/7.15 cnf(c2224,plain,~actual_world(skolem0001)|~of(skolem0001,X492,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X492)|~placename(skolem0001,X492)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,X491)|~white(skolem0001,X491)|~dirty(skolem0001,X491)|~old(skolem0001,X491)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X491)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c963, c279])).
% 6.98/7.15 cnf(c2247,plain,~actual_world(skolem0001)|~of(skolem0001,X495,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X495)|~placename(skolem0001,X495)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2224, c225])).
% 6.98/7.15 cnf(c2261,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2247, c27])).
% 6.98/7.15 cnf(c2275,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2261, c261])).
% 6.98/7.15 cnf(c2290,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2275, c243])).
% 6.98/7.15 cnf(c2307,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2290, c207])).
% 6.98/7.15 cnf(c2322,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2307, c153])).
% 6.98/7.15 cnf(c2328,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2322, c135])).
% 6.98/7.15 cnf(c2344,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2328, c117])).
% 6.98/7.15 cnf(c2366,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2344, c99])).
% 6.98/7.15 cnf(c2373,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2366, c189])).
% 6.98/7.15 cnf(c2389,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2373, c171])).
% 6.98/7.15 cnf(c2404,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2389, c81])).
% 6.98/7.15 cnf(c2427,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2404, c63])).
% 6.98/7.15 cnf(c2429,plain,~actual_world(skolem0001)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2427, c45])).
% 6.98/7.15 cnf(c2447,plain,hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2429, c9])).
% 6.98/7.15 cnf(c8,negated_conjecture,actual_world(skolem0001)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c44,negated_conjecture,city(skolem0001,skolem0003)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c62,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c80,negated_conjecture,placename(skolem0001,skolem0002)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c170,negated_conjecture,street(skolem0001,skolem0004)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c188,negated_conjecture,lonely(skolem0001,skolem0004)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c98,negated_conjecture,chevy(skolem0001,skolem0003)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c116,negated_conjecture,white(skolem0001,skolem0003)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c134,negated_conjecture,dirty(skolem0001,skolem0003)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c152,negated_conjecture,old(skolem0001,skolem0003)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c206,negated_conjecture,event(skolem0001,skolem0005)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c242,negated_conjecture,present(skolem0001,skolem0005)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c260,negated_conjecture,barrel(skolem0001,skolem0005)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c26,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c224,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c278,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c296,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c314,negated_conjecture,~actual_world(X112)|~of(X112,X113,X115)|~city(X112,X115)|~hollywood_placename(X112,X113)|~placename(X112,X113)|~street(X112,X110)|~lonely(X112,X110)|~chevy(X112,X114)|~white(X112,X114)|~dirty(X112,X114)|~old(X112,X114)|~event(X112,X111)|~agent(X112,X111,X114)|~present(X112,X111)|~barrel(X112,X111)|~down(X112,X111,X110)|~in(X112,X111,X115)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c940,plain,~actual_world(skolem0001)|~of(skolem0001,X378,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X378)|~placename(skolem0001,X378)|~street(skolem0001,X377)|~lonely(skolem0001,X377)|~chevy(skolem0001,X379)|~white(skolem0001,X379)|~dirty(skolem0001,X379)|~old(skolem0001,X379)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X379)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X377)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c314, c296])).
% 6.98/7.15 cnf(c1918,plain,~actual_world(skolem0001)|~of(skolem0001,X380,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X380)|~placename(skolem0001,X380)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,X381)|~white(skolem0001,X381)|~dirty(skolem0001,X381)|~old(skolem0001,X381)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X381)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c940, c278])).
% 6.98/7.15 cnf(c1933,plain,~actual_world(skolem0001)|~of(skolem0001,X382,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X382)|~placename(skolem0001,X382)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c1918, c224])).
% 6.98/7.15 cnf(c1959,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c1933, c26])).
% 6.98/7.15 cnf(c1970,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c1959, c260])).
% 6.98/7.15 cnf(c1986,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c1970, c242])).
% 6.98/7.15 cnf(c1992,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c1986, c206])).
% 6.98/7.15 cnf(c2022,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c1992, c152])).
% 6.98/7.15 cnf(c2033,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c2022, c134])).
% 6.98/7.15 cnf(c2050,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c2033, c116])).
% 6.98/7.15 cnf(c2067,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c2050, c98])).
% 6.98/7.15 cnf(c2084,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c2067, c188])).
% 6.98/7.15 cnf(c2089,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c2084, c170])).
% 6.98/7.15 cnf(c2107,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c2089, c80])).
% 6.98/7.15 cnf(c2129,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c2107, c62])).
% 6.98/7.15 cnf(c2138,plain,~actual_world(skolem0001)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c2129, c44])).
% 6.98/7.15 cnf(c2153,plain,city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c2138, c8])).
% 6.98/7.15 cnf(c6,negated_conjecture,actual_world(skolem0001)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c42,negated_conjecture,city(skolem0001,skolem0003)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c60,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c78,negated_conjecture,placename(skolem0001,skolem0002)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c168,negated_conjecture,street(skolem0001,skolem0004)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c186,negated_conjecture,lonely(skolem0001,skolem0004)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c96,negated_conjecture,chevy(skolem0001,skolem0003)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c114,negated_conjecture,white(skolem0001,skolem0003)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c132,negated_conjecture,dirty(skolem0001,skolem0003)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c150,negated_conjecture,old(skolem0001,skolem0003)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c204,negated_conjecture,event(skolem0001,skolem0005)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c240,negated_conjecture,present(skolem0001,skolem0005)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c258,negated_conjecture,barrel(skolem0001,skolem0005)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c24,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c222,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c276,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c294,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c312,negated_conjecture,~actual_world(X101)|~of(X101,X102,X104)|~city(X101,X104)|~hollywood_placename(X101,X102)|~placename(X101,X102)|~street(X101,X99)|~lonely(X101,X99)|~chevy(X101,X103)|~white(X101,X103)|~dirty(X101,X103)|~old(X101,X103)|~event(X101,X100)|~agent(X101,X100,X103)|~present(X101,X100)|~barrel(X101,X100)|~down(X101,X100,X99)|~in(X101,X100,X104)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.98/7.15 cnf(c871,plain,~actual_world(skolem0001)|~of(skolem0001,X222,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X222)|~placename(skolem0001,X222)|~street(skolem0001,X224)|~lonely(skolem0001,X224)|~chevy(skolem0001,X223)|~white(skolem0001,X223)|~dirty(skolem0001,X223)|~old(skolem0001,X223)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X223)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X224)|actual_world(skolem0006),inference(resolution,[status(thm)],[c312, c294])).
% 6.98/7.15 cnf(c1523,plain,~actual_world(skolem0001)|~of(skolem0001,X226,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X226)|~placename(skolem0001,X226)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,X225)|~white(skolem0001,X225)|~dirty(skolem0001,X225)|~old(skolem0001,X225)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X225)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|actual_world(skolem0006),inference(resolution,[status(thm)],[c871, c276])).
% 6.98/7.15 cnf(c1540,plain,~actual_world(skolem0001)|~of(skolem0001,X227,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X227)|~placename(skolem0001,X227)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1523, c222])).
% 6.98/7.15 cnf(c1559,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1540, c24])).
% 6.98/7.15 cnf(c1581,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1559, c258])).
% 6.98/7.15 cnf(c1590,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~event(skolem0001,skolem0005)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1581, c240])).
% 6.98/7.15 cnf(c1633,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1590, c204])).
% 6.98/7.15 cnf(c1653,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1633, c150])).
% 6.98/7.15 cnf(c1669,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1653, c132])).
% 6.98/7.15 cnf(c1688,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~chevy(skolem0001,skolem0003)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1669, c114])).
% 6.98/7.15 cnf(c1705,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1688, c96])).
% 6.98/7.15 cnf(c1714,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0004)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1705, c186])).
% 6.98/7.15 cnf(c1737,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1714, c168])).
% 6.98/7.15 cnf(c1757,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1737, c78])).
% 6.98/7.15 cnf(c1770,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1757, c60])).
% 6.98/7.15 cnf(c1786,plain,~actual_world(skolem0001)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1770, c42])).
% 6.98/7.15 cnf(c1803,plain,actual_world(skolem0006),inference(resolution,[status(thm)],[c1786, c6])).
% 6.98/7.15 % SZS output end Saturation
% 6.98/7.15
% 6.98/7.15 % Initial clauses : 324
% 6.98/7.15 % Processed clauses : 658
% 6.98/7.15 % Factors computed : 5
% 6.98/7.15 % Resolvents computed: 3968
% 6.98/7.15 % Tautologies deleted: 255
% 6.98/7.15 % Forward subsumed : 3384
% 6.98/7.15 % Backward subsumed : 637
% 6.98/7.15 % -------- CPU Time ---------
% 6.98/7.15 % User time : 6.803 s
% 6.98/7.15 % System time : 0.025 s
% 6.98/7.15 % Total time : 6.828 s
%------------------------------------------------------------------------------