PyRes---1.5.CSA-Sat.s

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

% Computer : n012.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Thu May  9 17:34:22 EDT 2024

% Result   : CounterSatisfiable 0.78s 0.95s
% Output   : Saturation 0.78s
% Verified : 
% SZS Type : -

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