PyRes---1.5.CSA-Sat.s

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

% Computer : n023.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:20 EDT 2024

% Result   : CounterSatisfiable 0.82s 1.00s
% Output   : Saturation 0.82s
% Verified : 
% SZS Type : -

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