%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PHI039+1 : TPTP v8.1.2. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n014.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.86s 1.06s
% Output : Saturation 0.91s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : PHI039+1 : TPTP v8.1.2. Released v7.4.0.
% 0.13/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n014.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 :
% 0.86/1.06 % Version: 1.5
% 0.86/1.06 % SZS status CounterSatisfiable
% 0.86/1.06 % SZS output start Saturation
% 0.86/1.06 cnf(reflexivity,axiom,X64=X64,theory(equality)).
% 0.86/1.06 cnf(c1,axiom,X94!=X95|X96!=X93|~existsIn(X94,X96)|existsIn(X95,X93),theory(equality)).
% 0.86/1.06 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.86/1.06 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.86/1.06 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.86/1.06 fof(c108,plain,(![X24]:(![X25]:(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:((~mode(X24)|((modification(X24,X25)&substance(X26))|(existsIn(X24,X27)&conceivedThru(X24,X28))))&(((~modification(X29,X30)|~substance(X30))&(~existsIn(X29,X31)|~conceivedThru(X29,X31)))|mode(X29))))))))))),inference(shift_quantors,[status(thm)],[fof(c107,plain,((![X24]:(~mode(X24)|(((![X25]:modification(X24,X25))&(![X26]:substance(X26)))|((![X27]:existsIn(X24,X27))&(![X28]:conceivedThru(X24,X28))))))&(![X29]:(((![X30]:(~modification(X29,X30)|~substance(X30)))&(![X31]:(~existsIn(X29,X31)|~conceivedThru(X29,X31))))|mode(X29)))),inference(variable_rename,[status(thm)],[c106])).])).
% 0.86/1.06 fof(c109,plain,(![X24]:(![X25]:(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:((((~mode(X24)|(modification(X24,X25)|existsIn(X24,X27)))&(~mode(X24)|(modification(X24,X25)|conceivedThru(X24,X28))))&((~mode(X24)|(substance(X26)|existsIn(X24,X27)))&(~mode(X24)|(substance(X26)|conceivedThru(X24,X28)))))&(((~modification(X29,X30)|~substance(X30))|mode(X29))&((~existsIn(X29,X31)|~conceivedThru(X29,X31))|mode(X29)))))))))))),inference(distribute,[status(thm)],[c108])).
% 0.86/1.06 cnf(c110,plain,~mode(X300)|modification(X300,X299)|existsIn(X300,X298),inference(split_conjunct,[status(thm)],[c109])).
% 0.86/1.06 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.86/1.06 fof(c179,plain,(![X]:(![Y]:(~conceivedThru(X,X)=>(conceivedThru(X,Y)&X!=Y)))),inference(fof_simplification,[status(thm)],[conceived_through])).
% 0.86/1.06 fof(c180,plain,(![X]:(![Y]:(conceivedThru(X,X)|(conceivedThru(X,Y)&X!=Y)))),inference(fof_nnf,[status(thm)],[c179])).
% 0.86/1.06 fof(c181,plain,(![X]:(conceivedThru(X,X)|((![Y]:conceivedThru(X,Y))&(![Y]:X!=Y)))),inference(shift_quantors,[status(thm)],[c180])).
% 0.86/1.06 fof(c183,plain,(![X56]:(![X57]:(![X58]:(conceivedThru(X56,X56)|(conceivedThru(X56,X57)&X56!=X58))))),inference(shift_quantors,[status(thm)],[fof(c182,plain,(![X56]:(conceivedThru(X56,X56)|((![X57]:conceivedThru(X56,X57))&(![X58]:X56!=X58)))),inference(variable_rename,[status(thm)],[c181])).])).
% 0.86/1.06 fof(c184,plain,(![X56]:(![X57]:(![X58]:((conceivedThru(X56,X56)|conceivedThru(X56,X57))&(conceivedThru(X56,X56)|X56!=X58))))),inference(distribute,[status(thm)],[c183])).
% 0.86/1.06 cnf(c185,plain,conceivedThru(X132,X132)|conceivedThru(X132,X131),inference(split_conjunct,[status(thm)],[c184])).
% 0.86/1.06 cnf(c204,plain,conceivedThru(X133,X133),inference(factor,[status(thm)],[c185])).
% 0.86/1.06 cnf(c115,plain,~existsIn(X309,X308)|~conceivedThru(X309,X308)|mode(X309),inference(split_conjunct,[status(thm)],[c109])).
% 0.86/1.06 cnf(c252,plain,~existsIn(X310,X310)|mode(X310),inference(resolution,[status(thm)],[c115, c204])).
% 0.86/1.06 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.86/1.06 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.86/1.06 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.86/1.06 fof(c190,plain,(![X59]:(![X60]:(![X61]:(![X62]:(![X63]:((~exists(X59)|(existsIn(X59,X59)|(existsIn(X59,X60)&X59!=X61)))&((~existsIn(X62,X62)&(~existsIn(X62,X63)|X62=X63))|exists(X62)))))))),inference(shift_quantors,[status(thm)],[fof(c189,plain,((![X59]:(~exists(X59)|(existsIn(X59,X59)|((![X60]:existsIn(X59,X60))&(![X61]:X59!=X61)))))&(![X62]:((~existsIn(X62,X62)&(![X63]:(~existsIn(X62,X63)|X62=X63)))|exists(X62)))),inference(variable_rename,[status(thm)],[c188])).])).
% 0.86/1.06 fof(c191,plain,(![X59]:(![X60]:(![X61]:(![X62]:(![X63]:(((~exists(X59)|(existsIn(X59,X59)|existsIn(X59,X60)))&(~exists(X59)|(existsIn(X59,X59)|X59!=X61)))&((~existsIn(X62,X62)|exists(X62))&((~existsIn(X62,X63)|X62=X63)|exists(X62))))))))),inference(distribute,[status(thm)],[c190])).
% 0.86/1.06 cnf(c193,plain,~exists(X321)|existsIn(X321,X321)|X321!=X322,inference(split_conjunct,[status(thm)],[c191])).
% 0.86/1.06 cnf(c253,plain,~exists(X323)|existsIn(X323,X323),inference(resolution,[status(thm)],[c193, reflexivity])).
% 0.86/1.06 fof(self_caused,axiom,(![X]:(selfCaused(X)<=>(essenceInvExistence(X)&natureConcOnlyByExistence(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', self_caused)).
% 0.86/1.06 fof(c138,plain,(![X]:((~selfCaused(X)|(essenceInvExistence(X)&natureConcOnlyByExistence(X)))&((~essenceInvExistence(X)|~natureConcOnlyByExistence(X))|selfCaused(X)))),inference(fof_nnf,[status(thm)],[self_caused])).
% 0.86/1.06 fof(c139,plain,((![X]:(~selfCaused(X)|(essenceInvExistence(X)&natureConcOnlyByExistence(X))))&(![X]:((~essenceInvExistence(X)|~natureConcOnlyByExistence(X))|selfCaused(X)))),inference(shift_quantors,[status(thm)],[c138])).
% 0.86/1.06 fof(c141,plain,(![X41]:(![X42]:((~selfCaused(X41)|(essenceInvExistence(X41)&natureConcOnlyByExistence(X41)))&((~essenceInvExistence(X42)|~natureConcOnlyByExistence(X42))|selfCaused(X42))))),inference(shift_quantors,[status(thm)],[fof(c140,plain,((![X41]:(~selfCaused(X41)|(essenceInvExistence(X41)&natureConcOnlyByExistence(X41))))&(![X42]:((~essenceInvExistence(X42)|~natureConcOnlyByExistence(X42))|selfCaused(X42)))),inference(variable_rename,[status(thm)],[c139])).])).
% 0.86/1.06 fof(c142,plain,(![X41]:(![X42]:(((~selfCaused(X41)|essenceInvExistence(X41))&(~selfCaused(X41)|natureConcOnlyByExistence(X41)))&((~essenceInvExistence(X42)|~natureConcOnlyByExistence(X42))|selfCaused(X42))))),inference(distribute,[status(thm)],[c141])).
% 0.86/1.06 cnf(c143,plain,~selfCaused(X83)|essenceInvExistence(X83),inference(split_conjunct,[status(thm)],[c142])).
% 0.86/1.06 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.86/1.06 fof(c54,plain,(![X]:(~inItself(X)|selfCaused(X))),inference(fof_nnf,[status(thm)],[is_in_itself_is_self_caused])).
% 0.86/1.06 fof(c55,plain,(![X4]:(~inItself(X4)|selfCaused(X4))),inference(variable_rename,[status(thm)],[c54])).
% 0.86/1.06 cnf(c56,plain,~inItself(X66)|selfCaused(X66),inference(split_conjunct,[status(thm)],[c55])).
% 0.86/1.06 fof(substance,axiom,(![X]:(substance(X)<=>(inItself(X)&conceivedThruItself(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', substance)).
% 0.86/1.06 fof(c122,plain,(![X]:((~substance(X)|(inItself(X)&conceivedThruItself(X)))&((~inItself(X)|~conceivedThruItself(X))|substance(X)))),inference(fof_nnf,[status(thm)],[substance])).
% 0.86/1.06 fof(c123,plain,((![X]:(~substance(X)|(inItself(X)&conceivedThruItself(X))))&(![X]:((~inItself(X)|~conceivedThruItself(X))|substance(X)))),inference(shift_quantors,[status(thm)],[c122])).
% 0.86/1.06 fof(c125,plain,(![X34]:(![X35]:((~substance(X34)|(inItself(X34)&conceivedThruItself(X34)))&((~inItself(X35)|~conceivedThruItself(X35))|substance(X35))))),inference(shift_quantors,[status(thm)],[fof(c124,plain,((![X34]:(~substance(X34)|(inItself(X34)&conceivedThruItself(X34))))&(![X35]:((~inItself(X35)|~conceivedThruItself(X35))|substance(X35)))),inference(variable_rename,[status(thm)],[c123])).])).
% 0.86/1.06 fof(c126,plain,(![X34]:(![X35]:(((~substance(X34)|inItself(X34))&(~substance(X34)|conceivedThruItself(X34)))&((~inItself(X35)|~conceivedThruItself(X35))|substance(X35))))),inference(distribute,[status(thm)],[c125])).
% 0.91/1.06 cnf(c127,plain,~substance(X81)|inItself(X81),inference(split_conjunct,[status(thm)],[c126])).
% 0.91/1.06 cnf(c113,plain,~mode(X287)|substance(X286)|conceivedThru(X287,X285),inference(split_conjunct,[status(thm)],[c109])).
% 0.91/1.06 fof(absolutely_infinite,conjecture,(![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.91/1.06 fof(c86,negated_conjecture,(~(![X]:(![Y]:(absolutelyInfinite(X)<=>((substance(X)&constInInfAttributes(X))&(attributeOf(Y,X)=>(expressesEternalEssentiality(Y)&expressesInfiniteEssentiality(Y)))))))),inference(assume_negation,[status(cth)],[absolutely_infinite])).
% 0.91/1.06 fof(c87,negated_conjecture,(?[X]:(?[Y]:((~absolutelyInfinite(X)|((~substance(X)|~constInInfAttributes(X))|(attributeOf(Y,X)&(~expressesEternalEssentiality(Y)|~expressesInfiniteEssentiality(Y)))))&(absolutelyInfinite(X)|((substance(X)&constInInfAttributes(X))&(~attributeOf(Y,X)|(expressesEternalEssentiality(Y)&expressesInfiniteEssentiality(Y)))))))),inference(fof_nnf,[status(thm)],[c86])).
% 0.91/1.06 fof(c88,negated_conjecture,(?[X20]:(?[X21]:((~absolutelyInfinite(X20)|((~substance(X20)|~constInInfAttributes(X20))|(attributeOf(X21,X20)&(~expressesEternalEssentiality(X21)|~expressesInfiniteEssentiality(X21)))))&(absolutelyInfinite(X20)|((substance(X20)&constInInfAttributes(X20))&(~attributeOf(X21,X20)|(expressesEternalEssentiality(X21)&expressesInfiniteEssentiality(X21)))))))),inference(variable_rename,[status(thm)],[c87])).
% 0.91/1.06 fof(c89,negated_conjecture,((~absolutelyInfinite(skolem0001)|((~substance(skolem0001)|~constInInfAttributes(skolem0001))|(attributeOf(skolem0002,skolem0001)&(~expressesEternalEssentiality(skolem0002)|~expressesInfiniteEssentiality(skolem0002)))))&(absolutelyInfinite(skolem0001)|((substance(skolem0001)&constInInfAttributes(skolem0001))&(~attributeOf(skolem0002,skolem0001)|(expressesEternalEssentiality(skolem0002)&expressesInfiniteEssentiality(skolem0002)))))),inference(skolemize,[status(esa)],[c88])).
% 0.91/1.06 fof(c90,negated_conjecture,(((~absolutelyInfinite(skolem0001)|((~substance(skolem0001)|~constInInfAttributes(skolem0001))|attributeOf(skolem0002,skolem0001)))&(~absolutelyInfinite(skolem0001)|((~substance(skolem0001)|~constInInfAttributes(skolem0001))|(~expressesEternalEssentiality(skolem0002)|~expressesInfiniteEssentiality(skolem0002)))))&(((absolutelyInfinite(skolem0001)|substance(skolem0001))&(absolutelyInfinite(skolem0001)|constInInfAttributes(skolem0001)))&((absolutelyInfinite(skolem0001)|(~attributeOf(skolem0002,skolem0001)|expressesEternalEssentiality(skolem0002)))&(absolutelyInfinite(skolem0001)|(~attributeOf(skolem0002,skolem0001)|expressesInfiniteEssentiality(skolem0002)))))),inference(distribute,[status(thm)],[c89])).
% 0.91/1.06 cnf(c93,negated_conjecture,absolutelyInfinite(skolem0001)|substance(skolem0001),inference(split_conjunct,[status(thm)],[c90])).
% 0.91/1.06 cnf(c200,plain,absolutelyInfinite(skolem0001)|inItself(skolem0001),inference(resolution,[status(thm)],[c93, c127])).
% 0.91/1.06 cnf(c208,plain,absolutelyInfinite(skolem0001)|selfCaused(skolem0001),inference(resolution,[status(thm)],[c200, c56])).
% 0.91/1.06 cnf(c211,plain,absolutelyInfinite(skolem0001)|essenceInvExistence(skolem0001),inference(resolution,[status(thm)],[c208, c143])).
% 0.91/1.06 fof(being_has_essense,axiom,(![X]:(being(X)=>hasEssence(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', being_has_essense)).
% 0.91/1.06 fof(c51,plain,(![X]:(~being(X)|hasEssence(X))),inference(fof_nnf,[status(thm)],[being_has_essense])).
% 0.91/1.06 fof(c52,plain,(![X3]:(~being(X3)|hasEssence(X3))),inference(variable_rename,[status(thm)],[c51])).
% 0.91/1.06 cnf(c53,plain,~being(X65)|hasEssence(X65),inference(split_conjunct,[status(thm)],[c52])).
% 0.91/1.06 fof(has_substance_being,axiom,(![X]:(substance(X)=>being(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', has_substance_being)).
% 0.91/1.06 fof(c57,plain,(![X]:(~substance(X)|being(X))),inference(fof_nnf,[status(thm)],[has_substance_being])).
% 0.91/1.06 fof(c58,plain,(![X5]:(~substance(X5)|being(X5))),inference(variable_rename,[status(thm)],[c57])).
% 0.91/1.06 cnf(c59,plain,~substance(X67)|being(X67),inference(split_conjunct,[status(thm)],[c58])).
% 0.91/1.06 cnf(c202,plain,absolutelyInfinite(skolem0001)|being(skolem0001),inference(resolution,[status(thm)],[c93, c59])).
% 0.91/1.06 cnf(c209,plain,absolutelyInfinite(skolem0001)|hasEssence(skolem0001),inference(resolution,[status(thm)],[c202, c53])).
% 0.91/1.06 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.91/1.06 fof(c48,plain,(![X]:((~essenceInvExistence(X)|~hasEssence(X))|exists(X))),inference(fof_nnf,[status(thm)],[essence_involves_existence_exists])).
% 0.91/1.06 fof(c49,plain,(![X2]:((~essenceInvExistence(X2)|~hasEssence(X2))|exists(X2))),inference(variable_rename,[status(thm)],[c48])).
% 0.91/1.06 cnf(c50,plain,~essenceInvExistence(X146)|~hasEssence(X146)|exists(X146),inference(split_conjunct,[status(thm)],[c49])).
% 0.91/1.06 cnf(c214,plain,~essenceInvExistence(skolem0001)|exists(skolem0001)|absolutelyInfinite(skolem0001),inference(resolution,[status(thm)],[c50, c209])).
% 0.91/1.06 cnf(c257,plain,exists(skolem0001)|absolutelyInfinite(skolem0001),inference(resolution,[status(thm)],[c214, c211])).
% 0.91/1.06 cnf(c258,plain,absolutelyInfinite(skolem0001)|existsIn(skolem0001,skolem0001),inference(resolution,[status(thm)],[c257, c253])).
% 0.91/1.06 cnf(c261,plain,absolutelyInfinite(skolem0001)|mode(skolem0001),inference(resolution,[status(thm)],[c258, c252])).
% 0.91/1.06 cnf(c269,plain,absolutelyInfinite(skolem0001)|substance(X342)|conceivedThru(skolem0001,X343),inference(resolution,[status(thm)],[c261, c113])).
% 0.91/1.06 cnf(c289,plain,absolutelyInfinite(skolem0001)|conceivedThru(skolem0001,X365)|inItself(X364),inference(resolution,[status(thm)],[c269, c127])).
% 0.91/1.06 cnf(c326,plain,absolutelyInfinite(skolem0001)|conceivedThru(skolem0001,X380)|selfCaused(X381),inference(resolution,[status(thm)],[c289, c56])).
% 0.91/1.06 cnf(c364,plain,absolutelyInfinite(skolem0001)|conceivedThru(skolem0001,X399)|essenceInvExistence(X398),inference(resolution,[status(thm)],[c326, c143])).
% 0.91/1.06 cnf(c291,plain,absolutelyInfinite(skolem0001)|conceivedThru(skolem0001,X369)|being(X368),inference(resolution,[status(thm)],[c269, c59])).
% 0.91/1.06 cnf(c335,plain,absolutelyInfinite(skolem0001)|conceivedThru(skolem0001,X383)|hasEssence(X382),inference(resolution,[status(thm)],[c291, c53])).
% 0.91/1.06 cnf(c368,plain,absolutelyInfinite(skolem0001)|conceivedThru(skolem0001,X418)|~essenceInvExistence(X417)|exists(X417),inference(resolution,[status(thm)],[c335, c50])).
% 0.91/1.06 cnf(c409,plain,absolutelyInfinite(skolem0001)|conceivedThru(skolem0001,X747)|exists(X746)|conceivedThru(skolem0001,X745),inference(resolution,[status(thm)],[c368, c364])).
% 0.91/1.06 cnf(c551,plain,absolutelyInfinite(skolem0001)|conceivedThru(skolem0001,X748)|exists(X749),inference(factor,[status(thm)],[c409])).
% 0.91/1.06 cnf(c561,plain,absolutelyInfinite(skolem0001)|conceivedThru(skolem0001,X754)|existsIn(X755,X755),inference(resolution,[status(thm)],[c551, c253])).
% 0.91/1.06 cnf(c567,plain,absolutelyInfinite(skolem0001)|conceivedThru(skolem0001,X756)|mode(X757),inference(resolution,[status(thm)],[c561, c252])).
% 0.91/1.06 cnf(c575,plain,absolutelyInfinite(skolem0001)|conceivedThru(skolem0001,X861)|modification(X859,X860)|existsIn(X859,X862),inference(resolution,[status(thm)],[c567, c110])).
% 0.91/1.06 cnf(c637,plain,absolutelyInfinite(skolem0001)|conceivedThru(skolem0001,X1527)|modification(X1525,X1528)|X1525!=X1524|X1523!=X1526|existsIn(X1524,X1526),inference(resolution,[status(thm)],[c575, c1])).
% 0.91/1.06 cnf(c724,plain,absolutelyInfinite(skolem0001)|conceivedThru(skolem0001,X1538)|modification(X1539,X1540)|X1539!=X1541|existsIn(X1541,X1542),inference(resolution,[status(thm)],[c637, reflexivity])).
% 0.91/1.06 cnf(c27,axiom,X239!=X240|X241!=X238|~modification(X239,X241)|modification(X240,X238),theory(equality)).
% 0.91/1.06 cnf(c634,plain,absolutelyInfinite(skolem0001)|conceivedThru(skolem0001,X1504)|existsIn(X1502,X1505)|X1502!=X1503|X1506!=X1501|modification(X1503,X1501),inference(resolution,[status(thm)],[c575, c27])).
% 0.91/1.06 cnf(c720,plain,absolutelyInfinite(skolem0001)|conceivedThru(skolem0001,X1515)|existsIn(X1516,X1518)|X1516!=X1514|modification(X1514,X1517),inference(resolution,[status(thm)],[c634, reflexivity])).
% 0.91/1.07 cnf(c2,axiom,X108!=X109|X110!=X107|~conceivedThru(X108,X110)|conceivedThru(X109,X107),theory(equality)).
% 0.91/1.07 cnf(c631,plain,absolutelyInfinite(skolem0001)|modification(X1477,X1478)|existsIn(X1477,X1476)|skolem0001!=X1474|X1475!=X1473|conceivedThru(X1474,X1473),inference(resolution,[status(thm)],[c575, c2])).
% 0.91/1.07 cnf(c716,plain,absolutelyInfinite(skolem0001)|modification(X1493,X1492)|existsIn(X1493,X1495)|skolem0001!=X1494|conceivedThru(X1494,X1496),inference(resolution,[status(thm)],[c631, reflexivity])).
% 0.91/1.07 cnf(c111,plain,~mode(X303)|modification(X303,X302)|conceivedThru(X303,X301),inference(split_conjunct,[status(thm)],[c109])).
% 0.91/1.07 cnf(c574,plain,absolutelyInfinite(skolem0001)|conceivedThru(skolem0001,X855)|modification(X853,X856)|conceivedThru(X853,X854),inference(resolution,[status(thm)],[c567, c111])).
% 0.91/1.07 cnf(c628,plain,absolutelyInfinite(skolem0001)|conceivedThru(skolem0001,X1451)|modification(X1449,X1452)|X1449!=X1448|X1450!=X1447|conceivedThru(X1448,X1447),inference(resolution,[status(thm)],[c574, c2])).
% 0.91/1.07 cnf(c712,plain,absolutelyInfinite(skolem0001)|conceivedThru(skolem0001,X1479)|modification(X1480,X1481)|X1480!=X1483|conceivedThru(X1483,X1482),inference(resolution,[status(thm)],[c628, reflexivity])).
% 0.91/1.07 cnf(c627,plain,absolutelyInfinite(skolem0001)|conceivedThru(skolem0001,X1444)|conceivedThru(X1443,X1441)|X1443!=X1445|X1446!=X1442|modification(X1445,X1442),inference(resolution,[status(thm)],[c574, c27])).
% 0.91/1.07 cnf(c710,plain,absolutelyInfinite(skolem0001)|conceivedThru(skolem0001,X1463)|conceivedThru(X1464,X1460)|X1464!=X1461|modification(X1461,X1462),inference(resolution,[status(thm)],[c627, reflexivity])).
% 0.91/1.07 cnf(c624,plain,absolutelyInfinite(skolem0001)|modification(X1423,X1422)|conceivedThru(X1423,X1418)|skolem0001!=X1420|X1421!=X1419|conceivedThru(X1420,X1419),inference(resolution,[status(thm)],[c574, c2])).
% 0.91/1.07 cnf(c707,plain,absolutelyInfinite(skolem0001)|modification(X1436,X1433)|conceivedThru(X1436,X1432)|skolem0001!=X1434|conceivedThru(X1434,X1435),inference(resolution,[status(thm)],[c624, reflexivity])).
% 0.91/1.07 cnf(c112,plain,~mode(X284)|substance(X283)|existsIn(X284,X282),inference(split_conjunct,[status(thm)],[c109])).
% 0.91/1.07 cnf(c268,plain,absolutelyInfinite(skolem0001)|substance(X339)|existsIn(skolem0001,X338),inference(resolution,[status(thm)],[c261, c112])).
% 0.91/1.07 cnf(c281,plain,absolutelyInfinite(skolem0001)|existsIn(skolem0001,X349)|inItself(X348),inference(resolution,[status(thm)],[c268, c127])).
% 0.91/1.07 cnf(c299,plain,absolutelyInfinite(skolem0001)|existsIn(skolem0001,X370)|selfCaused(X371),inference(resolution,[status(thm)],[c281, c56])).
% 0.91/1.07 cnf(c351,plain,absolutelyInfinite(skolem0001)|existsIn(skolem0001,X391)|essenceInvExistence(X390),inference(resolution,[status(thm)],[c299, c143])).
% 0.91/1.07 cnf(c283,plain,absolutelyInfinite(skolem0001)|existsIn(skolem0001,X361)|being(X360),inference(resolution,[status(thm)],[c268, c59])).
% 0.91/1.07 cnf(c312,plain,absolutelyInfinite(skolem0001)|existsIn(skolem0001,X375)|hasEssence(X374),inference(resolution,[status(thm)],[c283, c53])).
% 0.91/1.07 cnf(c357,plain,absolutelyInfinite(skolem0001)|existsIn(skolem0001,X415)|~essenceInvExistence(X414)|exists(X414),inference(resolution,[status(thm)],[c312, c50])).
% 0.91/1.07 cnf(c407,plain,absolutelyInfinite(skolem0001)|existsIn(skolem0001,X637)|exists(X638)|existsIn(skolem0001,X636),inference(resolution,[status(thm)],[c357, c351])).
% 0.91/1.07 cnf(c489,plain,absolutelyInfinite(skolem0001)|existsIn(skolem0001,X640)|exists(X639),inference(factor,[status(thm)],[c407])).
% 0.91/1.07 cnf(c505,plain,absolutelyInfinite(skolem0001)|existsIn(skolem0001,X644)|existsIn(X645,X645),inference(resolution,[status(thm)],[c489, c253])).
% 0.91/1.07 cnf(c512,plain,absolutelyInfinite(skolem0001)|existsIn(skolem0001,X652)|mode(X653),inference(resolution,[status(thm)],[c505, c252])).
% 0.91/1.07 cnf(c524,plain,absolutelyInfinite(skolem0001)|existsIn(skolem0001,X828)|modification(X825,X827)|existsIn(X825,X826),inference(resolution,[status(thm)],[c512, c110])).
% 0.91/1.07 cnf(c615,plain,absolutelyInfinite(skolem0001)|existsIn(skolem0001,X1393)|modification(X1395,X1392)|X1395!=X1394|X1391!=X1396|existsIn(X1394,X1396),inference(resolution,[status(thm)],[c524, c1])).
% 0.91/1.07 cnf(c703,plain,absolutelyInfinite(skolem0001)|existsIn(skolem0001,X1417)|modification(X1415,X1414)|X1415!=X1413|existsIn(X1413,X1416),inference(resolution,[status(thm)],[c615, reflexivity])).
% 0.91/1.07 cnf(c612,plain,absolutelyInfinite(skolem0001)|existsIn(skolem0001,X1383)|existsIn(X1382,X1385)|X1382!=X1384|X1386!=X1381|modification(X1384,X1381),inference(resolution,[status(thm)],[c524, c27])).
% 0.91/1.07 cnf(c700,plain,absolutelyInfinite(skolem0001)|existsIn(skolem0001,X1400)|existsIn(X1401,X1404)|X1401!=X1402|modification(X1402,X1403),inference(resolution,[status(thm)],[c612, reflexivity])).
% 0.91/1.07 cnf(c609,plain,absolutelyInfinite(skolem0001)|modification(X1365,X1363)|existsIn(X1365,X1367)|skolem0001!=X1364|X1362!=X1366|existsIn(X1364,X1366),inference(resolution,[status(thm)],[c524, c1])).
% 0.91/1.07 cnf(c697,plain,absolutelyInfinite(skolem0001)|modification(X1372,X1374)|existsIn(X1372,X1375)|skolem0001!=X1373|existsIn(X1373,X1376),inference(resolution,[status(thm)],[c609, reflexivity])).
% 0.91/1.07 cnf(c523,plain,absolutelyInfinite(skolem0001)|existsIn(skolem0001,X818)|modification(X815,X816)|conceivedThru(X815,X817),inference(resolution,[status(thm)],[c512, c111])).
% 0.91/1.07 cnf(c603,plain,absolutelyInfinite(skolem0001)|existsIn(skolem0001,X1338)|modification(X1336,X1339)|X1336!=X1335|X1337!=X1334|conceivedThru(X1335,X1334),inference(resolution,[status(thm)],[c523, c2])).
% 0.91/1.07 cnf(c693,plain,absolutelyInfinite(skolem0001)|existsIn(skolem0001,X1353)|modification(X1355,X1354)|X1355!=X1357|conceivedThru(X1357,X1356),inference(resolution,[status(thm)],[c603, reflexivity])).
% 0.91/1.07 cnf(c602,plain,absolutelyInfinite(skolem0001)|existsIn(skolem0001,X1310)|conceivedThru(X1309,X1312)|X1309!=X1311|X1313!=X1308|modification(X1311,X1308),inference(resolution,[status(thm)],[c523, c27])).
% 0.91/1.07 cnf(c689,plain,absolutelyInfinite(skolem0001)|existsIn(skolem0001,X1340)|conceivedThru(X1344,X1342)|X1344!=X1341|modification(X1341,X1343),inference(resolution,[status(thm)],[c602, reflexivity])).
% 0.91/1.07 cnf(c599,plain,absolutelyInfinite(skolem0001)|modification(X1303,X1305)|conceivedThru(X1303,X1307)|skolem0001!=X1304|X1302!=X1306|existsIn(X1304,X1306),inference(resolution,[status(thm)],[c523, c1])).
% 0.91/1.07 cnf(c687,plain,absolutelyInfinite(skolem0001)|modification(X1318,X1322)|conceivedThru(X1318,X1320)|skolem0001!=X1319|existsIn(X1319,X1321),inference(resolution,[status(thm)],[c599, reflexivity])).
% 0.91/1.07 fof(god,axiom,(![X]:(god(X)<=>(being(X)&absolutelyInfinite(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', god)).
% 0.91/1.07 fof(c97,plain,(![X]:((~god(X)|(being(X)&absolutelyInfinite(X)))&((~being(X)|~absolutelyInfinite(X))|god(X)))),inference(fof_nnf,[status(thm)],[god])).
% 0.91/1.07 fof(c98,plain,((![X]:(~god(X)|(being(X)&absolutelyInfinite(X))))&(![X]:((~being(X)|~absolutelyInfinite(X))|god(X)))),inference(shift_quantors,[status(thm)],[c97])).
% 0.91/1.07 fof(c100,plain,(![X22]:(![X23]:((~god(X22)|(being(X22)&absolutelyInfinite(X22)))&((~being(X23)|~absolutelyInfinite(X23))|god(X23))))),inference(shift_quantors,[status(thm)],[fof(c99,plain,((![X22]:(~god(X22)|(being(X22)&absolutelyInfinite(X22))))&(![X23]:((~being(X23)|~absolutelyInfinite(X23))|god(X23)))),inference(variable_rename,[status(thm)],[c98])).])).
% 0.91/1.07 fof(c101,plain,(![X22]:(![X23]:(((~god(X22)|being(X22))&(~god(X22)|absolutelyInfinite(X22)))&((~being(X23)|~absolutelyInfinite(X23))|god(X23))))),inference(distribute,[status(thm)],[c100])).
% 0.91/1.07 cnf(c104,plain,~being(X153)|~absolutelyInfinite(X153)|god(X153),inference(split_conjunct,[status(thm)],[c101])).
% 0.91/1.07 cnf(c630,plain,conceivedThru(skolem0001,X1258)|modification(X1256,X1257)|existsIn(X1256,X1255)|~being(skolem0001)|god(skolem0001),inference(resolution,[status(thm)],[c575, c104])).
% 0.91/1.07 cnf(c623,plain,conceivedThru(skolem0001,X1249)|modification(X1248,X1250)|conceivedThru(X1248,X1247)|~being(skolem0001)|god(skolem0001),inference(resolution,[status(thm)],[c574, c104])).
% 0.91/1.07 cnf(c606,plain,existsIn(skolem0001,X1237)|modification(X1234,X1235)|existsIn(X1234,X1236)|~being(skolem0001)|god(skolem0001),inference(resolution,[status(thm)],[c524, c104])).
% 0.91/1.07 cnf(c596,plain,existsIn(skolem0001,X1227)|modification(X1229,X1226)|conceivedThru(X1229,X1228)|~being(skolem0001)|god(skolem0001),inference(resolution,[status(thm)],[c523, c104])).
% 0.91/1.07 cnf(c569,plain,absolutelyInfinite(skolem0001)|conceivedThru(skolem0001,X1196)|X1198!=X1197|X1198!=X1199|existsIn(X1197,X1199),inference(resolution,[status(thm)],[c561, c1])).
% 0.91/1.07 cnf(c672,plain,absolutelyInfinite(skolem0001)|conceivedThru(skolem0001,X1206)|X1208!=X1207|existsIn(X1207,X1208),inference(resolution,[status(thm)],[c569, reflexivity])).
% 0.91/1.07 cnf(c565,plain,absolutelyInfinite(skolem0001)|existsIn(X1187,X1187)|skolem0001!=X1188|X1186!=X1185|conceivedThru(X1188,X1185),inference(resolution,[status(thm)],[c561, c2])).
% 0.91/1.07 cnf(c669,plain,absolutelyInfinite(skolem0001)|existsIn(X1193,X1193)|skolem0001!=X1191|conceivedThru(X1191,X1192),inference(resolution,[status(thm)],[c565, reflexivity])).
% 0.91/1.07 cnf(c514,plain,absolutelyInfinite(skolem0001)|existsIn(skolem0001,X1139)|X1137!=X1138|X1137!=X1140|existsIn(X1138,X1140),inference(resolution,[status(thm)],[c505, c1])).
% 0.91/1.07 cnf(c666,plain,absolutelyInfinite(skolem0001)|existsIn(skolem0001,X1150)|X1149!=X1151|existsIn(X1151,X1149),inference(resolution,[status(thm)],[c514, reflexivity])).
% 0.91/1.07 cnf(c510,plain,absolutelyInfinite(skolem0001)|existsIn(X1128,X1128)|skolem0001!=X1127|X1126!=X1129|existsIn(X1127,X1129),inference(resolution,[status(thm)],[c505, c1])).
% 0.91/1.07 cnf(c663,plain,absolutelyInfinite(skolem0001)|existsIn(X1134,X1134)|skolem0001!=X1132|existsIn(X1132,X1133),inference(resolution,[status(thm)],[c510, reflexivity])).
% 0.91/1.07 cnf(c572,plain,absolutelyInfinite(skolem0001)|mode(X1002)|skolem0001!=X1004|X1003!=X1001|conceivedThru(X1004,X1001),inference(resolution,[status(thm)],[c567, c2])).
% 0.91/1.07 cnf(c660,plain,absolutelyInfinite(skolem0001)|mode(X1007)|skolem0001!=X1008|conceivedThru(X1008,X1009),inference(resolution,[status(thm)],[c572, reflexivity])).
% 0.91/1.07 cnf(c559,plain,absolutelyInfinite(skolem0001)|exists(X987)|skolem0001!=X990|X989!=X988|conceivedThru(X990,X988),inference(resolution,[status(thm)],[c551, c2])).
% 0.91/1.07 cnf(c657,plain,absolutelyInfinite(skolem0001)|exists(X997)|skolem0001!=X996|conceivedThru(X996,X998),inference(resolution,[status(thm)],[c559, reflexivity])).
% 0.91/1.07 cnf(c521,plain,absolutelyInfinite(skolem0001)|mode(X973)|skolem0001!=X975|X974!=X976|existsIn(X975,X976),inference(resolution,[status(thm)],[c512, c1])).
% 0.91/1.07 cnf(c654,plain,absolutelyInfinite(skolem0001)|mode(X983)|skolem0001!=X982|existsIn(X982,X984),inference(resolution,[status(thm)],[c521, reflexivity])).
% 0.91/1.07 cnf(c503,plain,absolutelyInfinite(skolem0001)|exists(X964)|skolem0001!=X963|X962!=X965|existsIn(X963,X965),inference(resolution,[status(thm)],[c489, c1])).
% 0.91/1.07 cnf(c651,plain,absolutelyInfinite(skolem0001)|exists(X969)|skolem0001!=X968|existsIn(X968,X970),inference(resolution,[status(thm)],[c503, reflexivity])).
% 0.91/1.07 cnf(c267,plain,absolutelyInfinite(skolem0001)|modification(skolem0001,X396)|existsIn(skolem0001,X397),inference(resolution,[status(thm)],[c261, c110])).
% 0.91/1.07 cnf(c395,plain,absolutelyInfinite(skolem0001)|modification(skolem0001,X866)|skolem0001!=X864|X863!=X865|existsIn(X864,X865),inference(resolution,[status(thm)],[c267, c1])).
% 0.91/1.07 cnf(c640,plain,absolutelyInfinite(skolem0001)|modification(skolem0001,X937)|skolem0001!=X935|existsIn(X935,X936),inference(resolution,[status(thm)],[c395, reflexivity])).
% 0.91/1.07 cnf(c392,plain,absolutelyInfinite(skolem0001)|existsIn(skolem0001,X830)|skolem0001!=X831|X832!=X829|modification(X831,X829),inference(resolution,[status(thm)],[c267, c27])).
% 0.91/1.07 cnf(c618,plain,absolutelyInfinite(skolem0001)|existsIn(skolem0001,X928)|skolem0001!=X929|modification(X929,X930),inference(resolution,[status(thm)],[c392, reflexivity])).
% 0.91/1.07 cnf(c266,plain,absolutelyInfinite(skolem0001)|modification(skolem0001,X388)|conceivedThru(skolem0001,X387),inference(resolution,[status(thm)],[c261, c111])).
% 0.91/1.07 cnf(c378,plain,absolutelyInfinite(skolem0001)|modification(skolem0001,X753)|skolem0001!=X752|X751!=X750|conceivedThru(X752,X750),inference(resolution,[status(thm)],[c266, c2])).
% 0.91/1.07 cnf(c563,plain,absolutelyInfinite(skolem0001)|modification(skolem0001,X915)|skolem0001!=X917|conceivedThru(X917,X916),inference(resolution,[status(thm)],[c378, reflexivity])).
% 0.91/1.07 cnf(c377,plain,absolutelyInfinite(skolem0001)|conceivedThru(skolem0001,X734)|skolem0001!=X736|X737!=X735|modification(X736,X735),inference(resolution,[status(thm)],[c266, c27])).
% 0.91/1.07 cnf(c549,plain,absolutelyInfinite(skolem0001)|conceivedThru(skolem0001,X902)|skolem0001!=X903|modification(X903,X904),inference(resolution,[status(thm)],[c377, reflexivity])).
% 0.91/1.07 cnf(c398,plain,absolutelyInfinite(skolem0001)|essenceInvExistence(X881)|skolem0001!=X883|X882!=X880|conceivedThru(X883,X880),inference(resolution,[status(thm)],[c364, c2])).
% 0.91/1.07 cnf(c642,plain,absolutelyInfinite(skolem0001)|essenceInvExistence(X886)|skolem0001!=X888|conceivedThru(X888,X887),inference(resolution,[status(thm)],[c398, reflexivity])).
% 0.91/1.07 cnf(c564,plain,conceivedThru(skolem0001,X849)|existsIn(X850,X850)|~being(skolem0001)|god(skolem0001),inference(resolution,[status(thm)],[c561, c104])).
% 0.91/1.07 cnf(c390,plain,modification(skolem0001,X812)|existsIn(skolem0001,X811)|~being(skolem0001)|god(skolem0001),inference(resolution,[status(thm)],[c267, c104])).
% 0.91/1.07 cnf(c507,plain,existsIn(skolem0001,X810)|existsIn(X809,X809)|~being(skolem0001)|god(skolem0001),inference(resolution,[status(thm)],[c505, c104])).
% 0.91/1.07 cnf(c144,plain,~selfCaused(X86)|natureConcOnlyByExistence(X86),inference(split_conjunct,[status(thm)],[c142])).
% 0.91/1.07 cnf(c363,plain,absolutelyInfinite(skolem0001)|conceivedThru(skolem0001,X395)|natureConcOnlyByExistence(X394),inference(resolution,[status(thm)],[c326, c144])).
% 0.91/1.07 cnf(c387,plain,absolutelyInfinite(skolem0001)|natureConcOnlyByExistence(X796)|skolem0001!=X798|X797!=X795|conceivedThru(X798,X795),inference(resolution,[status(thm)],[c363, c2])).
% 0.91/1.07 cnf(c588,plain,absolutelyInfinite(skolem0001)|natureConcOnlyByExistence(X802)|skolem0001!=X801|conceivedThru(X801,X803),inference(resolution,[status(thm)],[c387, reflexivity])).
% 0.91/1.07 cnf(c383,plain,absolutelyInfinite(skolem0001)|essenceInvExistence(X783)|skolem0001!=X781|X780!=X782|existsIn(X781,X782),inference(resolution,[status(thm)],[c351, c1])).
% 0.91/1.07 cnf(c585,plain,absolutelyInfinite(skolem0001)|essenceInvExistence(X790)|skolem0001!=X792|existsIn(X792,X791),inference(resolution,[status(thm)],[c383, reflexivity])).
% 0.91/1.07 cnf(c571,plain,conceivedThru(skolem0001,X769)|mode(X768)|~being(skolem0001)|god(skolem0001),inference(resolution,[status(thm)],[c567, c104])).
% 0.91/1.07 cnf(c558,plain,conceivedThru(skolem0001,X761)|exists(X760)|~being(skolem0001)|god(skolem0001),inference(resolution,[status(thm)],[c551, c104])).
% 0.91/1.07 cnf(c350,plain,absolutelyInfinite(skolem0001)|existsIn(skolem0001,X385)|natureConcOnlyByExistence(X384),inference(resolution,[status(thm)],[c299, c144])).
% 0.91/1.07 cnf(c372,plain,absolutelyInfinite(skolem0001)|natureConcOnlyByExistence(X708)|skolem0001!=X707|X706!=X705|existsIn(X707,X705),inference(resolution,[status(thm)],[c350, c1])).
% 0.91/1.07 cnf(c541,plain,absolutelyInfinite(skolem0001)|natureConcOnlyByExistence(X742)|skolem0001!=X740|existsIn(X740,X741),inference(resolution,[status(thm)],[c372, reflexivity])).
% 0.91/1.07 cnf(c366,plain,absolutelyInfinite(skolem0001)|hasEssence(X690)|skolem0001!=X689|X688!=X687|conceivedThru(X689,X687),inference(resolution,[status(thm)],[c335, c2])).
% 0.91/1.07 cnf(c536,plain,absolutelyInfinite(skolem0001)|hasEssence(X728)|skolem0001!=X727|conceivedThru(X727,X729),inference(resolution,[status(thm)],[c366, reflexivity])).
% 0.91/1.07 cnf(c375,plain,modification(skolem0001,X722)|conceivedThru(skolem0001,X721)|~being(skolem0001)|god(skolem0001),inference(resolution,[status(thm)],[c266, c104])).
% 0.91/1.07 cnf(c361,plain,absolutelyInfinite(skolem0001)|selfCaused(X674)|skolem0001!=X675|X673!=X672|conceivedThru(X675,X672),inference(resolution,[status(thm)],[c326, c2])).
% 0.91/1.07 cnf(c533,plain,absolutelyInfinite(skolem0001)|selfCaused(X720)|skolem0001!=X718|conceivedThru(X718,X719),inference(resolution,[status(thm)],[c361, reflexivity])).
% 0.91/1.07 cnf(c355,plain,absolutelyInfinite(skolem0001)|hasEssence(X661)|skolem0001!=X659|X658!=X660|existsIn(X659,X660),inference(resolution,[status(thm)],[c312, c1])).
% 0.91/1.07 cnf(c528,plain,absolutelyInfinite(skolem0001)|hasEssence(X710)|skolem0001!=X709|existsIn(X709,X711),inference(resolution,[status(thm)],[c355, reflexivity])).
% 0.91/1.07 cnf(c518,plain,existsIn(skolem0001,X692)|mode(X691)|~being(skolem0001)|god(skolem0001),inference(resolution,[status(thm)],[c512, c104])).
% 0.91/1.07 cnf(c348,plain,absolutelyInfinite(skolem0001)|selfCaused(X649)|skolem0001!=X648|X647!=X650|existsIn(X648,X650),inference(resolution,[status(thm)],[c299, c1])).
% 0.91/1.07 cnf(c517,plain,absolutelyInfinite(skolem0001)|selfCaused(X684)|skolem0001!=X683|existsIn(X683,X682),inference(resolution,[status(thm)],[c348, reflexivity])).
% 0.91/1.07 cnf(c500,plain,existsIn(skolem0001,X670)|exists(X671)|~being(skolem0001)|god(skolem0001),inference(resolution,[status(thm)],[c489, c104])).
% 0.91/1.07 cnf(c332,plain,absolutelyInfinite(skolem0001)|being(X625)|skolem0001!=X628|X627!=X626|conceivedThru(X628,X626),inference(resolution,[status(thm)],[c291, c2])).
% 0.91/1.07 cnf(c487,plain,absolutelyInfinite(skolem0001)|being(X631)|skolem0001!=X632|conceivedThru(X632,X633),inference(resolution,[status(thm)],[c332, reflexivity])).
% 0.91/1.07 cnf(c128,plain,~substance(X82)|conceivedThruItself(X82),inference(split_conjunct,[status(thm)],[c126])).
% 0.91/1.07 cnf(c290,plain,absolutelyInfinite(skolem0001)|conceivedThru(skolem0001,X366)|conceivedThruItself(X367),inference(resolution,[status(thm)],[c269, c128])).
% 0.91/1.07 cnf(c328,plain,absolutelyInfinite(skolem0001)|conceivedThruItself(X611)|skolem0001!=X613|X612!=X610|conceivedThru(X613,X610),inference(resolution,[status(thm)],[c290, c2])).
% 0.91/1.07 cnf(c484,plain,absolutelyInfinite(skolem0001)|conceivedThruItself(X620)|skolem0001!=X622|conceivedThru(X622,X621),inference(resolution,[status(thm)],[c328, reflexivity])).
% 0.91/1.07 cnf(c324,plain,absolutelyInfinite(skolem0001)|inItself(X595)|skolem0001!=X598|X597!=X596|conceivedThru(X598,X596),inference(resolution,[status(thm)],[c289, c2])).
% 0.91/1.07 cnf(c473,plain,absolutelyInfinite(skolem0001)|inItself(X603)|skolem0001!=X602|conceivedThru(X602,X601),inference(resolution,[status(thm)],[c324, reflexivity])).
% 0.91/1.07 cnf(c309,plain,absolutelyInfinite(skolem0001)|being(X488)|skolem0001!=X487|X486!=X489|existsIn(X487,X489),inference(resolution,[status(thm)],[c283, c1])).
% 0.91/1.07 cnf(c454,plain,absolutelyInfinite(skolem0001)|being(X573)|skolem0001!=X571|existsIn(X571,X572),inference(resolution,[status(thm)],[c309, reflexivity])).
% 0.91/1.07 cnf(c282,plain,absolutelyInfinite(skolem0001)|existsIn(skolem0001,X356)|conceivedThruItself(X357),inference(resolution,[status(thm)],[c268, c128])).
% 0.91/1.07 cnf(c303,plain,absolutelyInfinite(skolem0001)|conceivedThruItself(X472)|skolem0001!=X474|X473!=X475|existsIn(X474,X475),inference(resolution,[status(thm)],[c282, c1])).
% 0.91/1.07 cnf(c446,plain,absolutelyInfinite(skolem0001)|conceivedThruItself(X559)|skolem0001!=X561|existsIn(X561,X560),inference(resolution,[status(thm)],[c303, reflexivity])).
% 0.91/1.07 cnf(c297,plain,absolutelyInfinite(skolem0001)|inItself(X460)|skolem0001!=X459|X458!=X461|existsIn(X459,X461),inference(resolution,[status(thm)],[c281, c1])).
% 0.91/1.07 cnf(c435,plain,absolutelyInfinite(skolem0001)|inItself(X546)|skolem0001!=X544|existsIn(X544,X545),inference(resolution,[status(thm)],[c297, reflexivity])).
% 0.91/1.07 cnf(c292,plain,absolutelyInfinite(skolem0001)|substance(X444)|skolem0001!=X447|X446!=X445|conceivedThru(X447,X445),inference(resolution,[status(thm)],[c269, c2])).
% 0.91/1.07 cnf(c427,plain,absolutelyInfinite(skolem0001)|substance(X534)|skolem0001!=X532|conceivedThru(X532,X533),inference(resolution,[status(thm)],[c292, reflexivity])).
% 0.91/1.07 cnf(c286,plain,absolutelyInfinite(skolem0001)|substance(X430)|skolem0001!=X431|X432!=X433|existsIn(X431,X433),inference(resolution,[status(thm)],[c268, c1])).
% 0.91/1.07 cnf(c416,plain,absolutelyInfinite(skolem0001)|substance(X520)|skolem0001!=X518|existsIn(X518,X519),inference(resolution,[status(thm)],[c286, reflexivity])).
% 0.91/1.07 cnf(c397,plain,conceivedThru(skolem0001,X507)|essenceInvExistence(X508)|~being(skolem0001)|god(skolem0001),inference(resolution,[status(thm)],[c364, c104])).
% 0.91/1.07 cnf(c386,plain,conceivedThru(skolem0001,X502)|natureConcOnlyByExistence(X501)|~being(skolem0001)|god(skolem0001),inference(resolution,[status(thm)],[c363, c104])).
% 0.91/1.07 cnf(c380,plain,existsIn(skolem0001,X496)|essenceInvExistence(X497)|~being(skolem0001)|god(skolem0001),inference(resolution,[status(thm)],[c351, c104])).
% 0.91/1.07 cnf(c369,plain,existsIn(skolem0001,X490)|natureConcOnlyByExistence(X491)|~being(skolem0001)|god(skolem0001),inference(resolution,[status(thm)],[c350, c104])).
% 0.91/1.07 cnf(c365,plain,conceivedThru(skolem0001,X482)|hasEssence(X483)|~being(skolem0001)|god(skolem0001),inference(resolution,[status(thm)],[c335, c104])).
% 0.91/1.07 cnf(c360,plain,conceivedThru(skolem0001,X479)|selfCaused(X478)|~being(skolem0001)|god(skolem0001),inference(resolution,[status(thm)],[c326, c104])).
% 0.91/1.07 cnf(c352,plain,existsIn(skolem0001,X470)|hasEssence(X471)|~being(skolem0001)|god(skolem0001),inference(resolution,[status(thm)],[c312, c104])).
% 0.91/1.07 cnf(c345,plain,existsIn(skolem0001,X467)|selfCaused(X466)|~being(skolem0001)|god(skolem0001),inference(resolution,[status(thm)],[c299, c104])).
% 0.91/1.07 cnf(c331,plain,conceivedThru(skolem0001,X463)|being(X462)|~being(skolem0001)|god(skolem0001),inference(resolution,[status(thm)],[c291, c104])).
% 0.91/1.07 cnf(c327,plain,conceivedThru(skolem0001,X455)|conceivedThruItself(X454)|~being(skolem0001)|god(skolem0001),inference(resolution,[status(thm)],[c290, c104])).
% 0.91/1.07 cnf(c323,plain,conceivedThru(skolem0001,X451)|inItself(X450)|~being(skolem0001)|god(skolem0001),inference(resolution,[status(thm)],[c289, c104])).
% 0.91/1.07 cnf(c306,plain,existsIn(skolem0001,X443)|being(X442)|~being(skolem0001)|god(skolem0001),inference(resolution,[status(thm)],[c283, c104])).
% 0.91/1.07 cnf(c300,plain,existsIn(skolem0001,X439)|conceivedThruItself(X438)|~being(skolem0001)|god(skolem0001),inference(resolution,[status(thm)],[c282, c104])).
% 0.91/1.07 cnf(c294,plain,existsIn(skolem0001,X435)|inItself(X434)|~being(skolem0001)|god(skolem0001),inference(resolution,[status(thm)],[c281, c104])).
% 0.91/1.07 cnf(c288,plain,substance(X426)|conceivedThru(skolem0001,X427)|~being(skolem0001)|god(skolem0001),inference(resolution,[status(thm)],[c269, c104])).
% 0.91/1.07 cnf(c280,plain,substance(X408)|existsIn(skolem0001,X409)|~being(skolem0001)|god(skolem0001),inference(resolution,[status(thm)],[c268, c104])).
% 0.91/1.07 cnf(c263,plain,absolutelyInfinite(skolem0001)|skolem0001!=X377|skolem0001!=X378|existsIn(X377,X378),inference(resolution,[status(thm)],[c258, c1])).
% 0.91/1.07 cnf(c359,plain,absolutelyInfinite(skolem0001)|skolem0001!=X407|existsIn(X407,skolem0001),inference(resolution,[status(thm)],[c263, reflexivity])).
% 0.91/1.07 cnf(c358,plain,absolutelyInfinite(skolem0001)|skolem0001!=X404|existsIn(X404,X404),inference(factor,[status(thm)],[c263])).
% 0.91/1.07 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.91/1.07 fof(c146,plain,(![X]:(canBeConceivedAsNonExisting(X)=>~essenceInvExistence(X))),inference(fof_simplification,[status(thm)],[can_be_conceived_as_non_existing])).
% 0.91/1.07 fof(c147,plain,(![X]:(~canBeConceivedAsNonExisting(X)|~essenceInvExistence(X))),inference(fof_nnf,[status(thm)],[c146])).
% 0.91/1.07 fof(c148,plain,(![X43]:(~canBeConceivedAsNonExisting(X43)|~essenceInvExistence(X43))),inference(variable_rename,[status(thm)],[c147])).
% 0.91/1.07 cnf(c149,plain,~canBeConceivedAsNonExisting(X87)|~essenceInvExistence(X87),inference(split_conjunct,[status(thm)],[c148])).
% 0.91/1.07 cnf(c400,plain,absolutelyInfinite(skolem0001)|conceivedThru(skolem0001,X402)|~canBeConceivedAsNonExisting(X403),inference(resolution,[status(thm)],[c364, c149])).
% 0.91/1.07 cnf(c385,plain,absolutelyInfinite(skolem0001)|existsIn(skolem0001,X400)|~canBeConceivedAsNonExisting(X401),inference(resolution,[status(thm)],[c351, c149])).
% 0.91/1.07 cnf(c260,plain,existsIn(skolem0001,skolem0001)|~being(skolem0001)|god(skolem0001),inference(resolution,[status(thm)],[c258, c104])).
% 0.91/1.07 cnf(c96,negated_conjecture,absolutelyInfinite(skolem0001)|~attributeOf(skolem0002,skolem0001)|expressesInfiniteEssentiality(skolem0002),inference(split_conjunct,[status(thm)],[c90])).
% 0.91/1.07 cnf(c95,negated_conjecture,absolutelyInfinite(skolem0001)|~attributeOf(skolem0002,skolem0001)|expressesEternalEssentiality(skolem0002),inference(split_conjunct,[status(thm)],[c90])).
% 0.91/1.07 cnf(c265,plain,mode(skolem0001)|~being(skolem0001)|god(skolem0001),inference(resolution,[status(thm)],[c261, c104])).
% 0.91/1.07 cnf(c259,plain,exists(skolem0001)|~being(skolem0001)|god(skolem0001),inference(resolution,[status(thm)],[c257, c104])).
% 0.91/1.07 cnf(c223,plain,~being(skolem0001)|god(skolem0001)|substance(skolem0001),inference(resolution,[status(thm)],[c104, c93])).
% 0.91/1.07 cnf(c92,negated_conjecture,~absolutelyInfinite(skolem0001)|~substance(skolem0001)|~constInInfAttributes(skolem0001)|~expressesEternalEssentiality(skolem0002)|~expressesInfiniteEssentiality(skolem0002),inference(split_conjunct,[status(thm)],[c90])).
% 0.91/1.07 cnf(c94,negated_conjecture,absolutelyInfinite(skolem0001)|constInInfAttributes(skolem0001),inference(split_conjunct,[status(thm)],[c90])).
% 0.91/1.07 cnf(c222,plain,~being(skolem0001)|god(skolem0001)|constInInfAttributes(skolem0001),inference(resolution,[status(thm)],[c104, c94])).
% 0.91/1.07 cnf(c221,plain,~being(skolem0001)|god(skolem0001)|inItself(skolem0001),inference(resolution,[status(thm)],[c104, c200])).
% 0.91/1.07 cnf(c220,plain,~being(skolem0001)|god(skolem0001)|essenceInvExistence(skolem0001),inference(resolution,[status(thm)],[c104, c211])).
% 0.91/1.07 cnf(c219,plain,~being(skolem0001)|god(skolem0001)|selfCaused(skolem0001),inference(resolution,[status(thm)],[c104, c208])).
% 0.91/1.07 cnf(c91,negated_conjecture,~absolutelyInfinite(skolem0001)|~substance(skolem0001)|~constInInfAttributes(skolem0001)|attributeOf(skolem0002,skolem0001),inference(split_conjunct,[status(thm)],[c90])).
% 0.91/1.07 cnf(c201,plain,absolutelyInfinite(skolem0001)|conceivedThruItself(skolem0001),inference(resolution,[status(thm)],[c93, c128])).
% 0.91/1.07 cnf(c217,plain,~being(skolem0001)|god(skolem0001)|conceivedThruItself(skolem0001),inference(resolution,[status(thm)],[c104, c201])).
% 0.91/1.07 cnf(c210,plain,absolutelyInfinite(skolem0001)|natureConcOnlyByExistence(skolem0001),inference(resolution,[status(thm)],[c208, c144])).
% 0.91/1.07 cnf(c215,plain,~being(skolem0001)|god(skolem0001)|natureConcOnlyByExistence(skolem0001),inference(resolution,[status(thm)],[c104, c210])).
% 0.91/1.07 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.91/1.07 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.91/1.07 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.91/1.07 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.91/1.07 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.91/1.07 cnf(c76,plain,~externalTo(X337,X336)|~determinedByFixedMethod(X336,X337)|~determinedByDefiniteMethod(X336,X337)|~isMethodExistence(X337)|necessary(X336),inference(split_conjunct,[status(thm)],[c70])).
% 0.91/1.07 cnf(c207,plain,X327!=X328|X327!=X326|conceivedThru(X328,X326),inference(resolution,[status(thm)],[c204, c2])).
% 0.91/1.07 cnf(c255,plain,X334!=X333|conceivedThru(X333,X334),inference(resolution,[status(thm)],[c207, reflexivity])).
% 0.91/1.07 cnf(c75,plain,~externalTo(X332,X331)|~determinedByFixedMethod(X331,X332)|~determinedByDefiniteMethod(X331,X332)|~isMethodAction(X332)|necessary(X331),inference(split_conjunct,[status(thm)],[c70])).
% 0.91/1.07 cnf(c195,plain,~existsIn(X324,X325)|X324=X325|exists(X324),inference(split_conjunct,[status(thm)],[c191])).
% 0.91/1.07 cnf(c44,axiom,X318!=X319|X320!=X317|~determinedByFixedMethod(X318,X320)|determinedByFixedMethod(X319,X317),theory(equality)).
% 0.91/1.07 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.91/1.07 fof(c150,plain,(![X]:(![Y]:(~trueIdea(X)|(correspondWith(X,Y)&(ideateOf(Y,X)|objectOf(Y,X)))))),inference(fof_nnf,[status(thm)],[true_idea])).
% 0.91/1.07 fof(c151,plain,(![X]:(~trueIdea(X)|((![Y]:correspondWith(X,Y))&(![Y]:(ideateOf(Y,X)|objectOf(Y,X)))))),inference(shift_quantors,[status(thm)],[c150])).
% 0.91/1.07 fof(c153,plain,(![X44]:(![X45]:(![X46]:(~trueIdea(X44)|(correspondWith(X44,X45)&(ideateOf(X46,X44)|objectOf(X46,X44))))))),inference(shift_quantors,[status(thm)],[fof(c152,plain,(![X44]:(~trueIdea(X44)|((![X45]:correspondWith(X44,X45))&(![X46]:(ideateOf(X46,X44)|objectOf(X46,X44)))))),inference(variable_rename,[status(thm)],[c151])).])).
% 0.91/1.07 fof(c154,plain,(![X44]:(![X45]:(![X46]:((~trueIdea(X44)|correspondWith(X44,X45))&(~trueIdea(X44)|(ideateOf(X46,X44)|objectOf(X46,X44))))))),inference(distribute,[status(thm)],[c153])).
% 0.91/1.07 cnf(c156,plain,~trueIdea(X314)|ideateOf(X313,X314)|objectOf(X313,X314),inference(split_conjunct,[status(thm)],[c154])).
% 0.91/1.07 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.91/1.07 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.91/1.07 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.91/1.07 fof(c133,plain,(![X36]:(![X37]:(![X38]:(![X39]:(![X40]:((~finiteAfterItsKind(X36)|(canBeLimitedBy(X36,X37)&sameKind(X36,X38)))&((~canBeLimitedBy(X39,X40)|~sameKind(X39,X40))|finiteAfterItsKind(X39)))))))),inference(shift_quantors,[status(thm)],[fof(c132,plain,((![X36]:(~finiteAfterItsKind(X36)|((![X37]:canBeLimitedBy(X36,X37))&(![X38]:sameKind(X36,X38)))))&(![X39]:((![X40]:(~canBeLimitedBy(X39,X40)|~sameKind(X39,X40)))|finiteAfterItsKind(X39)))),inference(variable_rename,[status(thm)],[c131])).])).
% 0.91/1.07 fof(c134,plain,(![X36]:(![X37]:(![X38]:(![X39]:(![X40]:(((~finiteAfterItsKind(X36)|canBeLimitedBy(X36,X37))&(~finiteAfterItsKind(X36)|sameKind(X36,X38)))&((~canBeLimitedBy(X39,X40)|~sameKind(X39,X40))|finiteAfterItsKind(X39)))))))),inference(distribute,[status(thm)],[c133])).
% 0.91/1.07 cnf(c137,plain,~canBeLimitedBy(X312,X311)|~sameKind(X312,X311)|finiteAfterItsKind(X312),inference(split_conjunct,[status(thm)],[c134])).
% 0.91/1.07 cnf(c43,axiom,X305!=X306|X307!=X304|~externalTo(X305,X307)|externalTo(X306,X304),theory(equality)).
% 0.91/1.07 fof(free,axiom,(![X]:(![Y]:(free(X)<=>(existsOnlyByNecessityOfOwnNature(X)&(actionOf(Y,X)=>determinedByItselfAlone(Y,X)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', free)).
% 0.91/1.07 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.91/1.07 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.91/1.07 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.91/1.07 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.91/1.07 cnf(c83,plain,~free(X297)|~actionOf(X296,X297)|determinedByItselfAlone(X296,X297),inference(split_conjunct,[status(thm)],[c81])).
% 0.91/1.07 cnf(c114,plain,~modification(X293,X292)|~substance(X292)|mode(X293),inference(split_conjunct,[status(thm)],[c109])).
% 0.91/1.07 cnf(c40,axiom,X289!=X290|X291!=X288|~determinedByDefiniteMethod(X289,X291)|determinedByDefiniteMethod(X290,X288),theory(equality)).
% 0.91/1.07 cnf(c85,plain,~existsOnlyByNecessityOfOwnNature(X281)|~determinedByItselfAlone(X280,X281)|free(X281),inference(split_conjunct,[status(thm)],[c81])).
% 0.91/1.07 cnf(c84,plain,~existsOnlyByNecessityOfOwnNature(X279)|actionOf(X278,X279)|free(X279),inference(split_conjunct,[status(thm)],[c81])).
% 0.91/1.07 cnf(c38,axiom,X274!=X275|X276!=X273|~determinedByItselfAlone(X274,X276)|determinedByItselfAlone(X275,X273),theory(equality)).
% 0.91/1.07 cnf(c47,axiom,X271!=X272|~hasEssence(X271)|hasEssence(X272),theory(equality)).
% 0.91/1.07 cnf(c46,axiom,X268!=X269|~existConcFollowFromDefEternal(X268)|existConcFollowFromDefEternal(X269),theory(equality)).
% 0.91/1.07 cnf(c45,axiom,X265!=X266|~eternity(X265)|eternity(X266),theory(equality)).
% 0.91/1.07 cnf(c37,axiom,X262!=X263|X264!=X261|~actionOf(X262,X264)|actionOf(X263,X261),theory(equality)).
% 0.91/1.07 cnf(c42,axiom,X258!=X259|~isMethodExistence(X258)|isMethodExistence(X259),theory(equality)).
% 0.91/1.07 cnf(c41,axiom,X255!=X256|~isMethodAction(X255)|isMethodAction(X256),theory(equality)).
% 0.91/1.07 cnf(c32,axiom,X251!=X252|X253!=X250|~attributeOf(X251,X253)|attributeOf(X252,X250),theory(equality)).
% 0.91/1.07 cnf(c39,axiom,X248!=X249|~necessary(X248)|necessary(X249),theory(equality)).
% 0.91/1.07 cnf(c36,axiom,X245!=X246|~existsOnlyByNecessityOfOwnNature(X245)|existsOnlyByNecessityOfOwnNature(X246),theory(equality)).
% 0.91/1.07 cnf(c35,axiom,X242!=X243|~free(X242)|free(X243),theory(equality)).
% 0.91/1.07 cnf(c34,axiom,X235!=X236|~expressesInfiniteEssentiality(X235)|expressesInfiniteEssentiality(X236),theory(equality)).
% 0.91/1.07 cnf(c33,axiom,X232!=X233|~expressesEternalEssentiality(X232)|expressesEternalEssentiality(X233),theory(equality)).
% 0.91/1.07 cnf(c20,axiom,X228!=X229|X230!=X227|~sameKind(X228,X230)|sameKind(X229,X227),theory(equality)).
% 0.91/1.07 cnf(c31,axiom,X225!=X226|~constInInfAttributes(X225)|constInInfAttributes(X226),theory(equality)).
% 0.91/1.07 cnf(c30,axiom,X222!=X223|~absolutelyInfinite(X222)|absolutelyInfinite(X223),theory(equality)).
% 0.91/1.07 cnf(c29,axiom,X219!=X220|~being(X219)|being(X220),theory(equality)).
% 0.91/1.07 cnf(c19,axiom,X216!=X217|X218!=X215|~canBeLimitedBy(X216,X218)|canBeLimitedBy(X217,X215),theory(equality)).
% 0.91/1.07 cnf(c28,axiom,X212!=X213|~god(X212)|god(X213),theory(equality)).
% 0.91/1.07 cnf(c26,axiom,X209!=X210|~mode(X209)|mode(X210),theory(equality)).
% 0.91/1.07 cnf(c13,axiom,X205!=X206|X207!=X204|~objectOf(X205,X207)|objectOf(X206,X204),theory(equality)).
% 0.91/1.07 cnf(c25,axiom,X202!=X203|~intPercAsConstEssSub(X202)|intPercAsConstEssSub(X203),theory(equality)).
% 0.91/1.07 cnf(c24,axiom,X199!=X200|~attribute(X199)|attribute(X200),theory(equality)).
% 0.91/1.07 cnf(c23,axiom,X196!=X197|~conceivedThruItself(X196)|conceivedThruItself(X197),theory(equality)).
% 0.91/1.07 cnf(c12,axiom,X193!=X194|X195!=X192|~ideateOf(X193,X195)|ideateOf(X194,X192),theory(equality)).
% 0.91/1.07 cnf(c22,axiom,X189!=X190|~inItself(X189)|inItself(X190),theory(equality)).
% 0.91/1.07 cnf(c21,axiom,X186!=X187|~substance(X186)|substance(X187),theory(equality)).
% 0.91/1.07 cnf(c11,axiom,X182!=X183|X184!=X181|~correspondWith(X182,X184)|correspondWith(X183,X181),theory(equality)).
% 0.91/1.07 cnf(c18,axiom,X179!=X180|~finiteAfterItsKind(X179)|finiteAfterItsKind(X180),theory(equality)).
% 0.91/1.07 cnf(c17,axiom,X176!=X177|~natureConcOnlyByExistence(X176)|natureConcOnlyByExistence(X177),theory(equality)).
% 0.91/1.07 cnf(c16,axiom,X173!=X174|~selfCaused(X173)|selfCaused(X174),theory(equality)).
% 0.91/1.07 cnf(c9,axiom,X170!=X171|X172!=X169|~canBeUnderstoodInTermsOf(X170,X172)|canBeUnderstoodInTermsOf(X171,X169),theory(equality)).
% 0.91/1.07 cnf(c15,axiom,X166!=X167|~essenceInvExistence(X166)|essenceInvExistence(X167),theory(equality)).
% 0.91/1.07 cnf(c14,axiom,X163!=X164|~canBeConceivedAsNonExisting(X163)|canBeConceivedAsNonExisting(X164),theory(equality)).
% 0.91/1.07 cnf(c8,axiom,X159!=X160|X161!=X158|~conceptionInvolves(X159,X161)|conceptionInvolves(X160,X158),theory(equality)).
% 0.91/1.07 cnf(c10,axiom,X156!=X157|~trueIdea(X156)|trueIdea(X157),theory(equality)).
% 0.91/1.07 cnf(c145,plain,~essenceInvExistence(X155)|~natureConcOnlyByExistence(X155)|selfCaused(X155),inference(split_conjunct,[status(thm)],[c142])).
% 0.91/1.07 cnf(c129,plain,~inItself(X154)|~conceivedThruItself(X154)|substance(X154),inference(split_conjunct,[status(thm)],[c126])).
% 0.91/1.07 cnf(c74,plain,~necessary(X151)|isMethodAction(X152)|isMethodExistence(X152),inference(split_conjunct,[status(thm)],[c70])).
% 0.91/1.07 cnf(c7,axiom,X148!=X149|X150!=X147|~haveNothingInCommon(X148,X150)|haveNothingInCommon(X149,X147),theory(equality)).
% 0.91/1.07 cnf(c213,plain,absolutelyInfinite(skolem0001)|~canBeConceivedAsNonExisting(skolem0001),inference(resolution,[status(thm)],[c211, c149])).
% 0.91/1.07 cnf(c6,axiom,X143!=X144|~knowledgeOfACause(X143)|knowledgeOfACause(X144),theory(equality)).
% 0.91/1.07 cnf(c5,axiom,X140!=X141|X142!=X139|~knowledgeOfEffect(X140,X142)|knowledgeOfEffect(X141,X139),theory(equality)).
% 0.91/1.07 cnf(c4,axiom,X128!=X129|X130!=X127|~effectNecessarilyFollowsFrom(X128,X130)|effectNecessarilyFollowsFrom(X129,X127),theory(equality)).
% 0.91/1.07 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.91/1.07 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.91/1.07 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.91/1.07 fof(c159,plain,(![X47]:(![X48]:(~haveNothingInCommon(X47,X48)|(((~canBeUnderstoodInTermsOf(X47,X48)&~canBeUnderstoodInTermsOf(X48,X47))&~conceptionInvolves(X47,X48))&~conceptionInvolves(X48,X47))))),inference(variable_rename,[status(thm)],[c158])).
% 0.91/1.07 fof(c160,plain,(![X47]:(![X48]:((((~haveNothingInCommon(X47,X48)|~canBeUnderstoodInTermsOf(X47,X48))&(~haveNothingInCommon(X47,X48)|~canBeUnderstoodInTermsOf(X48,X47)))&(~haveNothingInCommon(X47,X48)|~conceptionInvolves(X47,X48)))&(~haveNothingInCommon(X47,X48)|~conceptionInvolves(X48,X47))))),inference(distribute,[status(thm)],[c159])).
% 0.91/1.07 cnf(c164,plain,~haveNothingInCommon(X126,X125)|~conceptionInvolves(X125,X126),inference(split_conjunct,[status(thm)],[c160])).
% 0.91/1.07 cnf(c163,plain,~haveNothingInCommon(X124,X123)|~conceptionInvolves(X124,X123),inference(split_conjunct,[status(thm)],[c160])).
% 0.91/1.07 cnf(c162,plain,~haveNothingInCommon(X122,X121)|~canBeUnderstoodInTermsOf(X121,X122),inference(split_conjunct,[status(thm)],[c160])).
% 0.91/1.07 cnf(c161,plain,~haveNothingInCommon(X120,X119)|~canBeUnderstoodInTermsOf(X120,X119),inference(split_conjunct,[status(thm)],[c160])).
% 0.91/1.07 cnf(c3,axiom,X116!=X117|~definiteCause(X116)|definiteCause(X117),theory(equality)).
% 0.91/1.07 cnf(c194,plain,~existsIn(X115,X115)|exists(X115),inference(split_conjunct,[status(thm)],[c191])).
% 0.91/1.07 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.91/1.07 fof(c171,plain,(![X]:(![Y]:(definiteCause(X)=>(effectNecessarilyFollowsFrom(Y,X)&(~definiteCause(X)=>~effectNecessarilyFollowsFrom(Y,X)))))),inference(fof_simplification,[status(thm)],[definite_cause])).
% 0.91/1.07 fof(c172,plain,(![X]:(![Y]:(~definiteCause(X)|(effectNecessarilyFollowsFrom(Y,X)&(definiteCause(X)|~effectNecessarilyFollowsFrom(Y,X)))))),inference(fof_nnf,[status(thm)],[c171])).
% 0.91/1.07 fof(c173,plain,(![X]:(~definiteCause(X)|((![Y]:effectNecessarilyFollowsFrom(Y,X))&(definiteCause(X)|(![Y]:~effectNecessarilyFollowsFrom(Y,X)))))),inference(shift_quantors,[status(thm)],[c172])).
% 0.91/1.07 fof(c175,plain,(![X53]:(![X54]:(![X55]:(~definiteCause(X53)|(effectNecessarilyFollowsFrom(X54,X53)&(definiteCause(X53)|~effectNecessarilyFollowsFrom(X55,X53))))))),inference(shift_quantors,[status(thm)],[fof(c174,plain,(![X53]:(~definiteCause(X53)|((![X54]:effectNecessarilyFollowsFrom(X54,X53))&(definiteCause(X53)|(![X55]:~effectNecessarilyFollowsFrom(X55,X53)))))),inference(variable_rename,[status(thm)],[c173])).])).
% 0.91/1.07 fof(c176,plain,(![X53]:(![X54]:(![X55]:((~definiteCause(X53)|effectNecessarilyFollowsFrom(X54,X53))&(~definiteCause(X53)|(definiteCause(X53)|~effectNecessarilyFollowsFrom(X55,X53))))))),inference(distribute,[status(thm)],[c175])).
% 0.91/1.07 cnf(c177,plain,~definiteCause(X113)|effectNecessarilyFollowsFrom(X114,X113),inference(split_conjunct,[status(thm)],[c176])).
% 0.91/1.07 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.91/1.07 fof(c165,plain,(![X]:(![Y]:((~knowledgeOfEffect(X,Y)|knowledgeOfACause(X))&(~knowledgeOfACause(X)|knowledgeOfEffect(X,Y))))),inference(fof_nnf,[status(thm)],[knowledge_of_effect])).
% 0.91/1.07 fof(c166,plain,((![X]:((![Y]:~knowledgeOfEffect(X,Y))|knowledgeOfACause(X)))&(![X]:(~knowledgeOfACause(X)|(![Y]:knowledgeOfEffect(X,Y))))),inference(shift_quantors,[status(thm)],[c165])).
% 0.91/1.07 fof(c168,plain,(![X49]:(![X50]:(![X51]:(![X52]:((~knowledgeOfEffect(X49,X50)|knowledgeOfACause(X49))&(~knowledgeOfACause(X51)|knowledgeOfEffect(X51,X52))))))),inference(shift_quantors,[status(thm)],[fof(c167,plain,((![X49]:((![X50]:~knowledgeOfEffect(X49,X50))|knowledgeOfACause(X49)))&(![X51]:(~knowledgeOfACause(X51)|(![X52]:knowledgeOfEffect(X51,X52))))),inference(variable_rename,[status(thm)],[c166])).])).
% 0.91/1.07 cnf(c170,plain,~knowledgeOfACause(X112)|knowledgeOfEffect(X112,X111),inference(split_conjunct,[status(thm)],[c168])).
% 0.91/1.07 cnf(c169,plain,~knowledgeOfEffect(X106,X105)|knowledgeOfACause(X106),inference(split_conjunct,[status(thm)],[c168])).
% 0.91/1.07 cnf(c155,plain,~trueIdea(X104)|correspondWith(X104,X103),inference(split_conjunct,[status(thm)],[c154])).
% 0.91/1.07 cnf(c136,plain,~finiteAfterItsKind(X102)|sameKind(X102,X101),inference(split_conjunct,[status(thm)],[c134])).
% 0.91/1.07 cnf(c135,plain,~finiteAfterItsKind(X100)|canBeLimitedBy(X100,X99),inference(split_conjunct,[status(thm)],[c134])).
% 0.91/1.07 cnf(c73,plain,~necessary(X98)|determinedByDefiniteMethod(X98,X97),inference(split_conjunct,[status(thm)],[c70])).
% 0.91/1.07 cnf(c72,plain,~necessary(X91)|determinedByFixedMethod(X91,X92),inference(split_conjunct,[status(thm)],[c70])).
% 0.91/1.07 cnf(c71,plain,~necessary(X89)|externalTo(X90,X89),inference(split_conjunct,[status(thm)],[c70])).
% 0.91/1.07 cnf(c0,axiom,X84!=X85|~exists(X84)|exists(X85),theory(equality)).
% 0.91/1.07 fof(attribute,axiom,(![X]:(attribute(X)<=>intPercAsConstEssSub(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', attribute)).
% 0.91/1.07 fof(c116,plain,(![X]:((~attribute(X)|intPercAsConstEssSub(X))&(~intPercAsConstEssSub(X)|attribute(X)))),inference(fof_nnf,[status(thm)],[attribute])).
% 0.91/1.07 fof(c117,plain,((![X]:(~attribute(X)|intPercAsConstEssSub(X)))&(![X]:(~intPercAsConstEssSub(X)|attribute(X)))),inference(shift_quantors,[status(thm)],[c116])).
% 0.91/1.07 fof(c119,plain,(![X32]:(![X33]:((~attribute(X32)|intPercAsConstEssSub(X32))&(~intPercAsConstEssSub(X33)|attribute(X33))))),inference(shift_quantors,[status(thm)],[fof(c118,plain,((![X32]:(~attribute(X32)|intPercAsConstEssSub(X32)))&(![X33]:(~intPercAsConstEssSub(X33)|attribute(X33)))),inference(variable_rename,[status(thm)],[c117])).])).
% 0.91/1.07 cnf(c121,plain,~intPercAsConstEssSub(X80)|attribute(X80),inference(split_conjunct,[status(thm)],[c119])).
% 0.91/1.07 cnf(c120,plain,~attribute(X79)|intPercAsConstEssSub(X79),inference(split_conjunct,[status(thm)],[c119])).
% 0.91/1.07 cnf(transitivity,axiom,X77!=X76|X76!=X78|X77=X78,theory(equality)).
% 0.91/1.07 cnf(c103,plain,~god(X75)|absolutelyInfinite(X75),inference(split_conjunct,[status(thm)],[c101])).
% 0.91/1.07 cnf(c102,plain,~god(X74)|being(X74),inference(split_conjunct,[status(thm)],[c101])).
% 0.91/1.07 cnf(c82,plain,~free(X73)|existsOnlyByNecessityOfOwnNature(X73),inference(split_conjunct,[status(thm)],[c81])).
% 0.91/1.07 fof(eternity,axiom,(![X]:(eternity(X)<=>existConcFollowFromDefEternal(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', eternity)).
% 0.91/1.07 fof(c60,plain,(![X]:((~eternity(X)|existConcFollowFromDefEternal(X))&(~existConcFollowFromDefEternal(X)|eternity(X)))),inference(fof_nnf,[status(thm)],[eternity])).
% 0.91/1.07 fof(c61,plain,((![X]:(~eternity(X)|existConcFollowFromDefEternal(X)))&(![X]:(~existConcFollowFromDefEternal(X)|eternity(X)))),inference(shift_quantors,[status(thm)],[c60])).
% 0.91/1.07 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.91/1.07 cnf(c65,plain,~existConcFollowFromDefEternal(X72)|eternity(X72),inference(split_conjunct,[status(thm)],[c63])).
% 0.91/1.07 cnf(symmetry,axiom,X70!=X69|X69=X70,theory(equality)).
% 0.91/1.07 cnf(c64,plain,~eternity(X68)|existConcFollowFromDefEternal(X68),inference(split_conjunct,[status(thm)],[c63])).
% 0.91/1.07 % SZS output end Saturation
% 0.91/1.07
% 0.91/1.07 % Initial clauses : 110
% 0.91/1.07 % Processed clauses : 287
% 0.91/1.07 % Factors computed : 49
% 0.91/1.07 % Resolvents computed: 481
% 0.91/1.07 % Tautologies deleted: 34
% 0.91/1.07 % Forward subsumed : 319
% 0.91/1.07 % Backward subsumed : 53
% 0.91/1.07 % -------- CPU Time ---------
% 0.91/1.07 % User time : 0.696 s
% 0.91/1.07 % System time : 0.023 s
% 0.91/1.07 % Total time : 0.719 s
%------------------------------------------------------------------------------