%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PHI038+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:20 EDT 2024
% Result : CounterSatisfiable 0.77s 0.95s
% Output : Saturation 0.77s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : PHI038+1 : TPTP v8.1.2. Released v7.4.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n004.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Wed May 8 22:29:08 EDT 2024
% 0.15/0.36 % CPUTime :
% 0.77/0.95 % Version: 1.5
% 0.77/0.95 % SZS status CounterSatisfiable
% 0.77/0.95 % SZS output start Saturation
% 0.77/0.95 cnf(reflexivity,axiom,X66=X66,theory(equality)).
% 0.77/0.95 cnf(c1,axiom,X98!=X96|X95!=X97|~existsIn(X98,X95)|existsIn(X96,X97),theory(equality)).
% 0.77/0.95 fof(mode,axiom,(![X]:(![Y]:(![Z]:(mode(X)<=>((modification(X,Y)&substance(Y))|(existsIn(X,Z)&conceivedThru(X,Z))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', mode)).
% 0.77/0.95 fof(c105,plain,(![X]:(![Y]:(![Z]:((~mode(X)|((modification(X,Y)&substance(Y))|(existsIn(X,Z)&conceivedThru(X,Z))))&(((~modification(X,Y)|~substance(Y))&(~existsIn(X,Z)|~conceivedThru(X,Z)))|mode(X)))))),inference(fof_nnf,[status(thm)],[mode])).
% 0.77/0.95 fof(c106,plain,((![X]:(~mode(X)|(((![Y]:modification(X,Y))&(![Y]:substance(Y)))|((![Z]:existsIn(X,Z))&(![Z]:conceivedThru(X,Z))))))&(![X]:(((![Y]:(~modification(X,Y)|~substance(Y)))&(![Z]:(~existsIn(X,Z)|~conceivedThru(X,Z))))|mode(X)))),inference(shift_quantors,[status(thm)],[c105])).
% 0.77/0.95 fof(c108,plain,(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:(![X32]:(![X33]:((~mode(X26)|((modification(X26,X27)&substance(X28))|(existsIn(X26,X29)&conceivedThru(X26,X30))))&(((~modification(X31,X32)|~substance(X32))&(~existsIn(X31,X33)|~conceivedThru(X31,X33)))|mode(X31))))))))))),inference(shift_quantors,[status(thm)],[fof(c107,plain,((![X26]:(~mode(X26)|(((![X27]:modification(X26,X27))&(![X28]:substance(X28)))|((![X29]:existsIn(X26,X29))&(![X30]:conceivedThru(X26,X30))))))&(![X31]:(((![X32]:(~modification(X31,X32)|~substance(X32)))&(![X33]:(~existsIn(X31,X33)|~conceivedThru(X31,X33))))|mode(X31)))),inference(variable_rename,[status(thm)],[c106])).])).
% 0.77/0.95 fof(c109,plain,(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:(![X32]:(![X33]:((((~mode(X26)|(modification(X26,X27)|existsIn(X26,X29)))&(~mode(X26)|(modification(X26,X27)|conceivedThru(X26,X30))))&((~mode(X26)|(substance(X28)|existsIn(X26,X29)))&(~mode(X26)|(substance(X28)|conceivedThru(X26,X30)))))&(((~modification(X31,X32)|~substance(X32))|mode(X31))&((~existsIn(X31,X33)|~conceivedThru(X31,X33))|mode(X31)))))))))))),inference(distribute,[status(thm)],[c108])).
% 0.77/0.95 cnf(c110,plain,~mode(X308)|modification(X308,X307)|existsIn(X308,X309),inference(split_conjunct,[status(thm)],[c109])).
% 0.77/0.95 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)).
% 0.77/0.95 fof(c179,plain,(![X]:(![Y]:(~conceivedThru(X,X)=>(conceivedThru(X,Y)&X!=Y)))),inference(fof_simplification,[status(thm)],[conceived_through])).
% 0.77/0.95 fof(c180,plain,(![X]:(![Y]:(conceivedThru(X,X)|(conceivedThru(X,Y)&X!=Y)))),inference(fof_nnf,[status(thm)],[c179])).
% 0.77/0.95 fof(c181,plain,(![X]:(conceivedThru(X,X)|((![Y]:conceivedThru(X,Y))&(![Y]:X!=Y)))),inference(shift_quantors,[status(thm)],[c180])).
% 0.77/0.95 fof(c183,plain,(![X58]:(![X59]:(![X60]:(conceivedThru(X58,X58)|(conceivedThru(X58,X59)&X58!=X60))))),inference(shift_quantors,[status(thm)],[fof(c182,plain,(![X58]:(conceivedThru(X58,X58)|((![X59]:conceivedThru(X58,X59))&(![X60]:X58!=X60)))),inference(variable_rename,[status(thm)],[c181])).])).
% 0.77/0.95 fof(c184,plain,(![X58]:(![X59]:(![X60]:((conceivedThru(X58,X58)|conceivedThru(X58,X59))&(conceivedThru(X58,X58)|X58!=X60))))),inference(distribute,[status(thm)],[c183])).
% 0.77/0.95 cnf(c185,plain,conceivedThru(X133,X133)|conceivedThru(X133,X134),inference(split_conjunct,[status(thm)],[c184])).
% 0.77/0.95 cnf(c204,plain,conceivedThru(X135,X135),inference(factor,[status(thm)],[c185])).
% 0.77/0.95 cnf(c115,plain,~existsIn(X313,X314)|~conceivedThru(X313,X314)|mode(X313),inference(split_conjunct,[status(thm)],[c109])).
% 0.77/0.95 cnf(c245,plain,~existsIn(X315,X315)|mode(X315),inference(resolution,[status(thm)],[c115, c204])).
% 0.77/0.95 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)).
% 0.77/0.95 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])).
% 0.77/0.95 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])).
% 0.77/0.95 fof(c190,plain,(![X61]:(![X62]:(![X63]:(![X64]:(![X65]:((~exists(X61)|(existsIn(X61,X61)|(existsIn(X61,X62)&X61!=X63)))&((~existsIn(X64,X64)&(~existsIn(X64,X65)|X64=X65))|exists(X64)))))))),inference(shift_quantors,[status(thm)],[fof(c189,plain,((![X61]:(~exists(X61)|(existsIn(X61,X61)|((![X62]:existsIn(X61,X62))&(![X63]:X61!=X63)))))&(![X64]:((~existsIn(X64,X64)&(![X65]:(~existsIn(X64,X65)|X64=X65)))|exists(X64)))),inference(variable_rename,[status(thm)],[c188])).])).
% 0.77/0.95 fof(c191,plain,(![X61]:(![X62]:(![X63]:(![X64]:(![X65]:(((~exists(X61)|(existsIn(X61,X61)|existsIn(X61,X62)))&(~exists(X61)|(existsIn(X61,X61)|X61!=X63)))&((~existsIn(X64,X64)|exists(X64))&((~existsIn(X64,X65)|X64=X65)|exists(X64))))))))),inference(distribute,[status(thm)],[c190])).
% 0.77/0.95 cnf(c193,plain,~exists(X327)|existsIn(X327,X327)|X327!=X326,inference(split_conjunct,[status(thm)],[c191])).
% 0.77/0.95 cnf(c246,plain,~exists(X328)|existsIn(X328,X328),inference(resolution,[status(thm)],[c193, reflexivity])).
% 0.77/0.95 fof(self_caused,axiom,(![X]:(selfCaused(X)<=>(essenceInvExistence(X)&natureConcOnlyByExistence(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', self_caused)).
% 0.77/0.95 fof(c138,plain,(![X]:((~selfCaused(X)|(essenceInvExistence(X)&natureConcOnlyByExistence(X)))&((~essenceInvExistence(X)|~natureConcOnlyByExistence(X))|selfCaused(X)))),inference(fof_nnf,[status(thm)],[self_caused])).
% 0.77/0.95 fof(c139,plain,((![X]:(~selfCaused(X)|(essenceInvExistence(X)&natureConcOnlyByExistence(X))))&(![X]:((~essenceInvExistence(X)|~natureConcOnlyByExistence(X))|selfCaused(X)))),inference(shift_quantors,[status(thm)],[c138])).
% 0.77/0.95 fof(c141,plain,(![X43]:(![X44]:((~selfCaused(X43)|(essenceInvExistence(X43)&natureConcOnlyByExistence(X43)))&((~essenceInvExistence(X44)|~natureConcOnlyByExistence(X44))|selfCaused(X44))))),inference(shift_quantors,[status(thm)],[fof(c140,plain,((![X43]:(~selfCaused(X43)|(essenceInvExistence(X43)&natureConcOnlyByExistence(X43))))&(![X44]:((~essenceInvExistence(X44)|~natureConcOnlyByExistence(X44))|selfCaused(X44)))),inference(variable_rename,[status(thm)],[c139])).])).
% 0.77/0.95 fof(c142,plain,(![X43]:(![X44]:(((~selfCaused(X43)|essenceInvExistence(X43))&(~selfCaused(X43)|natureConcOnlyByExistence(X43)))&((~essenceInvExistence(X44)|~natureConcOnlyByExistence(X44))|selfCaused(X44))))),inference(distribute,[status(thm)],[c141])).
% 0.77/0.95 cnf(c143,plain,~selfCaused(X85)|essenceInvExistence(X85),inference(split_conjunct,[status(thm)],[c142])).
% 0.77/0.95 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)).
% 0.77/0.95 fof(c54,plain,(![X]:(~inItself(X)|selfCaused(X))),inference(fof_nnf,[status(thm)],[is_in_itself_is_self_caused])).
% 0.77/0.95 fof(c55,plain,(![X4]:(~inItself(X4)|selfCaused(X4))),inference(variable_rename,[status(thm)],[c54])).
% 0.77/0.95 cnf(c56,plain,~inItself(X68)|selfCaused(X68),inference(split_conjunct,[status(thm)],[c55])).
% 0.77/0.95 fof(substance,axiom,(![X]:(substance(X)<=>(inItself(X)&conceivedThruItself(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', substance)).
% 0.77/0.95 fof(c122,plain,(![X]:((~substance(X)|(inItself(X)&conceivedThruItself(X)))&((~inItself(X)|~conceivedThruItself(X))|substance(X)))),inference(fof_nnf,[status(thm)],[substance])).
% 0.77/0.95 fof(c123,plain,((![X]:(~substance(X)|(inItself(X)&conceivedThruItself(X))))&(![X]:((~inItself(X)|~conceivedThruItself(X))|substance(X)))),inference(shift_quantors,[status(thm)],[c122])).
% 0.77/0.95 fof(c125,plain,(![X36]:(![X37]:((~substance(X36)|(inItself(X36)&conceivedThruItself(X36)))&((~inItself(X37)|~conceivedThruItself(X37))|substance(X37))))),inference(shift_quantors,[status(thm)],[fof(c124,plain,((![X36]:(~substance(X36)|(inItself(X36)&conceivedThruItself(X36))))&(![X37]:((~inItself(X37)|~conceivedThruItself(X37))|substance(X37)))),inference(variable_rename,[status(thm)],[c123])).])).
% 0.77/0.95 fof(c126,plain,(![X36]:(![X37]:(((~substance(X36)|inItself(X36))&(~substance(X36)|conceivedThruItself(X36)))&((~inItself(X37)|~conceivedThruItself(X37))|substance(X37))))),inference(distribute,[status(thm)],[c125])).
% 0.77/0.95 cnf(c127,plain,~substance(X83)|inItself(X83),inference(split_conjunct,[status(thm)],[c126])).
% 0.77/0.95 cnf(c112,plain,~mode(X292)|substance(X291)|existsIn(X292,X293),inference(split_conjunct,[status(thm)],[c109])).
% 0.77/0.95 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)).
% 0.77/0.95 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])).
% 0.77/0.95 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])).
% 0.77/0.95 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])).])).
% 0.77/0.95 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])).
% 0.77/0.95 cnf(c91,plain,~absolutelyInfinite(X76)|substance(X76),inference(split_conjunct,[status(thm)],[c90])).
% 0.77/0.95 fof(god,conjecture,(![X]:(god(X)<=>(being(X)&absolutelyInfinite(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', god)).
% 0.77/0.95 fof(c97,negated_conjecture,(~(![X]:(god(X)<=>(being(X)&absolutelyInfinite(X))))),inference(assume_negation,[status(cth)],[god])).
% 0.77/0.95 fof(c98,negated_conjecture,(?[X]:((~god(X)|(~being(X)|~absolutelyInfinite(X)))&(god(X)|(being(X)&absolutelyInfinite(X))))),inference(fof_nnf,[status(thm)],[c97])).
% 0.77/0.95 fof(c99,negated_conjecture,(?[X25]:((~god(X25)|(~being(X25)|~absolutelyInfinite(X25)))&(god(X25)|(being(X25)&absolutelyInfinite(X25))))),inference(variable_rename,[status(thm)],[c98])).
% 0.77/0.95 fof(c100,negated_conjecture,((~god(skolem0001)|(~being(skolem0001)|~absolutelyInfinite(skolem0001)))&(god(skolem0001)|(being(skolem0001)&absolutelyInfinite(skolem0001)))),inference(skolemize,[status(esa)],[c99])).
% 0.77/0.95 fof(c101,negated_conjecture,((~god(skolem0001)|(~being(skolem0001)|~absolutelyInfinite(skolem0001)))&((god(skolem0001)|being(skolem0001))&(god(skolem0001)|absolutelyInfinite(skolem0001)))),inference(distribute,[status(thm)],[c100])).
% 0.77/0.95 cnf(c104,negated_conjecture,god(skolem0001)|absolutelyInfinite(skolem0001),inference(split_conjunct,[status(thm)],[c101])).
% 0.77/0.95 cnf(c201,plain,god(skolem0001)|substance(skolem0001),inference(resolution,[status(thm)],[c104, c91])).
% 0.77/0.95 cnf(c209,plain,god(skolem0001)|inItself(skolem0001),inference(resolution,[status(thm)],[c201, c127])).
% 0.77/0.95 cnf(c211,plain,god(skolem0001)|selfCaused(skolem0001),inference(resolution,[status(thm)],[c209, c56])).
% 0.77/0.95 cnf(c213,plain,god(skolem0001)|essenceInvExistence(skolem0001),inference(resolution,[status(thm)],[c211, c143])).
% 0.77/0.95 fof(being_has_essense,axiom,(![X]:(being(X)=>hasEssence(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', being_has_essense)).
% 0.77/0.95 fof(c51,plain,(![X]:(~being(X)|hasEssence(X))),inference(fof_nnf,[status(thm)],[being_has_essense])).
% 0.77/0.95 fof(c52,plain,(![X3]:(~being(X3)|hasEssence(X3))),inference(variable_rename,[status(thm)],[c51])).
% 0.77/0.95 cnf(c53,plain,~being(X67)|hasEssence(X67),inference(split_conjunct,[status(thm)],[c52])).
% 0.77/0.95 cnf(c103,negated_conjecture,god(skolem0001)|being(skolem0001),inference(split_conjunct,[status(thm)],[c101])).
% 0.77/0.95 cnf(c200,plain,god(skolem0001)|hasEssence(skolem0001),inference(resolution,[status(thm)],[c103, c53])).
% 0.77/0.95 fof(essence_involves_existence_exists,axiom,(![X]:((essenceInvExistence(X)&hasEssence(X))=>exists(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', essence_involves_existence_exists)).
% 0.77/0.95 fof(c48,plain,(![X]:((~essenceInvExistence(X)|~hasEssence(X))|exists(X))),inference(fof_nnf,[status(thm)],[essence_involves_existence_exists])).
% 0.77/0.95 fof(c49,plain,(![X2]:((~essenceInvExistence(X2)|~hasEssence(X2))|exists(X2))),inference(variable_rename,[status(thm)],[c48])).
% 0.77/0.95 cnf(c50,plain,~essenceInvExistence(X152)|~hasEssence(X152)|exists(X152),inference(split_conjunct,[status(thm)],[c49])).
% 0.77/0.95 cnf(c216,plain,~essenceInvExistence(skolem0001)|exists(skolem0001)|god(skolem0001),inference(resolution,[status(thm)],[c50, c200])).
% 0.77/0.95 cnf(c251,plain,exists(skolem0001)|god(skolem0001),inference(resolution,[status(thm)],[c216, c213])).
% 0.77/0.95 cnf(c252,plain,god(skolem0001)|existsIn(skolem0001,skolem0001),inference(resolution,[status(thm)],[c251, c246])).
% 0.77/0.95 cnf(c254,plain,god(skolem0001)|mode(skolem0001),inference(resolution,[status(thm)],[c252, c245])).
% 0.77/0.95 cnf(c260,plain,god(skolem0001)|substance(X349)|existsIn(skolem0001,X350),inference(resolution,[status(thm)],[c254, c112])).
% 0.77/0.95 cnf(c268,plain,god(skolem0001)|existsIn(skolem0001,X368)|inItself(X367),inference(resolution,[status(thm)],[c260, c127])).
% 0.77/0.95 cnf(c292,plain,god(skolem0001)|existsIn(skolem0001,X390)|selfCaused(X389),inference(resolution,[status(thm)],[c268, c56])).
% 0.77/0.95 cnf(c316,plain,god(skolem0001)|existsIn(skolem0001,X400)|essenceInvExistence(X399),inference(resolution,[status(thm)],[c292, c143])).
% 0.77/0.95 fof(has_substance_being,axiom,(![X]:(substance(X)=>being(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', has_substance_being)).
% 0.77/0.95 fof(c57,plain,(![X]:(~substance(X)|being(X))),inference(fof_nnf,[status(thm)],[has_substance_being])).
% 0.77/0.95 fof(c58,plain,(![X5]:(~substance(X5)|being(X5))),inference(variable_rename,[status(thm)],[c57])).
% 0.77/0.95 cnf(c59,plain,~substance(X69)|being(X69),inference(split_conjunct,[status(thm)],[c58])).
% 0.77/0.95 cnf(c267,plain,god(skolem0001)|existsIn(skolem0001,X364)|being(X363),inference(resolution,[status(thm)],[c260, c59])).
% 0.77/0.95 cnf(c287,plain,god(skolem0001)|existsIn(skolem0001,X383)|hasEssence(X384),inference(resolution,[status(thm)],[c267, c53])).
% 0.77/0.95 cnf(c309,plain,god(skolem0001)|existsIn(skolem0001,X430)|~essenceInvExistence(X429)|exists(X429),inference(resolution,[status(thm)],[c287, c50])).
% 0.77/0.95 cnf(c352,plain,god(skolem0001)|existsIn(skolem0001,X657)|exists(X658)|existsIn(skolem0001,X659),inference(resolution,[status(thm)],[c309, c316])).
% 0.77/0.95 cnf(c417,plain,god(skolem0001)|existsIn(skolem0001,X661)|exists(X660),inference(factor,[status(thm)],[c352])).
% 0.77/0.95 cnf(c431,plain,god(skolem0001)|existsIn(skolem0001,X668)|existsIn(X669,X669),inference(resolution,[status(thm)],[c417, c246])).
% 0.77/0.95 cnf(c440,plain,god(skolem0001)|existsIn(skolem0001,X675)|mode(X674),inference(resolution,[status(thm)],[c431, c245])).
% 0.77/0.95 cnf(c448,plain,god(skolem0001)|existsIn(skolem0001,X772)|modification(X770,X769)|existsIn(X770,X771),inference(resolution,[status(thm)],[c440, c110])).
% 0.77/0.95 cnf(c494,plain,god(skolem0001)|existsIn(skolem0001,X1201)|modification(X1200,X1203)|X1200!=X1202|X1204!=X1205|existsIn(X1202,X1205),inference(resolution,[status(thm)],[c448, c1])).
% 0.77/0.95 cnf(c562,plain,god(skolem0001)|existsIn(skolem0001,X1219)|modification(X1220,X1223)|X1220!=X1222|existsIn(X1222,X1221),inference(resolution,[status(thm)],[c494, reflexivity])).
% 0.77/0.95 cnf(c27,axiom,X241!=X239|X238!=X240|~modification(X241,X238)|modification(X239,X240),theory(equality)).
% 0.77/0.95 cnf(c490,plain,god(skolem0001)|existsIn(skolem0001,X1174)|existsIn(X1176,X1178)|X1176!=X1177|X1175!=X1179|modification(X1177,X1179),inference(resolution,[status(thm)],[c448, c27])).
% 0.77/0.95 cnf(c558,plain,god(skolem0001)|existsIn(skolem0001,X1206)|existsIn(X1209,X1207)|X1209!=X1208|modification(X1208,X1210),inference(resolution,[status(thm)],[c490, reflexivity])).
% 0.77/0.95 cnf(c488,plain,god(skolem0001)|modification(X1171,X1169)|existsIn(X1171,X1173)|skolem0001!=X1168|X1170!=X1172|existsIn(X1168,X1172),inference(resolution,[status(thm)],[c448, c1])).
% 0.77/0.95 cnf(c556,plain,god(skolem0001)|modification(X1184,X1185)|existsIn(X1184,X1188)|skolem0001!=X1186|existsIn(X1186,X1187),inference(resolution,[status(thm)],[c488, reflexivity])).
% 0.77/0.95 cnf(c2,axiom,X112!=X110|X109!=X111|~conceivedThru(X112,X109)|conceivedThru(X110,X111),theory(equality)).
% 0.77/0.95 cnf(c111,plain,~mode(X311)|modification(X311,X310)|conceivedThru(X311,X312),inference(split_conjunct,[status(thm)],[c109])).
% 0.77/0.95 cnf(c447,plain,god(skolem0001)|existsIn(skolem0001,X757)|modification(X755,X756)|conceivedThru(X755,X754),inference(resolution,[status(thm)],[c440, c111])).
% 0.77/0.95 cnf(c482,plain,god(skolem0001)|existsIn(skolem0001,X1148)|modification(X1150,X1149)|X1150!=X1147|X1145!=X1146|conceivedThru(X1147,X1146),inference(resolution,[status(thm)],[c447, c2])).
% 0.77/0.95 cnf(c553,plain,god(skolem0001)|existsIn(skolem0001,X1161)|modification(X1159,X1160)|X1159!=X1163|conceivedThru(X1163,X1162),inference(resolution,[status(thm)],[c482, reflexivity])).
% 0.77/0.95 cnf(c481,plain,god(skolem0001)|existsIn(skolem0001,X1120)|conceivedThru(X1121,X1118)|X1121!=X1122|X1119!=X1123|modification(X1122,X1123),inference(resolution,[status(thm)],[c447, c27])).
% 0.77/0.95 cnf(c548,plain,god(skolem0001)|existsIn(skolem0001,X1140)|conceivedThru(X1142,X1141)|X1142!=X1144|modification(X1144,X1143),inference(resolution,[status(thm)],[c481, reflexivity])).
% 0.77/0.95 cnf(c479,plain,god(skolem0001)|modification(X1110,X1112)|conceivedThru(X1110,X1108)|skolem0001!=X1109|X1111!=X1113|existsIn(X1109,X1113),inference(resolution,[status(thm)],[c447, c1])).
% 0.77/0.95 cnf(c546,plain,god(skolem0001)|modification(X1128,X1126)|conceivedThru(X1128,X1124)|skolem0001!=X1125|existsIn(X1125,X1127),inference(resolution,[status(thm)],[c479, reflexivity])).
% 0.77/0.95 cnf(c113,plain,~mode(X295)|substance(X294)|conceivedThru(X295,X296),inference(split_conjunct,[status(thm)],[c109])).
% 0.77/0.95 cnf(c259,plain,god(skolem0001)|substance(X345)|conceivedThru(skolem0001,X346),inference(resolution,[status(thm)],[c254, c113])).
% 0.77/0.95 cnf(c263,plain,god(skolem0001)|conceivedThru(skolem0001,X355)|inItself(X356),inference(resolution,[status(thm)],[c259, c127])).
% 0.77/0.95 cnf(c279,plain,god(skolem0001)|conceivedThru(skolem0001,X382)|selfCaused(X381),inference(resolution,[status(thm)],[c263, c56])).
% 0.77/0.95 cnf(c303,plain,god(skolem0001)|conceivedThru(skolem0001,X394)|essenceInvExistence(X393),inference(resolution,[status(thm)],[c279, c143])).
% 0.77/0.95 cnf(c262,plain,god(skolem0001)|conceivedThru(skolem0001,X354)|being(X353),inference(resolution,[status(thm)],[c259, c59])).
% 0.77/0.95 cnf(c276,plain,god(skolem0001)|conceivedThru(skolem0001,X380)|hasEssence(X379),inference(resolution,[status(thm)],[c262, c53])).
% 0.77/0.95 cnf(c300,plain,god(skolem0001)|conceivedThru(skolem0001,X426)|~essenceInvExistence(X427)|exists(X427),inference(resolution,[status(thm)],[c276, c50])).
% 0.77/0.95 cnf(c348,plain,god(skolem0001)|conceivedThru(skolem0001,X578)|exists(X580)|conceivedThru(skolem0001,X579),inference(resolution,[status(thm)],[c300, c303])).
% 0.77/0.95 cnf(c382,plain,god(skolem0001)|conceivedThru(skolem0001,X585)|exists(X586),inference(factor,[status(thm)],[c348])).
% 0.77/0.95 cnf(c392,plain,god(skolem0001)|conceivedThru(skolem0001,X587)|existsIn(X588,X588),inference(resolution,[status(thm)],[c382, c246])).
% 0.77/0.95 cnf(c396,plain,god(skolem0001)|conceivedThru(skolem0001,X590)|mode(X589),inference(resolution,[status(thm)],[c392, c245])).
% 0.77/0.95 cnf(c402,plain,god(skolem0001)|conceivedThru(skolem0001,X741)|modification(X739,X738)|existsIn(X739,X740),inference(resolution,[status(thm)],[c396, c110])).
% 0.77/0.95 cnf(c473,plain,god(skolem0001)|conceivedThru(skolem0001,X1092)|modification(X1089,X1090)|X1089!=X1091|X1093!=X1094|existsIn(X1091,X1094),inference(resolution,[status(thm)],[c402, c1])).
% 0.77/0.95 cnf(c543,plain,god(skolem0001)|conceivedThru(skolem0001,X1101)|modification(X1099,X1100)|X1099!=X1102|existsIn(X1102,X1103),inference(resolution,[status(thm)],[c473, reflexivity])).
% 0.77/0.95 cnf(c469,plain,god(skolem0001)|conceivedThru(skolem0001,X1065)|existsIn(X1064,X1066)|X1064!=X1067|X1063!=X1068|modification(X1067,X1068),inference(resolution,[status(thm)],[c402, c27])).
% 0.77/0.95 cnf(c539,plain,god(skolem0001)|conceivedThru(skolem0001,X1082)|existsIn(X1080,X1081)|X1080!=X1083|modification(X1083,X1084),inference(resolution,[status(thm)],[c469, reflexivity])).
% 0.77/0.95 cnf(c466,plain,god(skolem0001)|modification(X1037,X1038)|existsIn(X1037,X1040)|skolem0001!=X1039|X1035!=X1036|conceivedThru(X1039,X1036),inference(resolution,[status(thm)],[c402, c2])).
% 0.77/0.95 cnf(c535,plain,god(skolem0001)|modification(X1062,X1060)|existsIn(X1062,X1058)|skolem0001!=X1059|conceivedThru(X1059,X1061),inference(resolution,[status(thm)],[c466, reflexivity])).
% 0.77/0.95 cnf(c401,plain,god(skolem0001)|conceivedThru(skolem0001,X735)|modification(X734,X732)|conceivedThru(X734,X733),inference(resolution,[status(thm)],[c396, c111])).
% 0.77/0.95 cnf(c464,plain,god(skolem0001)|conceivedThru(skolem0001,X1034)|modification(X1033,X1031)|X1033!=X1032|X1029!=X1030|conceivedThru(X1032,X1030),inference(resolution,[status(thm)],[c401, c2])).
% 0.77/0.95 cnf(c533,plain,god(skolem0001)|conceivedThru(skolem0001,X1048)|modification(X1047,X1045)|X1047!=X1046|conceivedThru(X1046,X1049),inference(resolution,[status(thm)],[c464, reflexivity])).
% 0.77/0.95 cnf(c463,plain,god(skolem0001)|conceivedThru(skolem0001,X1012)|conceivedThru(X1009,X1007)|X1009!=X1010|X1008!=X1011|modification(X1010,X1011),inference(resolution,[status(thm)],[c401, c27])).
% 0.77/0.95 cnf(c529,plain,god(skolem0001)|conceivedThru(skolem0001,X1021)|conceivedThru(X1020,X1023)|X1020!=X1024|modification(X1024,X1022),inference(resolution,[status(thm)],[c463, reflexivity])).
% 0.77/0.95 cnf(c460,plain,god(skolem0001)|modification(X985,X982)|conceivedThru(X985,X983)|skolem0001!=X984|X980!=X981|conceivedThru(X984,X981),inference(resolution,[status(thm)],[c401, c2])).
% 0.77/0.95 cnf(c526,plain,god(skolem0001)|modification(X999,X998)|conceivedThru(X999,X1002)|skolem0001!=X1000|conceivedThru(X1000,X1001),inference(resolution,[status(thm)],[c460, reflexivity])).
% 0.77/0.95 cnf(c442,plain,god(skolem0001)|existsIn(skolem0001,X958)|X955!=X957|X955!=X956|existsIn(X957,X956),inference(resolution,[status(thm)],[c431, c1])).
% 0.77/0.95 cnf(c523,plain,god(skolem0001)|existsIn(skolem0001,X967)|X968!=X969|existsIn(X969,X968),inference(resolution,[status(thm)],[c442, reflexivity])).
% 0.77/0.95 cnf(c438,plain,god(skolem0001)|existsIn(X944,X944)|skolem0001!=X946|X947!=X945|existsIn(X946,X945),inference(resolution,[status(thm)],[c431, c1])).
% 0.77/0.95 cnf(c520,plain,god(skolem0001)|existsIn(X950,X950)|skolem0001!=X952|existsIn(X952,X951),inference(resolution,[status(thm)],[c438, reflexivity])).
% 0.77/0.95 cnf(c446,plain,god(skolem0001)|mode(X910)|skolem0001!=X911|X912!=X909|existsIn(X911,X909),inference(resolution,[status(thm)],[c440, c1])).
% 0.77/0.95 cnf(c517,plain,god(skolem0001)|mode(X915)|skolem0001!=X917|existsIn(X917,X916),inference(resolution,[status(thm)],[c446, reflexivity])).
% 0.77/0.95 cnf(c430,plain,god(skolem0001)|exists(X895)|skolem0001!=X897|X898!=X896|existsIn(X897,X896),inference(resolution,[status(thm)],[c417, c1])).
% 0.77/0.95 cnf(c514,plain,god(skolem0001)|exists(X906)|skolem0001!=X904|existsIn(X904,X905),inference(resolution,[status(thm)],[c430, reflexivity])).
% 0.77/0.95 cnf(c399,plain,god(skolem0001)|mode(X884)|skolem0001!=X887|X885!=X886|conceivedThru(X887,X886),inference(resolution,[status(thm)],[c396, c2])).
% 0.77/0.95 cnf(c511,plain,god(skolem0001)|mode(X892)|skolem0001!=X891|conceivedThru(X891,X890),inference(resolution,[status(thm)],[c399, reflexivity])).
% 0.77/0.95 cnf(c398,plain,god(skolem0001)|conceivedThru(skolem0001,X864)|X867!=X866|X867!=X865|existsIn(X866,X865),inference(resolution,[status(thm)],[c392, c1])).
% 0.77/0.96 cnf(c508,plain,god(skolem0001)|conceivedThru(skolem0001,X873)|X871!=X872|existsIn(X872,X871),inference(resolution,[status(thm)],[c398, reflexivity])).
% 0.77/0.96 cnf(c393,plain,god(skolem0001)|existsIn(X847,X847)|skolem0001!=X848|X845!=X846|conceivedThru(X848,X846),inference(resolution,[status(thm)],[c392, c2])).
% 0.77/0.96 cnf(c505,plain,god(skolem0001)|existsIn(X851,X851)|skolem0001!=X853|conceivedThru(X853,X852),inference(resolution,[status(thm)],[c393, reflexivity])).
% 0.77/0.96 cnf(c258,plain,god(skolem0001)|modification(skolem0001,X406)|existsIn(skolem0001,X407),inference(resolution,[status(thm)],[c254, c110])).
% 0.77/0.96 cnf(c343,plain,god(skolem0001)|modification(skolem0001,X745)|skolem0001!=X747|X748!=X746|existsIn(X747,X746),inference(resolution,[status(thm)],[c258, c1])).
% 0.77/0.96 cnf(c475,plain,god(skolem0001)|modification(skolem0001,X840)|skolem0001!=X842|existsIn(X842,X841),inference(resolution,[status(thm)],[c343, reflexivity])).
% 0.77/0.96 cnf(c390,plain,god(skolem0001)|exists(X830)|skolem0001!=X832|X829!=X831|conceivedThru(X832,X831),inference(resolution,[status(thm)],[c382, c2])).
% 0.77/0.96 cnf(c501,plain,god(skolem0001)|exists(X835)|skolem0001!=X837|conceivedThru(X837,X836),inference(resolution,[status(thm)],[c390, reflexivity])).
% 0.77/0.96 cnf(c339,plain,god(skolem0001)|existsIn(skolem0001,X713)|skolem0001!=X712|X715!=X714|modification(X712,X714),inference(resolution,[status(thm)],[c258, c27])).
% 0.77/0.96 cnf(c456,plain,god(skolem0001)|existsIn(skolem0001,X823)|skolem0001!=X824|modification(X824,X822),inference(resolution,[status(thm)],[c339, reflexivity])).
% 0.77/0.96 cnf(c257,plain,god(skolem0001)|modification(skolem0001,X398)|conceivedThru(skolem0001,X397),inference(resolution,[status(thm)],[c254, c111])).
% 0.77/0.96 cnf(c326,plain,god(skolem0001)|modification(skolem0001,X662)|skolem0001!=X665|X663!=X664|conceivedThru(X665,X664),inference(resolution,[status(thm)],[c257, c2])).
% 0.77/0.96 cnf(c433,plain,god(skolem0001)|modification(skolem0001,X812)|skolem0001!=X811|conceivedThru(X811,X813),inference(resolution,[status(thm)],[c326, reflexivity])).
% 0.77/0.96 cnf(c325,plain,god(skolem0001)|conceivedThru(skolem0001,X648)|skolem0001!=X645|X647!=X646|modification(X645,X646),inference(resolution,[status(thm)],[c257, c27])).
% 0.77/0.96 cnf(c416,plain,god(skolem0001)|conceivedThru(skolem0001,X796)|skolem0001!=X798|modification(X798,X797),inference(resolution,[status(thm)],[c325, reflexivity])).
% 0.77/0.96 cnf(c144,plain,~selfCaused(X88)|natureConcOnlyByExistence(X88),inference(split_conjunct,[status(thm)],[c142])).
% 0.77/0.96 cnf(c317,plain,god(skolem0001)|existsIn(skolem0001,X404)|natureConcOnlyByExistence(X403),inference(resolution,[status(thm)],[c292, c144])).
% 0.77/0.96 cnf(c336,plain,god(skolem0001)|natureConcOnlyByExistence(X694)|skolem0001!=X696|X697!=X695|existsIn(X696,X695),inference(resolution,[status(thm)],[c317, c1])).
% 0.77/0.96 cnf(c454,plain,god(skolem0001)|natureConcOnlyByExistence(X723)|skolem0001!=X725|existsIn(X725,X724),inference(resolution,[status(thm)],[c336, reflexivity])).
% 0.77/0.96 cnf(c331,plain,god(skolem0001)|essenceInvExistence(X680)|skolem0001!=X682|X683!=X681|existsIn(X682,X681),inference(resolution,[status(thm)],[c316, c1])).
% 0.77/0.96 cnf(c452,plain,god(skolem0001)|essenceInvExistence(X716)|skolem0001!=X717|existsIn(X717,X718),inference(resolution,[status(thm)],[c331, reflexivity])).
% 0.77/0.96 cnf(c304,plain,god(skolem0001)|conceivedThru(skolem0001,X396)|natureConcOnlyByExistence(X395),inference(resolution,[status(thm)],[c279, c144])).
% 0.77/0.96 cnf(c321,plain,god(skolem0001)|natureConcOnlyByExistence(X630)|skolem0001!=X632|X629!=X631|conceivedThru(X632,X631),inference(resolution,[status(thm)],[c304, c2])).
% 0.77/0.96 cnf(c412,plain,god(skolem0001)|natureConcOnlyByExistence(X642)|skolem0001!=X644|conceivedThru(X644,X643),inference(resolution,[status(thm)],[c321, reflexivity])).
% 0.77/0.96 cnf(c318,plain,god(skolem0001)|essenceInvExistence(X612)|skolem0001!=X613|X610!=X611|conceivedThru(X613,X611),inference(resolution,[status(thm)],[c303, c2])).
% 0.77/0.96 cnf(c409,plain,god(skolem0001)|essenceInvExistence(X635)|skolem0001!=X637|conceivedThru(X637,X636),inference(resolution,[status(thm)],[c318, reflexivity])).
% 0.77/0.96 cnf(c315,plain,god(skolem0001)|selfCaused(X596)|skolem0001!=X597|X598!=X595|existsIn(X597,X595),inference(resolution,[status(thm)],[c292, c1])).
% 0.77/0.96 cnf(c406,plain,god(skolem0001)|selfCaused(X625)|skolem0001!=X626|existsIn(X626,X624),inference(resolution,[status(thm)],[c315, reflexivity])).
% 0.77/0.96 cnf(c308,plain,god(skolem0001)|hasEssence(X581)|skolem0001!=X583|X584!=X582|existsIn(X583,X582),inference(resolution,[status(thm)],[c287, c1])).
% 0.77/0.96 cnf(c389,plain,god(skolem0001)|hasEssence(X599)|skolem0001!=X601|existsIn(X601,X600),inference(resolution,[status(thm)],[c308, reflexivity])).
% 0.77/0.96 cnf(c301,plain,god(skolem0001)|selfCaused(X565)|skolem0001!=X568|X566!=X567|conceivedThru(X568,X567),inference(resolution,[status(thm)],[c279, c2])).
% 0.77/0.96 cnf(c380,plain,god(skolem0001)|selfCaused(X573)|skolem0001!=X574|conceivedThru(X574,X575),inference(resolution,[status(thm)],[c301, reflexivity])).
% 0.77/0.96 cnf(c298,plain,god(skolem0001)|hasEssence(X551)|skolem0001!=X552|X549!=X550|conceivedThru(X552,X550),inference(resolution,[status(thm)],[c276, c2])).
% 0.77/0.96 cnf(c376,plain,god(skolem0001)|hasEssence(X564)|skolem0001!=X563|conceivedThru(X563,X562),inference(resolution,[status(thm)],[c298, reflexivity])).
% 0.77/0.96 cnf(c128,plain,~substance(X84)|conceivedThruItself(X84),inference(split_conjunct,[status(thm)],[c126])).
% 0.77/0.96 cnf(c269,plain,god(skolem0001)|existsIn(skolem0001,X376)|conceivedThruItself(X375),inference(resolution,[status(thm)],[c260, c128])).
% 0.77/0.96 cnf(c296,plain,god(skolem0001)|conceivedThruItself(X534)|skolem0001!=X535|X536!=X533|existsIn(X535,X533),inference(resolution,[status(thm)],[c269, c1])).
% 0.77/0.96 cnf(c372,plain,god(skolem0001)|conceivedThruItself(X556)|skolem0001!=X557|existsIn(X557,X555),inference(resolution,[status(thm)],[c296, reflexivity])).
% 0.77/0.96 cnf(c291,plain,god(skolem0001)|inItself(X520)|skolem0001!=X519|X521!=X518|existsIn(X519,X518),inference(resolution,[status(thm)],[c268, c1])).
% 0.77/0.96 cnf(c369,plain,god(skolem0001)|inItself(X545)|skolem0001!=X546|existsIn(X546,X544),inference(resolution,[status(thm)],[c291, reflexivity])).
% 0.77/0.96 cnf(c286,plain,god(skolem0001)|being(X504)|skolem0001!=X503|X505!=X502|existsIn(X503,X502),inference(resolution,[status(thm)],[c267, c1])).
% 0.77/0.96 cnf(c365,plain,god(skolem0001)|being(X539)|skolem0001!=X537|existsIn(X537,X538),inference(resolution,[status(thm)],[c286, reflexivity])).
% 0.77/0.96 cnf(c264,plain,god(skolem0001)|conceivedThru(skolem0001,X361)|conceivedThruItself(X362),inference(resolution,[status(thm)],[c259, c128])).
% 0.77/0.96 cnf(c280,plain,god(skolem0001)|conceivedThruItself(X488)|skolem0001!=X489|X486!=X487|conceivedThru(X489,X487),inference(resolution,[status(thm)],[c264, c2])).
% 0.77/0.96 cnf(c361,plain,god(skolem0001)|conceivedThruItself(X526)|skolem0001!=X528|conceivedThru(X528,X527),inference(resolution,[status(thm)],[c280, reflexivity])).
% 0.77/0.96 cnf(c277,plain,god(skolem0001)|inItself(X474)|skolem0001!=X475|X472!=X473|conceivedThru(X475,X473),inference(resolution,[status(thm)],[c263, c2])).
% 0.77/0.96 cnf(c359,plain,god(skolem0001)|inItself(X515)|skolem0001!=X517|conceivedThru(X517,X516),inference(resolution,[status(thm)],[c277, reflexivity])).
% 0.77/0.96 cnf(c274,plain,god(skolem0001)|being(X459)|skolem0001!=X461|X458!=X460|conceivedThru(X461,X460),inference(resolution,[status(thm)],[c262, c2])).
% 0.77/0.96 cnf(c357,plain,god(skolem0001)|being(X510)|skolem0001!=X508|conceivedThru(X508,X509),inference(resolution,[status(thm)],[c274, reflexivity])).
% 0.77/0.96 cnf(c273,plain,god(skolem0001)|substance(X447)|skolem0001!=X446|X444!=X445|existsIn(X446,X445),inference(resolution,[status(thm)],[c260, c1])).
% 0.77/0.96 cnf(c355,plain,god(skolem0001)|substance(X499)|skolem0001!=X497|existsIn(X497,X498),inference(resolution,[status(thm)],[c273, reflexivity])).
% 0.77/0.96 cnf(c265,plain,god(skolem0001)|substance(X422)|skolem0001!=X423|X420!=X421|conceivedThru(X423,X421),inference(resolution,[status(thm)],[c259, c2])).
% 0.77/0.96 cnf(c347,plain,god(skolem0001)|substance(X492)|skolem0001!=X490|conceivedThru(X490,X491),inference(resolution,[status(thm)],[c265, reflexivity])).
% 0.77/0.96 cnf(c256,plain,god(skolem0001)|skolem0001!=X388|skolem0001!=X387|existsIn(X388,X387),inference(resolution,[status(thm)],[c252, c1])).
% 0.77/0.96 cnf(c311,plain,god(skolem0001)|skolem0001!=X417|existsIn(X417,skolem0001),inference(resolution,[status(thm)],[c256, reflexivity])).
% 0.77/0.96 cnf(c310,plain,god(skolem0001)|skolem0001!=X413|existsIn(X413,X413),inference(factor,[status(thm)],[c256])).
% 0.77/0.96 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)).
% 0.77/0.96 fof(c146,plain,(![X]:(canBeConceivedAsNonExisting(X)=>~essenceInvExistence(X))),inference(fof_simplification,[status(thm)],[can_be_conceived_as_non_existing])).
% 0.77/0.96 fof(c147,plain,(![X]:(~canBeConceivedAsNonExisting(X)|~essenceInvExistence(X))),inference(fof_nnf,[status(thm)],[c146])).
% 0.77/0.96 fof(c148,plain,(![X45]:(~canBeConceivedAsNonExisting(X45)|~essenceInvExistence(X45))),inference(variable_rename,[status(thm)],[c147])).
% 0.77/0.96 cnf(c149,plain,~canBeConceivedAsNonExisting(X89)|~essenceInvExistence(X89),inference(split_conjunct,[status(thm)],[c148])).
% 0.77/0.96 cnf(c332,plain,god(skolem0001)|existsIn(skolem0001,X412)|~canBeConceivedAsNonExisting(X411),inference(resolution,[status(thm)],[c316, c149])).
% 0.77/0.96 cnf(c320,plain,god(skolem0001)|conceivedThru(skolem0001,X410)|~canBeConceivedAsNonExisting(X409),inference(resolution,[status(thm)],[c303, c149])).
% 0.77/0.96 cnf(c96,plain,~substance(X347)|~constInInfAttributes(X347)|~expressesEternalEssentiality(X348)|~expressesInfiniteEssentiality(X348)|absolutelyInfinite(X347),inference(split_conjunct,[status(thm)],[c90])).
% 0.77/0.96 cnf(c95,plain,~substance(X343)|~constInInfAttributes(X343)|attributeOf(X344,X343)|absolutelyInfinite(X343),inference(split_conjunct,[status(thm)],[c90])).
% 0.77/0.96 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)).
% 0.77/0.96 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])).
% 0.77/0.96 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])).
% 0.77/0.96 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])).])).
% 0.77/0.96 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])).
% 0.77/0.96 cnf(c76,plain,~externalTo(X341,X340)|~determinedByFixedMethod(X340,X341)|~determinedByDefiniteMethod(X340,X341)|~isMethodExistence(X341)|necessary(X340),inference(split_conjunct,[status(thm)],[c70])).
% 0.77/0.96 cnf(c207,plain,X333!=X335|X333!=X334|conceivedThru(X335,X334),inference(resolution,[status(thm)],[c204, c2])).
% 0.77/0.96 cnf(c249,plain,X338!=X339|conceivedThru(X339,X338),inference(resolution,[status(thm)],[c207, reflexivity])).
% 0.77/0.96 cnf(c102,negated_conjecture,~god(skolem0001)|~being(skolem0001)|~absolutelyInfinite(skolem0001),inference(split_conjunct,[status(thm)],[c101])).
% 0.77/0.96 cnf(c195,plain,~existsIn(X332,X331)|X332=X331|exists(X332),inference(split_conjunct,[status(thm)],[c191])).
% 0.77/0.96 cnf(c75,plain,~externalTo(X330,X329)|~determinedByFixedMethod(X329,X330)|~determinedByDefiniteMethod(X329,X330)|~isMethodAction(X330)|necessary(X329),inference(split_conjunct,[status(thm)],[c70])).
% 0.77/0.96 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)).
% 0.77/0.96 fof(c150,plain,(![X]:(![Y]:(~trueIdea(X)|(correspondWith(X,Y)&(ideateOf(Y,X)|objectOf(Y,X)))))),inference(fof_nnf,[status(thm)],[true_idea])).
% 0.77/0.96 fof(c151,plain,(![X]:(~trueIdea(X)|((![Y]:correspondWith(X,Y))&(![Y]:(ideateOf(Y,X)|objectOf(Y,X)))))),inference(shift_quantors,[status(thm)],[c150])).
% 0.77/0.96 fof(c153,plain,(![X46]:(![X47]:(![X48]:(~trueIdea(X46)|(correspondWith(X46,X47)&(ideateOf(X48,X46)|objectOf(X48,X46))))))),inference(shift_quantors,[status(thm)],[fof(c152,plain,(![X46]:(~trueIdea(X46)|((![X47]:correspondWith(X46,X47))&(![X48]:(ideateOf(X48,X46)|objectOf(X48,X46)))))),inference(variable_rename,[status(thm)],[c151])).])).
% 0.77/0.96 fof(c154,plain,(![X46]:(![X47]:(![X48]:((~trueIdea(X46)|correspondWith(X46,X47))&(~trueIdea(X46)|(ideateOf(X48,X46)|objectOf(X48,X46))))))),inference(distribute,[status(thm)],[c153])).
% 0.77/0.96 cnf(c156,plain,~trueIdea(X322)|ideateOf(X323,X322)|objectOf(X323,X322),inference(split_conjunct,[status(thm)],[c154])).
% 0.77/0.96 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)).
% 0.77/0.96 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])).
% 0.77/0.96 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])).
% 0.77/0.96 fof(c133,plain,(![X38]:(![X39]:(![X40]:(![X41]:(![X42]:((~finiteAfterItsKind(X38)|(canBeLimitedBy(X38,X39)&sameKind(X38,X40)))&((~canBeLimitedBy(X41,X42)|~sameKind(X41,X42))|finiteAfterItsKind(X41)))))))),inference(shift_quantors,[status(thm)],[fof(c132,plain,((![X38]:(~finiteAfterItsKind(X38)|((![X39]:canBeLimitedBy(X38,X39))&(![X40]:sameKind(X38,X40)))))&(![X41]:((![X42]:(~canBeLimitedBy(X41,X42)|~sameKind(X41,X42)))|finiteAfterItsKind(X41)))),inference(variable_rename,[status(thm)],[c131])).])).
% 0.77/0.96 fof(c134,plain,(![X38]:(![X39]:(![X40]:(![X41]:(![X42]:(((~finiteAfterItsKind(X38)|canBeLimitedBy(X38,X39))&(~finiteAfterItsKind(X38)|sameKind(X38,X40)))&((~canBeLimitedBy(X41,X42)|~sameKind(X41,X42))|finiteAfterItsKind(X41)))))))),inference(distribute,[status(thm)],[c133])).
% 0.77/0.96 cnf(c137,plain,~canBeLimitedBy(X321,X320)|~sameKind(X321,X320)|finiteAfterItsKind(X321),inference(split_conjunct,[status(thm)],[c134])).
% 0.77/0.96 cnf(c44,axiom,X319!=X317|X316!=X318|~determinedByFixedMethod(X319,X316)|determinedByFixedMethod(X317,X318),theory(equality)).
% 0.77/0.96 fof(free,axiom,(![X]:(![Y]:(free(X)<=>(existsOnlyByNecessityOfOwnNature(X)&(actionOf(Y,X)=>determinedByItselfAlone(Y,X)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', free)).
% 0.77/0.96 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])).
% 0.77/0.96 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])).
% 0.77/0.96 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])).])).
% 0.77/0.96 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])).
% 0.77/0.96 cnf(c83,plain,~free(X306)|~actionOf(X305,X306)|determinedByItselfAlone(X305,X306),inference(split_conjunct,[status(thm)],[c81])).
% 0.77/0.96 cnf(c43,axiom,X304!=X302|X301!=X303|~externalTo(X304,X301)|externalTo(X302,X303),theory(equality)).
% 0.77/0.96 cnf(c114,plain,~modification(X297,X298)|~substance(X298)|mode(X297),inference(split_conjunct,[status(thm)],[c109])).
% 0.77/0.96 cnf(c94,plain,~absolutelyInfinite(X290)|~attributeOf(X289,X290)|expressesInfiniteEssentiality(X289),inference(split_conjunct,[status(thm)],[c90])).
% 0.77/0.96 cnf(c40,axiom,X288!=X286|X285!=X287|~determinedByDefiniteMethod(X288,X285)|determinedByDefiniteMethod(X286,X287),theory(equality)).
% 0.77/0.96 cnf(c93,plain,~absolutelyInfinite(X284)|~attributeOf(X283,X284)|expressesEternalEssentiality(X283),inference(split_conjunct,[status(thm)],[c90])).
% 0.77/0.96 cnf(c85,plain,~existsOnlyByNecessityOfOwnNature(X281)|~determinedByItselfAlone(X282,X281)|free(X281),inference(split_conjunct,[status(thm)],[c81])).
% 0.77/0.96 cnf(c84,plain,~existsOnlyByNecessityOfOwnNature(X280)|actionOf(X279,X280)|free(X280),inference(split_conjunct,[status(thm)],[c81])).
% 0.77/0.96 cnf(c47,axiom,X277!=X276|~hasEssence(X277)|hasEssence(X276),theory(equality)).
% 0.77/0.96 cnf(c38,axiom,X275!=X273|X272!=X274|~determinedByItselfAlone(X275,X272)|determinedByItselfAlone(X273,X274),theory(equality)).
% 0.77/0.96 cnf(c46,axiom,X270!=X269|~existConcFollowFromDefEternal(X270)|existConcFollowFromDefEternal(X269),theory(equality)).
% 0.77/0.96 cnf(c45,axiom,X267!=X266|~eternity(X267)|eternity(X266),theory(equality)).
% 0.77/0.96 cnf(c37,axiom,X264!=X262|X261!=X263|~actionOf(X264,X261)|actionOf(X262,X263),theory(equality)).
% 0.77/0.96 cnf(c42,axiom,X260!=X259|~isMethodExistence(X260)|isMethodExistence(X259),theory(equality)).
% 0.77/0.96 cnf(c41,axiom,X257!=X256|~isMethodAction(X257)|isMethodAction(X256),theory(equality)).
% 0.77/0.96 cnf(c39,axiom,X254!=X253|~necessary(X254)|necessary(X253),theory(equality)).
% 0.77/0.96 cnf(c32,axiom,X252!=X250|X249!=X251|~attributeOf(X252,X249)|attributeOf(X250,X251),theory(equality)).
% 0.77/0.96 cnf(c36,axiom,X247!=X246|~existsOnlyByNecessityOfOwnNature(X247)|existsOnlyByNecessityOfOwnNature(X246),theory(equality)).
% 0.77/0.96 cnf(c35,axiom,X244!=X243|~free(X244)|free(X243),theory(equality)).
% 0.77/0.96 cnf(c34,axiom,X237!=X236|~expressesInfiniteEssentiality(X237)|expressesInfiniteEssentiality(X236),theory(equality)).
% 0.77/0.96 cnf(c33,axiom,X234!=X233|~expressesEternalEssentiality(X234)|expressesEternalEssentiality(X233),theory(equality)).
% 0.77/0.96 cnf(c31,axiom,X231!=X230|~constInInfAttributes(X231)|constInInfAttributes(X230),theory(equality)).
% 0.77/0.96 cnf(c20,axiom,X229!=X227|X226!=X228|~sameKind(X229,X226)|sameKind(X227,X228),theory(equality)).
% 0.77/0.96 cnf(c30,axiom,X224!=X223|~absolutelyInfinite(X224)|absolutelyInfinite(X223),theory(equality)).
% 0.77/0.96 cnf(c29,axiom,X221!=X220|~being(X221)|being(X220),theory(equality)).
% 0.77/0.96 cnf(c19,axiom,X218!=X216|X215!=X217|~canBeLimitedBy(X218,X215)|canBeLimitedBy(X216,X217),theory(equality)).
% 0.77/0.96 cnf(c28,axiom,X214!=X213|~god(X214)|god(X213),theory(equality)).
% 0.77/0.96 cnf(c26,axiom,X211!=X210|~mode(X211)|mode(X210),theory(equality)).
% 0.77/0.96 cnf(c25,axiom,X208!=X207|~intPercAsConstEssSub(X208)|intPercAsConstEssSub(X207),theory(equality)).
% 0.77/0.96 cnf(c13,axiom,X206!=X204|X203!=X205|~objectOf(X206,X203)|objectOf(X204,X205),theory(equality)).
% 0.77/0.96 cnf(c24,axiom,X201!=X200|~attribute(X201)|attribute(X200),theory(equality)).
% 0.77/0.96 cnf(c23,axiom,X198!=X197|~conceivedThruItself(X198)|conceivedThruItself(X197),theory(equality)).
% 0.77/0.96 cnf(c12,axiom,X195!=X193|X192!=X194|~ideateOf(X195,X192)|ideateOf(X193,X194),theory(equality)).
% 0.77/0.96 cnf(c22,axiom,X191!=X190|~inItself(X191)|inItself(X190),theory(equality)).
% 0.77/0.96 cnf(c21,axiom,X188!=X187|~substance(X188)|substance(X187),theory(equality)).
% 0.77/0.96 cnf(c18,axiom,X185!=X184|~finiteAfterItsKind(X185)|finiteAfterItsKind(X184),theory(equality)).
% 0.77/0.96 cnf(c11,axiom,X183!=X181|X180!=X182|~correspondWith(X183,X180)|correspondWith(X181,X182),theory(equality)).
% 0.77/0.96 cnf(c17,axiom,X178!=X177|~natureConcOnlyByExistence(X178)|natureConcOnlyByExistence(X177),theory(equality)).
% 0.77/0.96 cnf(c16,axiom,X175!=X174|~selfCaused(X175)|selfCaused(X174),theory(equality)).
% 0.77/0.96 cnf(c9,axiom,X172!=X170|X169!=X171|~canBeUnderstoodInTermsOf(X172,X169)|canBeUnderstoodInTermsOf(X170,X171),theory(equality)).
% 0.77/0.96 cnf(c15,axiom,X168!=X167|~essenceInvExistence(X168)|essenceInvExistence(X167),theory(equality)).
% 0.77/0.96 cnf(c14,axiom,X165!=X164|~canBeConceivedAsNonExisting(X165)|canBeConceivedAsNonExisting(X164),theory(equality)).
% 0.77/0.96 cnf(c10,axiom,X162!=X161|~trueIdea(X162)|trueIdea(X161),theory(equality)).
% 0.77/0.96 cnf(c8,axiom,X160!=X158|X157!=X159|~conceptionInvolves(X160,X157)|conceptionInvolves(X158,X159),theory(equality)).
% 0.77/0.96 cnf(c145,plain,~essenceInvExistence(X156)|~natureConcOnlyByExistence(X156)|selfCaused(X156),inference(split_conjunct,[status(thm)],[c142])).
% 0.77/0.96 cnf(c129,plain,~inItself(X155)|~conceivedThruItself(X155)|substance(X155),inference(split_conjunct,[status(thm)],[c126])).
% 0.77/0.96 cnf(c74,plain,~necessary(X153)|isMethodAction(X154)|isMethodExistence(X154),inference(split_conjunct,[status(thm)],[c70])).
% 0.77/0.96 cnf(c215,plain,god(skolem0001)|~canBeConceivedAsNonExisting(skolem0001),inference(resolution,[status(thm)],[c213, c149])).
% 0.77/0.96 cnf(c7,axiom,X151!=X149|X148!=X150|~haveNothingInCommon(X151,X148)|haveNothingInCommon(X149,X150),theory(equality)).
% 0.77/0.96 cnf(c214,plain,god(skolem0001)|natureConcOnlyByExistence(skolem0001),inference(resolution,[status(thm)],[c211, c144])).
% 0.77/0.96 cnf(c210,plain,god(skolem0001)|conceivedThruItself(skolem0001),inference(resolution,[status(thm)],[c201, c128])).
% 0.77/0.96 cnf(c6,axiom,X146!=X145|~knowledgeOfACause(X146)|knowledgeOfACause(X145),theory(equality)).
% 0.77/0.96 cnf(c92,plain,~absolutelyInfinite(X77)|constInInfAttributes(X77),inference(split_conjunct,[status(thm)],[c90])).
% 0.77/0.96 cnf(c202,plain,god(skolem0001)|constInInfAttributes(skolem0001),inference(resolution,[status(thm)],[c104, c92])).
% 0.77/0.96 cnf(c5,axiom,X144!=X142|X141!=X143|~knowledgeOfEffect(X144,X141)|knowledgeOfEffect(X142,X143),theory(equality)).
% 0.77/0.96 cnf(c4,axiom,X132!=X130|X129!=X131|~effectNecessarilyFollowsFrom(X132,X129)|effectNecessarilyFollowsFrom(X130,X131),theory(equality)).
% 0.77/0.96 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)).
% 0.77/0.96 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])).
% 0.77/0.96 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])).
% 0.77/0.96 fof(c159,plain,(![X49]:(![X50]:(~haveNothingInCommon(X49,X50)|(((~canBeUnderstoodInTermsOf(X49,X50)&~canBeUnderstoodInTermsOf(X50,X49))&~conceptionInvolves(X49,X50))&~conceptionInvolves(X50,X49))))),inference(variable_rename,[status(thm)],[c158])).
% 0.77/0.96 fof(c160,plain,(![X49]:(![X50]:((((~haveNothingInCommon(X49,X50)|~canBeUnderstoodInTermsOf(X49,X50))&(~haveNothingInCommon(X49,X50)|~canBeUnderstoodInTermsOf(X50,X49)))&(~haveNothingInCommon(X49,X50)|~conceptionInvolves(X49,X50)))&(~haveNothingInCommon(X49,X50)|~conceptionInvolves(X50,X49))))),inference(distribute,[status(thm)],[c159])).
% 0.77/0.96 cnf(c164,plain,~haveNothingInCommon(X127,X128)|~conceptionInvolves(X128,X127),inference(split_conjunct,[status(thm)],[c160])).
% 0.77/0.96 cnf(c163,plain,~haveNothingInCommon(X125,X126)|~conceptionInvolves(X125,X126),inference(split_conjunct,[status(thm)],[c160])).
% 0.77/0.96 cnf(c162,plain,~haveNothingInCommon(X123,X124)|~canBeUnderstoodInTermsOf(X124,X123),inference(split_conjunct,[status(thm)],[c160])).
% 0.77/0.96 cnf(c161,plain,~haveNothingInCommon(X121,X122)|~canBeUnderstoodInTermsOf(X121,X122),inference(split_conjunct,[status(thm)],[c160])).
% 0.77/0.96 cnf(c3,axiom,X119!=X118|~definiteCause(X119)|definiteCause(X118),theory(equality)).
% 0.77/0.96 cnf(c194,plain,~existsIn(X117,X117)|exists(X117),inference(split_conjunct,[status(thm)],[c191])).
% 0.77/0.96 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)).
% 0.77/0.96 fof(c171,plain,(![X]:(![Y]:(definiteCause(X)=>(effectNecessarilyFollowsFrom(Y,X)&(~definiteCause(X)=>~effectNecessarilyFollowsFrom(Y,X)))))),inference(fof_simplification,[status(thm)],[definite_cause])).
% 0.77/0.96 fof(c172,plain,(![X]:(![Y]:(~definiteCause(X)|(effectNecessarilyFollowsFrom(Y,X)&(definiteCause(X)|~effectNecessarilyFollowsFrom(Y,X)))))),inference(fof_nnf,[status(thm)],[c171])).
% 0.77/0.96 fof(c173,plain,(![X]:(~definiteCause(X)|((![Y]:effectNecessarilyFollowsFrom(Y,X))&(definiteCause(X)|(![Y]:~effectNecessarilyFollowsFrom(Y,X)))))),inference(shift_quantors,[status(thm)],[c172])).
% 0.77/0.96 fof(c175,plain,(![X55]:(![X56]:(![X57]:(~definiteCause(X55)|(effectNecessarilyFollowsFrom(X56,X55)&(definiteCause(X55)|~effectNecessarilyFollowsFrom(X57,X55))))))),inference(shift_quantors,[status(thm)],[fof(c174,plain,(![X55]:(~definiteCause(X55)|((![X56]:effectNecessarilyFollowsFrom(X56,X55))&(definiteCause(X55)|(![X57]:~effectNecessarilyFollowsFrom(X57,X55)))))),inference(variable_rename,[status(thm)],[c173])).])).
% 0.77/0.96 fof(c176,plain,(![X55]:(![X56]:(![X57]:((~definiteCause(X55)|effectNecessarilyFollowsFrom(X56,X55))&(~definiteCause(X55)|(definiteCause(X55)|~effectNecessarilyFollowsFrom(X57,X55))))))),inference(distribute,[status(thm)],[c175])).
% 0.77/0.96 cnf(c177,plain,~definiteCause(X116)|effectNecessarilyFollowsFrom(X115,X116),inference(split_conjunct,[status(thm)],[c176])).
% 0.77/0.96 fof(knowledge_of_effect,axiom,(![X]:(![Y]:(knowledgeOfEffect(X,Y)<=>knowledgeOfACause(X)))),file('/export/starexec/sandbox/benchmark/Axioms/PHI002+1.ax', knowledge_of_effect)).
% 0.77/0.96 fof(c165,plain,(![X]:(![Y]:((~knowledgeOfEffect(X,Y)|knowledgeOfACause(X))&(~knowledgeOfACause(X)|knowledgeOfEffect(X,Y))))),inference(fof_nnf,[status(thm)],[knowledge_of_effect])).
% 0.77/0.96 fof(c166,plain,((![X]:((![Y]:~knowledgeOfEffect(X,Y))|knowledgeOfACause(X)))&(![X]:(~knowledgeOfACause(X)|(![Y]:knowledgeOfEffect(X,Y))))),inference(shift_quantors,[status(thm)],[c165])).
% 0.77/0.96 fof(c168,plain,(![X51]:(![X52]:(![X53]:(![X54]:((~knowledgeOfEffect(X51,X52)|knowledgeOfACause(X51))&(~knowledgeOfACause(X53)|knowledgeOfEffect(X53,X54))))))),inference(shift_quantors,[status(thm)],[fof(c167,plain,((![X51]:((![X52]:~knowledgeOfEffect(X51,X52))|knowledgeOfACause(X51)))&(![X53]:(~knowledgeOfACause(X53)|(![X54]:knowledgeOfEffect(X53,X54))))),inference(variable_rename,[status(thm)],[c166])).])).
% 0.77/0.96 cnf(c170,plain,~knowledgeOfACause(X114)|knowledgeOfEffect(X114,X113),inference(split_conjunct,[status(thm)],[c168])).
% 0.77/0.96 cnf(c169,plain,~knowledgeOfEffect(X107,X108)|knowledgeOfACause(X107),inference(split_conjunct,[status(thm)],[c168])).
% 0.77/0.96 cnf(c155,plain,~trueIdea(X105)|correspondWith(X105,X106),inference(split_conjunct,[status(thm)],[c154])).
% 0.77/0.96 cnf(c136,plain,~finiteAfterItsKind(X103)|sameKind(X103,X104),inference(split_conjunct,[status(thm)],[c134])).
% 0.77/0.96 cnf(c135,plain,~finiteAfterItsKind(X101)|canBeLimitedBy(X101,X102),inference(split_conjunct,[status(thm)],[c134])).
% 0.77/0.96 cnf(c73,plain,~necessary(X99)|determinedByDefiniteMethod(X99,X100),inference(split_conjunct,[status(thm)],[c70])).
% 0.77/0.96 cnf(c72,plain,~necessary(X93)|determinedByFixedMethod(X93,X94),inference(split_conjunct,[status(thm)],[c70])).
% 0.77/0.96 cnf(c71,plain,~necessary(X91)|externalTo(X92,X91),inference(split_conjunct,[status(thm)],[c70])).
% 0.77/0.96 cnf(c0,axiom,X87!=X86|~exists(X87)|exists(X86),theory(equality)).
% 0.77/0.96 fof(attribute,axiom,(![X]:(attribute(X)<=>intPercAsConstEssSub(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', attribute)).
% 0.77/0.96 fof(c116,plain,(![X]:((~attribute(X)|intPercAsConstEssSub(X))&(~intPercAsConstEssSub(X)|attribute(X)))),inference(fof_nnf,[status(thm)],[attribute])).
% 0.77/0.96 fof(c117,plain,((![X]:(~attribute(X)|intPercAsConstEssSub(X)))&(![X]:(~intPercAsConstEssSub(X)|attribute(X)))),inference(shift_quantors,[status(thm)],[c116])).
% 0.77/0.96 fof(c119,plain,(![X34]:(![X35]:((~attribute(X34)|intPercAsConstEssSub(X34))&(~intPercAsConstEssSub(X35)|attribute(X35))))),inference(shift_quantors,[status(thm)],[fof(c118,plain,((![X34]:(~attribute(X34)|intPercAsConstEssSub(X34)))&(![X35]:(~intPercAsConstEssSub(X35)|attribute(X35)))),inference(variable_rename,[status(thm)],[c117])).])).
% 0.77/0.96 cnf(c121,plain,~intPercAsConstEssSub(X82)|attribute(X82),inference(split_conjunct,[status(thm)],[c119])).
% 0.77/0.96 cnf(c120,plain,~attribute(X81)|intPercAsConstEssSub(X81),inference(split_conjunct,[status(thm)],[c119])).
% 0.77/0.96 cnf(transitivity,axiom,X79!=X78|X78!=X80|X79=X80,theory(equality)).
% 0.77/0.96 cnf(c82,plain,~free(X75)|existsOnlyByNecessityOfOwnNature(X75),inference(split_conjunct,[status(thm)],[c81])).
% 0.77/0.96 fof(eternity,axiom,(![X]:(eternity(X)<=>existConcFollowFromDefEternal(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', eternity)).
% 0.77/0.96 fof(c60,plain,(![X]:((~eternity(X)|existConcFollowFromDefEternal(X))&(~existConcFollowFromDefEternal(X)|eternity(X)))),inference(fof_nnf,[status(thm)],[eternity])).
% 0.77/0.96 fof(c61,plain,((![X]:(~eternity(X)|existConcFollowFromDefEternal(X)))&(![X]:(~existConcFollowFromDefEternal(X)|eternity(X)))),inference(shift_quantors,[status(thm)],[c60])).
% 0.77/0.96 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])).])).
% 0.77/0.96 cnf(c65,plain,~existConcFollowFromDefEternal(X74)|eternity(X74),inference(split_conjunct,[status(thm)],[c63])).
% 0.77/0.96 cnf(symmetry,axiom,X72!=X71|X71=X72,theory(equality)).
% 0.77/0.96 cnf(c64,plain,~eternity(X70)|existConcFollowFromDefEternal(X70),inference(split_conjunct,[status(thm)],[c63])).
% 0.77/0.96 % SZS output end Saturation
% 0.77/0.96
% 0.77/0.96 % Initial clauses : 110
% 0.77/0.96 % Processed clauses : 249
% 0.77/0.96 % Factors computed : 49
% 0.77/0.96 % Resolvents computed: 320
% 0.77/0.96 % Tautologies deleted: 33
% 0.77/0.96 % Forward subsumed : 197
% 0.77/0.96 % Backward subsumed : 52
% 0.77/0.96 % -------- CPU Time ---------
% 0.77/0.96 % User time : 0.573 s
% 0.77/0.96 % System time : 0.025 s
% 0.77/0.96 % Total time : 0.598 s
%------------------------------------------------------------------------------