PyRes---1.5.CSA-Sat.s

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

% Computer : n012.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:13 EDT 2024

% Result   : CounterSatisfiable 7.50s 7.69s
% Output   : Saturation 7.56s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12  % Problem  : NLP123+1 : TPTP v8.1.2. Released v2.4.0.
% 0.03/0.13  % Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34  % Computer : n012.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:47:37 EDT 2024
% 0.14/0.34  % CPUTime  : 
% 7.50/7.69  % Version:  1.5
% 7.50/7.69  % SZS status CounterSatisfiable
% 7.50/7.69  % SZS output start Saturation
% 7.50/7.69  fof(co1,conjecture,(~(~(((?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(((((((((((((((of(U,V,W)&city(U,W))&hollywood_placename(U,V))&placename(U,V))&chevy(U,W))&white(U,W))&dirty(U,W))&old(U,W))&street(U,X))&lonely(U,X))&event(U,Y))&agent(U,Y,W))&present(U,Y))&barrel(U,Y))&down(U,Y,X))&in(U,Y,W))))))))=>(?[Z]:(actual_world(Z)&(?[X1]:(?[X2]:(?[X3]:(?[X4]:(?[X5]:(((((((((((((((of(Z,X2,X1)&city(Z,X1))&hollywood_placename(Z,X2))&placename(Z,X2))&chevy(Z,X3))&white(Z,X3))&dirty(Z,X3))&old(Z,X3))&street(Z,X4))&lonely(Z,X4))&event(Z,X5))&agent(Z,X5,X3))&present(Z,X5))&barrel(Z,X5))&down(Z,X5,X4))&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))&chevy(Z,X3))&white(Z,X3))&dirty(Z,X3))&old(Z,X3))&street(Z,X4))&lonely(Z,X4))&event(Z,X5))&agent(Z,X5,X3))&present(Z,X5))&barrel(Z,X5))&down(Z,X5,X4))&in(Z,X5,X1)))))))))=>(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(((((((((((((((of(U,V,W)&city(U,W))&hollywood_placename(U,V))&placename(U,V))&chevy(U,W))&white(U,W))&dirty(U,W))&old(U,W))&street(U,X))&lonely(U,X))&event(U,Y))&agent(U,Y,W))&present(U,Y))&barrel(U,Y))&down(U,Y,X))&in(U,Y,W)))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', co1)).
% 7.50/7.69  fof(c0,negated_conjecture,(~(~(~(((?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(((((((((((((((of(U,V,W)&city(U,W))&hollywood_placename(U,V))&placename(U,V))&chevy(U,W))&white(U,W))&dirty(U,W))&old(U,W))&street(U,X))&lonely(U,X))&event(U,Y))&agent(U,Y,W))&present(U,Y))&barrel(U,Y))&down(U,Y,X))&in(U,Y,W))))))))=>(?[Z]:(actual_world(Z)&(?[X1]:(?[X2]:(?[X3]:(?[X4]:(?[X5]:(((((((((((((((of(Z,X2,X1)&city(Z,X1))&hollywood_placename(Z,X2))&placename(Z,X2))&chevy(Z,X3))&white(Z,X3))&dirty(Z,X3))&old(Z,X3))&street(Z,X4))&lonely(Z,X4))&event(Z,X5))&agent(Z,X5,X3))&present(Z,X5))&barrel(Z,X5))&down(Z,X5,X4))&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))&chevy(Z,X3))&white(Z,X3))&dirty(Z,X3))&old(Z,X3))&street(Z,X4))&lonely(Z,X4))&event(Z,X5))&agent(Z,X5,X3))&present(Z,X5))&barrel(Z,X5))&down(Z,X5,X4))&in(Z,X5,X1)))))))))=>(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(((((((((((((((of(U,V,W)&city(U,W))&hollywood_placename(U,V))&placename(U,V))&chevy(U,W))&white(U,W))&dirty(U,W))&old(U,W))&street(U,X))&lonely(U,X))&event(U,Y))&agent(U,Y,W))&present(U,Y))&barrel(U,Y))&down(U,Y,X))&in(U,Y,W))))))))))))),inference(assume_negation,[status(cth)],[co1])).
% 7.50/7.69  fof(c1,negated_conjecture,(((?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(((((((((((((((of(U,V,W)&city(U,W))&hollywood_placename(U,V))&placename(U,V))&chevy(U,W))&white(U,W))&dirty(U,W))&old(U,W))&street(U,X))&lonely(U,X))&event(U,Y))&agent(U,Y,W))&present(U,Y))&barrel(U,Y))&down(U,Y,X))&in(U,Y,W))))))))&(![Z]:(~actual_world(Z)|(![X1]:(![X2]:(![X3]:(![X4]:(![X5]:(((((((((((((((~of(Z,X2,X1)|~city(Z,X1))|~hollywood_placename(Z,X2))|~placename(Z,X2))|~chevy(Z,X3))|~white(Z,X3))|~dirty(Z,X3))|~old(Z,X3))|~street(Z,X4))|~lonely(Z,X4))|~event(Z,X5))|~agent(Z,X5,X3))|~present(Z,X5))|~barrel(Z,X5))|~down(Z,X5,X4))|~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))&chevy(Z,X3))&white(Z,X3))&dirty(Z,X3))&old(Z,X3))&street(Z,X4))&lonely(Z,X4))&event(Z,X5))&agent(Z,X5,X3))&present(Z,X5))&barrel(Z,X5))&down(Z,X5,X4))&in(Z,X5,X1)))))))))&(![U]:(~actual_world(U)|(![V]:(![W]:(![X]:(![Y]:(((((((((((((((~of(U,V,W)|~city(U,W))|~hollywood_placename(U,V))|~placename(U,V))|~chevy(U,W))|~white(U,W))|~dirty(U,W))|~old(U,W))|~street(U,X))|~lonely(U,X))|~event(U,Y))|~agent(U,Y,W))|~present(U,Y))|~barrel(U,Y))|~down(U,Y,X))|~in(U,Y,W)))))))))),inference(fof_nnf,[status(thm)],[c0])).
% 7.50/7.69  fof(c2,negated_conjecture,(((?[X2]:(actual_world(X2)&(?[X3]:(?[X4]:(?[X5]:(?[X6]:(((((((((((((((of(X2,X3,X4)&city(X2,X4))&hollywood_placename(X2,X3))&placename(X2,X3))&chevy(X2,X4))&white(X2,X4))&dirty(X2,X4))&old(X2,X4))&street(X2,X5))&lonely(X2,X5))&event(X2,X6))&agent(X2,X6,X4))&present(X2,X6))&barrel(X2,X6))&down(X2,X6,X5))&in(X2,X6,X4))))))))&(![X7]:(~actual_world(X7)|(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~street(X7,X11))|~lonely(X7,X11))|~event(X7,X12))|~agent(X7,X12,X10))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X11))|~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))&chevy(X13,X16))&white(X13,X16))&dirty(X13,X16))&old(X13,X16))&street(X13,X17))&lonely(X13,X17))&event(X13,X18))&agent(X13,X18,X16))&present(X13,X18))&barrel(X13,X18))&down(X13,X18,X17))&in(X13,X18,X14)))))))))&(![X19]:(~actual_world(X19)|(![X20]:(![X21]:(![X22]:(![X23]:(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21)))))))))),inference(variable_rename,[status(thm)],[c1])).
% 7.50/7.69  fof(c4,negated_conjecture,(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(((actual_world(skolem0001)&(((((((((((((((of(skolem0001,skolem0002,skolem0003)&city(skolem0001,skolem0003))&hollywood_placename(skolem0001,skolem0002))&placename(skolem0001,skolem0002))&chevy(skolem0001,skolem0003))&white(skolem0001,skolem0003))&dirty(skolem0001,skolem0003))&old(skolem0001,skolem0003))&street(skolem0001,skolem0004))&lonely(skolem0001,skolem0004))&event(skolem0001,skolem0005))&agent(skolem0001,skolem0005,skolem0003))&present(skolem0001,skolem0005))&barrel(skolem0001,skolem0005))&down(skolem0001,skolem0005,skolem0004))&in(skolem0001,skolem0005,skolem0003)))&(~actual_world(X7)|(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~street(X7,X11))|~lonely(X7,X11))|~event(X7,X12))|~agent(X7,X12,X10))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X11))|~in(X7,X12,X8))))|((actual_world(skolem0006)&(((((((((((((((of(skolem0006,skolem0008,skolem0007)&city(skolem0006,skolem0007))&hollywood_placename(skolem0006,skolem0008))&placename(skolem0006,skolem0008))&chevy(skolem0006,skolem0009))&white(skolem0006,skolem0009))&dirty(skolem0006,skolem0009))&old(skolem0006,skolem0009))&street(skolem0006,skolem0010))&lonely(skolem0006,skolem0010))&event(skolem0006,skolem0011))&agent(skolem0006,skolem0011,skolem0009))&present(skolem0006,skolem0011))&barrel(skolem0006,skolem0011))&down(skolem0006,skolem0011,skolem0010))&in(skolem0006,skolem0011,skolem0007)))&(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21)))))))))))))))),inference(shift_quantors,[status(thm)],[fof(c3,negated_conjecture,(((actual_world(skolem0001)&(((((((((((((((of(skolem0001,skolem0002,skolem0003)&city(skolem0001,skolem0003))&hollywood_placename(skolem0001,skolem0002))&placename(skolem0001,skolem0002))&chevy(skolem0001,skolem0003))&white(skolem0001,skolem0003))&dirty(skolem0001,skolem0003))&old(skolem0001,skolem0003))&street(skolem0001,skolem0004))&lonely(skolem0001,skolem0004))&event(skolem0001,skolem0005))&agent(skolem0001,skolem0005,skolem0003))&present(skolem0001,skolem0005))&barrel(skolem0001,skolem0005))&down(skolem0001,skolem0005,skolem0004))&in(skolem0001,skolem0005,skolem0003)))&(![X7]:(~actual_world(X7)|(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~street(X7,X11))|~lonely(X7,X11))|~event(X7,X12))|~agent(X7,X12,X10))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X11))|~in(X7,X12,X8))))))))))|((actual_world(skolem0006)&(((((((((((((((of(skolem0006,skolem0008,skolem0007)&city(skolem0006,skolem0007))&hollywood_placename(skolem0006,skolem0008))&placename(skolem0006,skolem0008))&chevy(skolem0006,skolem0009))&white(skolem0006,skolem0009))&dirty(skolem0006,skolem0009))&old(skolem0006,skolem0009))&street(skolem0006,skolem0010))&lonely(skolem0006,skolem0010))&event(skolem0006,skolem0011))&agent(skolem0006,skolem0011,skolem0009))&present(skolem0006,skolem0011))&barrel(skolem0006,skolem0011))&down(skolem0006,skolem0011,skolem0010))&in(skolem0006,skolem0011,skolem0007)))&(![X19]:(~actual_world(X19)|(![X20]:(![X21]:(![X22]:(![X23]:(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21)))))))))),inference(skolemize,[status(esa)],[c2])).])).
% 7.50/7.70  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)|chevy(skolem0006,skolem0009)))&(actual_world(skolem0001)|white(skolem0006,skolem0009)))&(actual_world(skolem0001)|dirty(skolem0006,skolem0009)))&(actual_world(skolem0001)|old(skolem0006,skolem0009)))&(actual_world(skolem0001)|street(skolem0006,skolem0010)))&(actual_world(skolem0001)|lonely(skolem0006,skolem0010)))&(actual_world(skolem0001)|event(skolem0006,skolem0011)))&(actual_world(skolem0001)|agent(skolem0006,skolem0011,skolem0009)))&(actual_world(skolem0001)|present(skolem0006,skolem0011)))&(actual_world(skolem0001)|barrel(skolem0006,skolem0011)))&(actual_world(skolem0001)|down(skolem0006,skolem0011,skolem0010)))&(actual_world(skolem0001)|in(skolem0006,skolem0011,skolem0007))))&(actual_world(skolem0001)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21)))))&((((((((((((((((((of(skolem0001,skolem0002,skolem0003)|actual_world(skolem0006))&((((((((((((((((of(skolem0001,skolem0002,skolem0003)|of(skolem0006,skolem0008,skolem0007))&(of(skolem0001,skolem0002,skolem0003)|city(skolem0006,skolem0007)))&(of(skolem0001,skolem0002,skolem0003)|hollywood_placename(skolem0006,skolem0008)))&(of(skolem0001,skolem0002,skolem0003)|placename(skolem0006,skolem0008)))&(of(skolem0001,skolem0002,skolem0003)|chevy(skolem0006,skolem0009)))&(of(skolem0001,skolem0002,skolem0003)|white(skolem0006,skolem0009)))&(of(skolem0001,skolem0002,skolem0003)|dirty(skolem0006,skolem0009)))&(of(skolem0001,skolem0002,skolem0003)|old(skolem0006,skolem0009)))&(of(skolem0001,skolem0002,skolem0003)|street(skolem0006,skolem0010)))&(of(skolem0001,skolem0002,skolem0003)|lonely(skolem0006,skolem0010)))&(of(skolem0001,skolem0002,skolem0003)|event(skolem0006,skolem0011)))&(of(skolem0001,skolem0002,skolem0003)|agent(skolem0006,skolem0011,skolem0009)))&(of(skolem0001,skolem0002,skolem0003)|present(skolem0006,skolem0011)))&(of(skolem0001,skolem0002,skolem0003)|barrel(skolem0006,skolem0011)))&(of(skolem0001,skolem0002,skolem0003)|down(skolem0006,skolem0011,skolem0010)))&(of(skolem0001,skolem0002,skolem0003)|in(skolem0006,skolem0011,skolem0007))))&(of(skolem0001,skolem0002,skolem0003)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21)))))&(((city(skolem0001,skolem0003)|actual_world(skolem0006))&((((((((((((((((city(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007))&(city(skolem0001,skolem0003)|city(skolem0006,skolem0007)))&(city(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008)))&(city(skolem0001,skolem0003)|placename(skolem0006,skolem0008)))&(city(skolem0001,skolem0003)|chevy(skolem0006,skolem0009)))&(city(skolem0001,skolem0003)|white(skolem0006,skolem0009)))&(city(skolem0001,skolem0003)|dirty(skolem0006,skolem0009)))&(city(skolem0001,skolem0003)|old(skolem0006,skolem0009)))&(city(skolem0001,skolem0003)|street(skolem0006,skolem0010)))&(city(skolem0001,skolem0003)|lonely(skolem0006,skolem0010)))&(city(skolem0001,skolem0003)|event(skolem0006,skolem0011)))&(city(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0009)))&(city(skolem0001,skolem0003)|present(skolem0006,skolem0011)))&(city(skolem0001,skolem0003)|barrel(skolem0006,skolem0011)))&(city(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0010)))&(city(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007))))&(city(skolem0001,skolem0003)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21))))))&(((hollywood_placename(skolem0001,skolem0002)|actual_world(skolem0006))&((((((((((((((((hollywood_placename(skolem0001,skolem0002)|of(skolem0006,skolem0008,skolem0007))&(hollywood_placename(skolem0001,skolem0002)|city(skolem0006,skolem0007)))&(hollywood_placename(skolem0001,skolem0002)|hollywood_placename(skolem0006,skolem0008)))&(hollywood_placename(skolem0001,skolem0002)|placename(skolem0006,skolem0008)))&(hollywood_placename(skolem0001,skolem0002)|chevy(skolem0006,skolem0009)))&(hollywood_placename(skolem0001,skolem0002)|white(skolem0006,skolem0009)))&(hollywood_placename(skolem0001,skolem0002)|dirty(skolem0006,skolem0009)))&(hollywood_placename(skolem0001,skolem0002)|old(skolem0006,skolem0009)))&(hollywood_placename(skolem0001,skolem0002)|street(skolem0006,skolem0010)))&(hollywood_placename(skolem0001,skolem0002)|lonely(skolem0006,skolem0010)))&(hollywood_placename(skolem0001,skolem0002)|event(skolem0006,skolem0011)))&(hollywood_placename(skolem0001,skolem0002)|agent(skolem0006,skolem0011,skolem0009)))&(hollywood_placename(skolem0001,skolem0002)|present(skolem0006,skolem0011)))&(hollywood_placename(skolem0001,skolem0002)|barrel(skolem0006,skolem0011)))&(hollywood_placename(skolem0001,skolem0002)|down(skolem0006,skolem0011,skolem0010)))&(hollywood_placename(skolem0001,skolem0002)|in(skolem0006,skolem0011,skolem0007))))&(hollywood_placename(skolem0001,skolem0002)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21))))))&(((placename(skolem0001,skolem0002)|actual_world(skolem0006))&((((((((((((((((placename(skolem0001,skolem0002)|of(skolem0006,skolem0008,skolem0007))&(placename(skolem0001,skolem0002)|city(skolem0006,skolem0007)))&(placename(skolem0001,skolem0002)|hollywood_placename(skolem0006,skolem0008)))&(placename(skolem0001,skolem0002)|placename(skolem0006,skolem0008)))&(placename(skolem0001,skolem0002)|chevy(skolem0006,skolem0009)))&(placename(skolem0001,skolem0002)|white(skolem0006,skolem0009)))&(placename(skolem0001,skolem0002)|dirty(skolem0006,skolem0009)))&(placename(skolem0001,skolem0002)|old(skolem0006,skolem0009)))&(placename(skolem0001,skolem0002)|street(skolem0006,skolem0010)))&(placename(skolem0001,skolem0002)|lonely(skolem0006,skolem0010)))&(placename(skolem0001,skolem0002)|event(skolem0006,skolem0011)))&(placename(skolem0001,skolem0002)|agent(skolem0006,skolem0011,skolem0009)))&(placename(skolem0001,skolem0002)|present(skolem0006,skolem0011)))&(placename(skolem0001,skolem0002)|barrel(skolem0006,skolem0011)))&(placename(skolem0001,skolem0002)|down(skolem0006,skolem0011,skolem0010)))&(placename(skolem0001,skolem0002)|in(skolem0006,skolem0011,skolem0007))))&(placename(skolem0001,skolem0002)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21))))))&(((chevy(skolem0001,skolem0003)|actual_world(skolem0006))&((((((((((((((((chevy(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007))&(chevy(skolem0001,skolem0003)|city(skolem0006,skolem0007)))&(chevy(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008)))&(chevy(skolem0001,skolem0003)|placename(skolem0006,skolem0008)))&(chevy(skolem0001,skolem0003)|chevy(skolem0006,skolem0009)))&(chevy(skolem0001,skolem0003)|white(skolem0006,skolem0009)))&(chevy(skolem0001,skolem0003)|dirty(skolem0006,skolem0009)))&(chevy(skolem0001,skolem0003)|old(skolem0006,skolem0009)))&(chevy(skolem0001,skolem0003)|street(skolem0006,skolem0010)))&(chevy(skolem0001,skolem0003)|lonely(skolem0006,skolem0010)))&(chevy(skolem0001,skolem0003)|event(skolem0006,skolem0011)))&(chevy(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0009)))&(chevy(skolem0001,skolem0003)|present(skolem0006,skolem0011)))&(chevy(skolem0001,skolem0003)|barrel(skolem0006,skolem0011)))&(chevy(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0010)))&(chevy(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007))))&(chevy(skolem0001,skolem0003)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21))))))&(((white(skolem0001,skolem0003)|actual_world(skolem0006))&((((((((((((((((white(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007))&(white(skolem0001,skolem0003)|city(skolem0006,skolem0007)))&(white(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008)))&(white(skolem0001,skolem0003)|placename(skolem0006,skolem0008)))&(white(skolem0001,skolem0003)|chevy(skolem0006,skolem0009)))&(white(skolem0001,skolem0003)|white(skolem0006,skolem0009)))&(white(skolem0001,skolem0003)|dirty(skolem0006,skolem0009)))&(white(skolem0001,skolem0003)|old(skolem0006,skolem0009)))&(white(skolem0001,skolem0003)|street(skolem0006,skolem0010)))&(white(skolem0001,skolem0003)|lonely(skolem0006,skolem0010)))&(white(skolem0001,skolem0003)|event(skolem0006,skolem0011)))&(white(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0009)))&(white(skolem0001,skolem0003)|present(skolem0006,skolem0011)))&(white(skolem0001,skolem0003)|barrel(skolem0006,skolem0011)))&(white(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0010)))&(white(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007))))&(white(skolem0001,skolem0003)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21))))))&(((dirty(skolem0001,skolem0003)|actual_world(skolem0006))&((((((((((((((((dirty(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007))&(dirty(skolem0001,skolem0003)|city(skolem0006,skolem0007)))&(dirty(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008)))&(dirty(skolem0001,skolem0003)|placename(skolem0006,skolem0008)))&(dirty(skolem0001,skolem0003)|chevy(skolem0006,skolem0009)))&(dirty(skolem0001,skolem0003)|white(skolem0006,skolem0009)))&(dirty(skolem0001,skolem0003)|dirty(skolem0006,skolem0009)))&(dirty(skolem0001,skolem0003)|old(skolem0006,skolem0009)))&(dirty(skolem0001,skolem0003)|street(skolem0006,skolem0010)))&(dirty(skolem0001,skolem0003)|lonely(skolem0006,skolem0010)))&(dirty(skolem0001,skolem0003)|event(skolem0006,skolem0011)))&(dirty(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0009)))&(dirty(skolem0001,skolem0003)|present(skolem0006,skolem0011)))&(dirty(skolem0001,skolem0003)|barrel(skolem0006,skolem0011)))&(dirty(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0010)))&(dirty(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007))))&(dirty(skolem0001,skolem0003)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21))))))&(((old(skolem0001,skolem0003)|actual_world(skolem0006))&((((((((((((((((old(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007))&(old(skolem0001,skolem0003)|city(skolem0006,skolem0007)))&(old(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008)))&(old(skolem0001,skolem0003)|placename(skolem0006,skolem0008)))&(old(skolem0001,skolem0003)|chevy(skolem0006,skolem0009)))&(old(skolem0001,skolem0003)|white(skolem0006,skolem0009)))&(old(skolem0001,skolem0003)|dirty(skolem0006,skolem0009)))&(old(skolem0001,skolem0003)|old(skolem0006,skolem0009)))&(old(skolem0001,skolem0003)|street(skolem0006,skolem0010)))&(old(skolem0001,skolem0003)|lonely(skolem0006,skolem0010)))&(old(skolem0001,skolem0003)|event(skolem0006,skolem0011)))&(old(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0009)))&(old(skolem0001,skolem0003)|present(skolem0006,skolem0011)))&(old(skolem0001,skolem0003)|barrel(skolem0006,skolem0011)))&(old(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0010)))&(old(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007))))&(old(skolem0001,skolem0003)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21))))))&(((street(skolem0001,skolem0004)|actual_world(skolem0006))&((((((((((((((((street(skolem0001,skolem0004)|of(skolem0006,skolem0008,skolem0007))&(street(skolem0001,skolem0004)|city(skolem0006,skolem0007)))&(street(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0008)))&(street(skolem0001,skolem0004)|placename(skolem0006,skolem0008)))&(street(skolem0001,skolem0004)|chevy(skolem0006,skolem0009)))&(street(skolem0001,skolem0004)|white(skolem0006,skolem0009)))&(street(skolem0001,skolem0004)|dirty(skolem0006,skolem0009)))&(street(skolem0001,skolem0004)|old(skolem0006,skolem0009)))&(street(skolem0001,skolem0004)|street(skolem0006,skolem0010)))&(street(skolem0001,skolem0004)|lonely(skolem0006,skolem0010)))&(street(skolem0001,skolem0004)|event(skolem0006,skolem0011)))&(street(skolem0001,skolem0004)|agent(skolem0006,skolem0011,skolem0009)))&(street(skolem0001,skolem0004)|present(skolem0006,skolem0011)))&(street(skolem0001,skolem0004)|barrel(skolem0006,skolem0011)))&(street(skolem0001,skolem0004)|down(skolem0006,skolem0011,skolem0010)))&(street(skolem0001,skolem0004)|in(skolem0006,skolem0011,skolem0007))))&(street(skolem0001,skolem0004)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21))))))&(((lonely(skolem0001,skolem0004)|actual_world(skolem0006))&((((((((((((((((lonely(skolem0001,skolem0004)|of(skolem0006,skolem0008,skolem0007))&(lonely(skolem0001,skolem0004)|city(skolem0006,skolem0007)))&(lonely(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0008)))&(lonely(skolem0001,skolem0004)|placename(skolem0006,skolem0008)))&(lonely(skolem0001,skolem0004)|chevy(skolem0006,skolem0009)))&(lonely(skolem0001,skolem0004)|white(skolem0006,skolem0009)))&(lonely(skolem0001,skolem0004)|dirty(skolem0006,skolem0009)))&(lonely(skolem0001,skolem0004)|old(skolem0006,skolem0009)))&(lonely(skolem0001,skolem0004)|street(skolem0006,skolem0010)))&(lonely(skolem0001,skolem0004)|lonely(skolem0006,skolem0010)))&(lonely(skolem0001,skolem0004)|event(skolem0006,skolem0011)))&(lonely(skolem0001,skolem0004)|agent(skolem0006,skolem0011,skolem0009)))&(lonely(skolem0001,skolem0004)|present(skolem0006,skolem0011)))&(lonely(skolem0001,skolem0004)|barrel(skolem0006,skolem0011)))&(lonely(skolem0001,skolem0004)|down(skolem0006,skolem0011,skolem0010)))&(lonely(skolem0001,skolem0004)|in(skolem0006,skolem0011,skolem0007))))&(lonely(skolem0001,skolem0004)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21))))))&(((event(skolem0001,skolem0005)|actual_world(skolem0006))&((((((((((((((((event(skolem0001,skolem0005)|of(skolem0006,skolem0008,skolem0007))&(event(skolem0001,skolem0005)|city(skolem0006,skolem0007)))&(event(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0008)))&(event(skolem0001,skolem0005)|placename(skolem0006,skolem0008)))&(event(skolem0001,skolem0005)|chevy(skolem0006,skolem0009)))&(event(skolem0001,skolem0005)|white(skolem0006,skolem0009)))&(event(skolem0001,skolem0005)|dirty(skolem0006,skolem0009)))&(event(skolem0001,skolem0005)|old(skolem0006,skolem0009)))&(event(skolem0001,skolem0005)|street(skolem0006,skolem0010)))&(event(skolem0001,skolem0005)|lonely(skolem0006,skolem0010)))&(event(skolem0001,skolem0005)|event(skolem0006,skolem0011)))&(event(skolem0001,skolem0005)|agent(skolem0006,skolem0011,skolem0009)))&(event(skolem0001,skolem0005)|present(skolem0006,skolem0011)))&(event(skolem0001,skolem0005)|barrel(skolem0006,skolem0011)))&(event(skolem0001,skolem0005)|down(skolem0006,skolem0011,skolem0010)))&(event(skolem0001,skolem0005)|in(skolem0006,skolem0011,skolem0007))))&(event(skolem0001,skolem0005)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21))))))&(((agent(skolem0001,skolem0005,skolem0003)|actual_world(skolem0006))&((((((((((((((((agent(skolem0001,skolem0005,skolem0003)|of(skolem0006,skolem0008,skolem0007))&(agent(skolem0001,skolem0005,skolem0003)|city(skolem0006,skolem0007)))&(agent(skolem0001,skolem0005,skolem0003)|hollywood_placename(skolem0006,skolem0008)))&(agent(skolem0001,skolem0005,skolem0003)|placename(skolem0006,skolem0008)))&(agent(skolem0001,skolem0005,skolem0003)|chevy(skolem0006,skolem0009)))&(agent(skolem0001,skolem0005,skolem0003)|white(skolem0006,skolem0009)))&(agent(skolem0001,skolem0005,skolem0003)|dirty(skolem0006,skolem0009)))&(agent(skolem0001,skolem0005,skolem0003)|old(skolem0006,skolem0009)))&(agent(skolem0001,skolem0005,skolem0003)|street(skolem0006,skolem0010)))&(agent(skolem0001,skolem0005,skolem0003)|lonely(skolem0006,skolem0010)))&(agent(skolem0001,skolem0005,skolem0003)|event(skolem0006,skolem0011)))&(agent(skolem0001,skolem0005,skolem0003)|agent(skolem0006,skolem0011,skolem0009)))&(agent(skolem0001,skolem0005,skolem0003)|present(skolem0006,skolem0011)))&(agent(skolem0001,skolem0005,skolem0003)|barrel(skolem0006,skolem0011)))&(agent(skolem0001,skolem0005,skolem0003)|down(skolem0006,skolem0011,skolem0010)))&(agent(skolem0001,skolem0005,skolem0003)|in(skolem0006,skolem0011,skolem0007))))&(agent(skolem0001,skolem0005,skolem0003)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21))))))&(((present(skolem0001,skolem0005)|actual_world(skolem0006))&((((((((((((((((present(skolem0001,skolem0005)|of(skolem0006,skolem0008,skolem0007))&(present(skolem0001,skolem0005)|city(skolem0006,skolem0007)))&(present(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0008)))&(present(skolem0001,skolem0005)|placename(skolem0006,skolem0008)))&(present(skolem0001,skolem0005)|chevy(skolem0006,skolem0009)))&(present(skolem0001,skolem0005)|white(skolem0006,skolem0009)))&(present(skolem0001,skolem0005)|dirty(skolem0006,skolem0009)))&(present(skolem0001,skolem0005)|old(skolem0006,skolem0009)))&(present(skolem0001,skolem0005)|street(skolem0006,skolem0010)))&(present(skolem0001,skolem0005)|lonely(skolem0006,skolem0010)))&(present(skolem0001,skolem0005)|event(skolem0006,skolem0011)))&(present(skolem0001,skolem0005)|agent(skolem0006,skolem0011,skolem0009)))&(present(skolem0001,skolem0005)|present(skolem0006,skolem0011)))&(present(skolem0001,skolem0005)|barrel(skolem0006,skolem0011)))&(present(skolem0001,skolem0005)|down(skolem0006,skolem0011,skolem0010)))&(present(skolem0001,skolem0005)|in(skolem0006,skolem0011,skolem0007))))&(present(skolem0001,skolem0005)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21))))))&(((barrel(skolem0001,skolem0005)|actual_world(skolem0006))&((((((((((((((((barrel(skolem0001,skolem0005)|of(skolem0006,skolem0008,skolem0007))&(barrel(skolem0001,skolem0005)|city(skolem0006,skolem0007)))&(barrel(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0008)))&(barrel(skolem0001,skolem0005)|placename(skolem0006,skolem0008)))&(barrel(skolem0001,skolem0005)|chevy(skolem0006,skolem0009)))&(barrel(skolem0001,skolem0005)|white(skolem0006,skolem0009)))&(barrel(skolem0001,skolem0005)|dirty(skolem0006,skolem0009)))&(barrel(skolem0001,skolem0005)|old(skolem0006,skolem0009)))&(barrel(skolem0001,skolem0005)|street(skolem0006,skolem0010)))&(barrel(skolem0001,skolem0005)|lonely(skolem0006,skolem0010)))&(barrel(skolem0001,skolem0005)|event(skolem0006,skolem0011)))&(barrel(skolem0001,skolem0005)|agent(skolem0006,skolem0011,skolem0009)))&(barrel(skolem0001,skolem0005)|present(skolem0006,skolem0011)))&(barrel(skolem0001,skolem0005)|barrel(skolem0006,skolem0011)))&(barrel(skolem0001,skolem0005)|down(skolem0006,skolem0011,skolem0010)))&(barrel(skolem0001,skolem0005)|in(skolem0006,skolem0011,skolem0007))))&(barrel(skolem0001,skolem0005)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21))))))&(((down(skolem0001,skolem0005,skolem0004)|actual_world(skolem0006))&((((((((((((((((down(skolem0001,skolem0005,skolem0004)|of(skolem0006,skolem0008,skolem0007))&(down(skolem0001,skolem0005,skolem0004)|city(skolem0006,skolem0007)))&(down(skolem0001,skolem0005,skolem0004)|hollywood_placename(skolem0006,skolem0008)))&(down(skolem0001,skolem0005,skolem0004)|placename(skolem0006,skolem0008)))&(down(skolem0001,skolem0005,skolem0004)|chevy(skolem0006,skolem0009)))&(down(skolem0001,skolem0005,skolem0004)|white(skolem0006,skolem0009)))&(down(skolem0001,skolem0005,skolem0004)|dirty(skolem0006,skolem0009)))&(down(skolem0001,skolem0005,skolem0004)|old(skolem0006,skolem0009)))&(down(skolem0001,skolem0005,skolem0004)|street(skolem0006,skolem0010)))&(down(skolem0001,skolem0005,skolem0004)|lonely(skolem0006,skolem0010)))&(down(skolem0001,skolem0005,skolem0004)|event(skolem0006,skolem0011)))&(down(skolem0001,skolem0005,skolem0004)|agent(skolem0006,skolem0011,skolem0009)))&(down(skolem0001,skolem0005,skolem0004)|present(skolem0006,skolem0011)))&(down(skolem0001,skolem0005,skolem0004)|barrel(skolem0006,skolem0011)))&(down(skolem0001,skolem0005,skolem0004)|down(skolem0006,skolem0011,skolem0010)))&(down(skolem0001,skolem0005,skolem0004)|in(skolem0006,skolem0011,skolem0007))))&(down(skolem0001,skolem0005,skolem0004)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21))))))&(((in(skolem0001,skolem0005,skolem0003)|actual_world(skolem0006))&((((((((((((((((in(skolem0001,skolem0005,skolem0003)|of(skolem0006,skolem0008,skolem0007))&(in(skolem0001,skolem0005,skolem0003)|city(skolem0006,skolem0007)))&(in(skolem0001,skolem0005,skolem0003)|hollywood_placename(skolem0006,skolem0008)))&(in(skolem0001,skolem0005,skolem0003)|placename(skolem0006,skolem0008)))&(in(skolem0001,skolem0005,skolem0003)|chevy(skolem0006,skolem0009)))&(in(skolem0001,skolem0005,skolem0003)|white(skolem0006,skolem0009)))&(in(skolem0001,skolem0005,skolem0003)|dirty(skolem0006,skolem0009)))&(in(skolem0001,skolem0005,skolem0003)|old(skolem0006,skolem0009)))&(in(skolem0001,skolem0005,skolem0003)|street(skolem0006,skolem0010)))&(in(skolem0001,skolem0005,skolem0003)|lonely(skolem0006,skolem0010)))&(in(skolem0001,skolem0005,skolem0003)|event(skolem0006,skolem0011)))&(in(skolem0001,skolem0005,skolem0003)|agent(skolem0006,skolem0011,skolem0009)))&(in(skolem0001,skolem0005,skolem0003)|present(skolem0006,skolem0011)))&(in(skolem0001,skolem0005,skolem0003)|barrel(skolem0006,skolem0011)))&(in(skolem0001,skolem0005,skolem0003)|down(skolem0006,skolem0011,skolem0010)))&(in(skolem0001,skolem0005,skolem0003)|in(skolem0006,skolem0011,skolem0007))))&(in(skolem0001,skolem0005,skolem0003)|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21)))))))&((((~actual_world(X7)|(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~street(X7,X11))|~lonely(X7,X11))|~event(X7,X12))|~agent(X7,X12,X10))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X11))|~in(X7,X12,X8)))|actual_world(skolem0006))&(((((((((((((((((~actual_world(X7)|(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~street(X7,X11))|~lonely(X7,X11))|~event(X7,X12))|~agent(X7,X12,X10))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X11))|~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))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~street(X7,X11))|~lonely(X7,X11))|~event(X7,X12))|~agent(X7,X12,X10))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X11))|~in(X7,X12,X8)))|city(skolem0006,skolem0007)))&((~actual_world(X7)|(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~street(X7,X11))|~lonely(X7,X11))|~event(X7,X12))|~agent(X7,X12,X10))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X11))|~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))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~street(X7,X11))|~lonely(X7,X11))|~event(X7,X12))|~agent(X7,X12,X10))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X11))|~in(X7,X12,X8)))|placename(skolem0006,skolem0008)))&((~actual_world(X7)|(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~street(X7,X11))|~lonely(X7,X11))|~event(X7,X12))|~agent(X7,X12,X10))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X11))|~in(X7,X12,X8)))|chevy(skolem0006,skolem0009)))&((~actual_world(X7)|(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~street(X7,X11))|~lonely(X7,X11))|~event(X7,X12))|~agent(X7,X12,X10))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X11))|~in(X7,X12,X8)))|white(skolem0006,skolem0009)))&((~actual_world(X7)|(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~street(X7,X11))|~lonely(X7,X11))|~event(X7,X12))|~agent(X7,X12,X10))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X11))|~in(X7,X12,X8)))|dirty(skolem0006,skolem0009)))&((~actual_world(X7)|(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~street(X7,X11))|~lonely(X7,X11))|~event(X7,X12))|~agent(X7,X12,X10))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X11))|~in(X7,X12,X8)))|old(skolem0006,skolem0009)))&((~actual_world(X7)|(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~street(X7,X11))|~lonely(X7,X11))|~event(X7,X12))|~agent(X7,X12,X10))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X11))|~in(X7,X12,X8)))|street(skolem0006,skolem0010)))&((~actual_world(X7)|(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~street(X7,X11))|~lonely(X7,X11))|~event(X7,X12))|~agent(X7,X12,X10))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X11))|~in(X7,X12,X8)))|lonely(skolem0006,skolem0010)))&((~actual_world(X7)|(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~street(X7,X11))|~lonely(X7,X11))|~event(X7,X12))|~agent(X7,X12,X10))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X11))|~in(X7,X12,X8)))|event(skolem0006,skolem0011)))&((~actual_world(X7)|(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~street(X7,X11))|~lonely(X7,X11))|~event(X7,X12))|~agent(X7,X12,X10))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X11))|~in(X7,X12,X8)))|agent(skolem0006,skolem0011,skolem0009)))&((~actual_world(X7)|(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~street(X7,X11))|~lonely(X7,X11))|~event(X7,X12))|~agent(X7,X12,X10))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X11))|~in(X7,X12,X8)))|present(skolem0006,skolem0011)))&((~actual_world(X7)|(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~street(X7,X11))|~lonely(X7,X11))|~event(X7,X12))|~agent(X7,X12,X10))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X11))|~in(X7,X12,X8)))|barrel(skolem0006,skolem0011)))&((~actual_world(X7)|(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~street(X7,X11))|~lonely(X7,X11))|~event(X7,X12))|~agent(X7,X12,X10))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X11))|~in(X7,X12,X8)))|down(skolem0006,skolem0011,skolem0010)))&((~actual_world(X7)|(((((((((((((((~of(X7,X9,X8)|~city(X7,X8))|~hollywood_placename(X7,X9))|~placename(X7,X9))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~street(X7,X11))|~lonely(X7,X11))|~event(X7,X12))|~agent(X7,X12,X10))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X11))|~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))|~chevy(X7,X10))|~white(X7,X10))|~dirty(X7,X10))|~old(X7,X10))|~street(X7,X11))|~lonely(X7,X11))|~event(X7,X12))|~agent(X7,X12,X10))|~present(X7,X12))|~barrel(X7,X12))|~down(X7,X12,X11))|~in(X7,X12,X8)))|(~actual_world(X19)|(((((((((((((((~of(X19,X20,X21)|~city(X19,X21))|~hollywood_placename(X19,X20))|~placename(X19,X20))|~chevy(X19,X21))|~white(X19,X21))|~dirty(X19,X21))|~old(X19,X21))|~street(X19,X22))|~lonely(X19,X22))|~event(X19,X23))|~agent(X19,X23,X21))|~present(X19,X23))|~barrel(X19,X23))|~down(X19,X23,X22))|~in(X19,X23,X21))))))))))))))))),inference(distribute,[status(thm)],[c4])).
% 7.50/7.70  cnf(c18,negated_conjecture,actual_world(skolem0001)|agent(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c54,negated_conjecture,city(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c72,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|agent(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c90,negated_conjecture,placename(skolem0001,skolem0002)|agent(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c108,negated_conjecture,chevy(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c126,negated_conjecture,white(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c144,negated_conjecture,dirty(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c162,negated_conjecture,old(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c180,negated_conjecture,street(skolem0001,skolem0004)|agent(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c198,negated_conjecture,lonely(skolem0001,skolem0004)|agent(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c216,negated_conjecture,event(skolem0001,skolem0005)|agent(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c252,negated_conjecture,present(skolem0001,skolem0005)|agent(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c270,negated_conjecture,barrel(skolem0001,skolem0005)|agent(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c36,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|agent(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c234,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|agent(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c288,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|agent(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c306,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|agent(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c324,negated_conjecture,~actual_world(X195)|~of(X195,X196,X194)|~city(X195,X194)|~hollywood_placename(X195,X196)|~placename(X195,X196)|~chevy(X195,X197)|~white(X195,X197)|~dirty(X195,X197)|~old(X195,X197)|~street(X195,X193)|~lonely(X195,X193)|~event(X195,X198)|~agent(X195,X198,X197)|~present(X195,X198)|~barrel(X195,X198)|~down(X195,X198,X193)|~in(X195,X198,X194)|agent(skolem0006,skolem0011,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c1390,plain,~actual_world(skolem0001)|~of(skolem0001,X1547,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1547)|~placename(skolem0001,X1547)|~chevy(skolem0001,X1548)|~white(skolem0001,X1548)|~dirty(skolem0001,X1548)|~old(skolem0001,X1548)|~street(skolem0001,X1546)|~lonely(skolem0001,X1546)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1548)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X1546)|agent(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c324, c306])).
% 7.50/7.70  cnf(c4215,plain,~actual_world(skolem0001)|~of(skolem0001,X1549,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1549)|~placename(skolem0001,X1549)|~chevy(skolem0001,X1550)|~white(skolem0001,X1550)|~dirty(skolem0001,X1550)|~old(skolem0001,X1550)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1550)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|agent(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c1390, c288])).
% 7.50/7.70  cnf(c4216,plain,~actual_world(skolem0001)|~of(skolem0001,X1551,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1551)|~placename(skolem0001,X1551)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|agent(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c4215, c234])).
% 7.50/7.70  cnf(c4220,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|agent(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c4216, c36])).
% 7.50/7.70  cnf(c4222,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|agent(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c4220, c270])).
% 7.50/7.70  cnf(c4227,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|agent(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c4222, c252])).
% 7.50/7.70  cnf(c4229,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|agent(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c4227, c216])).
% 7.50/7.70  cnf(c4233,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|agent(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c4229, c198])).
% 7.50/7.70  cnf(c4236,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c4233, c180])).
% 7.50/7.70  cnf(c4238,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c4236, c162])).
% 7.50/7.70  cnf(c4241,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c4238, c144])).
% 7.50/7.70  cnf(c4245,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c4241, c126])).
% 7.50/7.70  cnf(c4248,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|agent(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c4245, c108])).
% 7.50/7.70  cnf(c4249,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|agent(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c4248, c90])).
% 7.50/7.70  cnf(c4252,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|agent(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c4249, c72])).
% 7.50/7.70  cnf(c4257,plain,~actual_world(skolem0001)|agent(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c4252, c54])).
% 7.50/7.70  cnf(c4259,plain,agent(skolem0006,skolem0011,skolem0009),inference(resolution,[status(thm)],[c4257, c18])).
% 7.50/7.70  cnf(c329,negated_conjecture,~actual_world(X215)|~of(X215,X217,X214)|~city(X215,X214)|~hollywood_placename(X215,X217)|~placename(X215,X217)|~chevy(X215,X220)|~white(X215,X220)|~dirty(X215,X220)|~old(X215,X220)|~street(X215,X211)|~lonely(X215,X211)|~event(X215,X221)|~agent(X215,X221,X220)|~present(X215,X221)|~barrel(X215,X221)|~down(X215,X221,X211)|~in(X215,X221,X214)|~actual_world(X216)|~of(X216,X213,X219)|~city(X216,X219)|~hollywood_placename(X216,X213)|~placename(X216,X213)|~chevy(X216,X219)|~white(X216,X219)|~dirty(X216,X219)|~old(X216,X219)|~street(X216,X212)|~lonely(X216,X212)|~event(X216,X218)|~agent(X216,X218,X219)|~present(X216,X218)|~barrel(X216,X218)|~down(X216,X218,X212)|~in(X216,X218,X219),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c1486,plain,~actual_world(X3886)|~of(X3886,X3889,X3887)|~city(X3886,X3887)|~hollywood_placename(X3886,X3889)|~placename(X3886,X3889)|~chevy(X3886,X3884)|~white(X3886,X3884)|~dirty(X3886,X3884)|~old(X3886,X3884)|~street(X3886,X3888)|~lonely(X3886,X3888)|~event(X3886,X3883)|~agent(X3886,X3883,X3884)|~present(X3886,X3883)|~barrel(X3886,X3883)|~down(X3886,X3883,X3888)|~in(X3886,X3883,X3887)|~of(X3886,X3885,X3887)|~hollywood_placename(X3886,X3885)|~placename(X3886,X3885)|~chevy(X3886,X3887)|~white(X3886,X3887)|~dirty(X3886,X3887)|~old(X3886,X3887)|~street(X3886,X3890)|~lonely(X3886,X3890)|~agent(X3886,X3883,X3887)|~down(X3886,X3883,X3890),inference(factor,[status(thm)],[c329])).
% 7.50/7.70  cnf(c4344,plain,~actual_world(X3907)|~of(X3907,X3912,X3911)|~city(X3907,X3911)|~hollywood_placename(X3907,X3912)|~placename(X3907,X3912)|~chevy(X3907,X3908)|~white(X3907,X3908)|~dirty(X3907,X3908)|~old(X3907,X3908)|~street(X3907,X3910)|~lonely(X3907,X3910)|~event(X3907,X3909)|~agent(X3907,X3909,X3908)|~present(X3907,X3909)|~barrel(X3907,X3909)|~down(X3907,X3909,X3910)|~in(X3907,X3909,X3911)|~of(X3907,X3906,X3911)|~hollywood_placename(X3907,X3906)|~placename(X3907,X3906)|~chevy(X3907,X3911)|~white(X3907,X3911)|~dirty(X3907,X3911)|~old(X3907,X3911)|~agent(X3907,X3909,X3911),inference(factor,[status(thm)],[c1486])).
% 7.50/7.70  cnf(c4347,plain,~actual_world(skolem0006)|~of(skolem0006,X4131,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X4131)|~placename(skolem0006,X4131)|~chevy(skolem0006,X4132)|~white(skolem0006,X4132)|~dirty(skolem0006,X4132)|~old(skolem0006,X4132)|~street(skolem0006,X4133)|~lonely(skolem0006,X4133)|~event(skolem0006,skolem0011)|~agent(skolem0006,skolem0011,X4132)|~present(skolem0006,skolem0011)|~barrel(skolem0006,skolem0011)|~down(skolem0006,skolem0011,X4133)|~in(skolem0006,skolem0011,skolem0009)|~of(skolem0006,X4130,skolem0009)|~hollywood_placename(skolem0006,X4130)|~placename(skolem0006,X4130)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009),inference(resolution,[status(thm)],[c4344, c4259])).
% 7.50/7.70  cnf(c4352,plain,~actual_world(skolem0006)|~of(skolem0006,X4136,skolem0009)|~city(skolem0006,skolem0009)|~hollywood_placename(skolem0006,X4136)|~placename(skolem0006,X4136)|~chevy(skolem0006,X4135)|~white(skolem0006,X4135)|~dirty(skolem0006,X4135)|~old(skolem0006,X4135)|~street(skolem0006,X4134)|~lonely(skolem0006,X4134)|~event(skolem0006,skolem0011)|~agent(skolem0006,skolem0011,X4135)|~present(skolem0006,skolem0011)|~barrel(skolem0006,skolem0011)|~down(skolem0006,skolem0011,X4134)|~in(skolem0006,skolem0011,skolem0009)|~chevy(skolem0006,skolem0009)|~white(skolem0006,skolem0009)|~dirty(skolem0006,skolem0009)|~old(skolem0006,skolem0009),inference(factor,[status(thm)],[c4347])).
% 7.50/7.70  cnf(c21,negated_conjecture,actual_world(skolem0001)|down(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c57,negated_conjecture,city(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c75,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|down(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c93,negated_conjecture,placename(skolem0001,skolem0002)|down(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c111,negated_conjecture,chevy(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c129,negated_conjecture,white(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c147,negated_conjecture,dirty(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c165,negated_conjecture,old(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c183,negated_conjecture,street(skolem0001,skolem0004)|down(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c201,negated_conjecture,lonely(skolem0001,skolem0004)|down(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c219,negated_conjecture,event(skolem0001,skolem0005)|down(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c255,negated_conjecture,present(skolem0001,skolem0005)|down(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c273,negated_conjecture,barrel(skolem0001,skolem0005)|down(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c39,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|down(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c237,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|down(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c291,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|down(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c309,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|down(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c327,negated_conjecture,~actual_world(X201)|~of(X201,X202,X200)|~city(X201,X200)|~hollywood_placename(X201,X202)|~placename(X201,X202)|~chevy(X201,X203)|~white(X201,X203)|~dirty(X201,X203)|~old(X201,X203)|~street(X201,X199)|~lonely(X201,X199)|~event(X201,X204)|~agent(X201,X204,X203)|~present(X201,X204)|~barrel(X201,X204)|~down(X201,X204,X199)|~in(X201,X204,X200)|down(skolem0006,skolem0011,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c1438,plain,~actual_world(skolem0001)|~of(skolem0001,X1570,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1570)|~placename(skolem0001,X1570)|~chevy(skolem0001,X1571)|~white(skolem0001,X1571)|~dirty(skolem0001,X1571)|~old(skolem0001,X1571)|~street(skolem0001,X1572)|~lonely(skolem0001,X1572)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1571)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X1572)|down(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c327, c309])).
% 7.50/7.70  cnf(c4261,plain,~actual_world(skolem0001)|~of(skolem0001,X1573,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1573)|~placename(skolem0001,X1573)|~chevy(skolem0001,X1574)|~white(skolem0001,X1574)|~dirty(skolem0001,X1574)|~old(skolem0001,X1574)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1574)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|down(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c1438, c291])).
% 7.50/7.70  cnf(c4263,plain,~actual_world(skolem0001)|~of(skolem0001,X1575,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1575)|~placename(skolem0001,X1575)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|down(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c4261, c237])).
% 7.50/7.70  cnf(c4265,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|down(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c4263, c39])).
% 7.50/7.70  cnf(c4268,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|down(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c4265, c273])).
% 7.50/7.70  cnf(c4270,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|down(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c4268, c255])).
% 7.50/7.70  cnf(c4272,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|down(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c4270, c219])).
% 7.50/7.70  cnf(c4274,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|down(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c4272, c201])).
% 7.50/7.70  cnf(c4276,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c4274, c183])).
% 7.50/7.70  cnf(c4277,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c4276, c165])).
% 7.50/7.70  cnf(c4279,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c4277, c147])).
% 7.50/7.70  cnf(c4282,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c4279, c129])).
% 7.50/7.70  cnf(c4284,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|down(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c4282, c111])).
% 7.50/7.70  cnf(c4285,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|down(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c4284, c93])).
% 7.50/7.70  cnf(c4288,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|down(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c4285, c75])).
% 7.50/7.70  cnf(c4289,plain,~actual_world(skolem0001)|down(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c4288, c57])).
% 7.50/7.70  cnf(c4292,plain,down(skolem0006,skolem0011,skolem0010),inference(resolution,[status(thm)],[c4289, c21])).
% 7.50/7.70  cnf(c22,negated_conjecture,actual_world(skolem0001)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c58,negated_conjecture,city(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c76,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c94,negated_conjecture,placename(skolem0001,skolem0002)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c112,negated_conjecture,chevy(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c130,negated_conjecture,white(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c148,negated_conjecture,dirty(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c166,negated_conjecture,old(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c184,negated_conjecture,street(skolem0001,skolem0004)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c202,negated_conjecture,lonely(skolem0001,skolem0004)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c220,negated_conjecture,event(skolem0001,skolem0005)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c256,negated_conjecture,present(skolem0001,skolem0005)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c274,negated_conjecture,barrel(skolem0001,skolem0005)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c40,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c238,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c292,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c310,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c328,negated_conjecture,~actual_world(X207)|~of(X207,X208,X206)|~city(X207,X206)|~hollywood_placename(X207,X208)|~placename(X207,X208)|~chevy(X207,X209)|~white(X207,X209)|~dirty(X207,X209)|~old(X207,X209)|~street(X207,X205)|~lonely(X207,X205)|~event(X207,X210)|~agent(X207,X210,X209)|~present(X207,X210)|~barrel(X207,X210)|~down(X207,X210,X205)|~in(X207,X210,X206)|in(skolem0006,skolem0011,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.70  cnf(c1482,plain,~actual_world(skolem0001)|~of(skolem0001,X1607,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1607)|~placename(skolem0001,X1607)|~chevy(skolem0001,X1608)|~white(skolem0001,X1608)|~dirty(skolem0001,X1608)|~old(skolem0001,X1608)|~street(skolem0001,X1609)|~lonely(skolem0001,X1609)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1608)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X1609)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c328, c310])).
% 7.50/7.71  cnf(c4308,plain,~actual_world(skolem0001)|~of(skolem0001,X1610,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1610)|~placename(skolem0001,X1610)|~chevy(skolem0001,X1611)|~white(skolem0001,X1611)|~dirty(skolem0001,X1611)|~old(skolem0001,X1611)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1611)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c1482, c292])).
% 7.50/7.71  cnf(c4309,plain,~actual_world(skolem0001)|~of(skolem0001,X1612,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1612)|~placename(skolem0001,X1612)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c4308, c238])).
% 7.50/7.71  cnf(c4310,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c4309, c40])).
% 7.50/7.71  cnf(c4311,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c4310, c274])).
% 7.50/7.71  cnf(c4312,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c4311, c256])).
% 7.50/7.71  cnf(c4313,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c4312, c220])).
% 7.50/7.71  cnf(c4314,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c4313, c202])).
% 7.50/7.71  cnf(c4315,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c4314, c184])).
% 7.50/7.71  cnf(c4316,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c4315, c166])).
% 7.50/7.71  cnf(c4317,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c4316, c148])).
% 7.50/7.71  cnf(c4318,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c4317, c130])).
% 7.50/7.71  cnf(c4319,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c4318, c112])).
% 7.50/7.71  cnf(c4320,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c4319, c94])).
% 7.50/7.71  cnf(c4321,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c4320, c76])).
% 7.50/7.71  cnf(c4322,plain,~actual_world(skolem0001)|in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c4321, c58])).
% 7.50/7.71  cnf(c4323,plain,in(skolem0006,skolem0011,skolem0007),inference(resolution,[status(thm)],[c4322, c22])).
% 7.50/7.71  cnf(c4346,plain,~actual_world(X3914)|~of(X3914,X3916,X3918)|~city(X3914,X3918)|~hollywood_placename(X3914,X3916)|~placename(X3914,X3916)|~chevy(X3914,X3918)|~white(X3914,X3918)|~dirty(X3914,X3918)|~old(X3914,X3918)|~street(X3914,X3917)|~lonely(X3914,X3917)|~event(X3914,X3913)|~agent(X3914,X3913,X3918)|~present(X3914,X3913)|~barrel(X3914,X3913)|~down(X3914,X3913,X3917)|~in(X3914,X3913,X3918)|~of(X3914,X3915,X3918)|~hollywood_placename(X3914,X3915)|~placename(X3914,X3915),inference(factor,[status(thm)],[c4344])).
% 7.50/7.71  cnf(c4348,plain,~actual_world(X3923)|~of(X3923,X3922,X3919)|~city(X3923,X3919)|~hollywood_placename(X3923,X3922)|~placename(X3923,X3922)|~chevy(X3923,X3919)|~white(X3923,X3919)|~dirty(X3923,X3919)|~old(X3923,X3919)|~street(X3923,X3920)|~lonely(X3923,X3920)|~event(X3923,X3921)|~agent(X3923,X3921,X3919)|~present(X3923,X3921)|~barrel(X3923,X3921)|~down(X3923,X3921,X3920)|~in(X3923,X3921,X3919),inference(factor,[status(thm)],[c4346])).
% 7.50/7.71  cnf(c4350,plain,~actual_world(skolem0006)|~of(skolem0006,X3932,skolem0007)|~city(skolem0006,skolem0007)|~hollywood_placename(skolem0006,X3932)|~placename(skolem0006,X3932)|~chevy(skolem0006,skolem0007)|~white(skolem0006,skolem0007)|~dirty(skolem0006,skolem0007)|~old(skolem0006,skolem0007)|~street(skolem0006,X3933)|~lonely(skolem0006,X3933)|~event(skolem0006,skolem0011)|~agent(skolem0006,skolem0011,skolem0007)|~present(skolem0006,skolem0011)|~barrel(skolem0006,skolem0011)|~down(skolem0006,skolem0011,X3933),inference(resolution,[status(thm)],[c4348, c4323])).
% 7.50/7.71  cnf(c4351,plain,~actual_world(skolem0006)|~of(skolem0006,X3934,skolem0007)|~city(skolem0006,skolem0007)|~hollywood_placename(skolem0006,X3934)|~placename(skolem0006,X3934)|~chevy(skolem0006,skolem0007)|~white(skolem0006,skolem0007)|~dirty(skolem0006,skolem0007)|~old(skolem0006,skolem0007)|~street(skolem0006,skolem0010)|~lonely(skolem0006,skolem0010)|~event(skolem0006,skolem0011)|~agent(skolem0006,skolem0011,skolem0007)|~present(skolem0006,skolem0011)|~barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4350, c4292])).
% 7.50/7.71  cnf(c7,negated_conjecture,actual_world(skolem0001)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c43,negated_conjecture,city(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c61,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c79,negated_conjecture,placename(skolem0001,skolem0002)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c97,negated_conjecture,chevy(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c115,negated_conjecture,white(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c133,negated_conjecture,dirty(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c151,negated_conjecture,old(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c169,negated_conjecture,street(skolem0001,skolem0004)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c187,negated_conjecture,lonely(skolem0001,skolem0004)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c205,negated_conjecture,event(skolem0001,skolem0005)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c241,negated_conjecture,present(skolem0001,skolem0005)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c259,negated_conjecture,barrel(skolem0001,skolem0005)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c25,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c223,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c277,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c295,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c313,negated_conjecture,~actual_world(X177)|~of(X177,X178,X176)|~city(X177,X176)|~hollywood_placename(X177,X178)|~placename(X177,X178)|~chevy(X177,X179)|~white(X177,X179)|~dirty(X177,X179)|~old(X177,X179)|~street(X177,X175)|~lonely(X177,X175)|~event(X177,X180)|~agent(X177,X180,X179)|~present(X177,X180)|~barrel(X177,X180)|~down(X177,X180,X175)|~in(X177,X180,X176)|of(skolem0006,skolem0008,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c1308,plain,~actual_world(skolem0001)|~of(skolem0001,X1517,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1517)|~placename(skolem0001,X1517)|~chevy(skolem0001,X1516)|~white(skolem0001,X1516)|~dirty(skolem0001,X1516)|~old(skolem0001,X1516)|~street(skolem0001,X1518)|~lonely(skolem0001,X1518)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1516)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X1518)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c313, c295])).
% 7.50/7.71  cnf(c4150,plain,~actual_world(skolem0001)|~of(skolem0001,X1520,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1520)|~placename(skolem0001,X1520)|~chevy(skolem0001,X1519)|~white(skolem0001,X1519)|~dirty(skolem0001,X1519)|~old(skolem0001,X1519)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1519)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c1308, c277])).
% 7.50/7.71  cnf(c4154,plain,~actual_world(skolem0001)|~of(skolem0001,X1521,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1521)|~placename(skolem0001,X1521)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c4150, c223])).
% 7.50/7.71  cnf(c4159,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c4154, c25])).
% 7.50/7.71  cnf(c4164,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c4159, c259])).
% 7.50/7.71  cnf(c4168,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c4164, c241])).
% 7.50/7.71  cnf(c4172,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c4168, c205])).
% 7.50/7.71  cnf(c4174,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c4172, c187])).
% 7.50/7.71  cnf(c4179,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c4174, c169])).
% 7.50/7.71  cnf(c4182,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c4179, c151])).
% 7.50/7.71  cnf(c4188,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c4182, c133])).
% 7.50/7.71  cnf(c4192,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c4188, c115])).
% 7.50/7.71  cnf(c4196,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c4192, c97])).
% 7.50/7.71  cnf(c4199,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c4196, c79])).
% 7.50/7.71  cnf(c4201,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c4199, c61])).
% 7.50/7.71  cnf(c4205,plain,~actual_world(skolem0001)|of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c4201, c43])).
% 7.50/7.71  cnf(c4209,plain,of(skolem0006,skolem0008,skolem0007),inference(resolution,[status(thm)],[c4205, c7])).
% 7.50/7.71  cnf(c20,negated_conjecture,actual_world(skolem0001)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c56,negated_conjecture,city(skolem0001,skolem0003)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c74,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c92,negated_conjecture,placename(skolem0001,skolem0002)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c110,negated_conjecture,chevy(skolem0001,skolem0003)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c128,negated_conjecture,white(skolem0001,skolem0003)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c146,negated_conjecture,dirty(skolem0001,skolem0003)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c164,negated_conjecture,old(skolem0001,skolem0003)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c182,negated_conjecture,street(skolem0001,skolem0004)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c200,negated_conjecture,lonely(skolem0001,skolem0004)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c218,negated_conjecture,event(skolem0001,skolem0005)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c254,negated_conjecture,present(skolem0001,skolem0005)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c272,negated_conjecture,barrel(skolem0001,skolem0005)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c38,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c236,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c290,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c308,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c326,negated_conjecture,~actual_world(X189)|~of(X189,X190,X188)|~city(X189,X188)|~hollywood_placename(X189,X190)|~placename(X189,X190)|~chevy(X189,X191)|~white(X189,X191)|~dirty(X189,X191)|~old(X189,X191)|~street(X189,X187)|~lonely(X189,X187)|~event(X189,X192)|~agent(X189,X192,X191)|~present(X189,X192)|~barrel(X189,X192)|~down(X189,X192,X187)|~in(X189,X192,X188)|barrel(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c1383,plain,~actual_world(skolem0001)|~of(skolem0001,X1227,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1227)|~placename(skolem0001,X1227)|~chevy(skolem0001,X1226)|~white(skolem0001,X1226)|~dirty(skolem0001,X1226)|~old(skolem0001,X1226)|~street(skolem0001,X1225)|~lonely(skolem0001,X1225)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1226)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X1225)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c326, c308])).
% 7.50/7.71  cnf(c4069,plain,~actual_world(skolem0001)|~of(skolem0001,X1228,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1228)|~placename(skolem0001,X1228)|~chevy(skolem0001,X1229)|~white(skolem0001,X1229)|~dirty(skolem0001,X1229)|~old(skolem0001,X1229)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1229)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c1383, c290])).
% 7.50/7.71  cnf(c4078,plain,~actual_world(skolem0001)|~of(skolem0001,X1232,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1232)|~placename(skolem0001,X1232)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4069, c236])).
% 7.50/7.71  cnf(c4080,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4078, c38])).
% 7.50/7.71  cnf(c4087,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4080, c272])).
% 7.50/7.71  cnf(c4090,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4087, c254])).
% 7.50/7.71  cnf(c4098,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4090, c218])).
% 7.50/7.71  cnf(c4103,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4098, c200])).
% 7.50/7.71  cnf(c4106,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4103, c182])).
% 7.50/7.71  cnf(c4112,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4106, c164])).
% 7.50/7.71  cnf(c4114,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4112, c146])).
% 7.50/7.71  cnf(c4121,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4114, c128])).
% 7.50/7.71  cnf(c4127,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4121, c110])).
% 7.50/7.71  cnf(c4133,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4127, c92])).
% 7.50/7.71  cnf(c4136,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4133, c74])).
% 7.50/7.71  cnf(c4139,plain,~actual_world(skolem0001)|barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4136, c56])).
% 7.50/7.71  cnf(c4145,plain,barrel(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4139, c20])).
% 7.50/7.71  cnf(c19,negated_conjecture,actual_world(skolem0001)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c55,negated_conjecture,city(skolem0001,skolem0003)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c73,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c91,negated_conjecture,placename(skolem0001,skolem0002)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c109,negated_conjecture,chevy(skolem0001,skolem0003)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c127,negated_conjecture,white(skolem0001,skolem0003)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c145,negated_conjecture,dirty(skolem0001,skolem0003)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c163,negated_conjecture,old(skolem0001,skolem0003)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c181,negated_conjecture,street(skolem0001,skolem0004)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c199,negated_conjecture,lonely(skolem0001,skolem0004)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c217,negated_conjecture,event(skolem0001,skolem0005)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c253,negated_conjecture,present(skolem0001,skolem0005)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c271,negated_conjecture,barrel(skolem0001,skolem0005)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c37,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c235,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c289,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c307,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c325,negated_conjecture,~actual_world(X183)|~of(X183,X184,X182)|~city(X183,X182)|~hollywood_placename(X183,X184)|~placename(X183,X184)|~chevy(X183,X185)|~white(X183,X185)|~dirty(X183,X185)|~old(X183,X185)|~street(X183,X181)|~lonely(X183,X181)|~event(X183,X186)|~agent(X183,X186,X185)|~present(X183,X186)|~barrel(X183,X186)|~down(X183,X186,X181)|~in(X183,X186,X182)|present(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c1333,plain,~actual_world(skolem0001)|~of(skolem0001,X1184,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1184)|~placename(skolem0001,X1184)|~chevy(skolem0001,X1185)|~white(skolem0001,X1185)|~dirty(skolem0001,X1185)|~old(skolem0001,X1185)|~street(skolem0001,X1186)|~lonely(skolem0001,X1186)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1185)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X1186)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c325, c307])).
% 7.50/7.71  cnf(c3977,plain,~actual_world(skolem0001)|~of(skolem0001,X1188,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1188)|~placename(skolem0001,X1188)|~chevy(skolem0001,X1187)|~white(skolem0001,X1187)|~dirty(skolem0001,X1187)|~old(skolem0001,X1187)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1187)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c1333, c289])).
% 7.50/7.71  cnf(c3984,plain,~actual_world(skolem0001)|~of(skolem0001,X1189,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1189)|~placename(skolem0001,X1189)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3977, c235])).
% 7.50/7.71  cnf(c3985,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3984, c37])).
% 7.50/7.71  cnf(c3992,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3985, c271])).
% 7.50/7.71  cnf(c3997,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3992, c253])).
% 7.50/7.71  cnf(c4008,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3997, c217])).
% 7.50/7.71  cnf(c4012,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4008, c199])).
% 7.50/7.71  cnf(c4016,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4012, c181])).
% 7.50/7.71  cnf(c4025,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4016, c163])).
% 7.50/7.71  cnf(c4027,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4025, c145])).
% 7.50/7.71  cnf(c4036,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4027, c127])).
% 7.50/7.71  cnf(c4044,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4036, c109])).
% 7.50/7.71  cnf(c4046,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4044, c91])).
% 7.50/7.71  cnf(c4054,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4046, c73])).
% 7.50/7.71  cnf(c4058,plain,~actual_world(skolem0001)|present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4054, c55])).
% 7.50/7.71  cnf(c4063,plain,present(skolem0006,skolem0011),inference(resolution,[status(thm)],[c4058, c19])).
% 7.50/7.71  cnf(c17,negated_conjecture,actual_world(skolem0001)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c53,negated_conjecture,city(skolem0001,skolem0003)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c71,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c89,negated_conjecture,placename(skolem0001,skolem0002)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c107,negated_conjecture,chevy(skolem0001,skolem0003)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c125,negated_conjecture,white(skolem0001,skolem0003)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c143,negated_conjecture,dirty(skolem0001,skolem0003)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c161,negated_conjecture,old(skolem0001,skolem0003)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c179,negated_conjecture,street(skolem0001,skolem0004)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c197,negated_conjecture,lonely(skolem0001,skolem0004)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c215,negated_conjecture,event(skolem0001,skolem0005)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c251,negated_conjecture,present(skolem0001,skolem0005)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c269,negated_conjecture,barrel(skolem0001,skolem0005)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c35,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c233,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c287,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c305,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c323,negated_conjecture,~actual_world(X171)|~of(X171,X172,X170)|~city(X171,X170)|~hollywood_placename(X171,X172)|~placename(X171,X172)|~chevy(X171,X173)|~white(X171,X173)|~dirty(X171,X173)|~old(X171,X173)|~street(X171,X169)|~lonely(X171,X169)|~event(X171,X174)|~agent(X171,X174,X173)|~present(X171,X174)|~barrel(X171,X174)|~down(X171,X174,X169)|~in(X171,X174,X170)|event(skolem0006,skolem0011),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c1271,plain,~actual_world(skolem0001)|~of(skolem0001,X1136,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1136)|~placename(skolem0001,X1136)|~chevy(skolem0001,X1134)|~white(skolem0001,X1134)|~dirty(skolem0001,X1134)|~old(skolem0001,X1134)|~street(skolem0001,X1135)|~lonely(skolem0001,X1135)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1134)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X1135)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c323, c305])).
% 7.50/7.71  cnf(c3849,plain,~actual_world(skolem0001)|~of(skolem0001,X1138,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1138)|~placename(skolem0001,X1138)|~chevy(skolem0001,X1137)|~white(skolem0001,X1137)|~dirty(skolem0001,X1137)|~old(skolem0001,X1137)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1137)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c1271, c287])).
% 7.50/7.71  cnf(c3851,plain,~actual_world(skolem0001)|~of(skolem0001,X1139,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1139)|~placename(skolem0001,X1139)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3849, c233])).
% 7.50/7.71  cnf(c3858,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3851, c35])).
% 7.50/7.71  cnf(c3865,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3858, c269])).
% 7.50/7.71  cnf(c3872,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3865, c251])).
% 7.50/7.71  cnf(c3879,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3872, c215])).
% 7.50/7.71  cnf(c3890,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3879, c197])).
% 7.50/7.71  cnf(c3897,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3890, c179])).
% 7.50/7.71  cnf(c3903,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3897, c161])).
% 7.50/7.71  cnf(c3907,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3903, c143])).
% 7.50/7.71  cnf(c3917,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3907, c125])).
% 7.50/7.71  cnf(c3923,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3917, c107])).
% 7.50/7.71  cnf(c3930,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3923, c89])).
% 7.50/7.71  cnf(c3935,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3930, c71])).
% 7.50/7.71  cnf(c3942,plain,~actual_world(skolem0001)|event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3935, c53])).
% 7.50/7.71  cnf(c3949,plain,event(skolem0006,skolem0011),inference(resolution,[status(thm)],[c3942, c17])).
% 7.50/7.71  cnf(c16,negated_conjecture,actual_world(skolem0001)|lonely(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c52,negated_conjecture,city(skolem0001,skolem0003)|lonely(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c70,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|lonely(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c88,negated_conjecture,placename(skolem0001,skolem0002)|lonely(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c106,negated_conjecture,chevy(skolem0001,skolem0003)|lonely(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c124,negated_conjecture,white(skolem0001,skolem0003)|lonely(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c142,negated_conjecture,dirty(skolem0001,skolem0003)|lonely(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c160,negated_conjecture,old(skolem0001,skolem0003)|lonely(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c178,negated_conjecture,street(skolem0001,skolem0004)|lonely(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c196,negated_conjecture,lonely(skolem0001,skolem0004)|lonely(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c214,negated_conjecture,event(skolem0001,skolem0005)|lonely(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c250,negated_conjecture,present(skolem0001,skolem0005)|lonely(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c268,negated_conjecture,barrel(skolem0001,skolem0005)|lonely(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c34,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|lonely(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c232,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|lonely(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c286,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|lonely(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c304,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|lonely(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c322,negated_conjecture,~actual_world(X165)|~of(X165,X166,X164)|~city(X165,X164)|~hollywood_placename(X165,X166)|~placename(X165,X166)|~chevy(X165,X167)|~white(X165,X167)|~dirty(X165,X167)|~old(X165,X167)|~street(X165,X163)|~lonely(X165,X163)|~event(X165,X168)|~agent(X165,X168,X167)|~present(X165,X168)|~barrel(X165,X168)|~down(X165,X168,X163)|~in(X165,X168,X164)|lonely(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.71  cnf(c1242,plain,~actual_world(skolem0001)|~of(skolem0001,X1077,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1077)|~placename(skolem0001,X1077)|~chevy(skolem0001,X1079)|~white(skolem0001,X1079)|~dirty(skolem0001,X1079)|~old(skolem0001,X1079)|~street(skolem0001,X1078)|~lonely(skolem0001,X1078)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1079)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X1078)|lonely(skolem0006,skolem0010),inference(resolution,[status(thm)],[c322, c304])).
% 7.50/7.71  cnf(c3716,plain,~actual_world(skolem0001)|~of(skolem0001,X1082,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1082)|~placename(skolem0001,X1082)|~chevy(skolem0001,X1083)|~white(skolem0001,X1083)|~dirty(skolem0001,X1083)|~old(skolem0001,X1083)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1083)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|lonely(skolem0006,skolem0010),inference(resolution,[status(thm)],[c1242, c286])).
% 7.50/7.71  cnf(c3727,plain,~actual_world(skolem0001)|~of(skolem0001,X1084,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1084)|~placename(skolem0001,X1084)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|lonely(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3716, c232])).
% 7.50/7.71  cnf(c3739,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|lonely(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3727, c34])).
% 7.50/7.71  cnf(c3742,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|lonely(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3739, c268])).
% 7.50/7.71  cnf(c3752,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|lonely(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3742, c250])).
% 7.50/7.71  cnf(c3760,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|lonely(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3752, c214])).
% 7.50/7.71  cnf(c3766,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|lonely(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3760, c196])).
% 7.50/7.71  cnf(c3778,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|lonely(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3766, c178])).
% 7.50/7.71  cnf(c3785,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|lonely(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3778, c160])).
% 7.50/7.71  cnf(c3790,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|lonely(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3785, c142])).
% 7.50/7.72  cnf(c3802,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|lonely(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3790, c124])).
% 7.50/7.72  cnf(c3807,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|lonely(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3802, c106])).
% 7.50/7.72  cnf(c3814,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|lonely(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3807, c88])).
% 7.50/7.72  cnf(c3823,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|lonely(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3814, c70])).
% 7.50/7.72  cnf(c3831,plain,~actual_world(skolem0001)|lonely(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3823, c52])).
% 7.50/7.72  cnf(c3837,plain,lonely(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3831, c16])).
% 7.50/7.72  cnf(c15,negated_conjecture,actual_world(skolem0001)|street(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c51,negated_conjecture,city(skolem0001,skolem0003)|street(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c69,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|street(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c87,negated_conjecture,placename(skolem0001,skolem0002)|street(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c105,negated_conjecture,chevy(skolem0001,skolem0003)|street(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c123,negated_conjecture,white(skolem0001,skolem0003)|street(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c141,negated_conjecture,dirty(skolem0001,skolem0003)|street(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c159,negated_conjecture,old(skolem0001,skolem0003)|street(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c177,negated_conjecture,street(skolem0001,skolem0004)|street(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c195,negated_conjecture,lonely(skolem0001,skolem0004)|street(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c213,negated_conjecture,event(skolem0001,skolem0005)|street(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c249,negated_conjecture,present(skolem0001,skolem0005)|street(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c267,negated_conjecture,barrel(skolem0001,skolem0005)|street(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c33,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|street(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c231,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|street(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c285,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|street(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c303,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|street(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c321,negated_conjecture,~actual_world(X159)|~of(X159,X160,X158)|~city(X159,X158)|~hollywood_placename(X159,X160)|~placename(X159,X160)|~chevy(X159,X161)|~white(X159,X161)|~dirty(X159,X161)|~old(X159,X161)|~street(X159,X157)|~lonely(X159,X157)|~event(X159,X162)|~agent(X159,X162,X161)|~present(X159,X162)|~barrel(X159,X162)|~down(X159,X162,X157)|~in(X159,X162,X158)|street(skolem0006,skolem0010),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c1212,plain,~actual_world(skolem0001)|~of(skolem0001,X1017,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1017)|~placename(skolem0001,X1017)|~chevy(skolem0001,X1016)|~white(skolem0001,X1016)|~dirty(skolem0001,X1016)|~old(skolem0001,X1016)|~street(skolem0001,X1015)|~lonely(skolem0001,X1015)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1016)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X1015)|street(skolem0006,skolem0010),inference(resolution,[status(thm)],[c321, c303])).
% 7.50/7.72  cnf(c3580,plain,~actual_world(skolem0001)|~of(skolem0001,X1018,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1018)|~placename(skolem0001,X1018)|~chevy(skolem0001,X1019)|~white(skolem0001,X1019)|~dirty(skolem0001,X1019)|~old(skolem0001,X1019)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X1019)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|street(skolem0006,skolem0010),inference(resolution,[status(thm)],[c1212, c285])).
% 7.50/7.72  cnf(c3588,plain,~actual_world(skolem0001)|~of(skolem0001,X1020,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X1020)|~placename(skolem0001,X1020)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|street(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3580, c231])).
% 7.50/7.72  cnf(c3590,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|street(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3588, c33])).
% 7.50/7.72  cnf(c3603,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|street(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3590, c267])).
% 7.50/7.72  cnf(c3614,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|street(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3603, c249])).
% 7.50/7.72  cnf(c3624,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|street(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3614, c213])).
% 7.50/7.72  cnf(c3633,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|street(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3624, c195])).
% 7.50/7.72  cnf(c3639,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|street(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3633, c177])).
% 7.50/7.72  cnf(c3645,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|street(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3639, c159])).
% 7.50/7.72  cnf(c3658,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|street(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3645, c141])).
% 7.50/7.72  cnf(c3668,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|street(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3658, c123])).
% 7.50/7.72  cnf(c3678,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|street(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3668, c105])).
% 7.50/7.72  cnf(c3681,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|street(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3678, c87])).
% 7.50/7.72  cnf(c3689,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|street(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3681, c69])).
% 7.50/7.72  cnf(c3700,plain,~actual_world(skolem0001)|street(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3689, c51])).
% 7.50/7.72  cnf(c3715,plain,street(skolem0006,skolem0010),inference(resolution,[status(thm)],[c3700, c15])).
% 7.50/7.72  cnf(c14,negated_conjecture,actual_world(skolem0001)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c50,negated_conjecture,city(skolem0001,skolem0003)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c68,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c86,negated_conjecture,placename(skolem0001,skolem0002)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c104,negated_conjecture,chevy(skolem0001,skolem0003)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c122,negated_conjecture,white(skolem0001,skolem0003)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c140,negated_conjecture,dirty(skolem0001,skolem0003)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c158,negated_conjecture,old(skolem0001,skolem0003)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c176,negated_conjecture,street(skolem0001,skolem0004)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c194,negated_conjecture,lonely(skolem0001,skolem0004)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c212,negated_conjecture,event(skolem0001,skolem0005)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c248,negated_conjecture,present(skolem0001,skolem0005)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c266,negated_conjecture,barrel(skolem0001,skolem0005)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c32,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c230,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c284,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c302,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c320,negated_conjecture,~actual_world(X153)|~of(X153,X154,X152)|~city(X153,X152)|~hollywood_placename(X153,X154)|~placename(X153,X154)|~chevy(X153,X155)|~white(X153,X155)|~dirty(X153,X155)|~old(X153,X155)|~street(X153,X151)|~lonely(X153,X151)|~event(X153,X156)|~agent(X153,X156,X155)|~present(X153,X156)|~barrel(X153,X156)|~down(X153,X156,X151)|~in(X153,X156,X152)|old(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c1149,plain,~actual_world(skolem0001)|~of(skolem0001,X946,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X946)|~placename(skolem0001,X946)|~chevy(skolem0001,X945)|~white(skolem0001,X945)|~dirty(skolem0001,X945)|~old(skolem0001,X945)|~street(skolem0001,X944)|~lonely(skolem0001,X944)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X945)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X944)|old(skolem0006,skolem0009),inference(resolution,[status(thm)],[c320, c302])).
% 7.50/7.72  cnf(c3420,plain,~actual_world(skolem0001)|~of(skolem0001,X948,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X948)|~placename(skolem0001,X948)|~chevy(skolem0001,X947)|~white(skolem0001,X947)|~dirty(skolem0001,X947)|~old(skolem0001,X947)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X947)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|old(skolem0006,skolem0009),inference(resolution,[status(thm)],[c1149, c284])).
% 7.50/7.72  cnf(c3422,plain,~actual_world(skolem0001)|~of(skolem0001,X951,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X951)|~placename(skolem0001,X951)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|old(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3420, c230])).
% 7.50/7.72  cnf(c3432,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|old(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3422, c32])).
% 7.50/7.72  cnf(c3445,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|old(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3432, c266])).
% 7.50/7.72  cnf(c3457,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|old(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3445, c248])).
% 7.50/7.72  cnf(c3465,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|old(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3457, c212])).
% 7.50/7.72  cnf(c3480,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|old(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3465, c194])).
% 7.50/7.72  cnf(c3486,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|old(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3480, c176])).
% 7.50/7.72  cnf(c3498,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|old(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3486, c158])).
% 7.50/7.72  cnf(c3504,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|old(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3498, c140])).
% 7.50/7.72  cnf(c3519,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|old(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3504, c122])).
% 7.50/7.72  cnf(c3522,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|old(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3519, c104])).
% 7.50/7.72  cnf(c3535,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|old(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3522, c86])).
% 7.50/7.72  cnf(c3549,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|old(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3535, c68])).
% 7.50/7.72  cnf(c3556,plain,~actual_world(skolem0001)|old(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3549, c50])).
% 7.50/7.72  cnf(c3562,plain,old(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3556, c14])).
% 7.50/7.72  cnf(c13,negated_conjecture,actual_world(skolem0001)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c49,negated_conjecture,city(skolem0001,skolem0003)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c67,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c85,negated_conjecture,placename(skolem0001,skolem0002)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c103,negated_conjecture,chevy(skolem0001,skolem0003)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c121,negated_conjecture,white(skolem0001,skolem0003)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c139,negated_conjecture,dirty(skolem0001,skolem0003)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c157,negated_conjecture,old(skolem0001,skolem0003)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c175,negated_conjecture,street(skolem0001,skolem0004)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c193,negated_conjecture,lonely(skolem0001,skolem0004)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c211,negated_conjecture,event(skolem0001,skolem0005)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c247,negated_conjecture,present(skolem0001,skolem0005)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c265,negated_conjecture,barrel(skolem0001,skolem0005)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c31,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c229,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c283,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c301,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c319,negated_conjecture,~actual_world(X147)|~of(X147,X148,X146)|~city(X147,X146)|~hollywood_placename(X147,X148)|~placename(X147,X148)|~chevy(X147,X149)|~white(X147,X149)|~dirty(X147,X149)|~old(X147,X149)|~street(X147,X145)|~lonely(X147,X145)|~event(X147,X150)|~agent(X147,X150,X149)|~present(X147,X150)|~barrel(X147,X150)|~down(X147,X150,X145)|~in(X147,X150,X146)|dirty(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c1116,plain,~actual_world(skolem0001)|~of(skolem0001,X869,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X869)|~placename(skolem0001,X869)|~chevy(skolem0001,X870)|~white(skolem0001,X870)|~dirty(skolem0001,X870)|~old(skolem0001,X870)|~street(skolem0001,X868)|~lonely(skolem0001,X868)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X870)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X868)|dirty(skolem0006,skolem0009),inference(resolution,[status(thm)],[c319, c301])).
% 7.50/7.72  cnf(c3204,plain,~actual_world(skolem0001)|~of(skolem0001,X871,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X871)|~placename(skolem0001,X871)|~chevy(skolem0001,X872)|~white(skolem0001,X872)|~dirty(skolem0001,X872)|~old(skolem0001,X872)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X872)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|dirty(skolem0006,skolem0009),inference(resolution,[status(thm)],[c1116, c283])).
% 7.50/7.72  cnf(c3214,plain,~actual_world(skolem0001)|~of(skolem0001,X873,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X873)|~placename(skolem0001,X873)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|dirty(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3204, c229])).
% 7.50/7.72  cnf(c3227,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|dirty(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3214, c31])).
% 7.50/7.72  cnf(c3241,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|dirty(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3227, c265])).
% 7.50/7.72  cnf(c3252,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|dirty(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3241, c247])).
% 7.50/7.72  cnf(c3258,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|dirty(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3252, c211])).
% 7.50/7.72  cnf(c3272,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|dirty(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3258, c193])).
% 7.50/7.72  cnf(c3280,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|dirty(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3272, c175])).
% 7.50/7.72  cnf(c3294,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|dirty(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3280, c157])).
% 7.50/7.72  cnf(c3303,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|dirty(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3294, c139])).
% 7.50/7.72  cnf(c3320,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|dirty(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3303, c121])).
% 7.50/7.72  cnf(c3327,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|dirty(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3320, c103])).
% 7.50/7.72  cnf(c3343,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|dirty(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3327, c85])).
% 7.50/7.72  cnf(c3352,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|dirty(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3343, c67])).
% 7.50/7.72  cnf(c3358,plain,~actual_world(skolem0001)|dirty(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3352, c49])).
% 7.50/7.72  cnf(c3376,plain,dirty(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3358, c13])).
% 7.50/7.72  cnf(c12,negated_conjecture,actual_world(skolem0001)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c48,negated_conjecture,city(skolem0001,skolem0003)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c66,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c84,negated_conjecture,placename(skolem0001,skolem0002)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c102,negated_conjecture,chevy(skolem0001,skolem0003)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c120,negated_conjecture,white(skolem0001,skolem0003)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c138,negated_conjecture,dirty(skolem0001,skolem0003)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c156,negated_conjecture,old(skolem0001,skolem0003)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c174,negated_conjecture,street(skolem0001,skolem0004)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c192,negated_conjecture,lonely(skolem0001,skolem0004)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c210,negated_conjecture,event(skolem0001,skolem0005)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c246,negated_conjecture,present(skolem0001,skolem0005)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c264,negated_conjecture,barrel(skolem0001,skolem0005)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c30,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c228,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c282,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c300,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c318,negated_conjecture,~actual_world(X136)|~of(X136,X137,X135)|~city(X136,X135)|~hollywood_placename(X136,X137)|~placename(X136,X137)|~chevy(X136,X138)|~white(X136,X138)|~dirty(X136,X138)|~old(X136,X138)|~street(X136,X134)|~lonely(X136,X134)|~event(X136,X139)|~agent(X136,X139,X138)|~present(X136,X139)|~barrel(X136,X139)|~down(X136,X139,X134)|~in(X136,X139,X135)|white(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.50/7.72  cnf(c1062,plain,~actual_world(skolem0001)|~of(skolem0001,X785,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X785)|~placename(skolem0001,X785)|~chevy(skolem0001,X783)|~white(skolem0001,X783)|~dirty(skolem0001,X783)|~old(skolem0001,X783)|~street(skolem0001,X784)|~lonely(skolem0001,X784)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X783)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X784)|white(skolem0006,skolem0009),inference(resolution,[status(thm)],[c318, c300])).
% 7.50/7.72  cnf(c3014,plain,~actual_world(skolem0001)|~of(skolem0001,X787,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X787)|~placename(skolem0001,X787)|~chevy(skolem0001,X786)|~white(skolem0001,X786)|~dirty(skolem0001,X786)|~old(skolem0001,X786)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X786)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|white(skolem0006,skolem0009),inference(resolution,[status(thm)],[c1062, c282])).
% 7.50/7.72  cnf(c3031,plain,~actual_world(skolem0001)|~of(skolem0001,X788,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X788)|~placename(skolem0001,X788)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|white(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3014, c228])).
% 7.50/7.72  cnf(c3037,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|white(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3031, c30])).
% 7.50/7.72  cnf(c3053,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|white(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3037, c264])).
% 7.50/7.72  cnf(c3063,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|white(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3053, c246])).
% 7.50/7.72  cnf(c3079,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|white(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3063, c210])).
% 7.56/7.72  cnf(c3088,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|white(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3079, c192])).
% 7.56/7.72  cnf(c3104,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|white(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3088, c174])).
% 7.56/7.72  cnf(c3110,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|white(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3104, c156])).
% 7.56/7.72  cnf(c3118,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|white(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3110, c138])).
% 7.56/7.72  cnf(c3141,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|white(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3118, c120])).
% 7.56/7.72  cnf(c3149,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|white(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3141, c102])).
% 7.56/7.72  cnf(c3160,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|white(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3149, c84])).
% 7.56/7.72  cnf(c3174,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|white(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3160, c66])).
% 7.56/7.72  cnf(c3179,plain,~actual_world(skolem0001)|white(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3174, c48])).
% 7.56/7.72  cnf(c3190,plain,white(skolem0006,skolem0009),inference(resolution,[status(thm)],[c3179, c12])).
% 7.56/7.72  cnf(c11,negated_conjecture,actual_world(skolem0001)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c47,negated_conjecture,city(skolem0001,skolem0003)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c65,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c83,negated_conjecture,placename(skolem0001,skolem0002)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c101,negated_conjecture,chevy(skolem0001,skolem0003)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c119,negated_conjecture,white(skolem0001,skolem0003)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c137,negated_conjecture,dirty(skolem0001,skolem0003)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c155,negated_conjecture,old(skolem0001,skolem0003)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c173,negated_conjecture,street(skolem0001,skolem0004)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c191,negated_conjecture,lonely(skolem0001,skolem0004)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c209,negated_conjecture,event(skolem0001,skolem0005)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c245,negated_conjecture,present(skolem0001,skolem0005)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c263,negated_conjecture,barrel(skolem0001,skolem0005)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c29,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c227,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c281,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c299,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c317,negated_conjecture,~actual_world(X130)|~of(X130,X131,X129)|~city(X130,X129)|~hollywood_placename(X130,X131)|~placename(X130,X131)|~chevy(X130,X132)|~white(X130,X132)|~dirty(X130,X132)|~old(X130,X132)|~street(X130,X128)|~lonely(X130,X128)|~event(X130,X133)|~agent(X130,X133,X132)|~present(X130,X133)|~barrel(X130,X133)|~down(X130,X133,X128)|~in(X130,X133,X129)|chevy(skolem0006,skolem0009),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c1022,plain,~actual_world(skolem0001)|~of(skolem0001,X691,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X691)|~placename(skolem0001,X691)|~chevy(skolem0001,X693)|~white(skolem0001,X693)|~dirty(skolem0001,X693)|~old(skolem0001,X693)|~street(skolem0001,X692)|~lonely(skolem0001,X692)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X693)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X692)|chevy(skolem0006,skolem0009),inference(resolution,[status(thm)],[c317, c299])).
% 7.56/7.72  cnf(c2761,plain,~actual_world(skolem0001)|~of(skolem0001,X697,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X697)|~placename(skolem0001,X697)|~chevy(skolem0001,X696)|~white(skolem0001,X696)|~dirty(skolem0001,X696)|~old(skolem0001,X696)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X696)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|chevy(skolem0006,skolem0009),inference(resolution,[status(thm)],[c1022, c281])).
% 7.56/7.72  cnf(c2776,plain,~actual_world(skolem0001)|~of(skolem0001,X698,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X698)|~placename(skolem0001,X698)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|chevy(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2761, c227])).
% 7.56/7.72  cnf(c2781,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|chevy(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2776, c29])).
% 7.56/7.72  cnf(c2796,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|chevy(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2781, c263])).
% 7.56/7.72  cnf(c2808,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|chevy(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2796, c245])).
% 7.56/7.72  cnf(c2827,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|chevy(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2808, c209])).
% 7.56/7.72  cnf(c2833,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|chevy(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2827, c191])).
% 7.56/7.72  cnf(c2850,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|chevy(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2833, c173])).
% 7.56/7.72  cnf(c2859,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|chevy(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2850, c155])).
% 7.56/7.72  cnf(c2877,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|chevy(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2859, c137])).
% 7.56/7.72  cnf(c2888,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|chevy(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2877, c119])).
% 7.56/7.72  cnf(c2898,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|chevy(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2888, c101])).
% 7.56/7.72  cnf(c2910,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|chevy(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2898, c83])).
% 7.56/7.72  cnf(c2926,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|chevy(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2910, c65])).
% 7.56/7.72  cnf(c2944,plain,~actual_world(skolem0001)|chevy(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2926, c47])).
% 7.56/7.72  cnf(c2947,plain,chevy(skolem0006,skolem0009),inference(resolution,[status(thm)],[c2944, c11])).
% 7.56/7.72  cnf(c10,negated_conjecture,actual_world(skolem0001)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c46,negated_conjecture,city(skolem0001,skolem0003)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c64,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c82,negated_conjecture,placename(skolem0001,skolem0002)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c100,negated_conjecture,chevy(skolem0001,skolem0003)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c118,negated_conjecture,white(skolem0001,skolem0003)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c136,negated_conjecture,dirty(skolem0001,skolem0003)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c154,negated_conjecture,old(skolem0001,skolem0003)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c172,negated_conjecture,street(skolem0001,skolem0004)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c190,negated_conjecture,lonely(skolem0001,skolem0004)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c208,negated_conjecture,event(skolem0001,skolem0005)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c244,negated_conjecture,present(skolem0001,skolem0005)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c262,negated_conjecture,barrel(skolem0001,skolem0005)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c28,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c226,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c280,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c298,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c316,negated_conjecture,~actual_world(X124)|~of(X124,X125,X123)|~city(X124,X123)|~hollywood_placename(X124,X125)|~placename(X124,X125)|~chevy(X124,X126)|~white(X124,X126)|~dirty(X124,X126)|~old(X124,X126)|~street(X124,X122)|~lonely(X124,X122)|~event(X124,X127)|~agent(X124,X127,X126)|~present(X124,X127)|~barrel(X124,X127)|~down(X124,X127,X122)|~in(X124,X127,X123)|placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.72  cnf(c986,plain,~actual_world(skolem0001)|~of(skolem0001,X595,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X595)|~placename(skolem0001,X595)|~chevy(skolem0001,X594)|~white(skolem0001,X594)|~dirty(skolem0001,X594)|~old(skolem0001,X594)|~street(skolem0001,X596)|~lonely(skolem0001,X596)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X594)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X596)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c316, c298])).
% 7.56/7.72  cnf(c2512,plain,~actual_world(skolem0001)|~of(skolem0001,X598,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X598)|~placename(skolem0001,X598)|~chevy(skolem0001,X597)|~white(skolem0001,X597)|~dirty(skolem0001,X597)|~old(skolem0001,X597)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X597)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c986, c280])).
% 7.56/7.72  cnf(c2525,plain,~actual_world(skolem0001)|~of(skolem0001,X599,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X599)|~placename(skolem0001,X599)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2512, c226])).
% 7.56/7.72  cnf(c2541,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2525, c28])).
% 7.56/7.72  cnf(c2558,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2541, c262])).
% 7.56/7.72  cnf(c2574,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2558, c244])).
% 7.56/7.73  cnf(c2589,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2574, c208])).
% 7.56/7.73  cnf(c2607,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2589, c190])).
% 7.56/7.73  cnf(c2615,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2607, c172])).
% 7.56/7.73  cnf(c2631,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2615, c154])).
% 7.56/7.73  cnf(c2644,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2631, c136])).
% 7.56/7.73  cnf(c2662,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2644, c118])).
% 7.56/7.73  cnf(c2665,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2662, c100])).
% 7.56/7.73  cnf(c2684,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2665, c82])).
% 7.56/7.73  cnf(c2700,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2684, c64])).
% 7.56/7.73  cnf(c2714,plain,~actual_world(skolem0001)|placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2700, c46])).
% 7.56/7.73  cnf(c2723,plain,placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2714, c10])).
% 7.56/7.73  cnf(c9,negated_conjecture,actual_world(skolem0001)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c45,negated_conjecture,city(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c63,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c81,negated_conjecture,placename(skolem0001,skolem0002)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c99,negated_conjecture,chevy(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c117,negated_conjecture,white(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c135,negated_conjecture,dirty(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c153,negated_conjecture,old(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c171,negated_conjecture,street(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c189,negated_conjecture,lonely(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c207,negated_conjecture,event(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c243,negated_conjecture,present(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c261,negated_conjecture,barrel(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c27,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c225,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c279,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c297,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c315,negated_conjecture,~actual_world(X118)|~of(X118,X119,X117)|~city(X118,X117)|~hollywood_placename(X118,X119)|~placename(X118,X119)|~chevy(X118,X120)|~white(X118,X120)|~dirty(X118,X120)|~old(X118,X120)|~street(X118,X116)|~lonely(X118,X116)|~event(X118,X121)|~agent(X118,X121,X120)|~present(X118,X121)|~barrel(X118,X121)|~down(X118,X121,X116)|~in(X118,X121,X117)|hollywood_placename(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c950,plain,~actual_world(skolem0001)|~of(skolem0001,X488,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X488)|~placename(skolem0001,X488)|~chevy(skolem0001,X489)|~white(skolem0001,X489)|~dirty(skolem0001,X489)|~old(skolem0001,X489)|~street(skolem0001,X490)|~lonely(skolem0001,X490)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X489)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X490)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c315, c297])).
% 7.56/7.73  cnf(c2229,plain,~actual_world(skolem0001)|~of(skolem0001,X491,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X491)|~placename(skolem0001,X491)|~chevy(skolem0001,X492)|~white(skolem0001,X492)|~dirty(skolem0001,X492)|~old(skolem0001,X492)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X492)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c950, c279])).
% 7.56/7.73  cnf(c2239,plain,~actual_world(skolem0001)|~of(skolem0001,X495,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X495)|~placename(skolem0001,X495)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2229, c225])).
% 7.56/7.73  cnf(c2259,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2239, c27])).
% 7.56/7.73  cnf(c2271,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2259, c261])).
% 7.56/7.73  cnf(c2289,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2271, c243])).
% 7.56/7.73  cnf(c2298,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2289, c207])).
% 7.56/7.73  cnf(c2316,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2298, c189])).
% 7.56/7.73  cnf(c2327,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2316, c171])).
% 7.56/7.73  cnf(c2343,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2327, c153])).
% 7.56/7.73  cnf(c2359,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2343, c135])).
% 7.56/7.73  cnf(c2373,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2359, c117])).
% 7.56/7.73  cnf(c2387,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2373, c99])).
% 7.56/7.73  cnf(c2412,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2387, c81])).
% 7.56/7.73  cnf(c2424,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2412, c63])).
% 7.56/7.73  cnf(c2437,plain,~actual_world(skolem0001)|hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2424, c45])).
% 7.56/7.73  cnf(c2444,plain,hollywood_placename(skolem0006,skolem0008),inference(resolution,[status(thm)],[c2437, c9])).
% 7.56/7.73  cnf(c8,negated_conjecture,actual_world(skolem0001)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c44,negated_conjecture,city(skolem0001,skolem0003)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c62,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c80,negated_conjecture,placename(skolem0001,skolem0002)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c98,negated_conjecture,chevy(skolem0001,skolem0003)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c116,negated_conjecture,white(skolem0001,skolem0003)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c134,negated_conjecture,dirty(skolem0001,skolem0003)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c152,negated_conjecture,old(skolem0001,skolem0003)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c170,negated_conjecture,street(skolem0001,skolem0004)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c188,negated_conjecture,lonely(skolem0001,skolem0004)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c206,negated_conjecture,event(skolem0001,skolem0005)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c242,negated_conjecture,present(skolem0001,skolem0005)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c260,negated_conjecture,barrel(skolem0001,skolem0005)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c26,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c224,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c278,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c296,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c314,negated_conjecture,~actual_world(X112)|~of(X112,X113,X111)|~city(X112,X111)|~hollywood_placename(X112,X113)|~placename(X112,X113)|~chevy(X112,X114)|~white(X112,X114)|~dirty(X112,X114)|~old(X112,X114)|~street(X112,X110)|~lonely(X112,X110)|~event(X112,X115)|~agent(X112,X115,X114)|~present(X112,X115)|~barrel(X112,X115)|~down(X112,X115,X110)|~in(X112,X115,X111)|city(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c923,plain,~actual_world(skolem0001)|~of(skolem0001,X377,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X377)|~placename(skolem0001,X377)|~chevy(skolem0001,X379)|~white(skolem0001,X379)|~dirty(skolem0001,X379)|~old(skolem0001,X379)|~street(skolem0001,X378)|~lonely(skolem0001,X378)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X379)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X378)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c314, c296])).
% 7.56/7.73  cnf(c1900,plain,~actual_world(skolem0001)|~of(skolem0001,X380,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X380)|~placename(skolem0001,X380)|~chevy(skolem0001,X381)|~white(skolem0001,X381)|~dirty(skolem0001,X381)|~old(skolem0001,X381)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X381)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c923, c278])).
% 7.56/7.73  cnf(c1913,plain,~actual_world(skolem0001)|~of(skolem0001,X382,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X382)|~placename(skolem0001,X382)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c1900, c224])).
% 7.56/7.73  cnf(c1936,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c1913, c26])).
% 7.56/7.73  cnf(c1953,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c1936, c260])).
% 7.56/7.73  cnf(c1967,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c1953, c242])).
% 7.56/7.73  cnf(c1996,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c1967, c206])).
% 7.56/7.73  cnf(c2019,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c1996, c188])).
% 7.56/7.73  cnf(c2025,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c2019, c170])).
% 7.56/7.73  cnf(c2041,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c2025, c152])).
% 7.56/7.73  cnf(c2058,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c2041, c134])).
% 7.56/7.73  cnf(c2087,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c2058, c116])).
% 7.56/7.73  cnf(c2090,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c2087, c98])).
% 7.56/7.73  cnf(c2105,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c2090, c80])).
% 7.56/7.73  cnf(c2134,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c2105, c62])).
% 7.56/7.73  cnf(c2144,plain,~actual_world(skolem0001)|city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c2134, c44])).
% 7.56/7.73  cnf(c2156,plain,city(skolem0006,skolem0007),inference(resolution,[status(thm)],[c2144, c8])).
% 7.56/7.73  cnf(c6,negated_conjecture,actual_world(skolem0001)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c42,negated_conjecture,city(skolem0001,skolem0003)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c60,negated_conjecture,hollywood_placename(skolem0001,skolem0002)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c78,negated_conjecture,placename(skolem0001,skolem0002)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c96,negated_conjecture,chevy(skolem0001,skolem0003)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c114,negated_conjecture,white(skolem0001,skolem0003)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c132,negated_conjecture,dirty(skolem0001,skolem0003)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c150,negated_conjecture,old(skolem0001,skolem0003)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c168,negated_conjecture,street(skolem0001,skolem0004)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c186,negated_conjecture,lonely(skolem0001,skolem0004)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c204,negated_conjecture,event(skolem0001,skolem0005)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c240,negated_conjecture,present(skolem0001,skolem0005)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c258,negated_conjecture,barrel(skolem0001,skolem0005)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c24,negated_conjecture,of(skolem0001,skolem0002,skolem0003)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c222,negated_conjecture,agent(skolem0001,skolem0005,skolem0003)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c276,negated_conjecture,down(skolem0001,skolem0005,skolem0004)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c294,negated_conjecture,in(skolem0001,skolem0005,skolem0003)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c312,negated_conjecture,~actual_world(X101)|~of(X101,X102,X100)|~city(X101,X100)|~hollywood_placename(X101,X102)|~placename(X101,X102)|~chevy(X101,X103)|~white(X101,X103)|~dirty(X101,X103)|~old(X101,X103)|~street(X101,X99)|~lonely(X101,X99)|~event(X101,X104)|~agent(X101,X104,X103)|~present(X101,X104)|~barrel(X101,X104)|~down(X101,X104,X99)|~in(X101,X104,X100)|actual_world(skolem0006),inference(split_conjunct,[status(thm)],[c5])).
% 7.56/7.73  cnf(c862,plain,~actual_world(skolem0001)|~of(skolem0001,X223,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X223)|~placename(skolem0001,X223)|~chevy(skolem0001,X222)|~white(skolem0001,X222)|~dirty(skolem0001,X222)|~old(skolem0001,X222)|~street(skolem0001,X224)|~lonely(skolem0001,X224)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X222)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|~down(skolem0001,skolem0005,X224)|actual_world(skolem0006),inference(resolution,[status(thm)],[c312, c294])).
% 7.56/7.73  cnf(c1521,plain,~actual_world(skolem0001)|~of(skolem0001,X225,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X225)|~placename(skolem0001,X225)|~chevy(skolem0001,X226)|~white(skolem0001,X226)|~dirty(skolem0001,X226)|~old(skolem0001,X226)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X226)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|actual_world(skolem0006),inference(resolution,[status(thm)],[c862, c276])).
% 7.56/7.73  cnf(c1548,plain,~actual_world(skolem0001)|~of(skolem0001,X227,skolem0003)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,X227)|~placename(skolem0001,X227)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1521, c222])).
% 7.56/7.73  cnf(c1558,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|~barrel(skolem0001,skolem0005)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1548, c24])).
% 7.56/7.73  cnf(c1574,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|~present(skolem0001,skolem0005)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1558, c258])).
% 7.56/7.73  cnf(c1590,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|~event(skolem0001,skolem0005)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1574, c240])).
% 7.56/7.73  cnf(c1623,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|~lonely(skolem0001,skolem0004)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1590, c204])).
% 7.56/7.73  cnf(c1640,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|~street(skolem0001,skolem0004)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1623, c186])).
% 7.56/7.73  cnf(c1658,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|~old(skolem0001,skolem0003)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1640, c168])).
% 7.56/7.73  cnf(c1680,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|~dirty(skolem0001,skolem0003)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1658, c150])).
% 7.56/7.73  cnf(c1696,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|~white(skolem0001,skolem0003)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1680, c132])).
% 7.56/7.73  cnf(c1711,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|~chevy(skolem0001,skolem0003)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1696, c114])).
% 7.56/7.73  cnf(c1730,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|~placename(skolem0001,skolem0002)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1711, c96])).
% 7.56/7.73  cnf(c1754,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|~hollywood_placename(skolem0001,skolem0002)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1730, c78])).
% 7.56/7.73  cnf(c1767,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0003)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1754, c60])).
% 7.56/7.73  cnf(c1781,plain,~actual_world(skolem0001)|actual_world(skolem0006),inference(resolution,[status(thm)],[c1767, c42])).
% 7.56/7.73  cnf(c1817,plain,actual_world(skolem0006),inference(resolution,[status(thm)],[c1781, c6])).
% 7.56/7.73  % SZS output end Saturation
% 7.56/7.73  
% 7.56/7.73  % Initial clauses    : 324
% 7.56/7.73  % Processed clauses  : 660
% 7.56/7.73  % Factors computed   : 5
% 7.56/7.73  % Resolvents computed: 4018
% 7.56/7.73  % Tautologies deleted: 255
% 7.56/7.73  % Forward subsumed   : 3432
% 7.56/7.73  % Backward subsumed  : 639
% 7.56/7.73  % -------- CPU Time ---------
% 7.56/7.73  % User time          : 7.357 s
% 7.56/7.73  % System time        : 0.027 s
% 7.56/7.73  % Total time         : 7.384 s
%------------------------------------------------------------------------------