%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP042+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n027.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:33:46 EDT 2024
% Result : CounterSatisfiable 0.47s 0.71s
% Output : Saturation 0.47s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : NLP042+1 : TPTP v8.1.2. Released v2.4.0.
% 0.10/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.33 % Computer : n027.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Wed May 8 13:21:23 EDT 2024
% 0.13/0.33 % CPUTime :
% 0.47/0.71 % Version: 1.5
% 0.47/0.71 % SZS status CounterSatisfiable
% 0.47/0.71 % SZS output start Saturation
% 0.47/0.71 fof(co1,conjecture,(~(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:((((((((((of(U,W,V)&woman(U,V))&mia_forename(U,W))&forename(U,W))&shake_beverage(U,X))&event(U,Y))&agent(U,Y,V))&patient(U,Y,X))&past(U,Y))&nonreflexive(U,Y))&order(U,Y))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1)).
% 0.47/0.71 fof(c38,negated_conjecture,(~(~(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:((((((((((of(U,W,V)&woman(U,V))&mia_forename(U,W))&forename(U,W))&shake_beverage(U,X))&event(U,Y))&agent(U,Y,V))&patient(U,Y,X))&past(U,Y))&nonreflexive(U,Y))&order(U,Y)))))))))),inference(assume_negation,[status(cth)],[co1])).
% 0.47/0.71 fof(c39,negated_conjecture,(?[U]:(actual_world(U)&(?[V]:(?[W]:(?[X]:(?[Y]:((((((((((of(U,W,V)&woman(U,V))&mia_forename(U,W))&forename(U,W))&shake_beverage(U,X))&event(U,Y))&agent(U,Y,V))&patient(U,Y,X))&past(U,Y))&nonreflexive(U,Y))&order(U,Y)))))))),inference(fof_nnf,[status(thm)],[c38])).
% 0.47/0.71 fof(c40,negated_conjecture,(?[X2]:(actual_world(X2)&(?[X3]:(?[X4]:(?[X5]:(?[X6]:((((((((((of(X2,X4,X3)&woman(X2,X3))&mia_forename(X2,X4))&forename(X2,X4))&shake_beverage(X2,X5))&event(X2,X6))&agent(X2,X6,X3))&patient(X2,X6,X5))&past(X2,X6))&nonreflexive(X2,X6))&order(X2,X6)))))))),inference(variable_rename,[status(thm)],[c39])).
% 0.47/0.71 fof(c41,negated_conjecture,(actual_world(skolem0001)&((((((((((of(skolem0001,skolem0003,skolem0002)&woman(skolem0001,skolem0002))&mia_forename(skolem0001,skolem0003))&forename(skolem0001,skolem0003))&shake_beverage(skolem0001,skolem0004))&event(skolem0001,skolem0005))&agent(skolem0001,skolem0005,skolem0002))&patient(skolem0001,skolem0005,skolem0004))&past(skolem0001,skolem0005))&nonreflexive(skolem0001,skolem0005))&order(skolem0001,skolem0005))),inference(skolemize,[status(esa)],[c40])).
% 0.47/0.71 cnf(c43,negated_conjecture,of(skolem0001,skolem0003,skolem0002),inference(split_conjunct,[status(thm)],[c41])).
% 0.47/0.71 fof(ax43,axiom,(![U]:(![V]:(![W]:(((entity(U,V)&forename(U,W))&of(U,W,V))=>(~(?[X]:((forename(U,X)&X!=W)&of(U,X,V)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax43)).
% 0.47/0.71 fof(c57,plain,(![U]:(![V]:(![W]:(((~entity(U,V)|~forename(U,W))|~of(U,W,V))|(![X]:((~forename(U,X)|X=W)|~of(U,X,V))))))),inference(fof_nnf,[status(thm)],[ax43])).
% 0.47/0.71 fof(c59,plain,(![X11]:(![X12]:(![X13]:(![X14]:(((~entity(X11,X12)|~forename(X11,X13))|~of(X11,X13,X12))|((~forename(X11,X14)|X14=X13)|~of(X11,X14,X12))))))),inference(shift_quantors,[status(thm)],[fof(c58,plain,(![X11]:(![X12]:(![X13]:(((~entity(X11,X12)|~forename(X11,X13))|~of(X11,X13,X12))|(![X14]:((~forename(X11,X14)|X14=X13)|~of(X11,X14,X12))))))),inference(variable_rename,[status(thm)],[c57])).])).
% 0.47/0.71 cnf(c60,plain,~entity(X454,X453)|~forename(X454,X452)|~of(X454,X452,X453)|~forename(X454,X455)|X455=X452|~of(X454,X455,X453),inference(split_conjunct,[status(thm)],[c59])).
% 0.47/0.71 cnf(c362,plain,~entity(skolem0001,skolem0002)|~forename(skolem0001,X521)|~of(skolem0001,X521,skolem0002)|~forename(skolem0001,skolem0003)|skolem0003=X521,inference(resolution,[status(thm)],[c60, c43])).
% 0.47/0.71 cnf(c49,negated_conjecture,agent(skolem0001,skolem0005,skolem0002),inference(split_conjunct,[status(thm)],[c41])).
% 0.47/0.71 cnf(c50,negated_conjecture,patient(skolem0001,skolem0005,skolem0004),inference(split_conjunct,[status(thm)],[c41])).
% 0.47/0.71 fof(ax44,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', ax44)).
% 0.47/0.71 fof(c54,plain,(![U]:(![V]:(![W]:(![X]:(((~nonreflexive(U,V)|~agent(U,V,W))|~patient(U,V,X))|W!=X))))),inference(fof_nnf,[status(thm)],[ax44])).
% 0.47/0.71 fof(c55,plain,(![X7]:(![X8]:(![X9]:(![X10]:(((~nonreflexive(X7,X8)|~agent(X7,X8,X9))|~patient(X7,X8,X10))|X9!=X10))))),inference(variable_rename,[status(thm)],[c54])).
% 0.47/0.71 cnf(c56,plain,~nonreflexive(X443,X446)|~agent(X443,X446,X445)|~patient(X443,X446,X444)|X445!=X444,inference(split_conjunct,[status(thm)],[c55])).
% 0.47/0.71 cnf(c357,plain,~nonreflexive(skolem0001,skolem0005)|~agent(skolem0001,skolem0005,X520)|X520!=skolem0004,inference(resolution,[status(thm)],[c56, c50])).
% 0.47/0.71 cnf(c401,plain,~nonreflexive(skolem0001,skolem0005)|skolem0002!=skolem0004,inference(resolution,[status(thm)],[c357, c49])).
% 0.47/0.71 cnf(reflexivity,axiom,X99=X99,theory(equality)).
% 0.47/0.71 cnf(c35,axiom,X424!=X423|X427!=X425|X428!=X426|~agent(X424,X427,X428)|agent(X423,X425,X426),theory(equality)).
% 0.47/0.71 cnf(c348,plain,skolem0001!=X514|skolem0005!=X515|skolem0002!=X516|agent(X514,X515,X516),inference(resolution,[status(thm)],[c35, c49])).
% 0.47/0.71 cnf(c398,plain,skolem0001!=X518|skolem0005!=X517|agent(X518,X517,skolem0002),inference(resolution,[status(thm)],[c348, reflexivity])).
% 0.47/0.71 cnf(c399,plain,skolem0001!=X519|agent(X519,skolem0005,skolem0002),inference(resolution,[status(thm)],[c398, reflexivity])).
% 0.47/0.71 cnf(c33,axiom,X403!=X402|X406!=X404|X407!=X405|~patient(X403,X406,X407)|patient(X402,X404,X405),theory(equality)).
% 0.47/0.71 cnf(c339,plain,skolem0001!=X507|skolem0005!=X505|skolem0004!=X506|patient(X507,X505,X506),inference(resolution,[status(thm)],[c33, c50])).
% 0.47/0.71 cnf(c395,plain,skolem0001!=X509|skolem0005!=X508|patient(X509,X508,skolem0004),inference(resolution,[status(thm)],[c339, reflexivity])).
% 0.47/0.71 cnf(c396,plain,skolem0001!=X510|patient(X510,skolem0005,skolem0004),inference(resolution,[status(thm)],[c395, reflexivity])).
% 0.47/0.71 cnf(c32,axiom,X393!=X392|X396!=X394|X397!=X395|~of(X393,X396,X397)|of(X392,X394,X395),theory(equality)).
% 0.47/0.71 cnf(c335,plain,skolem0001!=X496|skolem0003!=X498|skolem0002!=X497|of(X496,X498,X497),inference(resolution,[status(thm)],[c32, c43])).
% 0.47/0.71 cnf(c390,plain,skolem0001!=X503|skolem0003!=X502|of(X503,X502,skolem0002),inference(resolution,[status(thm)],[c335, reflexivity])).
% 0.47/0.71 cnf(c393,plain,skolem0001!=X504|of(X504,skolem0003,skolem0002),inference(resolution,[status(thm)],[c390, reflexivity])).
% 0.47/0.71 cnf(c51,negated_conjecture,past(skolem0001,skolem0005),inference(split_conjunct,[status(thm)],[c41])).
% 0.47/0.71 cnf(c37,axiom,X433!=X435|X434!=X436|~past(X433,X434)|past(X435,X436),theory(equality)).
% 0.47/0.71 cnf(c352,plain,skolem0001!=X500|skolem0005!=X499|past(X500,X499),inference(resolution,[status(thm)],[c37, c51])).
% 0.47/0.71 cnf(c391,plain,skolem0001!=X501|past(X501,skolem0005),inference(resolution,[status(thm)],[c352, reflexivity])).
% 0.47/0.71 cnf(c52,negated_conjecture,nonreflexive(skolem0001,skolem0005),inference(split_conjunct,[status(thm)],[c41])).
% 0.47/0.71 cnf(c34,axiom,X414!=X416|X415!=X417|~nonreflexive(X414,X415)|nonreflexive(X416,X417),theory(equality)).
% 0.47/0.71 cnf(c344,plain,skolem0001!=X493|skolem0005!=X494|nonreflexive(X493,X494),inference(resolution,[status(thm)],[c34, c52])).
% 0.47/0.71 cnf(c388,plain,skolem0001!=X495|nonreflexive(X495,skolem0005),inference(resolution,[status(thm)],[c344, reflexivity])).
% 0.47/0.71 cnf(c53,negated_conjecture,order(skolem0001,skolem0005),inference(split_conjunct,[status(thm)],[c41])).
% 0.47/0.71 fof(ax36,axiom,(![U]:(![V]:(order(U,V)=>act(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax36)).
% 0.47/0.71 fof(c85,plain,(![U]:(![V]:(~order(U,V)|act(U,V)))),inference(fof_nnf,[status(thm)],[ax36])).
% 0.47/0.71 fof(c86,plain,(![X27]:(![X28]:(~order(X27,X28)|act(X27,X28)))),inference(variable_rename,[status(thm)],[c85])).
% 0.47/0.71 cnf(c87,plain,~order(X127,X126)|act(X127,X126),inference(split_conjunct,[status(thm)],[c86])).
% 0.47/0.71 cnf(c197,plain,act(skolem0001,skolem0005),inference(resolution,[status(thm)],[c87, c53])).
% 0.47/0.71 cnf(c31,axiom,X383!=X385|X384!=X386|~act(X383,X384)|act(X385,X386),theory(equality)).
% 0.47/0.71 cnf(c331,plain,skolem0001!=X491|skolem0005!=X490|act(X491,X490),inference(resolution,[status(thm)],[c31, c197])).
% 0.47/0.71 cnf(c386,plain,skolem0001!=X492|act(X492,skolem0005),inference(resolution,[status(thm)],[c331, reflexivity])).
% 0.47/0.71 cnf(c48,negated_conjecture,event(skolem0001,skolem0005),inference(split_conjunct,[status(thm)],[c41])).
% 0.47/0.71 fof(ax34,axiom,(![U]:(![V]:(event(U,V)=>eventuality(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax34)).
% 0.47/0.71 fof(c91,plain,(![U]:(![V]:(~event(U,V)|eventuality(U,V)))),inference(fof_nnf,[status(thm)],[ax34])).
% 0.47/0.71 fof(c92,plain,(![X31]:(![X32]:(~event(X31,X32)|eventuality(X31,X32)))),inference(variable_rename,[status(thm)],[c91])).
% 0.47/0.71 cnf(c93,plain,~event(X130,X131)|eventuality(X130,X131),inference(split_conjunct,[status(thm)],[c92])).
% 0.47/0.71 cnf(c199,plain,eventuality(skolem0001,skolem0005),inference(resolution,[status(thm)],[c93, c48])).
% 0.47/0.71 fof(ax33,axiom,(![U]:(![V]:(eventuality(U,V)=>thing(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax33)).
% 0.47/0.71 fof(c94,plain,(![U]:(![V]:(~eventuality(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax33])).
% 0.47/0.71 fof(c95,plain,(![X33]:(![X34]:(~eventuality(X33,X34)|thing(X33,X34)))),inference(variable_rename,[status(thm)],[c94])).
% 0.47/0.71 cnf(c96,plain,~eventuality(X136,X137)|thing(X136,X137),inference(split_conjunct,[status(thm)],[c95])).
% 0.47/0.71 cnf(c200,plain,thing(skolem0001,skolem0005),inference(resolution,[status(thm)],[c96, c199])).
% 0.47/0.71 fof(ax32,axiom,(![U]:(![V]:(thing(U,V)=>singleton(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax32)).
% 0.47/0.71 fof(c97,plain,(![U]:(![V]:(~thing(U,V)|singleton(U,V)))),inference(fof_nnf,[status(thm)],[ax32])).
% 0.47/0.71 fof(c98,plain,(![X35]:(![X36]:(~thing(X35,X36)|singleton(X35,X36)))),inference(variable_rename,[status(thm)],[c97])).
% 0.47/0.71 cnf(c99,plain,~thing(X138,X139)|singleton(X138,X139),inference(split_conjunct,[status(thm)],[c98])).
% 0.47/0.71 cnf(c201,plain,singleton(skolem0001,skolem0005),inference(resolution,[status(thm)],[c99, c200])).
% 0.47/0.71 cnf(c30,axiom,X373!=X375|X374!=X376|~singleton(X373,X374)|singleton(X375,X376),theory(equality)).
% 0.47/0.71 cnf(c326,plain,skolem0001!=X487|skolem0005!=X488|singleton(X487,X488),inference(resolution,[status(thm)],[c30, c201])).
% 0.47/0.71 cnf(c384,plain,skolem0001!=X489|singleton(X489,skolem0005),inference(resolution,[status(thm)],[c326, reflexivity])).
% 0.47/0.71 fof(ax22,axiom,(![U]:(![V]:(entity(U,V)=>thing(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax22)).
% 0.47/0.71 fof(c127,plain,(![U]:(![V]:(~entity(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax22])).
% 0.47/0.71 fof(c128,plain,(![X55]:(![X56]:(~entity(X55,X56)|thing(X55,X56)))),inference(variable_rename,[status(thm)],[c127])).
% 0.47/0.71 cnf(c129,plain,~entity(X175,X174)|thing(X175,X174),inference(split_conjunct,[status(thm)],[c128])).
% 0.47/0.71 cnf(c44,negated_conjecture,woman(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c41])).
% 0.47/0.71 fof(ax8,axiom,(![U]:(![V]:(woman(U,V)=>human_person(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax8)).
% 0.47/0.71 fof(c169,plain,(![U]:(![V]:(~woman(U,V)|human_person(U,V)))),inference(fof_nnf,[status(thm)],[ax8])).
% 0.47/0.71 fof(c170,plain,(![X83]:(![X84]:(~woman(X83,X84)|human_person(X83,X84)))),inference(variable_rename,[status(thm)],[c169])).
% 0.47/0.71 cnf(c171,plain,~woman(X230,X231)|human_person(X230,X231),inference(split_conjunct,[status(thm)],[c170])).
% 0.47/0.71 cnf(c239,plain,human_person(skolem0001,skolem0002),inference(resolution,[status(thm)],[c171, c44])).
% 0.47/0.71 fof(ax7,axiom,(![U]:(![V]:(human_person(U,V)=>organism(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax7)).
% 0.47/0.71 fof(c172,plain,(![U]:(![V]:(~human_person(U,V)|organism(U,V)))),inference(fof_nnf,[status(thm)],[ax7])).
% 0.47/0.71 fof(c173,plain,(![X85]:(![X86]:(~human_person(X85,X86)|organism(X85,X86)))),inference(variable_rename,[status(thm)],[c172])).
% 0.47/0.71 cnf(c174,plain,~human_person(X233,X232)|organism(X233,X232),inference(split_conjunct,[status(thm)],[c173])).
% 0.47/0.71 cnf(c241,plain,organism(skolem0001,skolem0002),inference(resolution,[status(thm)],[c174, c239])).
% 0.47/0.71 fof(ax6,axiom,(![U]:(![V]:(organism(U,V)=>entity(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax6)).
% 0.47/0.71 fof(c175,plain,(![U]:(![V]:(~organism(U,V)|entity(U,V)))),inference(fof_nnf,[status(thm)],[ax6])).
% 0.47/0.71 fof(c176,plain,(![X87]:(![X88]:(~organism(X87,X88)|entity(X87,X88)))),inference(variable_rename,[status(thm)],[c175])).
% 0.47/0.71 cnf(c177,plain,~organism(X238,X239)|entity(X238,X239),inference(split_conjunct,[status(thm)],[c176])).
% 0.47/0.71 cnf(c244,plain,entity(skolem0001,skolem0002),inference(resolution,[status(thm)],[c177, c241])).
% 0.47/0.71 cnf(c245,plain,thing(skolem0001,skolem0002),inference(resolution,[status(thm)],[c244, c129])).
% 0.47/0.71 cnf(c249,plain,singleton(skolem0001,skolem0002),inference(resolution,[status(thm)],[c245, c99])).
% 0.47/0.71 cnf(c325,plain,skolem0001!=X484|skolem0002!=X485|singleton(X484,X485),inference(resolution,[status(thm)],[c30, c249])).
% 0.47/0.71 cnf(c382,plain,skolem0001!=X486|singleton(X486,skolem0002),inference(resolution,[status(thm)],[c325, reflexivity])).
% 0.47/0.71 cnf(c47,negated_conjecture,shake_beverage(skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c41])).
% 0.47/0.71 fof(ax27,axiom,(![U]:(![V]:(shake_beverage(U,V)=>beverage(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax27)).
% 0.47/0.71 fof(c112,plain,(![U]:(![V]:(~shake_beverage(U,V)|beverage(U,V)))),inference(fof_nnf,[status(thm)],[ax27])).
% 0.47/0.71 fof(c113,plain,(![X45]:(![X46]:(~shake_beverage(X45,X46)|beverage(X45,X46)))),inference(variable_rename,[status(thm)],[c112])).
% 0.47/0.71 cnf(c114,plain,~shake_beverage(X156,X157)|beverage(X156,X157),inference(split_conjunct,[status(thm)],[c113])).
% 0.47/0.71 cnf(c207,plain,beverage(skolem0001,skolem0004),inference(resolution,[status(thm)],[c114, c47])).
% 0.47/0.71 fof(ax26,axiom,(![U]:(![V]:(beverage(U,V)=>food(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax26)).
% 0.47/0.71 fof(c115,plain,(![U]:(![V]:(~beverage(U,V)|food(U,V)))),inference(fof_nnf,[status(thm)],[ax26])).
% 0.47/0.71 fof(c116,plain,(![X47]:(![X48]:(~beverage(X47,X48)|food(X47,X48)))),inference(variable_rename,[status(thm)],[c115])).
% 0.47/0.71 cnf(c117,plain,~beverage(X162,X163)|food(X162,X163),inference(split_conjunct,[status(thm)],[c116])).
% 0.47/0.71 cnf(c208,plain,food(skolem0001,skolem0004),inference(resolution,[status(thm)],[c117, c207])).
% 0.47/0.71 fof(ax25,axiom,(![U]:(![V]:(food(U,V)=>substance_matter(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax25)).
% 0.47/0.71 fof(c118,plain,(![U]:(![V]:(~food(U,V)|substance_matter(U,V)))),inference(fof_nnf,[status(thm)],[ax25])).
% 0.47/0.71 fof(c119,plain,(![X49]:(![X50]:(~food(X49,X50)|substance_matter(X49,X50)))),inference(variable_rename,[status(thm)],[c118])).
% 0.47/0.71 cnf(c120,plain,~food(X164,X165)|substance_matter(X164,X165),inference(split_conjunct,[status(thm)],[c119])).
% 0.47/0.71 cnf(c209,plain,substance_matter(skolem0001,skolem0004),inference(resolution,[status(thm)],[c120, c208])).
% 0.47/0.71 fof(ax24,axiom,(![U]:(![V]:(substance_matter(U,V)=>object(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax24)).
% 0.47/0.71 fof(c121,plain,(![U]:(![V]:(~substance_matter(U,V)|object(U,V)))),inference(fof_nnf,[status(thm)],[ax24])).
% 0.47/0.71 fof(c122,plain,(![X51]:(![X52]:(~substance_matter(X51,X52)|object(X51,X52)))),inference(variable_rename,[status(thm)],[c121])).
% 0.47/0.71 cnf(c123,plain,~substance_matter(X171,X170)|object(X171,X170),inference(split_conjunct,[status(thm)],[c122])).
% 0.47/0.71 cnf(c210,plain,object(skolem0001,skolem0004),inference(resolution,[status(thm)],[c123, c209])).
% 0.47/0.71 fof(ax23,axiom,(![U]:(![V]:(object(U,V)=>entity(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax23)).
% 0.47/0.71 fof(c124,plain,(![U]:(![V]:(~object(U,V)|entity(U,V)))),inference(fof_nnf,[status(thm)],[ax23])).
% 0.47/0.71 fof(c125,plain,(![X53]:(![X54]:(~object(X53,X54)|entity(X53,X54)))),inference(variable_rename,[status(thm)],[c124])).
% 0.47/0.71 cnf(c126,plain,~object(X172,X173)|entity(X172,X173),inference(split_conjunct,[status(thm)],[c125])).
% 0.47/0.71 cnf(c211,plain,entity(skolem0001,skolem0004),inference(resolution,[status(thm)],[c126, c210])).
% 0.47/0.71 cnf(c212,plain,thing(skolem0001,skolem0004),inference(resolution,[status(thm)],[c129, c211])).
% 0.47/0.71 cnf(c213,plain,singleton(skolem0001,skolem0004),inference(resolution,[status(thm)],[c212, c99])).
% 0.47/0.71 cnf(c324,plain,skolem0001!=X481|skolem0004!=X482|singleton(X481,X482),inference(resolution,[status(thm)],[c30, c213])).
% 0.47/0.71 cnf(c380,plain,skolem0001!=X483|singleton(X483,skolem0004),inference(resolution,[status(thm)],[c324, reflexivity])).
% 0.47/0.71 cnf(c46,negated_conjecture,forename(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c41])).
% 0.47/0.71 fof(ax16,axiom,(![U]:(![V]:(forename(U,V)=>relname(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax16)).
% 0.47/0.71 fof(c145,plain,(![U]:(![V]:(~forename(U,V)|relname(U,V)))),inference(fof_nnf,[status(thm)],[ax16])).
% 0.47/0.71 fof(c146,plain,(![X67]:(![X68]:(~forename(X67,X68)|relname(X67,X68)))),inference(variable_rename,[status(thm)],[c145])).
% 0.47/0.71 cnf(c147,plain,~forename(X199,X198)|relname(X199,X198),inference(split_conjunct,[status(thm)],[c146])).
% 0.47/0.71 cnf(c223,plain,relname(skolem0001,skolem0003),inference(resolution,[status(thm)],[c147, c46])).
% 0.47/0.71 fof(ax15,axiom,(![U]:(![V]:(relname(U,V)=>relation(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax15)).
% 0.47/0.71 fof(c148,plain,(![U]:(![V]:(~relname(U,V)|relation(U,V)))),inference(fof_nnf,[status(thm)],[ax15])).
% 0.47/0.71 fof(c149,plain,(![X69]:(![X70]:(~relname(X69,X70)|relation(X69,X70)))),inference(variable_rename,[status(thm)],[c148])).
% 0.47/0.71 cnf(c150,plain,~relname(X204,X205)|relation(X204,X205),inference(split_conjunct,[status(thm)],[c149])).
% 0.47/0.71 cnf(c225,plain,relation(skolem0001,skolem0003),inference(resolution,[status(thm)],[c150, c223])).
% 0.47/0.71 fof(ax14,axiom,(![U]:(![V]:(relation(U,V)=>abstraction(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax14)).
% 0.47/0.71 fof(c151,plain,(![U]:(![V]:(~relation(U,V)|abstraction(U,V)))),inference(fof_nnf,[status(thm)],[ax14])).
% 0.47/0.71 fof(c152,plain,(![X71]:(![X72]:(~relation(X71,X72)|abstraction(X71,X72)))),inference(variable_rename,[status(thm)],[c151])).
% 0.47/0.71 cnf(c153,plain,~relation(X206,X207)|abstraction(X206,X207),inference(split_conjunct,[status(thm)],[c152])).
% 0.47/0.71 cnf(c226,plain,abstraction(skolem0001,skolem0003),inference(resolution,[status(thm)],[c153, c225])).
% 0.47/0.71 fof(ax13,axiom,(![U]:(![V]:(abstraction(U,V)=>thing(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax13)).
% 0.47/0.71 fof(c154,plain,(![U]:(![V]:(~abstraction(U,V)|thing(U,V)))),inference(fof_nnf,[status(thm)],[ax13])).
% 0.47/0.71 fof(c155,plain,(![X73]:(![X74]:(~abstraction(X73,X74)|thing(X73,X74)))),inference(variable_rename,[status(thm)],[c154])).
% 0.47/0.71 cnf(c156,plain,~abstraction(X209,X208)|thing(X209,X208),inference(split_conjunct,[status(thm)],[c155])).
% 0.47/0.71 cnf(c227,plain,thing(skolem0001,skolem0003),inference(resolution,[status(thm)],[c156, c226])).
% 0.47/0.71 cnf(c229,plain,singleton(skolem0001,skolem0003),inference(resolution,[status(thm)],[c227, c99])).
% 0.47/0.71 cnf(c323,plain,skolem0001!=X478|skolem0003!=X479|singleton(X478,X479),inference(resolution,[status(thm)],[c30, c229])).
% 0.47/0.71 cnf(c378,plain,skolem0001!=X480|singleton(X480,skolem0003),inference(resolution,[status(thm)],[c323, reflexivity])).
% 0.47/0.71 fof(ax30,axiom,(![U]:(![V]:(eventuality(U,V)=>nonexistent(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax30)).
% 0.47/0.71 fof(c103,plain,(![U]:(![V]:(~eventuality(U,V)|nonexistent(U,V)))),inference(fof_nnf,[status(thm)],[ax30])).
% 0.47/0.71 fof(c104,plain,(![X39]:(![X40]:(~eventuality(X39,X40)|nonexistent(X39,X40)))),inference(variable_rename,[status(thm)],[c103])).
% 0.47/0.71 cnf(c105,plain,~eventuality(X147,X146)|nonexistent(X147,X146),inference(split_conjunct,[status(thm)],[c104])).
% 0.47/0.71 cnf(c203,plain,nonexistent(skolem0001,skolem0005),inference(resolution,[status(thm)],[c105, c199])).
% 0.47/0.71 cnf(c29,axiom,X365!=X367|X366!=X368|~nonexistent(X365,X366)|nonexistent(X367,X368),theory(equality)).
% 0.47/0.71 cnf(c319,plain,skolem0001!=X475|skolem0005!=X476|nonexistent(X475,X476),inference(resolution,[status(thm)],[c29, c203])).
% 0.47/0.71 cnf(c376,plain,skolem0001!=X477|nonexistent(X477,skolem0005),inference(resolution,[status(thm)],[c319, reflexivity])).
% 0.47/0.71 cnf(c28,axiom,X356!=X358|X357!=X359|~eventuality(X356,X357)|eventuality(X358,X359),theory(equality)).
% 0.47/0.71 cnf(c315,plain,skolem0001!=X472|skolem0005!=X473|eventuality(X472,X473),inference(resolution,[status(thm)],[c28, c199])).
% 0.47/0.71 cnf(c374,plain,skolem0001!=X474|eventuality(X474,skolem0005),inference(resolution,[status(thm)],[c315, reflexivity])).
% 0.47/0.71 cnf(c27,axiom,X346!=X348|X347!=X349|~event(X346,X347)|event(X348,X349),theory(equality)).
% 0.47/0.71 cnf(c310,plain,skolem0001!=X470|skolem0005!=X469|event(X470,X469),inference(resolution,[status(thm)],[c27, c48])).
% 0.47/0.71 cnf(c372,plain,skolem0001!=X471|event(X471,skolem0005),inference(resolution,[status(thm)],[c310, reflexivity])).
% 0.47/0.71 cnf(c26,axiom,X338!=X340|X339!=X341|~order(X338,X339)|order(X340,X341),theory(equality)).
% 0.47/0.71 cnf(c306,plain,skolem0001!=X466|skolem0005!=X467|order(X466,X467),inference(resolution,[status(thm)],[c26, c53])).
% 0.47/0.71 cnf(c370,plain,skolem0001!=X468|order(X468,skolem0005),inference(resolution,[status(thm)],[c306, reflexivity])).
% 0.47/0.71 cnf(c25,axiom,X329!=X331|X330!=X332|~shake_beverage(X329,X330)|shake_beverage(X331,X332),theory(equality)).
% 0.47/0.71 cnf(c302,plain,skolem0001!=X463|skolem0004!=X464|shake_beverage(X463,X464),inference(resolution,[status(thm)],[c25, c47])).
% 0.47/0.71 cnf(c368,plain,skolem0001!=X465|shake_beverage(X465,skolem0004),inference(resolution,[status(thm)],[c302, reflexivity])).
% 0.47/0.71 cnf(c24,axiom,X319!=X321|X320!=X322|~beverage(X319,X320)|beverage(X321,X322),theory(equality)).
% 0.47/0.71 cnf(c297,plain,skolem0001!=X461|skolem0004!=X460|beverage(X461,X460),inference(resolution,[status(thm)],[c24, c207])).
% 0.47/0.71 cnf(c366,plain,skolem0001!=X462|beverage(X462,skolem0004),inference(resolution,[status(thm)],[c297, reflexivity])).
% 0.47/0.71 cnf(c23,axiom,X311!=X313|X312!=X314|~food(X311,X312)|food(X313,X314),theory(equality)).
% 0.47/0.71 cnf(c293,plain,skolem0001!=X458|skolem0004!=X457|food(X458,X457),inference(resolution,[status(thm)],[c23, c208])).
% 0.47/0.71 cnf(c364,plain,skolem0001!=X459|food(X459,skolem0004),inference(resolution,[status(thm)],[c293, reflexivity])).
% 0.47/0.71 cnf(c22,axiom,X302!=X304|X303!=X305|~substance_matter(X302,X303)|substance_matter(X304,X305),theory(equality)).
% 0.47/0.71 cnf(c289,plain,skolem0001!=X451|skolem0004!=X450|substance_matter(X451,X450),inference(resolution,[status(thm)],[c22, c209])).
% 0.47/0.71 cnf(c360,plain,skolem0001!=X456|substance_matter(X456,skolem0004),inference(resolution,[status(thm)],[c289, reflexivity])).
% 0.47/0.71 fof(ax21,axiom,(![U]:(![V]:(entity(U,V)=>specific(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax21)).
% 0.47/0.71 fof(c130,plain,(![U]:(![V]:(~entity(U,V)|specific(U,V)))),inference(fof_nnf,[status(thm)],[ax21])).
% 0.47/0.71 fof(c131,plain,(![X57]:(![X58]:(~entity(X57,X58)|specific(X57,X58)))),inference(variable_rename,[status(thm)],[c130])).
% 0.47/0.71 cnf(c132,plain,~entity(X180,X181)|specific(X180,X181),inference(split_conjunct,[status(thm)],[c131])).
% 0.47/0.71 cnf(c214,plain,specific(skolem0001,skolem0004),inference(resolution,[status(thm)],[c132, c211])).
% 0.47/0.71 cnf(c21,axiom,X292!=X294|X293!=X295|~specific(X292,X293)|specific(X294,X295),theory(equality)).
% 0.47/0.71 cnf(c284,plain,skolem0001!=X447|skolem0004!=X448|specific(X447,X448),inference(resolution,[status(thm)],[c21, c214])).
% 0.47/0.71 cnf(c358,plain,skolem0001!=X449|specific(X449,skolem0004),inference(resolution,[status(thm)],[c284, reflexivity])).
% 0.47/0.71 fof(ax31,axiom,(![U]:(![V]:(eventuality(U,V)=>specific(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax31)).
% 0.47/0.71 fof(c100,plain,(![U]:(![V]:(~eventuality(U,V)|specific(U,V)))),inference(fof_nnf,[status(thm)],[ax31])).
% 0.47/0.71 fof(c101,plain,(![X37]:(![X38]:(~eventuality(X37,X38)|specific(X37,X38)))),inference(variable_rename,[status(thm)],[c100])).
% 0.47/0.71 cnf(c102,plain,~eventuality(X145,X144)|specific(X145,X144),inference(split_conjunct,[status(thm)],[c101])).
% 0.47/0.71 cnf(c202,plain,specific(skolem0001,skolem0005),inference(resolution,[status(thm)],[c102, c199])).
% 0.47/0.71 cnf(c283,plain,skolem0001!=X440|skolem0005!=X441|specific(X440,X441),inference(resolution,[status(thm)],[c21, c202])).
% 0.47/0.71 cnf(c355,plain,skolem0001!=X442|specific(X442,skolem0005),inference(resolution,[status(thm)],[c283, reflexivity])).
% 0.47/0.71 cnf(c246,plain,specific(skolem0001,skolem0002),inference(resolution,[status(thm)],[c244, c132])).
% 0.47/0.71 cnf(c282,plain,skolem0001!=X437|skolem0002!=X438|specific(X437,X438),inference(resolution,[status(thm)],[c21, c246])).
% 0.47/0.71 cnf(c353,plain,skolem0001!=X439|specific(X439,skolem0002),inference(resolution,[status(thm)],[c282, reflexivity])).
% 0.47/0.71 fof(ax20,axiom,(![U]:(![V]:(entity(U,V)=>existent(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax20)).
% 0.47/0.71 fof(c133,plain,(![U]:(![V]:(~entity(U,V)|existent(U,V)))),inference(fof_nnf,[status(thm)],[ax20])).
% 0.47/0.71 fof(c134,plain,(![X59]:(![X60]:(~entity(X59,X60)|existent(X59,X60)))),inference(variable_rename,[status(thm)],[c133])).
% 0.47/0.71 cnf(c135,plain,~entity(X182,X183)|existent(X182,X183),inference(split_conjunct,[status(thm)],[c134])).
% 0.47/0.71 cnf(c215,plain,existent(skolem0001,skolem0004),inference(resolution,[status(thm)],[c135, c211])).
% 0.47/0.71 cnf(c20,axiom,X284!=X286|X285!=X287|~existent(X284,X285)|existent(X286,X287),theory(equality)).
% 0.47/0.71 cnf(c278,plain,skolem0001!=X430|skolem0004!=X431|existent(X430,X431),inference(resolution,[status(thm)],[c20, c215])).
% 0.47/0.71 cnf(c350,plain,skolem0001!=X432|existent(X432,skolem0004),inference(resolution,[status(thm)],[c278, reflexivity])).
% 0.47/0.71 cnf(c247,plain,existent(skolem0001,skolem0002),inference(resolution,[status(thm)],[c244, c135])).
% 0.47/0.71 cnf(c277,plain,skolem0001!=X421|skolem0002!=X422|existent(X421,X422),inference(resolution,[status(thm)],[c20, c247])).
% 0.47/0.71 cnf(c347,plain,skolem0001!=X429|existent(X429,skolem0002),inference(resolution,[status(thm)],[c277, reflexivity])).
% 0.47/0.71 fof(ax19,axiom,(![U]:(![V]:(object(U,V)=>nonliving(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax19)).
% 0.47/0.71 fof(c136,plain,(![U]:(![V]:(~object(U,V)|nonliving(U,V)))),inference(fof_nnf,[status(thm)],[ax19])).
% 0.47/0.71 fof(c137,plain,(![X61]:(![X62]:(~object(X61,X62)|nonliving(X61,X62)))),inference(variable_rename,[status(thm)],[c136])).
% 0.47/0.71 cnf(c138,plain,~object(X189,X188)|nonliving(X189,X188),inference(split_conjunct,[status(thm)],[c137])).
% 0.47/0.71 cnf(c217,plain,nonliving(skolem0001,skolem0004),inference(resolution,[status(thm)],[c138, c210])).
% 0.47/0.71 cnf(c19,axiom,X275!=X277|X276!=X278|~nonliving(X275,X276)|nonliving(X277,X278),theory(equality)).
% 0.47/0.71 cnf(c273,plain,skolem0001!=X419|skolem0004!=X418|nonliving(X419,X418),inference(resolution,[status(thm)],[c19, c217])).
% 0.47/0.71 cnf(c345,plain,skolem0001!=X420|nonliving(X420,skolem0004),inference(resolution,[status(thm)],[c273, reflexivity])).
% 0.47/0.71 cnf(c18,axiom,X263!=X265|X264!=X266|~object(X263,X264)|object(X265,X266),theory(equality)).
% 0.47/0.71 cnf(c269,plain,skolem0001!=X411|skolem0004!=X412|object(X411,X412),inference(resolution,[status(thm)],[c18, c210])).
% 0.47/0.71 cnf(c342,plain,skolem0001!=X413|object(X413,skolem0004),inference(resolution,[status(thm)],[c269, reflexivity])).
% 0.47/0.71 cnf(c1,axiom,X122!=X124|X123!=X125|~female(X122,X123)|female(X124,X125),theory(equality)).
% 0.47/0.71 fof(ax1,axiom,(![U]:(![V]:(woman(U,V)=>female(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax1)).
% 0.47/0.71 fof(c190,plain,(![U]:(![V]:(~woman(U,V)|female(U,V)))),inference(fof_nnf,[status(thm)],[ax1])).
% 0.47/0.71 fof(c191,plain,(![X97]:(![X98]:(~woman(X97,X98)|female(X97,X98)))),inference(variable_rename,[status(thm)],[c190])).
% 0.47/0.71 cnf(c192,plain,~woman(X261,X260)|female(X261,X260),inference(split_conjunct,[status(thm)],[c191])).
% 0.47/0.71 cnf(c266,plain,female(skolem0001,skolem0002),inference(resolution,[status(thm)],[c192, c44])).
% 0.47/0.71 cnf(c268,plain,skolem0001!=X408|skolem0002!=X409|female(X408,X409),inference(resolution,[status(thm)],[c266, c1])).
% 0.47/0.71 cnf(c340,plain,skolem0001!=X410|female(X410,skolem0002),inference(resolution,[status(thm)],[c268, reflexivity])).
% 0.47/0.71 cnf(c3,axiom,X140!=X142|X141!=X143|~animate(X140,X141)|animate(X142,X143),theory(equality)).
% 0.47/0.71 fof(ax2,axiom,(![U]:(![V]:(human_person(U,V)=>animate(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax2)).
% 0.47/0.71 fof(c187,plain,(![U]:(![V]:(~human_person(U,V)|animate(U,V)))),inference(fof_nnf,[status(thm)],[ax2])).
% 0.47/0.71 fof(c188,plain,(![X95]:(![X96]:(~human_person(X95,X96)|animate(X95,X96)))),inference(variable_rename,[status(thm)],[c187])).
% 0.47/0.71 cnf(c189,plain,~human_person(X254,X255)|animate(X254,X255),inference(split_conjunct,[status(thm)],[c188])).
% 0.47/0.71 cnf(c263,plain,animate(skolem0001,skolem0002),inference(resolution,[status(thm)],[c189, c239])).
% 0.47/0.71 cnf(c265,plain,skolem0001!=X399|skolem0002!=X400|animate(X399,X400),inference(resolution,[status(thm)],[c263, c3])).
% 0.47/0.71 cnf(c337,plain,skolem0001!=X401|animate(X401,skolem0002),inference(resolution,[status(thm)],[c265, reflexivity])).
% 0.47/0.71 cnf(c17,axiom,X256!=X258|X257!=X259|~relname(X256,X257)|relname(X258,X259),theory(equality)).
% 0.47/0.71 cnf(c264,plain,skolem0001!=X391|skolem0003!=X390|relname(X391,X390),inference(resolution,[status(thm)],[c17, c223])).
% 0.47/0.71 cnf(c334,plain,skolem0001!=X398|relname(X398,skolem0003),inference(resolution,[status(thm)],[c264, reflexivity])).
% 0.47/0.71 cnf(c4,axiom,X148!=X150|X149!=X151|~human(X148,X149)|human(X150,X151),theory(equality)).
% 0.47/0.71 fof(ax3,axiom,(![U]:(![V]:(human_person(U,V)=>human(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax3)).
% 0.47/0.71 fof(c184,plain,(![U]:(![V]:(~human_person(U,V)|human(U,V)))),inference(fof_nnf,[status(thm)],[ax3])).
% 0.47/0.71 fof(c185,plain,(![X93]:(![X94]:(~human_person(X93,X94)|human(X93,X94)))),inference(variable_rename,[status(thm)],[c184])).
% 0.47/0.71 cnf(c186,plain,~human_person(X253,X252)|human(X253,X252),inference(split_conjunct,[status(thm)],[c185])).
% 0.47/0.71 cnf(c260,plain,human(skolem0001,skolem0002),inference(resolution,[status(thm)],[c186, c239])).
% 0.47/0.71 cnf(c261,plain,skolem0001!=X388|skolem0002!=X387|human(X388,X387),inference(resolution,[status(thm)],[c260, c4])).
% 0.47/0.71 cnf(c332,plain,skolem0001!=X389|human(X389,skolem0002),inference(resolution,[status(thm)],[c261, reflexivity])).
% 0.47/0.71 cnf(c16,axiom,X248!=X250|X249!=X251|~relation(X248,X249)|relation(X250,X251),theory(equality)).
% 0.47/0.71 cnf(c259,plain,skolem0001!=X380|skolem0003!=X381|relation(X380,X381),inference(resolution,[status(thm)],[c16, c225])).
% 0.47/0.71 cnf(c329,plain,skolem0001!=X382|relation(X382,skolem0003),inference(resolution,[status(thm)],[c259, reflexivity])).
% 0.47/0.71 cnf(c6,axiom,X166!=X168|X167!=X169|~living(X166,X167)|living(X168,X169),theory(equality)).
% 0.47/0.71 fof(ax4,axiom,(![U]:(![V]:(organism(U,V)=>living(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax4)).
% 0.47/0.71 fof(c181,plain,(![U]:(![V]:(~organism(U,V)|living(U,V)))),inference(fof_nnf,[status(thm)],[ax4])).
% 0.47/0.71 fof(c182,plain,(![X91]:(![X92]:(~organism(X91,X92)|living(X91,X92)))),inference(variable_rename,[status(thm)],[c181])).
% 0.47/0.71 cnf(c183,plain,~organism(X246,X247)|living(X246,X247),inference(split_conjunct,[status(thm)],[c182])).
% 0.47/0.71 cnf(c256,plain,living(skolem0001,skolem0002),inference(resolution,[status(thm)],[c183, c241])).
% 0.47/0.71 cnf(c258,plain,skolem0001!=X377|skolem0002!=X378|living(X377,X378),inference(resolution,[status(thm)],[c256, c6])).
% 0.47/0.71 cnf(c327,plain,skolem0001!=X379|living(X379,skolem0002),inference(resolution,[status(thm)],[c258, reflexivity])).
% 0.47/0.71 cnf(c7,axiom,X176!=X178|X177!=X179|~impartial(X176,X177)|impartial(X178,X179),theory(equality)).
% 0.47/0.71 fof(ax5,axiom,(![U]:(![V]:(organism(U,V)=>impartial(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax5)).
% 0.47/0.71 fof(c178,plain,(![U]:(![V]:(~organism(U,V)|impartial(U,V)))),inference(fof_nnf,[status(thm)],[ax5])).
% 0.47/0.71 fof(c179,plain,(![X89]:(![X90]:(~organism(X89,X90)|impartial(X89,X90)))),inference(variable_rename,[status(thm)],[c178])).
% 0.47/0.71 cnf(c180,plain,~organism(X244,X245)|impartial(X244,X245),inference(split_conjunct,[status(thm)],[c179])).
% 0.47/0.71 cnf(c254,plain,impartial(skolem0001,skolem0002),inference(resolution,[status(thm)],[c180, c241])).
% 0.47/0.71 cnf(c255,plain,skolem0001!=X370|skolem0002!=X371|impartial(X370,X371),inference(resolution,[status(thm)],[c254, c7])).
% 0.47/0.71 cnf(c321,plain,skolem0001!=X372|impartial(X372,skolem0002),inference(resolution,[status(thm)],[c255, reflexivity])).
% 0.47/0.71 cnf(c15,axiom,X240!=X242|X241!=X243|~thing(X240,X241)|thing(X242,X243),theory(equality)).
% 0.47/0.71 cnf(c253,plain,skolem0001!=X363|skolem0002!=X364|thing(X363,X364),inference(resolution,[status(thm)],[c15, c245])).
% 0.47/0.71 cnf(c318,plain,skolem0001!=X369|thing(X369,skolem0002),inference(resolution,[status(thm)],[c253, reflexivity])).
% 0.47/0.71 cnf(c252,plain,skolem0001!=X360|skolem0004!=X361|thing(X360,X361),inference(resolution,[status(thm)],[c15, c212])).
% 0.47/0.71 cnf(c316,plain,skolem0001!=X362|thing(X362,skolem0004),inference(resolution,[status(thm)],[c252, reflexivity])).
% 0.47/0.71 cnf(c251,plain,skolem0001!=X353|skolem0003!=X354|thing(X353,X354),inference(resolution,[status(thm)],[c15, c227])).
% 0.47/0.71 cnf(c313,plain,skolem0001!=X355|thing(X355,skolem0003),inference(resolution,[status(thm)],[c251, reflexivity])).
% 0.47/0.71 cnf(c250,plain,skolem0001!=X350|skolem0005!=X351|thing(X350,X351),inference(resolution,[status(thm)],[c15, c200])).
% 0.47/0.71 cnf(c311,plain,skolem0001!=X352|thing(X352,skolem0005),inference(resolution,[status(thm)],[c250, reflexivity])).
% 0.47/0.71 cnf(c8,axiom,X184!=X186|X185!=X187|~entity(X184,X185)|entity(X186,X187),theory(equality)).
% 0.47/0.71 cnf(c248,plain,skolem0001!=X344|skolem0002!=X343|entity(X344,X343),inference(resolution,[status(thm)],[c244, c8])).
% 0.47/0.71 cnf(c308,plain,skolem0001!=X345|entity(X345,skolem0002),inference(resolution,[status(thm)],[c248, reflexivity])).
% 0.47/0.71 fof(ax12,axiom,(![U]:(![V]:(abstraction(U,V)=>nonhuman(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax12)).
% 0.47/0.71 fof(c157,plain,(![U]:(![V]:(~abstraction(U,V)|nonhuman(U,V)))),inference(fof_nnf,[status(thm)],[ax12])).
% 0.47/0.71 fof(c158,plain,(![X75]:(![X76]:(~abstraction(X75,X76)|nonhuman(X75,X76)))),inference(variable_rename,[status(thm)],[c157])).
% 0.47/0.71 cnf(c159,plain,~abstraction(X214,X215)|nonhuman(X214,X215),inference(split_conjunct,[status(thm)],[c158])).
% 0.47/0.71 cnf(c230,plain,nonhuman(skolem0001,skolem0003),inference(resolution,[status(thm)],[c159, c226])).
% 0.47/0.71 cnf(c14,axiom,X234!=X236|X235!=X237|~nonhuman(X234,X235)|nonhuman(X236,X237),theory(equality)).
% 0.47/0.71 cnf(c243,plain,skolem0001!=X337|skolem0003!=X336|nonhuman(X337,X336),inference(resolution,[status(thm)],[c14, c230])).
% 0.47/0.71 cnf(c305,plain,skolem0001!=X342|nonhuman(X342,skolem0003),inference(resolution,[status(thm)],[c243, reflexivity])).
% 0.47/0.71 cnf(c5,axiom,X158!=X160|X159!=X161|~organism(X158,X159)|organism(X160,X161),theory(equality)).
% 0.47/0.71 cnf(c242,plain,skolem0001!=X334|skolem0002!=X333|organism(X334,X333),inference(resolution,[status(thm)],[c241, c5])).
% 0.47/0.71 cnf(c303,plain,skolem0001!=X335|organism(X335,skolem0002),inference(resolution,[status(thm)],[c242, reflexivity])).
% 0.47/0.71 cnf(c2,axiom,X132!=X134|X133!=X135|~human_person(X132,X133)|human_person(X134,X135),theory(equality)).
% 0.47/0.71 cnf(c240,plain,skolem0001!=X326|skolem0002!=X327|human_person(X326,X327),inference(resolution,[status(thm)],[c239, c2])).
% 0.47/0.71 cnf(c300,plain,skolem0001!=X328|human_person(X328,skolem0002),inference(resolution,[status(thm)],[c240, reflexivity])).
% 0.47/0.71 fof(ax11,axiom,(![U]:(![V]:(abstraction(U,V)=>general(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax11)).
% 0.47/0.71 fof(c160,plain,(![U]:(![V]:(~abstraction(U,V)|general(U,V)))),inference(fof_nnf,[status(thm)],[ax11])).
% 0.47/0.71 fof(c161,plain,(![X77]:(![X78]:(~abstraction(X77,X78)|general(X77,X78)))),inference(variable_rename,[status(thm)],[c160])).
% 0.47/0.71 cnf(c162,plain,~abstraction(X216,X217)|general(X216,X217),inference(split_conjunct,[status(thm)],[c161])).
% 0.47/0.71 cnf(c231,plain,general(skolem0001,skolem0003),inference(resolution,[status(thm)],[c162, c226])).
% 0.47/0.71 cnf(c13,axiom,X226!=X228|X227!=X229|~general(X226,X227)|general(X228,X229),theory(equality)).
% 0.47/0.71 cnf(c238,plain,skolem0001!=X323|skolem0003!=X324|general(X323,X324),inference(resolution,[status(thm)],[c13, c231])).
% 0.47/0.71 cnf(c298,plain,skolem0001!=X325|general(X325,skolem0003),inference(resolution,[status(thm)],[c238, reflexivity])).
% 0.47/0.71 cnf(c12,axiom,X218!=X220|X219!=X221|~unisex(X218,X219)|unisex(X220,X221),theory(equality)).
% 0.47/0.71 fof(ax10,axiom,(![U]:(![V]:(abstraction(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax10)).
% 0.47/0.71 fof(c163,plain,(![U]:(![V]:(~abstraction(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax10])).
% 0.47/0.71 fof(c164,plain,(![X79]:(![X80]:(~abstraction(X79,X80)|unisex(X79,X80)))),inference(variable_rename,[status(thm)],[c163])).
% 0.47/0.71 cnf(c165,plain,~abstraction(X223,X222)|unisex(X223,X222),inference(split_conjunct,[status(thm)],[c164])).
% 0.47/0.71 cnf(c235,plain,unisex(skolem0001,skolem0003),inference(resolution,[status(thm)],[c165, c226])).
% 0.47/0.71 cnf(c236,plain,skolem0001!=X317|skolem0003!=X316|unisex(X317,X316),inference(resolution,[status(thm)],[c235, c12])).
% 0.47/0.71 cnf(c295,plain,skolem0001!=X318|unisex(X318,skolem0003),inference(resolution,[status(thm)],[c236, reflexivity])).
% 0.47/0.71 fof(ax29,axiom,(![U]:(![V]:(eventuality(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax29)).
% 0.47/0.71 fof(c106,plain,(![U]:(![V]:(~eventuality(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax29])).
% 0.47/0.71 fof(c107,plain,(![X41]:(![X42]:(~eventuality(X41,X42)|unisex(X41,X42)))),inference(variable_rename,[status(thm)],[c106])).
% 0.47/0.71 cnf(c108,plain,~eventuality(X152,X153)|unisex(X152,X153),inference(split_conjunct,[status(thm)],[c107])).
% 0.47/0.71 cnf(c205,plain,unisex(skolem0001,skolem0005),inference(resolution,[status(thm)],[c108, c199])).
% 0.47/0.71 cnf(c233,plain,skolem0001!=X310|skolem0005!=X309|unisex(X310,X309),inference(resolution,[status(thm)],[c12, c205])).
% 0.47/0.71 cnf(c292,plain,skolem0001!=X315|unisex(X315,skolem0005),inference(resolution,[status(thm)],[c233, reflexivity])).
% 0.47/0.71 fof(ax17,axiom,(![U]:(![V]:(object(U,V)=>unisex(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax17)).
% 0.47/0.71 fof(c142,plain,(![U]:(![V]:(~object(U,V)|unisex(U,V)))),inference(fof_nnf,[status(thm)],[ax17])).
% 0.47/0.71 fof(c143,plain,(![X65]:(![X66]:(~object(X65,X66)|unisex(X65,X66)))),inference(variable_rename,[status(thm)],[c142])).
% 0.47/0.71 cnf(c144,plain,~object(X197,X196)|unisex(X197,X196),inference(split_conjunct,[status(thm)],[c143])).
% 0.47/0.71 cnf(c222,plain,unisex(skolem0001,skolem0004),inference(resolution,[status(thm)],[c144, c210])).
% 0.47/0.71 cnf(c232,plain,skolem0001!=X307|skolem0004!=X306|unisex(X307,X306),inference(resolution,[status(thm)],[c12, c222])).
% 0.47/0.71 cnf(c290,plain,skolem0001!=X308|unisex(X308,skolem0004),inference(resolution,[status(thm)],[c232, reflexivity])).
% 0.47/0.71 cnf(c11,axiom,X210!=X212|X211!=X213|~abstraction(X210,X211)|abstraction(X212,X213),theory(equality)).
% 0.47/0.71 cnf(c228,plain,skolem0001!=X299|skolem0003!=X300|abstraction(X299,X300),inference(resolution,[status(thm)],[c11, c226])).
% 0.47/0.71 cnf(c287,plain,skolem0001!=X301|abstraction(X301,skolem0003),inference(resolution,[status(thm)],[c228, reflexivity])).
% 0.47/0.71 cnf(c10,axiom,X200!=X202|X201!=X203|~forename(X200,X201)|forename(X202,X203),theory(equality)).
% 0.47/0.71 cnf(c224,plain,skolem0001!=X297|skolem0003!=X296|forename(X297,X296),inference(resolution,[status(thm)],[c10, c46])).
% 0.47/0.71 cnf(c285,plain,skolem0001!=X298|forename(X298,skolem0003),inference(resolution,[status(thm)],[c224, reflexivity])).
% 0.47/0.71 fof(ax18,axiom,(![U]:(![V]:(object(U,V)=>impartial(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax18)).
% 0.47/0.71 fof(c139,plain,(![U]:(![V]:(~object(U,V)|impartial(U,V)))),inference(fof_nnf,[status(thm)],[ax18])).
% 0.47/0.71 fof(c140,plain,(![X63]:(![X64]:(~object(X63,X64)|impartial(X63,X64)))),inference(variable_rename,[status(thm)],[c139])).
% 0.47/0.71 cnf(c141,plain,~object(X190,X191)|impartial(X190,X191),inference(split_conjunct,[status(thm)],[c140])).
% 0.47/0.71 cnf(c219,plain,impartial(skolem0001,skolem0004),inference(resolution,[status(thm)],[c141, c210])).
% 0.47/0.71 cnf(c221,plain,skolem0001!=X289|skolem0004!=X290|impartial(X289,X290),inference(resolution,[status(thm)],[c219, c7])).
% 0.47/0.71 cnf(c280,plain,skolem0001!=X291|impartial(X291,skolem0004),inference(resolution,[status(thm)],[c221, reflexivity])).
% 0.47/0.71 cnf(c45,negated_conjecture,mia_forename(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c41])).
% 0.47/0.71 cnf(c9,axiom,X192!=X194|X193!=X195|~mia_forename(X192,X193)|mia_forename(X194,X195),theory(equality)).
% 0.47/0.71 cnf(c220,plain,skolem0001!=X283|skolem0003!=X282|mia_forename(X283,X282),inference(resolution,[status(thm)],[c9, c45])).
% 0.47/0.71 cnf(c276,plain,skolem0001!=X288|mia_forename(X288,skolem0003),inference(resolution,[status(thm)],[c220, reflexivity])).
% 0.47/0.71 cnf(c216,plain,skolem0001!=X280|skolem0004!=X279|entity(X280,X279),inference(resolution,[status(thm)],[c8, c211])).
% 0.47/0.71 cnf(c274,plain,skolem0001!=X281|entity(X281,skolem0004),inference(resolution,[status(thm)],[c216, reflexivity])).
% 0.47/0.71 cnf(c0,axiom,X108!=X110|X109!=X111|~woman(X108,X109)|woman(X110,X111),theory(equality)).
% 0.47/0.71 cnf(c196,plain,skolem0001!=X272|skolem0002!=X273|woman(X272,X273),inference(resolution,[status(thm)],[c0, c44])).
% 0.47/0.71 cnf(c271,plain,skolem0001!=X274|woman(X274,skolem0002),inference(resolution,[status(thm)],[c196, reflexivity])).
% 0.47/0.71 cnf(c36,axiom,X269!=X270|~actual_world(X269)|actual_world(X270),theory(equality)).
% 0.47/0.71 fof(ax42,axiom,(![U]:(![V]:(unisex(U,V)=>(~female(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax42)).
% 0.47/0.71 fof(c61,plain,(![U]:(![V]:(unisex(U,V)=>~female(U,V)))),inference(fof_simplification,[status(thm)],[ax42])).
% 0.47/0.71 fof(c62,plain,(![U]:(![V]:(~unisex(U,V)|~female(U,V)))),inference(fof_nnf,[status(thm)],[c61])).
% 0.47/0.71 fof(c63,plain,(![X15]:(![X16]:(~unisex(X15,X16)|~female(X15,X16)))),inference(variable_rename,[status(thm)],[c62])).
% 0.47/0.71 cnf(c64,plain,~unisex(X106,X107)|~female(X106,X107),inference(split_conjunct,[status(thm)],[c63])).
% 0.47/0.71 cnf(c267,plain,~unisex(skolem0001,skolem0002),inference(resolution,[status(thm)],[c266, c64])).
% 0.47/0.71 fof(ax39,axiom,(![U]:(![V]:(nonhuman(U,V)=>(~human(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax39)).
% 0.47/0.71 fof(c73,plain,(![U]:(![V]:(nonhuman(U,V)=>~human(U,V)))),inference(fof_simplification,[status(thm)],[ax39])).
% 0.47/0.71 fof(c74,plain,(![U]:(![V]:(~nonhuman(U,V)|~human(U,V)))),inference(fof_nnf,[status(thm)],[c73])).
% 0.47/0.71 fof(c75,plain,(![X21]:(![X22]:(~nonhuman(X21,X22)|~human(X21,X22)))),inference(variable_rename,[status(thm)],[c74])).
% 0.47/0.71 cnf(c76,plain,~nonhuman(X117,X116)|~human(X117,X116),inference(split_conjunct,[status(thm)],[c75])).
% 0.47/0.71 cnf(c262,plain,~nonhuman(skolem0001,skolem0002),inference(resolution,[status(thm)],[c260, c76])).
% 0.47/0.71 fof(ax40,axiom,(![U]:(![V]:(nonliving(U,V)=>(~living(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax40)).
% 0.47/0.71 fof(c69,plain,(![U]:(![V]:(nonliving(U,V)=>~living(U,V)))),inference(fof_simplification,[status(thm)],[ax40])).
% 0.47/0.71 fof(c70,plain,(![U]:(![V]:(~nonliving(U,V)|~living(U,V)))),inference(fof_nnf,[status(thm)],[c69])).
% 0.47/0.71 fof(c71,plain,(![X19]:(![X20]:(~nonliving(X19,X20)|~living(X19,X20)))),inference(variable_rename,[status(thm)],[c70])).
% 0.47/0.71 cnf(c72,plain,~nonliving(X115,X114)|~living(X115,X114),inference(split_conjunct,[status(thm)],[c71])).
% 0.47/0.71 cnf(c257,plain,~nonliving(skolem0001,skolem0002),inference(resolution,[status(thm)],[c256, c72])).
% 0.47/0.71 fof(ax9,axiom,(![U]:(![V]:(mia_forename(U,V)=>forename(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax9)).
% 0.47/0.71 fof(c166,plain,(![U]:(![V]:(~mia_forename(U,V)|forename(U,V)))),inference(fof_nnf,[status(thm)],[ax9])).
% 0.47/0.71 fof(c167,plain,(![X81]:(![X82]:(~mia_forename(X81,X82)|forename(X81,X82)))),inference(variable_rename,[status(thm)],[c166])).
% 0.47/0.71 cnf(c168,plain,~mia_forename(X225,X224)|forename(X225,X224),inference(split_conjunct,[status(thm)],[c167])).
% 0.47/0.71 fof(ax41,axiom,(![U]:(![V]:(specific(U,V)=>(~general(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax41)).
% 0.47/0.71 fof(c65,plain,(![U]:(![V]:(specific(U,V)=>~general(U,V)))),inference(fof_simplification,[status(thm)],[ax41])).
% 0.47/0.71 fof(c66,plain,(![U]:(![V]:(~specific(U,V)|~general(U,V)))),inference(fof_nnf,[status(thm)],[c65])).
% 0.47/0.71 fof(c67,plain,(![X17]:(![X18]:(~specific(X17,X18)|~general(X17,X18)))),inference(variable_rename,[status(thm)],[c66])).
% 0.47/0.71 cnf(c68,plain,~specific(X113,X112)|~general(X113,X112),inference(split_conjunct,[status(thm)],[c67])).
% 0.47/0.71 cnf(c234,plain,~specific(skolem0001,skolem0003),inference(resolution,[status(thm)],[c231, c68])).
% 0.47/0.71 fof(ax37,axiom,(![U]:(![V]:(animate(U,V)=>(~nonliving(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax37)).
% 0.47/0.71 fof(c81,plain,(![U]:(![V]:(animate(U,V)=>~nonliving(U,V)))),inference(fof_simplification,[status(thm)],[ax37])).
% 0.47/0.71 fof(c82,plain,(![U]:(![V]:(~animate(U,V)|~nonliving(U,V)))),inference(fof_nnf,[status(thm)],[c81])).
% 0.47/0.71 fof(c83,plain,(![X25]:(![X26]:(~animate(X25,X26)|~nonliving(X25,X26)))),inference(variable_rename,[status(thm)],[c82])).
% 0.47/0.71 cnf(c84,plain,~animate(X120,X121)|~nonliving(X120,X121),inference(split_conjunct,[status(thm)],[c83])).
% 0.47/0.71 cnf(c218,plain,~animate(skolem0001,skolem0004),inference(resolution,[status(thm)],[c217, c84])).
% 0.47/0.71 fof(ax28,axiom,(![U]:(![V]:(order(U,V)=>event(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax28)).
% 0.47/0.71 fof(c109,plain,(![U]:(![V]:(~order(U,V)|event(U,V)))),inference(fof_nnf,[status(thm)],[ax28])).
% 0.47/0.71 fof(c110,plain,(![X43]:(![X44]:(~order(X43,X44)|event(X43,X44)))),inference(variable_rename,[status(thm)],[c109])).
% 0.47/0.71 cnf(c111,plain,~order(X154,X155)|event(X154,X155),inference(split_conjunct,[status(thm)],[c110])).
% 0.47/0.71 fof(ax38,axiom,(![U]:(![V]:(existent(U,V)=>(~nonexistent(U,V))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax38)).
% 0.47/0.71 fof(c77,plain,(![U]:(![V]:(existent(U,V)=>~nonexistent(U,V)))),inference(fof_simplification,[status(thm)],[ax38])).
% 0.47/0.71 fof(c78,plain,(![U]:(![V]:(~existent(U,V)|~nonexistent(U,V)))),inference(fof_nnf,[status(thm)],[c77])).
% 0.47/0.71 fof(c79,plain,(![X23]:(![X24]:(~existent(X23,X24)|~nonexistent(X23,X24)))),inference(variable_rename,[status(thm)],[c78])).
% 0.47/0.71 cnf(c80,plain,~existent(X119,X118)|~nonexistent(X119,X118),inference(split_conjunct,[status(thm)],[c79])).
% 0.47/0.71 cnf(c204,plain,~existent(skolem0001,skolem0005),inference(resolution,[status(thm)],[c203, c80])).
% 0.47/0.71 fof(ax35,axiom,(![U]:(![V]:(act(U,V)=>event(U,V)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', ax35)).
% 0.47/0.71 fof(c88,plain,(![U]:(![V]:(~act(U,V)|event(U,V)))),inference(fof_nnf,[status(thm)],[ax35])).
% 0.47/0.71 fof(c89,plain,(![X29]:(![X30]:(~act(X29,X30)|event(X29,X30)))),inference(variable_rename,[status(thm)],[c88])).
% 0.47/0.71 cnf(c90,plain,~act(X129,X128)|event(X129,X128),inference(split_conjunct,[status(thm)],[c89])).
% 0.47/0.71 cnf(transitivity,axiom,X105!=X104|X104!=X103|X105=X103,theory(equality)).
% 0.47/0.71 cnf(symmetry,axiom,X101!=X100|X100=X101,theory(equality)).
% 0.47/0.71 cnf(c42,negated_conjecture,actual_world(skolem0001),inference(split_conjunct,[status(thm)],[c41])).
% 0.47/0.71 % SZS output end Saturation
% 0.47/0.71
% 0.47/0.71 % Initial clauses : 97
% 0.47/0.71 % Processed clauses : 248
% 0.47/0.71 % Factors computed : 2
% 0.47/0.71 % Resolvents computed: 208
% 0.47/0.71 % Tautologies deleted: 3
% 0.47/0.71 % Forward subsumed : 56
% 0.47/0.71 % Backward subsumed : 0
% 0.47/0.71 % -------- CPU Time ---------
% 0.47/0.71 % User time : 0.362 s
% 0.47/0.71 % System time : 0.020 s
% 0.47/0.71 % Total time : 0.382 s
%------------------------------------------------------------------------------