%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP113+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n020.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:09 EDT 2024
% Result : CounterSatisfiable 0.47s 0.69s
% Output : Saturation 0.53s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : NLP113+1 : TPTP v8.1.2. Released v2.4.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n020.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Wed May 8 13:25:38 EDT 2024
% 0.14/0.36 % CPUTime :
% 0.47/0.69 % Version: 1.5
% 0.47/0.69 % SZS status CounterSatisfiable
% 0.47/0.69 % SZS output start Saturation
% 0.47/0.69 fof(co1,conjecture,(~(?[U]:(actual_world(U)&(?[V]:(restaurant(U,V)&(![W]:((customer(U,W)&in(U,W,V))=>(?[X]:(?[Y]:(?[Z]:(?[X1]:(((((((((((((coffee(U,X)&human_person(U,Y))&event(U,Z))&agent(U,Z,Y))&patient(U,Z,X))&past(U,Z))&nonreflexive(U,Z))&drink(U,Z))&event(U,X1))&agent(U,X1,W))&patient(U,X1,Y))&past(U,X1))&nonreflexive(U,X1))&see(U,X1))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1)).
% 0.47/0.69 fof(c33,negated_conjecture,(~(~(?[U]:(actual_world(U)&(?[V]:(restaurant(U,V)&(![W]:((customer(U,W)&in(U,W,V))=>(?[X]:(?[Y]:(?[Z]:(?[X1]:(((((((((((((coffee(U,X)&human_person(U,Y))&event(U,Z))&agent(U,Z,Y))&patient(U,Z,X))&past(U,Z))&nonreflexive(U,Z))&drink(U,Z))&event(U,X1))&agent(U,X1,W))&patient(U,X1,Y))&past(U,X1))&nonreflexive(U,X1))&see(U,X1)))))))))))))),inference(assume_negation,[status(cth)],[co1])).
% 0.47/0.69 fof(c34,negated_conjecture,(?[U]:(actual_world(U)&(?[V]:(restaurant(U,V)&(![W]:((~customer(U,W)|~in(U,W,V))|(?[X]:(?[Y]:(?[Z]:(?[X1]:(((((((((((((coffee(U,X)&human_person(U,Y))&event(U,Z))&agent(U,Z,Y))&patient(U,Z,X))&past(U,Z))&nonreflexive(U,Z))&drink(U,Z))&event(U,X1))&agent(U,X1,W))&patient(U,X1,Y))&past(U,X1))&nonreflexive(U,X1))&see(U,X1)))))))))))),inference(fof_nnf,[status(thm)],[c33])).
% 0.47/0.69 fof(c35,negated_conjecture,(?[X2]:(actual_world(X2)&(?[X3]:(restaurant(X2,X3)&(![X4]:((~customer(X2,X4)|~in(X2,X4,X3))|(?[X5]:(?[X6]:(?[X7]:(?[X8]:(((((((((((((coffee(X2,X5)&human_person(X2,X6))&event(X2,X7))&agent(X2,X7,X6))&patient(X2,X7,X5))&past(X2,X7))&nonreflexive(X2,X7))&drink(X2,X7))&event(X2,X8))&agent(X2,X8,X4))&patient(X2,X8,X6))&past(X2,X8))&nonreflexive(X2,X8))&see(X2,X8)))))))))))),inference(variable_rename,[status(thm)],[c34])).
% 0.47/0.69 fof(c37,negated_conjecture,(![X4]:(actual_world(skolem0001)&(restaurant(skolem0001,skolem0002)&((~customer(skolem0001,X4)|~in(skolem0001,X4,skolem0002))|(((((((((((((coffee(skolem0001,skolem0003(X4))&human_person(skolem0001,skolem0004(X4)))&event(skolem0001,skolem0005(X4)))&agent(skolem0001,skolem0005(X4),skolem0004(X4)))&patient(skolem0001,skolem0005(X4),skolem0003(X4)))&past(skolem0001,skolem0005(X4)))&nonreflexive(skolem0001,skolem0005(X4)))&drink(skolem0001,skolem0005(X4)))&event(skolem0001,skolem0006(X4)))&agent(skolem0001,skolem0006(X4),X4))&patient(skolem0001,skolem0006(X4),skolem0004(X4)))&past(skolem0001,skolem0006(X4)))&nonreflexive(skolem0001,skolem0006(X4)))&see(skolem0001,skolem0006(X4))))))),inference(shift_quantors,[status(thm)],[fof(c36,negated_conjecture,(actual_world(skolem0001)&(restaurant(skolem0001,skolem0002)&(![X4]:((~customer(skolem0001,X4)|~in(skolem0001,X4,skolem0002))|(((((((((((((coffee(skolem0001,skolem0003(X4))&human_person(skolem0001,skolem0004(X4)))&event(skolem0001,skolem0005(X4)))&agent(skolem0001,skolem0005(X4),skolem0004(X4)))&patient(skolem0001,skolem0005(X4),skolem0003(X4)))&past(skolem0001,skolem0005(X4)))&nonreflexive(skolem0001,skolem0005(X4)))&drink(skolem0001,skolem0005(X4)))&event(skolem0001,skolem0006(X4)))&agent(skolem0001,skolem0006(X4),X4))&patient(skolem0001,skolem0006(X4),skolem0004(X4)))&past(skolem0001,skolem0006(X4)))&nonreflexive(skolem0001,skolem0006(X4)))&see(skolem0001,skolem0006(X4))))))),inference(skolemize,[status(esa)],[c35])).])).
% 0.47/0.69 fof(c38,negated_conjecture,(![X4]:(actual_world(skolem0001)&(restaurant(skolem0001,skolem0002)&(((((((((((((((~customer(skolem0001,X4)|~in(skolem0001,X4,skolem0002))|coffee(skolem0001,skolem0003(X4)))&((~customer(skolem0001,X4)|~in(skolem0001,X4,skolem0002))|human_person(skolem0001,skolem0004(X4))))&((~customer(skolem0001,X4)|~in(skolem0001,X4,skolem0002))|event(skolem0001,skolem0005(X4))))&((~customer(skolem0001,X4)|~in(skolem0001,X4,skolem0002))|agent(skolem0001,skolem0005(X4),skolem0004(X4))))&((~customer(skolem0001,X4)|~in(skolem0001,X4,skolem0002))|patient(skolem0001,skolem0005(X4),skolem0003(X4))))&((~customer(skolem0001,X4)|~in(skolem0001,X4,skolem0002))|past(skolem0001,skolem0005(X4))))&((~customer(skolem0001,X4)|~in(skolem0001,X4,skolem0002))|nonreflexive(skolem0001,skolem0005(X4))))&((~customer(skolem0001,X4)|~in(skolem0001,X4,skolem0002))|drink(skolem0001,skolem0005(X4))))&((~customer(skolem0001,X4)|~in(skolem0001,X4,skolem0002))|event(skolem0001,skolem0006(X4))))&((~customer(skolem0001,X4)|~in(skolem0001,X4,skolem0002))|agent(skolem0001,skolem0006(X4),X4)))&((~customer(skolem0001,X4)|~in(skolem0001,X4,skolem0002))|patient(skolem0001,skolem0006(X4),skolem0004(X4))))&((~customer(skolem0001,X4)|~in(skolem0001,X4,skolem0002))|past(skolem0001,skolem0006(X4))))&((~customer(skolem0001,X4)|~in(skolem0001,X4,skolem0002))|nonreflexive(skolem0001,skolem0006(X4))))&((~customer(skolem0001,X4)|~in(skolem0001,X4,skolem0002))|see(skolem0001,skolem0006(X4))))))),inference(distribute,[status(thm)],[c37])).
% 0.47/0.69 cnf(c51,negated_conjecture,~customer(skolem0001,X349)|~in(skolem0001,X349,skolem0002)|patient(skolem0001,skolem0006(X349),skolem0004(X349)),inference(split_conjunct,[status(thm)],[c38])).
% 0.47/0.69 cnf(c45,negated_conjecture,~customer(skolem0001,X348)|~in(skolem0001,X348,skolem0002)|patient(skolem0001,skolem0005(X348),skolem0003(X348)),inference(split_conjunct,[status(thm)],[c38])).
% 0.47/0.69 cnf(c44,negated_conjecture,~customer(skolem0001,X347)|~in(skolem0001,X347,skolem0002)|agent(skolem0001,skolem0005(X347),skolem0004(X347)),inference(split_conjunct,[status(thm)],[c38])).
% 0.47/0.69 cnf(c50,negated_conjecture,~customer(skolem0001,X346)|~in(skolem0001,X346,skolem0002)|agent(skolem0001,skolem0006(X346),X346),inference(split_conjunct,[status(thm)],[c38])).
% 0.47/0.69 cnf(c54,negated_conjecture,~customer(skolem0001,X345)|~in(skolem0001,X345,skolem0002)|see(skolem0001,skolem0006(X345)),inference(split_conjunct,[status(thm)],[c38])).
% 0.47/0.69 cnf(c53,negated_conjecture,~customer(skolem0001,X344)|~in(skolem0001,X344,skolem0002)|nonreflexive(skolem0001,skolem0006(X344)),inference(split_conjunct,[status(thm)],[c38])).
% 0.47/0.69 cnf(c31,axiom,X340!=X338|X342!=X339|X343!=X341|~in(X340,X342,X343)|in(X338,X339,X341),theory(equality)).
% 0.47/0.69 cnf(c52,negated_conjecture,~customer(skolem0001,X337)|~in(skolem0001,X337,skolem0002)|past(skolem0001,skolem0006(X337)),inference(split_conjunct,[status(thm)],[c38])).
% 0.47/0.69 cnf(c49,negated_conjecture,~customer(skolem0001,X336)|~in(skolem0001,X336,skolem0002)|event(skolem0001,skolem0006(X336)),inference(split_conjunct,[status(thm)],[c38])).
% 0.47/0.69 cnf(c48,negated_conjecture,~customer(skolem0001,X335)|~in(skolem0001,X335,skolem0002)|drink(skolem0001,skolem0005(X335)),inference(split_conjunct,[status(thm)],[c38])).
% 0.47/0.69 cnf(c47,negated_conjecture,~customer(skolem0001,X334)|~in(skolem0001,X334,skolem0002)|nonreflexive(skolem0001,skolem0005(X334)),inference(split_conjunct,[status(thm)],[c38])).
% 0.47/0.69 cnf(c46,negated_conjecture,~customer(skolem0001,X333)|~in(skolem0001,X333,skolem0002)|past(skolem0001,skolem0005(X333)),inference(split_conjunct,[status(thm)],[c38])).
% 0.47/0.69 cnf(c28,axiom,X329!=X327|X331!=X328|X332!=X330|~agent(X329,X331,X332)|agent(X327,X328,X330),theory(equality)).
% 0.47/0.69 cnf(c43,negated_conjecture,~customer(skolem0001,X326)|~in(skolem0001,X326,skolem0002)|event(skolem0001,skolem0005(X326)),inference(split_conjunct,[status(thm)],[c38])).
% 0.47/0.69 cnf(c42,negated_conjecture,~customer(skolem0001,X325)|~in(skolem0001,X325,skolem0002)|human_person(skolem0001,skolem0004(X325)),inference(split_conjunct,[status(thm)],[c38])).
% 0.47/0.69 cnf(c41,negated_conjecture,~customer(skolem0001,X324)|~in(skolem0001,X324,skolem0002)|coffee(skolem0001,skolem0003(X324)),inference(split_conjunct,[status(thm)],[c38])).
% 0.47/0.69 fof(ax33,axiom,(![U]:(![V]:(![W]:(![X]:(((drink(U,V)&agent(U,V,W))&patient(U,V,X))=>beverage(U,X)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax33)).
% 0.47/0.69 fof(c58,plain,(![U]:(![V]:(![W]:(![X]:(((~drink(U,V)|~agent(U,V,W))|~patient(U,V,X))|beverage(U,X)))))),inference(fof_nnf,[status(thm)],[ax33])).
% 0.47/0.69 fof(c59,plain,(![X13]:(![X14]:(![X15]:(![X16]:(((~drink(X13,X14)|~agent(X13,X14,X15))|~patient(X13,X14,X16))|beverage(X13,X16)))))),inference(variable_rename,[status(thm)],[c58])).
% 0.47/0.69 cnf(c60,plain,~drink(X323,X322)|~agent(X323,X322,X321)|~patient(X323,X322,X320)|beverage(X323,X320),inference(split_conjunct,[status(thm)],[c59])).
% 0.47/0.69 fof(ax34,axiom,(![U]:(![V]:(![W]:(![X]:(((nonreflexive(U,V)&agent(U,V,W))&patient(U,V,X))=>W!=X))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax34)).
% 0.53/0.69 fof(c55,plain,(![U]:(![V]:(![W]:(![X]:(((~nonreflexive(U,V)|~agent(U,V,W))|~patient(U,V,X))|W!=X))))),inference(fof_nnf,[status(thm)],[ax34])).
% 0.53/0.69 fof(c56,plain,(![X9]:(![X10]:(![X11]:(![X12]:(((~nonreflexive(X9,X10)|~agent(X9,X10,X11))|~patient(X9,X10,X12))|X11!=X12))))),inference(variable_rename,[status(thm)],[c55])).
% 0.53/0.69 cnf(c57,plain,~nonreflexive(X318,X317)|~agent(X318,X317,X319)|~patient(X318,X317,X316)|X319!=X316,inference(split_conjunct,[status(thm)],[c56])).
% 0.53/0.69 cnf(c27,axiom,X312!=X310|X314!=X311|X315!=X313|~patient(X312,X314,X315)|patient(X310,X311,X313),theory(equality)).
% 0.53/0.69 cnf(c32,axiom,X309!=X307|X306!=X308|~past(X309,X306)|past(X307,X308),theory(equality)).
% 0.53/0.69 cnf(c29,axiom,X305!=X303|X302!=X304|~nonreflexive(X305,X302)|nonreflexive(X303,X304),theory(equality)).
% 0.53/0.69 cnf(reflexivity,axiom,X81=X81,theory(equality)).
% 0.53/0.69 fof(ax26,axiom,(![U]:(![V]:(thing(U,V)=>singleton(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax26)).
% 0.53/0.69 fof(c82,plain,(![U]:(![V]:(~thing(U,V)|singleton(U,V)))),inference(fof_nnf,[status(thm)],[ax26])).
% 0.53/0.69 fof(c83,plain,(![X29]:(![X30]:(~thing(X29,X30)|singleton(X29,X30)))),inference(variable_rename,[status(thm)],[c82])).
% 0.53/0.69 cnf(c84,plain,~thing(X104,X105)|singleton(X104,X105),inference(split_conjunct,[status(thm)],[c83])).
% 0.53/0.69 fof(ax16,axiom,(![U]:(![V]:(entity(U,V)=>thing(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax16)).
% 0.53/0.69 fof(c112,plain,(![U]:(![V]:(~entity(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax16])).
% 0.53/0.69 fof(c113,plain,(![X49]:(![X50]:(~entity(X49,X50)|thing(X49,X50)))),inference(variable_rename,[status(thm)],[c112])).
% 0.53/0.69 cnf(c114,plain,~entity(X133,X132)|thing(X133,X132),inference(split_conjunct,[status(thm)],[c113])).
% 0.53/0.69 fof(ax17,axiom,(![U]:(![V]:(object(U,V)=>entity(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax17)).
% 0.53/0.69 fof(c109,plain,(![U]:(![V]:(~object(U,V)|entity(U,V)))),inference(fof_nnf,[status(thm)],[ax17])).
% 0.53/0.69 fof(c110,plain,(![X47]:(![X48]:(~object(X47,X48)|entity(X47,X48)))),inference(variable_rename,[status(thm)],[c109])).
% 0.53/0.69 cnf(c111,plain,~object(X131,X130)|entity(X131,X130),inference(split_conjunct,[status(thm)],[c110])).
% 0.53/0.69 cnf(c40,negated_conjecture,restaurant(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c38])).
% 0.53/0.69 fof(ax3,axiom,(![U]:(![V]:(restaurant(U,V)=>building(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax3)).
% 0.53/0.69 fof(c151,plain,(![U]:(![V]:(~restaurant(U,V)|building(U,V)))),inference(fof_nnf,[status(thm)],[ax3])).
% 0.53/0.69 fof(c152,plain,(![X75]:(![X76]:(~restaurant(X75,X76)|building(X75,X76)))),inference(variable_rename,[status(thm)],[c151])).
% 0.53/0.69 cnf(c153,plain,~restaurant(X167,X166)|building(X167,X166),inference(split_conjunct,[status(thm)],[c152])).
% 0.53/0.69 cnf(c164,plain,building(skolem0001,skolem0002),inference(resolution,[status(thm)],[c153, c40])).
% 0.53/0.69 fof(ax2,axiom,(![U]:(![V]:(building(U,V)=>artifact(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax2)).
% 0.53/0.69 fof(c154,plain,(![U]:(![V]:(~building(U,V)|artifact(U,V)))),inference(fof_nnf,[status(thm)],[ax2])).
% 0.53/0.69 fof(c155,plain,(![X77]:(![X78]:(~building(X77,X78)|artifact(X77,X78)))),inference(variable_rename,[status(thm)],[c154])).
% 0.53/0.69 cnf(c156,plain,~building(X173,X172)|artifact(X173,X172),inference(split_conjunct,[status(thm)],[c155])).
% 0.53/0.69 cnf(c166,plain,artifact(skolem0001,skolem0002),inference(resolution,[status(thm)],[c156, c164])).
% 0.53/0.69 fof(ax1,axiom,(![U]:(![V]:(artifact(U,V)=>object(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax1)).
% 0.53/0.69 fof(c157,plain,(![U]:(![V]:(~artifact(U,V)|object(U,V)))),inference(fof_nnf,[status(thm)],[ax1])).
% 0.53/0.69 fof(c158,plain,(![X79]:(![X80]:(~artifact(X79,X80)|object(X79,X80)))),inference(variable_rename,[status(thm)],[c157])).
% 0.53/0.69 cnf(c159,plain,~artifact(X175,X174)|object(X175,X174),inference(split_conjunct,[status(thm)],[c158])).
% 0.53/0.69 cnf(c168,plain,object(skolem0001,skolem0002),inference(resolution,[status(thm)],[c159, c166])).
% 0.53/0.69 cnf(c173,plain,entity(skolem0001,skolem0002),inference(resolution,[status(thm)],[c168, c111])).
% 0.53/0.69 cnf(c176,plain,thing(skolem0001,skolem0002),inference(resolution,[status(thm)],[c173, c114])).
% 0.53/0.69 cnf(c178,plain,singleton(skolem0001,skolem0002),inference(resolution,[status(thm)],[c176, c84])).
% 0.53/0.69 cnf(c25,axiom,X294!=X292|X291!=X293|~singleton(X294,X291)|singleton(X292,X293),theory(equality)).
% 0.53/0.69 cnf(c209,plain,skolem0001!=X299|skolem0002!=X300|singleton(X299,X300),inference(resolution,[status(thm)],[c25, c178])).
% 0.53/0.69 cnf(c210,plain,skolem0001!=X301|singleton(X301,skolem0002),inference(resolution,[status(thm)],[c209, reflexivity])).
% 0.53/0.69 cnf(c26,axiom,X298!=X296|X295!=X297|~see(X298,X295)|see(X296,X297),theory(equality)).
% 0.53/0.69 cnf(c24,axiom,X290!=X288|X287!=X289|~nonexistent(X290,X287)|nonexistent(X288,X289),theory(equality)).
% 0.53/0.69 cnf(c23,axiom,X286!=X284|X283!=X285|~eventuality(X286,X283)|eventuality(X284,X285),theory(equality)).
% 0.53/0.69 cnf(c22,axiom,X282!=X280|X279!=X281|~event(X282,X279)|event(X280,X281),theory(equality)).
% 0.53/0.69 cnf(c21,axiom,X278!=X276|X275!=X277|~drink(X278,X275)|drink(X276,X277),theory(equality)).
% 0.53/0.69 cnf(c20,axiom,X274!=X272|X271!=X273|~coffee(X274,X271)|coffee(X272,X273),theory(equality)).
% 0.53/0.69 cnf(c19,axiom,X270!=X268|X267!=X269|~beverage(X270,X267)|beverage(X268,X269),theory(equality)).
% 0.53/0.69 cnf(c18,axiom,X266!=X264|X263!=X265|~food(X266,X263)|food(X264,X265),theory(equality)).
% 0.53/0.69 cnf(c16,axiom,X255!=X253|X252!=X254|~thing(X255,X252)|thing(X253,X254),theory(equality)).
% 0.53/0.69 cnf(c206,plain,skolem0001!=X261|skolem0002!=X260|thing(X261,X260),inference(resolution,[status(thm)],[c16, c176])).
% 0.53/0.69 cnf(c207,plain,skolem0001!=X262|thing(X262,skolem0002),inference(resolution,[status(thm)],[c206, reflexivity])).
% 0.53/0.69 cnf(c17,axiom,X259!=X257|X256!=X258|~substance_matter(X259,X256)|substance_matter(X257,X258),theory(equality)).
% 0.53/0.69 fof(ax15,axiom,(![U]:(![V]:(entity(U,V)=>specific(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax15)).
% 0.53/0.69 fof(c115,plain,(![U]:(![V]:(~entity(U,V)|specific(U,V)))),inference(fof_nnf,[status(thm)],[ax15])).
% 0.53/0.69 fof(c116,plain,(![X51]:(![X52]:(~entity(X51,X52)|specific(X51,X52)))),inference(variable_rename,[status(thm)],[c115])).
% 0.53/0.69 cnf(c117,plain,~entity(X134,X135)|specific(X134,X135),inference(split_conjunct,[status(thm)],[c116])).
% 0.53/0.69 cnf(c175,plain,specific(skolem0001,skolem0002),inference(resolution,[status(thm)],[c173, c117])).
% 0.53/0.69 cnf(c15,axiom,X248!=X246|X245!=X247|~specific(X248,X245)|specific(X246,X247),theory(equality)).
% 0.53/0.69 cnf(c203,plain,skolem0001!=X249|skolem0002!=X250|specific(X249,X250),inference(resolution,[status(thm)],[c15, c175])).
% 0.53/0.69 cnf(c204,plain,skolem0001!=X251|specific(X251,skolem0002),inference(resolution,[status(thm)],[c203, reflexivity])).
% 0.53/0.69 fof(ax14,axiom,(![U]:(![V]:(entity(U,V)=>existent(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax14)).
% 0.53/0.69 fof(c118,plain,(![U]:(![V]:(~entity(U,V)|existent(U,V)))),inference(fof_nnf,[status(thm)],[ax14])).
% 0.53/0.69 fof(c119,plain,(![X53]:(![X54]:(~entity(X53,X54)|existent(X53,X54)))),inference(variable_rename,[status(thm)],[c118])).
% 0.53/0.69 cnf(c120,plain,~entity(X136,X137)|existent(X136,X137),inference(split_conjunct,[status(thm)],[c119])).
% 0.53/0.69 cnf(c177,plain,existent(skolem0001,skolem0002),inference(resolution,[status(thm)],[c173, c120])).
% 0.53/0.69 cnf(c14,axiom,X238!=X236|X235!=X237|~existent(X238,X235)|existent(X236,X237),theory(equality)).
% 0.53/0.69 cnf(c198,plain,skolem0001!=X243|skolem0002!=X242|existent(X243,X242),inference(resolution,[status(thm)],[c14, c177])).
% 0.53/0.69 cnf(c201,plain,skolem0001!=X244|existent(X244,skolem0002),inference(resolution,[status(thm)],[c198, reflexivity])).
% 0.53/0.69 fof(ax13,axiom,(![U]:(![V]:(object(U,V)=>nonliving(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax13)).
% 0.53/0.69 fof(c121,plain,(![U]:(![V]:(~object(U,V)|nonliving(U,V)))),inference(fof_nnf,[status(thm)],[ax13])).
% 0.53/0.69 fof(c122,plain,(![X55]:(![X56]:(~object(X55,X56)|nonliving(X55,X56)))),inference(variable_rename,[status(thm)],[c121])).
% 0.53/0.69 cnf(c123,plain,~object(X138,X139)|nonliving(X138,X139),inference(split_conjunct,[status(thm)],[c122])).
% 0.53/0.69 cnf(c172,plain,nonliving(skolem0001,skolem0002),inference(resolution,[status(thm)],[c168, c123])).
% 0.53/0.69 cnf(c13,axiom,X234!=X232|X231!=X233|~nonliving(X234,X231)|nonliving(X232,X233),theory(equality)).
% 0.53/0.69 cnf(c197,plain,skolem0001!=X239|skolem0002!=X240|nonliving(X239,X240),inference(resolution,[status(thm)],[c13, c172])).
% 0.53/0.69 cnf(c199,plain,skolem0001!=X241|nonliving(X241,skolem0002),inference(resolution,[status(thm)],[c197, reflexivity])).
% 0.53/0.69 fof(ax11,axiom,(![U]:(![V]:(object(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax11)).
% 0.53/0.69 fof(c127,plain,(![U]:(![V]:(~object(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax11])).
% 0.53/0.69 fof(c128,plain,(![X59]:(![X60]:(~object(X59,X60)|unisex(X59,X60)))),inference(variable_rename,[status(thm)],[c127])).
% 0.53/0.69 cnf(c129,plain,~object(X147,X146)|unisex(X147,X146),inference(split_conjunct,[status(thm)],[c128])).
% 0.53/0.69 cnf(c171,plain,unisex(skolem0001,skolem0002),inference(resolution,[status(thm)],[c168, c129])).
% 0.53/0.69 cnf(c12,axiom,X227!=X225|X224!=X226|~unisex(X227,X224)|unisex(X225,X226),theory(equality)).
% 0.53/0.69 cnf(c194,plain,skolem0001!=X229|skolem0002!=X228|unisex(X229,X228),inference(resolution,[status(thm)],[c12, c171])).
% 0.53/0.69 cnf(c195,plain,skolem0001!=X230|unisex(X230,skolem0002),inference(resolution,[status(thm)],[c194, reflexivity])).
% 0.53/0.69 cnf(c11,axiom,X217!=X215|X214!=X216|~entity(X217,X214)|entity(X215,X216),theory(equality)).
% 0.53/0.69 cnf(c189,plain,skolem0001!=X221|skolem0002!=X222|entity(X221,X222),inference(resolution,[status(thm)],[c11, c173])).
% 0.53/0.69 cnf(c192,plain,skolem0001!=X223|entity(X223,skolem0002),inference(resolution,[status(thm)],[c189, reflexivity])).
% 0.53/0.69 fof(ax12,axiom,(![U]:(![V]:(object(U,V)=>impartial(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax12)).
% 0.53/0.69 fof(c124,plain,(![U]:(![V]:(~object(U,V)|impartial(U,V)))),inference(fof_nnf,[status(thm)],[ax12])).
% 0.53/0.69 fof(c125,plain,(![X57]:(![X58]:(~object(X57,X58)|impartial(X57,X58)))),inference(variable_rename,[status(thm)],[c124])).
% 0.53/0.69 cnf(c126,plain,~object(X145,X144)|impartial(X145,X144),inference(split_conjunct,[status(thm)],[c125])).
% 0.53/0.69 cnf(c170,plain,impartial(skolem0001,skolem0002),inference(resolution,[status(thm)],[c168, c126])).
% 0.53/0.69 cnf(c10,axiom,X209!=X207|X206!=X208|~impartial(X209,X206)|impartial(X207,X208),theory(equality)).
% 0.53/0.69 cnf(c185,plain,skolem0001!=X218|skolem0002!=X219|impartial(X218,X219),inference(resolution,[status(thm)],[c10, c170])).
% 0.53/0.69 cnf(c190,plain,skolem0001!=X220|impartial(X220,skolem0002),inference(resolution,[status(thm)],[c185, reflexivity])).
% 0.53/0.69 cnf(c1,axiom,X115!=X113|X112!=X114|~object(X115,X112)|object(X113,X114),theory(equality)).
% 0.53/0.69 cnf(c169,plain,skolem0001!=X211|skolem0002!=X212|object(X211,X212),inference(resolution,[status(thm)],[c168, c1])).
% 0.53/0.69 cnf(c187,plain,skolem0001!=X213|object(X213,skolem0002),inference(resolution,[status(thm)],[c169, reflexivity])).
% 0.53/0.69 cnf(c0,axiom,X101!=X99|X98!=X100|~artifact(X101,X98)|artifact(X99,X100),theory(equality)).
% 0.53/0.69 cnf(c167,plain,skolem0001!=X204|skolem0002!=X205|artifact(X204,X205),inference(resolution,[status(thm)],[c166, c0])).
% 0.53/0.69 cnf(c184,plain,skolem0001!=X210|artifact(X210,skolem0002),inference(resolution,[status(thm)],[c167, reflexivity])).
% 0.53/0.69 cnf(c2,axiom,X129!=X127|X126!=X128|~building(X129,X126)|building(X127,X128),theory(equality)).
% 0.53/0.69 cnf(c165,plain,skolem0001!=X202|skolem0002!=X201|building(X202,X201),inference(resolution,[status(thm)],[c164, c2])).
% 0.53/0.69 cnf(c182,plain,skolem0001!=X203|building(X203,skolem0002),inference(resolution,[status(thm)],[c165, reflexivity])).
% 0.53/0.69 cnf(c9,axiom,X200!=X198|X197!=X199|~living(X200,X197)|living(X198,X199),theory(equality)).
% 0.53/0.69 cnf(c3,axiom,X143!=X141|X140!=X142|~restaurant(X143,X140)|restaurant(X141,X142),theory(equality)).
% 0.53/0.69 cnf(c163,plain,skolem0001!=X194|skolem0002!=X195|restaurant(X194,X195),inference(resolution,[status(thm)],[c3, c40])).
% 0.53/0.69 cnf(c180,plain,skolem0001!=X196|restaurant(X196,skolem0002),inference(resolution,[status(thm)],[c163, reflexivity])).
% 0.53/0.69 cnf(c30,axiom,X192!=X191|~actual_world(X192)|actual_world(X191),theory(equality)).
% 0.53/0.69 cnf(c8,axiom,X188!=X186|X185!=X187|~organism(X188,X185)|organism(X186,X187),theory(equality)).
% 0.53/0.69 cnf(c7,axiom,X183!=X181|X180!=X182|~human(X183,X180)|human(X181,X182),theory(equality)).
% 0.53/0.69 fof(ax30,axiom,(![U]:(![V]:(animate(U,V)=>(~nonliving(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax30)).
% 0.53/0.69 fof(c69,plain,(![U]:(![V]:(animate(U,V)=>~nonliving(U,V)))),inference(fof_simplification,[status(thm)],[ax30])).
% 0.53/0.69 fof(c70,plain,(![U]:(![V]:(~animate(U,V)|~nonliving(U,V)))),inference(fof_nnf,[status(thm)],[c69])).
% 0.53/0.69 fof(c71,plain,(![X21]:(![X22]:(~animate(X21,X22)|~nonliving(X21,X22)))),inference(variable_rename,[status(thm)],[c70])).
% 0.53/0.69 cnf(c72,plain,~animate(X93,X92)|~nonliving(X93,X92),inference(split_conjunct,[status(thm)],[c71])).
% 0.53/0.69 cnf(c174,plain,~animate(skolem0001,skolem0002),inference(resolution,[status(thm)],[c172, c72])).
% 0.53/0.69 cnf(c6,axiom,X179!=X177|X176!=X178|~animate(X179,X176)|animate(X177,X178),theory(equality)).
% 0.53/0.69 cnf(c5,axiom,X171!=X169|X168!=X170|~human_person(X171,X168)|human_person(X169,X170),theory(equality)).
% 0.53/0.69 fof(ax4,axiom,(![U]:(![V]:(customer(U,V)=>human_person(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax4)).
% 0.53/0.69 fof(c148,plain,(![U]:(![V]:(~customer(U,V)|human_person(U,V)))),inference(fof_nnf,[status(thm)],[ax4])).
% 0.53/0.69 fof(c149,plain,(![X73]:(![X74]:(~customer(X73,X74)|human_person(X73,X74)))),inference(variable_rename,[status(thm)],[c148])).
% 0.53/0.69 cnf(c150,plain,~customer(X164,X165)|human_person(X164,X165),inference(split_conjunct,[status(thm)],[c149])).
% 0.53/0.69 fof(ax5,axiom,(![U]:(![V]:(human_person(U,V)=>animate(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax5)).
% 0.53/0.69 fof(c145,plain,(![U]:(![V]:(~human_person(U,V)|animate(U,V)))),inference(fof_nnf,[status(thm)],[ax5])).
% 0.53/0.69 fof(c146,plain,(![X71]:(![X72]:(~human_person(X71,X72)|animate(X71,X72)))),inference(variable_rename,[status(thm)],[c145])).
% 0.53/0.69 cnf(c147,plain,~human_person(X163,X162)|animate(X163,X162),inference(split_conjunct,[status(thm)],[c146])).
% 0.53/0.69 fof(ax6,axiom,(![U]:(![V]:(human_person(U,V)=>human(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax6)).
% 0.53/0.69 fof(c142,plain,(![U]:(![V]:(~human_person(U,V)|human(U,V)))),inference(fof_nnf,[status(thm)],[ax6])).
% 0.53/0.69 fof(c143,plain,(![X69]:(![X70]:(~human_person(X69,X70)|human(X69,X70)))),inference(variable_rename,[status(thm)],[c142])).
% 0.53/0.69 cnf(c144,plain,~human_person(X160,X161)|human(X160,X161),inference(split_conjunct,[status(thm)],[c143])).
% 0.53/0.69 fof(ax7,axiom,(![U]:(![V]:(organism(U,V)=>living(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax7)).
% 0.53/0.69 fof(c139,plain,(![U]:(![V]:(~organism(U,V)|living(U,V)))),inference(fof_nnf,[status(thm)],[ax7])).
% 0.53/0.69 fof(c140,plain,(![X67]:(![X68]:(~organism(X67,X68)|living(X67,X68)))),inference(variable_rename,[status(thm)],[c139])).
% 0.53/0.69 cnf(c141,plain,~organism(X159,X158)|living(X159,X158),inference(split_conjunct,[status(thm)],[c140])).
% 0.53/0.69 cnf(c4,axiom,X157!=X155|X154!=X156|~customer(X157,X154)|customer(X155,X156),theory(equality)).
% 0.53/0.69 fof(ax8,axiom,(![U]:(![V]:(organism(U,V)=>impartial(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax8)).
% 0.53/0.69 fof(c136,plain,(![U]:(![V]:(~organism(U,V)|impartial(U,V)))),inference(fof_nnf,[status(thm)],[ax8])).
% 0.53/0.69 fof(c137,plain,(![X65]:(![X66]:(~organism(X65,X66)|impartial(X65,X66)))),inference(variable_rename,[status(thm)],[c136])).
% 0.53/0.69 cnf(c138,plain,~organism(X153,X152)|impartial(X153,X152),inference(split_conjunct,[status(thm)],[c137])).
% 0.53/0.69 fof(ax9,axiom,(![U]:(![V]:(organism(U,V)=>entity(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax9)).
% 0.53/0.69 fof(c133,plain,(![U]:(![V]:(~organism(U,V)|entity(U,V)))),inference(fof_nnf,[status(thm)],[ax9])).
% 0.53/0.69 fof(c134,plain,(![X63]:(![X64]:(~organism(X63,X64)|entity(X63,X64)))),inference(variable_rename,[status(thm)],[c133])).
% 0.53/0.69 cnf(c135,plain,~organism(X151,X150)|entity(X151,X150),inference(split_conjunct,[status(thm)],[c134])).
% 0.53/0.69 fof(ax10,axiom,(![U]:(![V]:(human_person(U,V)=>organism(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax10)).
% 0.53/0.69 fof(c130,plain,(![U]:(![V]:(~human_person(U,V)|organism(U,V)))),inference(fof_nnf,[status(thm)],[ax10])).
% 0.53/0.69 fof(c131,plain,(![X61]:(![X62]:(~human_person(X61,X62)|organism(X61,X62)))),inference(variable_rename,[status(thm)],[c130])).
% 0.53/0.69 cnf(c132,plain,~human_person(X149,X148)|organism(X149,X148),inference(split_conjunct,[status(thm)],[c131])).
% 0.53/0.69 fof(ax18,axiom,(![U]:(![V]:(substance_matter(U,V)=>object(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax18)).
% 0.53/0.69 fof(c106,plain,(![U]:(![V]:(~substance_matter(U,V)|object(U,V)))),inference(fof_nnf,[status(thm)],[ax18])).
% 0.53/0.69 fof(c107,plain,(![X45]:(![X46]:(~substance_matter(X45,X46)|object(X45,X46)))),inference(variable_rename,[status(thm)],[c106])).
% 0.53/0.69 cnf(c108,plain,~substance_matter(X125,X124)|object(X125,X124),inference(split_conjunct,[status(thm)],[c107])).
% 0.53/0.69 fof(ax19,axiom,(![U]:(![V]:(food(U,V)=>substance_matter(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax19)).
% 0.53/0.69 fof(c103,plain,(![U]:(![V]:(~food(U,V)|substance_matter(U,V)))),inference(fof_nnf,[status(thm)],[ax19])).
% 0.53/0.69 fof(c104,plain,(![X43]:(![X44]:(~food(X43,X44)|substance_matter(X43,X44)))),inference(variable_rename,[status(thm)],[c103])).
% 0.53/0.69 cnf(c105,plain,~food(X122,X123)|substance_matter(X122,X123),inference(split_conjunct,[status(thm)],[c104])).
% 0.53/0.69 fof(ax20,axiom,(![U]:(![V]:(beverage(U,V)=>food(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax20)).
% 0.53/0.69 fof(c100,plain,(![U]:(![V]:(~beverage(U,V)|food(U,V)))),inference(fof_nnf,[status(thm)],[ax20])).
% 0.53/0.69 fof(c101,plain,(![X41]:(![X42]:(~beverage(X41,X42)|food(X41,X42)))),inference(variable_rename,[status(thm)],[c100])).
% 0.53/0.69 cnf(c102,plain,~beverage(X121,X120)|food(X121,X120),inference(split_conjunct,[status(thm)],[c101])).
% 0.53/0.69 fof(ax21,axiom,(![U]:(![V]:(coffee(U,V)=>beverage(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax21)).
% 0.53/0.69 fof(c97,plain,(![U]:(![V]:(~coffee(U,V)|beverage(U,V)))),inference(fof_nnf,[status(thm)],[ax21])).
% 0.53/0.69 fof(c98,plain,(![X39]:(![X40]:(~coffee(X39,X40)|beverage(X39,X40)))),inference(variable_rename,[status(thm)],[c97])).
% 0.53/0.69 cnf(c99,plain,~coffee(X119,X118)|beverage(X119,X118),inference(split_conjunct,[status(thm)],[c98])).
% 0.53/0.69 fof(ax22,axiom,(![U]:(![V]:(drink(U,V)=>event(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax22)).
% 0.53/0.69 fof(c94,plain,(![U]:(![V]:(~drink(U,V)|event(U,V)))),inference(fof_nnf,[status(thm)],[ax22])).
% 0.53/0.69 fof(c95,plain,(![X37]:(![X38]:(~drink(X37,X38)|event(X37,X38)))),inference(variable_rename,[status(thm)],[c94])).
% 0.53/0.69 cnf(c96,plain,~drink(X116,X117)|event(X116,X117),inference(split_conjunct,[status(thm)],[c95])).
% 0.53/0.69 fof(ax23,axiom,(![U]:(![V]:(eventuality(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax23)).
% 0.53/0.69 fof(c91,plain,(![U]:(![V]:(~eventuality(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax23])).
% 0.53/0.69 fof(c92,plain,(![X35]:(![X36]:(~eventuality(X35,X36)|unisex(X35,X36)))),inference(variable_rename,[status(thm)],[c91])).
% 0.53/0.69 cnf(c93,plain,~eventuality(X110,X111)|unisex(X110,X111),inference(split_conjunct,[status(thm)],[c92])).
% 0.53/0.69 fof(ax24,axiom,(![U]:(![V]:(eventuality(U,V)=>nonexistent(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax24)).
% 0.53/0.69 fof(c88,plain,(![U]:(![V]:(~eventuality(U,V)|nonexistent(U,V)))),inference(fof_nnf,[status(thm)],[ax24])).
% 0.53/0.69 fof(c89,plain,(![X33]:(![X34]:(~eventuality(X33,X34)|nonexistent(X33,X34)))),inference(variable_rename,[status(thm)],[c88])).
% 0.53/0.69 cnf(c90,plain,~eventuality(X109,X108)|nonexistent(X109,X108),inference(split_conjunct,[status(thm)],[c89])).
% 0.53/0.69 fof(ax25,axiom,(![U]:(![V]:(eventuality(U,V)=>specific(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax25)).
% 0.53/0.69 fof(c85,plain,(![U]:(![V]:(~eventuality(U,V)|specific(U,V)))),inference(fof_nnf,[status(thm)],[ax25])).
% 0.53/0.69 fof(c86,plain,(![X31]:(![X32]:(~eventuality(X31,X32)|specific(X31,X32)))),inference(variable_rename,[status(thm)],[c85])).
% 0.53/0.69 cnf(c87,plain,~eventuality(X106,X107)|specific(X106,X107),inference(split_conjunct,[status(thm)],[c86])).
% 0.53/0.69 fof(ax27,axiom,(![U]:(![V]:(eventuality(U,V)=>thing(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax27)).
% 0.53/0.69 fof(c79,plain,(![U]:(![V]:(~eventuality(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax27])).
% 0.53/0.69 fof(c80,plain,(![X27]:(![X28]:(~eventuality(X27,X28)|thing(X27,X28)))),inference(variable_rename,[status(thm)],[c79])).
% 0.53/0.69 cnf(c81,plain,~eventuality(X102,X103)|thing(X102,X103),inference(split_conjunct,[status(thm)],[c80])).
% 0.53/0.69 fof(ax28,axiom,(![U]:(![V]:(event(U,V)=>eventuality(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax28)).
% 0.53/0.69 fof(c76,plain,(![U]:(![V]:(~event(U,V)|eventuality(U,V)))),inference(fof_nnf,[status(thm)],[ax28])).
% 0.53/0.69 fof(c77,plain,(![X25]:(![X26]:(~event(X25,X26)|eventuality(X25,X26)))),inference(variable_rename,[status(thm)],[c76])).
% 0.53/0.69 cnf(c78,plain,~event(X96,X97)|eventuality(X96,X97),inference(split_conjunct,[status(thm)],[c77])).
% 0.53/0.69 fof(ax29,axiom,(![U]:(![V]:(see(U,V)=>event(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax29)).
% 0.53/0.69 fof(c73,plain,(![U]:(![V]:(~see(U,V)|event(U,V)))),inference(fof_nnf,[status(thm)],[ax29])).
% 0.53/0.69 fof(c74,plain,(![X23]:(![X24]:(~see(X23,X24)|event(X23,X24)))),inference(variable_rename,[status(thm)],[c73])).
% 0.53/0.69 cnf(c75,plain,~see(X94,X95)|event(X94,X95),inference(split_conjunct,[status(thm)],[c74])).
% 0.53/0.69 fof(ax31,axiom,(![U]:(![V]:(existent(U,V)=>(~nonexistent(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax31)).
% 0.53/0.69 fof(c65,plain,(![U]:(![V]:(existent(U,V)=>~nonexistent(U,V)))),inference(fof_simplification,[status(thm)],[ax31])).
% 0.53/0.69 fof(c66,plain,(![U]:(![V]:(~existent(U,V)|~nonexistent(U,V)))),inference(fof_nnf,[status(thm)],[c65])).
% 0.53/0.69 fof(c67,plain,(![X19]:(![X20]:(~existent(X19,X20)|~nonexistent(X19,X20)))),inference(variable_rename,[status(thm)],[c66])).
% 0.53/0.69 cnf(c68,plain,~existent(X90,X91)|~nonexistent(X90,X91),inference(split_conjunct,[status(thm)],[c67])).
% 0.53/0.69 fof(ax32,axiom,(![U]:(![V]:(nonliving(U,V)=>(~living(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax32)).
% 0.53/0.69 fof(c61,plain,(![U]:(![V]:(nonliving(U,V)=>~living(U,V)))),inference(fof_simplification,[status(thm)],[ax32])).
% 0.53/0.69 fof(c62,plain,(![U]:(![V]:(~nonliving(U,V)|~living(U,V)))),inference(fof_nnf,[status(thm)],[c61])).
% 0.53/0.69 fof(c63,plain,(![X17]:(![X18]:(~nonliving(X17,X18)|~living(X17,X18)))),inference(variable_rename,[status(thm)],[c62])).
% 0.53/0.69 cnf(c64,plain,~nonliving(X88,X89)|~living(X88,X89),inference(split_conjunct,[status(thm)],[c63])).
% 0.53/0.69 cnf(transitivity,axiom,X85!=X86|X86!=X87|X85=X87,theory(equality)).
% 0.53/0.69 cnf(symmetry,axiom,X82!=X83|X83=X82,theory(equality)).
% 0.53/0.69 cnf(c39,negated_conjecture,actual_world(skolem0001),inference(split_conjunct,[status(thm)],[c38])).
% 0.53/0.69 % SZS output end Saturation
% 0.53/0.69
% 0.53/0.69 % Initial clauses : 86
% 0.53/0.69 % Processed clauses : 122
% 0.53/0.69 % Factors computed : 1
% 0.53/0.69 % Resolvents computed: 51
% 0.53/0.69 % Tautologies deleted: 3
% 0.53/0.69 % Forward subsumed : 13
% 0.53/0.69 % Backward subsumed : 0
% 0.53/0.69 % -------- CPU Time ---------
% 0.53/0.69 % User time : 0.317 s
% 0.53/0.69 % System time : 0.014 s
% 0.53/0.69 % Total time : 0.331 s
%------------------------------------------------------------------------------