%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PHI026+1 : TPTP v8.1.2. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n021.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:18 EDT 2024
% Result : CounterSatisfiable 0.48s 0.66s
% Output : Saturation 0.48s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.14 % Problem : PHI026+1 : TPTP v8.1.2. Released v7.4.0.
% 0.10/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n021.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Wed May 8 22:29:38 EDT 2024
% 0.14/0.36 % CPUTime :
% 0.48/0.66 % Version: 1.5
% 0.48/0.66 % SZS status CounterSatisfiable
% 0.48/0.66 % SZS output start Saturation
% 0.48/0.66 cnf(reflexivity,axiom,X64=X64,theory(equality)).
% 0.48/0.66 cnf(c13,axiom,X178!=X177|X176!=X179|~existsIn(X178,X176)|existsIn(X177,X179),theory(equality)).
% 0.48/0.66 fof(self_caused,axiom,(![X]:(selfCaused(X)<=>(essenceInvExistence(X)&natureConcOnlyByExistence(X)))),file('/export/starexec/sandbox/benchmark/Axioms/PHI002+0.ax', self_caused)).
% 0.48/0.66 fof(c188,plain,(![X]:((~selfCaused(X)|(essenceInvExistence(X)&natureConcOnlyByExistence(X)))&((~essenceInvExistence(X)|~natureConcOnlyByExistence(X))|selfCaused(X)))),inference(fof_nnf,[status(thm)],[self_caused])).
% 0.48/0.66 fof(c189,plain,((![X]:(~selfCaused(X)|(essenceInvExistence(X)&natureConcOnlyByExistence(X))))&(![X]:((~essenceInvExistence(X)|~natureConcOnlyByExistence(X))|selfCaused(X)))),inference(shift_quantors,[status(thm)],[c188])).
% 0.48/0.66 fof(c191,plain,(![X62]:(![X63]:((~selfCaused(X62)|(essenceInvExistence(X62)&natureConcOnlyByExistence(X62)))&((~essenceInvExistence(X63)|~natureConcOnlyByExistence(X63))|selfCaused(X63))))),inference(shift_quantors,[status(thm)],[fof(c190,plain,((![X62]:(~selfCaused(X62)|(essenceInvExistence(X62)&natureConcOnlyByExistence(X62))))&(![X63]:((~essenceInvExistence(X63)|~natureConcOnlyByExistence(X63))|selfCaused(X63)))),inference(variable_rename,[status(thm)],[c189])).])).
% 0.48/0.66 fof(c192,plain,(![X62]:(![X63]:(((~selfCaused(X62)|essenceInvExistence(X62))&(~selfCaused(X62)|natureConcOnlyByExistence(X62)))&((~essenceInvExistence(X63)|~natureConcOnlyByExistence(X63))|selfCaused(X63))))),inference(distribute,[status(thm)],[c191])).
% 0.48/0.66 cnf(c193,plain,~selfCaused(X88)|essenceInvExistence(X88),inference(split_conjunct,[status(thm)],[c192])).
% 0.48/0.66 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.48/0.66 fof(c54,plain,(![X]:(~inItself(X)|selfCaused(X))),inference(fof_nnf,[status(thm)],[is_in_itself_is_self_caused])).
% 0.48/0.66 fof(c55,plain,(![X4]:(~inItself(X4)|selfCaused(X4))),inference(variable_rename,[status(thm)],[c54])).
% 0.48/0.66 cnf(c56,plain,~inItself(X66)|selfCaused(X66),inference(split_conjunct,[status(thm)],[c55])).
% 0.48/0.66 fof(substance,axiom,(![X]:(substance(X)<=>(inItself(X)&conceivedThruItself(X)))),file('/export/starexec/sandbox/benchmark/Axioms/PHI002+0.ax', substance)).
% 0.48/0.66 fof(c172,plain,(![X]:((~substance(X)|(inItself(X)&conceivedThruItself(X)))&((~inItself(X)|~conceivedThruItself(X))|substance(X)))),inference(fof_nnf,[status(thm)],[substance])).
% 0.48/0.66 fof(c173,plain,((![X]:(~substance(X)|(inItself(X)&conceivedThruItself(X))))&(![X]:((~inItself(X)|~conceivedThruItself(X))|substance(X)))),inference(shift_quantors,[status(thm)],[c172])).
% 0.48/0.66 fof(c175,plain,(![X55]:(![X56]:((~substance(X55)|(inItself(X55)&conceivedThruItself(X55)))&((~inItself(X56)|~conceivedThruItself(X56))|substance(X56))))),inference(shift_quantors,[status(thm)],[fof(c174,plain,((![X55]:(~substance(X55)|(inItself(X55)&conceivedThruItself(X55))))&(![X56]:((~inItself(X56)|~conceivedThruItself(X56))|substance(X56)))),inference(variable_rename,[status(thm)],[c173])).])).
% 0.48/0.66 fof(c176,plain,(![X55]:(![X56]:(((~substance(X55)|inItself(X55))&(~substance(X55)|conceivedThruItself(X55)))&((~inItself(X56)|~conceivedThruItself(X56))|substance(X56))))),inference(distribute,[status(thm)],[c175])).
% 0.48/0.66 cnf(c177,plain,~substance(X86)|inItself(X86),inference(split_conjunct,[status(thm)],[c176])).
% 0.48/0.66 fof(mode,axiom,(![X]:(![Y]:(![Z]:(mode(X)<=>((modification(X,Y)&substance(Y))|(existsIn(X,Z)&conceivedThru(X,Z))))))),file('/export/starexec/sandbox/benchmark/Axioms/PHI002+0.ax', mode)).
% 0.48/0.66 fof(c155,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.48/0.66 fof(c156,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)],[c155])).
% 0.48/0.66 fof(c158,plain,(![X45]:(![X46]:(![X47]:(![X48]:(![X49]:(![X50]:(![X51]:(![X52]:((~mode(X45)|((modification(X45,X46)&substance(X47))|(existsIn(X45,X48)&conceivedThru(X45,X49))))&(((~modification(X50,X51)|~substance(X51))&(~existsIn(X50,X52)|~conceivedThru(X50,X52)))|mode(X50))))))))))),inference(shift_quantors,[status(thm)],[fof(c157,plain,((![X45]:(~mode(X45)|(((![X46]:modification(X45,X46))&(![X47]:substance(X47)))|((![X48]:existsIn(X45,X48))&(![X49]:conceivedThru(X45,X49))))))&(![X50]:(((![X51]:(~modification(X50,X51)|~substance(X51)))&(![X52]:(~existsIn(X50,X52)|~conceivedThru(X50,X52))))|mode(X50)))),inference(variable_rename,[status(thm)],[c156])).])).
% 0.48/0.66 fof(c159,plain,(![X45]:(![X46]:(![X47]:(![X48]:(![X49]:(![X50]:(![X51]:(![X52]:((((~mode(X45)|(modification(X45,X46)|existsIn(X45,X48)))&(~mode(X45)|(modification(X45,X46)|conceivedThru(X45,X49))))&((~mode(X45)|(substance(X47)|existsIn(X45,X48)))&(~mode(X45)|(substance(X47)|conceivedThru(X45,X49)))))&(((~modification(X50,X51)|~substance(X51))|mode(X50))&((~existsIn(X50,X52)|~conceivedThru(X50,X52))|mode(X50)))))))))))),inference(distribute,[status(thm)],[c158])).
% 0.48/0.66 cnf(c162,plain,~mode(X274)|substance(X273)|existsIn(X274,X275),inference(split_conjunct,[status(thm)],[c159])).
% 0.48/0.66 fof(conceived_through,axiom,(![X]:(![Y]:((~conceivedThru(X,X))=>(conceivedThru(X,Y)&X!=Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', conceived_through)).
% 0.48/0.66 fof(c93,plain,(![X]:(![Y]:(~conceivedThru(X,X)=>(conceivedThru(X,Y)&X!=Y)))),inference(fof_simplification,[status(thm)],[conceived_through])).
% 0.48/0.66 fof(c94,plain,(![X]:(![Y]:(conceivedThru(X,X)|(conceivedThru(X,Y)&X!=Y)))),inference(fof_nnf,[status(thm)],[c93])).
% 0.48/0.66 fof(c95,plain,(![X]:(conceivedThru(X,X)|((![Y]:conceivedThru(X,Y))&(![Y]:X!=Y)))),inference(shift_quantors,[status(thm)],[c94])).
% 0.48/0.66 fof(c97,plain,(![X19]:(![X20]:(![X21]:(conceivedThru(X19,X19)|(conceivedThru(X19,X20)&X19!=X21))))),inference(shift_quantors,[status(thm)],[fof(c96,plain,(![X19]:(conceivedThru(X19,X19)|((![X20]:conceivedThru(X19,X20))&(![X21]:X19!=X21)))),inference(variable_rename,[status(thm)],[c95])).])).
% 0.48/0.66 fof(c98,plain,(![X19]:(![X20]:(![X21]:((conceivedThru(X19,X19)|conceivedThru(X19,X20))&(conceivedThru(X19,X19)|X19!=X21))))),inference(distribute,[status(thm)],[c97])).
% 0.48/0.66 cnf(c99,plain,conceivedThru(X130,X130)|conceivedThru(X130,X131),inference(split_conjunct,[status(thm)],[c98])).
% 0.48/0.66 cnf(c203,plain,conceivedThru(X132,X132),inference(factor,[status(thm)],[c99])).
% 0.48/0.66 cnf(c165,plain,~existsIn(X295,X296)|~conceivedThru(X295,X296)|mode(X295),inference(split_conjunct,[status(thm)],[c159])).
% 0.48/0.66 cnf(c230,plain,~existsIn(X297,X297)|mode(X297),inference(resolution,[status(thm)],[c165, c203])).
% 0.48/0.66 fof(exists,conjecture,(![X]:(![Y]:(exists(X)<=>(existsIn(X,X)|(existsIn(X,Y)&X!=Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', exists)).
% 0.48/0.66 fof(c101,negated_conjecture,(~(![X]:(![Y]:(exists(X)<=>(existsIn(X,X)|(existsIn(X,Y)&X!=Y)))))),inference(assume_negation,[status(cth)],[exists])).
% 0.48/0.66 fof(c102,negated_conjecture,(?[X]:(?[Y]:((~exists(X)|(~existsIn(X,X)&(~existsIn(X,Y)|X=Y)))&(exists(X)|(existsIn(X,X)|(existsIn(X,Y)&X!=Y)))))),inference(fof_nnf,[status(thm)],[c101])).
% 0.48/0.66 fof(c103,negated_conjecture,(?[X22]:(?[X23]:((~exists(X22)|(~existsIn(X22,X22)&(~existsIn(X22,X23)|X22=X23)))&(exists(X22)|(existsIn(X22,X22)|(existsIn(X22,X23)&X22!=X23)))))),inference(variable_rename,[status(thm)],[c102])).
% 0.48/0.66 fof(c104,negated_conjecture,((~exists(skolem0001)|(~existsIn(skolem0001,skolem0001)&(~existsIn(skolem0001,skolem0002)|skolem0001=skolem0002)))&(exists(skolem0001)|(existsIn(skolem0001,skolem0001)|(existsIn(skolem0001,skolem0002)&skolem0001!=skolem0002)))),inference(skolemize,[status(esa)],[c103])).
% 0.48/0.66 fof(c105,negated_conjecture,(((~exists(skolem0001)|~existsIn(skolem0001,skolem0001))&(~exists(skolem0001)|(~existsIn(skolem0001,skolem0002)|skolem0001=skolem0002)))&((exists(skolem0001)|(existsIn(skolem0001,skolem0001)|existsIn(skolem0001,skolem0002)))&(exists(skolem0001)|(existsIn(skolem0001,skolem0001)|skolem0001!=skolem0002)))),inference(distribute,[status(thm)],[c104])).
% 0.48/0.66 cnf(c108,negated_conjecture,exists(skolem0001)|existsIn(skolem0001,skolem0001)|existsIn(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c105])).
% 0.48/0.66 cnf(c234,plain,exists(skolem0001)|existsIn(skolem0001,skolem0002)|mode(skolem0001),inference(resolution,[status(thm)],[c108, c230])).
% 0.48/0.66 cnf(c244,plain,exists(skolem0001)|existsIn(skolem0001,skolem0002)|substance(X343)|existsIn(skolem0001,X342),inference(resolution,[status(thm)],[c234, c162])).
% 0.48/0.66 cnf(c252,plain,exists(skolem0001)|existsIn(skolem0001,skolem0002)|substance(X344),inference(factor,[status(thm)],[c244])).
% 0.48/0.66 cnf(c264,plain,exists(skolem0001)|existsIn(skolem0001,skolem0002)|inItself(X345),inference(resolution,[status(thm)],[c252, c177])).
% 0.48/0.66 cnf(c269,plain,exists(skolem0001)|existsIn(skolem0001,skolem0002)|selfCaused(X350),inference(resolution,[status(thm)],[c264, c56])).
% 0.48/0.66 cnf(c281,plain,exists(skolem0001)|existsIn(skolem0001,skolem0002)|essenceInvExistence(X353),inference(resolution,[status(thm)],[c269, c193])).
% 0.48/0.66 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.48/0.66 fof(c48,plain,(![X]:((~essenceInvExistence(X)|~hasEssence(X))|exists(X))),inference(fof_nnf,[status(thm)],[essence_involves_existence_exists])).
% 0.48/0.66 fof(c49,plain,(![X2]:((~essenceInvExistence(X2)|~hasEssence(X2))|exists(X2))),inference(variable_rename,[status(thm)],[c48])).
% 0.48/0.66 cnf(c50,plain,~essenceInvExistence(X142)|~hasEssence(X142)|exists(X142),inference(split_conjunct,[status(thm)],[c49])).
% 0.48/0.66 fof(being_has_essense,axiom,(![X]:(being(X)=>hasEssence(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', being_has_essense)).
% 0.48/0.66 fof(c51,plain,(![X]:(~being(X)|hasEssence(X))),inference(fof_nnf,[status(thm)],[being_has_essense])).
% 0.48/0.66 fof(c52,plain,(![X3]:(~being(X3)|hasEssence(X3))),inference(variable_rename,[status(thm)],[c51])).
% 0.48/0.66 cnf(c53,plain,~being(X65)|hasEssence(X65),inference(split_conjunct,[status(thm)],[c52])).
% 0.48/0.66 fof(has_substance_being,axiom,(![X]:(substance(X)=>being(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', has_substance_being)).
% 0.48/0.66 fof(c57,plain,(![X]:(~substance(X)|being(X))),inference(fof_nnf,[status(thm)],[has_substance_being])).
% 0.48/0.66 fof(c58,plain,(![X5]:(~substance(X5)|being(X5))),inference(variable_rename,[status(thm)],[c57])).
% 0.48/0.66 cnf(c59,plain,~substance(X67)|being(X67),inference(split_conjunct,[status(thm)],[c58])).
% 0.48/0.66 cnf(c266,plain,exists(skolem0001)|existsIn(skolem0001,skolem0002)|being(X349),inference(resolution,[status(thm)],[c252, c59])).
% 0.48/0.66 cnf(c277,plain,exists(skolem0001)|existsIn(skolem0001,skolem0002)|hasEssence(X351),inference(resolution,[status(thm)],[c266, c53])).
% 0.48/0.66 cnf(c284,plain,exists(skolem0001)|existsIn(skolem0001,skolem0002)|~essenceInvExistence(X356)|exists(X356),inference(resolution,[status(thm)],[c277, c50])).
% 0.48/0.66 cnf(c291,plain,exists(skolem0001)|existsIn(skolem0001,skolem0002)|exists(X357),inference(resolution,[status(thm)],[c284, c281])).
% 0.48/0.66 cnf(c292,plain,exists(skolem0001)|existsIn(skolem0001,skolem0002),inference(factor,[status(thm)],[c291])).
% 0.48/0.66 cnf(c297,plain,exists(skolem0001)|skolem0001!=X393|skolem0002!=X392|existsIn(X393,X392),inference(resolution,[status(thm)],[c292, c13])).
% 0.48/0.66 cnf(c299,plain,exists(skolem0001)|skolem0001!=X394|existsIn(X394,skolem0002),inference(resolution,[status(thm)],[c297, reflexivity])).
% 0.48/0.66 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/Axioms/PHI002+0.ax', necessary)).
% 0.48/0.66 fof(c116,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.48/0.66 fof(c117,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)],[c116])).
% 0.48/0.66 fof(c119,plain,(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:(![X32]:((~necessary(X26)|(((externalTo(X27,X26)&determinedByFixedMethod(X26,X28))&determinedByDefiniteMethod(X26,X29))&(isMethodAction(X30)|isMethodExistence(X30))))&((((~externalTo(X32,X31)|~determinedByFixedMethod(X31,X32))|~determinedByDefiniteMethod(X31,X32))|(~isMethodAction(X32)&~isMethodExistence(X32)))|necessary(X31)))))))))),inference(shift_quantors,[status(thm)],[fof(c118,plain,((![X26]:(~necessary(X26)|((((![X27]:externalTo(X27,X26))&(![X28]:determinedByFixedMethod(X26,X28)))&(![X29]:determinedByDefiniteMethod(X26,X29)))&(![X30]:(isMethodAction(X30)|isMethodExistence(X30))))))&(![X31]:((![X32]:(((~externalTo(X32,X31)|~determinedByFixedMethod(X31,X32))|~determinedByDefiniteMethod(X31,X32))|(~isMethodAction(X32)&~isMethodExistence(X32))))|necessary(X31)))),inference(variable_rename,[status(thm)],[c117])).])).
% 0.48/0.66 fof(c120,plain,(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:(![X32]:(((((~necessary(X26)|externalTo(X27,X26))&(~necessary(X26)|determinedByFixedMethod(X26,X28)))&(~necessary(X26)|determinedByDefiniteMethod(X26,X29)))&(~necessary(X26)|(isMethodAction(X30)|isMethodExistence(X30))))&(((((~externalTo(X32,X31)|~determinedByFixedMethod(X31,X32))|~determinedByDefiniteMethod(X31,X32))|~isMethodAction(X32))|necessary(X31))&((((~externalTo(X32,X31)|~determinedByFixedMethod(X31,X32))|~determinedByDefiniteMethod(X31,X32))|~isMethodExistence(X32))|necessary(X31))))))))))),inference(distribute,[status(thm)],[c119])).
% 0.48/0.66 cnf(c126,plain,~externalTo(X339,X338)|~determinedByFixedMethod(X338,X339)|~determinedByDefiniteMethod(X338,X339)|~isMethodExistence(X339)|necessary(X338),inference(split_conjunct,[status(thm)],[c120])).
% 0.48/0.66 cnf(c125,plain,~externalTo(X337,X336)|~determinedByFixedMethod(X336,X337)|~determinedByDefiniteMethod(X336,X337)|~isMethodAction(X337)|necessary(X336),inference(split_conjunct,[status(thm)],[c120])).
% 0.48/0.66 cnf(c109,negated_conjecture,exists(skolem0001)|existsIn(skolem0001,skolem0001)|skolem0001!=skolem0002,inference(split_conjunct,[status(thm)],[c105])).
% 0.48/0.66 cnf(c107,negated_conjecture,~exists(skolem0001)|~existsIn(skolem0001,skolem0002)|skolem0001=skolem0002,inference(split_conjunct,[status(thm)],[c105])).
% 0.48/0.66 cnf(c45,axiom,X334!=X333|X332!=X335|~objectOf(X334,X332)|objectOf(X333,X335),theory(equality)).
% 0.48/0.66 cnf(c44,axiom,X330!=X329|X328!=X331|~ideateOf(X330,X328)|ideateOf(X329,X331),theory(equality)).
% 0.48/0.66 cnf(c43,axiom,X326!=X325|X324!=X327|~correspondWith(X326,X324)|correspondWith(X325,X327),theory(equality)).
% 0.48/0.66 cnf(c41,axiom,X322!=X321|X320!=X323|~canBeUnderstoodInTermsOf(X322,X320)|canBeUnderstoodInTermsOf(X321,X323),theory(equality)).
% 0.48/0.66 fof(absolutely_infinite,axiom,(![X]:(![Y]:(absolutelyInfinite(X)<=>((substance(X)&constInInfAttributes(X))&(attributeOf(Y,X)=>(expressesEternalEssentiality(Y)&expressesInfiniteEssentiality(Y))))))),file('/export/starexec/sandbox/benchmark/Axioms/PHI002+0.ax', absolutely_infinite)).
% 0.48/0.66 fof(c136,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.48/0.66 fof(c137,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)],[c136])).
% 0.48/0.66 fof(c139,plain,(![X38]:(![X39]:(![X40]:(![X41]:(![X42]:((~absolutelyInfinite(X38)|((substance(X38)&constInInfAttributes(X38))&(~attributeOf(X39,X38)|(expressesEternalEssentiality(X39)&expressesInfiniteEssentiality(X39)))))&(((~substance(X40)|~constInInfAttributes(X40))|(attributeOf(X41,X40)&(~expressesEternalEssentiality(X42)|~expressesInfiniteEssentiality(X42))))|absolutelyInfinite(X40)))))))),inference(shift_quantors,[status(thm)],[fof(c138,plain,((![X38]:(~absolutelyInfinite(X38)|((substance(X38)&constInInfAttributes(X38))&(![X39]:(~attributeOf(X39,X38)|(expressesEternalEssentiality(X39)&expressesInfiniteEssentiality(X39)))))))&(![X40]:(((~substance(X40)|~constInInfAttributes(X40))|((![X41]:attributeOf(X41,X40))&(![X42]:(~expressesEternalEssentiality(X42)|~expressesInfiniteEssentiality(X42)))))|absolutelyInfinite(X40)))),inference(variable_rename,[status(thm)],[c137])).])).
% 0.48/0.66 fof(c140,plain,(![X38]:(![X39]:(![X40]:(![X41]:(![X42]:((((~absolutelyInfinite(X38)|substance(X38))&(~absolutelyInfinite(X38)|constInInfAttributes(X38)))&((~absolutelyInfinite(X38)|(~attributeOf(X39,X38)|expressesEternalEssentiality(X39)))&(~absolutelyInfinite(X38)|(~attributeOf(X39,X38)|expressesInfiniteEssentiality(X39)))))&((((~substance(X40)|~constInInfAttributes(X40))|attributeOf(X41,X40))|absolutelyInfinite(X40))&(((~substance(X40)|~constInInfAttributes(X40))|(~expressesEternalEssentiality(X42)|~expressesInfiniteEssentiality(X42)))|absolutelyInfinite(X40))))))))),inference(distribute,[status(thm)],[c139])).
% 0.48/0.66 cnf(c146,plain,~substance(X319)|~constInInfAttributes(X319)|~expressesEternalEssentiality(X318)|~expressesInfiniteEssentiality(X318)|absolutelyInfinite(X319),inference(split_conjunct,[status(thm)],[c140])).
% 0.48/0.66 cnf(c40,axiom,X316!=X315|X314!=X317|~conceptionInvolves(X316,X314)|conceptionInvolves(X315,X317),theory(equality)).
% 0.48/0.66 cnf(c145,plain,~substance(X313)|~constInInfAttributes(X313)|attributeOf(X312,X313)|absolutelyInfinite(X313),inference(split_conjunct,[status(thm)],[c140])).
% 0.48/0.66 cnf(c14,axiom,X190!=X189|X188!=X191|~conceivedThru(X190,X188)|conceivedThru(X189,X191),theory(equality)).
% 0.48/0.66 cnf(c215,plain,X306!=X304|X306!=X305|conceivedThru(X304,X305),inference(resolution,[status(thm)],[c14, c203])).
% 0.48/0.66 cnf(c232,plain,X309!=X310|conceivedThru(X310,X309),inference(resolution,[status(thm)],[c215, reflexivity])).
% 0.48/0.66 cnf(c39,axiom,X302!=X301|X300!=X303|~haveNothingInCommon(X302,X300)|haveNothingInCommon(X301,X303),theory(equality)).
% 0.48/0.66 fof(finite_after_its_kind,axiom,(![X]:(![Y]:(finiteAfterItsKind(X)<=>(canBeLimitedBy(X,Y)&sameKind(X,Y))))),file('/export/starexec/sandbox/benchmark/Axioms/PHI002+0.ax', finite_after_its_kind)).
% 0.48/0.66 fof(c180,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.48/0.66 fof(c181,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)],[c180])).
% 0.48/0.66 fof(c183,plain,(![X57]:(![X58]:(![X59]:(![X60]:(![X61]:((~finiteAfterItsKind(X57)|(canBeLimitedBy(X57,X58)&sameKind(X57,X59)))&((~canBeLimitedBy(X60,X61)|~sameKind(X60,X61))|finiteAfterItsKind(X60)))))))),inference(shift_quantors,[status(thm)],[fof(c182,plain,((![X57]:(~finiteAfterItsKind(X57)|((![X58]:canBeLimitedBy(X57,X58))&(![X59]:sameKind(X57,X59)))))&(![X60]:((![X61]:(~canBeLimitedBy(X60,X61)|~sameKind(X60,X61)))|finiteAfterItsKind(X60)))),inference(variable_rename,[status(thm)],[c181])).])).
% 0.48/0.66 fof(c184,plain,(![X57]:(![X58]:(![X59]:(![X60]:(![X61]:(((~finiteAfterItsKind(X57)|canBeLimitedBy(X57,X58))&(~finiteAfterItsKind(X57)|sameKind(X57,X59)))&((~canBeLimitedBy(X60,X61)|~sameKind(X60,X61))|finiteAfterItsKind(X60)))))))),inference(distribute,[status(thm)],[c183])).
% 0.48/0.66 cnf(c187,plain,~canBeLimitedBy(X299,X298)|~sameKind(X299,X298)|finiteAfterItsKind(X299),inference(split_conjunct,[status(thm)],[c184])).
% 0.48/0.66 cnf(c161,plain,~mode(X293)|modification(X293,X294)|conceivedThru(X293,X292),inference(split_conjunct,[status(thm)],[c159])).
% 0.48/0.66 cnf(c160,plain,~mode(X289)|modification(X289,X291)|existsIn(X289,X290),inference(split_conjunct,[status(thm)],[c159])).
% 0.48/0.66 cnf(c37,axiom,X287!=X286|X285!=X288|~knowledgeOfEffect(X287,X285)|knowledgeOfEffect(X286,X288),theory(equality)).
% 0.48/0.66 fof(free,axiom,(![X]:(![Y]:(free(X)<=>(existsOnlyByNecessityOfOwnNature(X)&(actionOf(Y,X)=>determinedByItselfAlone(Y,X)))))),file('/export/starexec/sandbox/benchmark/Axioms/PHI002+0.ax', free)).
% 0.48/0.66 fof(c127,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.48/0.66 fof(c128,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)],[c127])).
% 0.48/0.66 fof(c130,plain,(![X33]:(![X34]:(![X35]:(![X36]:(![X37]:((~free(X33)|(existsOnlyByNecessityOfOwnNature(X33)&(~actionOf(X34,X33)|determinedByItselfAlone(X34,X33))))&((~existsOnlyByNecessityOfOwnNature(X35)|(actionOf(X36,X35)&~determinedByItselfAlone(X37,X35)))|free(X35)))))))),inference(shift_quantors,[status(thm)],[fof(c129,plain,((![X33]:(~free(X33)|(existsOnlyByNecessityOfOwnNature(X33)&(![X34]:(~actionOf(X34,X33)|determinedByItselfAlone(X34,X33))))))&(![X35]:((~existsOnlyByNecessityOfOwnNature(X35)|((![X36]:actionOf(X36,X35))&(![X37]:~determinedByItselfAlone(X37,X35))))|free(X35)))),inference(variable_rename,[status(thm)],[c128])).])).
% 0.48/0.66 fof(c131,plain,(![X33]:(![X34]:(![X35]:(![X36]:(![X37]:(((~free(X33)|existsOnlyByNecessityOfOwnNature(X33))&(~free(X33)|(~actionOf(X34,X33)|determinedByItselfAlone(X34,X33))))&(((~existsOnlyByNecessityOfOwnNature(X35)|actionOf(X36,X35))|free(X35))&((~existsOnlyByNecessityOfOwnNature(X35)|~determinedByItselfAlone(X37,X35))|free(X35))))))))),inference(distribute,[status(thm)],[c130])).
% 0.48/0.66 cnf(c133,plain,~free(X284)|~actionOf(X283,X284)|determinedByItselfAlone(X283,X284),inference(split_conjunct,[status(thm)],[c131])).
% 0.48/0.66 fof(true_idea,axiom,(![X]:(![Y]:(trueIdea(X)=>(correspondWith(X,Y)&(ideateOf(Y,X)|objectOf(Y,X)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', true_idea)).
% 0.48/0.66 fof(c64,plain,(![X]:(![Y]:(~trueIdea(X)|(correspondWith(X,Y)&(ideateOf(Y,X)|objectOf(Y,X)))))),inference(fof_nnf,[status(thm)],[true_idea])).
% 0.48/0.66 fof(c65,plain,(![X]:(~trueIdea(X)|((![Y]:correspondWith(X,Y))&(![Y]:(ideateOf(Y,X)|objectOf(Y,X)))))),inference(shift_quantors,[status(thm)],[c64])).
% 0.48/0.66 fof(c67,plain,(![X7]:(![X8]:(![X9]:(~trueIdea(X7)|(correspondWith(X7,X8)&(ideateOf(X9,X7)|objectOf(X9,X7))))))),inference(shift_quantors,[status(thm)],[fof(c66,plain,(![X7]:(~trueIdea(X7)|((![X8]:correspondWith(X7,X8))&(![X9]:(ideateOf(X9,X7)|objectOf(X9,X7)))))),inference(variable_rename,[status(thm)],[c65])).])).
% 0.48/0.66 fof(c68,plain,(![X7]:(![X8]:(![X9]:((~trueIdea(X7)|correspondWith(X7,X8))&(~trueIdea(X7)|(ideateOf(X9,X7)|objectOf(X9,X7))))))),inference(distribute,[status(thm)],[c67])).
% 0.48/0.66 cnf(c70,plain,~trueIdea(X281)|ideateOf(X282,X281)|objectOf(X282,X281),inference(split_conjunct,[status(thm)],[c68])).
% 0.48/0.66 cnf(c164,plain,~modification(X279,X280)|~substance(X280)|mode(X279),inference(split_conjunct,[status(thm)],[c159])).
% 0.48/0.66 cnf(c163,plain,~mode(X278)|substance(X277)|conceivedThru(X278,X276),inference(split_conjunct,[status(thm)],[c159])).
% 0.48/0.66 cnf(c36,axiom,X271!=X270|X269!=X272|~effectNecessarilyFollowsFrom(X271,X269)|effectNecessarilyFollowsFrom(X270,X272),theory(equality)).
% 0.48/0.66 cnf(c144,plain,~absolutelyInfinite(X268)|~attributeOf(X267,X268)|expressesInfiniteEssentiality(X267),inference(split_conjunct,[status(thm)],[c140])).
% 0.48/0.66 cnf(c143,plain,~absolutelyInfinite(X266)|~attributeOf(X265,X266)|expressesEternalEssentiality(X265),inference(split_conjunct,[status(thm)],[c140])).
% 0.48/0.66 cnf(c135,plain,~existsOnlyByNecessityOfOwnNature(X264)|~determinedByItselfAlone(X263,X264)|free(X264),inference(split_conjunct,[status(thm)],[c131])).
% 0.48/0.66 cnf(c134,plain,~existsOnlyByNecessityOfOwnNature(X261)|actionOf(X262,X261)|free(X261),inference(split_conjunct,[status(thm)],[c131])).
% 0.48/0.66 cnf(c106,negated_conjecture,~exists(skolem0001)|~existsIn(skolem0001,skolem0001),inference(split_conjunct,[status(thm)],[c105])).
% 0.48/0.66 cnf(c31,axiom,X259!=X258|X257!=X260|~determinedByFixedMethod(X259,X257)|determinedByFixedMethod(X258,X260),theory(equality)).
% 0.48/0.66 cnf(c47,axiom,X253!=X252|~hasEssence(X253)|hasEssence(X252),theory(equality)).
% 0.48/0.66 cnf(c46,axiom,X250!=X249|~canBeConceivedAsNonExisting(X250)|canBeConceivedAsNonExisting(X249),theory(equality)).
% 0.48/0.66 cnf(c30,axiom,X247!=X246|X245!=X248|~externalTo(X247,X245)|externalTo(X246,X248),theory(equality)).
% 0.48/0.66 cnf(c42,axiom,X243!=X242|~trueIdea(X243)|trueIdea(X242),theory(equality)).
% 0.48/0.66 cnf(c38,axiom,X240!=X239|~knowledgeOfACause(X240)|knowledgeOfACause(X239),theory(equality)).
% 0.48/0.66 cnf(c27,axiom,X236!=X235|X234!=X237|~determinedByDefiniteMethod(X236,X234)|determinedByDefiniteMethod(X235,X237),theory(equality)).
% 0.48/0.66 cnf(c35,axiom,X233!=X232|~definiteCause(X233)|definiteCause(X232),theory(equality)).
% 0.48/0.66 cnf(c34,axiom,X230!=X229|~exists(X230)|exists(X229),theory(equality)).
% 0.48/0.66 cnf(c33,axiom,X227!=X226|~existConcFollowFromDefEternal(X227)|existConcFollowFromDefEternal(X226),theory(equality)).
% 0.48/0.66 cnf(c25,axiom,X224!=X223|X222!=X225|~determinedByItselfAlone(X224,X222)|determinedByItselfAlone(X223,X225),theory(equality)).
% 0.48/0.66 cnf(c32,axiom,X220!=X219|~eternity(X220)|eternity(X219),theory(equality)).
% 0.48/0.66 cnf(c29,axiom,X217!=X216|~isMethodExistence(X217)|isMethodExistence(X216),theory(equality)).
% 0.48/0.66 cnf(c24,axiom,X213!=X212|X211!=X214|~actionOf(X213,X211)|actionOf(X212,X214),theory(equality)).
% 0.48/0.66 cnf(c28,axiom,X210!=X209|~isMethodAction(X210)|isMethodAction(X209),theory(equality)).
% 0.48/0.66 cnf(c26,axiom,X207!=X206|~necessary(X207)|necessary(X206),theory(equality)).
% 0.48/0.66 cnf(c23,axiom,X204!=X203|~existsOnlyByNecessityOfOwnNature(X204)|existsOnlyByNecessityOfOwnNature(X203),theory(equality)).
% 0.48/0.66 cnf(c19,axiom,X201!=X200|X199!=X202|~attributeOf(X201,X199)|attributeOf(X200,X202),theory(equality)).
% 0.48/0.66 cnf(c22,axiom,X197!=X196|~free(X197)|free(X196),theory(equality)).
% 0.48/0.66 cnf(c21,axiom,X194!=X193|~expressesInfiniteEssentiality(X194)|expressesInfiniteEssentiality(X193),theory(equality)).
% 0.48/0.66 cnf(c20,axiom,X187!=X186|~expressesEternalEssentiality(X187)|expressesEternalEssentiality(X186),theory(equality)).
% 0.48/0.66 cnf(c18,axiom,X184!=X183|~constInInfAttributes(X184)|constInInfAttributes(X183),theory(equality)).
% 0.48/0.66 cnf(c17,axiom,X181!=X180|~absolutelyInfinite(X181)|absolutelyInfinite(X180),theory(equality)).
% 0.48/0.66 cnf(c16,axiom,X174!=X173|~being(X174)|being(X173),theory(equality)).
% 0.48/0.66 cnf(c15,axiom,X171!=X170|~god(X171)|god(X170),theory(equality)).
% 0.48/0.66 cnf(c12,axiom,X167!=X166|X165!=X168|~modification(X167,X165)|modification(X166,X168),theory(equality)).
% 0.48/0.66 cnf(c11,axiom,X164!=X163|~mode(X164)|mode(X163),theory(equality)).
% 0.48/0.66 cnf(c10,axiom,X161!=X160|~intPercAsConstEssSub(X161)|intPercAsConstEssSub(X160),theory(equality)).
% 0.48/0.66 cnf(c9,axiom,X157!=X156|~attribute(X157)|attribute(X156),theory(equality)).
% 0.48/0.66 cnf(c8,axiom,X155!=X154|~conceivedThruItself(X155)|conceivedThruItself(X154),theory(equality)).
% 0.48/0.66 cnf(c7,axiom,X152!=X151|~inItself(X152)|inItself(X151),theory(equality)).
% 0.48/0.66 cnf(c195,plain,~essenceInvExistence(X150)|~natureConcOnlyByExistence(X150)|selfCaused(X150),inference(split_conjunct,[status(thm)],[c192])).
% 0.48/0.66 cnf(c6,axiom,X148!=X147|~substance(X148)|substance(X147),theory(equality)).
% 0.48/0.66 cnf(c179,plain,~inItself(X146)|~conceivedThruItself(X146)|substance(X146),inference(split_conjunct,[status(thm)],[c176])).
% 0.48/0.66 fof(god,axiom,(![X]:(god(X)<=>(being(X)&absolutelyInfinite(X)))),file('/export/starexec/sandbox/benchmark/Axioms/PHI002+0.ax', god)).
% 0.48/0.66 fof(c147,plain,(![X]:((~god(X)|(being(X)&absolutelyInfinite(X)))&((~being(X)|~absolutelyInfinite(X))|god(X)))),inference(fof_nnf,[status(thm)],[god])).
% 0.48/0.66 fof(c148,plain,((![X]:(~god(X)|(being(X)&absolutelyInfinite(X))))&(![X]:((~being(X)|~absolutelyInfinite(X))|god(X)))),inference(shift_quantors,[status(thm)],[c147])).
% 0.48/0.66 fof(c150,plain,(![X43]:(![X44]:((~god(X43)|(being(X43)&absolutelyInfinite(X43)))&((~being(X44)|~absolutelyInfinite(X44))|god(X44))))),inference(shift_quantors,[status(thm)],[fof(c149,plain,((![X43]:(~god(X43)|(being(X43)&absolutelyInfinite(X43))))&(![X44]:((~being(X44)|~absolutelyInfinite(X44))|god(X44)))),inference(variable_rename,[status(thm)],[c148])).])).
% 0.48/0.66 fof(c151,plain,(![X43]:(![X44]:(((~god(X43)|being(X43))&(~god(X43)|absolutelyInfinite(X43)))&((~being(X44)|~absolutelyInfinite(X44))|god(X44))))),inference(distribute,[status(thm)],[c150])).
% 0.48/0.66 cnf(c154,plain,~being(X145)|~absolutelyInfinite(X145)|god(X145),inference(split_conjunct,[status(thm)],[c151])).
% 0.48/0.66 cnf(c124,plain,~necessary(X143)|isMethodAction(X144)|isMethodExistence(X144),inference(split_conjunct,[status(thm)],[c120])).
% 0.48/0.66 cnf(c5,axiom,X138!=X137|X136!=X139|~sameKind(X138,X136)|sameKind(X137,X139),theory(equality)).
% 0.48/0.66 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/theBenchmark.p', have_nothing_in_common)).
% 0.48/0.66 fof(c71,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.48/0.66 fof(c72,plain,(![X]:(![Y]:(~haveNothingInCommon(X,Y)|(((~canBeUnderstoodInTermsOf(X,Y)&~canBeUnderstoodInTermsOf(Y,X))&~conceptionInvolves(X,Y))&~conceptionInvolves(Y,X))))),inference(fof_nnf,[status(thm)],[c71])).
% 0.48/0.66 fof(c73,plain,(![X10]:(![X11]:(~haveNothingInCommon(X10,X11)|(((~canBeUnderstoodInTermsOf(X10,X11)&~canBeUnderstoodInTermsOf(X11,X10))&~conceptionInvolves(X10,X11))&~conceptionInvolves(X11,X10))))),inference(variable_rename,[status(thm)],[c72])).
% 0.48/0.66 fof(c74,plain,(![X10]:(![X11]:((((~haveNothingInCommon(X10,X11)|~canBeUnderstoodInTermsOf(X10,X11))&(~haveNothingInCommon(X10,X11)|~canBeUnderstoodInTermsOf(X11,X10)))&(~haveNothingInCommon(X10,X11)|~conceptionInvolves(X10,X11)))&(~haveNothingInCommon(X10,X11)|~conceptionInvolves(X11,X10))))),inference(distribute,[status(thm)],[c73])).
% 0.48/0.66 cnf(c78,plain,~haveNothingInCommon(X129,X128)|~conceptionInvolves(X128,X129),inference(split_conjunct,[status(thm)],[c74])).
% 0.48/0.66 cnf(c4,axiom,X126!=X125|X124!=X127|~canBeLimitedBy(X126,X124)|canBeLimitedBy(X125,X127),theory(equality)).
% 0.48/0.66 cnf(c77,plain,~haveNothingInCommon(X123,X122)|~conceptionInvolves(X123,X122),inference(split_conjunct,[status(thm)],[c74])).
% 0.48/0.66 cnf(c76,plain,~haveNothingInCommon(X121,X120)|~canBeUnderstoodInTermsOf(X120,X121),inference(split_conjunct,[status(thm)],[c74])).
% 0.48/0.66 cnf(c75,plain,~haveNothingInCommon(X119,X118)|~canBeUnderstoodInTermsOf(X119,X118),inference(split_conjunct,[status(thm)],[c74])).
% 0.48/0.66 cnf(c186,plain,~finiteAfterItsKind(X116)|sameKind(X116,X117),inference(split_conjunct,[status(thm)],[c184])).
% 0.48/0.66 cnf(c3,axiom,X114!=X113|~finiteAfterItsKind(X114)|finiteAfterItsKind(X113),theory(equality)).
% 0.48/0.66 cnf(c185,plain,~finiteAfterItsKind(X111)|canBeLimitedBy(X111,X112),inference(split_conjunct,[status(thm)],[c184])).
% 0.48/0.66 cnf(c123,plain,~necessary(X109)|determinedByDefiniteMethod(X109,X110),inference(split_conjunct,[status(thm)],[c120])).
% 0.48/0.66 cnf(c122,plain,~necessary(X107)|determinedByFixedMethod(X107,X108),inference(split_conjunct,[status(thm)],[c120])).
% 0.48/0.66 cnf(c121,plain,~necessary(X105)|externalTo(X106,X105),inference(split_conjunct,[status(thm)],[c120])).
% 0.48/0.66 cnf(c2,axiom,X103!=X102|~natureConcOnlyByExistence(X103)|natureConcOnlyByExistence(X102),theory(equality)).
% 0.48/0.66 fof(definite_cause,axiom,(![X]:(![Y]:(definiteCause(X)=>(effectNecessarilyFollowsFrom(Y,X)&((~definiteCause(X))=>(~effectNecessarilyFollowsFrom(Y,X))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', definite_cause)).
% 0.48/0.66 fof(c85,plain,(![X]:(![Y]:(definiteCause(X)=>(effectNecessarilyFollowsFrom(Y,X)&(~definiteCause(X)=>~effectNecessarilyFollowsFrom(Y,X)))))),inference(fof_simplification,[status(thm)],[definite_cause])).
% 0.48/0.66 fof(c86,plain,(![X]:(![Y]:(~definiteCause(X)|(effectNecessarilyFollowsFrom(Y,X)&(definiteCause(X)|~effectNecessarilyFollowsFrom(Y,X)))))),inference(fof_nnf,[status(thm)],[c85])).
% 0.48/0.66 fof(c87,plain,(![X]:(~definiteCause(X)|((![Y]:effectNecessarilyFollowsFrom(Y,X))&(definiteCause(X)|(![Y]:~effectNecessarilyFollowsFrom(Y,X)))))),inference(shift_quantors,[status(thm)],[c86])).
% 0.48/0.66 fof(c89,plain,(![X16]:(![X17]:(![X18]:(~definiteCause(X16)|(effectNecessarilyFollowsFrom(X17,X16)&(definiteCause(X16)|~effectNecessarilyFollowsFrom(X18,X16))))))),inference(shift_quantors,[status(thm)],[fof(c88,plain,(![X16]:(~definiteCause(X16)|((![X17]:effectNecessarilyFollowsFrom(X17,X16))&(definiteCause(X16)|(![X18]:~effectNecessarilyFollowsFrom(X18,X16)))))),inference(variable_rename,[status(thm)],[c87])).])).
% 0.48/0.66 fof(c90,plain,(![X16]:(![X17]:(![X18]:((~definiteCause(X16)|effectNecessarilyFollowsFrom(X17,X16))&(~definiteCause(X16)|(definiteCause(X16)|~effectNecessarilyFollowsFrom(X18,X16))))))),inference(distribute,[status(thm)],[c89])).
% 0.48/0.66 cnf(c91,plain,~definiteCause(X100)|effectNecessarilyFollowsFrom(X101,X100),inference(split_conjunct,[status(thm)],[c90])).
% 0.48/0.66 fof(knowledge_of_effect,axiom,(![X]:(![Y]:(knowledgeOfEffect(X,Y)<=>knowledgeOfACause(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', knowledge_of_effect)).
% 0.48/0.66 fof(c79,plain,(![X]:(![Y]:((~knowledgeOfEffect(X,Y)|knowledgeOfACause(X))&(~knowledgeOfACause(X)|knowledgeOfEffect(X,Y))))),inference(fof_nnf,[status(thm)],[knowledge_of_effect])).
% 0.48/0.66 fof(c80,plain,((![X]:((![Y]:~knowledgeOfEffect(X,Y))|knowledgeOfACause(X)))&(![X]:(~knowledgeOfACause(X)|(![Y]:knowledgeOfEffect(X,Y))))),inference(shift_quantors,[status(thm)],[c79])).
% 0.48/0.66 fof(c82,plain,(![X12]:(![X13]:(![X14]:(![X15]:((~knowledgeOfEffect(X12,X13)|knowledgeOfACause(X12))&(~knowledgeOfACause(X14)|knowledgeOfEffect(X14,X15))))))),inference(shift_quantors,[status(thm)],[fof(c81,plain,((![X12]:((![X13]:~knowledgeOfEffect(X12,X13))|knowledgeOfACause(X12)))&(![X14]:(~knowledgeOfACause(X14)|(![X15]:knowledgeOfEffect(X14,X15))))),inference(variable_rename,[status(thm)],[c80])).])).
% 0.48/0.66 cnf(c84,plain,~knowledgeOfACause(X99)|knowledgeOfEffect(X99,X98),inference(split_conjunct,[status(thm)],[c82])).
% 0.48/0.66 cnf(c83,plain,~knowledgeOfEffect(X97,X96)|knowledgeOfACause(X97),inference(split_conjunct,[status(thm)],[c82])).
% 0.48/0.66 cnf(c69,plain,~trueIdea(X94)|correspondWith(X94,X95),inference(split_conjunct,[status(thm)],[c68])).
% 0.48/0.66 cnf(c1,axiom,X92!=X91|~essenceInvExistence(X92)|essenceInvExistence(X91),theory(equality)).
% 0.48/0.66 cnf(c194,plain,~selfCaused(X89)|natureConcOnlyByExistence(X89),inference(split_conjunct,[status(thm)],[c192])).
% 0.48/0.66 cnf(c178,plain,~substance(X87)|conceivedThruItself(X87),inference(split_conjunct,[status(thm)],[c176])).
% 0.48/0.66 cnf(c0,axiom,X85!=X84|~selfCaused(X85)|selfCaused(X84),theory(equality)).
% 0.48/0.66 fof(attribute,axiom,(![X]:(attribute(X)<=>intPercAsConstEssSub(X))),file('/export/starexec/sandbox/benchmark/Axioms/PHI002+0.ax', attribute)).
% 0.48/0.66 fof(c166,plain,(![X]:((~attribute(X)|intPercAsConstEssSub(X))&(~intPercAsConstEssSub(X)|attribute(X)))),inference(fof_nnf,[status(thm)],[attribute])).
% 0.48/0.66 fof(c167,plain,((![X]:(~attribute(X)|intPercAsConstEssSub(X)))&(![X]:(~intPercAsConstEssSub(X)|attribute(X)))),inference(shift_quantors,[status(thm)],[c166])).
% 0.48/0.66 fof(c169,plain,(![X53]:(![X54]:((~attribute(X53)|intPercAsConstEssSub(X53))&(~intPercAsConstEssSub(X54)|attribute(X54))))),inference(shift_quantors,[status(thm)],[fof(c168,plain,((![X53]:(~attribute(X53)|intPercAsConstEssSub(X53)))&(![X54]:(~intPercAsConstEssSub(X54)|attribute(X54)))),inference(variable_rename,[status(thm)],[c167])).])).
% 0.48/0.66 cnf(c171,plain,~intPercAsConstEssSub(X83)|attribute(X83),inference(split_conjunct,[status(thm)],[c169])).
% 0.48/0.66 cnf(c170,plain,~attribute(X82)|intPercAsConstEssSub(X82),inference(split_conjunct,[status(thm)],[c169])).
% 0.48/0.66 cnf(c153,plain,~god(X81)|absolutelyInfinite(X81),inference(split_conjunct,[status(thm)],[c151])).
% 0.48/0.66 cnf(c152,plain,~god(X80)|being(X80),inference(split_conjunct,[status(thm)],[c151])).
% 0.48/0.66 cnf(c142,plain,~absolutelyInfinite(X79)|constInInfAttributes(X79),inference(split_conjunct,[status(thm)],[c140])).
% 0.48/0.66 cnf(transitivity,axiom,X78!=X76|X76!=X77|X78=X77,theory(equality)).
% 0.48/0.66 cnf(c141,plain,~absolutelyInfinite(X75)|substance(X75),inference(split_conjunct,[status(thm)],[c140])).
% 0.48/0.66 cnf(c132,plain,~free(X74)|existsOnlyByNecessityOfOwnNature(X74),inference(split_conjunct,[status(thm)],[c131])).
% 0.48/0.66 fof(eternity,axiom,(![X]:(eternity(X)<=>existConcFollowFromDefEternal(X))),file('/export/starexec/sandbox/benchmark/Axioms/PHI002+0.ax', eternity)).
% 0.48/0.66 fof(c110,plain,(![X]:((~eternity(X)|existConcFollowFromDefEternal(X))&(~existConcFollowFromDefEternal(X)|eternity(X)))),inference(fof_nnf,[status(thm)],[eternity])).
% 0.48/0.66 fof(c111,plain,((![X]:(~eternity(X)|existConcFollowFromDefEternal(X)))&(![X]:(~existConcFollowFromDefEternal(X)|eternity(X)))),inference(shift_quantors,[status(thm)],[c110])).
% 0.48/0.66 fof(c113,plain,(![X24]:(![X25]:((~eternity(X24)|existConcFollowFromDefEternal(X24))&(~existConcFollowFromDefEternal(X25)|eternity(X25))))),inference(shift_quantors,[status(thm)],[fof(c112,plain,((![X24]:(~eternity(X24)|existConcFollowFromDefEternal(X24)))&(![X25]:(~existConcFollowFromDefEternal(X25)|eternity(X25)))),inference(variable_rename,[status(thm)],[c111])).])).
% 0.48/0.66 cnf(c115,plain,~existConcFollowFromDefEternal(X73)|eternity(X73),inference(split_conjunct,[status(thm)],[c113])).
% 0.48/0.66 cnf(c114,plain,~eternity(X72)|existConcFollowFromDefEternal(X72),inference(split_conjunct,[status(thm)],[c113])).
% 0.48/0.66 cnf(symmetry,axiom,X70!=X69|X69=X70,theory(equality)).
% 0.48/0.66 fof(can_be_conceived_as_non_existing,axiom,(![X]:(canBeConceivedAsNonExisting(X)=>(~essenceInvExistence(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', can_be_conceived_as_non_existing)).
% 0.48/0.66 fof(c60,plain,(![X]:(canBeConceivedAsNonExisting(X)=>~essenceInvExistence(X))),inference(fof_simplification,[status(thm)],[can_be_conceived_as_non_existing])).
% 0.48/0.66 fof(c61,plain,(![X]:(~canBeConceivedAsNonExisting(X)|~essenceInvExistence(X))),inference(fof_nnf,[status(thm)],[c60])).
% 0.48/0.66 fof(c62,plain,(![X6]:(~canBeConceivedAsNonExisting(X6)|~essenceInvExistence(X6))),inference(variable_rename,[status(thm)],[c61])).
% 0.48/0.66 cnf(c63,plain,~canBeConceivedAsNonExisting(X68)|~essenceInvExistence(X68),inference(split_conjunct,[status(thm)],[c62])).
% 0.48/0.66 % SZS output end Saturation
% 0.48/0.66
% 0.48/0.66 % Initial clauses : 110
% 0.48/0.66 % Processed clauses : 132
% 0.48/0.66 % Factors computed : 6
% 0.48/0.66 % Resolvents computed: 99
% 0.48/0.66 % Tautologies deleted: 49
% 0.48/0.66 % Forward subsumed : 34
% 0.48/0.66 % Backward subsumed : 19
% 0.48/0.66 % -------- CPU Time ---------
% 0.48/0.66 % User time : 0.278 s
% 0.48/0.66 % System time : 0.021 s
% 0.48/0.66 % Total time : 0.299 s
%------------------------------------------------------------------------------