%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PHI025+1 : TPTP v8.1.2. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:37:18 EDT 2024
% Result : Satisfiable 0.49s 0.68s
% Output : Saturation 0.49s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.14 % Problem : PHI025+1 : TPTP v8.1.2. Released v7.4.0.
% 0.12/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.16/0.35 % Computer : n004.cluster.edu
% 0.16/0.35 % Model : x86_64 x86_64
% 0.16/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.35 % Memory : 8042.1875MB
% 0.16/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.35 % CPULimit : 300
% 0.16/0.35 % WCLimit : 300
% 0.16/0.36 % DateTime : Wed May 8 22:28:53 EDT 2024
% 0.16/0.36 % CPUTime :
% 0.49/0.68 % Version: 1.5
% 0.49/0.68 % SZS status Satisfiable
% 0.49/0.68 % SZS output start Saturation
% 0.49/0.68 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.49/0.68 fof(c103,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.49/0.68 fof(c104,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)],[c103])).
% 0.49/0.68 fof(c106,plain,(![X25]:(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:((~necessary(X25)|(((externalTo(X26,X25)&determinedByFixedMethod(X25,X27))&determinedByDefiniteMethod(X25,X28))&(isMethodAction(X29)|isMethodExistence(X29))))&((((~externalTo(X31,X30)|~determinedByFixedMethod(X30,X31))|~determinedByDefiniteMethod(X30,X31))|(~isMethodAction(X31)&~isMethodExistence(X31)))|necessary(X30)))))))))),inference(shift_quantors,[status(thm)],[fof(c105,plain,((![X25]:(~necessary(X25)|((((![X26]:externalTo(X26,X25))&(![X27]:determinedByFixedMethod(X25,X27)))&(![X28]:determinedByDefiniteMethod(X25,X28)))&(![X29]:(isMethodAction(X29)|isMethodExistence(X29))))))&(![X30]:((![X31]:(((~externalTo(X31,X30)|~determinedByFixedMethod(X30,X31))|~determinedByDefiniteMethod(X30,X31))|(~isMethodAction(X31)&~isMethodExistence(X31))))|necessary(X30)))),inference(variable_rename,[status(thm)],[c104])).])).
% 0.49/0.68 fof(c107,plain,(![X25]:(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:(((((~necessary(X25)|externalTo(X26,X25))&(~necessary(X25)|determinedByFixedMethod(X25,X27)))&(~necessary(X25)|determinedByDefiniteMethod(X25,X28)))&(~necessary(X25)|(isMethodAction(X29)|isMethodExistence(X29))))&(((((~externalTo(X31,X30)|~determinedByFixedMethod(X30,X31))|~determinedByDefiniteMethod(X30,X31))|~isMethodAction(X31))|necessary(X30))&((((~externalTo(X31,X30)|~determinedByFixedMethod(X30,X31))|~determinedByDefiniteMethod(X30,X31))|~isMethodExistence(X31))|necessary(X30))))))))))),inference(distribute,[status(thm)],[c106])).
% 0.49/0.68 cnf(c113,plain,~externalTo(X339,X338)|~determinedByFixedMethod(X338,X339)|~determinedByDefiniteMethod(X338,X339)|~isMethodExistence(X339)|necessary(X338),inference(split_conjunct,[status(thm)],[c107])).
% 0.49/0.68 cnf(c112,plain,~externalTo(X337,X336)|~determinedByFixedMethod(X336,X337)|~determinedByDefiniteMethod(X336,X337)|~isMethodAction(X337)|necessary(X336),inference(split_conjunct,[status(thm)],[c107])).
% 0.49/0.68 cnf(c45,axiom,X332!=X333|X334!=X335|~objectOf(X332,X334)|objectOf(X333,X335),theory(equality)).
% 0.49/0.68 cnf(c44,axiom,X328!=X329|X330!=X331|~ideateOf(X328,X330)|ideateOf(X329,X331),theory(equality)).
% 0.49/0.68 cnf(c43,axiom,X324!=X325|X326!=X327|~correspondWith(X324,X326)|correspondWith(X325,X327),theory(equality)).
% 0.49/0.68 cnf(c41,axiom,X320!=X321|X322!=X323|~canBeUnderstoodInTermsOf(X320,X322)|canBeUnderstoodInTermsOf(X321,X323),theory(equality)).
% 0.49/0.68 cnf(c40,axiom,X316!=X317|X318!=X319|~conceptionInvolves(X316,X318)|conceptionInvolves(X317,X319),theory(equality)).
% 0.49/0.68 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.49/0.68 fof(c123,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.49/0.68 fof(c124,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)],[c123])).
% 0.49/0.68 fof(c126,plain,(![X37]:(![X38]:(![X39]:(![X40]:(![X41]:((~absolutelyInfinite(X37)|((substance(X37)&constInInfAttributes(X37))&(~attributeOf(X38,X37)|(expressesEternalEssentiality(X38)&expressesInfiniteEssentiality(X38)))))&(((~substance(X39)|~constInInfAttributes(X39))|(attributeOf(X40,X39)&(~expressesEternalEssentiality(X41)|~expressesInfiniteEssentiality(X41))))|absolutelyInfinite(X39)))))))),inference(shift_quantors,[status(thm)],[fof(c125,plain,((![X37]:(~absolutelyInfinite(X37)|((substance(X37)&constInInfAttributes(X37))&(![X38]:(~attributeOf(X38,X37)|(expressesEternalEssentiality(X38)&expressesInfiniteEssentiality(X38)))))))&(![X39]:(((~substance(X39)|~constInInfAttributes(X39))|((![X40]:attributeOf(X40,X39))&(![X41]:(~expressesEternalEssentiality(X41)|~expressesInfiniteEssentiality(X41)))))|absolutelyInfinite(X39)))),inference(variable_rename,[status(thm)],[c124])).])).
% 0.49/0.68 fof(c127,plain,(![X37]:(![X38]:(![X39]:(![X40]:(![X41]:((((~absolutelyInfinite(X37)|substance(X37))&(~absolutelyInfinite(X37)|constInInfAttributes(X37)))&((~absolutelyInfinite(X37)|(~attributeOf(X38,X37)|expressesEternalEssentiality(X38)))&(~absolutelyInfinite(X37)|(~attributeOf(X38,X37)|expressesInfiniteEssentiality(X38)))))&((((~substance(X39)|~constInInfAttributes(X39))|attributeOf(X40,X39))|absolutelyInfinite(X39))&(((~substance(X39)|~constInInfAttributes(X39))|(~expressesEternalEssentiality(X41)|~expressesInfiniteEssentiality(X41)))|absolutelyInfinite(X39))))))))),inference(distribute,[status(thm)],[c126])).
% 0.49/0.68 cnf(c133,plain,~substance(X314)|~constInInfAttributes(X314)|~expressesEternalEssentiality(X315)|~expressesInfiniteEssentiality(X315)|absolutelyInfinite(X314),inference(split_conjunct,[status(thm)],[c127])).
% 0.49/0.68 cnf(c132,plain,~substance(X312)|~constInInfAttributes(X312)|attributeOf(X313,X312)|absolutelyInfinite(X312),inference(split_conjunct,[status(thm)],[c127])).
% 0.49/0.68 cnf(reflexivity,axiom,X63=X63,theory(equality)).
% 0.49/0.68 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.49/0.68 fof(c80,plain,(![X]:(![Y]:(~conceivedThru(X,X)=>(conceivedThru(X,Y)&X!=Y)))),inference(fof_simplification,[status(thm)],[conceived_through])).
% 0.49/0.68 fof(c81,plain,(![X]:(![Y]:(conceivedThru(X,X)|(conceivedThru(X,Y)&X!=Y)))),inference(fof_nnf,[status(thm)],[c80])).
% 0.49/0.68 fof(c82,plain,(![X]:(conceivedThru(X,X)|((![Y]:conceivedThru(X,Y))&(![Y]:X!=Y)))),inference(shift_quantors,[status(thm)],[c81])).
% 0.49/0.68 fof(c84,plain,(![X15]:(![X16]:(![X17]:(conceivedThru(X15,X15)|(conceivedThru(X15,X16)&X15!=X17))))),inference(shift_quantors,[status(thm)],[fof(c83,plain,(![X15]:(conceivedThru(X15,X15)|((![X16]:conceivedThru(X15,X16))&(![X17]:X15!=X17)))),inference(variable_rename,[status(thm)],[c82])).])).
% 0.49/0.68 fof(c85,plain,(![X15]:(![X16]:(![X17]:((conceivedThru(X15,X15)|conceivedThru(X15,X16))&(conceivedThru(X15,X15)|X15!=X17))))),inference(distribute,[status(thm)],[c84])).
% 0.49/0.68 cnf(c86,plain,conceivedThru(X124,X124)|conceivedThru(X124,X123),inference(split_conjunct,[status(thm)],[c85])).
% 0.49/0.68 cnf(c190,plain,conceivedThru(X129,X129),inference(factor,[status(thm)],[c86])).
% 0.49/0.68 cnf(c14,axiom,X188!=X189|X190!=X191|~conceivedThru(X188,X190)|conceivedThru(X189,X191),theory(equality)).
% 0.49/0.68 cnf(c203,plain,X300!=X302|X300!=X301|conceivedThru(X302,X301),inference(resolution,[status(thm)],[c14, c190])).
% 0.49/0.68 cnf(c219,plain,X309!=X310|conceivedThru(X310,X309),inference(resolution,[status(thm)],[c203, reflexivity])).
% 0.49/0.68 cnf(c39,axiom,X305!=X306|X307!=X308|~haveNothingInCommon(X305,X307)|haveNothingInCommon(X306,X308),theory(equality)).
% 0.49/0.68 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.49/0.68 fof(c167,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.49/0.68 fof(c168,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)],[c167])).
% 0.49/0.68 fof(c170,plain,(![X56]:(![X57]:(![X58]:(![X59]:(![X60]:((~finiteAfterItsKind(X56)|(canBeLimitedBy(X56,X57)&sameKind(X56,X58)))&((~canBeLimitedBy(X59,X60)|~sameKind(X59,X60))|finiteAfterItsKind(X59)))))))),inference(shift_quantors,[status(thm)],[fof(c169,plain,((![X56]:(~finiteAfterItsKind(X56)|((![X57]:canBeLimitedBy(X56,X57))&(![X58]:sameKind(X56,X58)))))&(![X59]:((![X60]:(~canBeLimitedBy(X59,X60)|~sameKind(X59,X60)))|finiteAfterItsKind(X59)))),inference(variable_rename,[status(thm)],[c168])).])).
% 0.49/0.68 fof(c171,plain,(![X56]:(![X57]:(![X58]:(![X59]:(![X60]:(((~finiteAfterItsKind(X56)|canBeLimitedBy(X56,X57))&(~finiteAfterItsKind(X56)|sameKind(X56,X58)))&((~canBeLimitedBy(X59,X60)|~sameKind(X59,X60))|finiteAfterItsKind(X59)))))))),inference(distribute,[status(thm)],[c170])).
% 0.49/0.68 cnf(c174,plain,~canBeLimitedBy(X298,X299)|~sameKind(X298,X299)|finiteAfterItsKind(X298),inference(split_conjunct,[status(thm)],[c171])).
% 0.49/0.68 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.49/0.68 fof(c142,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.49/0.68 fof(c143,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)],[c142])).
% 0.49/0.68 fof(c145,plain,(![X44]:(![X45]:(![X46]:(![X47]:(![X48]:(![X49]:(![X50]:(![X51]:((~mode(X44)|((modification(X44,X45)&substance(X46))|(existsIn(X44,X47)&conceivedThru(X44,X48))))&(((~modification(X49,X50)|~substance(X50))&(~existsIn(X49,X51)|~conceivedThru(X49,X51)))|mode(X49))))))))))),inference(shift_quantors,[status(thm)],[fof(c144,plain,((![X44]:(~mode(X44)|(((![X45]:modification(X44,X45))&(![X46]:substance(X46)))|((![X47]:existsIn(X44,X47))&(![X48]:conceivedThru(X44,X48))))))&(![X49]:(((![X50]:(~modification(X49,X50)|~substance(X50)))&(![X51]:(~existsIn(X49,X51)|~conceivedThru(X49,X51))))|mode(X49)))),inference(variable_rename,[status(thm)],[c143])).])).
% 0.49/0.68 fof(c146,plain,(![X44]:(![X45]:(![X46]:(![X47]:(![X48]:(![X49]:(![X50]:(![X51]:((((~mode(X44)|(modification(X44,X45)|existsIn(X44,X47)))&(~mode(X44)|(modification(X44,X45)|conceivedThru(X44,X48))))&((~mode(X44)|(substance(X46)|existsIn(X44,X47)))&(~mode(X44)|(substance(X46)|conceivedThru(X44,X48)))))&(((~modification(X49,X50)|~substance(X50))|mode(X49))&((~existsIn(X49,X51)|~conceivedThru(X49,X51))|mode(X49)))))))))))),inference(distribute,[status(thm)],[c145])).
% 0.49/0.68 cnf(c152,plain,~existsIn(X295,X296)|~conceivedThru(X295,X296)|mode(X295),inference(split_conjunct,[status(thm)],[c146])).
% 0.49/0.68 cnf(c217,plain,~existsIn(X297,X297)|mode(X297),inference(resolution,[status(thm)],[c152, c190])).
% 0.49/0.68 cnf(c37,axiom,X291!=X292|X293!=X294|~knowledgeOfEffect(X291,X293)|knowledgeOfEffect(X292,X294),theory(equality)).
% 0.49/0.68 cnf(c148,plain,~mode(X289)|modification(X289,X288)|conceivedThru(X289,X290),inference(split_conjunct,[status(thm)],[c146])).
% 0.49/0.68 cnf(c147,plain,~mode(X286)|modification(X286,X285)|existsIn(X286,X287),inference(split_conjunct,[status(thm)],[c146])).
% 0.49/0.68 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.49/0.68 fof(c114,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.49/0.68 fof(c115,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)],[c114])).
% 0.49/0.68 fof(c117,plain,(![X32]:(![X33]:(![X34]:(![X35]:(![X36]:((~free(X32)|(existsOnlyByNecessityOfOwnNature(X32)&(~actionOf(X33,X32)|determinedByItselfAlone(X33,X32))))&((~existsOnlyByNecessityOfOwnNature(X34)|(actionOf(X35,X34)&~determinedByItselfAlone(X36,X34)))|free(X34)))))))),inference(shift_quantors,[status(thm)],[fof(c116,plain,((![X32]:(~free(X32)|(existsOnlyByNecessityOfOwnNature(X32)&(![X33]:(~actionOf(X33,X32)|determinedByItselfAlone(X33,X32))))))&(![X34]:((~existsOnlyByNecessityOfOwnNature(X34)|((![X35]:actionOf(X35,X34))&(![X36]:~determinedByItselfAlone(X36,X34))))|free(X34)))),inference(variable_rename,[status(thm)],[c115])).])).
% 0.49/0.68 fof(c118,plain,(![X32]:(![X33]:(![X34]:(![X35]:(![X36]:(((~free(X32)|existsOnlyByNecessityOfOwnNature(X32))&(~free(X32)|(~actionOf(X33,X32)|determinedByItselfAlone(X33,X32))))&(((~existsOnlyByNecessityOfOwnNature(X34)|actionOf(X35,X34))|free(X34))&((~existsOnlyByNecessityOfOwnNature(X34)|~determinedByItselfAlone(X36,X34))|free(X34))))))))),inference(distribute,[status(thm)],[c117])).
% 0.49/0.68 cnf(c120,plain,~free(X284)|~actionOf(X283,X284)|determinedByItselfAlone(X283,X284),inference(split_conjunct,[status(thm)],[c118])).
% 0.49/0.68 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.49/0.68 fof(c88,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.49/0.68 fof(c89,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)],[c88])).
% 0.49/0.68 fof(c91,plain,(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:((~exists(X18)|(existsIn(X18,X18)|(existsIn(X18,X19)&X18!=X20)))&((~existsIn(X21,X21)&(~existsIn(X21,X22)|X21=X22))|exists(X21)))))))),inference(shift_quantors,[status(thm)],[fof(c90,plain,((![X18]:(~exists(X18)|(existsIn(X18,X18)|((![X19]:existsIn(X18,X19))&(![X20]:X18!=X20)))))&(![X21]:((~existsIn(X21,X21)&(![X22]:(~existsIn(X21,X22)|X21=X22)))|exists(X21)))),inference(variable_rename,[status(thm)],[c89])).])).
% 0.49/0.68 fof(c92,plain,(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(((~exists(X18)|(existsIn(X18,X18)|existsIn(X18,X19)))&(~exists(X18)|(existsIn(X18,X18)|X18!=X20)))&((~existsIn(X21,X21)|exists(X21))&((~existsIn(X21,X22)|X21=X22)|exists(X21))))))))),inference(distribute,[status(thm)],[c91])).
% 0.49/0.68 cnf(c96,plain,~existsIn(X281,X282)|X281=X282|exists(X281),inference(split_conjunct,[status(thm)],[c92])).
% 0.49/0.68 cnf(c94,plain,~exists(X275)|existsIn(X275,X275)|X275!=X274,inference(split_conjunct,[status(thm)],[c92])).
% 0.49/0.68 cnf(c216,plain,~exists(X280)|existsIn(X280,X280),inference(resolution,[status(thm)],[c94, reflexivity])).
% 0.49/0.68 cnf(c36,axiom,X276!=X277|X278!=X279|~effectNecessarilyFollowsFrom(X276,X278)|effectNecessarilyFollowsFrom(X277,X279),theory(equality)).
% 0.49/0.68 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.49/0.68 fof(c51,plain,(![X]:(![Y]:(~trueIdea(X)|(correspondWith(X,Y)&(ideateOf(Y,X)|objectOf(Y,X)))))),inference(fof_nnf,[status(thm)],[true_idea])).
% 0.49/0.68 fof(c52,plain,(![X]:(~trueIdea(X)|((![Y]:correspondWith(X,Y))&(![Y]:(ideateOf(Y,X)|objectOf(Y,X)))))),inference(shift_quantors,[status(thm)],[c51])).
% 0.49/0.68 fof(c54,plain,(![X3]:(![X4]:(![X5]:(~trueIdea(X3)|(correspondWith(X3,X4)&(ideateOf(X5,X3)|objectOf(X5,X3))))))),inference(shift_quantors,[status(thm)],[fof(c53,plain,(![X3]:(~trueIdea(X3)|((![X4]:correspondWith(X3,X4))&(![X5]:(ideateOf(X5,X3)|objectOf(X5,X3)))))),inference(variable_rename,[status(thm)],[c52])).])).
% 0.49/0.68 fof(c55,plain,(![X3]:(![X4]:(![X5]:((~trueIdea(X3)|correspondWith(X3,X4))&(~trueIdea(X3)|(ideateOf(X5,X3)|objectOf(X5,X3))))))),inference(distribute,[status(thm)],[c54])).
% 0.49/0.68 cnf(c57,plain,~trueIdea(X270)|ideateOf(X271,X270)|objectOf(X271,X270),inference(split_conjunct,[status(thm)],[c55])).
% 0.49/0.68 cnf(c151,plain,~modification(X269,X268)|~substance(X268)|mode(X269),inference(split_conjunct,[status(thm)],[c146])).
% 0.49/0.68 cnf(c150,plain,~mode(X265)|substance(X267)|conceivedThru(X265,X266),inference(split_conjunct,[status(thm)],[c146])).
% 0.49/0.68 cnf(c31,axiom,X261!=X262|X263!=X264|~determinedByFixedMethod(X261,X263)|determinedByFixedMethod(X262,X264),theory(equality)).
% 0.49/0.68 cnf(c149,plain,~mode(X258)|substance(X260)|existsIn(X258,X259),inference(split_conjunct,[status(thm)],[c146])).
% 0.49/0.68 cnf(c131,plain,~absolutelyInfinite(X257)|~attributeOf(X256,X257)|expressesInfiniteEssentiality(X256),inference(split_conjunct,[status(thm)],[c127])).
% 0.49/0.68 cnf(c130,plain,~absolutelyInfinite(X255)|~attributeOf(X254,X255)|expressesEternalEssentiality(X254),inference(split_conjunct,[status(thm)],[c127])).
% 0.49/0.68 cnf(c122,plain,~existsOnlyByNecessityOfOwnNature(X253)|~determinedByItselfAlone(X252,X253)|free(X253),inference(split_conjunct,[status(thm)],[c118])).
% 0.49/0.68 cnf(c121,plain,~existsOnlyByNecessityOfOwnNature(X251)|actionOf(X250,X251)|free(X251),inference(split_conjunct,[status(thm)],[c118])).
% 0.49/0.68 cnf(c30,axiom,X246!=X247|X248!=X249|~externalTo(X246,X248)|externalTo(X247,X249),theory(equality)).
% 0.49/0.68 cnf(c46,axiom,X241!=X242|~canBeConceivedAsNonExisting(X241)|canBeConceivedAsNonExisting(X242),theory(equality)).
% 0.49/0.68 cnf(c42,axiom,X238!=X239|~trueIdea(X238)|trueIdea(X239),theory(equality)).
% 0.49/0.68 cnf(c27,axiom,X234!=X235|X236!=X237|~determinedByDefiniteMethod(X234,X236)|determinedByDefiniteMethod(X235,X237),theory(equality)).
% 0.49/0.68 cnf(c38,axiom,X231!=X232|~knowledgeOfACause(X231)|knowledgeOfACause(X232),theory(equality)).
% 0.49/0.68 cnf(c35,axiom,X228!=X229|~definiteCause(X228)|definiteCause(X229),theory(equality)).
% 0.49/0.68 cnf(c25,axiom,X223!=X224|X225!=X226|~determinedByItselfAlone(X223,X225)|determinedByItselfAlone(X224,X226),theory(equality)).
% 0.49/0.68 cnf(c34,axiom,X221!=X222|~exists(X221)|exists(X222),theory(equality)).
% 0.49/0.68 cnf(c33,axiom,X218!=X219|~existConcFollowFromDefEternal(X218)|existConcFollowFromDefEternal(X219),theory(equality)).
% 0.49/0.68 cnf(c32,axiom,X215!=X216|~eternity(X215)|eternity(X216),theory(equality)).
% 0.49/0.68 cnf(c24,axiom,X211!=X212|X213!=X214|~actionOf(X211,X213)|actionOf(X212,X214),theory(equality)).
% 0.49/0.68 cnf(c29,axiom,X208!=X209|~isMethodExistence(X208)|isMethodExistence(X209),theory(equality)).
% 0.49/0.68 cnf(c28,axiom,X205!=X206|~isMethodAction(X205)|isMethodAction(X206),theory(equality)).
% 0.49/0.68 cnf(c19,axiom,X200!=X201|X202!=X203|~attributeOf(X200,X202)|attributeOf(X201,X203),theory(equality)).
% 0.49/0.68 cnf(c26,axiom,X198!=X199|~necessary(X198)|necessary(X199),theory(equality)).
% 0.49/0.68 cnf(c23,axiom,X195!=X196|~existsOnlyByNecessityOfOwnNature(X195)|existsOnlyByNecessityOfOwnNature(X196),theory(equality)).
% 0.49/0.68 cnf(c22,axiom,X192!=X193|~free(X192)|free(X193),theory(equality)).
% 0.49/0.68 cnf(c21,axiom,X185!=X186|~expressesInfiniteEssentiality(X185)|expressesInfiniteEssentiality(X186),theory(equality)).
% 0.49/0.68 cnf(c20,axiom,X182!=X183|~expressesEternalEssentiality(X182)|expressesEternalEssentiality(X183),theory(equality)).
% 0.49/0.68 cnf(c13,axiom,X177!=X178|X179!=X180|~existsIn(X177,X179)|existsIn(X178,X180),theory(equality)).
% 0.49/0.68 cnf(c18,axiom,X175!=X176|~constInInfAttributes(X175)|constInInfAttributes(X176),theory(equality)).
% 0.49/0.68 cnf(c17,axiom,X172!=X173|~absolutelyInfinite(X172)|absolutelyInfinite(X173),theory(equality)).
% 0.49/0.68 cnf(c16,axiom,X169!=X170|~being(X169)|being(X170),theory(equality)).
% 0.49/0.68 cnf(c12,axiom,X165!=X166|X167!=X168|~modification(X165,X167)|modification(X166,X168),theory(equality)).
% 0.49/0.68 cnf(c15,axiom,X162!=X163|~god(X162)|god(X163),theory(equality)).
% 0.49/0.68 cnf(c11,axiom,X159!=X160|~mode(X159)|mode(X160),theory(equality)).
% 0.49/0.68 cnf(c10,axiom,X156!=X157|~intPercAsConstEssSub(X156)|intPercAsConstEssSub(X157),theory(equality)).
% 0.49/0.68 cnf(c9,axiom,X153!=X154|~attribute(X153)|attribute(X154),theory(equality)).
% 0.49/0.68 cnf(c8,axiom,X150!=X151|~conceivedThruItself(X150)|conceivedThruItself(X151),theory(equality)).
% 0.49/0.68 cnf(c7,axiom,X147!=X148|~inItself(X147)|inItself(X148),theory(equality)).
% 0.49/0.68 cnf(c6,axiom,X144!=X145|~substance(X144)|substance(X145),theory(equality)).
% 0.49/0.68 fof(self_caused,axiom,(![X]:(selfCaused(X)<=>(essenceInvExistence(X)&natureConcOnlyByExistence(X)))),file('/export/starexec/sandbox/benchmark/Axioms/PHI002+0.ax', self_caused)).
% 0.49/0.68 fof(c175,plain,(![X]:((~selfCaused(X)|(essenceInvExistence(X)&natureConcOnlyByExistence(X)))&((~essenceInvExistence(X)|~natureConcOnlyByExistence(X))|selfCaused(X)))),inference(fof_nnf,[status(thm)],[self_caused])).
% 0.49/0.68 fof(c176,plain,((![X]:(~selfCaused(X)|(essenceInvExistence(X)&natureConcOnlyByExistence(X))))&(![X]:((~essenceInvExistence(X)|~natureConcOnlyByExistence(X))|selfCaused(X)))),inference(shift_quantors,[status(thm)],[c175])).
% 0.49/0.68 fof(c178,plain,(![X61]:(![X62]:((~selfCaused(X61)|(essenceInvExistence(X61)&natureConcOnlyByExistence(X61)))&((~essenceInvExistence(X62)|~natureConcOnlyByExistence(X62))|selfCaused(X62))))),inference(shift_quantors,[status(thm)],[fof(c177,plain,((![X61]:(~selfCaused(X61)|(essenceInvExistence(X61)&natureConcOnlyByExistence(X61))))&(![X62]:((~essenceInvExistence(X62)|~natureConcOnlyByExistence(X62))|selfCaused(X62)))),inference(variable_rename,[status(thm)],[c176])).])).
% 0.49/0.68 fof(c179,plain,(![X61]:(![X62]:(((~selfCaused(X61)|essenceInvExistence(X61))&(~selfCaused(X61)|natureConcOnlyByExistence(X61)))&((~essenceInvExistence(X62)|~natureConcOnlyByExistence(X62))|selfCaused(X62))))),inference(distribute,[status(thm)],[c178])).
% 0.49/0.68 cnf(c182,plain,~essenceInvExistence(X143)|~natureConcOnlyByExistence(X143)|selfCaused(X143),inference(split_conjunct,[status(thm)],[c179])).
% 0.49/0.68 fof(substance,axiom,(![X]:(substance(X)<=>(inItself(X)&conceivedThruItself(X)))),file('/export/starexec/sandbox/benchmark/Axioms/PHI002+0.ax', substance)).
% 0.49/0.68 fof(c159,plain,(![X]:((~substance(X)|(inItself(X)&conceivedThruItself(X)))&((~inItself(X)|~conceivedThruItself(X))|substance(X)))),inference(fof_nnf,[status(thm)],[substance])).
% 0.49/0.68 fof(c160,plain,((![X]:(~substance(X)|(inItself(X)&conceivedThruItself(X))))&(![X]:((~inItself(X)|~conceivedThruItself(X))|substance(X)))),inference(shift_quantors,[status(thm)],[c159])).
% 0.49/0.68 fof(c162,plain,(![X54]:(![X55]:((~substance(X54)|(inItself(X54)&conceivedThruItself(X54)))&((~inItself(X55)|~conceivedThruItself(X55))|substance(X55))))),inference(shift_quantors,[status(thm)],[fof(c161,plain,((![X54]:(~substance(X54)|(inItself(X54)&conceivedThruItself(X54))))&(![X55]:((~inItself(X55)|~conceivedThruItself(X55))|substance(X55)))),inference(variable_rename,[status(thm)],[c160])).])).
% 0.49/0.68 fof(c163,plain,(![X54]:(![X55]:(((~substance(X54)|inItself(X54))&(~substance(X54)|conceivedThruItself(X54)))&((~inItself(X55)|~conceivedThruItself(X55))|substance(X55))))),inference(distribute,[status(thm)],[c162])).
% 0.49/0.68 cnf(c166,plain,~inItself(X142)|~conceivedThruItself(X142)|substance(X142),inference(split_conjunct,[status(thm)],[c163])).
% 0.49/0.68 fof(god,axiom,(![X]:(god(X)<=>(being(X)&absolutelyInfinite(X)))),file('/export/starexec/sandbox/benchmark/Axioms/PHI002+0.ax', god)).
% 0.49/0.68 fof(c134,plain,(![X]:((~god(X)|(being(X)&absolutelyInfinite(X)))&((~being(X)|~absolutelyInfinite(X))|god(X)))),inference(fof_nnf,[status(thm)],[god])).
% 0.49/0.68 fof(c135,plain,((![X]:(~god(X)|(being(X)&absolutelyInfinite(X))))&(![X]:((~being(X)|~absolutelyInfinite(X))|god(X)))),inference(shift_quantors,[status(thm)],[c134])).
% 0.49/0.68 fof(c137,plain,(![X42]:(![X43]:((~god(X42)|(being(X42)&absolutelyInfinite(X42)))&((~being(X43)|~absolutelyInfinite(X43))|god(X43))))),inference(shift_quantors,[status(thm)],[fof(c136,plain,((![X42]:(~god(X42)|(being(X42)&absolutelyInfinite(X42))))&(![X43]:((~being(X43)|~absolutelyInfinite(X43))|god(X43)))),inference(variable_rename,[status(thm)],[c135])).])).
% 0.49/0.68 fof(c138,plain,(![X42]:(![X43]:(((~god(X42)|being(X42))&(~god(X42)|absolutelyInfinite(X42)))&((~being(X43)|~absolutelyInfinite(X43))|god(X43))))),inference(distribute,[status(thm)],[c137])).
% 0.49/0.68 cnf(c141,plain,~being(X141)|~absolutelyInfinite(X141)|god(X141),inference(split_conjunct,[status(thm)],[c138])).
% 0.49/0.68 cnf(c5,axiom,X137!=X138|X139!=X140|~sameKind(X137,X139)|sameKind(X138,X140),theory(equality)).
% 0.49/0.68 cnf(c111,plain,~necessary(X135)|isMethodAction(X136)|isMethodExistence(X136),inference(split_conjunct,[status(thm)],[c107])).
% 0.49/0.68 cnf(c4,axiom,X125!=X126|X127!=X128|~canBeLimitedBy(X125,X127)|canBeLimitedBy(X126,X128),theory(equality)).
% 0.49/0.68 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.49/0.68 fof(c58,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.49/0.68 fof(c59,plain,(![X]:(![Y]:(~haveNothingInCommon(X,Y)|(((~canBeUnderstoodInTermsOf(X,Y)&~canBeUnderstoodInTermsOf(Y,X))&~conceptionInvolves(X,Y))&~conceptionInvolves(Y,X))))),inference(fof_nnf,[status(thm)],[c58])).
% 0.49/0.68 fof(c60,plain,(![X6]:(![X7]:(~haveNothingInCommon(X6,X7)|(((~canBeUnderstoodInTermsOf(X6,X7)&~canBeUnderstoodInTermsOf(X7,X6))&~conceptionInvolves(X6,X7))&~conceptionInvolves(X7,X6))))),inference(variable_rename,[status(thm)],[c59])).
% 0.49/0.68 fof(c61,plain,(![X6]:(![X7]:((((~haveNothingInCommon(X6,X7)|~canBeUnderstoodInTermsOf(X6,X7))&(~haveNothingInCommon(X6,X7)|~canBeUnderstoodInTermsOf(X7,X6)))&(~haveNothingInCommon(X6,X7)|~conceptionInvolves(X6,X7)))&(~haveNothingInCommon(X6,X7)|~conceptionInvolves(X7,X6))))),inference(distribute,[status(thm)],[c60])).
% 0.49/0.68 cnf(c65,plain,~haveNothingInCommon(X121,X122)|~conceptionInvolves(X122,X121),inference(split_conjunct,[status(thm)],[c61])).
% 0.49/0.68 cnf(c64,plain,~haveNothingInCommon(X119,X120)|~conceptionInvolves(X119,X120),inference(split_conjunct,[status(thm)],[c61])).
% 0.49/0.68 cnf(c63,plain,~haveNothingInCommon(X117,X118)|~canBeUnderstoodInTermsOf(X118,X117),inference(split_conjunct,[status(thm)],[c61])).
% 0.49/0.68 cnf(c3,axiom,X114!=X115|~finiteAfterItsKind(X114)|finiteAfterItsKind(X115),theory(equality)).
% 0.49/0.68 cnf(c62,plain,~haveNothingInCommon(X112,X113)|~canBeUnderstoodInTermsOf(X112,X113),inference(split_conjunct,[status(thm)],[c61])).
% 0.49/0.68 cnf(c173,plain,~finiteAfterItsKind(X111)|sameKind(X111,X110),inference(split_conjunct,[status(thm)],[c171])).
% 0.49/0.68 cnf(c172,plain,~finiteAfterItsKind(X108)|canBeLimitedBy(X108,X109),inference(split_conjunct,[status(thm)],[c171])).
% 0.49/0.68 cnf(c110,plain,~necessary(X106)|determinedByDefiniteMethod(X106,X107),inference(split_conjunct,[status(thm)],[c107])).
% 0.49/0.68 cnf(c2,axiom,X103!=X104|~natureConcOnlyByExistence(X103)|natureConcOnlyByExistence(X104),theory(equality)).
% 0.49/0.68 cnf(c109,plain,~necessary(X101)|determinedByFixedMethod(X101,X102),inference(split_conjunct,[status(thm)],[c107])).
% 0.49/0.68 cnf(c108,plain,~necessary(X99)|externalTo(X100,X99),inference(split_conjunct,[status(thm)],[c107])).
% 0.49/0.68 cnf(c95,plain,~existsIn(X98,X98)|exists(X98),inference(split_conjunct,[status(thm)],[c92])).
% 0.49/0.68 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.49/0.68 fof(c72,plain,(![X]:(![Y]:(definiteCause(X)=>(effectNecessarilyFollowsFrom(Y,X)&(~definiteCause(X)=>~effectNecessarilyFollowsFrom(Y,X)))))),inference(fof_simplification,[status(thm)],[definite_cause])).
% 0.49/0.68 fof(c73,plain,(![X]:(![Y]:(~definiteCause(X)|(effectNecessarilyFollowsFrom(Y,X)&(definiteCause(X)|~effectNecessarilyFollowsFrom(Y,X)))))),inference(fof_nnf,[status(thm)],[c72])).
% 0.49/0.68 fof(c74,plain,(![X]:(~definiteCause(X)|((![Y]:effectNecessarilyFollowsFrom(Y,X))&(definiteCause(X)|(![Y]:~effectNecessarilyFollowsFrom(Y,X)))))),inference(shift_quantors,[status(thm)],[c73])).
% 0.49/0.68 fof(c76,plain,(![X12]:(![X13]:(![X14]:(~definiteCause(X12)|(effectNecessarilyFollowsFrom(X13,X12)&(definiteCause(X12)|~effectNecessarilyFollowsFrom(X14,X12))))))),inference(shift_quantors,[status(thm)],[fof(c75,plain,(![X12]:(~definiteCause(X12)|((![X13]:effectNecessarilyFollowsFrom(X13,X12))&(definiteCause(X12)|(![X14]:~effectNecessarilyFollowsFrom(X14,X12)))))),inference(variable_rename,[status(thm)],[c74])).])).
% 0.49/0.68 fof(c77,plain,(![X12]:(![X13]:(![X14]:((~definiteCause(X12)|effectNecessarilyFollowsFrom(X13,X12))&(~definiteCause(X12)|(definiteCause(X12)|~effectNecessarilyFollowsFrom(X14,X12))))))),inference(distribute,[status(thm)],[c76])).
% 0.49/0.68 cnf(c78,plain,~definiteCause(X96)|effectNecessarilyFollowsFrom(X97,X96),inference(split_conjunct,[status(thm)],[c77])).
% 0.49/0.68 cnf(c1,axiom,X93!=X94|~essenceInvExistence(X93)|essenceInvExistence(X94),theory(equality)).
% 0.49/0.68 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.49/0.68 fof(c66,plain,(![X]:(![Y]:((~knowledgeOfEffect(X,Y)|knowledgeOfACause(X))&(~knowledgeOfACause(X)|knowledgeOfEffect(X,Y))))),inference(fof_nnf,[status(thm)],[knowledge_of_effect])).
% 0.49/0.68 fof(c67,plain,((![X]:((![Y]:~knowledgeOfEffect(X,Y))|knowledgeOfACause(X)))&(![X]:(~knowledgeOfACause(X)|(![Y]:knowledgeOfEffect(X,Y))))),inference(shift_quantors,[status(thm)],[c66])).
% 0.49/0.68 fof(c69,plain,(![X8]:(![X9]:(![X10]:(![X11]:((~knowledgeOfEffect(X8,X9)|knowledgeOfACause(X8))&(~knowledgeOfACause(X10)|knowledgeOfEffect(X10,X11))))))),inference(shift_quantors,[status(thm)],[fof(c68,plain,((![X8]:((![X9]:~knowledgeOfEffect(X8,X9))|knowledgeOfACause(X8)))&(![X10]:(~knowledgeOfACause(X10)|(![X11]:knowledgeOfEffect(X10,X11))))),inference(variable_rename,[status(thm)],[c67])).])).
% 0.49/0.68 cnf(c71,plain,~knowledgeOfACause(X92)|knowledgeOfEffect(X92,X91),inference(split_conjunct,[status(thm)],[c69])).
% 0.49/0.68 cnf(c70,plain,~knowledgeOfEffect(X90,X89)|knowledgeOfACause(X90),inference(split_conjunct,[status(thm)],[c69])).
% 0.49/0.68 cnf(c56,plain,~trueIdea(X87)|correspondWith(X87,X88),inference(split_conjunct,[status(thm)],[c55])).
% 0.49/0.68 cnf(c181,plain,~selfCaused(X85)|natureConcOnlyByExistence(X85),inference(split_conjunct,[status(thm)],[c179])).
% 0.49/0.68 cnf(c0,axiom,X83!=X84|~selfCaused(X83)|selfCaused(X84),theory(equality)).
% 0.49/0.68 cnf(c180,plain,~selfCaused(X82)|essenceInvExistence(X82),inference(split_conjunct,[status(thm)],[c179])).
% 0.49/0.68 cnf(c165,plain,~substance(X81)|conceivedThruItself(X81),inference(split_conjunct,[status(thm)],[c163])).
% 0.49/0.68 cnf(c164,plain,~substance(X80)|inItself(X80),inference(split_conjunct,[status(thm)],[c163])).
% 0.49/0.68 fof(attribute,axiom,(![X]:(attribute(X)<=>intPercAsConstEssSub(X))),file('/export/starexec/sandbox/benchmark/Axioms/PHI002+0.ax', attribute)).
% 0.49/0.68 fof(c153,plain,(![X]:((~attribute(X)|intPercAsConstEssSub(X))&(~intPercAsConstEssSub(X)|attribute(X)))),inference(fof_nnf,[status(thm)],[attribute])).
% 0.49/0.68 fof(c154,plain,((![X]:(~attribute(X)|intPercAsConstEssSub(X)))&(![X]:(~intPercAsConstEssSub(X)|attribute(X)))),inference(shift_quantors,[status(thm)],[c153])).
% 0.49/0.68 fof(c156,plain,(![X52]:(![X53]:((~attribute(X52)|intPercAsConstEssSub(X52))&(~intPercAsConstEssSub(X53)|attribute(X53))))),inference(shift_quantors,[status(thm)],[fof(c155,plain,((![X52]:(~attribute(X52)|intPercAsConstEssSub(X52)))&(![X53]:(~intPercAsConstEssSub(X53)|attribute(X53)))),inference(variable_rename,[status(thm)],[c154])).])).
% 0.49/0.68 cnf(c158,plain,~intPercAsConstEssSub(X79)|attribute(X79),inference(split_conjunct,[status(thm)],[c156])).
% 0.49/0.68 cnf(c157,plain,~attribute(X78)|intPercAsConstEssSub(X78),inference(split_conjunct,[status(thm)],[c156])).
% 0.49/0.68 cnf(transitivity,axiom,X76!=X77|X77!=X75|X76=X75,theory(equality)).
% 0.49/0.68 cnf(c140,plain,~god(X74)|absolutelyInfinite(X74),inference(split_conjunct,[status(thm)],[c138])).
% 0.49/0.68 cnf(c139,plain,~god(X73)|being(X73),inference(split_conjunct,[status(thm)],[c138])).
% 0.49/0.68 cnf(c129,plain,~absolutelyInfinite(X72)|constInInfAttributes(X72),inference(split_conjunct,[status(thm)],[c127])).
% 0.49/0.68 cnf(c128,plain,~absolutelyInfinite(X71)|substance(X71),inference(split_conjunct,[status(thm)],[c127])).
% 0.49/0.68 cnf(symmetry,axiom,X68!=X69|X69=X68,theory(equality)).
% 0.49/0.68 cnf(c119,plain,~free(X67)|existsOnlyByNecessityOfOwnNature(X67),inference(split_conjunct,[status(thm)],[c118])).
% 0.49/0.68 fof(eternity,axiom,(![X]:(eternity(X)<=>existConcFollowFromDefEternal(X))),file('/export/starexec/sandbox/benchmark/Axioms/PHI002+0.ax', eternity)).
% 0.49/0.68 fof(c97,plain,(![X]:((~eternity(X)|existConcFollowFromDefEternal(X))&(~existConcFollowFromDefEternal(X)|eternity(X)))),inference(fof_nnf,[status(thm)],[eternity])).
% 0.49/0.68 fof(c98,plain,((![X]:(~eternity(X)|existConcFollowFromDefEternal(X)))&(![X]:(~existConcFollowFromDefEternal(X)|eternity(X)))),inference(shift_quantors,[status(thm)],[c97])).
% 0.49/0.68 fof(c100,plain,(![X23]:(![X24]:((~eternity(X23)|existConcFollowFromDefEternal(X23))&(~existConcFollowFromDefEternal(X24)|eternity(X24))))),inference(shift_quantors,[status(thm)],[fof(c99,plain,((![X23]:(~eternity(X23)|existConcFollowFromDefEternal(X23)))&(![X24]:(~existConcFollowFromDefEternal(X24)|eternity(X24)))),inference(variable_rename,[status(thm)],[c98])).])).
% 0.49/0.68 cnf(c102,plain,~existConcFollowFromDefEternal(X66)|eternity(X66),inference(split_conjunct,[status(thm)],[c100])).
% 0.49/0.68 cnf(c101,plain,~eternity(X65)|existConcFollowFromDefEternal(X65),inference(split_conjunct,[status(thm)],[c100])).
% 0.49/0.68 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.49/0.68 fof(c47,plain,(![X]:(canBeConceivedAsNonExisting(X)=>~essenceInvExistence(X))),inference(fof_simplification,[status(thm)],[can_be_conceived_as_non_existing])).
% 0.49/0.68 fof(c48,plain,(![X]:(~canBeConceivedAsNonExisting(X)|~essenceInvExistence(X))),inference(fof_nnf,[status(thm)],[c47])).
% 0.49/0.68 fof(c49,plain,(![X2]:(~canBeConceivedAsNonExisting(X2)|~essenceInvExistence(X2))),inference(variable_rename,[status(thm)],[c48])).
% 0.49/0.68 cnf(c50,plain,~canBeConceivedAsNonExisting(X64)|~essenceInvExistence(X64),inference(split_conjunct,[status(thm)],[c49])).
% 0.49/0.68 % SZS output end Saturation
% 0.49/0.68
% 0.49/0.68 % Initial clauses : 105
% 0.49/0.68 % Processed clauses : 108
% 0.49/0.68 % Factors computed : 3
% 0.49/0.68 % Resolvents computed: 35
% 0.49/0.68 % Tautologies deleted: 31
% 0.49/0.68 % Forward subsumed : 4
% 0.49/0.68 % Backward subsumed : 3
% 0.49/0.68 % -------- CPU Time ---------
% 0.49/0.68 % User time : 0.307 s
% 0.49/0.68 % System time : 0.015 s
% 0.49/0.68 % Total time : 0.322 s
%------------------------------------------------------------------------------