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