%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP114+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n025.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:09 EDT 2024
% Result : CounterSatisfiable 6.13s 6.33s
% Output : Saturation 6.13s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : NLP114+1 : TPTP v8.1.2. Released v2.4.0.
% 0.11/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n025.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Wed May 8 13:38:53 EDT 2024
% 0.14/0.34 % CPUTime :
% 6.13/6.33 % Version: 1.5
% 6.13/6.33 % SZS status CounterSatisfiable
% 6.13/6.33 % SZS output start Saturation
% 6.13/6.33 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))&street(U,W))&lonely(U,W))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&event(U,Y))&agent(U,Y,X))&present(U,Y))&barrel(U,Y))&down(U,Y,W))&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))&street(U,W))&lonely(U,W))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&event(U,Y))&agent(U,Y,X))&present(U,Y))&barrel(U,Y))&down(U,Y,W))&in(U,Y,W)))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', co1)).
% 6.13/6.33 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))&street(U,W))&lonely(U,W))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&event(U,Y))&agent(U,Y,X))&present(U,Y))&barrel(U,Y))&down(U,Y,W))&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))&street(U,W))&lonely(U,W))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&event(U,Y))&agent(U,Y,X))&present(U,Y))&barrel(U,Y))&down(U,Y,W))&in(U,Y,W))))))))))))),inference(assume_negation,[status(cth)],[co1])).
% 6.13/6.33 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))&street(U,W))&lonely(U,W))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&event(U,Y))&agent(U,Y,X))&present(U,Y))&barrel(U,Y))&down(U,Y,W))&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))|~street(U,W))|~lonely(U,W))|~chevy(U,X))|~white(U,X))|~dirty(U,X))|~old(U,X))|~event(U,Y))|~agent(U,Y,X))|~present(U,Y))|~barrel(U,Y))|~down(U,Y,W))|~in(U,Y,W)))))))))),inference(fof_nnf,[status(thm)],[c0])).
% 6.13/6.33 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))&street(X2,X4))&lonely(X2,X4))&chevy(X2,X5))&white(X2,X5))&dirty(X2,X5))&old(X2,X5))&event(X2,X6))&agent(X2,X6,X5))&present(X2,X6))&barrel(X2,X6))&down(X2,X6,X4))&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))|~street(X19,X21))|~lonely(X19,X21))|~chevy(X19,X22))|~white(X19,X22))|~dirty(X19,X22))|~old(X19,X22))|~event(X19,X23))|~agent(X19,X23,X22))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X21))|~in(X19,X23,X21)))))))))),inference(variable_rename,[status(thm)],[c1])).
% 6.13/6.33 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))&street(skolem0001,skolem0003))&lonely(skolem0001,skolem0003))&chevy(skolem0001,skolem0004))&white(skolem0001,skolem0004))&dirty(skolem0001,skolem0004))&old(skolem0001,skolem0004))&event(skolem0001,skolem0005))&agent(skolem0001,skolem0005,skolem0004))&present(skolem0001,skolem0005))&barrel(skolem0001,skolem0005))&down(skolem0001,skolem0005,skolem0003))&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))|~street(X19,X21))|~lonely(X19,X21))|~chevy(X19,X22))|~white(X19,X22))|~dirty(X19,X22))|~old(X19,X22))|~event(X19,X23))|~agent(X19,X23,X22))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X21))|~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))&street(skolem0001,skolem0003))&lonely(skolem0001,skolem0003))&chevy(skolem0001,skolem0004))&white(skolem0001,skolem0004))&dirty(skolem0001,skolem0004))&old(skolem0001,skolem0004))&event(skolem0001,skolem0005))&agent(skolem0001,skolem0005,skolem0004))&present(skolem0001,skolem0005))&barrel(skolem0001,skolem0005))&down(skolem0001,skolem0005,skolem0003))&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))|~street(X19,X21))|~lonely(X19,X21))|~chevy(X19,X22))|~white(X19,X22))|~dirty(X19,X22))|~old(X19,X22))|~event(X19,X23))|~agent(X19,X23,X22))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X21))|~in(X19,X23,X21)))))))))),inference(skolemize,[status(esa)],[c2])).])).
% 6.13/6.34 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))|~street(X19,X21))|~lonely(X19,X21))|~chevy(X19,X22))|~white(X19,X22))|~dirty(X19,X22))|~old(X19,X22))|~event(X19,X23))|~agent(X19,X23,X22))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X21))|~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))|~street(X19,X21))|~lonely(X19,X21))|~chevy(X19,X22))|~white(X19,X22))|~dirty(X19,X22))|~old(X19,X22))|~event(X19,X23))|~agent(X19,X23,X22))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X21))|~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))|~street(X19,X21))|~lonely(X19,X21))|~chevy(X19,X22))|~white(X19,X22))|~dirty(X19,X22))|~old(X19,X22))|~event(X19,X23))|~agent(X19,X23,X22))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X21))|~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))|~street(X19,X21))|~lonely(X19,X21))|~chevy(X19,X22))|~white(X19,X22))|~dirty(X19,X22))|~old(X19,X22))|~event(X19,X23))|~agent(X19,X23,X22))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X21))|~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))|~street(X19,X21))|~lonely(X19,X21))|~chevy(X19,X22))|~white(X19,X22))|~dirty(X19,X22))|~old(X19,X22))|~event(X19,X23))|~agent(X19,X23,X22))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X21))|~in(X19,X23,X21))))))&(((street(skolem0001,skolem0003)|actual_world(skolem0006))&((((((((((((((((street(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007))&(street(skolem0001,skolem0003)|city(skolem0006,skolem0007)))&(street(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008)))&(street(skolem0001,skolem0003)|placename(skolem0006,skolem0008)))&(street(skolem0001,skolem0003)|street(skolem0006,skolem0009)))&(street(skolem0001,skolem0003)|lonely(skolem0006,skolem0009)))&(street(skolem0001,skolem0003)|chevy(skolem0006,skolem0010)))&(street(skolem0001,skolem0003)|white(skolem0006,skolem0010)))&(street(skolem0001,skolem0003)|dirty(skolem0006,skolem0010)))&(street(skolem0001,skolem0003)|old(skolem0006,skolem0010)))&(street(skolem0001,skolem0003)|event(skolem0006,skolem0011)))&(street(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0010)))&(street(skolem0001,skolem0003)|present(skolem0006,skolem0011)))&(street(skolem0001,skolem0003)|barrel(skolem0006,skolem0011)))&(street(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0009)))&(street(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007))))&(street(skolem0001,skolem0003)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~street(X19,X21))|~lonely(X19,X21))|~chevy(X19,X22))|~white(X19,X22))|~dirty(X19,X22))|~old(X19,X22))|~event(X19,X23))|~agent(X19,X23,X22))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X21))|~in(X19,X23,X21))))))&(((lonely(skolem0001,skolem0003)|actual_world(skolem0006))&((((((((((((((((lonely(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007))&(lonely(skolem0001,skolem0003)|city(skolem0006,skolem0007)))&(lonely(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008)))&(lonely(skolem0001,skolem0003)|placename(skolem0006,skolem0008)))&(lonely(skolem0001,skolem0003)|street(skolem0006,skolem0009)))&(lonely(skolem0001,skolem0003)|lonely(skolem0006,skolem0009)))&(lonely(skolem0001,skolem0003)|chevy(skolem0006,skolem0010)))&(lonely(skolem0001,skolem0003)|white(skolem0006,skolem0010)))&(lonely(skolem0001,skolem0003)|dirty(skolem0006,skolem0010)))&(lonely(skolem0001,skolem0003)|old(skolem0006,skolem0010)))&(lonely(skolem0001,skolem0003)|event(skolem0006,skolem0011)))&(lonely(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0010)))&(lonely(skolem0001,skolem0003)|present(skolem0006,skolem0011)))&(lonely(skolem0001,skolem0003)|barrel(skolem0006,skolem0011)))&(lonely(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0009)))&(lonely(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007))))&(lonely(skolem0001,skolem0003)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~street(X19,X21))|~lonely(X19,X21))|~chevy(X19,X22))|~white(X19,X22))|~dirty(X19,X22))|~old(X19,X22))|~event(X19,X23))|~agent(X19,X23,X22))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X21))|~in(X19,X23,X21))))))&(((chevy(skolem0001,skolem0004)|actual_world(skolem0006))&((((((((((((((((chevy(skolem0001,skolem0004)|of(skolem0006,skolem0008,skolem0007))&(chevy(skolem0001,skolem0004)|city(skolem0006,skolem0007)))&(chevy(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0008)))&(chevy(skolem0001,skolem0004)|placename(skolem0006,skolem0008)))&(chevy(skolem0001,skolem0004)|street(skolem0006,skolem0009)))&(chevy(skolem0001,skolem0004)|lonely(skolem0006,skolem0009)))&(chevy(skolem0001,skolem0004)|chevy(skolem0006,skolem0010)))&(chevy(skolem0001,skolem0004)|white(skolem0006,skolem0010)))&(chevy(skolem0001,skolem0004)|dirty(skolem0006,skolem0010)))&(chevy(skolem0001,skolem0004)|old(skolem0006,skolem0010)))&(chevy(skolem0001,skolem0004)|event(skolem0006,skolem0011)))&(chevy(skolem0001,skolem0004)|agent(skolem0006,skolem0011,skolem0010)))&(chevy(skolem0001,skolem0004)|present(skolem0006,skolem0011)))&(chevy(skolem0001,skolem0004)|barrel(skolem0006,skolem0011)))&(chevy(skolem0001,skolem0004)|down(skolem0006,skolem0011,skolem0009)))&(chevy(skolem0001,skolem0004)|in(skolem0006,skolem0011,skolem0007))))&(chevy(skolem0001,skolem0004)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~street(X19,X21))|~lonely(X19,X21))|~chevy(X19,X22))|~white(X19,X22))|~dirty(X19,X22))|~old(X19,X22))|~event(X19,X23))|~agent(X19,X23,X22))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X21))|~in(X19,X23,X21))))))&(((white(skolem0001,skolem0004)|actual_world(skolem0006))&((((((((((((((((white(skolem0001,skolem0004)|of(skolem0006,skolem0008,skolem0007))&(white(skolem0001,skolem0004)|city(skolem0006,skolem0007)))&(white(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0008)))&(white(skolem0001,skolem0004)|placename(skolem0006,skolem0008)))&(white(skolem0001,skolem0004)|street(skolem0006,skolem0009)))&(white(skolem0001,skolem0004)|lonely(skolem0006,skolem0009)))&(white(skolem0001,skolem0004)|chevy(skolem0006,skolem0010)))&(white(skolem0001,skolem0004)|white(skolem0006,skolem0010)))&(white(skolem0001,skolem0004)|dirty(skolem0006,skolem0010)))&(white(skolem0001,skolem0004)|old(skolem0006,skolem0010)))&(white(skolem0001,skolem0004)|event(skolem0006,skolem0011)))&(white(skolem0001,skolem0004)|agent(skolem0006,skolem0011,skolem0010)))&(white(skolem0001,skolem0004)|present(skolem0006,skolem0011)))&(white(skolem0001,skolem0004)|barrel(skolem0006,skolem0011)))&(white(skolem0001,skolem0004)|down(skolem0006,skolem0011,skolem0009)))&(white(skolem0001,skolem0004)|in(skolem0006,skolem0011,skolem0007))))&(white(skolem0001,skolem0004)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~street(X19,X21))|~lonely(X19,X21))|~chevy(X19,X22))|~white(X19,X22))|~dirty(X19,X22))|~old(X19,X22))|~event(X19,X23))|~agent(X19,X23,X22))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X21))|~in(X19,X23,X21))))))&(((dirty(skolem0001,skolem0004)|actual_world(skolem0006))&((((((((((((((((dirty(skolem0001,skolem0004)|of(skolem0006,skolem0008,skolem0007))&(dirty(skolem0001,skolem0004)|city(skolem0006,skolem0007)))&(dirty(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0008)))&(dirty(skolem0001,skolem0004)|placename(skolem0006,skolem0008)))&(dirty(skolem0001,skolem0004)|street(skolem0006,skolem0009)))&(dirty(skolem0001,skolem0004)|lonely(skolem0006,skolem0009)))&(dirty(skolem0001,skolem0004)|chevy(skolem0006,skolem0010)))&(dirty(skolem0001,skolem0004)|white(skolem0006,skolem0010)))&(dirty(skolem0001,skolem0004)|dirty(skolem0006,skolem0010)))&(dirty(skolem0001,skolem0004)|old(skolem0006,skolem0010)))&(dirty(skolem0001,skolem0004)|event(skolem0006,skolem0011)))&(dirty(skolem0001,skolem0004)|agent(skolem0006,skolem0011,skolem0010)))&(dirty(skolem0001,skolem0004)|present(skolem0006,skolem0011)))&(dirty(skolem0001,skolem0004)|barrel(skolem0006,skolem0011)))&(dirty(skolem0001,skolem0004)|down(skolem0006,skolem0011,skolem0009)))&(dirty(skolem0001,skolem0004)|in(skolem0006,skolem0011,skolem0007))))&(dirty(skolem0001,skolem0004)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~street(X19,X21))|~lonely(X19,X21))|~chevy(X19,X22))|~white(X19,X22))|~dirty(X19,X22))|~old(X19,X22))|~event(X19,X23))|~agent(X19,X23,X22))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X21))|~in(X19,X23,X21))))))&(((old(skolem0001,skolem0004)|actual_world(skolem0006))&((((((((((((((((old(skolem0001,skolem0004)|of(skolem0006,skolem0008,skolem0007))&(old(skolem0001,skolem0004)|city(skolem0006,skolem0007)))&(old(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0008)))&(old(skolem0001,skolem0004)|placename(skolem0006,skolem0008)))&(old(skolem0001,skolem0004)|street(skolem0006,skolem0009)))&(old(skolem0001,skolem0004)|lonely(skolem0006,skolem0009)))&(old(skolem0001,skolem0004)|chevy(skolem0006,skolem0010)))&(old(skolem0001,skolem0004)|white(skolem0006,skolem0010)))&(old(skolem0001,skolem0004)|dirty(skolem0006,skolem0010)))&(old(skolem0001,skolem0004)|old(skolem0006,skolem0010)))&(old(skolem0001,skolem0004)|event(skolem0006,skolem0011)))&(old(skolem0001,skolem0004)|agent(skolem0006,skolem0011,skolem0010)))&(old(skolem0001,skolem0004)|present(skolem0006,skolem0011)))&(old(skolem0001,skolem0004)|barrel(skolem0006,skolem0011)))&(old(skolem0001,skolem0004)|down(skolem0006,skolem0011,skolem0009)))&(old(skolem0001,skolem0004)|in(skolem0006,skolem0011,skolem0007))))&(old(skolem0001,skolem0004)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~street(X19,X21))|~lonely(X19,X21))|~chevy(X19,X22))|~white(X19,X22))|~dirty(X19,X22))|~old(X19,X22))|~event(X19,X23))|~agent(X19,X23,X22))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X21))|~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))|~street(X19,X21))|~lonely(X19,X21))|~chevy(X19,X22))|~white(X19,X22))|~dirty(X19,X22))|~old(X19,X22))|~event(X19,X23))|~agent(X19,X23,X22))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X21))|~in(X19,X23,X21))))))&(((agent(skolem0001,skolem0005,skolem0004)|actual_world(skolem0006))&((((((((((((((((agent(skolem0001,skolem0005,skolem0004)|of(skolem0006,skolem0008,skolem0007))&(agent(skolem0001,skolem0005,skolem0004)|city(skolem0006,skolem0007)))&(agent(skolem0001,skolem0005,skolem0004)|hollywood_placename(skolem0006,skolem0008)))&(agent(skolem0001,skolem0005,skolem0004)|placename(skolem0006,skolem0008)))&(agent(skolem0001,skolem0005,skolem0004)|street(skolem0006,skolem0009)))&(agent(skolem0001,skolem0005,skolem0004)|lonely(skolem0006,skolem0009)))&(agent(skolem0001,skolem0005,skolem0004)|chevy(skolem0006,skolem0010)))&(agent(skolem0001,skolem0005,skolem0004)|white(skolem0006,skolem0010)))&(agent(skolem0001,skolem0005,skolem0004)|dirty(skolem0006,skolem0010)))&(agent(skolem0001,skolem0005,skolem0004)|old(skolem0006,skolem0010)))&(agent(skolem0001,skolem0005,skolem0004)|event(skolem0006,skolem0011)))&(agent(skolem0001,skolem0005,skolem0004)|agent(skolem0006,skolem0011,skolem0010)))&(agent(skolem0001,skolem0005,skolem0004)|present(skolem0006,skolem0011)))&(agent(skolem0001,skolem0005,skolem0004)|barrel(skolem0006,skolem0011)))&(agent(skolem0001,skolem0005,skolem0004)|down(skolem0006,skolem0011,skolem0009)))&(agent(skolem0001,skolem0005,skolem0004)|in(skolem0006,skolem0011,skolem0007))))&(agent(skolem0001,skolem0005,skolem0004)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~street(X19,X21))|~lonely(X19,X21))|~chevy(X19,X22))|~white(X19,X22))|~dirty(X19,X22))|~old(X19,X22))|~event(X19,X23))|~agent(X19,X23,X22))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X21))|~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))|~street(X19,X21))|~lonely(X19,X21))|~chevy(X19,X22))|~white(X19,X22))|~dirty(X19,X22))|~old(X19,X22))|~event(X19,X23))|~agent(X19,X23,X22))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X21))|~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))|~street(X19,X21))|~lonely(X19,X21))|~chevy(X19,X22))|~white(X19,X22))|~dirty(X19,X22))|~old(X19,X22))|~event(X19,X23))|~agent(X19,X23,X22))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X21))|~in(X19,X23,X21))))))&(((down(skolem0001,skolem0005,skolem0003)|actual_world(skolem0006))&((((((((((((((((down(skolem0001,skolem0005,skolem0003)|of(skolem0006,skolem0008,skolem0007))&(down(skolem0001,skolem0005,skolem0003)|city(skolem0006,skolem0007)))&(down(skolem0001,skolem0005,skolem0003)|hollywood_placename(skolem0006,skolem0008)))&(down(skolem0001,skolem0005,skolem0003)|placename(skolem0006,skolem0008)))&(down(skolem0001,skolem0005,skolem0003)|street(skolem0006,skolem0009)))&(down(skolem0001,skolem0005,skolem0003)|lonely(skolem0006,skolem0009)))&(down(skolem0001,skolem0005,skolem0003)|chevy(skolem0006,skolem0010)))&(down(skolem0001,skolem0005,skolem0003)|white(skolem0006,skolem0010)))&(down(skolem0001,skolem0005,skolem0003)|dirty(skolem0006,skolem0010)))&(down(skolem0001,skolem0005,skolem0003)|old(skolem0006,skolem0010)))&(down(skolem0001,skolem0005,skolem0003)|event(skolem0006,skolem0011)))&(down(skolem0001,skolem0005,skolem0003)|agent(skolem0006,skolem0011,skolem0010)))&(down(skolem0001,skolem0005,skolem0003)|present(skolem0006,skolem0011)))&(down(skolem0001,skolem0005,skolem0003)|barrel(skolem0006,skolem0011)))&(down(skolem0001,skolem0005,skolem0003)|down(skolem0006,skolem0011,skolem0009)))&(down(skolem0001,skolem0005,skolem0003)|in(skolem0006,skolem0011,skolem0007))))&(down(skolem0001,skolem0005,skolem0003)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~street(X19,X21))|~lonely(X19,X21))|~chevy(X19,X22))|~white(X19,X22))|~dirty(X19,X22))|~old(X19,X22))|~event(X19,X23))|~agent(X19,X23,X22))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X21))|~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))|~street(X19,X21))|~lonely(X19,X21))|~chevy(X19,X22))|~white(X19,X22))|~dirty(X19,X22))|~old(X19,X22))|~event(X19,X23))|~agent(X19,X23,X22))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X21))|~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))|~street(X19,X21))|~lonely(X19,X21))|~chevy(X19,X22))|~white(X19,X22))|~dirty(X19,X22))|~old(X19,X22))|~event(X19,X23))|~agent(X19,X23,X22))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X21))|~in(X19,X23,X21))))))))))))))))),inference(distribute,[status(thm)],[c4])).
% 6.13/6.34 cnf(c21,negated_conjecture,actual_world(skolem0001)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c57,negated_conjecture,city(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c75,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c93,negated_conjecture,placename(skolem0001,skolem0002)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c111,negated_conjecture,street(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c129,negated_conjecture,lonely(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c147,negated_conjecture,chevy(skolem0001,skolem0004)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c165,negated_conjecture,white(skolem0001,skolem0004)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c183,negated_conjecture,dirty(skolem0001,skolem0004)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c201,negated_conjecture,old(skolem0001,skolem0004)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c219,negated_conjecture,event(skolem0001,skolem0005)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c255,negated_conjecture,present(skolem0001,skolem0005)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c273,negated_conjecture,barrel(skolem0001,skolem0005)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c39,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c237,negated_conjecture,agent(skolem0001,skolem0005,skolem0004)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c291,negated_conjecture,down(skolem0001,skolem0005,skolem0003)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c309,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c327,negated_conjecture,~actual_world(X201)|~of(X201,X203,X204)|~city(X201,X204)|~hollywood_placename(X201,X203)|~placename(X201,X203)|~street(X201,X199)|~lonely(X201,X199)|~chevy(X201,X200)|~white(X201,X200)|~dirty(X201,X200)|~old(X201,X200)|~event(X201,X202)|~agent(X201,X202,X200)|~present(X201,X202)|~barrel(X201,X202)|~down(X201,X202,X199)|~in(X201,X202,X204)|down(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c1438,plain,~actual_world(skolem0001)|~of(skolem0001,X1552,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1552)|~placename(skolem0001,X1552)|~street(skolem0001,X1551)|~lonely(skolem0001,X1551)|~chevy(skolem0001,X1553)|~white(skolem0001,X1553)|~dirty(skolem0001,X1553)|~old(skolem0001,X1553)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1553)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X1551)|down(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c327, c309])).
% 6.13/6.34 cnf(c3921,plain,~actual_world(skolem0001)|~of(skolem0001,X1555,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1555)|~placename(skolem0001,X1555)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,X1554)|~white(skolem0001,X1554)|~dirty(skolem0001,X1554)|~old(skolem0001,X1554)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1554)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|down(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c1438, c291])).
% 6.13/6.34 cnf(c3923,plain,~actual_world(skolem0001)|~of(skolem0001,X1558,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1558)|~placename(skolem0001,X1558)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|down(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c3921, c237])).
% 6.13/6.34 cnf(c3925,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|down(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c3923, c39])).
% 6.13/6.34 cnf(c3928,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|down(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c3925, c273])).
% 6.13/6.34 cnf(c3930,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|down(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c3928, c255])).
% 6.13/6.34 cnf(c3932,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|down(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c3930, c219])).
% 6.13/6.34 cnf(c3934,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|down(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c3932, c201])).
% 6.13/6.34 cnf(c3936,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|down(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c3934, c183])).
% 6.13/6.34 cnf(c3937,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|down(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c3936, c165])).
% 6.13/6.34 cnf(c3939,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c3937, c147])).
% 6.13/6.34 cnf(c3942,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c3939, c129])).
% 6.13/6.34 cnf(c3944,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|down(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c3942, c111])).
% 6.13/6.34 cnf(c3945,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|down(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c3944, c93])).
% 6.13/6.34 cnf(c3948,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c3945, c75])).
% 6.13/6.34 cnf(c3949,plain,~actual_world(skolem0001)|down(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c3948, c57])).
% 6.13/6.34 cnf(c3952,plain,down(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c3949, c21])).
% 6.13/6.34 cnf(c329,negated_conjecture,~actual_world(X217)|~of(X217,X219,X220)|~city(X217,X220)|~hollywood_placename(X217,X219)|~placename(X217,X219)|~street(X217,X212)|~lonely(X217,X212)|~chevy(X217,X214)|~white(X217,X214)|~dirty(X217,X214)|~old(X217,X214)|~event(X217,X218)|~agent(X217,X218,X214)|~present(X217,X218)|~barrel(X217,X218)|~down(X217,X218,X212)|~in(X217,X218,X220)|~actual_world(X221)|~of(X221,X215,X216)|~city(X221,X216)|~hollywood_placename(X221,X215)|~placename(X221,X215)|~street(X221,X216)|~lonely(X221,X216)|~chevy(X221,X211)|~white(X221,X211)|~dirty(X221,X211)|~old(X221,X211)|~event(X221,X213)|~agent(X221,X213,X211)|~present(X221,X213)|~barrel(X221,X213)|~down(X221,X213,X216)|~in(X221,X213,X216),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c1486,plain,~actual_world(X3605)|~of(X3605,X3607,X3609)|~city(X3605,X3609)|~hollywood_placename(X3605,X3607)|~placename(X3605,X3607)|~street(X3605,X3606)|~lonely(X3605,X3606)|~chevy(X3605,X3610)|~white(X3605,X3610)|~dirty(X3605,X3610)|~old(X3605,X3610)|~event(X3605,X3611)|~agent(X3605,X3611,X3610)|~present(X3605,X3611)|~barrel(X3605,X3611)|~down(X3605,X3611,X3606)|~in(X3605,X3611,X3609)|~of(X3605,X3612,X3609)|~hollywood_placename(X3605,X3612)|~placename(X3605,X3612)|~street(X3605,X3609)|~lonely(X3605,X3609)|~chevy(X3605,X3608)|~white(X3605,X3608)|~dirty(X3605,X3608)|~old(X3605,X3608)|~agent(X3605,X3611,X3608)|~down(X3605,X3611,X3609),inference(factor,[status(thm)],[c329])).
% 6.13/6.34 cnf(c3988,plain,~actual_world(skolem0006)|~of(skolem0006,X3657,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3657)|~placename(skolem0006,X3657)|~street(skolem0006,X3656)|~lonely(skolem0006,X3656)|~chevy(skolem0006,X3659)|~white(skolem0006,X3659)|~dirty(skolem0006,X3659)|~old(skolem0006,X3659)|~event(skolem0006,skolem0011)|~agent(skolem0006,skolem0011,X3659)|~present(skolem0006,skolem0011)|~barrel(skolem0006,skolem0011)|~down(skolem0006,skolem0011,X3656)|~in(skolem0006,skolem0011,skolem0009)|~of(skolem0006,X3660,skolem0009)|~hollywood_placename(skolem0006,X3660)|~placename(skolem0006,X3660)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009)|~chevy(skolem0006,X3658)|~white(skolem0006,X3658)|~dirty(skolem0006,X3658)|~old(skolem0006,X3658)|~agent(skolem0006,skolem0011,X3658),inference(resolution,[status(thm)],[c1486, c3952])).
% 6.13/6.34 cnf(c3994,plain,~actual_world(skolem0006)|~of(skolem0006,X3663,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3663)|~placename(skolem0006,X3663)|~street(skolem0006,X3662)|~lonely(skolem0006,X3662)|~chevy(skolem0006,X3661)|~white(skolem0006,X3661)|~dirty(skolem0006,X3661)|~old(skolem0006,X3661)|~event(skolem0006,skolem0011)|~agent(skolem0006,skolem0011,X3661)|~present(skolem0006,skolem0011)|~barrel(skolem0006,skolem0011)|~down(skolem0006,skolem0011,X3662)|~in(skolem0006,skolem0011,skolem0009)|~of(skolem0006,X3664,skolem0009)|~hollywood_placename(skolem0006,X3664)|~placename(skolem0006,X3664)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009),inference(factor,[status(thm)],[c3988])).
% 6.13/6.34 cnf(c3996,plain,~actual_world(skolem0006)|~of(skolem0006,X3666,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X3666)|~placename(skolem0006,X3666)|~street(skolem0006,X3665)|~lonely(skolem0006,X3665)|~chevy(skolem0006,X3667)|~white(skolem0006,X3667)|~dirty(skolem0006,X3667)|~old(skolem0006,X3667)|~event(skolem0006,skolem0011)|~agent(skolem0006,skolem0011,X3667)|~present(skolem0006,skolem0011)|~barrel(skolem0006,skolem0011)|~down(skolem0006,skolem0011,X3665)|~in(skolem0006,skolem0011,skolem0009)|~street(skolem0006,skolem0009)|~lonely(skolem0006,skolem0009),inference(factor,[status(thm)],[c3994])).
% 6.13/6.34 cnf(c22,negated_conjecture,actual_world(skolem0001)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c58,negated_conjecture,city(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c76,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c94,negated_conjecture,placename(skolem0001,skolem0002)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c112,negated_conjecture,street(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c130,negated_conjecture,lonely(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c148,negated_conjecture,chevy(skolem0001,skolem0004)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c166,negated_conjecture,white(skolem0001,skolem0004)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c184,negated_conjecture,dirty(skolem0001,skolem0004)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c202,negated_conjecture,old(skolem0001,skolem0004)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c220,negated_conjecture,event(skolem0001,skolem0005)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c256,negated_conjecture,present(skolem0001,skolem0005)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c274,negated_conjecture,barrel(skolem0001,skolem0005)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c40,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c238,negated_conjecture,agent(skolem0001,skolem0005,skolem0004)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c292,negated_conjecture,down(skolem0001,skolem0005,skolem0003)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c310,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c328,negated_conjecture,~actual_world(X207)|~of(X207,X209,X210)|~city(X207,X210)|~hollywood_placename(X207,X209)|~placename(X207,X209)|~street(X207,X205)|~lonely(X207,X205)|~chevy(X207,X206)|~white(X207,X206)|~dirty(X207,X206)|~old(X207,X206)|~event(X207,X208)|~agent(X207,X208,X206)|~present(X207,X208)|~barrel(X207,X208)|~down(X207,X208,X205)|~in(X207,X208,X210)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.34 cnf(c1482,plain,~actual_world(skolem0001)|~of(skolem0001,X1571,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1571)|~placename(skolem0001,X1571)|~street(skolem0001,X1570)|~lonely(skolem0001,X1570)|~chevy(skolem0001,X1569)|~white(skolem0001,X1569)|~dirty(skolem0001,X1569)|~old(skolem0001,X1569)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1569)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X1570)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c328, c310])).
% 6.13/6.34 cnf(c3953,plain,~actual_world(skolem0001)|~of(skolem0001,X1574,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1574)|~placename(skolem0001,X1574)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,X1575)|~white(skolem0001,X1575)|~dirty(skolem0001,X1575)|~old(skolem0001,X1575)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1575)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c1482, c292])).
% 6.13/6.35 cnf(c3954,plain,~actual_world(skolem0001)|~of(skolem0001,X1576,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1576)|~placename(skolem0001,X1576)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c3953, c238])).
% 6.13/6.35 cnf(c3955,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c3954, c40])).
% 6.13/6.35 cnf(c3956,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c3955, c274])).
% 6.13/6.35 cnf(c3957,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c3956, c256])).
% 6.13/6.35 cnf(c3958,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c3957, c220])).
% 6.13/6.35 cnf(c3959,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c3958, c202])).
% 6.13/6.35 cnf(c3960,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c3959, c184])).
% 6.13/6.35 cnf(c3961,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c3960, c166])).
% 6.13/6.35 cnf(c3962,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c3961, c148])).
% 6.13/6.35 cnf(c3963,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c3962, c130])).
% 6.13/6.35 cnf(c3964,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c3963, c112])).
% 6.13/6.35 cnf(c3965,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c3964, c94])).
% 6.13/6.35 cnf(c3966,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c3965, c76])).
% 6.13/6.35 cnf(c3967,plain,~actual_world(skolem0001)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c3966, c58])).
% 6.13/6.35 cnf(c3968,plain,in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c3967, c22])).
% 6.13/6.35 cnf(c3987,plain,~actual_world(X3613)|~of(X3613,X3615,X3614)|~city(X3613,X3614)|~hollywood_placename(X3613,X3615)|~placename(X3613,X3615)|~street(X3613,X3614)|~lonely(X3613,X3614)|~chevy(X3613,X3618)|~white(X3613,X3618)|~dirty(X3613,X3618)|~old(X3613,X3618)|~event(X3613,X3616)|~agent(X3613,X3616,X3618)|~present(X3613,X3616)|~barrel(X3613,X3616)|~down(X3613,X3616,X3614)|~in(X3613,X3616,X3614)|~of(X3613,X3619,X3614)|~hollywood_placename(X3613,X3619)|~placename(X3613,X3619)|~chevy(X3613,X3617)|~white(X3613,X3617)|~dirty(X3613,X3617)|~old(X3613,X3617)|~agent(X3613,X3616,X3617),inference(factor,[status(thm)],[c1486])).
% 6.13/6.35 cnf(c3989,plain,~actual_world(X3631)|~of(X3631,X3633,X3632)|~city(X3631,X3632)|~hollywood_placename(X3631,X3633)|~placename(X3631,X3633)|~street(X3631,X3632)|~lonely(X3631,X3632)|~chevy(X3631,X3628)|~white(X3631,X3628)|~dirty(X3631,X3628)|~old(X3631,X3628)|~event(X3631,X3629)|~agent(X3631,X3629,X3628)|~present(X3631,X3629)|~barrel(X3631,X3629)|~down(X3631,X3629,X3632)|~in(X3631,X3629,X3632)|~of(X3631,X3630,X3632)|~hollywood_placename(X3631,X3630)|~placename(X3631,X3630),inference(factor,[status(thm)],[c3987])).
% 6.13/6.35 cnf(c3991,plain,~actual_world(X3634)|~of(X3634,X3638,X3637)|~city(X3634,X3637)|~hollywood_placename(X3634,X3638)|~placename(X3634,X3638)|~street(X3634,X3637)|~lonely(X3634,X3637)|~chevy(X3634,X3636)|~white(X3634,X3636)|~dirty(X3634,X3636)|~old(X3634,X3636)|~event(X3634,X3635)|~agent(X3634,X3635,X3636)|~present(X3634,X3635)|~barrel(X3634,X3635)|~down(X3634,X3635,X3637)|~in(X3634,X3635,X3637),inference(factor,[status(thm)],[c3989])).
% 6.13/6.35 cnf(c3993,plain,~actual_world(skolem0006)|~of(skolem0006,X3639,skolem0007)|~city(skolem0006,skolem0007)|~hollywood_placename(skolem0006,X3639)|~placename(skolem0006,X3639)|~street(skolem0006,skolem0007)|~lonely(skolem0006,skolem0007)|~chevy(skolem0006,X3640)|~white(skolem0006,X3640)|~dirty(skolem0006,X3640)|~old(skolem0006,X3640)|~event(skolem0006,skolem0011)|~agent(skolem0006,skolem0011,X3640)|~present(skolem0006,skolem0011)|~barrel(skolem0006,skolem0011)|~down(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c3991, c3968])).
% 6.13/6.35 cnf(c18,negated_conjecture,actual_world(skolem0001)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c54,negated_conjecture,city(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c72,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c90,negated_conjecture,placename(skolem0001,skolem0002)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c108,negated_conjecture,street(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c126,negated_conjecture,lonely(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c144,negated_conjecture,chevy(skolem0001,skolem0004)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c162,negated_conjecture,white(skolem0001,skolem0004)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c180,negated_conjecture,dirty(skolem0001,skolem0004)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c198,negated_conjecture,old(skolem0001,skolem0004)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c216,negated_conjecture,event(skolem0001,skolem0005)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c252,negated_conjecture,present(skolem0001,skolem0005)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c270,negated_conjecture,barrel(skolem0001,skolem0005)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c36,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c234,negated_conjecture,agent(skolem0001,skolem0005,skolem0004)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c288,negated_conjecture,down(skolem0001,skolem0005,skolem0003)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c306,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c324,negated_conjecture,~actual_world(X195)|~of(X195,X197,X198)|~city(X195,X198)|~hollywood_placename(X195,X197)|~placename(X195,X197)|~street(X195,X193)|~lonely(X195,X193)|~chevy(X195,X194)|~white(X195,X194)|~dirty(X195,X194)|~old(X195,X194)|~event(X195,X196)|~agent(X195,X196,X194)|~present(X195,X196)|~barrel(X195,X196)|~down(X195,X196,X193)|~in(X195,X196,X198)|agent(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c1390,plain,~actual_world(skolem0001)|~of(skolem0001,X1527,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1527)|~placename(skolem0001,X1527)|~street(skolem0001,X1529)|~lonely(skolem0001,X1529)|~chevy(skolem0001,X1528)|~white(skolem0001,X1528)|~dirty(skolem0001,X1528)|~old(skolem0001,X1528)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1528)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X1529)|agent(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c324, c306])).
% 6.13/6.35 cnf(c3875,plain,~actual_world(skolem0001)|~of(skolem0001,X1531,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1531)|~placename(skolem0001,X1531)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,X1530)|~white(skolem0001,X1530)|~dirty(skolem0001,X1530)|~old(skolem0001,X1530)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1530)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|agent(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c1390, c288])).
% 6.13/6.35 cnf(c3876,plain,~actual_world(skolem0001)|~of(skolem0001,X1534,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1534)|~placename(skolem0001,X1534)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|agent(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c3875, c234])).
% 6.13/6.35 cnf(c3880,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|agent(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c3876, c36])).
% 6.13/6.35 cnf(c3882,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|agent(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c3880, c270])).
% 6.13/6.35 cnf(c3887,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|agent(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c3882, c252])).
% 6.13/6.35 cnf(c3889,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|agent(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c3887, c216])).
% 6.13/6.35 cnf(c3893,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|agent(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c3889, c198])).
% 6.13/6.35 cnf(c3896,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|agent(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c3893, c180])).
% 6.13/6.35 cnf(c3898,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|agent(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c3896, c162])).
% 6.13/6.35 cnf(c3901,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c3898, c144])).
% 6.13/6.35 cnf(c3905,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c3901, c126])).
% 6.13/6.35 cnf(c3908,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|agent(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c3905, c108])).
% 6.13/6.35 cnf(c3909,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|agent(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c3908, c90])).
% 6.13/6.35 cnf(c3912,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c3909, c72])).
% 6.13/6.35 cnf(c3917,plain,~actual_world(skolem0001)|agent(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c3912, c54])).
% 6.13/6.35 cnf(c3919,plain,agent(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c3917, c18])).
% 6.13/6.35 cnf(c7,negated_conjecture,actual_world(skolem0001)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c43,negated_conjecture,city(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c61,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c79,negated_conjecture,placename(skolem0001,skolem0002)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c97,negated_conjecture,street(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c115,negated_conjecture,lonely(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c133,negated_conjecture,chevy(skolem0001,skolem0004)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c151,negated_conjecture,white(skolem0001,skolem0004)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c169,negated_conjecture,dirty(skolem0001,skolem0004)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c187,negated_conjecture,old(skolem0001,skolem0004)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c205,negated_conjecture,event(skolem0001,skolem0005)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c241,negated_conjecture,present(skolem0001,skolem0005)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c259,negated_conjecture,barrel(skolem0001,skolem0005)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c25,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c223,negated_conjecture,agent(skolem0001,skolem0005,skolem0004)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c277,negated_conjecture,down(skolem0001,skolem0005,skolem0003)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c295,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c313,negated_conjecture,~actual_world(X177)|~of(X177,X179,X180)|~city(X177,X180)|~hollywood_placename(X177,X179)|~placename(X177,X179)|~street(X177,X175)|~lonely(X177,X175)|~chevy(X177,X176)|~white(X177,X176)|~dirty(X177,X176)|~old(X177,X176)|~event(X177,X178)|~agent(X177,X178,X176)|~present(X177,X178)|~barrel(X177,X178)|~down(X177,X178,X175)|~in(X177,X178,X180)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c1308,plain,~actual_world(skolem0001)|~of(skolem0001,X1497,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1497)|~placename(skolem0001,X1497)|~street(skolem0001,X1499)|~lonely(skolem0001,X1499)|~chevy(skolem0001,X1498)|~white(skolem0001,X1498)|~dirty(skolem0001,X1498)|~old(skolem0001,X1498)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1498)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X1499)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c313, c295])).
% 6.13/6.35 cnf(c3810,plain,~actual_world(skolem0001)|~of(skolem0001,X1503,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1503)|~placename(skolem0001,X1503)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,X1502)|~white(skolem0001,X1502)|~dirty(skolem0001,X1502)|~old(skolem0001,X1502)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1502)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c1308, c277])).
% 6.13/6.35 cnf(c3814,plain,~actual_world(skolem0001)|~of(skolem0001,X1504,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1504)|~placename(skolem0001,X1504)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c3810, c223])).
% 6.13/6.35 cnf(c3819,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c3814, c25])).
% 6.13/6.35 cnf(c3824,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c3819, c259])).
% 6.13/6.35 cnf(c3828,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c3824, c241])).
% 6.13/6.35 cnf(c3832,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c3828, c205])).
% 6.13/6.35 cnf(c3834,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c3832, c187])).
% 6.13/6.35 cnf(c3839,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c3834, c169])).
% 6.13/6.35 cnf(c3842,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c3839, c151])).
% 6.13/6.35 cnf(c3848,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c3842, c133])).
% 6.13/6.35 cnf(c3852,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c3848, c115])).
% 6.13/6.35 cnf(c3856,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c3852, c97])).
% 6.13/6.35 cnf(c3859,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c3856, c79])).
% 6.13/6.35 cnf(c3861,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c3859, c61])).
% 6.13/6.35 cnf(c3865,plain,~actual_world(skolem0001)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c3861, c43])).
% 6.13/6.35 cnf(c3869,plain,of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c3865, c7])).
% 6.13/6.35 cnf(c20,negated_conjecture,actual_world(skolem0001)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c56,negated_conjecture,city(skolem0001,skolem0003)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c74,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c92,negated_conjecture,placename(skolem0001,skolem0002)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c110,negated_conjecture,street(skolem0001,skolem0003)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c128,negated_conjecture,lonely(skolem0001,skolem0003)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c146,negated_conjecture,chevy(skolem0001,skolem0004)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c164,negated_conjecture,white(skolem0001,skolem0004)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c182,negated_conjecture,dirty(skolem0001,skolem0004)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c200,negated_conjecture,old(skolem0001,skolem0004)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c218,negated_conjecture,event(skolem0001,skolem0005)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c254,negated_conjecture,present(skolem0001,skolem0005)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c272,negated_conjecture,barrel(skolem0001,skolem0005)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c38,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c236,negated_conjecture,agent(skolem0001,skolem0005,skolem0004)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c290,negated_conjecture,down(skolem0001,skolem0005,skolem0003)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c308,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c326,negated_conjecture,~actual_world(X189)|~of(X189,X191,X192)|~city(X189,X192)|~hollywood_placename(X189,X191)|~placename(X189,X191)|~street(X189,X187)|~lonely(X189,X187)|~chevy(X189,X188)|~white(X189,X188)|~dirty(X189,X188)|~old(X189,X188)|~event(X189,X190)|~agent(X189,X190,X188)|~present(X189,X190)|~barrel(X189,X190)|~down(X189,X190,X187)|~in(X189,X190,X192)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c1383,plain,~actual_world(skolem0001)|~of(skolem0001,X1224,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1224)|~placename(skolem0001,X1224)|~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.13/6.35 cnf(c3729,plain,~actual_world(skolem0001)|~of(skolem0001,X1228,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1228)|~placename(skolem0001,X1228)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,X1227)|~white(skolem0001,X1227)|~dirty(skolem0001,X1227)|~old(skolem0001,X1227)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1227)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c1383, c290])).
% 6.13/6.35 cnf(c3738,plain,~actual_world(skolem0001)|~of(skolem0001,X1229,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1229)|~placename(skolem0001,X1229)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3729, c236])).
% 6.13/6.35 cnf(c3740,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3738, c38])).
% 6.13/6.35 cnf(c3747,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3740, c272])).
% 6.13/6.35 cnf(c3750,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3747, c254])).
% 6.13/6.35 cnf(c3758,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3750, c218])).
% 6.13/6.35 cnf(c3763,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3758, c200])).
% 6.13/6.35 cnf(c3766,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3763, c182])).
% 6.13/6.35 cnf(c3772,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3766, c164])).
% 6.13/6.35 cnf(c3774,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3772, c146])).
% 6.13/6.35 cnf(c3781,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3774, c128])).
% 6.13/6.35 cnf(c3787,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3781, c110])).
% 6.13/6.35 cnf(c3793,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3787, c92])).
% 6.13/6.35 cnf(c3796,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3793, c74])).
% 6.13/6.35 cnf(c3799,plain,~actual_world(skolem0001)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3796, c56])).
% 6.13/6.35 cnf(c3805,plain,barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3799, c20])).
% 6.13/6.35 cnf(c19,negated_conjecture,actual_world(skolem0001)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c55,negated_conjecture,city(skolem0001,skolem0003)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c73,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c91,negated_conjecture,placename(skolem0001,skolem0002)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c109,negated_conjecture,street(skolem0001,skolem0003)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c127,negated_conjecture,lonely(skolem0001,skolem0003)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c145,negated_conjecture,chevy(skolem0001,skolem0004)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c163,negated_conjecture,white(skolem0001,skolem0004)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c181,negated_conjecture,dirty(skolem0001,skolem0004)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c199,negated_conjecture,old(skolem0001,skolem0004)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c217,negated_conjecture,event(skolem0001,skolem0005)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c253,negated_conjecture,present(skolem0001,skolem0005)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c271,negated_conjecture,barrel(skolem0001,skolem0005)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c37,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c235,negated_conjecture,agent(skolem0001,skolem0005,skolem0004)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c289,negated_conjecture,down(skolem0001,skolem0005,skolem0003)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c307,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c325,negated_conjecture,~actual_world(X183)|~of(X183,X185,X186)|~city(X183,X186)|~hollywood_placename(X183,X185)|~placename(X183,X185)|~street(X183,X181)|~lonely(X183,X181)|~chevy(X183,X182)|~white(X183,X182)|~dirty(X183,X182)|~old(X183,X182)|~event(X183,X184)|~agent(X183,X184,X182)|~present(X183,X184)|~barrel(X183,X184)|~down(X183,X184,X181)|~in(X183,X184,X186)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c1333,plain,~actual_world(skolem0001)|~of(skolem0001,X1183,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1183)|~placename(skolem0001,X1183)|~street(skolem0001,X1181)|~lonely(skolem0001,X1181)|~chevy(skolem0001,X1182)|~white(skolem0001,X1182)|~dirty(skolem0001,X1182)|~old(skolem0001,X1182)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1182)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X1181)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c325, c307])).
% 6.13/6.35 cnf(c3637,plain,~actual_world(skolem0001)|~of(skolem0001,X1186,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1186)|~placename(skolem0001,X1186)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~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)],[c1333, c289])).
% 6.13/6.35 cnf(c3644,plain,~actual_world(skolem0001)|~of(skolem0001,X1188,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1188)|~placename(skolem0001,X1188)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3637, c235])).
% 6.13/6.35 cnf(c3645,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3644, c37])).
% 6.13/6.35 cnf(c3652,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3645, c271])).
% 6.13/6.35 cnf(c3657,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3652, c253])).
% 6.13/6.35 cnf(c3668,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3657, c217])).
% 6.13/6.35 cnf(c3672,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3668, c199])).
% 6.13/6.35 cnf(c3676,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3672, c181])).
% 6.13/6.35 cnf(c3685,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3676, c163])).
% 6.13/6.35 cnf(c3687,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3685, c145])).
% 6.13/6.35 cnf(c3696,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3687, c127])).
% 6.13/6.35 cnf(c3704,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3696, c109])).
% 6.13/6.35 cnf(c3706,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3704, c91])).
% 6.13/6.35 cnf(c3714,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3706, c73])).
% 6.13/6.35 cnf(c3718,plain,~actual_world(skolem0001)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3714, c55])).
% 6.13/6.35 cnf(c3723,plain,present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3718, c19])).
% 6.13/6.35 cnf(c17,negated_conjecture,actual_world(skolem0001)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c53,negated_conjecture,city(skolem0001,skolem0003)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c71,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c89,negated_conjecture,placename(skolem0001,skolem0002)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c107,negated_conjecture,street(skolem0001,skolem0003)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c125,negated_conjecture,lonely(skolem0001,skolem0003)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c143,negated_conjecture,chevy(skolem0001,skolem0004)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c161,negated_conjecture,white(skolem0001,skolem0004)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c179,negated_conjecture,dirty(skolem0001,skolem0004)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c197,negated_conjecture,old(skolem0001,skolem0004)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c215,negated_conjecture,event(skolem0001,skolem0005)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c251,negated_conjecture,present(skolem0001,skolem0005)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c269,negated_conjecture,barrel(skolem0001,skolem0005)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c35,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c233,negated_conjecture,agent(skolem0001,skolem0005,skolem0004)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c287,negated_conjecture,down(skolem0001,skolem0005,skolem0003)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c305,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c323,negated_conjecture,~actual_world(X171)|~of(X171,X173,X174)|~city(X171,X174)|~hollywood_placename(X171,X173)|~placename(X171,X173)|~street(X171,X169)|~lonely(X171,X169)|~chevy(X171,X170)|~white(X171,X170)|~dirty(X171,X170)|~old(X171,X170)|~event(X171,X172)|~agent(X171,X172,X170)|~present(X171,X172)|~barrel(X171,X172)|~down(X171,X172,X169)|~in(X171,X172,X174)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.35 cnf(c1271,plain,~actual_world(skolem0001)|~of(skolem0001,X1135,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1135)|~placename(skolem0001,X1135)|~street(skolem0001,X1133)|~lonely(skolem0001,X1133)|~chevy(skolem0001,X1134)|~white(skolem0001,X1134)|~dirty(skolem0001,X1134)|~old(skolem0001,X1134)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1134)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X1133)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c323, c305])).
% 6.13/6.35 cnf(c3526,plain,~actual_world(skolem0001)|~of(skolem0001,X1136,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1136)|~placename(skolem0001,X1136)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~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)],[c1271, c287])).
% 6.13/6.35 cnf(c3528,plain,~actual_world(skolem0001)|~of(skolem0001,X1138,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1138)|~placename(skolem0001,X1138)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3526, c233])).
% 6.13/6.35 cnf(c3535,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3528, c35])).
% 6.13/6.35 cnf(c3542,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3535, c269])).
% 6.13/6.35 cnf(c3549,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3542, c251])).
% 6.13/6.35 cnf(c3556,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3549, c215])).
% 6.13/6.35 cnf(c3567,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3556, c197])).
% 6.13/6.35 cnf(c3574,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3567, c179])).
% 6.13/6.35 cnf(c3580,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3574, c161])).
% 6.13/6.35 cnf(c3584,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3580, c143])).
% 6.13/6.36 cnf(c3594,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3584, c125])).
% 6.13/6.36 cnf(c3600,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3594, c107])).
% 6.13/6.36 cnf(c3607,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3600, c89])).
% 6.13/6.36 cnf(c3612,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3607, c71])).
% 6.13/6.36 cnf(c3619,plain,~actual_world(skolem0001)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3612, c53])).
% 6.13/6.36 cnf(c3626,plain,event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3619, c17])).
% 6.13/6.36 cnf(c16,negated_conjecture,actual_world(skolem0001)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c52,negated_conjecture,city(skolem0001,skolem0003)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c70,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c88,negated_conjecture,placename(skolem0001,skolem0002)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c106,negated_conjecture,street(skolem0001,skolem0003)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c124,negated_conjecture,lonely(skolem0001,skolem0003)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c142,negated_conjecture,chevy(skolem0001,skolem0004)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c160,negated_conjecture,white(skolem0001,skolem0004)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c178,negated_conjecture,dirty(skolem0001,skolem0004)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c196,negated_conjecture,old(skolem0001,skolem0004)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c214,negated_conjecture,event(skolem0001,skolem0005)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c250,negated_conjecture,present(skolem0001,skolem0005)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c268,negated_conjecture,barrel(skolem0001,skolem0005)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c34,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c232,negated_conjecture,agent(skolem0001,skolem0005,skolem0004)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c286,negated_conjecture,down(skolem0001,skolem0005,skolem0003)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c304,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c322,negated_conjecture,~actual_world(X165)|~of(X165,X167,X168)|~city(X165,X168)|~hollywood_placename(X165,X167)|~placename(X165,X167)|~street(X165,X163)|~lonely(X165,X163)|~chevy(X165,X164)|~white(X165,X164)|~dirty(X165,X164)|~old(X165,X164)|~event(X165,X166)|~agent(X165,X166,X164)|~present(X165,X166)|~barrel(X165,X166)|~down(X165,X166,X163)|~in(X165,X166,X168)|old(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c1242,plain,~actual_world(skolem0001)|~of(skolem0001,X1076,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1076)|~placename(skolem0001,X1076)|~street(skolem0001,X1078)|~lonely(skolem0001,X1078)|~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,X1078)|old(skolem0006,skolem0010),inference(resolution,[status(thm)],[c322, c304])).
% 6.13/6.36 cnf(c3393,plain,~actual_world(skolem0001)|~of(skolem0001,X1080,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1080)|~placename(skolem0001,X1080)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,X1079)|~white(skolem0001,X1079)|~dirty(skolem0001,X1079)|~old(skolem0001,X1079)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1079)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|old(skolem0006,skolem0010),inference(resolution,[status(thm)],[c1242, c286])).
% 6.13/6.36 cnf(c3404,plain,~actual_world(skolem0001)|~of(skolem0001,X1083,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1083)|~placename(skolem0001,X1083)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|old(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3393, c232])).
% 6.13/6.36 cnf(c3416,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|old(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3404, c34])).
% 6.13/6.36 cnf(c3419,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|old(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3416, c268])).
% 6.13/6.36 cnf(c3429,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|old(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3419, c250])).
% 6.13/6.36 cnf(c3437,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|old(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3429, c214])).
% 6.13/6.36 cnf(c3443,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|old(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3437, c196])).
% 6.13/6.36 cnf(c3455,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|old(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3443, c178])).
% 6.13/6.36 cnf(c3462,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|old(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3455, c160])).
% 6.13/6.36 cnf(c3467,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|old(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3462, c142])).
% 6.13/6.36 cnf(c3479,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|old(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3467, c124])).
% 6.13/6.36 cnf(c3484,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|old(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3479, c106])).
% 6.13/6.36 cnf(c3491,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|old(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3484, c88])).
% 6.13/6.36 cnf(c3500,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|old(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3491, c70])).
% 6.13/6.36 cnf(c3508,plain,~actual_world(skolem0001)|old(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3500, c52])).
% 6.13/6.36 cnf(c3514,plain,old(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3508, c16])).
% 6.13/6.36 cnf(c15,negated_conjecture,actual_world(skolem0001)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c51,negated_conjecture,city(skolem0001,skolem0003)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c69,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c87,negated_conjecture,placename(skolem0001,skolem0002)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c105,negated_conjecture,street(skolem0001,skolem0003)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c123,negated_conjecture,lonely(skolem0001,skolem0003)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c141,negated_conjecture,chevy(skolem0001,skolem0004)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c159,negated_conjecture,white(skolem0001,skolem0004)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c177,negated_conjecture,dirty(skolem0001,skolem0004)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c195,negated_conjecture,old(skolem0001,skolem0004)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c213,negated_conjecture,event(skolem0001,skolem0005)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c249,negated_conjecture,present(skolem0001,skolem0005)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c267,negated_conjecture,barrel(skolem0001,skolem0005)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c33,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c231,negated_conjecture,agent(skolem0001,skolem0005,skolem0004)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c285,negated_conjecture,down(skolem0001,skolem0005,skolem0003)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c303,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c321,negated_conjecture,~actual_world(X159)|~of(X159,X161,X162)|~city(X159,X162)|~hollywood_placename(X159,X161)|~placename(X159,X161)|~street(X159,X157)|~lonely(X159,X157)|~chevy(X159,X158)|~white(X159,X158)|~dirty(X159,X158)|~old(X159,X158)|~event(X159,X160)|~agent(X159,X160,X158)|~present(X159,X160)|~barrel(X159,X160)|~down(X159,X160,X157)|~in(X159,X160,X162)|dirty(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c1212,plain,~actual_world(skolem0001)|~of(skolem0001,X1014,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1014)|~placename(skolem0001,X1014)|~street(skolem0001,X1015)|~lonely(skolem0001,X1015)|~chevy(skolem0001,X1016)|~white(skolem0001,X1016)|~dirty(skolem0001,X1016)|~old(skolem0001,X1016)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1016)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X1015)|dirty(skolem0006,skolem0010),inference(resolution,[status(thm)],[c321, c303])).
% 6.13/6.36 cnf(c3257,plain,~actual_world(skolem0001)|~of(skolem0001,X1017,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1017)|~placename(skolem0001,X1017)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,X1018)|~white(skolem0001,X1018)|~dirty(skolem0001,X1018)|~old(skolem0001,X1018)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1018)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|dirty(skolem0006,skolem0010),inference(resolution,[status(thm)],[c1212, c285])).
% 6.13/6.36 cnf(c3265,plain,~actual_world(skolem0001)|~of(skolem0001,X1019,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1019)|~placename(skolem0001,X1019)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|dirty(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3257, c231])).
% 6.13/6.36 cnf(c3267,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|dirty(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3265, c33])).
% 6.13/6.36 cnf(c3280,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|dirty(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3267, c267])).
% 6.13/6.36 cnf(c3291,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|dirty(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3280, c249])).
% 6.13/6.36 cnf(c3301,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|dirty(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3291, c213])).
% 6.13/6.36 cnf(c3310,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|dirty(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3301, c195])).
% 6.13/6.36 cnf(c3316,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|dirty(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3310, c177])).
% 6.13/6.36 cnf(c3322,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|dirty(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3316, c159])).
% 6.13/6.36 cnf(c3335,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|dirty(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3322, c141])).
% 6.13/6.36 cnf(c3345,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|dirty(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3335, c123])).
% 6.13/6.36 cnf(c3355,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|dirty(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3345, c105])).
% 6.13/6.36 cnf(c3358,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|dirty(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3355, c87])).
% 6.13/6.36 cnf(c3366,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|dirty(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3358, c69])).
% 6.13/6.36 cnf(c3377,plain,~actual_world(skolem0001)|dirty(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3366, c51])).
% 6.13/6.36 cnf(c3392,plain,dirty(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3377, c15])).
% 6.13/6.36 cnf(c14,negated_conjecture,actual_world(skolem0001)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c50,negated_conjecture,city(skolem0001,skolem0003)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c68,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c86,negated_conjecture,placename(skolem0001,skolem0002)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c104,negated_conjecture,street(skolem0001,skolem0003)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c122,negated_conjecture,lonely(skolem0001,skolem0003)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c140,negated_conjecture,chevy(skolem0001,skolem0004)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c158,negated_conjecture,white(skolem0001,skolem0004)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c176,negated_conjecture,dirty(skolem0001,skolem0004)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c194,negated_conjecture,old(skolem0001,skolem0004)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c212,negated_conjecture,event(skolem0001,skolem0005)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c248,negated_conjecture,present(skolem0001,skolem0005)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c266,negated_conjecture,barrel(skolem0001,skolem0005)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c32,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c230,negated_conjecture,agent(skolem0001,skolem0005,skolem0004)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c284,negated_conjecture,down(skolem0001,skolem0005,skolem0003)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c302,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c320,negated_conjecture,~actual_world(X153)|~of(X153,X155,X156)|~city(X153,X156)|~hollywood_placename(X153,X155)|~placename(X153,X155)|~street(X153,X151)|~lonely(X153,X151)|~chevy(X153,X152)|~white(X153,X152)|~dirty(X153,X152)|~old(X153,X152)|~event(X153,X154)|~agent(X153,X154,X152)|~present(X153,X154)|~barrel(X153,X154)|~down(X153,X154,X151)|~in(X153,X154,X156)|white(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c1149,plain,~actual_world(skolem0001)|~of(skolem0001,X945,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X945)|~placename(skolem0001,X945)|~street(skolem0001,X944)|~lonely(skolem0001,X944)|~chevy(skolem0001,X943)|~white(skolem0001,X943)|~dirty(skolem0001,X943)|~old(skolem0001,X943)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X943)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X944)|white(skolem0006,skolem0010),inference(resolution,[status(thm)],[c320, c302])).
% 6.13/6.36 cnf(c3097,plain,~actual_world(skolem0001)|~of(skolem0001,X947,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X947)|~placename(skolem0001,X947)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,X946)|~white(skolem0001,X946)|~dirty(skolem0001,X946)|~old(skolem0001,X946)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X946)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|white(skolem0006,skolem0010),inference(resolution,[status(thm)],[c1149, c284])).
% 6.13/6.36 cnf(c3099,plain,~actual_world(skolem0001)|~of(skolem0001,X948,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X948)|~placename(skolem0001,X948)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|white(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3097, c230])).
% 6.13/6.36 cnf(c3109,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|white(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3099, c32])).
% 6.13/6.36 cnf(c3122,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|white(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3109, c266])).
% 6.13/6.36 cnf(c3134,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|white(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3122, c248])).
% 6.13/6.36 cnf(c3142,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|white(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3134, c212])).
% 6.13/6.36 cnf(c3157,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|white(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3142, c194])).
% 6.13/6.36 cnf(c3163,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|white(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3157, c176])).
% 6.13/6.36 cnf(c3175,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|white(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3163, c158])).
% 6.13/6.36 cnf(c3181,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|white(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3175, c140])).
% 6.13/6.36 cnf(c3196,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|white(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3181, c122])).
% 6.13/6.36 cnf(c3199,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|white(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3196, c104])).
% 6.13/6.36 cnf(c3212,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|white(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3199, c86])).
% 6.13/6.36 cnf(c3226,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|white(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3212, c68])).
% 6.13/6.36 cnf(c3233,plain,~actual_world(skolem0001)|white(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3226, c50])).
% 6.13/6.36 cnf(c3239,plain,white(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3233, c14])).
% 6.13/6.36 cnf(c13,negated_conjecture,actual_world(skolem0001)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c49,negated_conjecture,city(skolem0001,skolem0003)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c67,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c85,negated_conjecture,placename(skolem0001,skolem0002)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c103,negated_conjecture,street(skolem0001,skolem0003)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c121,negated_conjecture,lonely(skolem0001,skolem0003)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c139,negated_conjecture,chevy(skolem0001,skolem0004)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c157,negated_conjecture,white(skolem0001,skolem0004)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c175,negated_conjecture,dirty(skolem0001,skolem0004)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c193,negated_conjecture,old(skolem0001,skolem0004)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c211,negated_conjecture,event(skolem0001,skolem0005)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c247,negated_conjecture,present(skolem0001,skolem0005)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c265,negated_conjecture,barrel(skolem0001,skolem0005)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c31,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c229,negated_conjecture,agent(skolem0001,skolem0005,skolem0004)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c283,negated_conjecture,down(skolem0001,skolem0005,skolem0003)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c301,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c319,negated_conjecture,~actual_world(X147)|~of(X147,X149,X150)|~city(X147,X150)|~hollywood_placename(X147,X149)|~placename(X147,X149)|~street(X147,X145)|~lonely(X147,X145)|~chevy(X147,X146)|~white(X147,X146)|~dirty(X147,X146)|~old(X147,X146)|~event(X147,X148)|~agent(X147,X148,X146)|~present(X147,X148)|~barrel(X147,X148)|~down(X147,X148,X145)|~in(X147,X148,X150)|chevy(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c1116,plain,~actual_world(skolem0001)|~of(skolem0001,X865,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X865)|~placename(skolem0001,X865)|~street(skolem0001,X867)|~lonely(skolem0001,X867)|~chevy(skolem0001,X866)|~white(skolem0001,X866)|~dirty(skolem0001,X866)|~old(skolem0001,X866)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X866)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X867)|chevy(skolem0006,skolem0010),inference(resolution,[status(thm)],[c319, c301])).
% 6.13/6.36 cnf(c2915,plain,~actual_world(skolem0001)|~of(skolem0001,X871,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X871)|~placename(skolem0001,X871)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~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)|chevy(skolem0006,skolem0010),inference(resolution,[status(thm)],[c1116, c283])).
% 6.13/6.36 cnf(c2925,plain,~actual_world(skolem0001)|~of(skolem0001,X872,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X872)|~placename(skolem0001,X872)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|chevy(skolem0006,skolem0010),inference(resolution,[status(thm)],[c2915, c229])).
% 6.13/6.36 cnf(c2938,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|chevy(skolem0006,skolem0010),inference(resolution,[status(thm)],[c2925, c31])).
% 6.13/6.36 cnf(c2952,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|chevy(skolem0006,skolem0010),inference(resolution,[status(thm)],[c2938, c265])).
% 6.13/6.36 cnf(c2963,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|chevy(skolem0006,skolem0010),inference(resolution,[status(thm)],[c2952, c247])).
% 6.13/6.36 cnf(c2969,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|chevy(skolem0006,skolem0010),inference(resolution,[status(thm)],[c2963, c211])).
% 6.13/6.36 cnf(c2983,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|chevy(skolem0006,skolem0010),inference(resolution,[status(thm)],[c2969, c193])).
% 6.13/6.36 cnf(c2991,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|chevy(skolem0006,skolem0010),inference(resolution,[status(thm)],[c2983, c175])).
% 6.13/6.36 cnf(c3005,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|chevy(skolem0006,skolem0010),inference(resolution,[status(thm)],[c2991, c157])).
% 6.13/6.36 cnf(c3014,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|chevy(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3005, c139])).
% 6.13/6.36 cnf(c3031,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|chevy(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3014, c121])).
% 6.13/6.36 cnf(c3038,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|chevy(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3031, c103])).
% 6.13/6.36 cnf(c3054,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|chevy(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3038, c85])).
% 6.13/6.36 cnf(c3063,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|chevy(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3054, c67])).
% 6.13/6.36 cnf(c3069,plain,~actual_world(skolem0001)|chevy(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3063, c49])).
% 6.13/6.36 cnf(c3087,plain,chevy(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3069, c13])).
% 6.13/6.36 cnf(c12,negated_conjecture,actual_world(skolem0001)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c48,negated_conjecture,city(skolem0001,skolem0003)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c66,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c84,negated_conjecture,placename(skolem0001,skolem0002)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c102,negated_conjecture,street(skolem0001,skolem0003)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c120,negated_conjecture,lonely(skolem0001,skolem0003)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c138,negated_conjecture,chevy(skolem0001,skolem0004)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c156,negated_conjecture,white(skolem0001,skolem0004)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c174,negated_conjecture,dirty(skolem0001,skolem0004)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c192,negated_conjecture,old(skolem0001,skolem0004)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c210,negated_conjecture,event(skolem0001,skolem0005)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c246,negated_conjecture,present(skolem0001,skolem0005)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c264,negated_conjecture,barrel(skolem0001,skolem0005)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c30,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c228,negated_conjecture,agent(skolem0001,skolem0005,skolem0004)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c282,negated_conjecture,down(skolem0001,skolem0005,skolem0003)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c300,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c318,negated_conjecture,~actual_world(X136)|~of(X136,X138,X139)|~city(X136,X139)|~hollywood_placename(X136,X138)|~placename(X136,X138)|~street(X136,X134)|~lonely(X136,X134)|~chevy(X136,X135)|~white(X136,X135)|~dirty(X136,X135)|~old(X136,X135)|~event(X136,X137)|~agent(X136,X137,X135)|~present(X136,X137)|~barrel(X136,X137)|~down(X136,X137,X134)|~in(X136,X137,X139)|lonely(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.36 cnf(c1062,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,X782)|~white(skolem0001,X782)|~dirty(skolem0001,X782)|~old(skolem0001,X782)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X782)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X783)|lonely(skolem0006,skolem0009),inference(resolution,[status(thm)],[c318, c300])).
% 6.13/6.36 cnf(c2725,plain,~actual_world(skolem0001)|~of(skolem0001,X785,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X785)|~placename(skolem0001,X785)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,X786)|~white(skolem0001,X786)|~dirty(skolem0001,X786)|~old(skolem0001,X786)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X786)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|lonely(skolem0006,skolem0009),inference(resolution,[status(thm)],[c1062, c282])).
% 6.13/6.36 cnf(c2742,plain,~actual_world(skolem0001)|~of(skolem0001,X787,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X787)|~placename(skolem0001,X787)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|lonely(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2725, c228])).
% 6.13/6.36 cnf(c2748,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|lonely(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2742, c30])).
% 6.13/6.36 cnf(c2764,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|lonely(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2748, c264])).
% 6.13/6.36 cnf(c2774,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|lonely(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2764, c246])).
% 6.13/6.37 cnf(c2790,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|lonely(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2774, c210])).
% 6.13/6.37 cnf(c2799,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|lonely(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2790, c192])).
% 6.13/6.37 cnf(c2815,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|lonely(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2799, c174])).
% 6.13/6.37 cnf(c2821,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|lonely(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2815, c156])).
% 6.13/6.37 cnf(c2829,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|lonely(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2821, c138])).
% 6.13/6.37 cnf(c2852,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|lonely(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2829, c120])).
% 6.13/6.37 cnf(c2860,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|lonely(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2852, c102])).
% 6.13/6.37 cnf(c2871,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|lonely(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2860, c84])).
% 6.13/6.37 cnf(c2885,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|lonely(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2871, c66])).
% 6.13/6.37 cnf(c2890,plain,~actual_world(skolem0001)|lonely(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2885, c48])).
% 6.13/6.37 cnf(c2901,plain,lonely(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2890, c12])).
% 6.13/6.37 cnf(c11,negated_conjecture,actual_world(skolem0001)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c47,negated_conjecture,city(skolem0001,skolem0003)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c65,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c83,negated_conjecture,placename(skolem0001,skolem0002)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c101,negated_conjecture,street(skolem0001,skolem0003)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c119,negated_conjecture,lonely(skolem0001,skolem0003)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c137,negated_conjecture,chevy(skolem0001,skolem0004)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c155,negated_conjecture,white(skolem0001,skolem0004)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c173,negated_conjecture,dirty(skolem0001,skolem0004)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c191,negated_conjecture,old(skolem0001,skolem0004)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c209,negated_conjecture,event(skolem0001,skolem0005)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c245,negated_conjecture,present(skolem0001,skolem0005)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c263,negated_conjecture,barrel(skolem0001,skolem0005)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c29,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c227,negated_conjecture,agent(skolem0001,skolem0005,skolem0004)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c281,negated_conjecture,down(skolem0001,skolem0005,skolem0003)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c299,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c317,negated_conjecture,~actual_world(X130)|~of(X130,X132,X133)|~city(X130,X133)|~hollywood_placename(X130,X132)|~placename(X130,X132)|~street(X130,X128)|~lonely(X130,X128)|~chevy(X130,X129)|~white(X130,X129)|~dirty(X130,X129)|~old(X130,X129)|~event(X130,X131)|~agent(X130,X131,X129)|~present(X130,X131)|~barrel(X130,X131)|~down(X130,X131,X128)|~in(X130,X131,X133)|street(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c1022,plain,~actual_world(skolem0001)|~of(skolem0001,X692,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X692)|~placename(skolem0001,X692)|~street(skolem0001,X690)|~lonely(skolem0001,X690)|~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,X690)|street(skolem0006,skolem0009),inference(resolution,[status(thm)],[c317, c299])).
% 6.13/6.37 cnf(c2523,plain,~actual_world(skolem0001)|~of(skolem0001,X693,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X693)|~placename(skolem0001,X693)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,X694)|~white(skolem0001,X694)|~dirty(skolem0001,X694)|~old(skolem0001,X694)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X694)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|street(skolem0006,skolem0009),inference(resolution,[status(thm)],[c1022, c281])).
% 6.13/6.37 cnf(c2538,plain,~actual_world(skolem0001)|~of(skolem0001,X697,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X697)|~placename(skolem0001,X697)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|street(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2523, c227])).
% 6.13/6.37 cnf(c2543,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|street(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2538, c29])).
% 6.13/6.37 cnf(c2558,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|street(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2543, c263])).
% 6.13/6.37 cnf(c2570,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|street(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2558, c245])).
% 6.13/6.37 cnf(c2589,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|street(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2570, c209])).
% 6.13/6.37 cnf(c2595,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|street(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2589, c191])).
% 6.13/6.37 cnf(c2612,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|street(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2595, c173])).
% 6.13/6.37 cnf(c2621,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|street(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2612, c155])).
% 6.13/6.37 cnf(c2639,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|street(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2621, c137])).
% 6.13/6.37 cnf(c2650,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|street(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2639, c119])).
% 6.13/6.37 cnf(c2660,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|street(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2650, c101])).
% 6.13/6.37 cnf(c2672,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|street(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2660, c83])).
% 6.13/6.37 cnf(c2688,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|street(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2672, c65])).
% 6.13/6.37 cnf(c2706,plain,~actual_world(skolem0001)|street(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2688, c47])).
% 6.13/6.37 cnf(c2709,plain,street(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2706, c11])).
% 6.13/6.37 cnf(c10,negated_conjecture,actual_world(skolem0001)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c46,negated_conjecture,city(skolem0001,skolem0003)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c64,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c82,negated_conjecture,placename(skolem0001,skolem0002)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c100,negated_conjecture,street(skolem0001,skolem0003)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c118,negated_conjecture,lonely(skolem0001,skolem0003)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c136,negated_conjecture,chevy(skolem0001,skolem0004)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c154,negated_conjecture,white(skolem0001,skolem0004)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c172,negated_conjecture,dirty(skolem0001,skolem0004)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c190,negated_conjecture,old(skolem0001,skolem0004)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c208,negated_conjecture,event(skolem0001,skolem0005)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c244,negated_conjecture,present(skolem0001,skolem0005)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c262,negated_conjecture,barrel(skolem0001,skolem0005)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c28,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c226,negated_conjecture,agent(skolem0001,skolem0005,skolem0004)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c280,negated_conjecture,down(skolem0001,skolem0005,skolem0003)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c298,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c316,negated_conjecture,~actual_world(X124)|~of(X124,X126,X127)|~city(X124,X127)|~hollywood_placename(X124,X126)|~placename(X124,X126)|~street(X124,X122)|~lonely(X124,X122)|~chevy(X124,X123)|~white(X124,X123)|~dirty(X124,X123)|~old(X124,X123)|~event(X124,X125)|~agent(X124,X125,X123)|~present(X124,X125)|~barrel(X124,X125)|~down(X124,X125,X122)|~in(X124,X125,X127)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c986,plain,~actual_world(skolem0001)|~of(skolem0001,X593,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X593)|~placename(skolem0001,X593)|~street(skolem0001,X594)|~lonely(skolem0001,X594)|~chevy(skolem0001,X595)|~white(skolem0001,X595)|~dirty(skolem0001,X595)|~old(skolem0001,X595)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X595)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X594)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c316, c298])).
% 6.13/6.37 cnf(c2291,plain,~actual_world(skolem0001)|~of(skolem0001,X597,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X597)|~placename(skolem0001,X597)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~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)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c986, c280])).
% 6.13/6.37 cnf(c2304,plain,~actual_world(skolem0001)|~of(skolem0001,X598,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X598)|~placename(skolem0001,X598)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2291, c226])).
% 6.13/6.37 cnf(c2320,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2304, c28])).
% 6.13/6.37 cnf(c2337,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2320, c262])).
% 6.13/6.37 cnf(c2353,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2337, c244])).
% 6.13/6.37 cnf(c2368,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2353, c208])).
% 6.13/6.37 cnf(c2386,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2368, c190])).
% 6.13/6.37 cnf(c2394,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2386, c172])).
% 6.13/6.37 cnf(c2410,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2394, c154])).
% 6.13/6.37 cnf(c2423,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2410, c136])).
% 6.13/6.37 cnf(c2441,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2423, c118])).
% 6.13/6.37 cnf(c2444,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2441, c100])).
% 6.13/6.37 cnf(c2463,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2444, c82])).
% 6.13/6.37 cnf(c2479,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2463, c64])).
% 6.13/6.37 cnf(c2493,plain,~actual_world(skolem0001)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2479, c46])).
% 6.13/6.37 cnf(c2502,plain,placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2493, c10])).
% 6.13/6.37 cnf(c9,negated_conjecture,actual_world(skolem0001)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c45,negated_conjecture,city(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c63,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c81,negated_conjecture,placename(skolem0001,skolem0002)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c99,negated_conjecture,street(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c117,negated_conjecture,lonely(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c135,negated_conjecture,chevy(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c153,negated_conjecture,white(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c171,negated_conjecture,dirty(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c189,negated_conjecture,old(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c207,negated_conjecture,event(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c243,negated_conjecture,present(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c261,negated_conjecture,barrel(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c27,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c225,negated_conjecture,agent(skolem0001,skolem0005,skolem0004)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c279,negated_conjecture,down(skolem0001,skolem0005,skolem0003)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c297,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c315,negated_conjecture,~actual_world(X118)|~of(X118,X120,X121)|~city(X118,X121)|~hollywood_placename(X118,X120)|~placename(X118,X120)|~street(X118,X116)|~lonely(X118,X116)|~chevy(X118,X117)|~white(X118,X117)|~dirty(X118,X117)|~old(X118,X117)|~event(X118,X119)|~agent(X118,X119,X117)|~present(X118,X119)|~barrel(X118,X119)|~down(X118,X119,X116)|~in(X118,X119,X121)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c950,plain,~actual_world(skolem0001)|~of(skolem0001,X488,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X488)|~placename(skolem0001,X488)|~street(skolem0001,X487)|~lonely(skolem0001,X487)|~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,X487)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c315, c297])).
% 6.13/6.37 cnf(c2059,plain,~actual_world(skolem0001)|~of(skolem0001,X490,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X490)|~placename(skolem0001,X490)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~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)],[c950, c279])).
% 6.13/6.37 cnf(c2069,plain,~actual_world(skolem0001)|~of(skolem0001,X492,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X492)|~placename(skolem0001,X492)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2059, c225])).
% 6.13/6.37 cnf(c2089,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2069, c27])).
% 6.13/6.37 cnf(c2101,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2089, c261])).
% 6.13/6.37 cnf(c2119,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2101, c243])).
% 6.13/6.37 cnf(c2128,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2119, c207])).
% 6.13/6.37 cnf(c2146,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2128, c189])).
% 6.13/6.37 cnf(c2157,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2146, c171])).
% 6.13/6.37 cnf(c2173,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2157, c153])).
% 6.13/6.37 cnf(c2189,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2173, c135])).
% 6.13/6.37 cnf(c2203,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2189, c117])).
% 6.13/6.37 cnf(c2217,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2203, c99])).
% 6.13/6.37 cnf(c2242,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2217, c81])).
% 6.13/6.37 cnf(c2254,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2242, c63])).
% 6.13/6.37 cnf(c2267,plain,~actual_world(skolem0001)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2254, c45])).
% 6.13/6.37 cnf(c2274,plain,hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2267, c9])).
% 6.13/6.37 cnf(c8,negated_conjecture,actual_world(skolem0001)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c44,negated_conjecture,city(skolem0001,skolem0003)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c62,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c80,negated_conjecture,placename(skolem0001,skolem0002)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c98,negated_conjecture,street(skolem0001,skolem0003)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c116,negated_conjecture,lonely(skolem0001,skolem0003)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c134,negated_conjecture,chevy(skolem0001,skolem0004)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c152,negated_conjecture,white(skolem0001,skolem0004)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c170,negated_conjecture,dirty(skolem0001,skolem0004)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c188,negated_conjecture,old(skolem0001,skolem0004)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c206,negated_conjecture,event(skolem0001,skolem0005)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c242,negated_conjecture,present(skolem0001,skolem0005)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c260,negated_conjecture,barrel(skolem0001,skolem0005)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c26,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c224,negated_conjecture,agent(skolem0001,skolem0005,skolem0004)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c278,negated_conjecture,down(skolem0001,skolem0005,skolem0003)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c296,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c314,negated_conjecture,~actual_world(X112)|~of(X112,X114,X115)|~city(X112,X115)|~hollywood_placename(X112,X114)|~placename(X112,X114)|~street(X112,X110)|~lonely(X112,X110)|~chevy(X112,X111)|~white(X112,X111)|~dirty(X112,X111)|~old(X112,X111)|~event(X112,X113)|~agent(X112,X113,X111)|~present(X112,X113)|~barrel(X112,X113)|~down(X112,X113,X110)|~in(X112,X113,X115)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c923,plain,~actual_world(skolem0001)|~of(skolem0001,X376,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X376)|~placename(skolem0001,X376)|~street(skolem0001,X375)|~lonely(skolem0001,X375)|~chevy(skolem0001,X374)|~white(skolem0001,X374)|~dirty(skolem0001,X374)|~old(skolem0001,X374)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X374)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X375)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c314, c296])).
% 6.13/6.37 cnf(c1798,plain,~actual_world(skolem0001)|~of(skolem0001,X379,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X379)|~placename(skolem0001,X379)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,X380)|~white(skolem0001,X380)|~dirty(skolem0001,X380)|~old(skolem0001,X380)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X380)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c923, c278])).
% 6.13/6.37 cnf(c1811,plain,~actual_world(skolem0001)|~of(skolem0001,X381,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X381)|~placename(skolem0001,X381)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c1798, c224])).
% 6.13/6.37 cnf(c1834,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c1811, c26])).
% 6.13/6.37 cnf(c1851,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c1834, c260])).
% 6.13/6.37 cnf(c1865,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c1851, c242])).
% 6.13/6.37 cnf(c1877,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c1865, c206])).
% 6.13/6.37 cnf(c1900,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c1877, c188])).
% 6.13/6.37 cnf(c1906,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c1900, c170])).
% 6.13/6.37 cnf(c1922,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c1906, c152])).
% 6.13/6.37 cnf(c1939,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c1922, c134])).
% 6.13/6.37 cnf(c1968,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c1939, c116])).
% 6.13/6.37 cnf(c1971,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c1968, c98])).
% 6.13/6.37 cnf(c1986,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c1971, c80])).
% 6.13/6.37 cnf(c2015,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c1986, c62])).
% 6.13/6.37 cnf(c2025,plain,~actual_world(skolem0001)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c2015, c44])).
% 6.13/6.37 cnf(c2037,plain,city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c2025, c8])).
% 6.13/6.37 cnf(c6,negated_conjecture,actual_world(skolem0001)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c42,negated_conjecture,city(skolem0001,skolem0003)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c60,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c78,negated_conjecture,placename(skolem0001,skolem0002)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c96,negated_conjecture,street(skolem0001,skolem0003)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c114,negated_conjecture,lonely(skolem0001,skolem0003)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c132,negated_conjecture,chevy(skolem0001,skolem0004)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c150,negated_conjecture,white(skolem0001,skolem0004)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c168,negated_conjecture,dirty(skolem0001,skolem0004)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c186,negated_conjecture,old(skolem0001,skolem0004)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c204,negated_conjecture,event(skolem0001,skolem0005)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c240,negated_conjecture,present(skolem0001,skolem0005)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c258,negated_conjecture,barrel(skolem0001,skolem0005)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c24,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c222,negated_conjecture,agent(skolem0001,skolem0005,skolem0004)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c276,negated_conjecture,down(skolem0001,skolem0005,skolem0003)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c294,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c312,negated_conjecture,~actual_world(X101)|~of(X101,X103,X104)|~city(X101,X104)|~hollywood_placename(X101,X103)|~placename(X101,X103)|~street(X101,X99)|~lonely(X101,X99)|~chevy(X101,X100)|~white(X101,X100)|~dirty(X101,X100)|~old(X101,X100)|~event(X101,X102)|~agent(X101,X102,X100)|~present(X101,X102)|~barrel(X101,X102)|~down(X101,X102,X99)|~in(X101,X102,X104)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 6.13/6.37 cnf(c862,plain,~actual_world(skolem0001)|~of(skolem0001,X223,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X223)|~placename(skolem0001,X223)|~street(skolem0001,X222)|~lonely(skolem0001,X222)|~chevy(skolem0001,X224)|~white(skolem0001,X224)|~dirty(skolem0001,X224)|~old(skolem0001,X224)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X224)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X222)|actual_world(skolem0006),inference(resolution,[status(thm)],[c312, c294])).
% 6.13/6.37 cnf(c1521,plain,~actual_world(skolem0001)|~of(skolem0001,X226,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X226)|~placename(skolem0001,X226)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,X225)|~white(skolem0001,X225)|~dirty(skolem0001,X225)|~old(skolem0001,X225)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X225)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|actual_world(skolem0006),inference(resolution,[status(thm)],[c862, c276])).
% 6.13/6.37 cnf(c1548,plain,~actual_world(skolem0001)|~of(skolem0001,X227,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X227)|~placename(skolem0001,X227)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1521, c222])).
% 6.13/6.37 cnf(c1558,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1548, c24])).
% 6.13/6.37 cnf(c1574,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1558, c258])).
% 6.13/6.37 cnf(c1590,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1574, c240])).
% 6.13/6.37 cnf(c1606,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1590, c204])).
% 6.13/6.37 cnf(c1623,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1606, c186])).
% 6.13/6.37 cnf(c1641,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1623, c168])).
% 6.13/6.37 cnf(c1663,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1641, c150])).
% 6.13/6.37 cnf(c1679,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|~lonely(skolem0001,skolem0003)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1663, c132])).
% 6.13/6.37 cnf(c1694,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~street(skolem0001,skolem0003)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1679, c114])).
% 6.13/6.37 cnf(c1713,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1694, c96])).
% 6.13/6.37 cnf(c1737,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1713, c78])).
% 6.13/6.37 cnf(c1750,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1737, c60])).
% 6.13/6.37 cnf(c1764,plain,~actual_world(skolem0001)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1750, c42])).
% 6.13/6.37 cnf(c1783,plain,actual_world(skolem0006),inference(resolution,[status(thm)],[c1764, c6])).
% 6.13/6.37 % SZS output end Saturation
% 6.13/6.37
% 6.13/6.37 % Initial clauses : 324
% 6.13/6.37 % Processed clauses : 642
% 6.13/6.37 % Factors computed : 6
% 6.13/6.37 % Resolvents computed: 3661
% 6.13/6.37 % Tautologies deleted: 221
% 6.13/6.37 % Forward subsumed : 3128
% 6.13/6.37 % Backward subsumed : 622
% 6.13/6.37 % -------- CPU Time ---------
% 6.13/6.37 % User time : 5.980 s
% 6.13/6.37 % System time : 0.034 s
% 6.13/6.37 % Total time : 6.014 s
%------------------------------------------------------------------------------