PyRes---1.5.THM-Ref.s

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

% Computer : n028.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:33:30 EDT 2024

% Result   : Theorem 3.90s 4.11s
% Output   : Refutation 3.96s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12  % Problem  : NLP001+1 : TPTP v8.1.2. Released v2.4.0.
% 0.03/0.13  % Command  : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.33  % Computer : n028.cluster.edu
% 0.13/0.33  % Model    : x86_64 x86_64
% 0.13/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33  % Memory   : 8042.1875MB
% 0.13/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33  % CPULimit : 300
% 0.13/0.33  % WCLimit  : 300
% 0.13/0.33  % DateTime : Wed May  8 13:31:52 EDT 2024
% 0.13/0.33  % CPUTime  : 
% 3.90/4.11  % Version:  1.5
% 3.90/4.11  % SZS status Theorem
% 3.90/4.11  % SZS output start CNFRefutation
% 3.90/4.11  fof(co1,conjecture,(((?[U]:(?[V]:(?[W]:(?[X]:(((((((((((((hollywood(U)&city(U))&event(V))&street(W))&way(W))&lonely(W))&chevy(X))&car(X))&white(X))&dirty(X))&old(X))&barrel(V,X))&down(V,W))&in(V,U))))))=>(?[Y]:(?[Z]:(?[X1]:(?[X2]:(((((((((((((hollywood(Y)&city(Y))&event(Z))&chevy(X1))&car(X1))&white(X1))&dirty(X1))&old(X1))&street(X2))&way(X2))&lonely(X2))&barrel(Z,X1))&down(Z,X2))&in(Z,Y)))))))&((?[X3]:(?[X4]:(?[X5]:(?[X6]:(((((((((((((hollywood(X3)&city(X3))&event(X4))&chevy(X5))&car(X5))&white(X5))&dirty(X5))&old(X5))&street(X6))&way(X6))&lonely(X6))&barrel(X4,X5))&down(X4,X6))&in(X4,X3))))))=>(?[X7]:(?[X8]:(?[X9]:(?[X10]:(((((((((((((hollywood(X7)&city(X7))&event(X8))&street(X9))&way(X9))&lonely(X9))&chevy(X10))&car(X10))&white(X10))&dirty(X10))&old(X10))&barrel(X8,X10))&down(X8,X9))&in(X8,X7)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', co1)).
% 3.90/4.11  fof(c0,negated_conjecture,(~(((?[U]:(?[V]:(?[W]:(?[X]:(((((((((((((hollywood(U)&city(U))&event(V))&street(W))&way(W))&lonely(W))&chevy(X))&car(X))&white(X))&dirty(X))&old(X))&barrel(V,X))&down(V,W))&in(V,U))))))=>(?[Y]:(?[Z]:(?[X1]:(?[X2]:(((((((((((((hollywood(Y)&city(Y))&event(Z))&chevy(X1))&car(X1))&white(X1))&dirty(X1))&old(X1))&street(X2))&way(X2))&lonely(X2))&barrel(Z,X1))&down(Z,X2))&in(Z,Y)))))))&((?[X3]:(?[X4]:(?[X5]:(?[X6]:(((((((((((((hollywood(X3)&city(X3))&event(X4))&chevy(X5))&car(X5))&white(X5))&dirty(X5))&old(X5))&street(X6))&way(X6))&lonely(X6))&barrel(X4,X5))&down(X4,X6))&in(X4,X3))))))=>(?[X7]:(?[X8]:(?[X9]:(?[X10]:(((((((((((((hollywood(X7)&city(X7))&event(X8))&street(X9))&way(X9))&lonely(X9))&chevy(X10))&car(X10))&white(X10))&dirty(X10))&old(X10))&barrel(X8,X10))&down(X8,X9))&in(X8,X7))))))))),inference(assume_negation,[status(cth)],[co1])).
% 3.90/4.11  fof(c1,negated_conjecture,(((?[U]:(?[V]:(?[W]:(?[X]:(((((((((((((hollywood(U)&city(U))&event(V))&street(W))&way(W))&lonely(W))&chevy(X))&car(X))&white(X))&dirty(X))&old(X))&barrel(V,X))&down(V,W))&in(V,U))))))&(![Y]:(![Z]:(![X1]:(![X2]:(((((((((((((~hollywood(Y)|~city(Y))|~event(Z))|~chevy(X1))|~car(X1))|~white(X1))|~dirty(X1))|~old(X1))|~street(X2))|~way(X2))|~lonely(X2))|~barrel(Z,X1))|~down(Z,X2))|~in(Z,Y)))))))|((?[X3]:(?[X4]:(?[X5]:(?[X6]:(((((((((((((hollywood(X3)&city(X3))&event(X4))&chevy(X5))&car(X5))&white(X5))&dirty(X5))&old(X5))&street(X6))&way(X6))&lonely(X6))&barrel(X4,X5))&down(X4,X6))&in(X4,X3))))))&(![X7]:(![X8]:(![X9]:(![X10]:(((((((((((((~hollywood(X7)|~city(X7))|~event(X8))|~street(X9))|~way(X9))|~lonely(X9))|~chevy(X10))|~car(X10))|~white(X10))|~dirty(X10))|~old(X10))|~barrel(X8,X10))|~down(X8,X9))|~in(X8,X7)))))))),inference(fof_nnf,[status(thm)],[c0])).
% 3.90/4.11  fof(c2,negated_conjecture,(((?[U]:(?[V]:((?[W]:((?[X]:(((((((((((hollywood(U)&city(U))&event(V))&street(W))&way(W))&lonely(W))&chevy(X))&car(X))&white(X))&dirty(X))&old(X))&barrel(V,X)))&down(V,W)))&in(V,U))))&(![Y]:(![Z]:((![X1]:(![X2]:((((((((((((~hollywood(Y)|~city(Y))|~event(Z))|~chevy(X1))|~car(X1))|~white(X1))|~dirty(X1))|~old(X1))|~street(X2))|~way(X2))|~lonely(X2))|~barrel(Z,X1))|~down(Z,X2))))|~in(Z,Y)))))|((?[X3]:(?[X4]:((?[X5]:(?[X6]:((((((((((((hollywood(X3)&city(X3))&event(X4))&chevy(X5))&car(X5))&white(X5))&dirty(X5))&old(X5))&street(X6))&way(X6))&lonely(X6))&barrel(X4,X5))&down(X4,X6))))&in(X4,X3))))&(![X7]:(![X8]:((![X9]:((![X10]:(((((((((((~hollywood(X7)|~city(X7))|~event(X8))|~street(X9))|~way(X9))|~lonely(X9))|~chevy(X10))|~car(X10))|~white(X10))|~dirty(X10))|~old(X10))|~barrel(X8,X10)))|~down(X8,X9)))|~in(X8,X7)))))),inference(shift_quantors,[status(thm)],[c1])).
% 3.90/4.11  fof(c3,negated_conjecture,(((?[X2]:(?[X3]:((?[X4]:((?[X5]:(((((((((((hollywood(X2)&city(X2))&event(X3))&street(X4))&way(X4))&lonely(X4))&chevy(X5))&car(X5))&white(X5))&dirty(X5))&old(X5))&barrel(X3,X5)))&down(X3,X4)))&in(X3,X2))))&(![X6]:(![X7]:((![X8]:(![X9]:((((((((((((~hollywood(X6)|~city(X6))|~event(X7))|~chevy(X8))|~car(X8))|~white(X8))|~dirty(X8))|~old(X8))|~street(X9))|~way(X9))|~lonely(X9))|~barrel(X7,X8))|~down(X7,X9))))|~in(X7,X6)))))|((?[X10]:(?[X11]:((?[X12]:(?[X13]:((((((((((((hollywood(X10)&city(X10))&event(X11))&chevy(X12))&car(X12))&white(X12))&dirty(X12))&old(X12))&street(X13))&way(X13))&lonely(X13))&barrel(X11,X12))&down(X11,X13))))&in(X11,X10))))&(![X14]:(![X15]:((![X16]:((![X17]:(((((((((((~hollywood(X14)|~city(X14))|~event(X15))|~street(X16))|~way(X16))|~lonely(X16))|~chevy(X17))|~car(X17))|~white(X17))|~dirty(X17))|~old(X17))|~barrel(X15,X17)))|~down(X15,X16)))|~in(X15,X14)))))),inference(variable_rename,[status(thm)],[c2])).
% 3.90/4.11  fof(c5,negated_conjecture,(![X6]:(![X7]:(![X8]:(![X9]:(![X14]:(![X15]:(![X16]:(![X17]:(((((((((((((((hollywood(skolem0001)&city(skolem0001))&event(skolem0002))&street(skolem0003))&way(skolem0003))&lonely(skolem0003))&chevy(skolem0004))&car(skolem0004))&white(skolem0004))&dirty(skolem0004))&old(skolem0004))&barrel(skolem0002,skolem0004))&down(skolem0002,skolem0003))&in(skolem0002,skolem0001))&(((((((((((((~hollywood(X6)|~city(X6))|~event(X7))|~chevy(X8))|~car(X8))|~white(X8))|~dirty(X8))|~old(X8))|~street(X9))|~way(X9))|~lonely(X9))|~barrel(X7,X8))|~down(X7,X9))|~in(X7,X6)))|((((((((((((((hollywood(skolem0005)&city(skolem0005))&event(skolem0006))&chevy(skolem0007))&car(skolem0007))&white(skolem0007))&dirty(skolem0007))&old(skolem0007))&street(skolem0008))&way(skolem0008))&lonely(skolem0008))&barrel(skolem0006,skolem0007))&down(skolem0006,skolem0008))&in(skolem0006,skolem0005))&(((((((((((((~hollywood(X14)|~city(X14))|~event(X15))|~street(X16))|~way(X16))|~lonely(X16))|~chevy(X17))|~car(X17))|~white(X17))|~dirty(X17))|~old(X17))|~barrel(X15,X17))|~down(X15,X16))|~in(X15,X14)))))))))))),inference(shift_quantors,[status(thm)],[fof(c4,negated_conjecture,(((((((((((((((hollywood(skolem0001)&city(skolem0001))&event(skolem0002))&street(skolem0003))&way(skolem0003))&lonely(skolem0003))&chevy(skolem0004))&car(skolem0004))&white(skolem0004))&dirty(skolem0004))&old(skolem0004))&barrel(skolem0002,skolem0004))&down(skolem0002,skolem0003))&in(skolem0002,skolem0001))&(![X6]:(![X7]:((![X8]:(![X9]:((((((((((((~hollywood(X6)|~city(X6))|~event(X7))|~chevy(X8))|~car(X8))|~white(X8))|~dirty(X8))|~old(X8))|~street(X9))|~way(X9))|~lonely(X9))|~barrel(X7,X8))|~down(X7,X9))))|~in(X7,X6)))))|((((((((((((((hollywood(skolem0005)&city(skolem0005))&event(skolem0006))&chevy(skolem0007))&car(skolem0007))&white(skolem0007))&dirty(skolem0007))&old(skolem0007))&street(skolem0008))&way(skolem0008))&lonely(skolem0008))&barrel(skolem0006,skolem0007))&down(skolem0006,skolem0008))&in(skolem0006,skolem0005))&(![X14]:(![X15]:((![X16]:((![X17]:(((((((((((~hollywood(X14)|~city(X14))|~event(X15))|~street(X16))|~way(X16))|~lonely(X16))|~chevy(X17))|~car(X17))|~white(X17))|~dirty(X17))|~old(X17))|~barrel(X15,X17)))|~down(X15,X16)))|~in(X15,X14)))))),inference(skolemize,[status(esa)],[c3])).])).
% 3.90/4.11  fof(c6,negated_conjecture,(![X6]:(![X7]:(![X8]:(![X9]:(![X14]:(![X15]:(![X16]:(![X17]:(((((((((((((((((((((((((((((hollywood(skolem0001)|hollywood(skolem0005))&(hollywood(skolem0001)|city(skolem0005)))&(hollywood(skolem0001)|event(skolem0006)))&(hollywood(skolem0001)|chevy(skolem0007)))&(hollywood(skolem0001)|car(skolem0007)))&(hollywood(skolem0001)|white(skolem0007)))&(hollywood(skolem0001)|dirty(skolem0007)))&(hollywood(skolem0001)|old(skolem0007)))&(hollywood(skolem0001)|street(skolem0008)))&(hollywood(skolem0001)|way(skolem0008)))&(hollywood(skolem0001)|lonely(skolem0008)))&(hollywood(skolem0001)|barrel(skolem0006,skolem0007)))&(hollywood(skolem0001)|down(skolem0006,skolem0008)))&(hollywood(skolem0001)|in(skolem0006,skolem0005)))&(hollywood(skolem0001)|(((((((((((((~hollywood(X14)|~city(X14))|~event(X15))|~street(X16))|~way(X16))|~lonely(X16))|~chevy(X17))|~car(X17))|~white(X17))|~dirty(X17))|~old(X17))|~barrel(X15,X17))|~down(X15,X16))|~in(X15,X14))))&(((((((((((((((city(skolem0001)|hollywood(skolem0005))&(city(skolem0001)|city(skolem0005)))&(city(skolem0001)|event(skolem0006)))&(city(skolem0001)|chevy(skolem0007)))&(city(skolem0001)|car(skolem0007)))&(city(skolem0001)|white(skolem0007)))&(city(skolem0001)|dirty(skolem0007)))&(city(skolem0001)|old(skolem0007)))&(city(skolem0001)|street(skolem0008)))&(city(skolem0001)|way(skolem0008)))&(city(skolem0001)|lonely(skolem0008)))&(city(skolem0001)|barrel(skolem0006,skolem0007)))&(city(skolem0001)|down(skolem0006,skolem0008)))&(city(skolem0001)|in(skolem0006,skolem0005)))&(city(skolem0001)|(((((((((((((~hollywood(X14)|~city(X14))|~event(X15))|~street(X16))|~way(X16))|~lonely(X16))|~chevy(X17))|~car(X17))|~white(X17))|~dirty(X17))|~old(X17))|~barrel(X15,X17))|~down(X15,X16))|~in(X15,X14)))))&(((((((((((((((event(skolem0002)|hollywood(skolem0005))&(event(skolem0002)|city(skolem0005)))&(event(skolem0002)|event(skolem0006)))&(event(skolem0002)|chevy(skolem0007)))&(event(skolem0002)|car(skolem0007)))&(event(skolem0002)|white(skolem0007)))&(event(skolem0002)|dirty(skolem0007)))&(event(skolem0002)|old(skolem0007)))&(event(skolem0002)|street(skolem0008)))&(event(skolem0002)|way(skolem0008)))&(event(skolem0002)|lonely(skolem0008)))&(event(skolem0002)|barrel(skolem0006,skolem0007)))&(event(skolem0002)|down(skolem0006,skolem0008)))&(event(skolem0002)|in(skolem0006,skolem0005)))&(event(skolem0002)|(((((((((((((~hollywood(X14)|~city(X14))|~event(X15))|~street(X16))|~way(X16))|~lonely(X16))|~chevy(X17))|~car(X17))|~white(X17))|~dirty(X17))|~old(X17))|~barrel(X15,X17))|~down(X15,X16))|~in(X15,X14)))))&(((((((((((((((street(skolem0003)|hollywood(skolem0005))&(street(skolem0003)|city(skolem0005)))&(street(skolem0003)|event(skolem0006)))&(street(skolem0003)|chevy(skolem0007)))&(street(skolem0003)|car(skolem0007)))&(street(skolem0003)|white(skolem0007)))&(street(skolem0003)|dirty(skolem0007)))&(street(skolem0003)|old(skolem0007)))&(street(skolem0003)|street(skolem0008)))&(street(skolem0003)|way(skolem0008)))&(street(skolem0003)|lonely(skolem0008)))&(street(skolem0003)|barrel(skolem0006,skolem0007)))&(street(skolem0003)|down(skolem0006,skolem0008)))&(street(skolem0003)|in(skolem0006,skolem0005)))&(street(skolem0003)|(((((((((((((~hollywood(X14)|~city(X14))|~event(X15))|~street(X16))|~way(X16))|~lonely(X16))|~chevy(X17))|~car(X17))|~white(X17))|~dirty(X17))|~old(X17))|~barrel(X15,X17))|~down(X15,X16))|~in(X15,X14)))))&(((((((((((((((way(skolem0003)|hollywood(skolem0005))&(way(skolem0003)|city(skolem0005)))&(way(skolem0003)|event(skolem0006)))&(way(skolem0003)|chevy(skolem0007)))&(way(skolem0003)|car(skolem0007)))&(way(skolem0003)|white(skolem0007)))&(way(skolem0003)|dirty(skolem0007)))&(way(skolem0003)|old(skolem0007)))&(way(skolem0003)|street(skolem0008)))&(way(skolem0003)|way(skolem0008)))&(way(skolem0003)|lonely(skolem0008)))&(way(skolem0003)|barrel(skolem0006,skolem0007)))&(way(skolem0003)|down(skolem0006,skolem0008)))&(way(skolem0003)|in(skolem0006,skolem0005)))&(way(skolem0003)|(((((((((((((~hollywood(X14)|~city(X14))|~event(X15))|~street(X16))|~way(X16))|~lonely(X16))|~chevy(X17))|~car(X17))|~white(X17))|~dirty(X17))|~old(X17))|~barrel(X15,X17))|~down(X15,X16))|~in(X15,X14)))))&(((((((((((((((lonely(skolem0003)|hollywood(skolem0005))&(lonely(skolem0003)|city(skolem0005)))&(lonely(skolem0003)|event(skolem0006)))&(lonely(skolem0003)|chevy(skolem0007)))&(lonely(skolem0003)|car(skolem0007)))&(lonely(skolem0003)|white(skolem0007)))&(lonely(skolem0003)|dirty(skolem0007)))&(lonely(skolem0003)|old(skolem0007)))&(lonely(skolem0003)|street(skolem0008)))&(lonely(skolem0003)|way(skolem0008)))&(lonely(skolem0003)|lonely(skolem0008)))&(lonely(skolem0003)|barrel(skolem0006,skolem0007)))&(lonely(skolem0003)|down(skolem0006,skolem0008)))&(lonely(skolem0003)|in(skolem0006,skolem0005)))&(lonely(skolem0003)|(((((((((((((~hollywood(X14)|~city(X14))|~event(X15))|~street(X16))|~way(X16))|~lonely(X16))|~chevy(X17))|~car(X17))|~white(X17))|~dirty(X17))|~old(X17))|~barrel(X15,X17))|~down(X15,X16))|~in(X15,X14)))))&(((((((((((((((chevy(skolem0004)|hollywood(skolem0005))&(chevy(skolem0004)|city(skolem0005)))&(chevy(skolem0004)|event(skolem0006)))&(chevy(skolem0004)|chevy(skolem0007)))&(chevy(skolem0004)|car(skolem0007)))&(chevy(skolem0004)|white(skolem0007)))&(chevy(skolem0004)|dirty(skolem0007)))&(chevy(skolem0004)|old(skolem0007)))&(chevy(skolem0004)|street(skolem0008)))&(chevy(skolem0004)|way(skolem0008)))&(chevy(skolem0004)|lonely(skolem0008)))&(chevy(skolem0004)|barrel(skolem0006,skolem0007)))&(chevy(skolem0004)|down(skolem0006,skolem0008)))&(chevy(skolem0004)|in(skolem0006,skolem0005)))&(chevy(skolem0004)|(((((((((((((~hollywood(X14)|~city(X14))|~event(X15))|~street(X16))|~way(X16))|~lonely(X16))|~chevy(X17))|~car(X17))|~white(X17))|~dirty(X17))|~old(X17))|~barrel(X15,X17))|~down(X15,X16))|~in(X15,X14)))))&(((((((((((((((car(skolem0004)|hollywood(skolem0005))&(car(skolem0004)|city(skolem0005)))&(car(skolem0004)|event(skolem0006)))&(car(skolem0004)|chevy(skolem0007)))&(car(skolem0004)|car(skolem0007)))&(car(skolem0004)|white(skolem0007)))&(car(skolem0004)|dirty(skolem0007)))&(car(skolem0004)|old(skolem0007)))&(car(skolem0004)|street(skolem0008)))&(car(skolem0004)|way(skolem0008)))&(car(skolem0004)|lonely(skolem0008)))&(car(skolem0004)|barrel(skolem0006,skolem0007)))&(car(skolem0004)|down(skolem0006,skolem0008)))&(car(skolem0004)|in(skolem0006,skolem0005)))&(car(skolem0004)|(((((((((((((~hollywood(X14)|~city(X14))|~event(X15))|~street(X16))|~way(X16))|~lonely(X16))|~chevy(X17))|~car(X17))|~white(X17))|~dirty(X17))|~old(X17))|~barrel(X15,X17))|~down(X15,X16))|~in(X15,X14)))))&(((((((((((((((white(skolem0004)|hollywood(skolem0005))&(white(skolem0004)|city(skolem0005)))&(white(skolem0004)|event(skolem0006)))&(white(skolem0004)|chevy(skolem0007)))&(white(skolem0004)|car(skolem0007)))&(white(skolem0004)|white(skolem0007)))&(white(skolem0004)|dirty(skolem0007)))&(white(skolem0004)|old(skolem0007)))&(white(skolem0004)|street(skolem0008)))&(white(skolem0004)|way(skolem0008)))&(white(skolem0004)|lonely(skolem0008)))&(white(skolem0004)|barrel(skolem0006,skolem0007)))&(white(skolem0004)|down(skolem0006,skolem0008)))&(white(skolem0004)|in(skolem0006,skolem0005)))&(white(skolem0004)|(((((((((((((~hollywood(X14)|~city(X14))|~event(X15))|~street(X16))|~way(X16))|~lonely(X16))|~chevy(X17))|~car(X17))|~white(X17))|~dirty(X17))|~old(X17))|~barrel(X15,X17))|~down(X15,X16))|~in(X15,X14)))))&(((((((((((((((dirty(skolem0004)|hollywood(skolem0005))&(dirty(skolem0004)|city(skolem0005)))&(dirty(skolem0004)|event(skolem0006)))&(dirty(skolem0004)|chevy(skolem0007)))&(dirty(skolem0004)|car(skolem0007)))&(dirty(skolem0004)|white(skolem0007)))&(dirty(skolem0004)|dirty(skolem0007)))&(dirty(skolem0004)|old(skolem0007)))&(dirty(skolem0004)|street(skolem0008)))&(dirty(skolem0004)|way(skolem0008)))&(dirty(skolem0004)|lonely(skolem0008)))&(dirty(skolem0004)|barrel(skolem0006,skolem0007)))&(dirty(skolem0004)|down(skolem0006,skolem0008)))&(dirty(skolem0004)|in(skolem0006,skolem0005)))&(dirty(skolem0004)|(((((((((((((~hollywood(X14)|~city(X14))|~event(X15))|~street(X16))|~way(X16))|~lonely(X16))|~chevy(X17))|~car(X17))|~white(X17))|~dirty(X17))|~old(X17))|~barrel(X15,X17))|~down(X15,X16))|~in(X15,X14)))))&(((((((((((((((old(skolem0004)|hollywood(skolem0005))&(old(skolem0004)|city(skolem0005)))&(old(skolem0004)|event(skolem0006)))&(old(skolem0004)|chevy(skolem0007)))&(old(skolem0004)|car(skolem0007)))&(old(skolem0004)|white(skolem0007)))&(old(skolem0004)|dirty(skolem0007)))&(old(skolem0004)|old(skolem0007)))&(old(skolem0004)|street(skolem0008)))&(old(skolem0004)|way(skolem0008)))&(old(skolem0004)|lonely(skolem0008)))&(old(skolem0004)|barrel(skolem0006,skolem0007)))&(old(skolem0004)|down(skolem0006,skolem0008)))&(old(skolem0004)|in(skolem0006,skolem0005)))&(old(skolem0004)|(((((((((((((~hollywood(X14)|~city(X14))|~event(X15))|~street(X16))|~way(X16))|~lonely(X16))|~chevy(X17))|~car(X17))|~white(X17))|~dirty(X17))|~old(X17))|~barrel(X15,X17))|~down(X15,X16))|~in(X15,X14)))))&(((((((((((((((barrel(skolem0002,skolem0004)|hollywood(skolem0005))&(barrel(skolem0002,skolem0004)|city(skolem0005)))&(barrel(skolem0002,skolem0004)|event(skolem0006)))&(barrel(skolem0002,skolem0004)|chevy(skolem0007)))&(barrel(skolem0002,skolem0004)|car(skolem0007)))&(barrel(skolem0002,skolem0004)|white(skolem0007)))&(barrel(skolem0002,skolem0004)|dirty(skolem0007)))&(barrel(skolem0002,skolem0004)|old(skolem0007)))&(barrel(skolem0002,skolem0004)|street(skolem0008)))&(barrel(skolem0002,skolem0004)|way(skolem0008)))&(barrel(skolem0002,skolem0004)|lonely(skolem0008)))&(barrel(skolem0002,skolem0004)|barrel(skolem0006,skolem0007)))&(barrel(skolem0002,skolem0004)|down(skolem0006,skolem0008)))&(barrel(skolem0002,skolem0004)|in(skolem0006,skolem0005)))&(barrel(skolem0002,skolem0004)|(((((((((((((~hollywood(X14)|~city(X14))|~event(X15))|~street(X16))|~way(X16))|~lonely(X16))|~chevy(X17))|~car(X17))|~white(X17))|~dirty(X17))|~old(X17))|~barrel(X15,X17))|~down(X15,X16))|~in(X15,X14)))))&(((((((((((((((down(skolem0002,skolem0003)|hollywood(skolem0005))&(down(skolem0002,skolem0003)|city(skolem0005)))&(down(skolem0002,skolem0003)|event(skolem0006)))&(down(skolem0002,skolem0003)|chevy(skolem0007)))&(down(skolem0002,skolem0003)|car(skolem0007)))&(down(skolem0002,skolem0003)|white(skolem0007)))&(down(skolem0002,skolem0003)|dirty(skolem0007)))&(down(skolem0002,skolem0003)|old(skolem0007)))&(down(skolem0002,skolem0003)|street(skolem0008)))&(down(skolem0002,skolem0003)|way(skolem0008)))&(down(skolem0002,skolem0003)|lonely(skolem0008)))&(down(skolem0002,skolem0003)|barrel(skolem0006,skolem0007)))&(down(skolem0002,skolem0003)|down(skolem0006,skolem0008)))&(down(skolem0002,skolem0003)|in(skolem0006,skolem0005)))&(down(skolem0002,skolem0003)|(((((((((((((~hollywood(X14)|~city(X14))|~event(X15))|~street(X16))|~way(X16))|~lonely(X16))|~chevy(X17))|~car(X17))|~white(X17))|~dirty(X17))|~old(X17))|~barrel(X15,X17))|~down(X15,X16))|~in(X15,X14)))))&(((((((((((((((in(skolem0002,skolem0001)|hollywood(skolem0005))&(in(skolem0002,skolem0001)|city(skolem0005)))&(in(skolem0002,skolem0001)|event(skolem0006)))&(in(skolem0002,skolem0001)|chevy(skolem0007)))&(in(skolem0002,skolem0001)|car(skolem0007)))&(in(skolem0002,skolem0001)|white(skolem0007)))&(in(skolem0002,skolem0001)|dirty(skolem0007)))&(in(skolem0002,skolem0001)|old(skolem0007)))&(in(skolem0002,skolem0001)|street(skolem0008)))&(in(skolem0002,skolem0001)|way(skolem0008)))&(in(skolem0002,skolem0001)|lonely(skolem0008)))&(in(skolem0002,skolem0001)|barrel(skolem0006,skolem0007)))&(in(skolem0002,skolem0001)|down(skolem0006,skolem0008)))&(in(skolem0002,skolem0001)|in(skolem0006,skolem0005)))&(in(skolem0002,skolem0001)|(((((((((((((~hollywood(X14)|~city(X14))|~event(X15))|~street(X16))|~way(X16))|~lonely(X16))|~chevy(X17))|~car(X17))|~white(X17))|~dirty(X17))|~old(X17))|~barrel(X15,X17))|~down(X15,X16))|~in(X15,X14)))))&((((((((((((((((((((((((((((~hollywood(X6)|~city(X6))|~event(X7))|~chevy(X8))|~car(X8))|~white(X8))|~dirty(X8))|~old(X8))|~street(X9))|~way(X9))|~lonely(X9))|~barrel(X7,X8))|~down(X7,X9))|~in(X7,X6))|hollywood(skolem0005))&((((((((((((((~hollywood(X6)|~city(X6))|~event(X7))|~chevy(X8))|~car(X8))|~white(X8))|~dirty(X8))|~old(X8))|~street(X9))|~way(X9))|~lonely(X9))|~barrel(X7,X8))|~down(X7,X9))|~in(X7,X6))|city(skolem0005)))&((((((((((((((~hollywood(X6)|~city(X6))|~event(X7))|~chevy(X8))|~car(X8))|~white(X8))|~dirty(X8))|~old(X8))|~street(X9))|~way(X9))|~lonely(X9))|~barrel(X7,X8))|~down(X7,X9))|~in(X7,X6))|event(skolem0006)))&((((((((((((((~hollywood(X6)|~city(X6))|~event(X7))|~chevy(X8))|~car(X8))|~white(X8))|~dirty(X8))|~old(X8))|~street(X9))|~way(X9))|~lonely(X9))|~barrel(X7,X8))|~down(X7,X9))|~in(X7,X6))|chevy(skolem0007)))&((((((((((((((~hollywood(X6)|~city(X6))|~event(X7))|~chevy(X8))|~car(X8))|~white(X8))|~dirty(X8))|~old(X8))|~street(X9))|~way(X9))|~lonely(X9))|~barrel(X7,X8))|~down(X7,X9))|~in(X7,X6))|car(skolem0007)))&((((((((((((((~hollywood(X6)|~city(X6))|~event(X7))|~chevy(X8))|~car(X8))|~white(X8))|~dirty(X8))|~old(X8))|~street(X9))|~way(X9))|~lonely(X9))|~barrel(X7,X8))|~down(X7,X9))|~in(X7,X6))|white(skolem0007)))&((((((((((((((~hollywood(X6)|~city(X6))|~event(X7))|~chevy(X8))|~car(X8))|~white(X8))|~dirty(X8))|~old(X8))|~street(X9))|~way(X9))|~lonely(X9))|~barrel(X7,X8))|~down(X7,X9))|~in(X7,X6))|dirty(skolem0007)))&((((((((((((((~hollywood(X6)|~city(X6))|~event(X7))|~chevy(X8))|~car(X8))|~white(X8))|~dirty(X8))|~old(X8))|~street(X9))|~way(X9))|~lonely(X9))|~barrel(X7,X8))|~down(X7,X9))|~in(X7,X6))|old(skolem0007)))&((((((((((((((~hollywood(X6)|~city(X6))|~event(X7))|~chevy(X8))|~car(X8))|~white(X8))|~dirty(X8))|~old(X8))|~street(X9))|~way(X9))|~lonely(X9))|~barrel(X7,X8))|~down(X7,X9))|~in(X7,X6))|street(skolem0008)))&((((((((((((((~hollywood(X6)|~city(X6))|~event(X7))|~chevy(X8))|~car(X8))|~white(X8))|~dirty(X8))|~old(X8))|~street(X9))|~way(X9))|~lonely(X9))|~barrel(X7,X8))|~down(X7,X9))|~in(X7,X6))|way(skolem0008)))&((((((((((((((~hollywood(X6)|~city(X6))|~event(X7))|~chevy(X8))|~car(X8))|~white(X8))|~dirty(X8))|~old(X8))|~street(X9))|~way(X9))|~lonely(X9))|~barrel(X7,X8))|~down(X7,X9))|~in(X7,X6))|lonely(skolem0008)))&((((((((((((((~hollywood(X6)|~city(X6))|~event(X7))|~chevy(X8))|~car(X8))|~white(X8))|~dirty(X8))|~old(X8))|~street(X9))|~way(X9))|~lonely(X9))|~barrel(X7,X8))|~down(X7,X9))|~in(X7,X6))|barrel(skolem0006,skolem0007)))&((((((((((((((~hollywood(X6)|~city(X6))|~event(X7))|~chevy(X8))|~car(X8))|~white(X8))|~dirty(X8))|~old(X8))|~street(X9))|~way(X9))|~lonely(X9))|~barrel(X7,X8))|~down(X7,X9))|~in(X7,X6))|down(skolem0006,skolem0008)))&((((((((((((((~hollywood(X6)|~city(X6))|~event(X7))|~chevy(X8))|~car(X8))|~white(X8))|~dirty(X8))|~old(X8))|~street(X9))|~way(X9))|~lonely(X9))|~barrel(X7,X8))|~down(X7,X9))|~in(X7,X6))|in(skolem0006,skolem0005)))&((((((((((((((~hollywood(X6)|~city(X6))|~event(X7))|~chevy(X8))|~car(X8))|~white(X8))|~dirty(X8))|~old(X8))|~street(X9))|~way(X9))|~lonely(X9))|~barrel(X7,X8))|~down(X7,X9))|~in(X7,X6))|(((((((((((((~hollywood(X14)|~city(X14))|~event(X15))|~street(X16))|~way(X16))|~lonely(X16))|~chevy(X17))|~car(X17))|~white(X17))|~dirty(X17))|~old(X17))|~barrel(X15,X17))|~down(X15,X16))|~in(X15,X14))))))))))))),inference(distribute,[status(thm)],[c5])).
% 3.90/4.11  cnf(c7,negated_conjecture,hollywood(skolem0001)|hollywood(skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.11  cnf(c8,negated_conjecture,hollywood(skolem0001)|city(skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.11  cnf(c9,negated_conjecture,hollywood(skolem0001)|event(skolem0006),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.11  cnf(c15,negated_conjecture,hollywood(skolem0001)|street(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.11  cnf(c16,negated_conjecture,hollywood(skolem0001)|way(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.11  cnf(c17,negated_conjecture,hollywood(skolem0001)|lonely(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.11  cnf(c10,negated_conjecture,hollywood(skolem0001)|chevy(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.11  cnf(c11,negated_conjecture,hollywood(skolem0001)|car(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.11  cnf(c12,negated_conjecture,hollywood(skolem0001)|white(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.11  cnf(c13,negated_conjecture,hollywood(skolem0001)|dirty(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.11  cnf(c14,negated_conjecture,hollywood(skolem0001)|old(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.11  cnf(c18,negated_conjecture,hollywood(skolem0001)|barrel(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.11  cnf(c19,negated_conjecture,hollywood(skolem0001)|down(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.11  cnf(c20,negated_conjecture,hollywood(skolem0001)|in(skolem0006,skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.11  cnf(c21,negated_conjecture,hollywood(skolem0001)|~hollywood(X18)|~city(X18)|~event(X21)|~street(X20)|~way(X20)|~lonely(X20)|~chevy(X19)|~car(X19)|~white(X19)|~dirty(X19)|~old(X19)|~barrel(X21,X19)|~down(X21,X20)|~in(X21,X18),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.11  cnf(c232,plain,hollywood(skolem0001)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(X123)|~way(X123)|~lonely(X123)|~chevy(X122)|~car(X122)|~white(X122)|~dirty(X122)|~old(X122)|~barrel(skolem0006,X122)|~down(skolem0006,X123),inference(resolution,[status(thm)],[c21, c20])).
% 3.90/4.11  cnf(c966,plain,hollywood(skolem0001)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(X124)|~car(X124)|~white(X124)|~dirty(X124)|~old(X124)|~barrel(skolem0006,X124),inference(resolution,[status(thm)],[c232, c19])).
% 3.90/4.11  cnf(c975,plain,hollywood(skolem0001)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007)|~dirty(skolem0007)|~old(skolem0007),inference(resolution,[status(thm)],[c966, c18])).
% 3.90/4.11  cnf(c999,plain,hollywood(skolem0001)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007)|~dirty(skolem0007),inference(resolution,[status(thm)],[c975, c14])).
% 3.90/4.11  cnf(c1006,plain,hollywood(skolem0001)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007),inference(resolution,[status(thm)],[c999, c13])).
% 3.90/4.11  cnf(c1021,plain,hollywood(skolem0001)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007),inference(resolution,[status(thm)],[c1006, c12])).
% 3.90/4.11  cnf(c1061,plain,hollywood(skolem0001)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007),inference(resolution,[status(thm)],[c1021, c11])).
% 3.90/4.11  cnf(c1080,plain,hollywood(skolem0001)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008),inference(resolution,[status(thm)],[c1061, c10])).
% 3.90/4.11  cnf(c1092,plain,hollywood(skolem0001)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008),inference(resolution,[status(thm)],[c1080, c17])).
% 3.90/4.11  cnf(c1107,plain,hollywood(skolem0001)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008),inference(resolution,[status(thm)],[c1092, c16])).
% 3.90/4.11  cnf(c1123,plain,hollywood(skolem0001)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006),inference(resolution,[status(thm)],[c1107, c15])).
% 3.90/4.11  cnf(c1156,plain,hollywood(skolem0001)|~hollywood(skolem0005)|~city(skolem0005),inference(resolution,[status(thm)],[c1123, c9])).
% 3.90/4.11  cnf(c1183,plain,hollywood(skolem0001)|~hollywood(skolem0005),inference(resolution,[status(thm)],[c1156, c8])).
% 3.90/4.11  cnf(c1190,plain,hollywood(skolem0001),inference(resolution,[status(thm)],[c1183, c7])).
% 3.90/4.11  cnf(c22,negated_conjecture,city(skolem0001)|hollywood(skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.11  cnf(c23,negated_conjecture,city(skolem0001)|city(skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.11  cnf(c24,negated_conjecture,city(skolem0001)|event(skolem0006),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.11  cnf(c30,negated_conjecture,city(skolem0001)|street(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.11  cnf(c31,negated_conjecture,city(skolem0001)|way(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.11  cnf(c32,negated_conjecture,city(skolem0001)|lonely(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.11  cnf(c25,negated_conjecture,city(skolem0001)|chevy(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.11  cnf(c26,negated_conjecture,city(skolem0001)|car(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.11  cnf(c27,negated_conjecture,city(skolem0001)|white(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.11  cnf(c28,negated_conjecture,city(skolem0001)|dirty(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.11  cnf(c29,negated_conjecture,city(skolem0001)|old(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.11  cnf(c33,negated_conjecture,city(skolem0001)|barrel(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.11  cnf(c34,negated_conjecture,city(skolem0001)|down(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.11  cnf(c35,negated_conjecture,city(skolem0001)|in(skolem0006,skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.11  cnf(c36,negated_conjecture,city(skolem0001)|~hollywood(X22)|~city(X22)|~event(X25)|~street(X24)|~way(X24)|~lonely(X24)|~chevy(X23)|~car(X23)|~white(X23)|~dirty(X23)|~old(X23)|~barrel(X25,X23)|~down(X25,X24)|~in(X25,X22),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.11  cnf(c234,plain,city(skolem0001)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(X144)|~way(X144)|~lonely(X144)|~chevy(X143)|~car(X143)|~white(X143)|~dirty(X143)|~old(X143)|~barrel(skolem0006,X143)|~down(skolem0006,X144),inference(resolution,[status(thm)],[c36, c35])).
% 3.90/4.11  cnf(c1227,plain,city(skolem0001)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(X195)|~car(X195)|~white(X195)|~dirty(X195)|~old(X195)|~barrel(skolem0006,X195),inference(resolution,[status(thm)],[c234, c34])).
% 3.90/4.11  cnf(c1285,plain,city(skolem0001)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007)|~dirty(skolem0007)|~old(skolem0007),inference(resolution,[status(thm)],[c1227, c33])).
% 3.90/4.11  cnf(c1331,plain,city(skolem0001)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007)|~dirty(skolem0007),inference(resolution,[status(thm)],[c1285, c29])).
% 3.90/4.11  cnf(c1348,plain,city(skolem0001)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007),inference(resolution,[status(thm)],[c1331, c28])).
% 3.90/4.11  cnf(c1362,plain,city(skolem0001)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007),inference(resolution,[status(thm)],[c1348, c27])).
% 3.90/4.12  cnf(c1369,plain,city(skolem0001)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007),inference(resolution,[status(thm)],[c1362, c26])).
% 3.90/4.12  cnf(c1394,plain,city(skolem0001)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008),inference(resolution,[status(thm)],[c1369, c25])).
% 3.90/4.12  cnf(c1398,plain,city(skolem0001)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008),inference(resolution,[status(thm)],[c1394, c32])).
% 3.90/4.12  cnf(c1418,plain,city(skolem0001)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008),inference(resolution,[status(thm)],[c1398, c31])).
% 3.90/4.12  cnf(c1430,plain,city(skolem0001)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006),inference(resolution,[status(thm)],[c1418, c30])).
% 3.90/4.12  cnf(c1437,plain,city(skolem0001)|~hollywood(skolem0005)|~city(skolem0005),inference(resolution,[status(thm)],[c1430, c24])).
% 3.90/4.12  cnf(c1456,plain,city(skolem0001)|~hollywood(skolem0005),inference(resolution,[status(thm)],[c1437, c23])).
% 3.90/4.12  cnf(c1471,plain,city(skolem0001),inference(resolution,[status(thm)],[c1456, c22])).
% 3.90/4.12  cnf(c37,negated_conjecture,event(skolem0002)|hollywood(skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c38,negated_conjecture,event(skolem0002)|city(skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c39,negated_conjecture,event(skolem0002)|event(skolem0006),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c45,negated_conjecture,event(skolem0002)|street(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c46,negated_conjecture,event(skolem0002)|way(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c47,negated_conjecture,event(skolem0002)|lonely(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c40,negated_conjecture,event(skolem0002)|chevy(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c41,negated_conjecture,event(skolem0002)|car(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c42,negated_conjecture,event(skolem0002)|white(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c43,negated_conjecture,event(skolem0002)|dirty(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c44,negated_conjecture,event(skolem0002)|old(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c48,negated_conjecture,event(skolem0002)|barrel(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c49,negated_conjecture,event(skolem0002)|down(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c50,negated_conjecture,event(skolem0002)|in(skolem0006,skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c51,negated_conjecture,event(skolem0002)|~hollywood(X26)|~city(X26)|~event(X29)|~street(X28)|~way(X28)|~lonely(X28)|~chevy(X27)|~car(X27)|~white(X27)|~dirty(X27)|~old(X27)|~barrel(X29,X27)|~down(X29,X28)|~in(X29,X26),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c239,plain,event(skolem0002)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(X153)|~way(X153)|~lonely(X153)|~chevy(X154)|~car(X154)|~white(X154)|~dirty(X154)|~old(X154)|~barrel(skolem0006,X154)|~down(skolem0006,X153),inference(resolution,[status(thm)],[c51, c50])).
% 3.90/4.12  cnf(c1249,plain,event(skolem0002)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(X198)|~car(X198)|~white(X198)|~dirty(X198)|~old(X198)|~barrel(skolem0006,X198),inference(resolution,[status(thm)],[c239, c49])).
% 3.90/4.12  cnf(c1294,plain,event(skolem0002)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007)|~dirty(skolem0007)|~old(skolem0007),inference(resolution,[status(thm)],[c1249, c48])).
% 3.90/4.12  cnf(c1507,plain,event(skolem0002)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007)|~dirty(skolem0007),inference(resolution,[status(thm)],[c1294, c44])).
% 3.90/4.12  cnf(c1512,plain,event(skolem0002)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007),inference(resolution,[status(thm)],[c1507, c43])).
% 3.90/4.12  cnf(c1525,plain,event(skolem0002)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007),inference(resolution,[status(thm)],[c1512, c42])).
% 3.90/4.12  cnf(c1541,plain,event(skolem0002)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007),inference(resolution,[status(thm)],[c1525, c41])).
% 3.90/4.12  cnf(c1552,plain,event(skolem0002)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008),inference(resolution,[status(thm)],[c1541, c40])).
% 3.90/4.12  cnf(c1568,plain,event(skolem0002)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008),inference(resolution,[status(thm)],[c1552, c47])).
% 3.90/4.12  cnf(c1574,plain,event(skolem0002)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008),inference(resolution,[status(thm)],[c1568, c46])).
% 3.90/4.12  cnf(c1588,plain,event(skolem0002)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006),inference(resolution,[status(thm)],[c1574, c45])).
% 3.90/4.12  cnf(c1600,plain,event(skolem0002)|~hollywood(skolem0005)|~city(skolem0005),inference(resolution,[status(thm)],[c1588, c39])).
% 3.90/4.12  cnf(c1605,plain,event(skolem0002)|~hollywood(skolem0005),inference(resolution,[status(thm)],[c1600, c38])).
% 3.90/4.12  cnf(c1640,plain,event(skolem0002),inference(resolution,[status(thm)],[c1605, c37])).
% 3.90/4.12  cnf(c97,negated_conjecture,chevy(skolem0004)|hollywood(skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c98,negated_conjecture,chevy(skolem0004)|city(skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c99,negated_conjecture,chevy(skolem0004)|event(skolem0006),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c105,negated_conjecture,chevy(skolem0004)|street(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c106,negated_conjecture,chevy(skolem0004)|way(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c107,negated_conjecture,chevy(skolem0004)|lonely(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c100,negated_conjecture,chevy(skolem0004)|chevy(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c101,negated_conjecture,chevy(skolem0004)|car(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c102,negated_conjecture,chevy(skolem0004)|white(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c103,negated_conjecture,chevy(skolem0004)|dirty(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c104,negated_conjecture,chevy(skolem0004)|old(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c108,negated_conjecture,chevy(skolem0004)|barrel(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c109,negated_conjecture,chevy(skolem0004)|down(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c110,negated_conjecture,chevy(skolem0004)|in(skolem0006,skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c111,negated_conjecture,chevy(skolem0004)|~hollywood(X42)|~city(X42)|~event(X45)|~street(X44)|~way(X44)|~lonely(X44)|~chevy(X43)|~car(X43)|~white(X43)|~dirty(X43)|~old(X43)|~barrel(X45,X43)|~down(X45,X44)|~in(X45,X42),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c289,plain,chevy(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(X258)|~way(X258)|~lonely(X258)|~chevy(X257)|~car(X257)|~white(X257)|~dirty(X257)|~old(X257)|~barrel(skolem0006,X257)|~down(skolem0006,X258),inference(resolution,[status(thm)],[c111, c110])).
% 3.90/4.12  cnf(c1625,plain,chevy(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(X396)|~car(X396)|~white(X396)|~dirty(X396)|~old(X396)|~barrel(skolem0006,X396),inference(resolution,[status(thm)],[c289, c109])).
% 3.90/4.12  cnf(c1973,plain,chevy(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007)|~dirty(skolem0007)|~old(skolem0007),inference(resolution,[status(thm)],[c1625, c108])).
% 3.90/4.12  cnf(c2119,plain,chevy(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007)|~dirty(skolem0007),inference(resolution,[status(thm)],[c1973, c104])).
% 3.90/4.12  cnf(c2131,plain,chevy(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007),inference(resolution,[status(thm)],[c2119, c103])).
% 3.90/4.12  cnf(c2132,plain,chevy(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007),inference(resolution,[status(thm)],[c2131, c102])).
% 3.90/4.12  cnf(c2140,plain,chevy(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007),inference(resolution,[status(thm)],[c2132, c101])).
% 3.90/4.12  cnf(c2153,plain,chevy(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008),inference(resolution,[status(thm)],[c2140, c100])).
% 3.90/4.12  cnf(c2161,plain,chevy(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008),inference(resolution,[status(thm)],[c2153, c107])).
% 3.90/4.12  cnf(c2165,plain,chevy(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008),inference(resolution,[status(thm)],[c2161, c106])).
% 3.90/4.12  cnf(c2173,plain,chevy(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006),inference(resolution,[status(thm)],[c2165, c105])).
% 3.90/4.12  cnf(c2186,plain,chevy(skolem0004)|~hollywood(skolem0005)|~city(skolem0005),inference(resolution,[status(thm)],[c2173, c99])).
% 3.90/4.12  cnf(c2188,plain,chevy(skolem0004)|~hollywood(skolem0005),inference(resolution,[status(thm)],[c2186, c98])).
% 3.90/4.12  cnf(c2197,plain,chevy(skolem0004),inference(resolution,[status(thm)],[c2188, c97])).
% 3.90/4.12  cnf(c112,negated_conjecture,car(skolem0004)|hollywood(skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c113,negated_conjecture,car(skolem0004)|city(skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c114,negated_conjecture,car(skolem0004)|event(skolem0006),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c120,negated_conjecture,car(skolem0004)|street(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c121,negated_conjecture,car(skolem0004)|way(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c122,negated_conjecture,car(skolem0004)|lonely(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c115,negated_conjecture,car(skolem0004)|chevy(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c116,negated_conjecture,car(skolem0004)|car(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c117,negated_conjecture,car(skolem0004)|white(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c118,negated_conjecture,car(skolem0004)|dirty(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c119,negated_conjecture,car(skolem0004)|old(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c123,negated_conjecture,car(skolem0004)|barrel(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c124,negated_conjecture,car(skolem0004)|down(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c125,negated_conjecture,car(skolem0004)|in(skolem0006,skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c126,negated_conjecture,car(skolem0004)|~hollywood(X46)|~city(X46)|~event(X49)|~street(X48)|~way(X48)|~lonely(X48)|~chevy(X47)|~car(X47)|~white(X47)|~dirty(X47)|~old(X47)|~barrel(X49,X47)|~down(X49,X48)|~in(X49,X46),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c317,plain,car(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(X313)|~way(X313)|~lonely(X313)|~chevy(X314)|~car(X314)|~white(X314)|~dirty(X314)|~old(X314)|~barrel(skolem0006,X314)|~down(skolem0006,X313),inference(resolution,[status(thm)],[c126, c125])).
% 3.90/4.12  cnf(c1785,plain,car(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(X401)|~car(X401)|~white(X401)|~dirty(X401)|~old(X401)|~barrel(skolem0006,X401),inference(resolution,[status(thm)],[c317, c124])).
% 3.90/4.12  cnf(c1984,plain,car(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007)|~dirty(skolem0007)|~old(skolem0007),inference(resolution,[status(thm)],[c1785, c123])).
% 3.90/4.12  cnf(c2208,plain,car(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007)|~dirty(skolem0007),inference(resolution,[status(thm)],[c1984, c119])).
% 3.90/4.12  cnf(c2211,plain,car(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007),inference(resolution,[status(thm)],[c2208, c118])).
% 3.90/4.12  cnf(c2224,plain,car(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007),inference(resolution,[status(thm)],[c2211, c117])).
% 3.90/4.12  cnf(c2225,plain,car(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007),inference(resolution,[status(thm)],[c2224, c116])).
% 3.90/4.12  cnf(c2232,plain,car(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008),inference(resolution,[status(thm)],[c2225, c115])).
% 3.90/4.12  cnf(c2245,plain,car(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008),inference(resolution,[status(thm)],[c2232, c122])).
% 3.90/4.12  cnf(c2251,plain,car(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008),inference(resolution,[status(thm)],[c2245, c121])).
% 3.90/4.12  cnf(c2254,plain,car(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006),inference(resolution,[status(thm)],[c2251, c120])).
% 3.90/4.12  cnf(c2266,plain,car(skolem0004)|~hollywood(skolem0005)|~city(skolem0005),inference(resolution,[status(thm)],[c2254, c114])).
% 3.90/4.12  cnf(c2269,plain,car(skolem0004)|~hollywood(skolem0005),inference(resolution,[status(thm)],[c2266, c113])).
% 3.90/4.12  cnf(c2277,plain,car(skolem0004),inference(resolution,[status(thm)],[c2269, c112])).
% 3.90/4.12  cnf(c127,negated_conjecture,white(skolem0004)|hollywood(skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c128,negated_conjecture,white(skolem0004)|city(skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c129,negated_conjecture,white(skolem0004)|event(skolem0006),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c135,negated_conjecture,white(skolem0004)|street(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c136,negated_conjecture,white(skolem0004)|way(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c137,negated_conjecture,white(skolem0004)|lonely(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c130,negated_conjecture,white(skolem0004)|chevy(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c131,negated_conjecture,white(skolem0004)|car(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c132,negated_conjecture,white(skolem0004)|white(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c133,negated_conjecture,white(skolem0004)|dirty(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c134,negated_conjecture,white(skolem0004)|old(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c138,negated_conjecture,white(skolem0004)|barrel(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c139,negated_conjecture,white(skolem0004)|down(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c140,negated_conjecture,white(skolem0004)|in(skolem0006,skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c141,negated_conjecture,white(skolem0004)|~hollywood(X50)|~city(X50)|~event(X53)|~street(X52)|~way(X52)|~lonely(X52)|~chevy(X51)|~car(X51)|~white(X51)|~dirty(X51)|~old(X51)|~barrel(X53,X51)|~down(X53,X52)|~in(X53,X50),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c330,plain,white(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(X339)|~way(X339)|~lonely(X339)|~chevy(X340)|~car(X340)|~white(X340)|~dirty(X340)|~old(X340)|~barrel(skolem0006,X340)|~down(skolem0006,X339),inference(resolution,[status(thm)],[c141, c140])).
% 3.90/4.12  cnf(c1816,plain,white(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(X402)|~car(X402)|~white(X402)|~dirty(X402)|~old(X402)|~barrel(skolem0006,X402),inference(resolution,[status(thm)],[c330, c139])).
% 3.90/4.12  cnf(c1996,plain,white(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007)|~dirty(skolem0007)|~old(skolem0007),inference(resolution,[status(thm)],[c1816, c138])).
% 3.90/4.12  cnf(c2281,plain,white(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007)|~dirty(skolem0007),inference(resolution,[status(thm)],[c1996, c134])).
% 3.90/4.12  cnf(c2291,plain,white(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007),inference(resolution,[status(thm)],[c2281, c133])).
% 3.90/4.12  cnf(c2298,plain,white(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007),inference(resolution,[status(thm)],[c2291, c132])).
% 3.90/4.12  cnf(c2302,plain,white(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007),inference(resolution,[status(thm)],[c2298, c131])).
% 3.90/4.12  cnf(c2306,plain,white(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008),inference(resolution,[status(thm)],[c2302, c130])).
% 3.90/4.12  cnf(c2314,plain,white(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008),inference(resolution,[status(thm)],[c2306, c137])).
% 3.90/4.12  cnf(c2321,plain,white(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008),inference(resolution,[status(thm)],[c2314, c136])).
% 3.90/4.12  cnf(c2323,plain,white(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006),inference(resolution,[status(thm)],[c2321, c135])).
% 3.90/4.12  cnf(c2333,plain,white(skolem0004)|~hollywood(skolem0005)|~city(skolem0005),inference(resolution,[status(thm)],[c2323, c129])).
% 3.90/4.12  cnf(c2339,plain,white(skolem0004)|~hollywood(skolem0005),inference(resolution,[status(thm)],[c2333, c128])).
% 3.90/4.12  cnf(c2341,plain,white(skolem0004),inference(resolution,[status(thm)],[c2339, c127])).
% 3.90/4.12  cnf(c142,negated_conjecture,dirty(skolem0004)|hollywood(skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c143,negated_conjecture,dirty(skolem0004)|city(skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c144,negated_conjecture,dirty(skolem0004)|event(skolem0006),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c150,negated_conjecture,dirty(skolem0004)|street(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c151,negated_conjecture,dirty(skolem0004)|way(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c152,negated_conjecture,dirty(skolem0004)|lonely(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c145,negated_conjecture,dirty(skolem0004)|chevy(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c146,negated_conjecture,dirty(skolem0004)|car(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c147,negated_conjecture,dirty(skolem0004)|white(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c148,negated_conjecture,dirty(skolem0004)|dirty(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c149,negated_conjecture,dirty(skolem0004)|old(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c153,negated_conjecture,dirty(skolem0004)|barrel(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c154,negated_conjecture,dirty(skolem0004)|down(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c155,negated_conjecture,dirty(skolem0004)|in(skolem0006,skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c156,negated_conjecture,dirty(skolem0004)|~hollywood(X54)|~city(X54)|~event(X57)|~street(X56)|~way(X56)|~lonely(X56)|~chevy(X55)|~car(X55)|~white(X55)|~dirty(X55)|~old(X55)|~barrel(X57,X55)|~down(X57,X56)|~in(X57,X54),inference(split_conjunct,[status(thm)],[c6])).
% 3.90/4.12  cnf(c335,plain,dirty(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(X349)|~way(X349)|~lonely(X349)|~chevy(X350)|~car(X350)|~white(X350)|~dirty(X350)|~old(X350)|~barrel(skolem0006,X350)|~down(skolem0006,X349),inference(resolution,[status(thm)],[c156, c155])).
% 3.90/4.12  cnf(c1900,plain,dirty(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(X407)|~car(X407)|~white(X407)|~dirty(X407)|~old(X407)|~barrel(skolem0006,X407),inference(resolution,[status(thm)],[c335, c154])).
% 3.90/4.12  cnf(c1999,plain,dirty(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007)|~dirty(skolem0007)|~old(skolem0007),inference(resolution,[status(thm)],[c1900, c153])).
% 3.90/4.12  cnf(c2349,plain,dirty(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007)|~dirty(skolem0007),inference(resolution,[status(thm)],[c1999, c149])).
% 3.90/4.12  cnf(c2354,plain,dirty(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007),inference(resolution,[status(thm)],[c2349, c148])).
% 3.90/4.12  cnf(c2359,plain,dirty(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007),inference(resolution,[status(thm)],[c2354, c147])).
% 3.90/4.12  cnf(c2365,plain,dirty(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007),inference(resolution,[status(thm)],[c2359, c146])).
% 3.90/4.12  cnf(c2371,plain,dirty(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008),inference(resolution,[status(thm)],[c2365, c145])).
% 3.90/4.12  cnf(c2372,plain,dirty(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008),inference(resolution,[status(thm)],[c2371, c152])).
% 3.90/4.12  cnf(c2379,plain,dirty(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008),inference(resolution,[status(thm)],[c2372, c151])).
% 3.90/4.12  cnf(c2382,plain,dirty(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006),inference(resolution,[status(thm)],[c2379, c150])).
% 3.90/4.12  cnf(c2391,plain,dirty(skolem0004)|~hollywood(skolem0005)|~city(skolem0005),inference(resolution,[status(thm)],[c2382, c144])).
% 3.90/4.12  cnf(c2393,plain,dirty(skolem0004)|~hollywood(skolem0005),inference(resolution,[status(thm)],[c2391, c143])).
% 3.90/4.12  cnf(c2398,plain,dirty(skolem0004),inference(resolution,[status(thm)],[c2393, c142])).
% 3.96/4.12  cnf(c157,negated_conjecture,old(skolem0004)|hollywood(skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c158,negated_conjecture,old(skolem0004)|city(skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c159,negated_conjecture,old(skolem0004)|event(skolem0006),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c165,negated_conjecture,old(skolem0004)|street(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c166,negated_conjecture,old(skolem0004)|way(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c167,negated_conjecture,old(skolem0004)|lonely(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c160,negated_conjecture,old(skolem0004)|chevy(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c161,negated_conjecture,old(skolem0004)|car(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c162,negated_conjecture,old(skolem0004)|white(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c163,negated_conjecture,old(skolem0004)|dirty(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c164,negated_conjecture,old(skolem0004)|old(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c168,negated_conjecture,old(skolem0004)|barrel(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c169,negated_conjecture,old(skolem0004)|down(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c170,negated_conjecture,old(skolem0004)|in(skolem0006,skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c171,negated_conjecture,old(skolem0004)|~hollywood(X58)|~city(X58)|~event(X61)|~street(X60)|~way(X60)|~lonely(X60)|~chevy(X59)|~car(X59)|~white(X59)|~dirty(X59)|~old(X59)|~barrel(X61,X59)|~down(X61,X60)|~in(X61,X58),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c342,plain,old(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(X363)|~way(X363)|~lonely(X363)|~chevy(X364)|~car(X364)|~white(X364)|~dirty(X364)|~old(X364)|~barrel(skolem0006,X364)|~down(skolem0006,X363),inference(resolution,[status(thm)],[c171, c170])).
% 3.96/4.12  cnf(c1962,plain,old(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(X408)|~car(X408)|~white(X408)|~dirty(X408)|~old(X408)|~barrel(skolem0006,X408),inference(resolution,[status(thm)],[c342, c169])).
% 3.96/4.12  cnf(c2010,plain,old(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007)|~dirty(skolem0007)|~old(skolem0007),inference(resolution,[status(thm)],[c1962, c168])).
% 3.96/4.12  cnf(c2405,plain,old(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007)|~dirty(skolem0007),inference(resolution,[status(thm)],[c2010, c164])).
% 3.96/4.12  cnf(c2408,plain,old(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007),inference(resolution,[status(thm)],[c2405, c163])).
% 3.96/4.12  cnf(c2413,plain,old(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007),inference(resolution,[status(thm)],[c2408, c162])).
% 3.96/4.12  cnf(c2416,plain,old(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007),inference(resolution,[status(thm)],[c2413, c161])).
% 3.96/4.12  cnf(c2418,plain,old(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008),inference(resolution,[status(thm)],[c2416, c160])).
% 3.96/4.12  cnf(c2423,plain,old(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008),inference(resolution,[status(thm)],[c2418, c167])).
% 3.96/4.12  cnf(c2428,plain,old(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008),inference(resolution,[status(thm)],[c2423, c166])).
% 3.96/4.12  cnf(c2432,plain,old(skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006),inference(resolution,[status(thm)],[c2428, c165])).
% 3.96/4.12  cnf(c2435,plain,old(skolem0004)|~hollywood(skolem0005)|~city(skolem0005),inference(resolution,[status(thm)],[c2432, c159])).
% 3.96/4.12  cnf(c2439,plain,old(skolem0004)|~hollywood(skolem0005),inference(resolution,[status(thm)],[c2435, c158])).
% 3.96/4.12  cnf(c2442,plain,old(skolem0004),inference(resolution,[status(thm)],[c2439, c157])).
% 3.96/4.12  cnf(c52,negated_conjecture,street(skolem0003)|hollywood(skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c53,negated_conjecture,street(skolem0003)|city(skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c54,negated_conjecture,street(skolem0003)|event(skolem0006),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c60,negated_conjecture,street(skolem0003)|street(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c61,negated_conjecture,street(skolem0003)|way(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c62,negated_conjecture,street(skolem0003)|lonely(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c55,negated_conjecture,street(skolem0003)|chevy(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c56,negated_conjecture,street(skolem0003)|car(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c57,negated_conjecture,street(skolem0003)|white(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c58,negated_conjecture,street(skolem0003)|dirty(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c59,negated_conjecture,street(skolem0003)|old(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c63,negated_conjecture,street(skolem0003)|barrel(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c64,negated_conjecture,street(skolem0003)|down(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c65,negated_conjecture,street(skolem0003)|in(skolem0006,skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c66,negated_conjecture,street(skolem0003)|~hollywood(X30)|~city(X30)|~event(X33)|~street(X32)|~way(X32)|~lonely(X32)|~chevy(X31)|~car(X31)|~white(X31)|~dirty(X31)|~old(X31)|~barrel(X33,X31)|~down(X33,X32)|~in(X33,X30),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c246,plain,street(skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(X167)|~way(X167)|~lonely(X167)|~chevy(X168)|~car(X168)|~white(X168)|~dirty(X168)|~old(X168)|~barrel(skolem0006,X168)|~down(skolem0006,X167),inference(resolution,[status(thm)],[c66, c65])).
% 3.96/4.12  cnf(c1259,plain,street(skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(X199)|~car(X199)|~white(X199)|~dirty(X199)|~old(X199)|~barrel(skolem0006,X199),inference(resolution,[status(thm)],[c246, c64])).
% 3.96/4.12  cnf(c1315,plain,street(skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007)|~dirty(skolem0007)|~old(skolem0007),inference(resolution,[status(thm)],[c1259, c63])).
% 3.96/4.12  cnf(c1654,plain,street(skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007)|~dirty(skolem0007),inference(resolution,[status(thm)],[c1315, c59])).
% 3.96/4.12  cnf(c1669,plain,street(skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007),inference(resolution,[status(thm)],[c1654, c58])).
% 3.96/4.12  cnf(c1683,plain,street(skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007),inference(resolution,[status(thm)],[c1669, c57])).
% 3.96/4.12  cnf(c1691,plain,street(skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007),inference(resolution,[status(thm)],[c1683, c56])).
% 3.96/4.12  cnf(c1699,plain,street(skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008),inference(resolution,[status(thm)],[c1691, c55])).
% 3.96/4.12  cnf(c1708,plain,street(skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008),inference(resolution,[status(thm)],[c1699, c62])).
% 3.96/4.12  cnf(c1719,plain,street(skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008),inference(resolution,[status(thm)],[c1708, c61])).
% 3.96/4.12  cnf(c1739,plain,street(skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006),inference(resolution,[status(thm)],[c1719, c60])).
% 3.96/4.12  cnf(c1754,plain,street(skolem0003)|~hollywood(skolem0005)|~city(skolem0005),inference(resolution,[status(thm)],[c1739, c54])).
% 3.96/4.12  cnf(c1769,plain,street(skolem0003)|~hollywood(skolem0005),inference(resolution,[status(thm)],[c1754, c53])).
% 3.96/4.12  cnf(c1774,plain,street(skolem0003),inference(resolution,[status(thm)],[c1769, c52])).
% 3.96/4.12  cnf(c67,negated_conjecture,way(skolem0003)|hollywood(skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c68,negated_conjecture,way(skolem0003)|city(skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c69,negated_conjecture,way(skolem0003)|event(skolem0006),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c75,negated_conjecture,way(skolem0003)|street(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c76,negated_conjecture,way(skolem0003)|way(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c77,negated_conjecture,way(skolem0003)|lonely(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c70,negated_conjecture,way(skolem0003)|chevy(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c71,negated_conjecture,way(skolem0003)|car(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c72,negated_conjecture,way(skolem0003)|white(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c73,negated_conjecture,way(skolem0003)|dirty(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c74,negated_conjecture,way(skolem0003)|old(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c78,negated_conjecture,way(skolem0003)|barrel(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c79,negated_conjecture,way(skolem0003)|down(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c80,negated_conjecture,way(skolem0003)|in(skolem0006,skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c81,negated_conjecture,way(skolem0003)|~hollywood(X34)|~city(X34)|~event(X37)|~street(X36)|~way(X36)|~lonely(X36)|~chevy(X35)|~car(X35)|~white(X35)|~dirty(X35)|~old(X35)|~barrel(X37,X35)|~down(X37,X36)|~in(X37,X34),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c252,plain,way(skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(X180)|~way(X180)|~lonely(X180)|~chevy(X179)|~car(X179)|~white(X179)|~dirty(X179)|~old(X179)|~barrel(skolem0006,X179)|~down(skolem0006,X180),inference(resolution,[status(thm)],[c81, c80])).
% 3.96/4.12  cnf(c1277,plain,way(skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(X200)|~car(X200)|~white(X200)|~dirty(X200)|~old(X200)|~barrel(skolem0006,X200),inference(resolution,[status(thm)],[c252, c79])).
% 3.96/4.12  cnf(c1321,plain,way(skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007)|~dirty(skolem0007)|~old(skolem0007),inference(resolution,[status(thm)],[c1277, c78])).
% 3.96/4.12  cnf(c1834,plain,way(skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007)|~dirty(skolem0007),inference(resolution,[status(thm)],[c1321, c74])).
% 3.96/4.12  cnf(c1851,plain,way(skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007),inference(resolution,[status(thm)],[c1834, c73])).
% 3.96/4.12  cnf(c1859,plain,way(skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007),inference(resolution,[status(thm)],[c1851, c72])).
% 3.96/4.12  cnf(c1873,plain,way(skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007),inference(resolution,[status(thm)],[c1859, c71])).
% 3.96/4.12  cnf(c1883,plain,way(skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008),inference(resolution,[status(thm)],[c1873, c70])).
% 3.96/4.12  cnf(c1887,plain,way(skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008),inference(resolution,[status(thm)],[c1883, c77])).
% 3.96/4.12  cnf(c1911,plain,way(skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008),inference(resolution,[status(thm)],[c1887, c76])).
% 3.96/4.12  cnf(c1921,plain,way(skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006),inference(resolution,[status(thm)],[c1911, c75])).
% 3.96/4.12  cnf(c1931,plain,way(skolem0003)|~hollywood(skolem0005)|~city(skolem0005),inference(resolution,[status(thm)],[c1921, c69])).
% 3.96/4.12  cnf(c1939,plain,way(skolem0003)|~hollywood(skolem0005),inference(resolution,[status(thm)],[c1931, c68])).
% 3.96/4.12  cnf(c1951,plain,way(skolem0003),inference(resolution,[status(thm)],[c1939, c67])).
% 3.96/4.12  cnf(c82,negated_conjecture,lonely(skolem0003)|hollywood(skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c83,negated_conjecture,lonely(skolem0003)|city(skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c84,negated_conjecture,lonely(skolem0003)|event(skolem0006),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c90,negated_conjecture,lonely(skolem0003)|street(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c91,negated_conjecture,lonely(skolem0003)|way(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c92,negated_conjecture,lonely(skolem0003)|lonely(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c85,negated_conjecture,lonely(skolem0003)|chevy(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c86,negated_conjecture,lonely(skolem0003)|car(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c87,negated_conjecture,lonely(skolem0003)|white(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c88,negated_conjecture,lonely(skolem0003)|dirty(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c89,negated_conjecture,lonely(skolem0003)|old(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c93,negated_conjecture,lonely(skolem0003)|barrel(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c94,negated_conjecture,lonely(skolem0003)|down(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c95,negated_conjecture,lonely(skolem0003)|in(skolem0006,skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c96,negated_conjecture,lonely(skolem0003)|~hollywood(X38)|~city(X38)|~event(X41)|~street(X40)|~way(X40)|~lonely(X40)|~chevy(X39)|~car(X39)|~white(X39)|~dirty(X39)|~old(X39)|~barrel(X41,X39)|~down(X41,X40)|~in(X41,X38),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c272,plain,lonely(skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(X223)|~way(X223)|~lonely(X223)|~chevy(X224)|~car(X224)|~white(X224)|~dirty(X224)|~old(X224)|~barrel(skolem0006,X224)|~down(skolem0006,X223),inference(resolution,[status(thm)],[c96, c95])).
% 3.96/4.12  cnf(c1488,plain,lonely(skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(X393)|~car(X393)|~white(X393)|~dirty(X393)|~old(X393)|~barrel(skolem0006,X393),inference(resolution,[status(thm)],[c272, c94])).
% 3.96/4.12  cnf(c1968,plain,lonely(skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007)|~dirty(skolem0007)|~old(skolem0007),inference(resolution,[status(thm)],[c1488, c93])).
% 3.96/4.12  cnf(c2020,plain,lonely(skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007)|~dirty(skolem0007),inference(resolution,[status(thm)],[c1968, c89])).
% 3.96/4.12  cnf(c2032,plain,lonely(skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007),inference(resolution,[status(thm)],[c2020, c88])).
% 3.96/4.12  cnf(c2038,plain,lonely(skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007),inference(resolution,[status(thm)],[c2032, c87])).
% 3.96/4.12  cnf(c2044,plain,lonely(skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007),inference(resolution,[status(thm)],[c2038, c86])).
% 3.96/4.12  cnf(c2058,plain,lonely(skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008),inference(resolution,[status(thm)],[c2044, c85])).
% 3.96/4.12  cnf(c2062,plain,lonely(skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008),inference(resolution,[status(thm)],[c2058, c92])).
% 3.96/4.12  cnf(c2072,plain,lonely(skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008),inference(resolution,[status(thm)],[c2062, c91])).
% 3.96/4.12  cnf(c2082,plain,lonely(skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006),inference(resolution,[status(thm)],[c2072, c90])).
% 3.96/4.12  cnf(c2093,plain,lonely(skolem0003)|~hollywood(skolem0005)|~city(skolem0005),inference(resolution,[status(thm)],[c2082, c84])).
% 3.96/4.12  cnf(c2106,plain,lonely(skolem0003)|~hollywood(skolem0005),inference(resolution,[status(thm)],[c2093, c83])).
% 3.96/4.12  cnf(c2110,plain,lonely(skolem0003),inference(resolution,[status(thm)],[c2106, c82])).
% 3.96/4.12  cnf(c172,negated_conjecture,barrel(skolem0002,skolem0004)|hollywood(skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c187,negated_conjecture,down(skolem0002,skolem0003)|hollywood(skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c202,negated_conjecture,in(skolem0002,skolem0001)|hollywood(skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c217,negated_conjecture,~hollywood(X66)|~city(X66)|~event(X67)|~chevy(X69)|~car(X69)|~white(X69)|~dirty(X69)|~old(X69)|~street(X68)|~way(X68)|~lonely(X68)|~barrel(X67,X69)|~down(X67,X68)|~in(X67,X66)|hollywood(skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c585,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(X575)|~car(X575)|~white(X575)|~dirty(X575)|~old(X575)|~street(X576)|~way(X576)|~lonely(X576)|~barrel(skolem0002,X575)|~down(skolem0002,X576)|hollywood(skolem0005),inference(resolution,[status(thm)],[c217, c202])).
% 3.96/4.12  cnf(c2453,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(X579)|~car(X579)|~white(X579)|~dirty(X579)|~old(X579)|~street(skolem0003)|~way(skolem0003)|~lonely(skolem0003)|~barrel(skolem0002,X579)|hollywood(skolem0005),inference(resolution,[status(thm)],[c585, c187])).
% 3.96/4.12  cnf(c2467,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003)|~way(skolem0003)|~lonely(skolem0003)|hollywood(skolem0005),inference(resolution,[status(thm)],[c2453, c172])).
% 3.96/4.12  cnf(c2474,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003)|~way(skolem0003)|hollywood(skolem0005),inference(resolution,[status(thm)],[c2467, c2110])).
% 3.96/4.12  cnf(c2475,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003)|hollywood(skolem0005),inference(resolution,[status(thm)],[c2474, c1951])).
% 3.96/4.12  cnf(c2476,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|hollywood(skolem0005),inference(resolution,[status(thm)],[c2475, c1774])).
% 3.96/4.12  cnf(c2477,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|hollywood(skolem0005),inference(resolution,[status(thm)],[c2476, c2442])).
% 3.96/4.12  cnf(c2478,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|hollywood(skolem0005),inference(resolution,[status(thm)],[c2477, c2398])).
% 3.96/4.12  cnf(c2479,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|hollywood(skolem0005),inference(resolution,[status(thm)],[c2478, c2341])).
% 3.96/4.12  cnf(c2480,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|hollywood(skolem0005),inference(resolution,[status(thm)],[c2479, c2277])).
% 3.96/4.12  cnf(c2481,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|hollywood(skolem0005),inference(resolution,[status(thm)],[c2480, c2197])).
% 3.96/4.12  cnf(c2482,plain,~hollywood(skolem0001)|~city(skolem0001)|hollywood(skolem0005),inference(resolution,[status(thm)],[c2481, c1640])).
% 3.96/4.12  cnf(c2483,plain,~hollywood(skolem0001)|hollywood(skolem0005),inference(resolution,[status(thm)],[c2482, c1471])).
% 3.96/4.12  cnf(c2484,plain,hollywood(skolem0005),inference(resolution,[status(thm)],[c2483, c1190])).
% 3.96/4.12  cnf(c173,negated_conjecture,barrel(skolem0002,skolem0004)|city(skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c188,negated_conjecture,down(skolem0002,skolem0003)|city(skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c203,negated_conjecture,in(skolem0002,skolem0001)|city(skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.12  cnf(c218,negated_conjecture,~hollywood(X74)|~city(X74)|~event(X75)|~chevy(X77)|~car(X77)|~white(X77)|~dirty(X77)|~old(X77)|~street(X76)|~way(X76)|~lonely(X76)|~barrel(X75,X77)|~down(X75,X76)|~in(X75,X74)|city(skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c645,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(X584)|~car(X584)|~white(X584)|~dirty(X584)|~old(X584)|~street(X585)|~way(X585)|~lonely(X585)|~barrel(skolem0002,X584)|~down(skolem0002,X585)|city(skolem0005),inference(resolution,[status(thm)],[c218, c203])).
% 3.96/4.13  cnf(c2492,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(X586)|~car(X586)|~white(X586)|~dirty(X586)|~old(X586)|~street(skolem0003)|~way(skolem0003)|~lonely(skolem0003)|~barrel(skolem0002,X586)|city(skolem0005),inference(resolution,[status(thm)],[c645, c188])).
% 3.96/4.13  cnf(c2509,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003)|~way(skolem0003)|~lonely(skolem0003)|city(skolem0005),inference(resolution,[status(thm)],[c2492, c173])).
% 3.96/4.13  cnf(c2511,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003)|~way(skolem0003)|city(skolem0005),inference(resolution,[status(thm)],[c2509, c2110])).
% 3.96/4.13  cnf(c2512,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003)|city(skolem0005),inference(resolution,[status(thm)],[c2511, c1951])).
% 3.96/4.13  cnf(c2513,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|city(skolem0005),inference(resolution,[status(thm)],[c2512, c1774])).
% 3.96/4.13  cnf(c2514,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|city(skolem0005),inference(resolution,[status(thm)],[c2513, c2442])).
% 3.96/4.13  cnf(c2515,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|city(skolem0005),inference(resolution,[status(thm)],[c2514, c2398])).
% 3.96/4.13  cnf(c2516,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|city(skolem0005),inference(resolution,[status(thm)],[c2515, c2341])).
% 3.96/4.13  cnf(c2517,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|city(skolem0005),inference(resolution,[status(thm)],[c2516, c2277])).
% 3.96/4.13  cnf(c2518,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|city(skolem0005),inference(resolution,[status(thm)],[c2517, c2197])).
% 3.96/4.13  cnf(c2519,plain,~hollywood(skolem0001)|~city(skolem0001)|city(skolem0005),inference(resolution,[status(thm)],[c2518, c1640])).
% 3.96/4.13  cnf(c2520,plain,~hollywood(skolem0001)|city(skolem0005),inference(resolution,[status(thm)],[c2519, c1471])).
% 3.96/4.13  cnf(c2521,plain,city(skolem0005),inference(resolution,[status(thm)],[c2520, c1190])).
% 3.96/4.13  cnf(c174,negated_conjecture,barrel(skolem0002,skolem0004)|event(skolem0006),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c189,negated_conjecture,down(skolem0002,skolem0003)|event(skolem0006),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c204,negated_conjecture,in(skolem0002,skolem0001)|event(skolem0006),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c219,negated_conjecture,~hollywood(X78)|~city(X78)|~event(X79)|~chevy(X81)|~car(X81)|~white(X81)|~dirty(X81)|~old(X81)|~street(X80)|~way(X80)|~lonely(X80)|~barrel(X79,X81)|~down(X79,X80)|~in(X79,X78)|event(skolem0006),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c664,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(X593)|~car(X593)|~white(X593)|~dirty(X593)|~old(X593)|~street(X594)|~way(X594)|~lonely(X594)|~barrel(skolem0002,X593)|~down(skolem0002,X594)|event(skolem0006),inference(resolution,[status(thm)],[c219, c204])).
% 3.96/4.13  cnf(c2531,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(X595)|~car(X595)|~white(X595)|~dirty(X595)|~old(X595)|~street(skolem0003)|~way(skolem0003)|~lonely(skolem0003)|~barrel(skolem0002,X595)|event(skolem0006),inference(resolution,[status(thm)],[c664, c189])).
% 3.96/4.13  cnf(c2543,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003)|~way(skolem0003)|~lonely(skolem0003)|event(skolem0006),inference(resolution,[status(thm)],[c2531, c174])).
% 3.96/4.13  cnf(c2546,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003)|~way(skolem0003)|event(skolem0006),inference(resolution,[status(thm)],[c2543, c2110])).
% 3.96/4.13  cnf(c2547,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003)|event(skolem0006),inference(resolution,[status(thm)],[c2546, c1951])).
% 3.96/4.13  cnf(c2548,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|event(skolem0006),inference(resolution,[status(thm)],[c2547, c1774])).
% 3.96/4.13  cnf(c2549,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|event(skolem0006),inference(resolution,[status(thm)],[c2548, c2442])).
% 3.96/4.13  cnf(c2550,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|event(skolem0006),inference(resolution,[status(thm)],[c2549, c2398])).
% 3.96/4.13  cnf(c2551,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|event(skolem0006),inference(resolution,[status(thm)],[c2550, c2341])).
% 3.96/4.13  cnf(c2552,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|event(skolem0006),inference(resolution,[status(thm)],[c2551, c2277])).
% 3.96/4.13  cnf(c2553,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|event(skolem0006),inference(resolution,[status(thm)],[c2552, c2197])).
% 3.96/4.13  cnf(c2554,plain,~hollywood(skolem0001)|~city(skolem0001)|event(skolem0006),inference(resolution,[status(thm)],[c2553, c1640])).
% 3.96/4.13  cnf(c2555,plain,~hollywood(skolem0001)|event(skolem0006),inference(resolution,[status(thm)],[c2554, c1471])).
% 3.96/4.13  cnf(c2556,plain,event(skolem0006),inference(resolution,[status(thm)],[c2555, c1190])).
% 3.96/4.13  cnf(c180,negated_conjecture,barrel(skolem0002,skolem0004)|street(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c195,negated_conjecture,down(skolem0002,skolem0003)|street(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c210,negated_conjecture,in(skolem0002,skolem0001)|street(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c225,negated_conjecture,~hollywood(X106)|~city(X106)|~event(X107)|~chevy(X109)|~car(X109)|~white(X109)|~dirty(X109)|~old(X109)|~street(X108)|~way(X108)|~lonely(X108)|~barrel(X107,X109)|~down(X107,X108)|~in(X107,X106)|street(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c868,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(X646)|~car(X646)|~white(X646)|~dirty(X646)|~old(X646)|~street(X645)|~way(X645)|~lonely(X645)|~barrel(skolem0002,X646)|~down(skolem0002,X645)|street(skolem0008),inference(resolution,[status(thm)],[c225, c210])).
% 3.96/4.13  cnf(c2703,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(X647)|~car(X647)|~white(X647)|~dirty(X647)|~old(X647)|~street(skolem0003)|~way(skolem0003)|~lonely(skolem0003)|~barrel(skolem0002,X647)|street(skolem0008),inference(resolution,[status(thm)],[c868, c195])).
% 3.96/4.13  cnf(c2712,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003)|~way(skolem0003)|~lonely(skolem0003)|street(skolem0008),inference(resolution,[status(thm)],[c2703, c180])).
% 3.96/4.13  cnf(c2714,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003)|~way(skolem0003)|street(skolem0008),inference(resolution,[status(thm)],[c2712, c2110])).
% 3.96/4.13  cnf(c2715,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003)|street(skolem0008),inference(resolution,[status(thm)],[c2714, c1951])).
% 3.96/4.13  cnf(c2716,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|street(skolem0008),inference(resolution,[status(thm)],[c2715, c1774])).
% 3.96/4.13  cnf(c2717,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|street(skolem0008),inference(resolution,[status(thm)],[c2716, c2442])).
% 3.96/4.13  cnf(c2718,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|street(skolem0008),inference(resolution,[status(thm)],[c2717, c2398])).
% 3.96/4.13  cnf(c2719,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|street(skolem0008),inference(resolution,[status(thm)],[c2718, c2341])).
% 3.96/4.13  cnf(c2720,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|street(skolem0008),inference(resolution,[status(thm)],[c2719, c2277])).
% 3.96/4.13  cnf(c2721,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|street(skolem0008),inference(resolution,[status(thm)],[c2720, c2197])).
% 3.96/4.13  cnf(c2722,plain,~hollywood(skolem0001)|~city(skolem0001)|street(skolem0008),inference(resolution,[status(thm)],[c2721, c1640])).
% 3.96/4.13  cnf(c2723,plain,~hollywood(skolem0001)|street(skolem0008),inference(resolution,[status(thm)],[c2722, c1471])).
% 3.96/4.13  cnf(c2724,plain,street(skolem0008),inference(resolution,[status(thm)],[c2723, c1190])).
% 3.96/4.13  cnf(c181,negated_conjecture,barrel(skolem0002,skolem0004)|way(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c196,negated_conjecture,down(skolem0002,skolem0003)|way(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c211,negated_conjecture,in(skolem0002,skolem0001)|way(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c226,negated_conjecture,~hollywood(X110)|~city(X110)|~event(X111)|~chevy(X113)|~car(X113)|~white(X113)|~dirty(X113)|~old(X113)|~street(X112)|~way(X112)|~lonely(X112)|~barrel(X111,X113)|~down(X111,X112)|~in(X111,X110)|way(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c890,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(X654)|~car(X654)|~white(X654)|~dirty(X654)|~old(X654)|~street(X655)|~way(X655)|~lonely(X655)|~barrel(skolem0002,X654)|~down(skolem0002,X655)|way(skolem0008),inference(resolution,[status(thm)],[c226, c211])).
% 3.96/4.13  cnf(c2726,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(X656)|~car(X656)|~white(X656)|~dirty(X656)|~old(X656)|~street(skolem0003)|~way(skolem0003)|~lonely(skolem0003)|~barrel(skolem0002,X656)|way(skolem0008),inference(resolution,[status(thm)],[c890, c196])).
% 3.96/4.13  cnf(c2734,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003)|~way(skolem0003)|~lonely(skolem0003)|way(skolem0008),inference(resolution,[status(thm)],[c2726, c181])).
% 3.96/4.13  cnf(c2735,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003)|~way(skolem0003)|way(skolem0008),inference(resolution,[status(thm)],[c2734, c2110])).
% 3.96/4.13  cnf(c2736,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003)|way(skolem0008),inference(resolution,[status(thm)],[c2735, c1951])).
% 3.96/4.13  cnf(c2737,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|way(skolem0008),inference(resolution,[status(thm)],[c2736, c1774])).
% 3.96/4.13  cnf(c2738,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|way(skolem0008),inference(resolution,[status(thm)],[c2737, c2442])).
% 3.96/4.13  cnf(c2739,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|way(skolem0008),inference(resolution,[status(thm)],[c2738, c2398])).
% 3.96/4.13  cnf(c2740,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|way(skolem0008),inference(resolution,[status(thm)],[c2739, c2341])).
% 3.96/4.13  cnf(c2741,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|way(skolem0008),inference(resolution,[status(thm)],[c2740, c2277])).
% 3.96/4.13  cnf(c2742,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|way(skolem0008),inference(resolution,[status(thm)],[c2741, c2197])).
% 3.96/4.13  cnf(c2743,plain,~hollywood(skolem0001)|~city(skolem0001)|way(skolem0008),inference(resolution,[status(thm)],[c2742, c1640])).
% 3.96/4.13  cnf(c2744,plain,~hollywood(skolem0001)|way(skolem0008),inference(resolution,[status(thm)],[c2743, c1471])).
% 3.96/4.13  cnf(c2745,plain,way(skolem0008),inference(resolution,[status(thm)],[c2744, c1190])).
% 3.96/4.13  cnf(c182,negated_conjecture,barrel(skolem0002,skolem0004)|lonely(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c197,negated_conjecture,down(skolem0002,skolem0003)|lonely(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c212,negated_conjecture,in(skolem0002,skolem0001)|lonely(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c227,negated_conjecture,~hollywood(X114)|~city(X114)|~event(X115)|~chevy(X117)|~car(X117)|~white(X117)|~dirty(X117)|~old(X117)|~street(X116)|~way(X116)|~lonely(X116)|~barrel(X115,X117)|~down(X115,X116)|~in(X115,X114)|lonely(skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c913,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(X661)|~car(X661)|~white(X661)|~dirty(X661)|~old(X661)|~street(X662)|~way(X662)|~lonely(X662)|~barrel(skolem0002,X661)|~down(skolem0002,X662)|lonely(skolem0008),inference(resolution,[status(thm)],[c227, c212])).
% 3.96/4.13  cnf(c2747,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(X665)|~car(X665)|~white(X665)|~dirty(X665)|~old(X665)|~street(skolem0003)|~way(skolem0003)|~lonely(skolem0003)|~barrel(skolem0002,X665)|lonely(skolem0008),inference(resolution,[status(thm)],[c913, c197])).
% 3.96/4.13  cnf(c2752,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003)|~way(skolem0003)|~lonely(skolem0003)|lonely(skolem0008),inference(resolution,[status(thm)],[c2747, c182])).
% 3.96/4.13  cnf(c2754,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003)|~way(skolem0003)|lonely(skolem0008),inference(resolution,[status(thm)],[c2752, c2110])).
% 3.96/4.13  cnf(c2755,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003)|lonely(skolem0008),inference(resolution,[status(thm)],[c2754, c1951])).
% 3.96/4.13  cnf(c2756,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|lonely(skolem0008),inference(resolution,[status(thm)],[c2755, c1774])).
% 3.96/4.13  cnf(c2757,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|lonely(skolem0008),inference(resolution,[status(thm)],[c2756, c2442])).
% 3.96/4.13  cnf(c2758,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|lonely(skolem0008),inference(resolution,[status(thm)],[c2757, c2398])).
% 3.96/4.13  cnf(c2759,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|lonely(skolem0008),inference(resolution,[status(thm)],[c2758, c2341])).
% 3.96/4.13  cnf(c2760,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|lonely(skolem0008),inference(resolution,[status(thm)],[c2759, c2277])).
% 3.96/4.13  cnf(c2761,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|lonely(skolem0008),inference(resolution,[status(thm)],[c2760, c2197])).
% 3.96/4.13  cnf(c2762,plain,~hollywood(skolem0001)|~city(skolem0001)|lonely(skolem0008),inference(resolution,[status(thm)],[c2761, c1640])).
% 3.96/4.13  cnf(c2763,plain,~hollywood(skolem0001)|lonely(skolem0008),inference(resolution,[status(thm)],[c2762, c1471])).
% 3.96/4.13  cnf(c2764,plain,lonely(skolem0008),inference(resolution,[status(thm)],[c2763, c1190])).
% 3.96/4.13  cnf(c175,negated_conjecture,barrel(skolem0002,skolem0004)|chevy(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c190,negated_conjecture,down(skolem0002,skolem0003)|chevy(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c205,negated_conjecture,in(skolem0002,skolem0001)|chevy(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c220,negated_conjecture,~hollywood(X82)|~city(X82)|~event(X83)|~chevy(X85)|~car(X85)|~white(X85)|~dirty(X85)|~old(X85)|~street(X84)|~way(X84)|~lonely(X84)|~barrel(X83,X85)|~down(X83,X84)|~in(X83,X82)|chevy(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c682,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(X602)|~car(X602)|~white(X602)|~dirty(X602)|~old(X602)|~street(X603)|~way(X603)|~lonely(X603)|~barrel(skolem0002,X602)|~down(skolem0002,X603)|chevy(skolem0007),inference(resolution,[status(thm)],[c220, c205])).
% 3.96/4.13  cnf(c2565,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(X604)|~car(X604)|~white(X604)|~dirty(X604)|~old(X604)|~street(skolem0003)|~way(skolem0003)|~lonely(skolem0003)|~barrel(skolem0002,X604)|chevy(skolem0007),inference(resolution,[status(thm)],[c682, c190])).
% 3.96/4.13  cnf(c2578,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003)|~way(skolem0003)|~lonely(skolem0003)|chevy(skolem0007),inference(resolution,[status(thm)],[c2565, c175])).
% 3.96/4.13  cnf(c2579,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003)|~way(skolem0003)|chevy(skolem0007),inference(resolution,[status(thm)],[c2578, c2110])).
% 3.96/4.13  cnf(c2580,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003)|chevy(skolem0007),inference(resolution,[status(thm)],[c2579, c1951])).
% 3.96/4.13  cnf(c2581,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|chevy(skolem0007),inference(resolution,[status(thm)],[c2580, c1774])).
% 3.96/4.13  cnf(c2582,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|chevy(skolem0007),inference(resolution,[status(thm)],[c2581, c2442])).
% 3.96/4.13  cnf(c2583,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|chevy(skolem0007),inference(resolution,[status(thm)],[c2582, c2398])).
% 3.96/4.13  cnf(c2584,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|chevy(skolem0007),inference(resolution,[status(thm)],[c2583, c2341])).
% 3.96/4.13  cnf(c2585,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|chevy(skolem0007),inference(resolution,[status(thm)],[c2584, c2277])).
% 3.96/4.13  cnf(c2586,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|chevy(skolem0007),inference(resolution,[status(thm)],[c2585, c2197])).
% 3.96/4.13  cnf(c2587,plain,~hollywood(skolem0001)|~city(skolem0001)|chevy(skolem0007),inference(resolution,[status(thm)],[c2586, c1640])).
% 3.96/4.13  cnf(c2588,plain,~hollywood(skolem0001)|chevy(skolem0007),inference(resolution,[status(thm)],[c2587, c1471])).
% 3.96/4.13  cnf(c2589,plain,chevy(skolem0007),inference(resolution,[status(thm)],[c2588, c1190])).
% 3.96/4.13  cnf(c176,negated_conjecture,barrel(skolem0002,skolem0004)|car(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c191,negated_conjecture,down(skolem0002,skolem0003)|car(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c206,negated_conjecture,in(skolem0002,skolem0001)|car(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c221,negated_conjecture,~hollywood(X86)|~city(X86)|~event(X87)|~chevy(X89)|~car(X89)|~white(X89)|~dirty(X89)|~old(X89)|~street(X88)|~way(X88)|~lonely(X88)|~barrel(X87,X89)|~down(X87,X88)|~in(X87,X86)|car(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c714,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(X612)|~car(X612)|~white(X612)|~dirty(X612)|~old(X612)|~street(X611)|~way(X611)|~lonely(X611)|~barrel(skolem0002,X612)|~down(skolem0002,X611)|car(skolem0007),inference(resolution,[status(thm)],[c221, c206])).
% 3.96/4.13  cnf(c2594,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(X613)|~car(X613)|~white(X613)|~dirty(X613)|~old(X613)|~street(skolem0003)|~way(skolem0003)|~lonely(skolem0003)|~barrel(skolem0002,X613)|car(skolem0007),inference(resolution,[status(thm)],[c714, c191])).
% 3.96/4.13  cnf(c2609,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003)|~way(skolem0003)|~lonely(skolem0003)|car(skolem0007),inference(resolution,[status(thm)],[c2594, c176])).
% 3.96/4.13  cnf(c2610,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003)|~way(skolem0003)|car(skolem0007),inference(resolution,[status(thm)],[c2609, c2110])).
% 3.96/4.13  cnf(c2611,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003)|car(skolem0007),inference(resolution,[status(thm)],[c2610, c1951])).
% 3.96/4.13  cnf(c2612,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|car(skolem0007),inference(resolution,[status(thm)],[c2611, c1774])).
% 3.96/4.13  cnf(c2613,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|car(skolem0007),inference(resolution,[status(thm)],[c2612, c2442])).
% 3.96/4.13  cnf(c2614,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|car(skolem0007),inference(resolution,[status(thm)],[c2613, c2398])).
% 3.96/4.13  cnf(c2615,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|car(skolem0007),inference(resolution,[status(thm)],[c2614, c2341])).
% 3.96/4.13  cnf(c2616,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|car(skolem0007),inference(resolution,[status(thm)],[c2615, c2277])).
% 3.96/4.13  cnf(c2617,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|car(skolem0007),inference(resolution,[status(thm)],[c2616, c2197])).
% 3.96/4.13  cnf(c2618,plain,~hollywood(skolem0001)|~city(skolem0001)|car(skolem0007),inference(resolution,[status(thm)],[c2617, c1640])).
% 3.96/4.13  cnf(c2619,plain,~hollywood(skolem0001)|car(skolem0007),inference(resolution,[status(thm)],[c2618, c1471])).
% 3.96/4.13  cnf(c2620,plain,car(skolem0007),inference(resolution,[status(thm)],[c2619, c1190])).
% 3.96/4.13  cnf(c177,negated_conjecture,barrel(skolem0002,skolem0004)|white(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c192,negated_conjecture,down(skolem0002,skolem0003)|white(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c207,negated_conjecture,in(skolem0002,skolem0001)|white(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c222,negated_conjecture,~hollywood(X90)|~city(X90)|~event(X91)|~chevy(X93)|~car(X93)|~white(X93)|~dirty(X93)|~old(X93)|~street(X92)|~way(X92)|~lonely(X92)|~barrel(X91,X93)|~down(X91,X92)|~in(X91,X90)|white(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c759,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(X619)|~car(X619)|~white(X619)|~dirty(X619)|~old(X619)|~street(X618)|~way(X618)|~lonely(X618)|~barrel(skolem0002,X619)|~down(skolem0002,X618)|white(skolem0007),inference(resolution,[status(thm)],[c222, c207])).
% 3.96/4.13  cnf(c2622,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(X622)|~car(X622)|~white(X622)|~dirty(X622)|~old(X622)|~street(skolem0003)|~way(skolem0003)|~lonely(skolem0003)|~barrel(skolem0002,X622)|white(skolem0007),inference(resolution,[status(thm)],[c759, c192])).
% 3.96/4.13  cnf(c2637,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003)|~way(skolem0003)|~lonely(skolem0003)|white(skolem0007),inference(resolution,[status(thm)],[c2622, c177])).
% 3.96/4.13  cnf(c2639,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003)|~way(skolem0003)|white(skolem0007),inference(resolution,[status(thm)],[c2637, c2110])).
% 3.96/4.13  cnf(c2640,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003)|white(skolem0007),inference(resolution,[status(thm)],[c2639, c1951])).
% 3.96/4.13  cnf(c2641,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|white(skolem0007),inference(resolution,[status(thm)],[c2640, c1774])).
% 3.96/4.13  cnf(c2642,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|white(skolem0007),inference(resolution,[status(thm)],[c2641, c2442])).
% 3.96/4.13  cnf(c2643,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|white(skolem0007),inference(resolution,[status(thm)],[c2642, c2398])).
% 3.96/4.13  cnf(c2644,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|white(skolem0007),inference(resolution,[status(thm)],[c2643, c2341])).
% 3.96/4.13  cnf(c2645,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|white(skolem0007),inference(resolution,[status(thm)],[c2644, c2277])).
% 3.96/4.13  cnf(c2646,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|white(skolem0007),inference(resolution,[status(thm)],[c2645, c2197])).
% 3.96/4.13  cnf(c2647,plain,~hollywood(skolem0001)|~city(skolem0001)|white(skolem0007),inference(resolution,[status(thm)],[c2646, c1640])).
% 3.96/4.13  cnf(c2648,plain,~hollywood(skolem0001)|white(skolem0007),inference(resolution,[status(thm)],[c2647, c1471])).
% 3.96/4.13  cnf(c2649,plain,white(skolem0007),inference(resolution,[status(thm)],[c2648, c1190])).
% 3.96/4.13  cnf(c178,negated_conjecture,barrel(skolem0002,skolem0004)|dirty(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c193,negated_conjecture,down(skolem0002,skolem0003)|dirty(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c208,negated_conjecture,in(skolem0002,skolem0001)|dirty(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c223,negated_conjecture,~hollywood(X98)|~city(X98)|~event(X99)|~chevy(X101)|~car(X101)|~white(X101)|~dirty(X101)|~old(X101)|~street(X100)|~way(X100)|~lonely(X100)|~barrel(X99,X101)|~down(X99,X100)|~in(X99,X98)|dirty(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c814,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(X628)|~car(X628)|~white(X628)|~dirty(X628)|~old(X628)|~street(X627)|~way(X627)|~lonely(X627)|~barrel(skolem0002,X628)|~down(skolem0002,X627)|dirty(skolem0007),inference(resolution,[status(thm)],[c223, c208])).
% 3.96/4.13  cnf(c2651,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(X629)|~car(X629)|~white(X629)|~dirty(X629)|~old(X629)|~street(skolem0003)|~way(skolem0003)|~lonely(skolem0003)|~barrel(skolem0002,X629)|dirty(skolem0007),inference(resolution,[status(thm)],[c814, c193])).
% 3.96/4.13  cnf(c2665,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003)|~way(skolem0003)|~lonely(skolem0003)|dirty(skolem0007),inference(resolution,[status(thm)],[c2651, c178])).
% 3.96/4.13  cnf(c2666,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003)|~way(skolem0003)|dirty(skolem0007),inference(resolution,[status(thm)],[c2665, c2110])).
% 3.96/4.13  cnf(c2667,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003)|dirty(skolem0007),inference(resolution,[status(thm)],[c2666, c1951])).
% 3.96/4.13  cnf(c2668,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|dirty(skolem0007),inference(resolution,[status(thm)],[c2667, c1774])).
% 3.96/4.13  cnf(c2669,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|dirty(skolem0007),inference(resolution,[status(thm)],[c2668, c2442])).
% 3.96/4.13  cnf(c2670,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|dirty(skolem0007),inference(resolution,[status(thm)],[c2669, c2398])).
% 3.96/4.13  cnf(c2671,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|dirty(skolem0007),inference(resolution,[status(thm)],[c2670, c2341])).
% 3.96/4.13  cnf(c2672,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|dirty(skolem0007),inference(resolution,[status(thm)],[c2671, c2277])).
% 3.96/4.13  cnf(c2673,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|dirty(skolem0007),inference(resolution,[status(thm)],[c2672, c2197])).
% 3.96/4.13  cnf(c2674,plain,~hollywood(skolem0001)|~city(skolem0001)|dirty(skolem0007),inference(resolution,[status(thm)],[c2673, c1640])).
% 3.96/4.13  cnf(c2675,plain,~hollywood(skolem0001)|dirty(skolem0007),inference(resolution,[status(thm)],[c2674, c1471])).
% 3.96/4.13  cnf(c2676,plain,dirty(skolem0007),inference(resolution,[status(thm)],[c2675, c1190])).
% 3.96/4.13  cnf(c179,negated_conjecture,barrel(skolem0002,skolem0004)|old(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c194,negated_conjecture,down(skolem0002,skolem0003)|old(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c209,negated_conjecture,in(skolem0002,skolem0001)|old(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c224,negated_conjecture,~hollywood(X102)|~city(X102)|~event(X103)|~chevy(X105)|~car(X105)|~white(X105)|~dirty(X105)|~old(X105)|~street(X104)|~way(X104)|~lonely(X104)|~barrel(X103,X105)|~down(X103,X104)|~in(X103,X102)|old(skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c828,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(X636)|~car(X636)|~white(X636)|~dirty(X636)|~old(X636)|~street(X637)|~way(X637)|~lonely(X637)|~barrel(skolem0002,X636)|~down(skolem0002,X637)|old(skolem0007),inference(resolution,[status(thm)],[c224, c209])).
% 3.96/4.13  cnf(c2679,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(X638)|~car(X638)|~white(X638)|~dirty(X638)|~old(X638)|~street(skolem0003)|~way(skolem0003)|~lonely(skolem0003)|~barrel(skolem0002,X638)|old(skolem0007),inference(resolution,[status(thm)],[c828, c194])).
% 3.96/4.13  cnf(c2687,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003)|~way(skolem0003)|~lonely(skolem0003)|old(skolem0007),inference(resolution,[status(thm)],[c2679, c179])).
% 3.96/4.13  cnf(c2691,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003)|~way(skolem0003)|old(skolem0007),inference(resolution,[status(thm)],[c2687, c2110])).
% 3.96/4.13  cnf(c2692,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003)|old(skolem0007),inference(resolution,[status(thm)],[c2691, c1951])).
% 3.96/4.13  cnf(c2693,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|old(skolem0007),inference(resolution,[status(thm)],[c2692, c1774])).
% 3.96/4.13  cnf(c2694,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|old(skolem0007),inference(resolution,[status(thm)],[c2693, c2442])).
% 3.96/4.13  cnf(c2695,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|old(skolem0007),inference(resolution,[status(thm)],[c2694, c2398])).
% 3.96/4.13  cnf(c2696,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|old(skolem0007),inference(resolution,[status(thm)],[c2695, c2341])).
% 3.96/4.13  cnf(c2697,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|old(skolem0007),inference(resolution,[status(thm)],[c2696, c2277])).
% 3.96/4.13  cnf(c2698,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|old(skolem0007),inference(resolution,[status(thm)],[c2697, c2197])).
% 3.96/4.13  cnf(c2699,plain,~hollywood(skolem0001)|~city(skolem0001)|old(skolem0007),inference(resolution,[status(thm)],[c2698, c1640])).
% 3.96/4.13  cnf(c2700,plain,~hollywood(skolem0001)|old(skolem0007),inference(resolution,[status(thm)],[c2699, c1471])).
% 3.96/4.13  cnf(c2701,plain,old(skolem0007),inference(resolution,[status(thm)],[c2700, c1190])).
% 3.96/4.13  cnf(c183,negated_conjecture,barrel(skolem0002,skolem0004)|barrel(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c184,negated_conjecture,barrel(skolem0002,skolem0004)|down(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c185,negated_conjecture,barrel(skolem0002,skolem0004)|in(skolem0006,skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c186,negated_conjecture,barrel(skolem0002,skolem0004)|~hollywood(X62)|~city(X62)|~event(X65)|~street(X64)|~way(X64)|~lonely(X64)|~chevy(X63)|~car(X63)|~white(X63)|~dirty(X63)|~old(X63)|~barrel(X65,X63)|~down(X65,X64)|~in(X65,X62),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c505,plain,barrel(skolem0002,skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(X685)|~way(X685)|~lonely(X685)|~chevy(X684)|~car(X684)|~white(X684)|~dirty(X684)|~old(X684)|~barrel(skolem0006,X684)|~down(skolem0006,X685),inference(resolution,[status(thm)],[c186, c185])).
% 3.96/4.13  cnf(c2766,plain,barrel(skolem0002,skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(X686)|~car(X686)|~white(X686)|~dirty(X686)|~old(X686)|~barrel(skolem0006,X686),inference(resolution,[status(thm)],[c505, c184])).
% 3.96/4.13  cnf(c2768,plain,barrel(skolem0002,skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007)|~dirty(skolem0007)|~old(skolem0007),inference(resolution,[status(thm)],[c2766, c183])).
% 3.96/4.13  cnf(c2771,plain,barrel(skolem0002,skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007)|~dirty(skolem0007),inference(resolution,[status(thm)],[c2768, c2701])).
% 3.96/4.13  cnf(c2772,plain,barrel(skolem0002,skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007),inference(resolution,[status(thm)],[c2771, c2676])).
% 3.96/4.13  cnf(c2773,plain,barrel(skolem0002,skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007),inference(resolution,[status(thm)],[c2772, c2649])).
% 3.96/4.13  cnf(c2774,plain,barrel(skolem0002,skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007),inference(resolution,[status(thm)],[c2773, c2620])).
% 3.96/4.13  cnf(c2775,plain,barrel(skolem0002,skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008),inference(resolution,[status(thm)],[c2774, c2589])).
% 3.96/4.13  cnf(c2776,plain,barrel(skolem0002,skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008),inference(resolution,[status(thm)],[c2775, c2764])).
% 3.96/4.13  cnf(c2777,plain,barrel(skolem0002,skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008),inference(resolution,[status(thm)],[c2776, c2745])).
% 3.96/4.13  cnf(c2778,plain,barrel(skolem0002,skolem0004)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006),inference(resolution,[status(thm)],[c2777, c2724])).
% 3.96/4.13  cnf(c2779,plain,barrel(skolem0002,skolem0004)|~hollywood(skolem0005)|~city(skolem0005),inference(resolution,[status(thm)],[c2778, c2556])).
% 3.96/4.13  cnf(c2780,plain,barrel(skolem0002,skolem0004)|~hollywood(skolem0005),inference(resolution,[status(thm)],[c2779, c2521])).
% 3.96/4.13  cnf(c2781,plain,barrel(skolem0002,skolem0004),inference(resolution,[status(thm)],[c2780, c2484])).
% 3.96/4.13  cnf(c198,negated_conjecture,down(skolem0002,skolem0003)|barrel(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c199,negated_conjecture,down(skolem0002,skolem0003)|down(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c200,negated_conjecture,down(skolem0002,skolem0003)|in(skolem0006,skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c201,negated_conjecture,down(skolem0002,skolem0003)|~hollywood(X70)|~city(X70)|~event(X73)|~street(X72)|~way(X72)|~lonely(X72)|~chevy(X71)|~car(X71)|~white(X71)|~dirty(X71)|~old(X71)|~barrel(X73,X71)|~down(X73,X72)|~in(X73,X70),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c600,plain,down(skolem0002,skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(X693)|~way(X693)|~lonely(X693)|~chevy(X694)|~car(X694)|~white(X694)|~dirty(X694)|~old(X694)|~barrel(skolem0006,X694)|~down(skolem0006,X693),inference(resolution,[status(thm)],[c201, c200])).
% 3.96/4.13  cnf(c2783,plain,down(skolem0002,skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(X695)|~car(X695)|~white(X695)|~dirty(X695)|~old(X695)|~barrel(skolem0006,X695),inference(resolution,[status(thm)],[c600, c199])).
% 3.96/4.13  cnf(c2785,plain,down(skolem0002,skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007)|~dirty(skolem0007)|~old(skolem0007),inference(resolution,[status(thm)],[c2783, c198])).
% 3.96/4.13  cnf(c2786,plain,down(skolem0002,skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007)|~dirty(skolem0007),inference(resolution,[status(thm)],[c2785, c2701])).
% 3.96/4.13  cnf(c2787,plain,down(skolem0002,skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007),inference(resolution,[status(thm)],[c2786, c2676])).
% 3.96/4.13  cnf(c2788,plain,down(skolem0002,skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007),inference(resolution,[status(thm)],[c2787, c2649])).
% 3.96/4.13  cnf(c2789,plain,down(skolem0002,skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007),inference(resolution,[status(thm)],[c2788, c2620])).
% 3.96/4.13  cnf(c2790,plain,down(skolem0002,skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008),inference(resolution,[status(thm)],[c2789, c2589])).
% 3.96/4.13  cnf(c2791,plain,down(skolem0002,skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008),inference(resolution,[status(thm)],[c2790, c2764])).
% 3.96/4.13  cnf(c2792,plain,down(skolem0002,skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008),inference(resolution,[status(thm)],[c2791, c2745])).
% 3.96/4.13  cnf(c2793,plain,down(skolem0002,skolem0003)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006),inference(resolution,[status(thm)],[c2792, c2724])).
% 3.96/4.13  cnf(c2794,plain,down(skolem0002,skolem0003)|~hollywood(skolem0005)|~city(skolem0005),inference(resolution,[status(thm)],[c2793, c2556])).
% 3.96/4.13  cnf(c2795,plain,down(skolem0002,skolem0003)|~hollywood(skolem0005),inference(resolution,[status(thm)],[c2794, c2521])).
% 3.96/4.13  cnf(c2796,plain,down(skolem0002,skolem0003),inference(resolution,[status(thm)],[c2795, c2484])).
% 3.96/4.13  cnf(c213,negated_conjecture,in(skolem0002,skolem0001)|barrel(skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c214,negated_conjecture,in(skolem0002,skolem0001)|down(skolem0006,skolem0008),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c215,negated_conjecture,in(skolem0002,skolem0001)|in(skolem0006,skolem0005),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c216,negated_conjecture,in(skolem0002,skolem0001)|~hollywood(X94)|~city(X94)|~event(X97)|~street(X96)|~way(X96)|~lonely(X96)|~chevy(X95)|~car(X95)|~white(X95)|~dirty(X95)|~old(X95)|~barrel(X97,X95)|~down(X97,X96)|~in(X97,X94),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.13  cnf(c790,plain,in(skolem0002,skolem0001)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(X700)|~way(X700)|~lonely(X700)|~chevy(X701)|~car(X701)|~white(X701)|~dirty(X701)|~old(X701)|~barrel(skolem0006,X701)|~down(skolem0006,X700),inference(resolution,[status(thm)],[c216, c215])).
% 3.96/4.13  cnf(c2797,plain,in(skolem0002,skolem0001)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(X704)|~car(X704)|~white(X704)|~dirty(X704)|~old(X704)|~barrel(skolem0006,X704),inference(resolution,[status(thm)],[c790, c214])).
% 3.96/4.14  cnf(c2798,plain,in(skolem0002,skolem0001)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007)|~dirty(skolem0007)|~old(skolem0007),inference(resolution,[status(thm)],[c2797, c213])).
% 3.96/4.14  cnf(c2799,plain,in(skolem0002,skolem0001)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007)|~dirty(skolem0007),inference(resolution,[status(thm)],[c2798, c2701])).
% 3.96/4.14  cnf(c2800,plain,in(skolem0002,skolem0001)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007)|~white(skolem0007),inference(resolution,[status(thm)],[c2799, c2676])).
% 3.96/4.14  cnf(c2801,plain,in(skolem0002,skolem0001)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007)|~car(skolem0007),inference(resolution,[status(thm)],[c2800, c2649])).
% 3.96/4.14  cnf(c2802,plain,in(skolem0002,skolem0001)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008)|~chevy(skolem0007),inference(resolution,[status(thm)],[c2801, c2620])).
% 3.96/4.14  cnf(c2803,plain,in(skolem0002,skolem0001)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008)|~lonely(skolem0008),inference(resolution,[status(thm)],[c2802, c2589])).
% 3.96/4.14  cnf(c2804,plain,in(skolem0002,skolem0001)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008)|~way(skolem0008),inference(resolution,[status(thm)],[c2803, c2764])).
% 3.96/4.14  cnf(c2805,plain,in(skolem0002,skolem0001)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006)|~street(skolem0008),inference(resolution,[status(thm)],[c2804, c2745])).
% 3.96/4.14  cnf(c2806,plain,in(skolem0002,skolem0001)|~hollywood(skolem0005)|~city(skolem0005)|~event(skolem0006),inference(resolution,[status(thm)],[c2805, c2724])).
% 3.96/4.14  cnf(c2807,plain,in(skolem0002,skolem0001)|~hollywood(skolem0005)|~city(skolem0005),inference(resolution,[status(thm)],[c2806, c2556])).
% 3.96/4.14  cnf(c2808,plain,in(skolem0002,skolem0001)|~hollywood(skolem0005),inference(resolution,[status(thm)],[c2807, c2521])).
% 3.96/4.14  cnf(c2809,plain,in(skolem0002,skolem0001),inference(resolution,[status(thm)],[c2808, c2484])).
% 3.96/4.14  cnf(c231,negated_conjecture,~hollywood(X138)|~city(X138)|~event(X137)|~chevy(X140)|~car(X140)|~white(X140)|~dirty(X140)|~old(X140)|~street(X136)|~way(X136)|~lonely(X136)|~barrel(X137,X140)|~down(X137,X136)|~in(X137,X138)|~hollywood(X135)|~city(X135)|~event(X133)|~street(X134)|~way(X134)|~lonely(X134)|~chevy(X139)|~car(X139)|~white(X139)|~dirty(X139)|~old(X139)|~barrel(X133,X139)|~down(X133,X134)|~in(X133,X135),inference(split_conjunct,[status(thm)],[c6])).
% 3.96/4.14  cnf(c1198,plain,~hollywood(X1976)|~city(X1976)|~event(X1981)|~chevy(X1978)|~car(X1978)|~white(X1978)|~dirty(X1978)|~old(X1978)|~street(X1980)|~way(X1980)|~lonely(X1980)|~barrel(X1981,X1978)|~down(X1981,X1980)|~in(X1981,X1976)|~street(X1979)|~way(X1979)|~lonely(X1979)|~chevy(X1977)|~car(X1977)|~white(X1977)|~dirty(X1977)|~old(X1977)|~barrel(X1981,X1977)|~down(X1981,X1979),inference(factor,[status(thm)],[c231])).
% 3.96/4.14  cnf(c2854,plain,~hollywood(X2067)|~city(X2067)|~event(X2069)|~chevy(X2071)|~car(X2071)|~white(X2071)|~dirty(X2071)|~old(X2071)|~street(X2070)|~way(X2070)|~lonely(X2070)|~barrel(X2069,X2071)|~down(X2069,X2070)|~in(X2069,X2067)|~chevy(X2068)|~car(X2068)|~white(X2068)|~dirty(X2068)|~old(X2068)|~barrel(X2069,X2068),inference(factor,[status(thm)],[c1198])).
% 3.96/4.14  cnf(c2857,plain,~hollywood(X2074)|~city(X2074)|~event(X2075)|~chevy(X2073)|~car(X2073)|~white(X2073)|~dirty(X2073)|~old(X2073)|~street(X2072)|~way(X2072)|~lonely(X2072)|~barrel(X2075,X2073)|~down(X2075,X2072)|~in(X2075,X2074),inference(factor,[status(thm)],[c2854])).
% 3.96/4.14  cnf(c2860,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(X2077)|~car(X2077)|~white(X2077)|~dirty(X2077)|~old(X2077)|~street(X2076)|~way(X2076)|~lonely(X2076)|~barrel(skolem0002,X2077)|~down(skolem0002,X2076),inference(resolution,[status(thm)],[c2857, c2809])).
% 3.96/4.14  cnf(c2862,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(X2078)|~car(X2078)|~white(X2078)|~dirty(X2078)|~old(X2078)|~street(skolem0003)|~way(skolem0003)|~lonely(skolem0003)|~barrel(skolem0002,X2078),inference(resolution,[status(thm)],[c2860, c2796])).
% 3.96/4.14  cnf(c2863,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003)|~way(skolem0003)|~lonely(skolem0003),inference(resolution,[status(thm)],[c2862, c2781])).
% 3.96/4.14  cnf(c2864,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003)|~way(skolem0003),inference(resolution,[status(thm)],[c2863, c2110])).
% 3.96/4.14  cnf(c2865,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004)|~street(skolem0003),inference(resolution,[status(thm)],[c2864, c1951])).
% 3.96/4.14  cnf(c2866,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004)|~old(skolem0004),inference(resolution,[status(thm)],[c2865, c1774])).
% 3.96/4.14  cnf(c2867,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004)|~dirty(skolem0004),inference(resolution,[status(thm)],[c2866, c2442])).
% 3.96/4.14  cnf(c2868,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004)|~white(skolem0004),inference(resolution,[status(thm)],[c2867, c2398])).
% 3.96/4.14  cnf(c2869,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004)|~car(skolem0004),inference(resolution,[status(thm)],[c2868, c2341])).
% 3.96/4.14  cnf(c2870,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002)|~chevy(skolem0004),inference(resolution,[status(thm)],[c2869, c2277])).
% 3.96/4.14  cnf(c2871,plain,~hollywood(skolem0001)|~city(skolem0001)|~event(skolem0002),inference(resolution,[status(thm)],[c2870, c2197])).
% 3.96/4.14  cnf(c2872,plain,~hollywood(skolem0001)|~city(skolem0001),inference(resolution,[status(thm)],[c2871, c1640])).
% 3.96/4.14  cnf(c2873,plain,~hollywood(skolem0001),inference(resolution,[status(thm)],[c2872, c1471])).
% 3.96/4.14  cnf(c2874,plain,$false,inference(resolution,[status(thm)],[c2873, c1190])).
% 3.96/4.14  % SZS output end CNFRefutation
% 3.96/4.14  
% 3.96/4.14  % Initial clauses    : 225
% 3.96/4.14  % Processed clauses  : 639
% 3.96/4.14  % Factors computed   : 3
% 3.96/4.14  % Resolvents computed: 2640
% 3.96/4.14  % Tautologies deleted: 84
% 3.96/4.14  % Forward subsumed   : 2121
% 3.96/4.14  % Backward subsumed  : 609
% 3.96/4.14  % -------- CPU Time ---------
% 3.96/4.14  % User time          : 3.772 s
% 3.96/4.14  % System time        : 0.029 s
% 3.96/4.14  % Total time         : 3.801 s
%------------------------------------------------------------------------------