%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP155+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:34:26 EDT 2024
% Result : CounterSatisfiable 0.66s 0.92s
% Output : Saturation 0.76s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : NLP155+1 : TPTP v8.1.2. Released v2.4.0.
% 0.06/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.11/0.33 % Computer : n010.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Wed May 8 13:37:23 EDT 2024
% 0.11/0.33 % CPUTime :
% 0.66/0.92 % Version: 1.5
% 0.66/0.92 % SZS status CounterSatisfiable
% 0.66/0.92 % SZS output start Saturation
% 0.66/0.92 fof(co1,conjecture,(~((?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(((((((((((((((of(U,W,V)&city(U,V))&hollywood_placename(U,W))&placename(U,W))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&street(U,Y))&lonely(U,Y))&event(U,Z))&agent(U,Z,X))&present(U,Z))&barrel(U,Z))&down(U,Z,Y))&in(U,Z,V)))))))))&(~(?[X1]:(actual_world(X1)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X2]:(((((((((((((((((((of(X1,W,V)&city(X1,V))&hollywood_placename(X1,W))&placename(X1,W))&chevy(X1,X))&white(X1,X))&dirty(X1,X))&old(X1,X))&street(X1,Y))&lonely(X1,Y))&event(X1,Z))&agent(X1,Z,X))&present(X1,Z))&barrel(X1,Z))&down(X1,Z,Y))&in(X1,Z,V))&(![X3]:(member(X1,X3,X2)=>(?[X4]:(?[X5]:(((frontseat(X1,X5)&state(X1,X4))&be(X1,X4,X3,X5))&in(X1,X5,X5)))))))&two(X1,X2))&group(X1,X2))&(![X6]:(member(X1,X6,X2)=>(fellow(X1,X6)&young(X1,X6)))))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1)).
% 0.66/0.92 fof(c59,negated_conjecture,(~(~((?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(((((((((((((((of(U,W,V)&city(U,V))&hollywood_placename(U,W))&placename(U,W))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&street(U,Y))&lonely(U,Y))&event(U,Z))&agent(U,Z,X))&present(U,Z))&barrel(U,Z))&down(U,Z,Y))&in(U,Z,V)))))))))&(~(?[X1]:(actual_world(X1)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(?[X2]:(((((((((((((((((((of(X1,W,V)&city(X1,V))&hollywood_placename(X1,W))&placename(X1,W))&chevy(X1,X))&white(X1,X))&dirty(X1,X))&old(X1,X))&street(X1,Y))&lonely(X1,Y))&event(X1,Z))&agent(X1,Z,X))&present(X1,Z))&barrel(X1,Z))&down(X1,Z,Y))&in(X1,Z,V))&(![X3]:(member(X1,X3,X2)=>(?[X4]:(?[X5]:(((frontseat(X1,X5)&state(X1,X4))&be(X1,X4,X3,X5))&in(X1,X5,X5)))))))&two(X1,X2))&group(X1,X2))&(![X6]:(member(X1,X6,X2)=>(fellow(X1,X6)&young(X1,X6))))))))))))))))),inference(assume_negation,[status(cth)],[co1])).
% 0.66/0.92 fof(c60,negated_conjecture,((?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:(?[Z]:(((((((((((((((of(U,W,V)&city(U,V))&hollywood_placename(U,W))&placename(U,W))&chevy(U,X))&white(U,X))&dirty(U,X))&old(U,X))&street(U,Y))&lonely(U,Y))&event(U,Z))&agent(U,Z,X))&present(U,Z))&barrel(U,Z))&down(U,Z,Y))&in(U,Z,V)))))))))&(![X1]:(~actual_world(X1)|(![V]:(![W]:(![X]:(![Y]:(![Z]:(![X2]:(((((((((((((((((((~of(X1,W,V)|~city(X1,V))|~hollywood_placename(X1,W))|~placename(X1,W))|~chevy(X1,X))|~white(X1,X))|~dirty(X1,X))|~old(X1,X))|~street(X1,Y))|~lonely(X1,Y))|~event(X1,Z))|~agent(X1,Z,X))|~present(X1,Z))|~barrel(X1,Z))|~down(X1,Z,Y))|~in(X1,Z,V))|(?[X3]:(member(X1,X3,X2)&(![X4]:(![X5]:(((~frontseat(X1,X5)|~state(X1,X4))|~be(X1,X4,X3,X5))|~in(X1,X5,X5)))))))|~two(X1,X2))|~group(X1,X2))|(?[X6]:(member(X1,X6,X2)&(~fellow(X1,X6)|~young(X1,X6)))))))))))))),inference(fof_nnf,[status(thm)],[c59])).
% 0.66/0.92 fof(c61,negated_conjecture,((?[X2]:(actual_world(X2)&(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(((((((((((((((of(X2,X4,X3)&city(X2,X3))&hollywood_placename(X2,X4))&placename(X2,X4))&chevy(X2,X5))&white(X2,X5))&dirty(X2,X5))&old(X2,X5))&street(X2,X6))&lonely(X2,X6))&event(X2,X7))&agent(X2,X7,X5))&present(X2,X7))&barrel(X2,X7))&down(X2,X7,X6))&in(X2,X7,X3)))))))))&(![X8]:(~actual_world(X8)|(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(((((((((((((((((((~of(X8,X10,X9)|~city(X8,X9))|~hollywood_placename(X8,X10))|~placename(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~street(X8,X12))|~lonely(X8,X12))|~event(X8,X13))|~agent(X8,X13,X11))|~present(X8,X13))|~barrel(X8,X13))|~down(X8,X13,X12))|~in(X8,X13,X9))|(?[X15]:(member(X8,X15,X14)&(![X16]:(![X17]:(((~frontseat(X8,X17)|~state(X8,X16))|~be(X8,X16,X15,X17))|~in(X8,X17,X17)))))))|~two(X8,X14))|~group(X8,X14))|(?[X18]:(member(X8,X18,X14)&(~fellow(X8,X18)|~young(X8,X18)))))))))))))),inference(variable_rename,[status(thm)],[c60])).
% 0.66/0.92 fof(c63,negated_conjecture,(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(![X16]:(![X17]:((actual_world(skolem0001)&(((((((((((((((of(skolem0001,skolem0003,skolem0002)&city(skolem0001,skolem0002))&hollywood_placename(skolem0001,skolem0003))&placename(skolem0001,skolem0003))&chevy(skolem0001,skolem0004))&white(skolem0001,skolem0004))&dirty(skolem0001,skolem0004))&old(skolem0001,skolem0004))&street(skolem0001,skolem0005))&lonely(skolem0001,skolem0005))&event(skolem0001,skolem0006))&agent(skolem0001,skolem0006,skolem0004))&present(skolem0001,skolem0006))&barrel(skolem0001,skolem0006))&down(skolem0001,skolem0006,skolem0005))&in(skolem0001,skolem0006,skolem0002)))&(~actual_world(X8)|(((((((((((((((((((~of(X8,X10,X9)|~city(X8,X9))|~hollywood_placename(X8,X10))|~placename(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~street(X8,X12))|~lonely(X8,X12))|~event(X8,X13))|~agent(X8,X13,X11))|~present(X8,X13))|~barrel(X8,X13))|~down(X8,X13,X12))|~in(X8,X13,X9))|(member(X8,skolem0007(X8,X9,X10,X11,X12,X13,X14),X14)&(((~frontseat(X8,X17)|~state(X8,X16))|~be(X8,X16,skolem0007(X8,X9,X10,X11,X12,X13,X14),X17))|~in(X8,X17,X17))))|~two(X8,X14))|~group(X8,X14))|(member(X8,skolem0008(X8,X9,X10,X11,X12,X13,X14),X14)&(~fellow(X8,skolem0008(X8,X9,X10,X11,X12,X13,X14))|~young(X8,skolem0008(X8,X9,X10,X11,X12,X13,X14)))))))))))))))),inference(shift_quantors,[status(thm)],[fof(c62,negated_conjecture,((actual_world(skolem0001)&(((((((((((((((of(skolem0001,skolem0003,skolem0002)&city(skolem0001,skolem0002))&hollywood_placename(skolem0001,skolem0003))&placename(skolem0001,skolem0003))&chevy(skolem0001,skolem0004))&white(skolem0001,skolem0004))&dirty(skolem0001,skolem0004))&old(skolem0001,skolem0004))&street(skolem0001,skolem0005))&lonely(skolem0001,skolem0005))&event(skolem0001,skolem0006))&agent(skolem0001,skolem0006,skolem0004))&present(skolem0001,skolem0006))&barrel(skolem0001,skolem0006))&down(skolem0001,skolem0006,skolem0005))&in(skolem0001,skolem0006,skolem0002)))&(![X8]:(~actual_world(X8)|(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(((((((((((((((((((~of(X8,X10,X9)|~city(X8,X9))|~hollywood_placename(X8,X10))|~placename(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~street(X8,X12))|~lonely(X8,X12))|~event(X8,X13))|~agent(X8,X13,X11))|~present(X8,X13))|~barrel(X8,X13))|~down(X8,X13,X12))|~in(X8,X13,X9))|(member(X8,skolem0007(X8,X9,X10,X11,X12,X13,X14),X14)&(![X16]:(![X17]:(((~frontseat(X8,X17)|~state(X8,X16))|~be(X8,X16,skolem0007(X8,X9,X10,X11,X12,X13,X14),X17))|~in(X8,X17,X17))))))|~two(X8,X14))|~group(X8,X14))|(member(X8,skolem0008(X8,X9,X10,X11,X12,X13,X14),X14)&(~fellow(X8,skolem0008(X8,X9,X10,X11,X12,X13,X14))|~young(X8,skolem0008(X8,X9,X10,X11,X12,X13,X14)))))))))))))),inference(skolemize,[status(esa)],[c61])).])).
% 0.66/0.92 fof(c64,negated_conjecture,(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(![X16]:(![X17]:((actual_world(skolem0001)&(((((((((((((((of(skolem0001,skolem0003,skolem0002)&city(skolem0001,skolem0002))&hollywood_placename(skolem0001,skolem0003))&placename(skolem0001,skolem0003))&chevy(skolem0001,skolem0004))&white(skolem0001,skolem0004))&dirty(skolem0001,skolem0004))&old(skolem0001,skolem0004))&street(skolem0001,skolem0005))&lonely(skolem0001,skolem0005))&event(skolem0001,skolem0006))&agent(skolem0001,skolem0006,skolem0004))&present(skolem0001,skolem0006))&barrel(skolem0001,skolem0006))&down(skolem0001,skolem0006,skolem0005))&in(skolem0001,skolem0006,skolem0002)))&(((~actual_world(X8)|(((((((((((((((((((~of(X8,X10,X9)|~city(X8,X9))|~hollywood_placename(X8,X10))|~placename(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~street(X8,X12))|~lonely(X8,X12))|~event(X8,X13))|~agent(X8,X13,X11))|~present(X8,X13))|~barrel(X8,X13))|~down(X8,X13,X12))|~in(X8,X13,X9))|member(X8,skolem0007(X8,X9,X10,X11,X12,X13,X14),X14))|~two(X8,X14))|~group(X8,X14))|member(X8,skolem0008(X8,X9,X10,X11,X12,X13,X14),X14)))&(~actual_world(X8)|(((((((((((((((((((~of(X8,X10,X9)|~city(X8,X9))|~hollywood_placename(X8,X10))|~placename(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~street(X8,X12))|~lonely(X8,X12))|~event(X8,X13))|~agent(X8,X13,X11))|~present(X8,X13))|~barrel(X8,X13))|~down(X8,X13,X12))|~in(X8,X13,X9))|member(X8,skolem0007(X8,X9,X10,X11,X12,X13,X14),X14))|~two(X8,X14))|~group(X8,X14))|(~fellow(X8,skolem0008(X8,X9,X10,X11,X12,X13,X14))|~young(X8,skolem0008(X8,X9,X10,X11,X12,X13,X14))))))&((~actual_world(X8)|(((((((((((((((((((~of(X8,X10,X9)|~city(X8,X9))|~hollywood_placename(X8,X10))|~placename(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~street(X8,X12))|~lonely(X8,X12))|~event(X8,X13))|~agent(X8,X13,X11))|~present(X8,X13))|~barrel(X8,X13))|~down(X8,X13,X12))|~in(X8,X13,X9))|(((~frontseat(X8,X17)|~state(X8,X16))|~be(X8,X16,skolem0007(X8,X9,X10,X11,X12,X13,X14),X17))|~in(X8,X17,X17)))|~two(X8,X14))|~group(X8,X14))|member(X8,skolem0008(X8,X9,X10,X11,X12,X13,X14),X14)))&(~actual_world(X8)|(((((((((((((((((((~of(X8,X10,X9)|~city(X8,X9))|~hollywood_placename(X8,X10))|~placename(X8,X10))|~chevy(X8,X11))|~white(X8,X11))|~dirty(X8,X11))|~old(X8,X11))|~street(X8,X12))|~lonely(X8,X12))|~event(X8,X13))|~agent(X8,X13,X11))|~present(X8,X13))|~barrel(X8,X13))|~down(X8,X13,X12))|~in(X8,X13,X9))|(((~frontseat(X8,X17)|~state(X8,X16))|~be(X8,X16,skolem0007(X8,X9,X10,X11,X12,X13,X14),X17))|~in(X8,X17,X17)))|~two(X8,X14))|~group(X8,X14))|(~fellow(X8,skolem0008(X8,X9,X10,X11,X12,X13,X14))|~young(X8,skolem0008(X8,X9,X10,X11,X12,X13,X14))))))))))))))))),inference(distribute,[status(thm)],[c63])).
% 0.66/0.92 cnf(c66,negated_conjecture,of(skolem0001,skolem0003,skolem0002),inference(split_conjunct,[status(thm)],[c64])).
% 0.66/0.92 cnf(c77,negated_conjecture,agent(skolem0001,skolem0006,skolem0004),inference(split_conjunct,[status(thm)],[c64])).
% 0.66/0.92 cnf(c80,negated_conjecture,down(skolem0001,skolem0006,skolem0005),inference(split_conjunct,[status(thm)],[c64])).
% 0.66/0.92 cnf(c81,negated_conjecture,in(skolem0001,skolem0006,skolem0002),inference(split_conjunct,[status(thm)],[c64])).
% 0.66/0.92 cnf(c82,negated_conjecture,~actual_world(X706)|~of(X706,X708,X703)|~city(X706,X703)|~hollywood_placename(X706,X708)|~placename(X706,X708)|~chevy(X706,X704)|~white(X706,X704)|~dirty(X706,X704)|~old(X706,X704)|~street(X706,X702)|~lonely(X706,X702)|~event(X706,X705)|~agent(X706,X705,X704)|~present(X706,X705)|~barrel(X706,X705)|~down(X706,X705,X702)|~in(X706,X705,X703)|member(X706,skolem0007(X706,X703,X708,X704,X702,X705,X707),X707)|~two(X706,X707)|~group(X706,X707)|member(X706,skolem0008(X706,X703,X708,X704,X702,X705,X707),X707),inference(split_conjunct,[status(thm)],[c64])).
% 0.66/0.92 cnf(c523,plain,~actual_world(skolem0001)|~of(skolem0001,X805,skolem0002)|~city(skolem0001,skolem0002)|~hollywood_placename(skolem0001,X805)|~placename(skolem0001,X805)|~chevy(skolem0001,X803)|~white(skolem0001,X803)|~dirty(skolem0001,X803)|~old(skolem0001,X803)|~street(skolem0001,X804)|~lonely(skolem0001,X804)|~event(skolem0001,skolem0006)|~agent(skolem0001,skolem0006,X803)|~present(skolem0001,skolem0006)|~barrel(skolem0001,skolem0006)|~down(skolem0001,skolem0006,X804)|member(skolem0001,skolem0007(skolem0001,skolem0002,X805,X803,X804,skolem0006,X806),X806)|~two(skolem0001,X806)|~group(skolem0001,X806)|member(skolem0001,skolem0008(skolem0001,skolem0002,X805,X803,X804,skolem0006,X806),X806),inference(resolution,[status(thm)],[c82, c81])).
% 0.66/0.92 cnf(c553,plain,~actual_world(skolem0001)|~of(skolem0001,X809,skolem0002)|~city(skolem0001,skolem0002)|~hollywood_placename(skolem0001,X809)|~placename(skolem0001,X809)|~chevy(skolem0001,X807)|~white(skolem0001,X807)|~dirty(skolem0001,X807)|~old(skolem0001,X807)|~street(skolem0001,skolem0005)|~lonely(skolem0001,skolem0005)|~event(skolem0001,skolem0006)|~agent(skolem0001,skolem0006,X807)|~present(skolem0001,skolem0006)|~barrel(skolem0001,skolem0006)|member(skolem0001,skolem0007(skolem0001,skolem0002,X809,X807,skolem0005,skolem0006,X808),X808)|~two(skolem0001,X808)|~group(skolem0001,X808)|member(skolem0001,skolem0008(skolem0001,skolem0002,X809,X807,skolem0005,skolem0006,X808),X808),inference(resolution,[status(thm)],[c523, c80])).
% 0.66/0.92 cnf(c554,plain,~actual_world(skolem0001)|~of(skolem0001,X811,skolem0002)|~city(skolem0001,skolem0002)|~hollywood_placename(skolem0001,X811)|~placename(skolem0001,X811)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~street(skolem0001,skolem0005)|~lonely(skolem0001,skolem0005)|~event(skolem0001,skolem0006)|~present(skolem0001,skolem0006)|~barrel(skolem0001,skolem0006)|member(skolem0001,skolem0007(skolem0001,skolem0002,X811,skolem0004,skolem0005,skolem0006,X810),X810)|~two(skolem0001,X810)|~group(skolem0001,X810)|member(skolem0001,skolem0008(skolem0001,skolem0002,X811,skolem0004,skolem0005,skolem0006,X810),X810),inference(resolution,[status(thm)],[c553, c77])).
% 0.66/0.92 cnf(c555,plain,~actual_world(skolem0001)|~city(skolem0001,skolem0002)|~hollywood_placename(skolem0001,skolem0003)|~placename(skolem0001,skolem0003)|~chevy(skolem0001,skolem0004)|~white(skolem0001,skolem0004)|~dirty(skolem0001,skolem0004)|~old(skolem0001,skolem0004)|~street(skolem0001,skolem0005)|~lonely(skolem0001,skolem0005)|~event(skolem0001,skolem0006)|~present(skolem0001,skolem0006)|~barrel(skolem0001,skolem0006)|member(skolem0001,skolem0007(skolem0001,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,X812),X812)|~two(skolem0001,X812)|~group(skolem0001,X812)|member(skolem0001,skolem0008(skolem0001,skolem0002,skolem0003,skolem0004,skolem0005,skolem0006,X812),X812),inference(resolution,[status(thm)],[c554, c66])).
% 0.66/0.92 fof(ax58,axiom,(![U]:(![V]:(![W]:(((entity(U,V)&placename(U,W))&of(U,W,V))=>(~(?[X]:((placename(U,X)&X!=W)&of(U,X,V)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax58)).
% 0.66/0.92 fof(c105,plain,(![U]:(![V]:(![W]:(((~entity(U,V)|~placename(U,W))|~of(U,W,V))|(![X]:((~placename(U,X)|X=W)|~of(U,X,V))))))),inference(fof_nnf,[status(thm)],[ax58])).
% 0.66/0.92 fof(c107,plain,(![X35]:(![X36]:(![X37]:(![X38]:(((~entity(X35,X36)|~placename(X35,X37))|~of(X35,X37,X36))|((~placename(X35,X38)|X38=X37)|~of(X35,X38,X36))))))),inference(shift_quantors,[status(thm)],[fof(c106,plain,(![X35]:(![X36]:(![X37]:(((~entity(X35,X36)|~placename(X35,X37))|~of(X35,X37,X36))|(![X38]:((~placename(X35,X38)|X38=X37)|~of(X35,X38,X36))))))),inference(variable_rename,[status(thm)],[c105])).])).
% 0.66/0.92 cnf(c108,plain,~entity(X797,X795)|~placename(X797,X798)|~of(X797,X798,X795)|~placename(X797,X796)|X796=X798|~of(X797,X796,X795),inference(split_conjunct,[status(thm)],[c107])).
% 0.66/0.92 cnf(c551,plain,~entity(skolem0001,skolem0002)|~placename(skolem0001,X802)|~of(skolem0001,X802,skolem0002)|~placename(skolem0001,skolem0003)|skolem0003=X802,inference(resolution,[status(thm)],[c108, c66])).
% 0.66/0.92 fof(ax60,axiom,(![U]:(![V]:(two(U,V)<=>(?[W]:(member(U,W,V)&(?[X]:((member(U,X,V)&X!=W)&(![Y]:(member(U,Y,V)=>(Y=X|Y=W)))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax60)).
% 0.66/0.92 fof(c89,plain,(![U]:(![V]:((~two(U,V)|(?[W]:(member(U,W,V)&(?[X]:((member(U,X,V)&X!=W)&(![Y]:(~member(U,Y,V)|(Y=X|Y=W))))))))&((![W]:(~member(U,W,V)|(![X]:((~member(U,X,V)|X=W)|(?[Y]:(member(U,Y,V)&(Y!=X&Y!=W)))))))|two(U,V))))),inference(fof_nnf,[status(thm)],[ax60])).
% 0.66/0.92 fof(c90,plain,((![U]:(![V]:(~two(U,V)|(?[W]:(member(U,W,V)&(?[X]:((member(U,X,V)&X!=W)&(![Y]:(~member(U,Y,V)|(Y=X|Y=W))))))))))&(![U]:(![V]:((![W]:(~member(U,W,V)|(![X]:((~member(U,X,V)|X=W)|(?[Y]:(member(U,Y,V)&(Y!=X&Y!=W)))))))|two(U,V))))),inference(shift_quantors,[status(thm)],[c89])).
% 0.66/0.92 fof(c91,plain,((![X21]:(![X22]:(~two(X21,X22)|(?[X23]:(member(X21,X23,X22)&(?[X24]:((member(X21,X24,X22)&X24!=X23)&(![X25]:(~member(X21,X25,X22)|(X25=X24|X25=X23))))))))))&(![X26]:(![X27]:((![X28]:(~member(X26,X28,X27)|(![X29]:((~member(X26,X29,X27)|X29=X28)|(?[X30]:(member(X26,X30,X27)&(X30!=X29&X30!=X28)))))))|two(X26,X27))))),inference(variable_rename,[status(thm)],[c90])).
% 0.66/0.92 fof(c93,plain,(![X21]:(![X22]:(![X25]:(![X26]:(![X27]:(![X28]:(![X29]:((~two(X21,X22)|(member(X21,skolem0009(X21,X22),X22)&((member(X21,skolem0010(X21,X22),X22)&skolem0010(X21,X22)!=skolem0009(X21,X22))&(~member(X21,X25,X22)|(X25=skolem0010(X21,X22)|X25=skolem0009(X21,X22))))))&((~member(X26,X28,X27)|((~member(X26,X29,X27)|X29=X28)|(member(X26,skolem0011(X26,X27,X28,X29),X27)&(skolem0011(X26,X27,X28,X29)!=X29&skolem0011(X26,X27,X28,X29)!=X28))))|two(X26,X27)))))))))),inference(shift_quantors,[status(thm)],[fof(c92,plain,((![X21]:(![X22]:(~two(X21,X22)|(member(X21,skolem0009(X21,X22),X22)&((member(X21,skolem0010(X21,X22),X22)&skolem0010(X21,X22)!=skolem0009(X21,X22))&(![X25]:(~member(X21,X25,X22)|(X25=skolem0010(X21,X22)|X25=skolem0009(X21,X22)))))))))&(![X26]:(![X27]:((![X28]:(~member(X26,X28,X27)|(![X29]:((~member(X26,X29,X27)|X29=X28)|(member(X26,skolem0011(X26,X27,X28,X29),X27)&(skolem0011(X26,X27,X28,X29)!=X29&skolem0011(X26,X27,X28,X29)!=X28))))))|two(X26,X27))))),inference(skolemize,[status(esa)],[c91])).])).
% 0.66/0.92 fof(c94,plain,(![X21]:(![X22]:(![X25]:(![X26]:(![X27]:(![X28]:(![X29]:(((~two(X21,X22)|member(X21,skolem0009(X21,X22),X22))&(((~two(X21,X22)|member(X21,skolem0010(X21,X22),X22))&(~two(X21,X22)|skolem0010(X21,X22)!=skolem0009(X21,X22)))&(~two(X21,X22)|(~member(X21,X25,X22)|(X25=skolem0010(X21,X22)|X25=skolem0009(X21,X22))))))&(((~member(X26,X28,X27)|((~member(X26,X29,X27)|X29=X28)|member(X26,skolem0011(X26,X27,X28,X29),X27)))|two(X26,X27))&(((~member(X26,X28,X27)|((~member(X26,X29,X27)|X29=X28)|skolem0011(X26,X27,X28,X29)!=X29))|two(X26,X27))&((~member(X26,X28,X27)|((~member(X26,X29,X27)|X29=X28)|skolem0011(X26,X27,X28,X29)!=X28))|two(X26,X27)))))))))))),inference(distribute,[status(thm)],[c93])).
% 0.66/0.92 cnf(c101,plain,~member(X788,X790,X791)|~member(X788,X789,X791)|X789=X790|skolem0011(X788,X791,X790,X789)!=X790|two(X788,X791),inference(split_conjunct,[status(thm)],[c94])).
% 0.66/0.92 cnf(reflexivity,axiom,X153=X153,theory(equality)).
% 0.66/0.92 cnf(c55,axiom,X668!=X665|X669!=X666|X664!=X667|~agent(X668,X669,X664)|agent(X665,X666,X667),theory(equality)).
% 0.66/0.92 cnf(c506,plain,skolem0001!=X782|skolem0006!=X783|skolem0004!=X784|agent(X782,X783,X784),inference(resolution,[status(thm)],[c55, c77])).
% 0.66/0.92 cnf(c547,plain,skolem0001!=X786|skolem0006!=X785|agent(X786,X785,skolem0004),inference(resolution,[status(thm)],[c506, reflexivity])).
% 0.66/0.92 cnf(c548,plain,skolem0001!=X787|agent(X787,skolem0006,skolem0004),inference(resolution,[status(thm)],[c547, reflexivity])).
% 0.66/0.92 cnf(c53,axiom,X648!=X645|X649!=X646|X644!=X647|~down(X648,X649,X644)|down(X645,X646,X647),theory(equality)).
% 0.66/0.92 cnf(c497,plain,skolem0001!=X774|skolem0006!=X773|skolem0005!=X772|down(X774,X773,X772),inference(resolution,[status(thm)],[c53, c80])).
% 0.66/0.92 cnf(c544,plain,skolem0001!=X776|skolem0006!=X775|down(X776,X775,skolem0005),inference(resolution,[status(thm)],[c497, reflexivity])).
% 0.66/0.92 cnf(c545,plain,skolem0001!=X781|down(X781,skolem0006,skolem0005),inference(resolution,[status(thm)],[c544, reflexivity])).
% 0.66/0.92 cnf(c100,plain,~member(X777,X779,X780)|~member(X777,X778,X780)|X778=X779|skolem0011(X777,X780,X779,X778)!=X778|two(X777,X780),inference(split_conjunct,[status(thm)],[c94])).
% 0.66/0.92 cnf(c52,axiom,X637!=X634|X638!=X635|X633!=X636|~in(X637,X638,X633)|in(X634,X635,X636),theory(equality)).
% 0.66/0.92 cnf(c493,plain,skolem0001!=X763|skolem0006!=X762|skolem0002!=X764|in(X763,X762,X764),inference(resolution,[status(thm)],[c52, c81])).
% 0.66/0.92 cnf(c540,plain,skolem0001!=X770|skolem0006!=X769|in(X770,X769,skolem0002),inference(resolution,[status(thm)],[c493, reflexivity])).
% 0.66/0.92 cnf(c542,plain,skolem0001!=X771|in(X771,skolem0006,skolem0002),inference(resolution,[status(thm)],[c540, reflexivity])).
% 0.66/0.92 cnf(c99,plain,~member(X765,X767,X768)|~member(X765,X766,X768)|X766=X767|member(X765,skolem0011(X765,X768,X767,X766),X768)|two(X765,X768),inference(split_conjunct,[status(thm)],[c94])).
% 0.66/0.92 cnf(c48,axiom,X602!=X599|X603!=X600|X598!=X601|~of(X602,X603,X598)|of(X599,X600,X601),theory(equality)).
% 0.66/0.92 cnf(c482,plain,skolem0001!=X758|skolem0003!=X757|skolem0002!=X756|of(X758,X757,X756),inference(resolution,[status(thm)],[c48, c66])).
% 0.66/0.92 cnf(c537,plain,skolem0001!=X759|skolem0003!=X760|of(X759,X760,skolem0002),inference(resolution,[status(thm)],[c482, reflexivity])).
% 0.66/0.92 cnf(c538,plain,skolem0001!=X761|of(X761,skolem0003,skolem0002),inference(resolution,[status(thm)],[c537, reflexivity])).
% 0.66/0.92 cnf(c98,plain,~two(X753,X754)|~member(X753,X755,X754)|X755=skolem0010(X753,X754)|X755=skolem0009(X753,X754),inference(split_conjunct,[status(thm)],[c94])).
% 0.66/0.92 cnf(c71,negated_conjecture,white(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c64])).
% 0.66/0.92 cnf(c58,axiom,X694!=X696|X695!=X693|~white(X694,X695)|white(X696,X693),theory(equality)).
% 0.66/0.92 cnf(c519,plain,skolem0001!=X751|skolem0004!=X750|white(X751,X750),inference(resolution,[status(thm)],[c58, c71])).
% 0.66/0.92 cnf(c535,plain,skolem0001!=X752|white(X752,skolem0004),inference(resolution,[status(thm)],[c519, reflexivity])).
% 0.66/0.92 cnf(c72,negated_conjecture,dirty(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c64])).
% 0.66/0.92 cnf(c57,axiom,X684!=X686|X685!=X683|~dirty(X684,X685)|dirty(X686,X683),theory(equality)).
% 0.66/0.92 cnf(c514,plain,skolem0001!=X739|skolem0004!=X738|dirty(X739,X738),inference(resolution,[status(thm)],[c57, c72])).
% 0.66/0.92 cnf(c533,plain,skolem0001!=X749|dirty(X749,skolem0004),inference(resolution,[status(thm)],[c514, reflexivity])).
% 0.66/0.92 cnf(c85,negated_conjecture,~actual_world(X746)|~of(X746,X748,X741)|~city(X746,X741)|~hollywood_placename(X746,X748)|~placename(X746,X748)|~chevy(X746,X742)|~white(X746,X742)|~dirty(X746,X742)|~old(X746,X742)|~street(X746,X740)|~lonely(X746,X740)|~event(X746,X743)|~agent(X746,X743,X742)|~present(X746,X743)|~barrel(X746,X743)|~down(X746,X743,X740)|~in(X746,X743,X741)|~frontseat(X746,X744)|~state(X746,X745)|~be(X746,X745,skolem0007(X746,X741,X748,X742,X740,X743,X747),X744)|~in(X746,X744,X744)|~two(X746,X747)|~group(X746,X747)|~fellow(X746,skolem0008(X746,X741,X748,X742,X740,X743,X747))|~young(X746,skolem0008(X746,X741,X748,X742,X740,X743,X747)),inference(split_conjunct,[status(thm)],[c64])).
% 0.66/0.92 cnf(c75,negated_conjecture,lonely(skolem0001,skolem0005),inference(split_conjunct,[status(thm)],[c64])).
% 0.66/0.92 cnf(c56,axiom,X676!=X678|X677!=X675|~lonely(X676,X677)|lonely(X678,X675),theory(equality)).
% 0.66/0.92 cnf(c510,plain,skolem0001!=X736|skolem0005!=X735|lonely(X736,X735),inference(resolution,[status(thm)],[c56, c75])).
% 0.66/0.92 cnf(c531,plain,skolem0001!=X737|lonely(X737,skolem0005),inference(resolution,[status(thm)],[c510, reflexivity])).
% 0.66/0.92 cnf(c84,negated_conjecture,~actual_world(X732)|~of(X732,X734,X727)|~city(X732,X727)|~hollywood_placename(X732,X734)|~placename(X732,X734)|~chevy(X732,X728)|~white(X732,X728)|~dirty(X732,X728)|~old(X732,X728)|~street(X732,X726)|~lonely(X732,X726)|~event(X732,X729)|~agent(X732,X729,X728)|~present(X732,X729)|~barrel(X732,X729)|~down(X732,X729,X726)|~in(X732,X729,X727)|~frontseat(X732,X730)|~state(X732,X731)|~be(X732,X731,skolem0007(X732,X727,X734,X728,X726,X729,X733),X730)|~in(X732,X730,X730)|~two(X732,X733)|~group(X732,X733)|member(X732,skolem0008(X732,X727,X734,X728,X726,X729,X733),X733),inference(split_conjunct,[status(thm)],[c64])).
% 0.66/0.92 cnf(c78,negated_conjecture,present(skolem0001,skolem0006),inference(split_conjunct,[status(thm)],[c64])).
% 0.66/0.92 cnf(c54,axiom,X655!=X657|X656!=X654|~present(X655,X656)|present(X657,X654),theory(equality)).
% 0.66/0.92 cnf(c501,plain,skolem0001!=X723|skolem0006!=X724|present(X723,X724),inference(resolution,[status(thm)],[c54, c78])).
% 0.66/0.92 cnf(c529,plain,skolem0001!=X725|present(X725,skolem0006),inference(resolution,[status(thm)],[c501, reflexivity])).
% 0.66/0.92 cnf(c73,negated_conjecture,old(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c64])).
% 0.66/0.92 cnf(c47,axiom,X589!=X591|X590!=X588|~old(X589,X590)|old(X591,X588),theory(equality)).
% 0.66/0.92 cnf(c477,plain,skolem0001!=X721|skolem0004!=X720|old(X721,X720),inference(resolution,[status(thm)],[c47, c73])).
% 0.66/0.92 cnf(c527,plain,skolem0001!=X722|old(X722,skolem0004),inference(resolution,[status(thm)],[c477, reflexivity])).
% 0.66/0.92 cnf(c83,negated_conjecture,~actual_world(X717)|~of(X717,X719,X714)|~city(X717,X714)|~hollywood_placename(X717,X719)|~placename(X717,X719)|~chevy(X717,X715)|~white(X717,X715)|~dirty(X717,X715)|~old(X717,X715)|~street(X717,X713)|~lonely(X717,X713)|~event(X717,X716)|~agent(X717,X716,X715)|~present(X717,X716)|~barrel(X717,X716)|~down(X717,X716,X713)|~in(X717,X716,X714)|member(X717,skolem0007(X717,X714,X719,X715,X713,X716,X718),X718)|~two(X717,X718)|~group(X717,X718)|~fellow(X717,skolem0008(X717,X714,X719,X715,X713,X716,X718))|~young(X717,skolem0008(X717,X714,X719,X715,X713,X716,X718)),inference(split_conjunct,[status(thm)],[c64])).
% 0.66/0.92 fof(ax44,axiom,(![U]:(![V]:(thing(U,V)=>singleton(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax44)).
% 0.66/0.92 fof(c156,plain,(![U]:(![V]:(~thing(U,V)|singleton(U,V)))),inference(fof_nnf,[status(thm)],[ax44])).
% 0.66/0.92 fof(c157,plain,(![X65]:(![X66]:(~thing(X65,X66)|singleton(X65,X66)))),inference(variable_rename,[status(thm)],[c156])).
% 0.66/0.92 cnf(c158,plain,~thing(X205,X204)|singleton(X205,X204),inference(split_conjunct,[status(thm)],[c157])).
% 0.66/0.92 fof(ax45,axiom,(![U]:(![V]:(entity(U,V)=>thing(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax45)).
% 0.66/0.93 fof(c153,plain,(![U]:(![V]:(~entity(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax45])).
% 0.66/0.93 fof(c154,plain,(![X63]:(![X64]:(~entity(X63,X64)|thing(X63,X64)))),inference(variable_rename,[status(thm)],[c153])).
% 0.66/0.93 cnf(c155,plain,~entity(X202,X203)|thing(X202,X203),inference(split_conjunct,[status(thm)],[c154])).
% 0.66/0.93 fof(ax19,axiom,(![U]:(![V]:(object(U,V)=>entity(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax19)).
% 0.66/0.93 fof(c231,plain,(![U]:(![V]:(~object(U,V)|entity(U,V)))),inference(fof_nnf,[status(thm)],[ax19])).
% 0.66/0.93 fof(c232,plain,(![X115]:(![X116]:(~object(X115,X116)|entity(X115,X116)))),inference(variable_rename,[status(thm)],[c231])).
% 0.66/0.93 cnf(c233,plain,~object(X287,X286)|entity(X287,X286),inference(split_conjunct,[status(thm)],[c232])).
% 0.66/0.93 fof(ax20,axiom,(![U]:(![V]:(artifact(U,V)=>object(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax20)).
% 0.66/0.93 fof(c228,plain,(![U]:(![V]:(~artifact(U,V)|object(U,V)))),inference(fof_nnf,[status(thm)],[ax20])).
% 0.66/0.93 fof(c229,plain,(![X113]:(![X114]:(~artifact(X113,X114)|object(X113,X114)))),inference(variable_rename,[status(thm)],[c228])).
% 0.66/0.93 cnf(c230,plain,~artifact(X284,X285)|object(X284,X285),inference(split_conjunct,[status(thm)],[c229])).
% 0.66/0.93 cnf(c74,negated_conjecture,street(skolem0001,skolem0005),inference(split_conjunct,[status(thm)],[c64])).
% 0.66/0.93 fof(ax15,axiom,(![U]:(![V]:(street(U,V)=>way(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax15)).
% 0.66/0.93 fof(c243,plain,(![U]:(![V]:(~street(U,V)|way(U,V)))),inference(fof_nnf,[status(thm)],[ax15])).
% 0.66/0.93 fof(c244,plain,(![X123]:(![X124]:(~street(X123,X124)|way(X123,X124)))),inference(variable_rename,[status(thm)],[c243])).
% 0.66/0.93 cnf(c245,plain,~street(X306,X307)|way(X306,X307),inference(split_conjunct,[status(thm)],[c244])).
% 0.66/0.93 cnf(c324,plain,way(skolem0001,skolem0005),inference(resolution,[status(thm)],[c245, c74])).
% 0.66/0.93 fof(ax14,axiom,(![U]:(![V]:(way(U,V)=>artifact(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax14)).
% 0.66/0.93 fof(c246,plain,(![U]:(![V]:(~way(U,V)|artifact(U,V)))),inference(fof_nnf,[status(thm)],[ax14])).
% 0.66/0.93 fof(c247,plain,(![X125]:(![X126]:(~way(X125,X126)|artifact(X125,X126)))),inference(variable_rename,[status(thm)],[c246])).
% 0.66/0.93 cnf(c248,plain,~way(X309,X308)|artifact(X309,X308),inference(split_conjunct,[status(thm)],[c247])).
% 0.66/0.93 cnf(c325,plain,artifact(skolem0001,skolem0005),inference(resolution,[status(thm)],[c248, c324])).
% 0.66/0.93 cnf(c326,plain,object(skolem0001,skolem0005),inference(resolution,[status(thm)],[c325, c230])).
% 0.66/0.93 cnf(c328,plain,entity(skolem0001,skolem0005),inference(resolution,[status(thm)],[c326, c233])).
% 0.66/0.93 cnf(c334,plain,thing(skolem0001,skolem0005),inference(resolution,[status(thm)],[c328, c155])).
% 0.66/0.93 cnf(c339,plain,singleton(skolem0001,skolem0005),inference(resolution,[status(thm)],[c334, c158])).
% 0.66/0.93 cnf(c44,axiom,X562!=X564|X563!=X561|~singleton(X562,X563)|singleton(X564,X561),theory(equality)).
% 0.66/0.93 cnf(c466,plain,skolem0001!=X710|skolem0005!=X711|singleton(X710,X711),inference(resolution,[status(thm)],[c44, c339])).
% 0.66/0.93 cnf(c525,plain,skolem0001!=X712|singleton(X712,skolem0005),inference(resolution,[status(thm)],[c466, reflexivity])).
% 0.66/0.93 cnf(c70,negated_conjecture,chevy(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c64])).
% 0.66/0.93 fof(ax25,axiom,(![U]:(![V]:(chevy(U,V)=>car(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax25)).
% 0.66/0.93 fof(c213,plain,(![U]:(![V]:(~chevy(U,V)|car(U,V)))),inference(fof_nnf,[status(thm)],[ax25])).
% 0.66/0.93 fof(c214,plain,(![X103]:(![X104]:(~chevy(X103,X104)|car(X103,X104)))),inference(variable_rename,[status(thm)],[c213])).
% 0.66/0.93 cnf(c215,plain,~chevy(X266,X267)|car(X266,X267),inference(split_conjunct,[status(thm)],[c214])).
% 0.66/0.93 cnf(c303,plain,car(skolem0001,skolem0004),inference(resolution,[status(thm)],[c215, c70])).
% 0.66/0.93 fof(ax24,axiom,(![U]:(![V]:(car(U,V)=>vehicle(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax24)).
% 0.66/0.93 fof(c216,plain,(![U]:(![V]:(~car(U,V)|vehicle(U,V)))),inference(fof_nnf,[status(thm)],[ax24])).
% 0.66/0.93 fof(c217,plain,(![X105]:(![X106]:(~car(X105,X106)|vehicle(X105,X106)))),inference(variable_rename,[status(thm)],[c216])).
% 0.66/0.93 cnf(c218,plain,~car(X269,X268)|vehicle(X269,X268),inference(split_conjunct,[status(thm)],[c217])).
% 0.66/0.93 cnf(c304,plain,vehicle(skolem0001,skolem0004),inference(resolution,[status(thm)],[c218, c303])).
% 0.66/0.93 fof(ax23,axiom,(![U]:(![V]:(vehicle(U,V)=>transport(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax23)).
% 0.66/0.93 fof(c219,plain,(![U]:(![V]:(~vehicle(U,V)|transport(U,V)))),inference(fof_nnf,[status(thm)],[ax23])).
% 0.66/0.93 fof(c220,plain,(![X107]:(![X108]:(~vehicle(X107,X108)|transport(X107,X108)))),inference(variable_rename,[status(thm)],[c219])).
% 0.66/0.93 cnf(c221,plain,~vehicle(X274,X275)|transport(X274,X275),inference(split_conjunct,[status(thm)],[c220])).
% 0.66/0.93 cnf(c306,plain,transport(skolem0001,skolem0004),inference(resolution,[status(thm)],[c221, c304])).
% 0.66/0.93 fof(ax22,axiom,(![U]:(![V]:(transport(U,V)=>instrumentality(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax22)).
% 0.66/0.93 fof(c222,plain,(![U]:(![V]:(~transport(U,V)|instrumentality(U,V)))),inference(fof_nnf,[status(thm)],[ax22])).
% 0.66/0.93 fof(c223,plain,(![X109]:(![X110]:(~transport(X109,X110)|instrumentality(X109,X110)))),inference(variable_rename,[status(thm)],[c222])).
% 0.66/0.93 cnf(c224,plain,~transport(X276,X277)|instrumentality(X276,X277),inference(split_conjunct,[status(thm)],[c223])).
% 0.66/0.93 cnf(c307,plain,instrumentality(skolem0001,skolem0004),inference(resolution,[status(thm)],[c224, c306])).
% 0.66/0.93 fof(ax21,axiom,(![U]:(![V]:(instrumentality(U,V)=>artifact(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax21)).
% 0.66/0.93 fof(c225,plain,(![U]:(![V]:(~instrumentality(U,V)|artifact(U,V)))),inference(fof_nnf,[status(thm)],[ax21])).
% 0.66/0.93 fof(c226,plain,(![X111]:(![X112]:(~instrumentality(X111,X112)|artifact(X111,X112)))),inference(variable_rename,[status(thm)],[c225])).
% 0.66/0.93 cnf(c227,plain,~instrumentality(X279,X278)|artifact(X279,X278),inference(split_conjunct,[status(thm)],[c226])).
% 0.66/0.93 cnf(c309,plain,artifact(skolem0001,skolem0004),inference(resolution,[status(thm)],[c227, c307])).
% 0.66/0.93 cnf(c310,plain,object(skolem0001,skolem0004),inference(resolution,[status(thm)],[c230, c309])).
% 0.66/0.93 cnf(c312,plain,entity(skolem0001,skolem0004),inference(resolution,[status(thm)],[c233, c310])).
% 0.66/0.93 cnf(c314,plain,thing(skolem0001,skolem0004),inference(resolution,[status(thm)],[c312, c155])).
% 0.66/0.93 cnf(c316,plain,singleton(skolem0001,skolem0004),inference(resolution,[status(thm)],[c314, c158])).
% 0.66/0.93 cnf(c465,plain,skolem0001!=X700|skolem0004!=X701|singleton(X700,X701),inference(resolution,[status(thm)],[c44, c316])).
% 0.66/0.93 cnf(c522,plain,skolem0001!=X709|singleton(X709,skolem0004),inference(resolution,[status(thm)],[c465, reflexivity])).
% 0.66/0.93 fof(ax32,axiom,(![U]:(![V]:(eventuality(U,V)=>thing(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax32)).
% 0.66/0.93 fof(c192,plain,(![U]:(![V]:(~eventuality(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax32])).
% 0.66/0.93 fof(c193,plain,(![X89]:(![X90]:(~eventuality(X89,X90)|thing(X89,X90)))),inference(variable_rename,[status(thm)],[c192])).
% 0.66/0.93 cnf(c194,plain,~eventuality(X240,X241)|thing(X240,X241),inference(split_conjunct,[status(thm)],[c193])).
% 0.66/0.93 cnf(c76,negated_conjecture,event(skolem0001,skolem0006),inference(split_conjunct,[status(thm)],[c64])).
% 0.66/0.93 fof(ax27,axiom,(![U]:(![V]:(event(U,V)=>eventuality(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax27)).
% 0.66/0.93 fof(c207,plain,(![U]:(![V]:(~event(U,V)|eventuality(U,V)))),inference(fof_nnf,[status(thm)],[ax27])).
% 0.66/0.93 fof(c208,plain,(![X99]:(![X100]:(~event(X99,X100)|eventuality(X99,X100)))),inference(variable_rename,[status(thm)],[c207])).
% 0.66/0.93 cnf(c209,plain,~event(X254,X255)|eventuality(X254,X255),inference(split_conjunct,[status(thm)],[c208])).
% 0.66/0.93 cnf(c294,plain,eventuality(skolem0001,skolem0006),inference(resolution,[status(thm)],[c209, c76])).
% 0.66/0.93 cnf(c298,plain,thing(skolem0001,skolem0006),inference(resolution,[status(thm)],[c294, c194])).
% 0.66/0.93 cnf(c301,plain,singleton(skolem0001,skolem0006),inference(resolution,[status(thm)],[c298, c158])).
% 0.66/0.93 cnf(c464,plain,skolem0001!=X697|skolem0006!=X698|singleton(X697,X698),inference(resolution,[status(thm)],[c44, c301])).
% 0.66/0.93 cnf(c520,plain,skolem0001!=X699|singleton(X699,skolem0006),inference(resolution,[status(thm)],[c464, reflexivity])).
% 0.66/0.93 cnf(c67,negated_conjecture,city(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c64])).
% 0.66/0.93 fof(ax5,axiom,(![U]:(![V]:(city(U,V)=>location(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax5)).
% 0.66/0.93 fof(c273,plain,(![U]:(![V]:(~city(U,V)|location(U,V)))),inference(fof_nnf,[status(thm)],[ax5])).
% 0.66/0.93 fof(c274,plain,(![X143]:(![X144]:(~city(X143,X144)|location(X143,X144)))),inference(variable_rename,[status(thm)],[c273])).
% 0.66/0.93 cnf(c275,plain,~city(X350,X351)|location(X350,X351),inference(split_conjunct,[status(thm)],[c274])).
% 0.66/0.93 cnf(c364,plain,location(skolem0001,skolem0002),inference(resolution,[status(thm)],[c275, c67])).
% 0.66/0.93 fof(ax4,axiom,(![U]:(![V]:(location(U,V)=>object(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax4)).
% 0.66/0.93 fof(c276,plain,(![U]:(![V]:(~location(U,V)|object(U,V)))),inference(fof_nnf,[status(thm)],[ax4])).
% 0.66/0.93 fof(c277,plain,(![X145]:(![X146]:(~location(X145,X146)|object(X145,X146)))),inference(variable_rename,[status(thm)],[c276])).
% 0.66/0.93 cnf(c278,plain,~location(X356,X357)|object(X356,X357),inference(split_conjunct,[status(thm)],[c277])).
% 0.66/0.93 cnf(c368,plain,object(skolem0001,skolem0002),inference(resolution,[status(thm)],[c278, c364])).
% 0.76/0.93 cnf(c370,plain,entity(skolem0001,skolem0002),inference(resolution,[status(thm)],[c368, c233])).
% 0.76/0.93 cnf(c378,plain,thing(skolem0001,skolem0002),inference(resolution,[status(thm)],[c370, c155])).
% 0.76/0.93 cnf(c384,plain,singleton(skolem0001,skolem0002),inference(resolution,[status(thm)],[c378, c158])).
% 0.76/0.93 cnf(c463,plain,skolem0001!=X690|skolem0002!=X691|singleton(X690,X691),inference(resolution,[status(thm)],[c44, c384])).
% 0.76/0.93 cnf(c517,plain,skolem0001!=X692|singleton(X692,skolem0002),inference(resolution,[status(thm)],[c463, reflexivity])).
% 0.76/0.93 cnf(c69,negated_conjecture,placename(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c64])).
% 0.76/0.93 fof(ax13,axiom,(![U]:(![V]:(placename(U,V)=>relname(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax13)).
% 0.76/0.93 fof(c249,plain,(![U]:(![V]:(~placename(U,V)|relname(U,V)))),inference(fof_nnf,[status(thm)],[ax13])).
% 0.76/0.93 fof(c250,plain,(![X127]:(![X128]:(~placename(X127,X128)|relname(X127,X128)))),inference(variable_rename,[status(thm)],[c249])).
% 0.76/0.93 cnf(c251,plain,~placename(X323,X322)|relname(X323,X322),inference(split_conjunct,[status(thm)],[c250])).
% 0.76/0.93 cnf(c342,plain,relname(skolem0001,skolem0003),inference(resolution,[status(thm)],[c251, c69])).
% 0.76/0.93 fof(ax12,axiom,(![U]:(![V]:(relname(U,V)=>relation(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax12)).
% 0.76/0.93 fof(c252,plain,(![U]:(![V]:(~relname(U,V)|relation(U,V)))),inference(fof_nnf,[status(thm)],[ax12])).
% 0.76/0.93 fof(c253,plain,(![X129]:(![X130]:(~relname(X129,X130)|relation(X129,X130)))),inference(variable_rename,[status(thm)],[c252])).
% 0.76/0.93 cnf(c254,plain,~relname(X324,X325)|relation(X324,X325),inference(split_conjunct,[status(thm)],[c253])).
% 0.76/0.93 cnf(c344,plain,relation(skolem0001,skolem0003),inference(resolution,[status(thm)],[c254, c342])).
% 0.76/0.93 fof(ax11,axiom,(![U]:(![V]:(relation(U,V)=>abstraction(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax11)).
% 0.76/0.93 fof(c255,plain,(![U]:(![V]:(~relation(U,V)|abstraction(U,V)))),inference(fof_nnf,[status(thm)],[ax11])).
% 0.76/0.93 fof(c256,plain,(![X131]:(![X132]:(~relation(X131,X132)|abstraction(X131,X132)))),inference(variable_rename,[status(thm)],[c255])).
% 0.76/0.93 cnf(c257,plain,~relation(X326,X327)|abstraction(X326,X327),inference(split_conjunct,[status(thm)],[c256])).
% 0.76/0.93 cnf(c346,plain,abstraction(skolem0001,skolem0003),inference(resolution,[status(thm)],[c257, c344])).
% 0.76/0.93 fof(ax10,axiom,(![U]:(![V]:(abstraction(U,V)=>thing(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax10)).
% 0.76/0.93 fof(c258,plain,(![U]:(![V]:(~abstraction(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax10])).
% 0.76/0.93 fof(c259,plain,(![X133]:(![X134]:(~abstraction(X133,X134)|thing(X133,X134)))),inference(variable_rename,[status(thm)],[c258])).
% 0.76/0.93 cnf(c260,plain,~abstraction(X332,X333)|thing(X332,X333),inference(split_conjunct,[status(thm)],[c259])).
% 0.76/0.93 cnf(c349,plain,thing(skolem0001,skolem0003),inference(resolution,[status(thm)],[c260, c346])).
% 0.76/0.93 cnf(c351,plain,singleton(skolem0001,skolem0003),inference(resolution,[status(thm)],[c349, c158])).
% 0.76/0.93 cnf(c462,plain,skolem0001!=X687|skolem0003!=X688|singleton(X687,X688),inference(resolution,[status(thm)],[c44, c351])).
% 0.76/0.93 cnf(c515,plain,skolem0001!=X689|singleton(X689,skolem0003),inference(resolution,[status(thm)],[c462, reflexivity])).
% 0.76/0.93 fof(ax42,axiom,(![U]:(![V]:(entity(U,V)=>existent(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax42)).
% 0.76/0.93 fof(c162,plain,(![U]:(![V]:(~entity(U,V)|existent(U,V)))),inference(fof_nnf,[status(thm)],[ax42])).
% 0.76/0.93 fof(c163,plain,(![X69]:(![X70]:(~entity(X69,X70)|existent(X69,X70)))),inference(variable_rename,[status(thm)],[c162])).
% 0.76/0.93 cnf(c164,plain,~entity(X212,X213)|existent(X212,X213),inference(split_conjunct,[status(thm)],[c163])).
% 0.76/0.93 cnf(c376,plain,existent(skolem0001,skolem0002),inference(resolution,[status(thm)],[c370, c164])).
% 0.76/0.93 cnf(c43,axiom,X554!=X556|X555!=X553|~existent(X554,X555)|existent(X556,X553),theory(equality)).
% 0.76/0.93 cnf(c458,plain,skolem0001!=X681|skolem0002!=X680|existent(X681,X680),inference(resolution,[status(thm)],[c43, c376])).
% 0.76/0.93 cnf(c512,plain,skolem0001!=X682|existent(X682,skolem0002),inference(resolution,[status(thm)],[c458, reflexivity])).
% 0.76/0.93 cnf(c333,plain,existent(skolem0001,skolem0005),inference(resolution,[status(thm)],[c328, c164])).
% 0.76/0.93 cnf(c457,plain,skolem0001!=X674|skolem0005!=X673|existent(X674,X673),inference(resolution,[status(thm)],[c43, c333])).
% 0.76/0.93 cnf(c509,plain,skolem0001!=X679|existent(X679,skolem0005),inference(resolution,[status(thm)],[c457, reflexivity])).
% 0.76/0.93 cnf(c313,plain,existent(skolem0001,skolem0004),inference(resolution,[status(thm)],[c312, c164])).
% 0.76/0.93 cnf(c456,plain,skolem0001!=X671|skolem0004!=X670|existent(X671,X670),inference(resolution,[status(thm)],[c43, c313])).
% 0.76/0.93 cnf(c507,plain,skolem0001!=X672|existent(X672,skolem0004),inference(resolution,[status(thm)],[c456, reflexivity])).
% 0.76/0.93 fof(ax43,axiom,(![U]:(![V]:(entity(U,V)=>specific(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax43)).
% 0.76/0.93 fof(c159,plain,(![U]:(![V]:(~entity(U,V)|specific(U,V)))),inference(fof_nnf,[status(thm)],[ax43])).
% 0.76/0.93 fof(c160,plain,(![X67]:(![X68]:(~entity(X67,X68)|specific(X67,X68)))),inference(variable_rename,[status(thm)],[c159])).
% 0.76/0.93 cnf(c161,plain,~entity(X210,X211)|specific(X210,X211),inference(split_conjunct,[status(thm)],[c160])).
% 0.76/0.93 cnf(c335,plain,specific(skolem0001,skolem0005),inference(resolution,[status(thm)],[c328, c161])).
% 0.76/0.93 cnf(c31,axiom,X446!=X448|X447!=X445|~specific(X446,X447)|specific(X448,X445),theory(equality)).
% 0.76/0.93 cnf(c415,plain,skolem0001!=X661|skolem0005!=X662|specific(X661,X662),inference(resolution,[status(thm)],[c31, c335])).
% 0.76/0.93 cnf(c504,plain,skolem0001!=X663|specific(X663,skolem0005),inference(resolution,[status(thm)],[c415, reflexivity])).
% 0.76/0.93 fof(ax31,axiom,(![U]:(![V]:(eventuality(U,V)=>specific(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax31)).
% 0.76/0.93 fof(c195,plain,(![U]:(![V]:(~eventuality(U,V)|specific(U,V)))),inference(fof_nnf,[status(thm)],[ax31])).
% 0.76/0.93 fof(c196,plain,(![X91]:(![X92]:(~eventuality(X91,X92)|specific(X91,X92)))),inference(variable_rename,[status(thm)],[c195])).
% 0.76/0.93 cnf(c197,plain,~eventuality(X243,X242)|specific(X243,X242),inference(split_conjunct,[status(thm)],[c196])).
% 0.76/0.93 cnf(c297,plain,specific(skolem0001,skolem0006),inference(resolution,[status(thm)],[c294, c197])).
% 0.76/0.93 cnf(c414,plain,skolem0001!=X658|skolem0006!=X659|specific(X658,X659),inference(resolution,[status(thm)],[c31, c297])).
% 0.76/0.93 cnf(c502,plain,skolem0001!=X660|specific(X660,skolem0006),inference(resolution,[status(thm)],[c414, reflexivity])).
% 0.76/0.93 cnf(c315,plain,specific(skolem0001,skolem0004),inference(resolution,[status(thm)],[c312, c161])).
% 0.76/0.93 cnf(c413,plain,skolem0001!=X651|skolem0004!=X652|specific(X651,X652),inference(resolution,[status(thm)],[c31, c315])).
% 0.76/0.93 cnf(c499,plain,skolem0001!=X653|specific(X653,skolem0004),inference(resolution,[status(thm)],[c413, reflexivity])).
% 0.76/0.93 cnf(c379,plain,specific(skolem0001,skolem0002),inference(resolution,[status(thm)],[c370, c161])).
% 0.76/0.93 cnf(c412,plain,skolem0001!=X642|skolem0002!=X643|specific(X642,X643),inference(resolution,[status(thm)],[c31, c379])).
% 0.76/0.93 cnf(c496,plain,skolem0001!=X650|specific(X650,skolem0002),inference(resolution,[status(thm)],[c412, reflexivity])).
% 0.76/0.93 fof(ax30,axiom,(![U]:(![V]:(eventuality(U,V)=>nonexistent(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax30)).
% 0.76/0.93 fof(c198,plain,(![U]:(![V]:(~eventuality(U,V)|nonexistent(U,V)))),inference(fof_nnf,[status(thm)],[ax30])).
% 0.76/0.93 fof(c199,plain,(![X93]:(![X94]:(~eventuality(X93,X94)|nonexistent(X93,X94)))),inference(variable_rename,[status(thm)],[c198])).
% 0.76/0.93 cnf(c200,plain,~eventuality(X245,X244)|nonexistent(X245,X244),inference(split_conjunct,[status(thm)],[c199])).
% 0.76/0.93 cnf(c296,plain,nonexistent(skolem0001,skolem0006),inference(resolution,[status(thm)],[c294, c200])).
% 0.76/0.93 cnf(c30,axiom,X437!=X439|X438!=X436|~nonexistent(X437,X438)|nonexistent(X439,X436),theory(equality)).
% 0.76/0.93 cnf(c408,plain,skolem0001!=X640|skolem0006!=X639|nonexistent(X640,X639),inference(resolution,[status(thm)],[c30, c296])).
% 0.76/0.93 cnf(c494,plain,skolem0001!=X641|nonexistent(X641,skolem0006),inference(resolution,[status(thm)],[c408, reflexivity])).
% 0.76/0.93 cnf(c28,axiom,X419!=X421|X420!=X418|~eventuality(X419,X420)|eventuality(X421,X418),theory(equality)).
% 0.76/0.93 cnf(c400,plain,skolem0001!=X631|skolem0006!=X630|eventuality(X631,X630),inference(resolution,[status(thm)],[c28, c294])).
% 0.76/0.93 cnf(c491,plain,skolem0001!=X632|eventuality(X632,skolem0006),inference(resolution,[status(thm)],[c400, reflexivity])).
% 0.76/0.93 cnf(c27,axiom,X410!=X412|X411!=X409|~event(X410,X411)|event(X412,X409),theory(equality)).
% 0.76/0.93 cnf(c396,plain,skolem0001!=X628|skolem0006!=X627|event(X628,X627),inference(resolution,[status(thm)],[c27, c76])).
% 0.76/0.93 cnf(c489,plain,skolem0001!=X629|event(X629,skolem0006),inference(resolution,[status(thm)],[c396, reflexivity])).
% 0.76/0.93 cnf(c50,axiom,X625!=X622|X626!=X623|X621!=X624|~member(X625,X626,X621)|member(X622,X623,X624),theory(equality)).
% 0.76/0.93 cnf(c79,negated_conjecture,barrel(skolem0001,skolem0006),inference(split_conjunct,[status(thm)],[c64])).
% 0.76/0.93 cnf(c26,axiom,X400!=X402|X401!=X399|~barrel(X400,X401)|barrel(X402,X399),theory(equality)).
% 0.76/0.93 cnf(c391,plain,skolem0001!=X619|skolem0006!=X618|barrel(X619,X618),inference(resolution,[status(thm)],[c26, c79])).
% 0.76/0.93 cnf(c487,plain,skolem0001!=X620|barrel(X620,skolem0006),inference(resolution,[status(thm)],[c391, reflexivity])).
% 0.76/0.93 cnf(c25,axiom,X389!=X391|X390!=X388|~chevy(X389,X390)|chevy(X391,X388),theory(equality)).
% 0.76/0.93 cnf(c388,plain,skolem0001!=X607|skolem0004!=X608|chevy(X607,X608),inference(resolution,[status(thm)],[c25, c70])).
% 0.76/0.93 cnf(c485,plain,skolem0001!=X617|chevy(X617,skolem0004),inference(resolution,[status(thm)],[c388, reflexivity])).
% 0.76/0.93 cnf(c49,axiom,X615!=X611|X616!=X613|X609!=X614|X610!=X612|~be(X615,X616,X609,X610)|be(X611,X613,X614,X612),theory(equality)).
% 0.76/0.93 cnf(c24,axiom,X374!=X376|X375!=X373|~car(X374,X375)|car(X376,X373),theory(equality)).
% 0.76/0.93 cnf(c386,plain,skolem0001!=X605|skolem0004!=X604|car(X605,X604),inference(resolution,[status(thm)],[c24, c303])).
% 0.76/0.93 cnf(c483,plain,skolem0001!=X606|car(X606,skolem0004),inference(resolution,[status(thm)],[c386, reflexivity])).
% 0.76/0.93 cnf(c23,axiom,X363!=X365|X364!=X362|~vehicle(X363,X364)|vehicle(X365,X362),theory(equality)).
% 0.76/0.93 cnf(c385,plain,skolem0001!=X595|skolem0004!=X596|vehicle(X595,X596),inference(resolution,[status(thm)],[c23, c304])).
% 0.76/0.93 cnf(c480,plain,skolem0001!=X597|vehicle(X597,skolem0004),inference(resolution,[status(thm)],[c385, reflexivity])).
% 0.76/0.93 cnf(c13,axiom,X295!=X297|X296!=X294|~thing(X295,X296)|thing(X297,X294),theory(equality)).
% 0.76/0.93 cnf(c383,plain,skolem0001!=X593|skolem0002!=X592|thing(X593,X592),inference(resolution,[status(thm)],[c378, c13])).
% 0.76/0.93 cnf(c478,plain,skolem0001!=X594|thing(X594,skolem0002),inference(resolution,[status(thm)],[c383, reflexivity])).
% 0.76/0.93 cnf(c10,axiom,X271!=X273|X272!=X270|~unisex(X271,X272)|unisex(X273,X270),theory(equality)).
% 0.76/0.93 fof(ax16,axiom,(![U]:(![V]:(object(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax16)).
% 0.76/0.93 fof(c240,plain,(![U]:(![V]:(~object(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax16])).
% 0.76/0.93 fof(c241,plain,(![X121]:(![X122]:(~object(X121,X122)|unisex(X121,X122)))),inference(variable_rename,[status(thm)],[c240])).
% 0.76/0.93 cnf(c242,plain,~object(X301,X300)|unisex(X301,X300),inference(split_conjunct,[status(thm)],[c241])).
% 0.76/0.93 cnf(c373,plain,unisex(skolem0001,skolem0002),inference(resolution,[status(thm)],[c368, c242])).
% 0.76/0.93 cnf(c382,plain,skolem0001!=X585|skolem0002!=X586|unisex(X585,X586),inference(resolution,[status(thm)],[c373, c10])).
% 0.76/0.93 cnf(c475,plain,skolem0001!=X587|unisex(X587,skolem0002),inference(resolution,[status(thm)],[c382, reflexivity])).
% 0.76/0.93 cnf(c22,axiom,X359!=X361|X360!=X358|~transport(X359,X360)|transport(X361,X358),theory(equality)).
% 0.76/0.93 cnf(c381,plain,skolem0001!=X579|skolem0004!=X578|transport(X579,X578),inference(resolution,[status(thm)],[c22, c306])).
% 0.76/0.93 cnf(c473,plain,skolem0001!=X584|transport(X584,skolem0004),inference(resolution,[status(thm)],[c381, reflexivity])).
% 0.76/0.93 cnf(c46,axiom,X581!=X583|X582!=X580|~young(X581,X582)|young(X583,X580),theory(equality)).
% 0.76/0.93 cnf(c19,axiom,X337!=X339|X338!=X336|~impartial(X337,X338)|impartial(X339,X336),theory(equality)).
% 0.76/0.93 fof(ax17,axiom,(![U]:(![V]:(object(U,V)=>impartial(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax17)).
% 0.76/0.93 fof(c237,plain,(![U]:(![V]:(~object(U,V)|impartial(U,V)))),inference(fof_nnf,[status(thm)],[ax17])).
% 0.76/0.93 fof(c238,plain,(![X119]:(![X120]:(~object(X119,X120)|impartial(X119,X120)))),inference(variable_rename,[status(thm)],[c237])).
% 0.76/0.93 cnf(c239,plain,~object(X298,X299)|impartial(X298,X299),inference(split_conjunct,[status(thm)],[c238])).
% 0.76/0.93 cnf(c372,plain,impartial(skolem0001,skolem0002),inference(resolution,[status(thm)],[c368, c239])).
% 0.76/0.93 cnf(c380,plain,skolem0001!=X576|skolem0002!=X575|impartial(X576,X575),inference(resolution,[status(thm)],[c372, c19])).
% 0.76/0.93 cnf(c471,plain,skolem0001!=X577|impartial(X577,skolem0002),inference(resolution,[status(thm)],[c380, reflexivity])).
% 0.76/0.93 cnf(c45,axiom,X572!=X574|X573!=X571|~fellow(X572,X573)|fellow(X574,X571),theory(equality)).
% 0.76/0.93 cnf(c21,axiom,X353!=X355|X354!=X352|~entity(X353,X354)|entity(X355,X352),theory(equality)).
% 0.76/0.93 cnf(c377,plain,skolem0001!=X568|skolem0002!=X569|entity(X568,X569),inference(resolution,[status(thm)],[c370, c21])).
% 0.76/0.93 cnf(c469,plain,skolem0001!=X570|entity(X570,skolem0002),inference(resolution,[status(thm)],[c377, reflexivity])).
% 0.76/0.93 cnf(c20,axiom,X345!=X347|X346!=X344|~nonliving(X345,X346)|nonliving(X347,X344),theory(equality)).
% 0.76/0.93 fof(ax18,axiom,(![U]:(![V]:(object(U,V)=>nonliving(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax18)).
% 0.76/0.93 fof(c234,plain,(![U]:(![V]:(~object(U,V)|nonliving(U,V)))),inference(fof_nnf,[status(thm)],[ax18])).
% 0.76/0.93 fof(c235,plain,(![X117]:(![X118]:(~object(X117,X118)|nonliving(X117,X118)))),inference(variable_rename,[status(thm)],[c234])).
% 0.76/0.93 cnf(c236,plain,~object(X293,X292)|nonliving(X293,X292),inference(split_conjunct,[status(thm)],[c235])).
% 0.76/0.93 cnf(c369,plain,nonliving(skolem0001,skolem0002),inference(resolution,[status(thm)],[c368, c236])).
% 0.76/0.93 cnf(c375,plain,skolem0001!=X566|skolem0002!=X565|nonliving(X566,X565),inference(resolution,[status(thm)],[c369, c20])).
% 0.76/0.93 cnf(c467,plain,skolem0001!=X567|nonliving(X567,skolem0002),inference(resolution,[status(thm)],[c375, reflexivity])).
% 0.76/0.93 cnf(c5,axiom,X221!=X223|X222!=X220|~object(X221,X222)|object(X223,X220),theory(equality)).
% 0.76/0.93 cnf(c371,plain,skolem0001!=X559|skolem0002!=X558|object(X559,X558),inference(resolution,[status(thm)],[c368, c5])).
% 0.76/0.93 cnf(c460,plain,skolem0001!=X560|object(X560,skolem0002),inference(resolution,[status(thm)],[c371, reflexivity])).
% 0.76/0.93 cnf(c367,plain,skolem0001!=X551|skolem0004!=X552|entity(X551,X552),inference(resolution,[status(thm)],[c21, c312])).
% 0.76/0.93 cnf(c455,plain,skolem0001!=X557|entity(X557,skolem0004),inference(resolution,[status(thm)],[c367, reflexivity])).
% 0.76/0.93 cnf(c366,plain,skolem0001!=X548|skolem0005!=X549|entity(X548,X549),inference(resolution,[status(thm)],[c21, c328])).
% 0.76/0.93 cnf(c453,plain,skolem0001!=X550|entity(X550,skolem0005),inference(resolution,[status(thm)],[c366, reflexivity])).
% 0.76/0.93 cnf(c42,axiom,X545!=X547|X546!=X544|~living(X545,X546)|living(X547,X544),theory(equality)).
% 0.76/0.93 cnf(c4,axiom,X207!=X209|X208!=X206|~location(X207,X208)|location(X209,X206),theory(equality)).
% 0.76/0.93 cnf(c365,plain,skolem0001!=X541|skolem0002!=X542|location(X541,X542),inference(resolution,[status(thm)],[c364, c4])).
% 0.76/0.93 cnf(c451,plain,skolem0001!=X543|location(X543,skolem0002),inference(resolution,[status(thm)],[c365, reflexivity])).
% 0.76/0.93 fof(ax7,axiom,(![U]:(![V]:(abstraction(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax7)).
% 0.76/0.93 fof(c267,plain,(![U]:(![V]:(~abstraction(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax7])).
% 0.76/0.93 fof(c268,plain,(![X139]:(![X140]:(~abstraction(X139,X140)|unisex(X139,X140)))),inference(variable_rename,[status(thm)],[c267])).
% 0.76/0.93 cnf(c269,plain,~abstraction(X342,X343)|unisex(X342,X343),inference(split_conjunct,[status(thm)],[c268])).
% 0.76/0.93 cnf(c359,plain,unisex(skolem0001,skolem0003),inference(resolution,[status(thm)],[c269, c346])).
% 0.76/0.93 cnf(c362,plain,skolem0001!=X538|skolem0003!=X539|unisex(X538,X539),inference(resolution,[status(thm)],[c359, c10])).
% 0.76/0.93 cnf(c449,plain,skolem0001!=X540|unisex(X540,skolem0003),inference(resolution,[status(thm)],[c362, reflexivity])).
% 0.76/0.93 cnf(c41,axiom,X535!=X537|X536!=X534|~organism(X535,X536)|organism(X537,X534),theory(equality)).
% 0.76/0.93 cnf(c317,plain,nonliving(skolem0001,skolem0004),inference(resolution,[status(thm)],[c236, c310])).
% 0.76/0.93 cnf(c361,plain,skolem0001!=X532|skolem0004!=X531|nonliving(X532,X531),inference(resolution,[status(thm)],[c20, c317])).
% 0.76/0.93 cnf(c447,plain,skolem0001!=X533|nonliving(X533,skolem0004),inference(resolution,[status(thm)],[c361, reflexivity])).
% 0.76/0.93 cnf(c327,plain,nonliving(skolem0001,skolem0005),inference(resolution,[status(thm)],[c326, c236])).
% 0.76/0.93 cnf(c360,plain,skolem0001!=X525|skolem0005!=X524|nonliving(X525,X524),inference(resolution,[status(thm)],[c20, c327])).
% 0.76/0.93 cnf(c445,plain,skolem0001!=X530|nonliving(X530,skolem0005),inference(resolution,[status(thm)],[c360, reflexivity])).
% 0.76/0.93 cnf(c40,axiom,X527!=X529|X528!=X526|~human(X527,X528)|human(X529,X526),theory(equality)).
% 0.76/0.93 cnf(c11,axiom,X281!=X283|X282!=X280|~general(X281,X282)|general(X283,X280),theory(equality)).
% 0.76/0.93 fof(ax8,axiom,(![U]:(![V]:(abstraction(U,V)=>general(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax8)).
% 0.76/0.93 fof(c264,plain,(![U]:(![V]:(~abstraction(U,V)|general(U,V)))),inference(fof_nnf,[status(thm)],[ax8])).
% 0.76/0.93 fof(c265,plain,(![X137]:(![X138]:(~abstraction(X137,X138)|general(X137,X138)))),inference(variable_rename,[status(thm)],[c264])).
% 0.76/0.93 cnf(c266,plain,~abstraction(X340,X341)|general(X340,X341),inference(split_conjunct,[status(thm)],[c265])).
% 0.76/0.93 cnf(c356,plain,general(skolem0001,skolem0003),inference(resolution,[status(thm)],[c266, c346])).
% 0.76/0.93 cnf(c358,plain,skolem0001!=X522|skolem0003!=X521|general(X522,X521),inference(resolution,[status(thm)],[c356, c11])).
% 0.76/0.93 cnf(c443,plain,skolem0001!=X523|general(X523,skolem0003),inference(resolution,[status(thm)],[c358, reflexivity])).
% 0.76/0.93 cnf(c39,axiom,X518!=X520|X519!=X517|~animate(X518,X519)|animate(X520,X517),theory(equality)).
% 0.76/0.93 cnf(c12,axiom,X289!=X291|X290!=X288|~nonhuman(X289,X290)|nonhuman(X291,X288),theory(equality)).
% 0.76/0.93 fof(ax9,axiom,(![U]:(![V]:(abstraction(U,V)=>nonhuman(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax9)).
% 0.76/0.93 fof(c261,plain,(![U]:(![V]:(~abstraction(U,V)|nonhuman(U,V)))),inference(fof_nnf,[status(thm)],[ax9])).
% 0.76/0.93 fof(c262,plain,(![X135]:(![X136]:(~abstraction(X135,X136)|nonhuman(X135,X136)))),inference(variable_rename,[status(thm)],[c261])).
% 0.76/0.93 cnf(c263,plain,~abstraction(X335,X334)|nonhuman(X335,X334),inference(split_conjunct,[status(thm)],[c262])).
% 0.76/0.93 cnf(c352,plain,nonhuman(skolem0001,skolem0003),inference(resolution,[status(thm)],[c263, c346])).
% 0.76/0.93 cnf(c355,plain,skolem0001!=X515|skolem0003!=X514|nonhuman(X515,X514),inference(resolution,[status(thm)],[c352, c12])).
% 0.76/0.93 cnf(c441,plain,skolem0001!=X516|nonhuman(X516,skolem0003),inference(resolution,[status(thm)],[c355, reflexivity])).
% 0.76/0.93 cnf(c330,plain,impartial(skolem0001,skolem0005),inference(resolution,[status(thm)],[c326, c239])).
% 0.76/0.93 cnf(c354,plain,skolem0001!=X512|skolem0005!=X511|impartial(X512,X511),inference(resolution,[status(thm)],[c19, c330])).
% 0.76/0.93 cnf(c439,plain,skolem0001!=X513|impartial(X513,skolem0005),inference(resolution,[status(thm)],[c354, reflexivity])).
% 0.76/0.93 cnf(c38,axiom,X508!=X510|X509!=X507|~human_person(X508,X509)|human_person(X510,X507),theory(equality)).
% 0.76/0.93 cnf(c321,plain,impartial(skolem0001,skolem0004),inference(resolution,[status(thm)],[c239, c310])).
% 0.76/0.93 cnf(c353,plain,skolem0001!=X505|skolem0004!=X504|impartial(X505,X504),inference(resolution,[status(thm)],[c19, c321])).
% 0.76/0.93 cnf(c437,plain,skolem0001!=X506|impartial(X506,skolem0004),inference(resolution,[status(thm)],[c353, reflexivity])).
% 0.76/0.93 cnf(c350,plain,skolem0001!=X498|skolem0003!=X497|thing(X498,X497),inference(resolution,[status(thm)],[c349, c13])).
% 0.76/0.93 cnf(c435,plain,skolem0001!=X503|thing(X503,skolem0003),inference(resolution,[status(thm)],[c350, reflexivity])).
% 0.76/0.93 cnf(c37,axiom,X500!=X502|X501!=X499|~male(X500,X501)|male(X502,X499),theory(equality)).
% 0.76/0.93 cnf(c9,axiom,X263!=X265|X264!=X262|~abstraction(X263,X264)|abstraction(X265,X262),theory(equality)).
% 0.76/0.93 cnf(c348,plain,skolem0001!=X494|skolem0003!=X495|abstraction(X494,X495),inference(resolution,[status(thm)],[c346, c9])).
% 0.76/0.93 cnf(c433,plain,skolem0001!=X496|abstraction(X496,skolem0003),inference(resolution,[status(thm)],[c348, reflexivity])).
% 0.76/0.93 cnf(c36,axiom,X491!=X493|X492!=X490|~man(X491,X492)|man(X493,X490),theory(equality)).
% 0.76/0.93 cnf(c18,axiom,X329!=X331|X330!=X328|~street(X329,X330)|street(X331,X328),theory(equality)).
% 0.76/0.93 cnf(c347,plain,skolem0001!=X488|skolem0005!=X487|street(X488,X487),inference(resolution,[status(thm)],[c18, c74])).
% 0.76/0.93 cnf(c431,plain,skolem0001!=X489|street(X489,skolem0005),inference(resolution,[status(thm)],[c347, reflexivity])).
% 0.76/0.93 cnf(c14,axiom,X303!=X305|X304!=X302|~relation(X303,X304)|relation(X305,X302),theory(equality)).
% 0.76/0.93 cnf(c345,plain,skolem0001!=X484|skolem0003!=X485|relation(X484,X485),inference(resolution,[status(thm)],[c344, c14])).
% 0.76/0.93 cnf(c429,plain,skolem0001!=X486|relation(X486,skolem0003),inference(resolution,[status(thm)],[c345, reflexivity])).
% 0.76/0.93 cnf(c35,axiom,X481!=X483|X482!=X480|~multiple(X481,X482)|multiple(X483,X480),theory(equality)).
% 0.76/0.93 cnf(c15,axiom,X311!=X313|X312!=X310|~relname(X311,X312)|relname(X313,X310),theory(equality)).
% 0.76/0.93 cnf(c343,plain,skolem0001!=X477|skolem0003!=X478|relname(X477,X478),inference(resolution,[status(thm)],[c342, c15])).
% 0.76/0.93 cnf(c427,plain,skolem0001!=X479|relname(X479,skolem0003),inference(resolution,[status(thm)],[c343, reflexivity])).
% 0.76/0.93 cnf(c17,axiom,X319!=X321|X320!=X318|~artifact(X319,X320)|artifact(X321,X318),theory(equality)).
% 0.76/0.93 cnf(c341,plain,skolem0001!=X470|skolem0004!=X471|artifact(X470,X471),inference(resolution,[status(thm)],[c17, c309])).
% 0.76/0.93 cnf(c425,plain,skolem0001!=X476|artifact(X476,skolem0004),inference(resolution,[status(thm)],[c341, reflexivity])).
% 0.76/0.93 cnf(c34,axiom,X473!=X475|X474!=X472|~set(X473,X474)|set(X475,X472),theory(equality)).
% 0.76/0.93 cnf(c340,plain,skolem0001!=X467|skolem0005!=X468|artifact(X467,X468),inference(resolution,[status(thm)],[c17, c325])).
% 0.76/0.93 cnf(c423,plain,skolem0001!=X469|artifact(X469,skolem0005),inference(resolution,[status(thm)],[c340, reflexivity])).
% 0.76/0.93 cnf(c33,axiom,X464!=X466|X465!=X463|~group(X464,X465)|group(X466,X463),theory(equality)).
% 0.76/0.93 cnf(c338,plain,skolem0001!=X461|skolem0005!=X460|thing(X461,X460),inference(resolution,[status(thm)],[c334, c13])).
% 0.76/0.93 cnf(c421,plain,skolem0001!=X462|thing(X462,skolem0005),inference(resolution,[status(thm)],[c338, reflexivity])).
% 0.76/0.93 cnf(c16,axiom,X315!=X317|X316!=X314|~way(X315,X316)|way(X317,X314),theory(equality)).
% 0.76/0.93 cnf(c337,plain,skolem0001!=X458|skolem0005!=X457|way(X458,X457),inference(resolution,[status(thm)],[c16, c324])).
% 0.76/0.93 cnf(c419,plain,skolem0001!=X459|way(X459,skolem0005),inference(resolution,[status(thm)],[c337, reflexivity])).
% 0.76/0.93 cnf(c32,axiom,X454!=X456|X455!=X453|~two(X454,X455)|two(X456,X453),theory(equality)).
% 0.76/0.93 cnf(c331,plain,unisex(skolem0001,skolem0005),inference(resolution,[status(thm)],[c326, c242])).
% 0.76/0.93 cnf(c336,plain,skolem0001!=X450|skolem0005!=X451|unisex(X450,X451),inference(resolution,[status(thm)],[c331, c10])).
% 0.76/0.93 cnf(c417,plain,skolem0001!=X452|unisex(X452,skolem0005),inference(resolution,[status(thm)],[c336, reflexivity])).
% 0.76/0.93 cnf(c329,plain,skolem0001!=X444|skolem0005!=X443|object(X444,X443),inference(resolution,[status(thm)],[c326, c5])).
% 0.76/0.93 cnf(c411,plain,skolem0001!=X449|object(X449,skolem0005),inference(resolution,[status(thm)],[c329, reflexivity])).
% 0.76/0.93 cnf(c322,plain,unisex(skolem0001,skolem0004),inference(resolution,[status(thm)],[c242, c310])).
% 0.76/0.93 cnf(c323,plain,skolem0001!=X440|skolem0004!=X441|unisex(X440,X441),inference(resolution,[status(thm)],[c322, c10])).
% 0.76/0.93 cnf(c409,plain,skolem0001!=X442|unisex(X442,skolem0004),inference(resolution,[status(thm)],[c323, reflexivity])).
% 0.76/0.93 cnf(c319,plain,skolem0001!=X434|skolem0006!=X433|thing(X434,X433),inference(resolution,[status(thm)],[c13, c298])).
% 0.76/0.93 cnf(c406,plain,skolem0001!=X435|thing(X435,skolem0006),inference(resolution,[status(thm)],[c319, reflexivity])).
% 0.76/0.93 cnf(c318,plain,skolem0001!=X431|skolem0004!=X430|thing(X431,X430),inference(resolution,[status(thm)],[c13, c314])).
% 0.76/0.93 cnf(c404,plain,skolem0001!=X432|thing(X432,skolem0004),inference(resolution,[status(thm)],[c318, reflexivity])).
% 0.76/0.93 cnf(c29,axiom,X427!=X429|X428!=X426|~state(X427,X428)|state(X429,X426),theory(equality)).
% 0.76/0.93 cnf(c311,plain,skolem0001!=X424|skolem0004!=X423|object(X424,X423),inference(resolution,[status(thm)],[c310, c5])).
% 0.76/0.93 cnf(c402,plain,skolem0001!=X425|object(X425,skolem0004),inference(resolution,[status(thm)],[c311, reflexivity])).
% 0.76/0.93 cnf(c1,axiom,X167!=X169|X168!=X166|~instrumentality(X167,X168)|instrumentality(X169,X166),theory(equality)).
% 0.76/0.93 cnf(c308,plain,skolem0001!=X416|skolem0004!=X417|instrumentality(X416,X417),inference(resolution,[status(thm)],[c307, c1])).
% 0.76/0.93 cnf(c399,plain,skolem0001!=X422|instrumentality(X422,skolem0004),inference(resolution,[status(thm)],[c308, reflexivity])).
% 0.76/0.93 fof(ax29,axiom,(![U]:(![V]:(eventuality(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax29)).
% 0.76/0.93 fof(c201,plain,(![U]:(![V]:(~eventuality(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax29])).
% 0.76/0.93 fof(c202,plain,(![X95]:(![X96]:(~eventuality(X95,X96)|unisex(X95,X96)))),inference(variable_rename,[status(thm)],[c201])).
% 0.76/0.93 cnf(c203,plain,~eventuality(X246,X247)|unisex(X246,X247),inference(split_conjunct,[status(thm)],[c202])).
% 0.76/0.93 cnf(c295,plain,unisex(skolem0001,skolem0006),inference(resolution,[status(thm)],[c294, c203])).
% 0.76/0.93 cnf(c305,plain,skolem0001!=X413|skolem0006!=X414|unisex(X413,X414),inference(resolution,[status(thm)],[c10, c295])).
% 0.76/0.93 cnf(c397,plain,skolem0001!=X415|unisex(X415,skolem0006),inference(resolution,[status(thm)],[c305, reflexivity])).
% 0.76/0.93 cnf(c8,axiom,X257!=X259|X258!=X256|~placename(X257,X258)|placename(X259,X256),theory(equality)).
% 0.76/0.93 cnf(c300,plain,skolem0001!=X406|skolem0003!=X407|placename(X406,X407),inference(resolution,[status(thm)],[c8, c69])).
% 0.76/0.93 cnf(c394,plain,skolem0001!=X408|placename(X408,skolem0003),inference(resolution,[status(thm)],[c300, reflexivity])).
% 0.76/0.93 cnf(c68,negated_conjecture,hollywood_placename(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c64])).
% 0.76/0.93 cnf(c7,axiom,X249!=X251|X250!=X248|~hollywood_placename(X249,X250)|hollywood_placename(X251,X248),theory(equality)).
% 0.76/0.93 cnf(c293,plain,skolem0001!=X404|skolem0003!=X403|hollywood_placename(X404,X403),inference(resolution,[status(thm)],[c7, c68])).
% 0.76/0.93 cnf(c392,plain,skolem0001!=X405|hollywood_placename(X405,skolem0003),inference(resolution,[status(thm)],[c293, reflexivity])).
% 0.76/0.93 cnf(c6,axiom,X235!=X237|X236!=X234|~city(X235,X236)|city(X237,X234),theory(equality)).
% 0.76/0.93 cnf(c292,plain,skolem0001!=X396|skolem0002!=X397|city(X396,X397),inference(resolution,[status(thm)],[c6, c67])).
% 0.76/0.93 cnf(c389,plain,skolem0001!=X398|city(X398,skolem0002),inference(resolution,[status(thm)],[c292, reflexivity])).
% 0.76/0.93 cnf(c97,plain,~two(X394,X395)|skolem0010(X394,X395)!=skolem0009(X394,X395),inference(split_conjunct,[status(thm)],[c94])).
% 0.76/0.93 cnf(c96,plain,~two(X392,X393)|member(X392,skolem0010(X392,X393),X393),inference(split_conjunct,[status(thm)],[c94])).
% 0.76/0.93 cnf(c95,plain,~two(X386,X387)|member(X386,skolem0009(X386,X387),X387),inference(split_conjunct,[status(thm)],[c94])).
% 0.76/0.93 fof(ax59,axiom,(![U]:(![V]:(![W]:(![X]:(be(U,V,W,X)=>W=X))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax59)).
% 0.76/0.93 fof(c102,plain,(![U]:(![V]:(![W]:(![X]:(~be(U,V,W,X)|W=X))))),inference(fof_nnf,[status(thm)],[ax59])).
% 0.76/0.93 fof(c103,plain,(![X31]:(![X32]:(![X33]:(![X34]:(~be(X31,X32,X33,X34)|X33=X34))))),inference(variable_rename,[status(thm)],[c102])).
% 0.76/0.93 cnf(c104,plain,~be(X382,X383,X384,X385)|X384=X385,inference(split_conjunct,[status(thm)],[c103])).
% 0.76/0.93 cnf(c51,axiom,X379!=X380|~actual_world(X379)|actual_world(X380),theory(equality)).
% 0.76/0.93 fof(ax1,axiom,(![U]:(![V]:(furniture(U,V)=>instrumentality(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax1)).
% 0.76/0.93 fof(c285,plain,(![U]:(![V]:(~furniture(U,V)|instrumentality(U,V)))),inference(fof_nnf,[status(thm)],[ax1])).
% 0.76/0.93 fof(c286,plain,(![X151]:(![X152]:(~furniture(X151,X152)|instrumentality(X151,X152)))),inference(variable_rename,[status(thm)],[c285])).
% 0.76/0.93 cnf(c287,plain,~furniture(X370,X371)|instrumentality(X370,X371),inference(split_conjunct,[status(thm)],[c286])).
% 0.76/0.93 fof(ax2,axiom,(![U]:(![V]:(seat(U,V)=>furniture(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax2)).
% 0.76/0.93 fof(c282,plain,(![U]:(![V]:(~seat(U,V)|furniture(U,V)))),inference(fof_nnf,[status(thm)],[ax2])).
% 0.76/0.93 fof(c283,plain,(![X149]:(![X150]:(~seat(X149,X150)|furniture(X149,X150)))),inference(variable_rename,[status(thm)],[c282])).
% 0.76/0.93 cnf(c284,plain,~seat(X368,X369)|furniture(X368,X369),inference(split_conjunct,[status(thm)],[c283])).
% 0.76/0.93 fof(ax3,axiom,(![U]:(![V]:(frontseat(U,V)=>seat(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax3)).
% 0.76/0.93 fof(c279,plain,(![U]:(![V]:(~frontseat(U,V)|seat(U,V)))),inference(fof_nnf,[status(thm)],[ax3])).
% 0.76/0.93 fof(c280,plain,(![X147]:(![X148]:(~frontseat(X147,X148)|seat(X147,X148)))),inference(variable_rename,[status(thm)],[c279])).
% 0.76/0.93 cnf(c281,plain,~frontseat(X366,X367)|seat(X366,X367),inference(split_conjunct,[status(thm)],[c280])).
% 0.76/0.93 fof(ax50,axiom,(![U]:(![V]:(animate(U,V)=>(~nonliving(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax50)).
% 0.76/0.93 fof(c137,plain,(![U]:(![V]:(animate(U,V)=>~nonliving(U,V)))),inference(fof_simplification,[status(thm)],[ax50])).
% 0.76/0.93 fof(c138,plain,(![U]:(![V]:(~animate(U,V)|~nonliving(U,V)))),inference(fof_nnf,[status(thm)],[c137])).
% 0.76/0.93 fof(c139,plain,(![X53]:(![X54]:(~animate(X53,X54)|~nonliving(X53,X54)))),inference(variable_rename,[status(thm)],[c138])).
% 0.76/0.93 cnf(c140,plain,~animate(X189,X188)|~nonliving(X189,X188),inference(split_conjunct,[status(thm)],[c139])).
% 0.76/0.93 cnf(c374,plain,~animate(skolem0001,skolem0002),inference(resolution,[status(thm)],[c369, c140])).
% 0.76/0.93 fof(ax6,axiom,(![U]:(![V]:(hollywood_placename(U,V)=>placename(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax6)).
% 0.76/0.93 fof(c270,plain,(![U]:(![V]:(~hollywood_placename(U,V)|placename(U,V)))),inference(fof_nnf,[status(thm)],[ax6])).
% 0.76/0.93 fof(c271,plain,(![X141]:(![X142]:(~hollywood_placename(X141,X142)|placename(X141,X142)))),inference(variable_rename,[status(thm)],[c270])).
% 0.76/0.93 cnf(c272,plain,~hollywood_placename(X348,X349)|placename(X348,X349),inference(split_conjunct,[status(thm)],[c271])).
% 0.76/0.93 fof(ax55,axiom,(![U]:(![V]:(specific(U,V)=>(~general(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax55)).
% 0.76/0.93 fof(c117,plain,(![U]:(![V]:(specific(U,V)=>~general(U,V)))),inference(fof_simplification,[status(thm)],[ax55])).
% 0.76/0.93 fof(c118,plain,(![U]:(![V]:(~specific(U,V)|~general(U,V)))),inference(fof_nnf,[status(thm)],[c117])).
% 0.76/0.93 fof(c119,plain,(![X43]:(![X44]:(~specific(X43,X44)|~general(X43,X44)))),inference(variable_rename,[status(thm)],[c118])).
% 0.76/0.93 cnf(c120,plain,~specific(X174,X175)|~general(X174,X175),inference(split_conjunct,[status(thm)],[c119])).
% 0.76/0.93 cnf(c357,plain,~specific(skolem0001,skolem0003),inference(resolution,[status(thm)],[c356, c120])).
% 0.76/0.93 cnf(c332,plain,~animate(skolem0001,skolem0005),inference(resolution,[status(thm)],[c327, c140])).
% 0.76/0.93 cnf(c320,plain,~animate(skolem0001,skolem0004),inference(resolution,[status(thm)],[c317, c140])).
% 0.76/0.93 fof(ax26,axiom,(![U]:(![V]:(barrel(U,V)=>event(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax26)).
% 0.76/0.93 fof(c210,plain,(![U]:(![V]:(~barrel(U,V)|event(U,V)))),inference(fof_nnf,[status(thm)],[ax26])).
% 0.76/0.93 fof(c211,plain,(![X101]:(![X102]:(~barrel(X101,X102)|event(X101,X102)))),inference(variable_rename,[status(thm)],[c210])).
% 0.76/0.93 cnf(c212,plain,~barrel(X260,X261)|event(X260,X261),inference(split_conjunct,[status(thm)],[c211])).
% 0.76/0.93 fof(ax51,axiom,(![U]:(![V]:(existent(U,V)=>(~nonexistent(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax51)).
% 0.76/0.93 fof(c133,plain,(![U]:(![V]:(existent(U,V)=>~nonexistent(U,V)))),inference(fof_simplification,[status(thm)],[ax51])).
% 0.76/0.93 fof(c134,plain,(![U]:(![V]:(~existent(U,V)|~nonexistent(U,V)))),inference(fof_nnf,[status(thm)],[c133])).
% 0.76/0.93 fof(c135,plain,(![X51]:(![X52]:(~existent(X51,X52)|~nonexistent(X51,X52)))),inference(variable_rename,[status(thm)],[c134])).
% 0.76/0.93 cnf(c136,plain,~existent(X187,X186)|~nonexistent(X187,X186),inference(split_conjunct,[status(thm)],[c135])).
% 0.76/0.93 cnf(c299,plain,~existent(skolem0001,skolem0006),inference(resolution,[status(thm)],[c296, c136])).
% 0.76/0.93 fof(ax28,axiom,(![U]:(![V]:(state(U,V)=>event(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax28)).
% 0.76/0.93 fof(c204,plain,(![U]:(![V]:(~state(U,V)|event(U,V)))),inference(fof_nnf,[status(thm)],[ax28])).
% 0.76/0.93 fof(c205,plain,(![X97]:(![X98]:(~state(X97,X98)|event(X97,X98)))),inference(variable_rename,[status(thm)],[c204])).
% 0.76/0.93 cnf(c206,plain,~state(X252,X253)|event(X252,X253),inference(split_conjunct,[status(thm)],[c205])).
% 0.76/0.93 fof(ax33,axiom,(![U]:(![V]:(state(U,V)=>eventuality(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax33)).
% 0.76/0.93 fof(c189,plain,(![U]:(![V]:(~state(U,V)|eventuality(U,V)))),inference(fof_nnf,[status(thm)],[ax33])).
% 0.76/0.93 fof(c190,plain,(![X87]:(![X88]:(~state(X87,X88)|eventuality(X87,X88)))),inference(variable_rename,[status(thm)],[c189])).
% 0.76/0.93 cnf(c191,plain,~state(X238,X239)|eventuality(X238,X239),inference(split_conjunct,[status(thm)],[c190])).
% 0.76/0.94 fof(ax34,axiom,(![U]:(![V]:(two(U,V)=>group(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax34)).
% 0.76/0.94 fof(c186,plain,(![U]:(![V]:(~two(U,V)|group(U,V)))),inference(fof_nnf,[status(thm)],[ax34])).
% 0.76/0.94 fof(c187,plain,(![X85]:(![X86]:(~two(X85,X86)|group(X85,X86)))),inference(variable_rename,[status(thm)],[c186])).
% 0.76/0.94 cnf(c188,plain,~two(X233,X232)|group(X233,X232),inference(split_conjunct,[status(thm)],[c187])).
% 0.76/0.94 fof(ax35,axiom,(![U]:(![V]:(set(U,V)=>multiple(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax35)).
% 0.76/0.94 fof(c183,plain,(![U]:(![V]:(~set(U,V)|multiple(U,V)))),inference(fof_nnf,[status(thm)],[ax35])).
% 0.76/0.94 fof(c184,plain,(![X83]:(![X84]:(~set(X83,X84)|multiple(X83,X84)))),inference(variable_rename,[status(thm)],[c183])).
% 0.76/0.94 cnf(c185,plain,~set(X230,X231)|multiple(X230,X231),inference(split_conjunct,[status(thm)],[c184])).
% 0.76/0.94 fof(ax36,axiom,(![U]:(![V]:(group(U,V)=>set(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax36)).
% 0.76/0.94 fof(c180,plain,(![U]:(![V]:(~group(U,V)|set(U,V)))),inference(fof_nnf,[status(thm)],[ax36])).
% 0.76/0.94 fof(c181,plain,(![X81]:(![X82]:(~group(X81,X82)|set(X81,X82)))),inference(variable_rename,[status(thm)],[c180])).
% 0.76/0.94 cnf(c182,plain,~group(X228,X229)|set(X228,X229),inference(split_conjunct,[status(thm)],[c181])).
% 0.76/0.94 fof(ax37,axiom,(![U]:(![V]:(man(U,V)=>male(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax37)).
% 0.76/0.94 fof(c177,plain,(![U]:(![V]:(~man(U,V)|male(U,V)))),inference(fof_nnf,[status(thm)],[ax37])).
% 0.76/0.94 fof(c178,plain,(![X79]:(![X80]:(~man(X79,X80)|male(X79,X80)))),inference(variable_rename,[status(thm)],[c177])).
% 0.76/0.94 cnf(c179,plain,~man(X227,X226)|male(X227,X226),inference(split_conjunct,[status(thm)],[c178])).
% 0.76/0.94 fof(ax38,axiom,(![U]:(![V]:(human_person(U,V)=>animate(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax38)).
% 0.76/0.94 fof(c174,plain,(![U]:(![V]:(~human_person(U,V)|animate(U,V)))),inference(fof_nnf,[status(thm)],[ax38])).
% 0.76/0.94 fof(c175,plain,(![X77]:(![X78]:(~human_person(X77,X78)|animate(X77,X78)))),inference(variable_rename,[status(thm)],[c174])).
% 0.76/0.94 cnf(c176,plain,~human_person(X224,X225)|animate(X224,X225),inference(split_conjunct,[status(thm)],[c175])).
% 0.76/0.94 fof(ax39,axiom,(![U]:(![V]:(human_person(U,V)=>human(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax39)).
% 0.76/0.94 fof(c171,plain,(![U]:(![V]:(~human_person(U,V)|human(U,V)))),inference(fof_nnf,[status(thm)],[ax39])).
% 0.76/0.94 fof(c172,plain,(![X75]:(![X76]:(~human_person(X75,X76)|human(X75,X76)))),inference(variable_rename,[status(thm)],[c171])).
% 0.76/0.94 cnf(c173,plain,~human_person(X219,X218)|human(X219,X218),inference(split_conjunct,[status(thm)],[c172])).
% 0.76/0.94 fof(ax40,axiom,(![U]:(![V]:(organism(U,V)=>living(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax40)).
% 0.76/0.94 fof(c168,plain,(![U]:(![V]:(~organism(U,V)|living(U,V)))),inference(fof_nnf,[status(thm)],[ax40])).
% 0.76/0.94 fof(c169,plain,(![X73]:(![X74]:(~organism(X73,X74)|living(X73,X74)))),inference(variable_rename,[status(thm)],[c168])).
% 0.76/0.94 cnf(c170,plain,~organism(X216,X217)|living(X216,X217),inference(split_conjunct,[status(thm)],[c169])).
% 0.76/0.94 fof(ax41,axiom,(![U]:(![V]:(organism(U,V)=>impartial(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax41)).
% 0.76/0.94 fof(c165,plain,(![U]:(![V]:(~organism(U,V)|impartial(U,V)))),inference(fof_nnf,[status(thm)],[ax41])).
% 0.76/0.94 fof(c166,plain,(![X71]:(![X72]:(~organism(X71,X72)|impartial(X71,X72)))),inference(variable_rename,[status(thm)],[c165])).
% 0.76/0.94 cnf(c167,plain,~organism(X214,X215)|impartial(X214,X215),inference(split_conjunct,[status(thm)],[c166])).
% 0.76/0.94 fof(ax46,axiom,(![U]:(![V]:(organism(U,V)=>entity(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax46)).
% 0.76/0.94 fof(c150,plain,(![U]:(![V]:(~organism(U,V)|entity(U,V)))),inference(fof_nnf,[status(thm)],[ax46])).
% 0.76/0.94 fof(c151,plain,(![X61]:(![X62]:(~organism(X61,X62)|entity(X61,X62)))),inference(variable_rename,[status(thm)],[c150])).
% 0.76/0.94 cnf(c152,plain,~organism(X201,X200)|entity(X201,X200),inference(split_conjunct,[status(thm)],[c151])).
% 0.76/0.94 fof(ax47,axiom,(![U]:(![V]:(human_person(U,V)=>organism(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax47)).
% 0.76/0.94 fof(c147,plain,(![U]:(![V]:(~human_person(U,V)|organism(U,V)))),inference(fof_nnf,[status(thm)],[ax47])).
% 0.76/0.94 fof(c148,plain,(![X59]:(![X60]:(~human_person(X59,X60)|organism(X59,X60)))),inference(variable_rename,[status(thm)],[c147])).
% 0.76/0.94 cnf(c149,plain,~human_person(X198,X199)|organism(X198,X199),inference(split_conjunct,[status(thm)],[c148])).
% 0.76/0.94 fof(ax48,axiom,(![U]:(![V]:(man(U,V)=>human_person(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax48)).
% 0.76/0.94 fof(c144,plain,(![U]:(![V]:(~man(U,V)|human_person(U,V)))),inference(fof_nnf,[status(thm)],[ax48])).
% 0.76/0.94 fof(c145,plain,(![X57]:(![X58]:(~man(X57,X58)|human_person(X57,X58)))),inference(variable_rename,[status(thm)],[c144])).
% 0.76/0.94 cnf(c146,plain,~man(X197,X196)|human_person(X197,X196),inference(split_conjunct,[status(thm)],[c145])).
% 0.76/0.94 cnf(c3,axiom,X193!=X195|X194!=X192|~frontseat(X193,X194)|frontseat(X195,X192),theory(equality)).
% 0.76/0.94 fof(ax49,axiom,(![U]:(![V]:(fellow(U,V)=>man(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax49)).
% 0.76/0.94 fof(c141,plain,(![U]:(![V]:(~fellow(U,V)|man(U,V)))),inference(fof_nnf,[status(thm)],[ax49])).
% 0.76/0.94 fof(c142,plain,(![X55]:(![X56]:(~fellow(X55,X56)|man(X55,X56)))),inference(variable_rename,[status(thm)],[c141])).
% 0.76/0.94 cnf(c143,plain,~fellow(X191,X190)|man(X191,X190),inference(split_conjunct,[status(thm)],[c142])).
% 0.76/0.94 fof(ax52,axiom,(![U]:(![V]:(nonhuman(U,V)=>(~human(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax52)).
% 0.76/0.94 fof(c129,plain,(![U]:(![V]:(nonhuman(U,V)=>~human(U,V)))),inference(fof_simplification,[status(thm)],[ax52])).
% 0.76/0.94 fof(c130,plain,(![U]:(![V]:(~nonhuman(U,V)|~human(U,V)))),inference(fof_nnf,[status(thm)],[c129])).
% 0.76/0.94 fof(c131,plain,(![X49]:(![X50]:(~nonhuman(X49,X50)|~human(X49,X50)))),inference(variable_rename,[status(thm)],[c130])).
% 0.76/0.94 cnf(c132,plain,~nonhuman(X184,X185)|~human(X184,X185),inference(split_conjunct,[status(thm)],[c131])).
% 0.76/0.94 fof(ax53,axiom,(![U]:(![V]:(nonliving(U,V)=>(~living(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax53)).
% 0.76/0.94 fof(c125,plain,(![U]:(![V]:(nonliving(U,V)=>~living(U,V)))),inference(fof_simplification,[status(thm)],[ax53])).
% 0.76/0.94 fof(c126,plain,(![U]:(![V]:(~nonliving(U,V)|~living(U,V)))),inference(fof_nnf,[status(thm)],[c125])).
% 0.76/0.94 fof(c127,plain,(![X47]:(![X48]:(~nonliving(X47,X48)|~living(X47,X48)))),inference(variable_rename,[status(thm)],[c126])).
% 0.76/0.94 cnf(c128,plain,~nonliving(X183,X182)|~living(X183,X182),inference(split_conjunct,[status(thm)],[c127])).
% 0.76/0.94 cnf(c2,axiom,X179!=X181|X180!=X178|~seat(X179,X180)|seat(X181,X178),theory(equality)).
% 0.76/0.94 fof(ax54,axiom,(![U]:(![V]:(singleton(U,V)=>(~multiple(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax54)).
% 0.76/0.94 fof(c121,plain,(![U]:(![V]:(singleton(U,V)=>~multiple(U,V)))),inference(fof_simplification,[status(thm)],[ax54])).
% 0.76/0.94 fof(c122,plain,(![U]:(![V]:(~singleton(U,V)|~multiple(U,V)))),inference(fof_nnf,[status(thm)],[c121])).
% 0.76/0.94 fof(c123,plain,(![X45]:(![X46]:(~singleton(X45,X46)|~multiple(X45,X46)))),inference(variable_rename,[status(thm)],[c122])).
% 0.76/0.94 cnf(c124,plain,~singleton(X177,X176)|~multiple(X177,X176),inference(split_conjunct,[status(thm)],[c123])).
% 0.76/0.94 fof(ax56,axiom,(![U]:(![V]:(unisex(U,V)=>(~male(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax56)).
% 0.76/0.94 fof(c113,plain,(![U]:(![V]:(unisex(U,V)=>~male(U,V)))),inference(fof_simplification,[status(thm)],[ax56])).
% 0.76/0.94 fof(c114,plain,(![U]:(![V]:(~unisex(U,V)|~male(U,V)))),inference(fof_nnf,[status(thm)],[c113])).
% 0.76/0.94 fof(c115,plain,(![X41]:(![X42]:(~unisex(X41,X42)|~male(X41,X42)))),inference(variable_rename,[status(thm)],[c114])).
% 0.76/0.94 cnf(c116,plain,~unisex(X172,X173)|~male(X172,X173),inference(split_conjunct,[status(thm)],[c115])).
% 0.76/0.94 fof(ax57,axiom,(![U]:(![V]:(young(U,V)=>(~old(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax57)).
% 0.76/0.94 fof(c109,plain,(![U]:(![V]:(young(U,V)=>~old(U,V)))),inference(fof_simplification,[status(thm)],[ax57])).
% 0.76/0.94 fof(c110,plain,(![U]:(![V]:(~young(U,V)|~old(U,V)))),inference(fof_nnf,[status(thm)],[c109])).
% 0.76/0.94 fof(c111,plain,(![X39]:(![X40]:(~young(X39,X40)|~old(X39,X40)))),inference(variable_rename,[status(thm)],[c110])).
% 0.76/0.94 cnf(c112,plain,~young(X170,X171)|~old(X170,X171),inference(split_conjunct,[status(thm)],[c111])).
% 0.76/0.94 cnf(c291,plain,~young(skolem0001,skolem0004),inference(resolution,[status(thm)],[c112, c73])).
% 0.76/0.94 cnf(c0,axiom,X163!=X165|X164!=X162|~furniture(X163,X164)|furniture(X165,X162),theory(equality)).
% 0.76/0.94 cnf(transitivity,axiom,X159!=X160|X160!=X161|X159=X161,theory(equality)).
% 0.76/0.94 cnf(symmetry,axiom,X156!=X157|X157=X156,theory(equality)).
% 0.76/0.94 fof(ax61,axiom,(![U]:(~(?[V]:member(U,V,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax61)).
% 0.76/0.94 fof(c86,plain,(![U]:(![V]:~member(U,V,V))),inference(fof_nnf,[status(thm)],[ax61])).
% 0.76/0.94 fof(c87,plain,(![X19]:(![X20]:~member(X19,X20,X20))),inference(variable_rename,[status(thm)],[c86])).
% 0.76/0.94 cnf(c88,plain,~member(X154,X155,X155),inference(split_conjunct,[status(thm)],[c87])).
% 0.76/0.94 cnf(c65,negated_conjecture,actual_world(skolem0001),inference(split_conjunct,[status(thm)],[c64])).
% 0.76/0.94 % SZS output end Saturation
% 0.76/0.94
% 0.76/0.94 % Initial clauses : 150
% 0.76/0.94 % Processed clauses : 344
% 0.76/0.94 % Factors computed : 3
% 0.76/0.94 % Resolvents computed: 265
% 0.76/0.94 % Tautologies deleted: 3
% 0.76/0.94 % Forward subsumed : 71
% 0.76/0.94 % Backward subsumed : 0
% 0.76/0.94 % -------- CPU Time ---------
% 0.76/0.94 % User time : 0.579 s
% 0.76/0.94 % System time : 0.020 s
% 0.76/0.94 % Total time : 0.599 s
%------------------------------------------------------------------------------