%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PHI037+1 : TPTP v8.1.2. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n004.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:37:19 EDT 2024
% Result : CounterSatisfiable 1.38s 1.56s
% Output : Saturation 1.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : PHI037+1 : TPTP v8.1.2. Released v7.4.0.
% 0.07/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n004.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed May 8 22:29:53 EDT 2024
% 0.14/0.35 % CPUTime :
% 1.38/1.56 % Version: 1.5
% 1.38/1.56 % SZS status CounterSatisfiable
% 1.38/1.56 % SZS output start Saturation
% 1.38/1.56 cnf(reflexivity,axiom,X62=X62,theory(equality)).
% 1.38/1.56 cnf(c1,axiom,X90!=X89|X92!=X91|~existsIn(X90,X92)|existsIn(X89,X91),theory(equality)).
% 1.38/1.56 fof(exists,axiom,(![X]:(![Y]:(exists(X)<=>(existsIn(X,X)|(existsIn(X,Y)&X!=Y))))),file('/export/starexec/sandbox/benchmark/Axioms/PHI002+1.ax', exists)).
% 1.38/1.56 fof(c187,plain,(![X]:(![Y]:((~exists(X)|(existsIn(X,X)|(existsIn(X,Y)&X!=Y)))&((~existsIn(X,X)&(~existsIn(X,Y)|X=Y))|exists(X))))),inference(fof_nnf,[status(thm)],[exists])).
% 1.38/1.56 fof(c188,plain,((![X]:(~exists(X)|(existsIn(X,X)|((![Y]:existsIn(X,Y))&(![Y]:X!=Y)))))&(![X]:((~existsIn(X,X)&(![Y]:(~existsIn(X,Y)|X=Y)))|exists(X)))),inference(shift_quantors,[status(thm)],[c187])).
% 1.38/1.56 fof(c190,plain,(![X57]:(![X58]:(![X59]:(![X60]:(![X61]:((~exists(X57)|(existsIn(X57,X57)|(existsIn(X57,X58)&X57!=X59)))&((~existsIn(X60,X60)&(~existsIn(X60,X61)|X60=X61))|exists(X60)))))))),inference(shift_quantors,[status(thm)],[fof(c189,plain,((![X57]:(~exists(X57)|(existsIn(X57,X57)|((![X58]:existsIn(X57,X58))&(![X59]:X57!=X59)))))&(![X60]:((~existsIn(X60,X60)&(![X61]:(~existsIn(X60,X61)|X60=X61)))|exists(X60)))),inference(variable_rename,[status(thm)],[c188])).])).
% 1.38/1.56 fof(c191,plain,(![X57]:(![X58]:(![X59]:(![X60]:(![X61]:(((~exists(X57)|(existsIn(X57,X57)|existsIn(X57,X58)))&(~exists(X57)|(existsIn(X57,X57)|X57!=X59)))&((~existsIn(X60,X60)|exists(X60))&((~existsIn(X60,X61)|X60=X61)|exists(X60))))))))),inference(distribute,[status(thm)],[c190])).
% 1.38/1.56 cnf(c193,plain,~exists(X297)|existsIn(X297,X297)|X297!=X296,inference(split_conjunct,[status(thm)],[c191])).
% 1.38/1.56 cnf(c232,plain,~exists(X298)|existsIn(X298,X298),inference(resolution,[status(thm)],[c193, reflexivity])).
% 1.38/1.56 cnf(c0,axiom,X83!=X82|~exists(X83)|exists(X82),theory(equality)).
% 1.38/1.56 cnf(symmetry,axiom,X67!=X68|X68=X67,theory(equality)).
% 1.38/1.56 cnf(c195,plain,~existsIn(X300,X299)|X300=X299|exists(X300),inference(split_conjunct,[status(thm)],[c191])).
% 1.38/1.56 fof(mode,conjecture,(![X]:(![Y]:(![Z]:(mode(X)<=>((modification(X,Y)&substance(Y))|(existsIn(X,Z)&conceivedThru(X,Z))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', mode)).
% 1.38/1.56 fof(c105,negated_conjecture,(~(![X]:(![Y]:(![Z]:(mode(X)<=>((modification(X,Y)&substance(Y))|(existsIn(X,Z)&conceivedThru(X,Z)))))))),inference(assume_negation,[status(cth)],[mode])).
% 1.38/1.56 fof(c106,negated_conjecture,(?[X]:(?[Y]:(?[Z]:((~mode(X)|((~modification(X,Y)|~substance(Y))&(~existsIn(X,Z)|~conceivedThru(X,Z))))&(mode(X)|((modification(X,Y)&substance(Y))|(existsIn(X,Z)&conceivedThru(X,Z)))))))),inference(fof_nnf,[status(thm)],[c105])).
% 1.38/1.56 fof(c107,negated_conjecture,(?[X27]:(?[X28]:(?[X29]:((~mode(X27)|((~modification(X27,X28)|~substance(X28))&(~existsIn(X27,X29)|~conceivedThru(X27,X29))))&(mode(X27)|((modification(X27,X28)&substance(X28))|(existsIn(X27,X29)&conceivedThru(X27,X29)))))))),inference(variable_rename,[status(thm)],[c106])).
% 1.38/1.56 fof(c108,negated_conjecture,((~mode(skolem0001)|((~modification(skolem0001,skolem0002)|~substance(skolem0002))&(~existsIn(skolem0001,skolem0003)|~conceivedThru(skolem0001,skolem0003))))&(mode(skolem0001)|((modification(skolem0001,skolem0002)&substance(skolem0002))|(existsIn(skolem0001,skolem0003)&conceivedThru(skolem0001,skolem0003))))),inference(skolemize,[status(esa)],[c107])).
% 1.38/1.56 fof(c109,negated_conjecture,(((~mode(skolem0001)|(~modification(skolem0001,skolem0002)|~substance(skolem0002)))&(~mode(skolem0001)|(~existsIn(skolem0001,skolem0003)|~conceivedThru(skolem0001,skolem0003))))&(((mode(skolem0001)|(modification(skolem0001,skolem0002)|existsIn(skolem0001,skolem0003)))&(mode(skolem0001)|(modification(skolem0001,skolem0002)|conceivedThru(skolem0001,skolem0003))))&((mode(skolem0001)|(substance(skolem0002)|existsIn(skolem0001,skolem0003)))&(mode(skolem0001)|(substance(skolem0002)|conceivedThru(skolem0001,skolem0003)))))),inference(distribute,[status(thm)],[c108])).
% 1.38/1.56 cnf(c112,negated_conjecture,mode(skolem0001)|modification(skolem0001,skolem0002)|existsIn(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c109])).
% 1.38/1.56 cnf(c293,plain,mode(skolem0001)|modification(skolem0001,skolem0002)|skolem0001=skolem0003|exists(skolem0001),inference(resolution,[status(thm)],[c112, c195])).
% 1.38/1.56 cnf(c1180,plain,mode(skolem0001)|modification(skolem0001,skolem0002)|exists(skolem0001)|skolem0003=skolem0001,inference(resolution,[status(thm)],[c293, symmetry])).
% 1.38/1.56 cnf(c1399,plain,mode(skolem0001)|modification(skolem0001,skolem0002)|exists(skolem0001)|~exists(skolem0003),inference(resolution,[status(thm)],[c1180, c0])).
% 1.38/1.56 cnf(c194,plain,~existsIn(X115,X115)|exists(X115),inference(split_conjunct,[status(thm)],[c191])).
% 1.38/1.56 cnf(c292,plain,mode(skolem0001)|modification(skolem0001,skolem0002)|skolem0001!=X379|skolem0003!=X378|existsIn(X379,X378),inference(resolution,[status(thm)],[c112, c1])).
% 1.38/1.56 cnf(c1163,plain,mode(skolem0001)|modification(skolem0001,skolem0002)|skolem0001!=X474|existsIn(X474,skolem0003),inference(resolution,[status(thm)],[c292, reflexivity])).
% 1.38/1.56 cnf(c1353,plain,mode(skolem0001)|modification(skolem0001,skolem0002)|existsIn(skolem0003,skolem0003)|exists(skolem0001),inference(resolution,[status(thm)],[c1163, c293])).
% 1.38/1.56 cnf(c1428,plain,mode(skolem0001)|modification(skolem0001,skolem0002)|exists(skolem0001)|exists(skolem0003),inference(resolution,[status(thm)],[c1353, c194])).
% 1.38/1.56 cnf(c1436,plain,mode(skolem0001)|modification(skolem0001,skolem0002)|exists(skolem0001),inference(resolution,[status(thm)],[c1428, c1399])).
% 1.38/1.56 cnf(c1439,plain,mode(skolem0001)|modification(skolem0001,skolem0002)|existsIn(skolem0001,skolem0001),inference(resolution,[status(thm)],[c1436, c232])).
% 1.38/1.56 cnf(c1443,plain,mode(skolem0001)|modification(skolem0001,skolem0002)|skolem0001!=X616|skolem0001!=X615|existsIn(X616,X615),inference(resolution,[status(thm)],[c1439, c1])).
% 1.38/1.56 cnf(c1498,plain,mode(skolem0001)|modification(skolem0001,skolem0002)|skolem0001!=X618|existsIn(X618,skolem0001),inference(resolution,[status(thm)],[c1443, reflexivity])).
% 1.38/1.56 cnf(c1497,plain,mode(skolem0001)|modification(skolem0001,skolem0002)|skolem0001!=X617|existsIn(X617,X617),inference(factor,[status(thm)],[c1443])).
% 1.38/1.56 cnf(c27,axiom,X251!=X250|X253!=X252|~modification(X251,X253)|modification(X250,X252),theory(equality)).
% 1.38/1.56 cnf(c1441,plain,mode(skolem0001)|existsIn(skolem0001,skolem0001)|skolem0001!=X611|skolem0002!=X612|modification(X611,X612),inference(resolution,[status(thm)],[c1439, c27])).
% 1.38/1.56 cnf(c1495,plain,mode(skolem0001)|existsIn(skolem0001,skolem0001)|skolem0001!=X613|modification(X613,skolem0002),inference(resolution,[status(thm)],[c1441, reflexivity])).
% 1.38/1.56 fof(self_caused,axiom,(![X]:(selfCaused(X)<=>(essenceInvExistence(X)&natureConcOnlyByExistence(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', self_caused)).
% 1.38/1.56 fof(c138,plain,(![X]:((~selfCaused(X)|(essenceInvExistence(X)&natureConcOnlyByExistence(X)))&((~essenceInvExistence(X)|~natureConcOnlyByExistence(X))|selfCaused(X)))),inference(fof_nnf,[status(thm)],[self_caused])).
% 1.38/1.56 fof(c139,plain,((![X]:(~selfCaused(X)|(essenceInvExistence(X)&natureConcOnlyByExistence(X))))&(![X]:((~essenceInvExistence(X)|~natureConcOnlyByExistence(X))|selfCaused(X)))),inference(shift_quantors,[status(thm)],[c138])).
% 1.38/1.56 fof(c141,plain,(![X39]:(![X40]:((~selfCaused(X39)|(essenceInvExistence(X39)&natureConcOnlyByExistence(X39)))&((~essenceInvExistence(X40)|~natureConcOnlyByExistence(X40))|selfCaused(X40))))),inference(shift_quantors,[status(thm)],[fof(c140,plain,((![X39]:(~selfCaused(X39)|(essenceInvExistence(X39)&natureConcOnlyByExistence(X39))))&(![X40]:((~essenceInvExistence(X40)|~natureConcOnlyByExistence(X40))|selfCaused(X40)))),inference(variable_rename,[status(thm)],[c139])).])).
% 1.38/1.56 fof(c142,plain,(![X39]:(![X40]:(((~selfCaused(X39)|essenceInvExistence(X39))&(~selfCaused(X39)|natureConcOnlyByExistence(X39)))&((~essenceInvExistence(X40)|~natureConcOnlyByExistence(X40))|selfCaused(X40))))),inference(distribute,[status(thm)],[c141])).
% 1.38/1.56 cnf(c143,plain,~selfCaused(X85)|essenceInvExistence(X85),inference(split_conjunct,[status(thm)],[c142])).
% 1.38/1.56 fof(is_in_itself_is_self_caused,axiom,(![X]:(inItself(X)=>selfCaused(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', is_in_itself_is_self_caused)).
% 1.38/1.56 fof(c54,plain,(![X]:(~inItself(X)|selfCaused(X))),inference(fof_nnf,[status(thm)],[is_in_itself_is_self_caused])).
% 1.38/1.56 fof(c55,plain,(![X4]:(~inItself(X4)|selfCaused(X4))),inference(variable_rename,[status(thm)],[c54])).
% 1.38/1.56 cnf(c56,plain,~inItself(X64)|selfCaused(X64),inference(split_conjunct,[status(thm)],[c55])).
% 1.38/1.56 fof(substance,axiom,(![X]:(substance(X)<=>(inItself(X)&conceivedThruItself(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', substance)).
% 1.38/1.56 fof(c122,plain,(![X]:((~substance(X)|(inItself(X)&conceivedThruItself(X)))&((~inItself(X)|~conceivedThruItself(X))|substance(X)))),inference(fof_nnf,[status(thm)],[substance])).
% 1.38/1.56 fof(c123,plain,((![X]:(~substance(X)|(inItself(X)&conceivedThruItself(X))))&(![X]:((~inItself(X)|~conceivedThruItself(X))|substance(X)))),inference(shift_quantors,[status(thm)],[c122])).
% 1.38/1.56 fof(c125,plain,(![X32]:(![X33]:((~substance(X32)|(inItself(X32)&conceivedThruItself(X32)))&((~inItself(X33)|~conceivedThruItself(X33))|substance(X33))))),inference(shift_quantors,[status(thm)],[fof(c124,plain,((![X32]:(~substance(X32)|(inItself(X32)&conceivedThruItself(X32))))&(![X33]:((~inItself(X33)|~conceivedThruItself(X33))|substance(X33)))),inference(variable_rename,[status(thm)],[c123])).])).
% 1.38/1.56 fof(c126,plain,(![X32]:(![X33]:(((~substance(X32)|inItself(X32))&(~substance(X32)|conceivedThruItself(X32)))&((~inItself(X33)|~conceivedThruItself(X33))|substance(X33))))),inference(distribute,[status(thm)],[c125])).
% 1.38/1.56 cnf(c127,plain,~substance(X81)|inItself(X81),inference(split_conjunct,[status(thm)],[c126])).
% 1.38/1.56 cnf(c114,negated_conjecture,mode(skolem0001)|substance(skolem0002)|existsIn(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c109])).
% 1.38/1.56 cnf(c240,plain,mode(skolem0001)|substance(skolem0002)|skolem0001=skolem0003|exists(skolem0001),inference(resolution,[status(thm)],[c114, c195])).
% 1.38/1.56 cnf(c309,plain,mode(skolem0001)|substance(skolem0002)|exists(skolem0001)|skolem0003=skolem0001,inference(resolution,[status(thm)],[c240, symmetry])).
% 1.38/1.56 cnf(c647,plain,mode(skolem0001)|substance(skolem0002)|exists(skolem0001)|~exists(skolem0003),inference(resolution,[status(thm)],[c309, c0])).
% 1.38/1.56 cnf(c239,plain,mode(skolem0001)|substance(skolem0002)|skolem0001!=X338|skolem0003!=X337|existsIn(X338,X337),inference(resolution,[status(thm)],[c114, c1])).
% 1.38/1.56 cnf(c335,plain,mode(skolem0001)|substance(skolem0002)|skolem0001!=X353|existsIn(X353,skolem0003),inference(resolution,[status(thm)],[c239, reflexivity])).
% 1.38/1.56 cnf(c659,plain,mode(skolem0001)|substance(skolem0002)|existsIn(skolem0003,skolem0003)|exists(skolem0001),inference(resolution,[status(thm)],[c335, c240])).
% 1.38/1.56 cnf(c1228,plain,mode(skolem0001)|substance(skolem0002)|exists(skolem0001)|exists(skolem0003),inference(resolution,[status(thm)],[c659, c194])).
% 1.38/1.56 cnf(c1238,plain,mode(skolem0001)|substance(skolem0002)|exists(skolem0001),inference(resolution,[status(thm)],[c1228, c647])).
% 1.38/1.56 cnf(c1245,plain,mode(skolem0001)|exists(skolem0001)|inItself(skolem0002),inference(resolution,[status(thm)],[c1238, c127])).
% 1.38/1.56 cnf(c1250,plain,mode(skolem0001)|exists(skolem0001)|selfCaused(skolem0002),inference(resolution,[status(thm)],[c1245, c56])).
% 1.38/1.56 cnf(c1256,plain,mode(skolem0001)|exists(skolem0001)|essenceInvExistence(skolem0002),inference(resolution,[status(thm)],[c1250, c143])).
% 1.38/1.56 fof(essence_involves_existence_exists,axiom,(![X]:((essenceInvExistence(X)&hasEssence(X))=>exists(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', essence_involves_existence_exists)).
% 1.38/1.56 fof(c48,plain,(![X]:((~essenceInvExistence(X)|~hasEssence(X))|exists(X))),inference(fof_nnf,[status(thm)],[essence_involves_existence_exists])).
% 1.38/1.56 fof(c49,plain,(![X2]:((~essenceInvExistence(X2)|~hasEssence(X2))|exists(X2))),inference(variable_rename,[status(thm)],[c48])).
% 1.38/1.56 cnf(c50,plain,~essenceInvExistence(X143)|~hasEssence(X143)|exists(X143),inference(split_conjunct,[status(thm)],[c49])).
% 1.38/1.56 fof(being_has_essense,axiom,(![X]:(being(X)=>hasEssence(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', being_has_essense)).
% 1.38/1.56 fof(c51,plain,(![X]:(~being(X)|hasEssence(X))),inference(fof_nnf,[status(thm)],[being_has_essense])).
% 1.38/1.56 fof(c52,plain,(![X3]:(~being(X3)|hasEssence(X3))),inference(variable_rename,[status(thm)],[c51])).
% 1.38/1.56 cnf(c53,plain,~being(X63)|hasEssence(X63),inference(split_conjunct,[status(thm)],[c52])).
% 1.38/1.56 fof(has_substance_being,axiom,(![X]:(substance(X)=>being(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', has_substance_being)).
% 1.38/1.56 fof(c57,plain,(![X]:(~substance(X)|being(X))),inference(fof_nnf,[status(thm)],[has_substance_being])).
% 1.38/1.56 fof(c58,plain,(![X5]:(~substance(X5)|being(X5))),inference(variable_rename,[status(thm)],[c57])).
% 1.38/1.56 cnf(c59,plain,~substance(X65)|being(X65),inference(split_conjunct,[status(thm)],[c58])).
% 1.38/1.56 cnf(c1247,plain,mode(skolem0001)|exists(skolem0001)|being(skolem0002),inference(resolution,[status(thm)],[c1238, c59])).
% 1.38/1.56 cnf(c1254,plain,mode(skolem0001)|exists(skolem0001)|hasEssence(skolem0002),inference(resolution,[status(thm)],[c1247, c53])).
% 1.38/1.56 cnf(c1259,plain,mode(skolem0001)|exists(skolem0001)|~essenceInvExistence(skolem0002)|exists(skolem0002),inference(resolution,[status(thm)],[c1254, c50])).
% 1.38/1.56 cnf(c1301,plain,mode(skolem0001)|exists(skolem0001)|exists(skolem0002),inference(resolution,[status(thm)],[c1259, c1256])).
% 1.38/1.56 cnf(c1304,plain,mode(skolem0001)|exists(skolem0002)|existsIn(skolem0001,skolem0001),inference(resolution,[status(thm)],[c1301, c232])).
% 1.38/1.56 cnf(c1306,plain,mode(skolem0001)|existsIn(skolem0001,skolem0001)|existsIn(skolem0002,skolem0002),inference(resolution,[status(thm)],[c1304, c232])).
% 1.38/1.56 cnf(c1318,plain,mode(skolem0001)|existsIn(skolem0001,skolem0001)|skolem0002!=X600|skolem0002!=X599|existsIn(X600,X599),inference(resolution,[status(thm)],[c1306, c1])).
% 1.38/1.56 cnf(c1492,plain,mode(skolem0001)|existsIn(skolem0001,skolem0001)|skolem0002!=X603|existsIn(X603,skolem0002),inference(resolution,[status(thm)],[c1318, reflexivity])).
% 1.38/1.56 cnf(c1491,plain,mode(skolem0001)|existsIn(skolem0001,skolem0001)|skolem0002!=X601|existsIn(X601,X601),inference(factor,[status(thm)],[c1318])).
% 1.38/1.56 cnf(c1315,plain,mode(skolem0001)|existsIn(skolem0002,skolem0002)|skolem0001!=X595|skolem0001!=X594|existsIn(X595,X594),inference(resolution,[status(thm)],[c1306, c1])).
% 1.38/1.56 cnf(c1488,plain,mode(skolem0001)|existsIn(skolem0002,skolem0002)|skolem0001!=X598|existsIn(X598,skolem0001),inference(resolution,[status(thm)],[c1315, reflexivity])).
% 1.38/1.56 cnf(c1487,plain,mode(skolem0001)|existsIn(skolem0002,skolem0002)|skolem0001!=X596|existsIn(X596,X596),inference(factor,[status(thm)],[c1315])).
% 1.38/1.56 cnf(c1438,plain,mode(skolem0001)|exists(skolem0001)|skolem0001!=X586|skolem0002!=X587|modification(X586,X587),inference(resolution,[status(thm)],[c1436, c27])).
% 1.38/1.56 cnf(c1485,plain,mode(skolem0001)|exists(skolem0001)|skolem0001!=X589|modification(X589,skolem0002),inference(resolution,[status(thm)],[c1438, reflexivity])).
% 1.38/1.56 cnf(c1305,plain,mode(skolem0001)|exists(skolem0001)|existsIn(skolem0002,skolem0002),inference(resolution,[status(thm)],[c1301, c232])).
% 1.38/1.56 cnf(c1312,plain,mode(skolem0001)|exists(skolem0001)|skolem0002!=X576|skolem0002!=X575|existsIn(X576,X575),inference(resolution,[status(thm)],[c1305, c1])).
% 1.38/1.56 cnf(c1482,plain,mode(skolem0001)|exists(skolem0001)|skolem0002!=X578|existsIn(X578,skolem0002),inference(resolution,[status(thm)],[c1312, reflexivity])).
% 1.38/1.56 cnf(c1481,plain,mode(skolem0001)|exists(skolem0001)|skolem0002!=X577|existsIn(X577,X577),inference(factor,[status(thm)],[c1312])).
% 1.38/1.56 cnf(c1308,plain,mode(skolem0001)|exists(skolem0002)|skolem0001!=X571|skolem0001!=X570|existsIn(X571,X570),inference(resolution,[status(thm)],[c1304, c1])).
% 1.38/1.56 cnf(c1478,plain,mode(skolem0001)|exists(skolem0002)|skolem0001!=X573|existsIn(X573,skolem0001),inference(resolution,[status(thm)],[c1308, reflexivity])).
% 1.38/1.56 cnf(c1477,plain,mode(skolem0001)|exists(skolem0002)|skolem0001!=X572|existsIn(X572,X572),inference(factor,[status(thm)],[c1308])).
% 1.38/1.56 cnf(c144,plain,~selfCaused(X86)|natureConcOnlyByExistence(X86),inference(split_conjunct,[status(thm)],[c142])).
% 1.38/1.56 cnf(c1257,plain,mode(skolem0001)|exists(skolem0001)|natureConcOnlyByExistence(skolem0002),inference(resolution,[status(thm)],[c1250, c144])).
% 1.38/1.56 cnf(c1262,plain,mode(skolem0001)|natureConcOnlyByExistence(skolem0002)|existsIn(skolem0001,skolem0001),inference(resolution,[status(thm)],[c1257, c232])).
% 1.38/1.56 cnf(c1298,plain,mode(skolem0001)|natureConcOnlyByExistence(skolem0002)|skolem0001!=X566|skolem0001!=X565|existsIn(X566,X565),inference(resolution,[status(thm)],[c1262, c1])).
% 1.38/1.57 cnf(c1474,plain,mode(skolem0001)|natureConcOnlyByExistence(skolem0002)|skolem0001!=X568|existsIn(X568,skolem0001),inference(resolution,[status(thm)],[c1298, reflexivity])).
% 1.38/1.57 cnf(c1473,plain,mode(skolem0001)|natureConcOnlyByExistence(skolem0002)|skolem0001!=X567|existsIn(X567,X567),inference(factor,[status(thm)],[c1298])).
% 1.38/1.57 cnf(c1260,plain,mode(skolem0001)|essenceInvExistence(skolem0002)|existsIn(skolem0001,skolem0001),inference(resolution,[status(thm)],[c1256, c232])).
% 1.38/1.57 cnf(c1294,plain,mode(skolem0001)|essenceInvExistence(skolem0002)|skolem0001!=X561|skolem0001!=X560|existsIn(X561,X560),inference(resolution,[status(thm)],[c1260, c1])).
% 1.38/1.57 cnf(c1470,plain,mode(skolem0001)|essenceInvExistence(skolem0002)|skolem0001!=X563|existsIn(X563,skolem0001),inference(resolution,[status(thm)],[c1294, reflexivity])).
% 1.38/1.57 cnf(c1469,plain,mode(skolem0001)|essenceInvExistence(skolem0002)|skolem0001!=X562|existsIn(X562,X562),inference(factor,[status(thm)],[c1294])).
% 1.38/1.57 cnf(c1258,plain,mode(skolem0001)|hasEssence(skolem0002)|existsIn(skolem0001,skolem0001),inference(resolution,[status(thm)],[c1254, c232])).
% 1.38/1.57 cnf(c1290,plain,mode(skolem0001)|hasEssence(skolem0002)|skolem0001!=X556|skolem0001!=X555|existsIn(X556,X555),inference(resolution,[status(thm)],[c1258, c1])).
% 1.38/1.57 cnf(c1466,plain,mode(skolem0001)|hasEssence(skolem0002)|skolem0001!=X558|existsIn(X558,skolem0001),inference(resolution,[status(thm)],[c1290, reflexivity])).
% 1.38/1.57 cnf(c1465,plain,mode(skolem0001)|hasEssence(skolem0002)|skolem0001!=X557|existsIn(X557,X557),inference(factor,[status(thm)],[c1290])).
% 1.38/1.57 cnf(c1255,plain,mode(skolem0001)|selfCaused(skolem0002)|existsIn(skolem0001,skolem0001),inference(resolution,[status(thm)],[c1250, c232])).
% 1.38/1.57 cnf(c1286,plain,mode(skolem0001)|selfCaused(skolem0002)|skolem0001!=X551|skolem0001!=X550|existsIn(X551,X550),inference(resolution,[status(thm)],[c1255, c1])).
% 1.38/1.57 cnf(c1462,plain,mode(skolem0001)|selfCaused(skolem0002)|skolem0001!=X553|existsIn(X553,skolem0001),inference(resolution,[status(thm)],[c1286, reflexivity])).
% 1.38/1.57 cnf(c1461,plain,mode(skolem0001)|selfCaused(skolem0002)|skolem0001!=X552|existsIn(X552,X552),inference(factor,[status(thm)],[c1286])).
% 1.38/1.57 cnf(c1253,plain,mode(skolem0001)|being(skolem0002)|existsIn(skolem0001,skolem0001),inference(resolution,[status(thm)],[c1247, c232])).
% 1.38/1.57 cnf(c1281,plain,mode(skolem0001)|being(skolem0002)|skolem0001!=X545|skolem0001!=X544|existsIn(X545,X544),inference(resolution,[status(thm)],[c1253, c1])).
% 1.38/1.57 cnf(c1458,plain,mode(skolem0001)|being(skolem0002)|skolem0001!=X547|existsIn(X547,skolem0001),inference(resolution,[status(thm)],[c1281, reflexivity])).
% 1.38/1.57 cnf(c1457,plain,mode(skolem0001)|being(skolem0002)|skolem0001!=X546|existsIn(X546,X546),inference(factor,[status(thm)],[c1281])).
% 1.38/1.57 cnf(c128,plain,~substance(X84)|conceivedThruItself(X84),inference(split_conjunct,[status(thm)],[c126])).
% 1.38/1.57 cnf(c1246,plain,mode(skolem0001)|exists(skolem0001)|conceivedThruItself(skolem0002),inference(resolution,[status(thm)],[c1238, c128])).
% 1.38/1.57 cnf(c1251,plain,mode(skolem0001)|conceivedThruItself(skolem0002)|existsIn(skolem0001,skolem0001),inference(resolution,[status(thm)],[c1246, c232])).
% 1.38/1.57 cnf(c1277,plain,mode(skolem0001)|conceivedThruItself(skolem0002)|skolem0001!=X540|skolem0001!=X539|existsIn(X540,X539),inference(resolution,[status(thm)],[c1251, c1])).
% 1.38/1.57 cnf(c1454,plain,mode(skolem0001)|conceivedThruItself(skolem0002)|skolem0001!=X542|existsIn(X542,skolem0001),inference(resolution,[status(thm)],[c1277, reflexivity])).
% 1.38/1.57 cnf(c1453,plain,mode(skolem0001)|conceivedThruItself(skolem0002)|skolem0001!=X541|existsIn(X541,X541),inference(factor,[status(thm)],[c1277])).
% 1.38/1.57 cnf(c1249,plain,mode(skolem0001)|inItself(skolem0002)|existsIn(skolem0001,skolem0001),inference(resolution,[status(thm)],[c1245, c232])).
% 1.38/1.57 cnf(c1273,plain,mode(skolem0001)|inItself(skolem0002)|skolem0001!=X535|skolem0001!=X534|existsIn(X535,X534),inference(resolution,[status(thm)],[c1249, c1])).
% 1.38/1.57 cnf(c1450,plain,mode(skolem0001)|inItself(skolem0002)|skolem0001!=X537|existsIn(X537,skolem0001),inference(resolution,[status(thm)],[c1273, reflexivity])).
% 1.38/1.57 cnf(c1449,plain,mode(skolem0001)|inItself(skolem0002)|skolem0001!=X536|existsIn(X536,X536),inference(factor,[status(thm)],[c1273])).
% 1.38/1.57 cnf(c1248,plain,mode(skolem0001)|substance(skolem0002)|existsIn(skolem0001,skolem0001),inference(resolution,[status(thm)],[c1238, c232])).
% 1.38/1.57 cnf(c1269,plain,mode(skolem0001)|substance(skolem0002)|skolem0001!=X530|skolem0001!=X529|existsIn(X530,X529),inference(resolution,[status(thm)],[c1248, c1])).
% 1.38/1.57 cnf(c1446,plain,mode(skolem0001)|substance(skolem0002)|skolem0001!=X532|existsIn(X532,skolem0001),inference(resolution,[status(thm)],[c1269, reflexivity])).
% 1.38/1.57 cnf(c1445,plain,mode(skolem0001)|substance(skolem0002)|skolem0001!=X531|existsIn(X531,X531),inference(factor,[status(thm)],[c1269])).
% 1.38/1.57 cnf(c115,negated_conjecture,mode(skolem0001)|substance(skolem0002)|conceivedThru(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c109])).
% 1.38/1.57 cnf(c241,plain,mode(skolem0001)|conceivedThru(skolem0001,skolem0003)|inItself(skolem0002),inference(resolution,[status(thm)],[c115, c127])).
% 1.38/1.57 cnf(c255,plain,mode(skolem0001)|conceivedThru(skolem0001,skolem0003)|selfCaused(skolem0002),inference(resolution,[status(thm)],[c241, c56])).
% 1.38/1.57 cnf(c268,plain,mode(skolem0001)|conceivedThru(skolem0001,skolem0003)|essenceInvExistence(skolem0002),inference(resolution,[status(thm)],[c255, c143])).
% 1.38/1.57 cnf(c243,plain,mode(skolem0001)|conceivedThru(skolem0001,skolem0003)|being(skolem0002),inference(resolution,[status(thm)],[c115, c59])).
% 1.38/1.57 cnf(c259,plain,mode(skolem0001)|conceivedThru(skolem0001,skolem0003)|hasEssence(skolem0002),inference(resolution,[status(thm)],[c243, c53])).
% 1.38/1.57 cnf(c271,plain,mode(skolem0001)|conceivedThru(skolem0001,skolem0003)|~essenceInvExistence(skolem0002)|exists(skolem0002),inference(resolution,[status(thm)],[c259, c50])).
% 1.38/1.57 cnf(c525,plain,mode(skolem0001)|conceivedThru(skolem0001,skolem0003)|exists(skolem0002),inference(resolution,[status(thm)],[c271, c268])).
% 1.38/1.57 cnf(c528,plain,mode(skolem0001)|conceivedThru(skolem0001,skolem0003)|existsIn(skolem0002,skolem0002),inference(resolution,[status(thm)],[c525, c232])).
% 1.38/1.57 cnf(c532,plain,mode(skolem0001)|conceivedThru(skolem0001,skolem0003)|skolem0002!=X419|skolem0002!=X418|existsIn(X419,X418),inference(resolution,[status(thm)],[c528, c1])).
% 1.38/1.57 cnf(c1348,plain,mode(skolem0001)|conceivedThru(skolem0001,skolem0003)|skolem0002!=X483|existsIn(X483,skolem0002),inference(resolution,[status(thm)],[c532, reflexivity])).
% 1.38/1.57 cnf(c2,axiom,X104!=X103|X106!=X105|~conceivedThru(X104,X106)|conceivedThru(X103,X105),theory(equality)).
% 1.38/1.57 cnf(c530,plain,mode(skolem0001)|existsIn(skolem0002,skolem0002)|skolem0001!=X416|skolem0003!=X417|conceivedThru(X416,X417),inference(resolution,[status(thm)],[c528, c2])).
% 1.38/1.57 cnf(c1346,plain,mode(skolem0001)|existsIn(skolem0002,skolem0002)|skolem0001!=X482|conceivedThru(X482,skolem0003),inference(resolution,[status(thm)],[c530, reflexivity])).
% 1.38/1.57 cnf(c236,plain,mode(skolem0001)|existsIn(skolem0001,skolem0003)|inItself(skolem0002),inference(resolution,[status(thm)],[c114, c127])).
% 1.38/1.57 cnf(c247,plain,mode(skolem0001)|existsIn(skolem0001,skolem0003)|selfCaused(skolem0002),inference(resolution,[status(thm)],[c236, c56])).
% 1.38/1.57 cnf(c262,plain,mode(skolem0001)|existsIn(skolem0001,skolem0003)|essenceInvExistence(skolem0002),inference(resolution,[status(thm)],[c247, c143])).
% 1.38/1.57 cnf(c238,plain,mode(skolem0001)|existsIn(skolem0001,skolem0003)|being(skolem0002),inference(resolution,[status(thm)],[c114, c59])).
% 1.38/1.57 cnf(c253,plain,mode(skolem0001)|existsIn(skolem0001,skolem0003)|hasEssence(skolem0002),inference(resolution,[status(thm)],[c238, c53])).
% 1.38/1.57 cnf(c266,plain,mode(skolem0001)|existsIn(skolem0001,skolem0003)|~essenceInvExistence(skolem0002)|exists(skolem0002),inference(resolution,[status(thm)],[c253, c50])).
% 1.38/1.57 cnf(c513,plain,mode(skolem0001)|existsIn(skolem0001,skolem0003)|exists(skolem0002),inference(resolution,[status(thm)],[c266, c262])).
% 1.38/1.57 cnf(c517,plain,mode(skolem0001)|existsIn(skolem0001,skolem0003)|existsIn(skolem0002,skolem0002),inference(resolution,[status(thm)],[c513, c232])).
% 1.38/1.57 cnf(c521,plain,mode(skolem0001)|existsIn(skolem0001,skolem0003)|skolem0002!=X411|skolem0002!=X410|existsIn(X411,X410),inference(resolution,[status(thm)],[c517, c1])).
% 1.38/1.57 cnf(c1341,plain,mode(skolem0001)|existsIn(skolem0001,skolem0003)|skolem0002!=X481|existsIn(X481,skolem0002),inference(resolution,[status(thm)],[c521, reflexivity])).
% 1.38/1.57 cnf(c518,plain,mode(skolem0001)|existsIn(skolem0002,skolem0002)|skolem0001!=X409|skolem0003!=X408|existsIn(X409,X408),inference(resolution,[status(thm)],[c517, c1])).
% 1.38/1.57 cnf(c1339,plain,mode(skolem0001)|existsIn(skolem0002,skolem0002)|skolem0001!=X479|existsIn(X479,skolem0003),inference(resolution,[status(thm)],[c518, reflexivity])).
% 1.38/1.57 cnf(c113,negated_conjecture,mode(skolem0001)|modification(skolem0001,skolem0002)|conceivedThru(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c109])).
% 1.38/1.57 cnf(c297,plain,mode(skolem0001)|modification(skolem0001,skolem0002)|skolem0001!=X383|skolem0003!=X384|conceivedThru(X383,X384),inference(resolution,[status(thm)],[c113, c2])).
% 1.38/1.57 cnf(c1264,plain,mode(skolem0001)|modification(skolem0001,skolem0002)|skolem0001!=X477|conceivedThru(X477,skolem0003),inference(resolution,[status(thm)],[c297, reflexivity])).
% 1.38/1.57 cnf(c295,plain,mode(skolem0001)|conceivedThru(skolem0001,skolem0003)|skolem0001!=X381|skolem0002!=X382|modification(X381,X382),inference(resolution,[status(thm)],[c113, c27])).
% 1.38/1.57 cnf(c1224,plain,mode(skolem0001)|conceivedThru(skolem0001,skolem0003)|skolem0001!=X476|modification(X476,skolem0002),inference(resolution,[status(thm)],[c295, reflexivity])).
% 1.38/1.57 cnf(c291,plain,mode(skolem0001)|existsIn(skolem0001,skolem0003)|skolem0001!=X374|skolem0002!=X375|modification(X374,X375),inference(resolution,[status(thm)],[c112, c27])).
% 1.38/1.57 cnf(c1140,plain,mode(skolem0001)|existsIn(skolem0001,skolem0003)|skolem0001!=X472|modification(X472,skolem0002),inference(resolution,[status(thm)],[c291, reflexivity])).
% 1.38/1.57 cnf(c1347,plain,mode(skolem0001)|conceivedThru(skolem0001,skolem0003)|skolem0002!=X420|existsIn(X420,X420),inference(factor,[status(thm)],[c532])).
% 1.38/1.57 cnf(c527,plain,mode(skolem0001)|exists(skolem0002)|skolem0001!=X413|skolem0003!=X414|conceivedThru(X413,X414),inference(resolution,[status(thm)],[c525, c2])).
% 1.38/1.57 cnf(c1343,plain,mode(skolem0001)|exists(skolem0002)|skolem0001!=X415|conceivedThru(X415,skolem0003),inference(resolution,[status(thm)],[c527, reflexivity])).
% 1.38/1.57 cnf(c1340,plain,mode(skolem0001)|existsIn(skolem0001,skolem0003)|skolem0002!=X412|existsIn(X412,X412),inference(factor,[status(thm)],[c521])).
% 1.38/1.57 cnf(c515,plain,mode(skolem0001)|exists(skolem0002)|skolem0001!=X406|skolem0003!=X405|existsIn(X406,X405),inference(resolution,[status(thm)],[c513, c1])).
% 1.38/1.57 cnf(c1336,plain,mode(skolem0001)|exists(skolem0002)|skolem0001!=X407|existsIn(X407,skolem0003),inference(resolution,[status(thm)],[c515, reflexivity])).
% 1.38/1.57 cnf(c269,plain,mode(skolem0001)|conceivedThru(skolem0001,skolem0003)|natureConcOnlyByExistence(skolem0002),inference(resolution,[status(thm)],[c255, c144])).
% 1.38/1.57 cnf(c280,plain,mode(skolem0001)|natureConcOnlyByExistence(skolem0002)|skolem0001!=X371|skolem0003!=X372|conceivedThru(X371,X372),inference(resolution,[status(thm)],[c269, c2])).
% 1.38/1.57 cnf(c1070,plain,mode(skolem0001)|natureConcOnlyByExistence(skolem0002)|skolem0001!=X394|conceivedThru(X394,skolem0003),inference(resolution,[status(thm)],[c280, reflexivity])).
% 1.38/1.57 cnf(c278,plain,mode(skolem0001)|essenceInvExistence(skolem0002)|skolem0001!=X369|skolem0003!=X370|conceivedThru(X369,X370),inference(resolution,[status(thm)],[c268, c2])).
% 1.38/1.57 cnf(c1010,plain,mode(skolem0001)|essenceInvExistence(skolem0002)|skolem0001!=X393|conceivedThru(X393,skolem0003),inference(resolution,[status(thm)],[c278, reflexivity])).
% 1.38/1.57 cnf(c263,plain,mode(skolem0001)|existsIn(skolem0001,skolem0003)|natureConcOnlyByExistence(skolem0002),inference(resolution,[status(thm)],[c247, c144])).
% 1.38/1.57 cnf(c275,plain,mode(skolem0001)|natureConcOnlyByExistence(skolem0002)|skolem0001!=X366|skolem0003!=X365|existsIn(X366,X365),inference(resolution,[status(thm)],[c263, c1])).
% 1.38/1.57 cnf(c983,plain,mode(skolem0001)|natureConcOnlyByExistence(skolem0002)|skolem0001!=X392|existsIn(X392,skolem0003),inference(resolution,[status(thm)],[c275, reflexivity])).
% 1.38/1.57 cnf(c272,plain,mode(skolem0001)|essenceInvExistence(skolem0002)|skolem0001!=X364|skolem0003!=X363|existsIn(X364,X363),inference(resolution,[status(thm)],[c262, c1])).
% 1.38/1.57 cnf(c889,plain,mode(skolem0001)|essenceInvExistence(skolem0002)|skolem0001!=X391|existsIn(X391,skolem0003),inference(resolution,[status(thm)],[c272, reflexivity])).
% 1.38/1.57 cnf(c270,plain,mode(skolem0001)|hasEssence(skolem0002)|skolem0001!=X361|skolem0003!=X362|conceivedThru(X361,X362),inference(resolution,[status(thm)],[c259, c2])).
% 1.38/1.57 cnf(c831,plain,mode(skolem0001)|hasEssence(skolem0002)|skolem0001!=X390|conceivedThru(X390,skolem0003),inference(resolution,[status(thm)],[c270, reflexivity])).
% 1.38/1.57 cnf(c267,plain,mode(skolem0001)|selfCaused(skolem0002)|skolem0001!=X358|skolem0003!=X359|conceivedThru(X358,X359),inference(resolution,[status(thm)],[c255, c2])).
% 1.38/1.57 cnf(c817,plain,mode(skolem0001)|selfCaused(skolem0002)|skolem0001!=X389|conceivedThru(X389,skolem0003),inference(resolution,[status(thm)],[c267, reflexivity])).
% 1.38/1.57 cnf(c264,plain,mode(skolem0001)|hasEssence(skolem0002)|skolem0001!=X357|skolem0003!=X356|existsIn(X357,X356),inference(resolution,[status(thm)],[c253, c1])).
% 1.38/1.57 cnf(c765,plain,mode(skolem0001)|hasEssence(skolem0002)|skolem0001!=X387|existsIn(X387,skolem0003),inference(resolution,[status(thm)],[c264, reflexivity])).
% 1.38/1.57 cnf(c260,plain,mode(skolem0001)|selfCaused(skolem0002)|skolem0001!=X355|skolem0003!=X354|existsIn(X355,X354),inference(resolution,[status(thm)],[c247, c1])).
% 1.38/1.57 cnf(c671,plain,mode(skolem0001)|selfCaused(skolem0002)|skolem0001!=X385|existsIn(X385,skolem0003),inference(resolution,[status(thm)],[c260, reflexivity])).
% 1.38/1.57 fof(can_be_conceived_as_non_existing,axiom,(![X]:(canBeConceivedAsNonExisting(X)=>(~essenceInvExistence(X)))),file('/export/starexec/sandbox/benchmark/Axioms/PHI002+1.ax', can_be_conceived_as_non_existing)).
% 1.38/1.57 fof(c146,plain,(![X]:(canBeConceivedAsNonExisting(X)=>~essenceInvExistence(X))),inference(fof_simplification,[status(thm)],[can_be_conceived_as_non_existing])).
% 1.38/1.57 fof(c147,plain,(![X]:(~canBeConceivedAsNonExisting(X)|~essenceInvExistence(X))),inference(fof_nnf,[status(thm)],[c146])).
% 1.38/1.57 fof(c148,plain,(![X41]:(~canBeConceivedAsNonExisting(X41)|~essenceInvExistence(X41))),inference(variable_rename,[status(thm)],[c147])).
% 1.38/1.57 cnf(c149,plain,~canBeConceivedAsNonExisting(X87)|~essenceInvExistence(X87),inference(split_conjunct,[status(thm)],[c148])).
% 1.38/1.57 cnf(c1292,plain,mode(skolem0001)|existsIn(skolem0001,skolem0001)|~canBeConceivedAsNonExisting(skolem0002),inference(resolution,[status(thm)],[c1260, c149])).
% 1.38/1.57 cnf(c1261,plain,mode(skolem0001)|exists(skolem0001)|~canBeConceivedAsNonExisting(skolem0002),inference(resolution,[status(thm)],[c1256, c149])).
% 1.38/1.57 cnf(c258,plain,mode(skolem0001)|being(skolem0002)|skolem0001!=X351|skolem0003!=X352|conceivedThru(X351,X352),inference(resolution,[status(thm)],[c243, c2])).
% 1.38/1.57 cnf(c657,plain,mode(skolem0001)|being(skolem0002)|skolem0001!=X380|conceivedThru(X380,skolem0003),inference(resolution,[status(thm)],[c258, reflexivity])).
% 1.38/1.57 cnf(c242,plain,mode(skolem0001)|conceivedThru(skolem0001,skolem0003)|conceivedThruItself(skolem0002),inference(resolution,[status(thm)],[c115, c128])).
% 1.38/1.57 cnf(c256,plain,mode(skolem0001)|conceivedThruItself(skolem0002)|skolem0001!=X349|skolem0003!=X350|conceivedThru(X349,X350),inference(resolution,[status(thm)],[c242, c2])).
% 1.38/1.57 cnf(c607,plain,mode(skolem0001)|conceivedThruItself(skolem0002)|skolem0001!=X377|conceivedThru(X377,skolem0003),inference(resolution,[status(thm)],[c256, reflexivity])).
% 1.38/1.57 cnf(c254,plain,mode(skolem0001)|inItself(skolem0002)|skolem0001!=X347|skolem0003!=X348|conceivedThru(X347,X348),inference(resolution,[status(thm)],[c241, c2])).
% 1.38/1.57 cnf(c606,plain,mode(skolem0001)|inItself(skolem0002)|skolem0001!=X376|conceivedThru(X376,skolem0003),inference(resolution,[status(thm)],[c254, reflexivity])).
% 1.38/1.57 cnf(c251,plain,mode(skolem0001)|being(skolem0002)|skolem0001!=X346|skolem0003!=X345|existsIn(X346,X345),inference(resolution,[status(thm)],[c238, c1])).
% 1.38/1.57 cnf(c605,plain,mode(skolem0001)|being(skolem0002)|skolem0001!=X373|existsIn(X373,skolem0003),inference(resolution,[status(thm)],[c251, reflexivity])).
% 1.38/1.57 cnf(c237,plain,mode(skolem0001)|existsIn(skolem0001,skolem0003)|conceivedThruItself(skolem0002),inference(resolution,[status(thm)],[c114, c128])).
% 1.38/1.57 cnf(c248,plain,mode(skolem0001)|conceivedThruItself(skolem0002)|skolem0001!=X344|skolem0003!=X343|existsIn(X344,X343),inference(resolution,[status(thm)],[c237, c1])).
% 1.38/1.57 cnf(c534,plain,mode(skolem0001)|conceivedThruItself(skolem0002)|skolem0001!=X368|existsIn(X368,skolem0003),inference(resolution,[status(thm)],[c248, reflexivity])).
% 1.38/1.57 cnf(c245,plain,mode(skolem0001)|inItself(skolem0002)|skolem0001!=X342|skolem0003!=X341|existsIn(X342,X341),inference(resolution,[status(thm)],[c236, c1])).
% 1.38/1.57 cnf(c523,plain,mode(skolem0001)|inItself(skolem0002)|skolem0001!=X367|existsIn(X367,skolem0003),inference(resolution,[status(thm)],[c245, reflexivity])).
% 1.38/1.57 cnf(c244,plain,mode(skolem0001)|substance(skolem0002)|skolem0001!=X339|skolem0003!=X340|conceivedThru(X339,X340),inference(resolution,[status(thm)],[c115, c2])).
% 1.38/1.57 cnf(c441,plain,mode(skolem0001)|substance(skolem0002)|skolem0001!=X360|conceivedThru(X360,skolem0003),inference(resolution,[status(thm)],[c244, reflexivity])).
% 1.38/1.57 cnf(c111,negated_conjecture,~mode(skolem0001)|~existsIn(skolem0001,skolem0003)|~conceivedThru(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c109])).
% 1.38/1.57 fof(absolutely_infinite,axiom,(![X]:(![Y]:(absolutelyInfinite(X)<=>((substance(X)&constInInfAttributes(X))&(attributeOf(Y,X)=>(expressesEternalEssentiality(Y)&expressesInfiniteEssentiality(Y))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', absolutely_infinite)).
% 1.38/1.57 fof(c86,plain,(![X]:(![Y]:((~absolutelyInfinite(X)|((substance(X)&constInInfAttributes(X))&(~attributeOf(Y,X)|(expressesEternalEssentiality(Y)&expressesInfiniteEssentiality(Y)))))&(((~substance(X)|~constInInfAttributes(X))|(attributeOf(Y,X)&(~expressesEternalEssentiality(Y)|~expressesInfiniteEssentiality(Y))))|absolutelyInfinite(X))))),inference(fof_nnf,[status(thm)],[absolutely_infinite])).
% 1.38/1.57 fof(c87,plain,((![X]:(~absolutelyInfinite(X)|((substance(X)&constInInfAttributes(X))&(![Y]:(~attributeOf(Y,X)|(expressesEternalEssentiality(Y)&expressesInfiniteEssentiality(Y)))))))&(![X]:(((~substance(X)|~constInInfAttributes(X))|((![Y]:attributeOf(Y,X))&(![Y]:(~expressesEternalEssentiality(Y)|~expressesInfiniteEssentiality(Y)))))|absolutelyInfinite(X)))),inference(shift_quantors,[status(thm)],[c86])).
% 1.38/1.57 fof(c89,plain,(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:((~absolutelyInfinite(X20)|((substance(X20)&constInInfAttributes(X20))&(~attributeOf(X21,X20)|(expressesEternalEssentiality(X21)&expressesInfiniteEssentiality(X21)))))&(((~substance(X22)|~constInInfAttributes(X22))|(attributeOf(X23,X22)&(~expressesEternalEssentiality(X24)|~expressesInfiniteEssentiality(X24))))|absolutelyInfinite(X22)))))))),inference(shift_quantors,[status(thm)],[fof(c88,plain,((![X20]:(~absolutelyInfinite(X20)|((substance(X20)&constInInfAttributes(X20))&(![X21]:(~attributeOf(X21,X20)|(expressesEternalEssentiality(X21)&expressesInfiniteEssentiality(X21)))))))&(![X22]:(((~substance(X22)|~constInInfAttributes(X22))|((![X23]:attributeOf(X23,X22))&(![X24]:(~expressesEternalEssentiality(X24)|~expressesInfiniteEssentiality(X24)))))|absolutelyInfinite(X22)))),inference(variable_rename,[status(thm)],[c87])).])).
% 1.38/1.57 fof(c90,plain,(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:((((~absolutelyInfinite(X20)|substance(X20))&(~absolutelyInfinite(X20)|constInInfAttributes(X20)))&((~absolutelyInfinite(X20)|(~attributeOf(X21,X20)|expressesEternalEssentiality(X21)))&(~absolutelyInfinite(X20)|(~attributeOf(X21,X20)|expressesInfiniteEssentiality(X21)))))&((((~substance(X22)|~constInInfAttributes(X22))|attributeOf(X23,X22))|absolutelyInfinite(X22))&(((~substance(X22)|~constInInfAttributes(X22))|(~expressesEternalEssentiality(X24)|~expressesInfiniteEssentiality(X24)))|absolutelyInfinite(X22))))))))),inference(distribute,[status(thm)],[c89])).
% 1.38/1.57 cnf(c96,plain,~substance(X328)|~constInInfAttributes(X328)|~expressesEternalEssentiality(X327)|~expressesInfiniteEssentiality(X327)|absolutelyInfinite(X328),inference(split_conjunct,[status(thm)],[c90])).
% 1.38/1.57 cnf(c279,plain,mode(skolem0001)|conceivedThru(skolem0001,skolem0003)|~canBeConceivedAsNonExisting(skolem0002),inference(resolution,[status(thm)],[c268, c149])).
% 1.38/1.57 cnf(c274,plain,mode(skolem0001)|existsIn(skolem0001,skolem0003)|~canBeConceivedAsNonExisting(skolem0002),inference(resolution,[status(thm)],[c262, c149])).
% 1.38/1.57 fof(necessary,axiom,(![X]:(![Y]:(necessary(X)<=>(((externalTo(Y,X)&determinedByFixedMethod(X,Y))&determinedByDefiniteMethod(X,Y))&(isMethodAction(Y)|isMethodExistence(Y)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', necessary)).
% 1.38/1.57 fof(c66,plain,(![X]:(![Y]:((~necessary(X)|(((externalTo(Y,X)&determinedByFixedMethod(X,Y))&determinedByDefiniteMethod(X,Y))&(isMethodAction(Y)|isMethodExistence(Y))))&((((~externalTo(Y,X)|~determinedByFixedMethod(X,Y))|~determinedByDefiniteMethod(X,Y))|(~isMethodAction(Y)&~isMethodExistence(Y)))|necessary(X))))),inference(fof_nnf,[status(thm)],[necessary])).
% 1.38/1.57 fof(c67,plain,((![X]:(~necessary(X)|((((![Y]:externalTo(Y,X))&(![Y]:determinedByFixedMethod(X,Y)))&(![Y]:determinedByDefiniteMethod(X,Y)))&(![Y]:(isMethodAction(Y)|isMethodExistence(Y))))))&(![X]:((![Y]:(((~externalTo(Y,X)|~determinedByFixedMethod(X,Y))|~determinedByDefiniteMethod(X,Y))|(~isMethodAction(Y)&~isMethodExistence(Y))))|necessary(X)))),inference(shift_quantors,[status(thm)],[c66])).
% 1.38/1.57 fof(c69,plain,(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:((~necessary(X8)|(((externalTo(X9,X8)&determinedByFixedMethod(X8,X10))&determinedByDefiniteMethod(X8,X11))&(isMethodAction(X12)|isMethodExistence(X12))))&((((~externalTo(X14,X13)|~determinedByFixedMethod(X13,X14))|~determinedByDefiniteMethod(X13,X14))|(~isMethodAction(X14)&~isMethodExistence(X14)))|necessary(X13)))))))))),inference(shift_quantors,[status(thm)],[fof(c68,plain,((![X8]:(~necessary(X8)|((((![X9]:externalTo(X9,X8))&(![X10]:determinedByFixedMethod(X8,X10)))&(![X11]:determinedByDefiniteMethod(X8,X11)))&(![X12]:(isMethodAction(X12)|isMethodExistence(X12))))))&(![X13]:((![X14]:(((~externalTo(X14,X13)|~determinedByFixedMethod(X13,X14))|~determinedByDefiniteMethod(X13,X14))|(~isMethodAction(X14)&~isMethodExistence(X14))))|necessary(X13)))),inference(variable_rename,[status(thm)],[c67])).])).
% 1.38/1.57 fof(c70,plain,(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(((((~necessary(X8)|externalTo(X9,X8))&(~necessary(X8)|determinedByFixedMethod(X8,X10)))&(~necessary(X8)|determinedByDefiniteMethod(X8,X11)))&(~necessary(X8)|(isMethodAction(X12)|isMethodExistence(X12))))&(((((~externalTo(X14,X13)|~determinedByFixedMethod(X13,X14))|~determinedByDefiniteMethod(X13,X14))|~isMethodAction(X14))|necessary(X13))&((((~externalTo(X14,X13)|~determinedByFixedMethod(X13,X14))|~determinedByDefiniteMethod(X13,X14))|~isMethodExistence(X14))|necessary(X13))))))))))),inference(distribute,[status(thm)],[c69])).
% 1.38/1.57 cnf(c76,plain,~externalTo(X325,X326)|~determinedByFixedMethod(X326,X325)|~determinedByDefiniteMethod(X326,X325)|~isMethodExistence(X325)|necessary(X326),inference(split_conjunct,[status(thm)],[c70])).
% 1.38/1.57 cnf(c75,plain,~externalTo(X323,X324)|~determinedByFixedMethod(X324,X323)|~determinedByDefiniteMethod(X324,X323)|~isMethodAction(X323)|necessary(X324),inference(split_conjunct,[status(thm)],[c70])).
% 1.38/1.57 cnf(c44,axiom,X320!=X319|X322!=X321|~determinedByFixedMethod(X320,X322)|determinedByFixedMethod(X319,X321),theory(equality)).
% 1.38/1.57 cnf(c110,negated_conjecture,~mode(skolem0001)|~modification(skolem0001,skolem0002)|~substance(skolem0002),inference(split_conjunct,[status(thm)],[c109])).
% 1.38/1.57 cnf(c43,axiom,X316!=X315|X318!=X317|~externalTo(X316,X318)|externalTo(X315,X317),theory(equality)).
% 1.38/1.57 cnf(c95,plain,~substance(X313)|~constInInfAttributes(X313)|attributeOf(X314,X313)|absolutelyInfinite(X313),inference(split_conjunct,[status(thm)],[c90])).
% 1.38/1.57 fof(conceived_through,axiom,(![X]:(![Y]:((~conceivedThru(X,X))=>(conceivedThru(X,Y)&X!=Y)))),file('/export/starexec/sandbox/benchmark/Axioms/PHI002+1.ax', conceived_through)).
% 1.38/1.57 fof(c179,plain,(![X]:(![Y]:(~conceivedThru(X,X)=>(conceivedThru(X,Y)&X!=Y)))),inference(fof_simplification,[status(thm)],[conceived_through])).
% 1.38/1.57 fof(c180,plain,(![X]:(![Y]:(conceivedThru(X,X)|(conceivedThru(X,Y)&X!=Y)))),inference(fof_nnf,[status(thm)],[c179])).
% 1.38/1.57 fof(c181,plain,(![X]:(conceivedThru(X,X)|((![Y]:conceivedThru(X,Y))&(![Y]:X!=Y)))),inference(shift_quantors,[status(thm)],[c180])).
% 1.38/1.57 fof(c183,plain,(![X54]:(![X55]:(![X56]:(conceivedThru(X54,X54)|(conceivedThru(X54,X55)&X54!=X56))))),inference(shift_quantors,[status(thm)],[fof(c182,plain,(![X54]:(conceivedThru(X54,X54)|((![X55]:conceivedThru(X54,X55))&(![X56]:X54!=X56)))),inference(variable_rename,[status(thm)],[c181])).])).
% 1.38/1.57 fof(c184,plain,(![X54]:(![X55]:(![X56]:((conceivedThru(X54,X54)|conceivedThru(X54,X55))&(conceivedThru(X54,X54)|X54!=X56))))),inference(distribute,[status(thm)],[c183])).
% 1.38/1.57 cnf(c185,plain,conceivedThru(X131,X131)|conceivedThru(X131,X132),inference(split_conjunct,[status(thm)],[c184])).
% 1.38/1.57 cnf(c201,plain,conceivedThru(X133,X133),inference(factor,[status(thm)],[c185])).
% 1.38/1.57 cnf(c204,plain,X307!=X305|X307!=X306|conceivedThru(X305,X306),inference(resolution,[status(thm)],[c201, c2])).
% 1.38/1.57 cnf(c234,plain,X310!=X311|conceivedThru(X311,X310),inference(resolution,[status(thm)],[c204, reflexivity])).
% 1.38/1.57 cnf(c40,axiom,X302!=X301|X304!=X303|~determinedByDefiniteMethod(X302,X304)|determinedByDefiniteMethod(X301,X303),theory(equality)).
% 1.38/1.57 fof(true_idea,axiom,(![X]:(![Y]:(trueIdea(X)=>(correspondWith(X,Y)&(ideateOf(Y,X)|objectOf(Y,X)))))),file('/export/starexec/sandbox/benchmark/Axioms/PHI002+1.ax', true_idea)).
% 1.38/1.57 fof(c150,plain,(![X]:(![Y]:(~trueIdea(X)|(correspondWith(X,Y)&(ideateOf(Y,X)|objectOf(Y,X)))))),inference(fof_nnf,[status(thm)],[true_idea])).
% 1.38/1.57 fof(c151,plain,(![X]:(~trueIdea(X)|((![Y]:correspondWith(X,Y))&(![Y]:(ideateOf(Y,X)|objectOf(Y,X)))))),inference(shift_quantors,[status(thm)],[c150])).
% 1.38/1.57 fof(c153,plain,(![X42]:(![X43]:(![X44]:(~trueIdea(X42)|(correspondWith(X42,X43)&(ideateOf(X44,X42)|objectOf(X44,X42))))))),inference(shift_quantors,[status(thm)],[fof(c152,plain,(![X42]:(~trueIdea(X42)|((![X43]:correspondWith(X42,X43))&(![X44]:(ideateOf(X44,X42)|objectOf(X44,X42)))))),inference(variable_rename,[status(thm)],[c151])).])).
% 1.38/1.57 fof(c154,plain,(![X42]:(![X43]:(![X44]:((~trueIdea(X42)|correspondWith(X42,X43))&(~trueIdea(X42)|(ideateOf(X44,X42)|objectOf(X44,X42))))))),inference(distribute,[status(thm)],[c153])).
% 1.38/1.57 cnf(c156,plain,~trueIdea(X292)|ideateOf(X293,X292)|objectOf(X293,X292),inference(split_conjunct,[status(thm)],[c154])).
% 1.38/1.57 cnf(c38,axiom,X289!=X288|X291!=X290|~determinedByItselfAlone(X289,X291)|determinedByItselfAlone(X288,X290),theory(equality)).
% 1.38/1.57 fof(finite_after_its_kind,axiom,(![X]:(![Y]:(finiteAfterItsKind(X)<=>(canBeLimitedBy(X,Y)&sameKind(X,Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', finite_after_its_kind)).
% 1.38/1.57 fof(c130,plain,(![X]:(![Y]:((~finiteAfterItsKind(X)|(canBeLimitedBy(X,Y)&sameKind(X,Y)))&((~canBeLimitedBy(X,Y)|~sameKind(X,Y))|finiteAfterItsKind(X))))),inference(fof_nnf,[status(thm)],[finite_after_its_kind])).
% 1.38/1.57 fof(c131,plain,((![X]:(~finiteAfterItsKind(X)|((![Y]:canBeLimitedBy(X,Y))&(![Y]:sameKind(X,Y)))))&(![X]:((![Y]:(~canBeLimitedBy(X,Y)|~sameKind(X,Y)))|finiteAfterItsKind(X)))),inference(shift_quantors,[status(thm)],[c130])).
% 1.38/1.57 fof(c133,plain,(![X34]:(![X35]:(![X36]:(![X37]:(![X38]:((~finiteAfterItsKind(X34)|(canBeLimitedBy(X34,X35)&sameKind(X34,X36)))&((~canBeLimitedBy(X37,X38)|~sameKind(X37,X38))|finiteAfterItsKind(X37)))))))),inference(shift_quantors,[status(thm)],[fof(c132,plain,((![X34]:(~finiteAfterItsKind(X34)|((![X35]:canBeLimitedBy(X34,X35))&(![X36]:sameKind(X34,X36)))))&(![X37]:((![X38]:(~canBeLimitedBy(X37,X38)|~sameKind(X37,X38)))|finiteAfterItsKind(X37)))),inference(variable_rename,[status(thm)],[c131])).])).
% 1.38/1.57 fof(c134,plain,(![X34]:(![X35]:(![X36]:(![X37]:(![X38]:(((~finiteAfterItsKind(X34)|canBeLimitedBy(X34,X35))&(~finiteAfterItsKind(X34)|sameKind(X34,X36)))&((~canBeLimitedBy(X37,X38)|~sameKind(X37,X38))|finiteAfterItsKind(X37)))))))),inference(distribute,[status(thm)],[c133])).
% 1.38/1.57 cnf(c137,plain,~canBeLimitedBy(X286,X287)|~sameKind(X286,X287)|finiteAfterItsKind(X286),inference(split_conjunct,[status(thm)],[c134])).
% 1.38/1.57 fof(free,axiom,(![X]:(![Y]:(free(X)<=>(existsOnlyByNecessityOfOwnNature(X)&(actionOf(Y,X)=>determinedByItselfAlone(Y,X)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', free)).
% 1.38/1.57 fof(c77,plain,(![X]:(![Y]:((~free(X)|(existsOnlyByNecessityOfOwnNature(X)&(~actionOf(Y,X)|determinedByItselfAlone(Y,X))))&((~existsOnlyByNecessityOfOwnNature(X)|(actionOf(Y,X)&~determinedByItselfAlone(Y,X)))|free(X))))),inference(fof_nnf,[status(thm)],[free])).
% 1.38/1.57 fof(c78,plain,((![X]:(~free(X)|(existsOnlyByNecessityOfOwnNature(X)&(![Y]:(~actionOf(Y,X)|determinedByItselfAlone(Y,X))))))&(![X]:((~existsOnlyByNecessityOfOwnNature(X)|((![Y]:actionOf(Y,X))&(![Y]:~determinedByItselfAlone(Y,X))))|free(X)))),inference(shift_quantors,[status(thm)],[c77])).
% 1.38/1.57 fof(c80,plain,(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:((~free(X15)|(existsOnlyByNecessityOfOwnNature(X15)&(~actionOf(X16,X15)|determinedByItselfAlone(X16,X15))))&((~existsOnlyByNecessityOfOwnNature(X17)|(actionOf(X18,X17)&~determinedByItselfAlone(X19,X17)))|free(X17)))))))),inference(shift_quantors,[status(thm)],[fof(c79,plain,((![X15]:(~free(X15)|(existsOnlyByNecessityOfOwnNature(X15)&(![X16]:(~actionOf(X16,X15)|determinedByItselfAlone(X16,X15))))))&(![X17]:((~existsOnlyByNecessityOfOwnNature(X17)|((![X18]:actionOf(X18,X17))&(![X19]:~determinedByItselfAlone(X19,X17))))|free(X17)))),inference(variable_rename,[status(thm)],[c78])).])).
% 1.38/1.57 fof(c81,plain,(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(((~free(X15)|existsOnlyByNecessityOfOwnNature(X15))&(~free(X15)|(~actionOf(X16,X15)|determinedByItselfAlone(X16,X15))))&(((~existsOnlyByNecessityOfOwnNature(X17)|actionOf(X18,X17))|free(X17))&((~existsOnlyByNecessityOfOwnNature(X17)|~determinedByItselfAlone(X19,X17))|free(X17))))))))),inference(distribute,[status(thm)],[c80])).
% 1.38/1.57 cnf(c83,plain,~free(X284)|~actionOf(X285,X284)|determinedByItselfAlone(X285,X284),inference(split_conjunct,[status(thm)],[c81])).
% 1.38/1.57 cnf(c94,plain,~absolutelyInfinite(X281)|~attributeOf(X280,X281)|expressesInfiniteEssentiality(X280),inference(split_conjunct,[status(thm)],[c90])).
% 1.38/1.57 cnf(c93,plain,~absolutelyInfinite(X279)|~attributeOf(X278,X279)|expressesEternalEssentiality(X278),inference(split_conjunct,[status(thm)],[c90])).
% 1.38/1.57 cnf(c37,axiom,X275!=X274|X277!=X276|~actionOf(X275,X277)|actionOf(X274,X276),theory(equality)).
% 1.38/1.57 cnf(c85,plain,~existsOnlyByNecessityOfOwnNature(X272)|~determinedByItselfAlone(X273,X272)|free(X272),inference(split_conjunct,[status(thm)],[c81])).
% 1.38/1.57 cnf(c84,plain,~existsOnlyByNecessityOfOwnNature(X271)|actionOf(X270,X271)|free(X271),inference(split_conjunct,[status(thm)],[c81])).
% 1.38/1.57 cnf(c47,axiom,X268!=X267|~hasEssence(X268)|hasEssence(X267),theory(equality)).
% 1.38/1.57 cnf(c32,axiom,X263!=X262|X265!=X264|~attributeOf(X263,X265)|attributeOf(X262,X264),theory(equality)).
% 1.38/1.57 cnf(c46,axiom,X261!=X260|~existConcFollowFromDefEternal(X261)|existConcFollowFromDefEternal(X260),theory(equality)).
% 1.38/1.57 cnf(c45,axiom,X258!=X257|~eternity(X258)|eternity(X257),theory(equality)).
% 1.38/1.57 cnf(c42,axiom,X255!=X254|~isMethodExistence(X255)|isMethodExistence(X254),theory(equality)).
% 1.38/1.57 cnf(c41,axiom,X248!=X247|~isMethodAction(X248)|isMethodAction(X247),theory(equality)).
% 1.38/1.57 cnf(c39,axiom,X245!=X244|~necessary(X245)|necessary(X244),theory(equality)).
% 1.38/1.57 cnf(c20,axiom,X240!=X239|X242!=X241|~sameKind(X240,X242)|sameKind(X239,X241),theory(equality)).
% 1.38/1.57 cnf(c36,axiom,X238!=X237|~existsOnlyByNecessityOfOwnNature(X238)|existsOnlyByNecessityOfOwnNature(X237),theory(equality)).
% 1.38/1.57 cnf(c35,axiom,X235!=X234|~free(X235)|free(X234),theory(equality)).
% 1.38/1.57 cnf(c34,axiom,X232!=X231|~expressesInfiniteEssentiality(X232)|expressesInfiniteEssentiality(X231),theory(equality)).
% 1.38/1.57 cnf(c19,axiom,X228!=X227|X230!=X229|~canBeLimitedBy(X228,X230)|canBeLimitedBy(X227,X229),theory(equality)).
% 1.38/1.57 cnf(c33,axiom,X225!=X224|~expressesEternalEssentiality(X225)|expressesEternalEssentiality(X224),theory(equality)).
% 1.38/1.57 cnf(c31,axiom,X222!=X221|~constInInfAttributes(X222)|constInInfAttributes(X221),theory(equality)).
% 1.38/1.57 cnf(c13,axiom,X217!=X216|X219!=X218|~objectOf(X217,X219)|objectOf(X216,X218),theory(equality)).
% 1.38/1.57 cnf(c30,axiom,X215!=X214|~absolutelyInfinite(X215)|absolutelyInfinite(X214),theory(equality)).
% 1.38/1.57 cnf(c29,axiom,X212!=X211|~being(X212)|being(X211),theory(equality)).
% 1.38/1.57 cnf(c28,axiom,X209!=X208|~god(X209)|god(X208),theory(equality)).
% 1.38/1.57 cnf(c12,axiom,X205!=X204|X207!=X206|~ideateOf(X205,X207)|ideateOf(X204,X206),theory(equality)).
% 1.38/1.57 cnf(c26,axiom,X202!=X201|~mode(X202)|mode(X201),theory(equality)).
% 1.38/1.57 cnf(c25,axiom,X199!=X198|~intPercAsConstEssSub(X199)|intPercAsConstEssSub(X198),theory(equality)).
% 1.38/1.57 cnf(c11,axiom,X194!=X193|X196!=X195|~correspondWith(X194,X196)|correspondWith(X193,X195),theory(equality)).
% 1.38/1.57 cnf(c24,axiom,X192!=X191|~attribute(X192)|attribute(X191),theory(equality)).
% 1.38/1.57 cnf(c23,axiom,X189!=X188|~conceivedThruItself(X189)|conceivedThruItself(X188),theory(equality)).
% 1.38/1.57 cnf(c22,axiom,X186!=X185|~inItself(X186)|inItself(X185),theory(equality)).
% 1.38/1.57 cnf(c9,axiom,X182!=X181|X184!=X183|~canBeUnderstoodInTermsOf(X182,X184)|canBeUnderstoodInTermsOf(X181,X183),theory(equality)).
% 1.38/1.57 cnf(c21,axiom,X179!=X178|~substance(X179)|substance(X178),theory(equality)).
% 1.38/1.57 cnf(c18,axiom,X176!=X175|~finiteAfterItsKind(X176)|finiteAfterItsKind(X175),theory(equality)).
% 1.38/1.57 cnf(c8,axiom,X171!=X170|X173!=X172|~conceptionInvolves(X171,X173)|conceptionInvolves(X170,X172),theory(equality)).
% 1.38/1.57 cnf(c17,axiom,X169!=X168|~natureConcOnlyByExistence(X169)|natureConcOnlyByExistence(X168),theory(equality)).
% 1.38/1.57 cnf(c16,axiom,X166!=X165|~selfCaused(X166)|selfCaused(X165),theory(equality)).
% 1.38/1.57 cnf(c15,axiom,X163!=X162|~essenceInvExistence(X163)|essenceInvExistence(X162),theory(equality)).
% 1.38/1.57 cnf(c7,axiom,X159!=X158|X161!=X160|~haveNothingInCommon(X159,X161)|haveNothingInCommon(X158,X160),theory(equality)).
% 1.38/1.57 cnf(c14,axiom,X156!=X155|~canBeConceivedAsNonExisting(X156)|canBeConceivedAsNonExisting(X155),theory(equality)).
% 1.38/1.57 cnf(c10,axiom,X153!=X152|~trueIdea(X153)|trueIdea(X152),theory(equality)).
% 1.38/1.57 cnf(c6,axiom,X150!=X149|~knowledgeOfACause(X150)|knowledgeOfACause(X149),theory(equality)).
% 1.38/1.57 cnf(c145,plain,~essenceInvExistence(X148)|~natureConcOnlyByExistence(X148)|selfCaused(X148),inference(split_conjunct,[status(thm)],[c142])).
% 1.38/1.57 cnf(c129,plain,~inItself(X147)|~conceivedThruItself(X147)|substance(X147),inference(split_conjunct,[status(thm)],[c126])).
% 1.38/1.57 fof(god,axiom,(![X]:(god(X)<=>(being(X)&absolutelyInfinite(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', god)).
% 1.38/1.57 fof(c97,plain,(![X]:((~god(X)|(being(X)&absolutelyInfinite(X)))&((~being(X)|~absolutelyInfinite(X))|god(X)))),inference(fof_nnf,[status(thm)],[god])).
% 1.38/1.57 fof(c98,plain,((![X]:(~god(X)|(being(X)&absolutelyInfinite(X))))&(![X]:((~being(X)|~absolutelyInfinite(X))|god(X)))),inference(shift_quantors,[status(thm)],[c97])).
% 1.38/1.57 fof(c100,plain,(![X25]:(![X26]:((~god(X25)|(being(X25)&absolutelyInfinite(X25)))&((~being(X26)|~absolutelyInfinite(X26))|god(X26))))),inference(shift_quantors,[status(thm)],[fof(c99,plain,((![X25]:(~god(X25)|(being(X25)&absolutelyInfinite(X25))))&(![X26]:((~being(X26)|~absolutelyInfinite(X26))|god(X26)))),inference(variable_rename,[status(thm)],[c98])).])).
% 1.38/1.57 fof(c101,plain,(![X25]:(![X26]:(((~god(X25)|being(X25))&(~god(X25)|absolutelyInfinite(X25)))&((~being(X26)|~absolutelyInfinite(X26))|god(X26))))),inference(distribute,[status(thm)],[c100])).
% 1.38/1.57 cnf(c104,plain,~being(X146)|~absolutelyInfinite(X146)|god(X146),inference(split_conjunct,[status(thm)],[c101])).
% 1.38/1.57 cnf(c74,plain,~necessary(X145)|isMethodAction(X144)|isMethodExistence(X144),inference(split_conjunct,[status(thm)],[c70])).
% 1.38/1.57 cnf(c5,axiom,X140!=X139|X142!=X141|~knowledgeOfEffect(X140,X142)|knowledgeOfEffect(X139,X141),theory(equality)).
% 1.38/1.57 cnf(c4,axiom,X128!=X127|X130!=X129|~effectNecessarilyFollowsFrom(X128,X130)|effectNecessarilyFollowsFrom(X127,X129),theory(equality)).
% 1.38/1.57 fof(have_nothing_in_common,axiom,(![X]:(![Y]:(haveNothingInCommon(X,Y)=>((((~canBeUnderstoodInTermsOf(X,Y))&(~canBeUnderstoodInTermsOf(Y,X)))&(~conceptionInvolves(X,Y)))&(~conceptionInvolves(Y,X)))))),file('/export/starexec/sandbox/benchmark/Axioms/PHI002+1.ax', have_nothing_in_common)).
% 1.38/1.57 fof(c157,plain,(![X]:(![Y]:(haveNothingInCommon(X,Y)=>(((~canBeUnderstoodInTermsOf(X,Y)&~canBeUnderstoodInTermsOf(Y,X))&~conceptionInvolves(X,Y))&~conceptionInvolves(Y,X))))),inference(fof_simplification,[status(thm)],[have_nothing_in_common])).
% 1.38/1.57 fof(c158,plain,(![X]:(![Y]:(~haveNothingInCommon(X,Y)|(((~canBeUnderstoodInTermsOf(X,Y)&~canBeUnderstoodInTermsOf(Y,X))&~conceptionInvolves(X,Y))&~conceptionInvolves(Y,X))))),inference(fof_nnf,[status(thm)],[c157])).
% 1.38/1.57 fof(c159,plain,(![X45]:(![X46]:(~haveNothingInCommon(X45,X46)|(((~canBeUnderstoodInTermsOf(X45,X46)&~canBeUnderstoodInTermsOf(X46,X45))&~conceptionInvolves(X45,X46))&~conceptionInvolves(X46,X45))))),inference(variable_rename,[status(thm)],[c158])).
% 1.38/1.57 fof(c160,plain,(![X45]:(![X46]:((((~haveNothingInCommon(X45,X46)|~canBeUnderstoodInTermsOf(X45,X46))&(~haveNothingInCommon(X45,X46)|~canBeUnderstoodInTermsOf(X46,X45)))&(~haveNothingInCommon(X45,X46)|~conceptionInvolves(X45,X46)))&(~haveNothingInCommon(X45,X46)|~conceptionInvolves(X46,X45))))),inference(distribute,[status(thm)],[c159])).
% 1.38/1.57 cnf(c164,plain,~haveNothingInCommon(X125,X126)|~conceptionInvolves(X126,X125),inference(split_conjunct,[status(thm)],[c160])).
% 1.38/1.57 cnf(c163,plain,~haveNothingInCommon(X123,X124)|~conceptionInvolves(X123,X124),inference(split_conjunct,[status(thm)],[c160])).
% 1.38/1.57 cnf(c162,plain,~haveNothingInCommon(X121,X122)|~canBeUnderstoodInTermsOf(X122,X121),inference(split_conjunct,[status(thm)],[c160])).
% 1.38/1.57 cnf(c161,plain,~haveNothingInCommon(X119,X120)|~canBeUnderstoodInTermsOf(X119,X120),inference(split_conjunct,[status(thm)],[c160])).
% 1.38/1.57 cnf(c3,axiom,X117!=X116|~definiteCause(X117)|definiteCause(X116),theory(equality)).
% 1.38/1.57 fof(definite_cause,axiom,(![X]:(![Y]:(definiteCause(X)=>(effectNecessarilyFollowsFrom(Y,X)&((~definiteCause(X))=>(~effectNecessarilyFollowsFrom(Y,X))))))),file('/export/starexec/sandbox/benchmark/Axioms/PHI002+1.ax', definite_cause)).
% 1.38/1.57 fof(c171,plain,(![X]:(![Y]:(definiteCause(X)=>(effectNecessarilyFollowsFrom(Y,X)&(~definiteCause(X)=>~effectNecessarilyFollowsFrom(Y,X)))))),inference(fof_simplification,[status(thm)],[definite_cause])).
% 1.38/1.57 fof(c172,plain,(![X]:(![Y]:(~definiteCause(X)|(effectNecessarilyFollowsFrom(Y,X)&(definiteCause(X)|~effectNecessarilyFollowsFrom(Y,X)))))),inference(fof_nnf,[status(thm)],[c171])).
% 1.38/1.57 fof(c173,plain,(![X]:(~definiteCause(X)|((![Y]:effectNecessarilyFollowsFrom(Y,X))&(definiteCause(X)|(![Y]:~effectNecessarilyFollowsFrom(Y,X)))))),inference(shift_quantors,[status(thm)],[c172])).
% 1.38/1.57 fof(c175,plain,(![X51]:(![X52]:(![X53]:(~definiteCause(X51)|(effectNecessarilyFollowsFrom(X52,X51)&(definiteCause(X51)|~effectNecessarilyFollowsFrom(X53,X51))))))),inference(shift_quantors,[status(thm)],[fof(c174,plain,(![X51]:(~definiteCause(X51)|((![X52]:effectNecessarilyFollowsFrom(X52,X51))&(definiteCause(X51)|(![X53]:~effectNecessarilyFollowsFrom(X53,X51)))))),inference(variable_rename,[status(thm)],[c173])).])).
% 1.38/1.57 fof(c176,plain,(![X51]:(![X52]:(![X53]:((~definiteCause(X51)|effectNecessarilyFollowsFrom(X52,X51))&(~definiteCause(X51)|(definiteCause(X51)|~effectNecessarilyFollowsFrom(X53,X51))))))),inference(distribute,[status(thm)],[c175])).
% 1.38/1.57 cnf(c177,plain,~definiteCause(X114)|effectNecessarilyFollowsFrom(X113,X114),inference(split_conjunct,[status(thm)],[c176])).
% 1.38/1.57 fof(knowledge_of_effect,axiom,(![X]:(![Y]:(knowledgeOfEffect(X,Y)<=>knowledgeOfACause(X)))),file('/export/starexec/sandbox/benchmark/Axioms/PHI002+1.ax', knowledge_of_effect)).
% 1.38/1.57 fof(c165,plain,(![X]:(![Y]:((~knowledgeOfEffect(X,Y)|knowledgeOfACause(X))&(~knowledgeOfACause(X)|knowledgeOfEffect(X,Y))))),inference(fof_nnf,[status(thm)],[knowledge_of_effect])).
% 1.38/1.57 fof(c166,plain,((![X]:((![Y]:~knowledgeOfEffect(X,Y))|knowledgeOfACause(X)))&(![X]:(~knowledgeOfACause(X)|(![Y]:knowledgeOfEffect(X,Y))))),inference(shift_quantors,[status(thm)],[c165])).
% 1.38/1.57 fof(c168,plain,(![X47]:(![X48]:(![X49]:(![X50]:((~knowledgeOfEffect(X47,X48)|knowledgeOfACause(X47))&(~knowledgeOfACause(X49)|knowledgeOfEffect(X49,X50))))))),inference(shift_quantors,[status(thm)],[fof(c167,plain,((![X47]:((![X48]:~knowledgeOfEffect(X47,X48))|knowledgeOfACause(X47)))&(![X49]:(~knowledgeOfACause(X49)|(![X50]:knowledgeOfEffect(X49,X50))))),inference(variable_rename,[status(thm)],[c166])).])).
% 1.38/1.57 cnf(c170,plain,~knowledgeOfACause(X112)|knowledgeOfEffect(X112,X111),inference(split_conjunct,[status(thm)],[c168])).
% 1.38/1.57 cnf(c169,plain,~knowledgeOfEffect(X109,X110)|knowledgeOfACause(X109),inference(split_conjunct,[status(thm)],[c168])).
% 1.38/1.57 cnf(c155,plain,~trueIdea(X108)|correspondWith(X108,X107),inference(split_conjunct,[status(thm)],[c154])).
% 1.38/1.57 cnf(c136,plain,~finiteAfterItsKind(X101)|sameKind(X101,X102),inference(split_conjunct,[status(thm)],[c134])).
% 1.38/1.57 cnf(c135,plain,~finiteAfterItsKind(X99)|canBeLimitedBy(X99,X100),inference(split_conjunct,[status(thm)],[c134])).
% 1.38/1.57 cnf(c73,plain,~necessary(X98)|determinedByDefiniteMethod(X98,X97),inference(split_conjunct,[status(thm)],[c70])).
% 1.38/1.57 cnf(c72,plain,~necessary(X96)|determinedByFixedMethod(X96,X95),inference(split_conjunct,[status(thm)],[c70])).
% 1.38/1.57 cnf(c71,plain,~necessary(X94)|externalTo(X93,X94),inference(split_conjunct,[status(thm)],[c70])).
% 1.38/1.57 fof(attribute,axiom,(![X]:(attribute(X)<=>intPercAsConstEssSub(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', attribute)).
% 1.38/1.57 fof(c116,plain,(![X]:((~attribute(X)|intPercAsConstEssSub(X))&(~intPercAsConstEssSub(X)|attribute(X)))),inference(fof_nnf,[status(thm)],[attribute])).
% 1.38/1.57 fof(c117,plain,((![X]:(~attribute(X)|intPercAsConstEssSub(X)))&(![X]:(~intPercAsConstEssSub(X)|attribute(X)))),inference(shift_quantors,[status(thm)],[c116])).
% 1.38/1.57 fof(c119,plain,(![X30]:(![X31]:((~attribute(X30)|intPercAsConstEssSub(X30))&(~intPercAsConstEssSub(X31)|attribute(X31))))),inference(shift_quantors,[status(thm)],[fof(c118,plain,((![X30]:(~attribute(X30)|intPercAsConstEssSub(X30)))&(![X31]:(~intPercAsConstEssSub(X31)|attribute(X31)))),inference(variable_rename,[status(thm)],[c117])).])).
% 1.38/1.57 cnf(c121,plain,~intPercAsConstEssSub(X80)|attribute(X80),inference(split_conjunct,[status(thm)],[c119])).
% 1.38/1.57 cnf(c120,plain,~attribute(X79)|intPercAsConstEssSub(X79),inference(split_conjunct,[status(thm)],[c119])).
% 1.38/1.57 cnf(c103,plain,~god(X78)|absolutelyInfinite(X78),inference(split_conjunct,[status(thm)],[c101])).
% 1.38/1.57 cnf(c102,plain,~god(X77)|being(X77),inference(split_conjunct,[status(thm)],[c101])).
% 1.38/1.57 cnf(transitivity,axiom,X74!=X76|X76!=X75|X74=X75,theory(equality)).
% 1.38/1.57 cnf(c92,plain,~absolutelyInfinite(X73)|constInInfAttributes(X73),inference(split_conjunct,[status(thm)],[c90])).
% 1.38/1.57 cnf(c91,plain,~absolutelyInfinite(X72)|substance(X72),inference(split_conjunct,[status(thm)],[c90])).
% 1.38/1.57 cnf(c82,plain,~free(X71)|existsOnlyByNecessityOfOwnNature(X71),inference(split_conjunct,[status(thm)],[c81])).
% 1.38/1.57 fof(eternity,axiom,(![X]:(eternity(X)<=>existConcFollowFromDefEternal(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', eternity)).
% 1.38/1.57 fof(c60,plain,(![X]:((~eternity(X)|existConcFollowFromDefEternal(X))&(~existConcFollowFromDefEternal(X)|eternity(X)))),inference(fof_nnf,[status(thm)],[eternity])).
% 1.38/1.57 fof(c61,plain,((![X]:(~eternity(X)|existConcFollowFromDefEternal(X)))&(![X]:(~existConcFollowFromDefEternal(X)|eternity(X)))),inference(shift_quantors,[status(thm)],[c60])).
% 1.38/1.57 fof(c63,plain,(![X6]:(![X7]:((~eternity(X6)|existConcFollowFromDefEternal(X6))&(~existConcFollowFromDefEternal(X7)|eternity(X7))))),inference(shift_quantors,[status(thm)],[fof(c62,plain,((![X6]:(~eternity(X6)|existConcFollowFromDefEternal(X6)))&(![X7]:(~existConcFollowFromDefEternal(X7)|eternity(X7)))),inference(variable_rename,[status(thm)],[c61])).])).
% 1.38/1.57 cnf(c65,plain,~existConcFollowFromDefEternal(X70)|eternity(X70),inference(split_conjunct,[status(thm)],[c63])).
% 1.38/1.57 cnf(c64,plain,~eternity(X66)|existConcFollowFromDefEternal(X66),inference(split_conjunct,[status(thm)],[c63])).
% 1.38/1.57 % SZS output end Saturation
% 1.38/1.57
% 1.38/1.57 % Initial clauses : 110
% 1.38/1.57 % Processed clauses : 307
% 1.38/1.57 % Factors computed : 18
% 1.38/1.57 % Resolvents computed: 1287
% 1.38/1.57 % Tautologies deleted: 72
% 1.38/1.57 % Forward subsumed : 1036
% 1.38/1.57 % Backward subsumed : 57
% 1.38/1.57 % -------- CPU Time ---------
% 1.38/1.57 % User time : 1.195 s
% 1.38/1.57 % System time : 0.020 s
% 1.38/1.57 % Total time : 1.215 s
%------------------------------------------------------------------------------