%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PHI016+1 : TPTP v8.1.2. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n018.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:17 EDT 2024
% Result : CounterSatisfiable 0.42s 0.59s
% Output : Saturation 0.42s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : PHI016+1 : TPTP v8.1.2. Released v7.4.0.
% 0.03/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.11/0.32 % Computer : n018.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Wed May 8 22:30:08 EDT 2024
% 0.11/0.32 % CPUTime :
% 0.42/0.59 % Version: 1.5
% 0.42/0.59 % SZS status CounterSatisfiable
% 0.42/0.59 % SZS output start Saturation
% 0.42/0.59 fof(necessary,axiom,(![X]:(![Y]:(necessary(X)<=>(((externalTo(Y,X)&determinedByFixedMethod(X,Y))&determinedByDefiniteMethod(X,Y))&(isMethodAction(Y)|isMethodExistence(Y)))))),file('/export/starexec/sandbox2/benchmark/Axioms/PHI002+0.ax', necessary)).
% 0.42/0.59 fof(c109,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.42/0.59 fof(c110,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)],[c109])).
% 0.42/0.59 fof(c112,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(c111,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)],[c110])).])).
% 0.42/0.59 fof(c113,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)],[c112])).
% 0.42/0.59 cnf(c119,plain,~externalTo(X340,X341)|~determinedByFixedMethod(X341,X340)|~determinedByDefiniteMethod(X341,X340)|~isMethodExistence(X340)|necessary(X341),inference(split_conjunct,[status(thm)],[c113])).
% 0.42/0.59 cnf(c118,plain,~externalTo(X338,X339)|~determinedByFixedMethod(X339,X338)|~determinedByDefiniteMethod(X339,X338)|~isMethodAction(X338)|necessary(X339),inference(split_conjunct,[status(thm)],[c113])).
% 0.42/0.59 cnf(c45,axiom,X335!=X337|X336!=X334|~objectOf(X335,X336)|objectOf(X337,X334),theory(equality)).
% 0.42/0.59 cnf(c44,axiom,X331!=X333|X332!=X330|~ideateOf(X331,X332)|ideateOf(X333,X330),theory(equality)).
% 0.42/0.59 cnf(c43,axiom,X327!=X329|X328!=X326|~correspondWith(X327,X328)|correspondWith(X329,X326),theory(equality)).
% 0.42/0.59 cnf(c41,axiom,X323!=X325|X324!=X322|~canBeUnderstoodInTermsOf(X323,X324)|canBeUnderstoodInTermsOf(X325,X322),theory(equality)).
% 0.42/0.59 cnf(c40,axiom,X319!=X321|X320!=X318|~conceptionInvolves(X319,X320)|conceptionInvolves(X321,X318),theory(equality)).
% 0.42/0.59 fof(absolutely_infinite,axiom,(![X]:(![Y]:(absolutelyInfinite(X)<=>((substance(X)&constInInfAttributes(X))&(attributeOf(Y,X)=>(expressesEternalEssentiality(Y)&expressesInfiniteEssentiality(Y))))))),file('/export/starexec/sandbox2/benchmark/Axioms/PHI002+0.ax', absolutely_infinite)).
% 0.42/0.59 fof(c129,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.42/0.59 fof(c130,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)],[c129])).
% 0.42/0.59 fof(c132,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(c131,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)],[c130])).])).
% 0.42/0.59 fof(c133,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)],[c132])).
% 0.42/0.59 cnf(c139,plain,~substance(X316)|~constInInfAttributes(X316)|~expressesEternalEssentiality(X317)|~expressesInfiniteEssentiality(X317)|absolutelyInfinite(X316),inference(split_conjunct,[status(thm)],[c133])).
% 0.42/0.59 cnf(c138,plain,~substance(X313)|~constInInfAttributes(X313)|attributeOf(X314,X313)|absolutelyInfinite(X313),inference(split_conjunct,[status(thm)],[c133])).
% 0.42/0.59 cnf(c39,axiom,X310!=X312|X311!=X309|~haveNothingInCommon(X310,X311)|haveNothingInCommon(X312,X309),theory(equality)).
% 0.42/0.59 cnf(reflexivity,axiom,X64=X64,theory(equality)).
% 0.42/0.59 fof(conceived_through,axiom,(![X]:(![Y]:((~conceivedThru(X,X))=>(conceivedThru(X,Y)&X!=Y)))),file('/export/starexec/sandbox2/benchmark/Axioms/PHI002+1.ax', conceived_through)).
% 0.42/0.59 fof(c86,plain,(![X]:(![Y]:(~conceivedThru(X,X)=>(conceivedThru(X,Y)&X!=Y)))),inference(fof_simplification,[status(thm)],[conceived_through])).
% 0.42/0.59 fof(c87,plain,(![X]:(![Y]:(conceivedThru(X,X)|(conceivedThru(X,Y)&X!=Y)))),inference(fof_nnf,[status(thm)],[c86])).
% 0.42/0.59 fof(c88,plain,(![X]:(conceivedThru(X,X)|((![Y]:conceivedThru(X,Y))&(![Y]:X!=Y)))),inference(shift_quantors,[status(thm)],[c87])).
% 0.42/0.59 fof(c90,plain,(![X16]:(![X17]:(![X18]:(conceivedThru(X16,X16)|(conceivedThru(X16,X17)&X16!=X18))))),inference(shift_quantors,[status(thm)],[fof(c89,plain,(![X16]:(conceivedThru(X16,X16)|((![X17]:conceivedThru(X16,X17))&(![X18]:X16!=X18)))),inference(variable_rename,[status(thm)],[c88])).])).
% 0.42/0.59 fof(c91,plain,(![X16]:(![X17]:(![X18]:((conceivedThru(X16,X16)|conceivedThru(X16,X17))&(conceivedThru(X16,X16)|X16!=X18))))),inference(distribute,[status(thm)],[c90])).
% 0.42/0.59 cnf(c92,plain,conceivedThru(X132,X132)|conceivedThru(X132,X133),inference(split_conjunct,[status(thm)],[c91])).
% 0.42/0.59 cnf(c202,plain,conceivedThru(X134,X134),inference(factor,[status(thm)],[c92])).
% 0.42/0.59 cnf(c14,axiom,X193!=X195|X194!=X192|~conceivedThru(X193,X194)|conceivedThru(X195,X192),theory(equality)).
% 0.42/0.59 cnf(c218,plain,X301!=X303|X301!=X302|conceivedThru(X303,X302),inference(resolution,[status(thm)],[c14, c202])).
% 0.42/0.59 cnf(c233,plain,X307!=X306|conceivedThru(X306,X307),inference(resolution,[status(thm)],[c218, reflexivity])).
% 0.42/0.59 fof(finite_after_its_kind,axiom,(![X]:(![Y]:(finiteAfterItsKind(X)<=>(canBeLimitedBy(X,Y)&sameKind(X,Y))))),file('/export/starexec/sandbox2/benchmark/Axioms/PHI002+0.ax', finite_after_its_kind)).
% 0.42/0.59 fof(c173,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.42/0.59 fof(c174,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)],[c173])).
% 0.42/0.59 fof(c176,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(c175,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)],[c174])).])).
% 0.42/0.59 fof(c177,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)],[c176])).
% 0.42/0.59 cnf(c180,plain,~canBeLimitedBy(X299,X300)|~sameKind(X299,X300)|finiteAfterItsKind(X299),inference(split_conjunct,[status(thm)],[c177])).
% 0.42/0.59 cnf(c37,axiom,X296!=X298|X297!=X295|~knowledgeOfEffect(X296,X297)|knowledgeOfEffect(X298,X295),theory(equality)).
% 0.42/0.59 fof(mode,axiom,(![X]:(![Y]:(![Z]:(mode(X)<=>((modification(X,Y)&substance(Y))|(existsIn(X,Z)&conceivedThru(X,Z))))))),file('/export/starexec/sandbox2/benchmark/Axioms/PHI002+0.ax', mode)).
% 0.42/0.59 fof(c148,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.42/0.59 fof(c149,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)],[c148])).
% 0.42/0.59 fof(c151,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(c150,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)],[c149])).])).
% 0.42/0.59 fof(c152,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)],[c151])).
% 0.42/0.59 cnf(c158,plain,~existsIn(X292,X293)|~conceivedThru(X292,X293)|mode(X292),inference(split_conjunct,[status(thm)],[c152])).
% 0.42/0.59 cnf(c231,plain,~existsIn(X294,X294)|mode(X294),inference(resolution,[status(thm)],[c158, c202])).
% 0.42/0.59 cnf(c154,plain,~mode(X289)|modification(X289,X290)|conceivedThru(X289,X291),inference(split_conjunct,[status(thm)],[c152])).
% 0.42/0.59 cnf(c153,plain,~mode(X286)|modification(X286,X287)|existsIn(X286,X288),inference(split_conjunct,[status(thm)],[c152])).
% 0.42/0.59 fof(free,axiom,(![X]:(![Y]:(free(X)<=>(existsOnlyByNecessityOfOwnNature(X)&(actionOf(Y,X)=>determinedByItselfAlone(Y,X)))))),file('/export/starexec/sandbox2/benchmark/Axioms/PHI002+0.ax', free)).
% 0.42/0.59 fof(c120,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.42/0.59 fof(c121,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)],[c120])).
% 0.42/0.59 fof(c123,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(c122,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)],[c121])).])).
% 0.42/0.59 fof(c124,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)],[c123])).
% 0.42/0.59 cnf(c126,plain,~free(X285)|~actionOf(X284,X285)|determinedByItselfAlone(X284,X285),inference(split_conjunct,[status(thm)],[c124])).
% 0.42/0.59 cnf(c36,axiom,X281!=X283|X282!=X280|~effectNecessarilyFollowsFrom(X281,X282)|effectNecessarilyFollowsFrom(X283,X280),theory(equality)).
% 0.42/0.59 fof(exists,axiom,(![X]:(![Y]:(exists(X)<=>(existsIn(X,X)|(existsIn(X,Y)&X!=Y))))),file('/export/starexec/sandbox2/benchmark/Axioms/PHI002+1.ax', exists)).
% 0.42/0.59 fof(c94,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.42/0.59 fof(c95,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)],[c94])).
% 0.42/0.59 fof(c97,plain,(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:((~exists(X19)|(existsIn(X19,X19)|(existsIn(X19,X20)&X19!=X21)))&((~existsIn(X22,X22)&(~existsIn(X22,X23)|X22=X23))|exists(X22)))))))),inference(shift_quantors,[status(thm)],[fof(c96,plain,((![X19]:(~exists(X19)|(existsIn(X19,X19)|((![X20]:existsIn(X19,X20))&(![X21]:X19!=X21)))))&(![X22]:((~existsIn(X22,X22)&(![X23]:(~existsIn(X22,X23)|X22=X23)))|exists(X22)))),inference(variable_rename,[status(thm)],[c95])).])).
% 0.42/0.59 fof(c98,plain,(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(((~exists(X19)|(existsIn(X19,X19)|existsIn(X19,X20)))&(~exists(X19)|(existsIn(X19,X19)|X19!=X21)))&((~existsIn(X22,X22)|exists(X22))&((~existsIn(X22,X23)|X22=X23)|exists(X22))))))))),inference(distribute,[status(thm)],[c97])).
% 0.42/0.59 cnf(c102,plain,~existsIn(X279,X278)|X279=X278|exists(X279),inference(split_conjunct,[status(thm)],[c98])).
% 0.42/0.59 cnf(c100,plain,~exists(X276)|existsIn(X276,X276)|X276!=X275,inference(split_conjunct,[status(thm)],[c98])).
% 0.42/0.59 cnf(c230,plain,~exists(X277)|existsIn(X277,X277),inference(resolution,[status(thm)],[c100, reflexivity])).
% 0.42/0.59 fof(true_idea,axiom,(![X]:(![Y]:(trueIdea(X)=>(correspondWith(X,Y)&(ideateOf(Y,X)|objectOf(Y,X)))))),file('/export/starexec/sandbox2/benchmark/Axioms/PHI002+1.ax', true_idea)).
% 0.42/0.59 fof(c57,plain,(![X]:(![Y]:(~trueIdea(X)|(correspondWith(X,Y)&(ideateOf(Y,X)|objectOf(Y,X)))))),inference(fof_nnf,[status(thm)],[true_idea])).
% 0.42/0.59 fof(c58,plain,(![X]:(~trueIdea(X)|((![Y]:correspondWith(X,Y))&(![Y]:(ideateOf(Y,X)|objectOf(Y,X)))))),inference(shift_quantors,[status(thm)],[c57])).
% 0.42/0.59 fof(c60,plain,(![X4]:(![X5]:(![X6]:(~trueIdea(X4)|(correspondWith(X4,X5)&(ideateOf(X6,X4)|objectOf(X6,X4))))))),inference(shift_quantors,[status(thm)],[fof(c59,plain,(![X4]:(~trueIdea(X4)|((![X5]:correspondWith(X4,X5))&(![X6]:(ideateOf(X6,X4)|objectOf(X6,X4)))))),inference(variable_rename,[status(thm)],[c58])).])).
% 0.42/0.60 fof(c61,plain,(![X4]:(![X5]:(![X6]:((~trueIdea(X4)|correspondWith(X4,X5))&(~trueIdea(X4)|(ideateOf(X6,X4)|objectOf(X6,X4))))))),inference(distribute,[status(thm)],[c60])).
% 0.42/0.60 cnf(c63,plain,~trueIdea(X272)|ideateOf(X271,X272)|objectOf(X271,X272),inference(split_conjunct,[status(thm)],[c61])).
% 0.42/0.60 cnf(c31,axiom,X268!=X270|X269!=X267|~determinedByFixedMethod(X268,X269)|determinedByFixedMethod(X270,X267),theory(equality)).
% 0.42/0.60 cnf(c157,plain,~modification(X266,X265)|~substance(X265)|mode(X266),inference(split_conjunct,[status(thm)],[c152])).
% 0.42/0.60 cnf(c156,plain,~mode(X263)|substance(X262)|conceivedThru(X263,X264),inference(split_conjunct,[status(thm)],[c152])).
% 0.42/0.60 cnf(c155,plain,~mode(X260)|substance(X259)|existsIn(X260,X261),inference(split_conjunct,[status(thm)],[c152])).
% 0.42/0.60 cnf(c137,plain,~absolutelyInfinite(X257)|~attributeOf(X258,X257)|expressesInfiniteEssentiality(X258),inference(split_conjunct,[status(thm)],[c133])).
% 0.42/0.60 cnf(c136,plain,~absolutelyInfinite(X255)|~attributeOf(X256,X255)|expressesEternalEssentiality(X256),inference(split_conjunct,[status(thm)],[c133])).
% 0.42/0.60 cnf(c30,axiom,X252!=X254|X253!=X251|~externalTo(X252,X253)|externalTo(X254,X251),theory(equality)).
% 0.42/0.60 cnf(c128,plain,~existsOnlyByNecessityOfOwnNature(X250)|~determinedByItselfAlone(X249,X250)|free(X250),inference(split_conjunct,[status(thm)],[c124])).
% 0.42/0.60 cnf(c127,plain,~existsOnlyByNecessityOfOwnNature(X247)|actionOf(X248,X247)|free(X247),inference(split_conjunct,[status(thm)],[c124])).
% 0.42/0.60 cnf(c46,axiom,X242!=X243|~canBeConceivedAsNonExisting(X242)|canBeConceivedAsNonExisting(X243),theory(equality)).
% 0.42/0.60 cnf(c27,axiom,X239!=X241|X240!=X238|~determinedByDefiniteMethod(X239,X240)|determinedByDefiniteMethod(X241,X238),theory(equality)).
% 0.42/0.60 cnf(c42,axiom,X235!=X236|~trueIdea(X235)|trueIdea(X236),theory(equality)).
% 0.42/0.60 cnf(c38,axiom,X232!=X233|~knowledgeOfACause(X232)|knowledgeOfACause(X233),theory(equality)).
% 0.42/0.60 cnf(c25,axiom,X228!=X230|X229!=X227|~determinedByItselfAlone(X228,X229)|determinedByItselfAlone(X230,X227),theory(equality)).
% 0.42/0.60 cnf(c35,axiom,X225!=X226|~definiteCause(X225)|definiteCause(X226),theory(equality)).
% 0.42/0.60 cnf(c34,axiom,X222!=X223|~exists(X222)|exists(X223),theory(equality)).
% 0.42/0.60 cnf(c33,axiom,X219!=X220|~existConcFollowFromDefEternal(X219)|existConcFollowFromDefEternal(X220),theory(equality)).
% 0.42/0.60 cnf(c24,axiom,X216!=X218|X217!=X215|~actionOf(X216,X217)|actionOf(X218,X215),theory(equality)).
% 0.42/0.60 cnf(c32,axiom,X212!=X213|~eternity(X212)|eternity(X213),theory(equality)).
% 0.42/0.60 cnf(c29,axiom,X209!=X210|~isMethodExistence(X209)|isMethodExistence(X210),theory(equality)).
% 0.42/0.60 cnf(c19,axiom,X205!=X207|X206!=X204|~attributeOf(X205,X206)|attributeOf(X207,X204),theory(equality)).
% 0.42/0.60 cnf(c28,axiom,X202!=X203|~isMethodAction(X202)|isMethodAction(X203),theory(equality)).
% 0.42/0.60 cnf(c26,axiom,X199!=X200|~necessary(X199)|necessary(X200),theory(equality)).
% 0.42/0.60 cnf(c23,axiom,X196!=X197|~existsOnlyByNecessityOfOwnNature(X196)|existsOnlyByNecessityOfOwnNature(X197),theory(equality)).
% 0.42/0.60 cnf(c22,axiom,X189!=X190|~free(X189)|free(X190),theory(equality)).
% 0.42/0.60 cnf(c21,axiom,X186!=X187|~expressesInfiniteEssentiality(X186)|expressesInfiniteEssentiality(X187),theory(equality)).
% 0.42/0.60 cnf(c13,axiom,X182!=X184|X183!=X181|~existsIn(X182,X183)|existsIn(X184,X181),theory(equality)).
% 0.42/0.60 cnf(c20,axiom,X179!=X180|~expressesEternalEssentiality(X179)|expressesEternalEssentiality(X180),theory(equality)).
% 0.42/0.60 cnf(c18,axiom,X176!=X177|~constInInfAttributes(X176)|constInInfAttributes(X177),theory(equality)).
% 0.42/0.60 cnf(c17,axiom,X173!=X174|~absolutelyInfinite(X173)|absolutelyInfinite(X174),theory(equality)).
% 0.42/0.60 cnf(c12,axiom,X170!=X172|X171!=X169|~modification(X170,X171)|modification(X172,X169),theory(equality)).
% 0.42/0.60 cnf(c16,axiom,X166!=X167|~being(X166)|being(X167),theory(equality)).
% 0.42/0.60 cnf(c15,axiom,X163!=X164|~god(X163)|god(X164),theory(equality)).
% 0.42/0.60 cnf(c11,axiom,X160!=X161|~mode(X160)|mode(X161),theory(equality)).
% 0.42/0.60 cnf(c10,axiom,X157!=X158|~intPercAsConstEssSub(X157)|intPercAsConstEssSub(X158),theory(equality)).
% 0.42/0.60 cnf(c9,axiom,X154!=X155|~attribute(X154)|attribute(X155),theory(equality)).
% 0.42/0.60 cnf(c8,axiom,X151!=X152|~conceivedThruItself(X151)|conceivedThruItself(X152),theory(equality)).
% 0.42/0.60 fof(self_caused,axiom,(![X]:(selfCaused(X)<=>(essenceInvExistence(X)&natureConcOnlyByExistence(X)))),file('/export/starexec/sandbox2/benchmark/Axioms/PHI002+0.ax', self_caused)).
% 0.42/0.60 fof(c181,plain,(![X]:((~selfCaused(X)|(essenceInvExistence(X)&natureConcOnlyByExistence(X)))&((~essenceInvExistence(X)|~natureConcOnlyByExistence(X))|selfCaused(X)))),inference(fof_nnf,[status(thm)],[self_caused])).
% 0.42/0.60 fof(c182,plain,((![X]:(~selfCaused(X)|(essenceInvExistence(X)&natureConcOnlyByExistence(X))))&(![X]:((~essenceInvExistence(X)|~natureConcOnlyByExistence(X))|selfCaused(X)))),inference(shift_quantors,[status(thm)],[c181])).
% 0.42/0.60 fof(c184,plain,(![X62]:(![X63]:((~selfCaused(X62)|(essenceInvExistence(X62)&natureConcOnlyByExistence(X62)))&((~essenceInvExistence(X63)|~natureConcOnlyByExistence(X63))|selfCaused(X63))))),inference(shift_quantors,[status(thm)],[fof(c183,plain,((![X62]:(~selfCaused(X62)|(essenceInvExistence(X62)&natureConcOnlyByExistence(X62))))&(![X63]:((~essenceInvExistence(X63)|~natureConcOnlyByExistence(X63))|selfCaused(X63)))),inference(variable_rename,[status(thm)],[c182])).])).
% 0.42/0.60 fof(c185,plain,(![X62]:(![X63]:(((~selfCaused(X62)|essenceInvExistence(X62))&(~selfCaused(X62)|natureConcOnlyByExistence(X62)))&((~essenceInvExistence(X63)|~natureConcOnlyByExistence(X63))|selfCaused(X63))))),inference(distribute,[status(thm)],[c184])).
% 0.42/0.60 cnf(c188,plain,~essenceInvExistence(X150)|~natureConcOnlyByExistence(X150)|selfCaused(X150),inference(split_conjunct,[status(thm)],[c185])).
% 0.42/0.60 fof(substance,axiom,(![X]:(substance(X)<=>(inItself(X)&conceivedThruItself(X)))),file('/export/starexec/sandbox2/benchmark/Axioms/PHI002+0.ax', substance)).
% 0.42/0.60 fof(c165,plain,(![X]:((~substance(X)|(inItself(X)&conceivedThruItself(X)))&((~inItself(X)|~conceivedThruItself(X))|substance(X)))),inference(fof_nnf,[status(thm)],[substance])).
% 0.42/0.60 fof(c166,plain,((![X]:(~substance(X)|(inItself(X)&conceivedThruItself(X))))&(![X]:((~inItself(X)|~conceivedThruItself(X))|substance(X)))),inference(shift_quantors,[status(thm)],[c165])).
% 0.42/0.60 fof(c168,plain,(![X55]:(![X56]:((~substance(X55)|(inItself(X55)&conceivedThruItself(X55)))&((~inItself(X56)|~conceivedThruItself(X56))|substance(X56))))),inference(shift_quantors,[status(thm)],[fof(c167,plain,((![X55]:(~substance(X55)|(inItself(X55)&conceivedThruItself(X55))))&(![X56]:((~inItself(X56)|~conceivedThruItself(X56))|substance(X56)))),inference(variable_rename,[status(thm)],[c166])).])).
% 0.42/0.60 fof(c169,plain,(![X55]:(![X56]:(((~substance(X55)|inItself(X55))&(~substance(X55)|conceivedThruItself(X55)))&((~inItself(X56)|~conceivedThruItself(X56))|substance(X56))))),inference(distribute,[status(thm)],[c168])).
% 0.42/0.60 cnf(c172,plain,~inItself(X149)|~conceivedThruItself(X149)|substance(X149),inference(split_conjunct,[status(thm)],[c169])).
% 0.42/0.60 cnf(c7,axiom,X146!=X147|~inItself(X146)|inItself(X147),theory(equality)).
% 0.42/0.60 fof(god,axiom,(![X]:(god(X)<=>(being(X)&absolutelyInfinite(X)))),file('/export/starexec/sandbox2/benchmark/Axioms/PHI002+0.ax', god)).
% 0.42/0.60 fof(c140,plain,(![X]:((~god(X)|(being(X)&absolutelyInfinite(X)))&((~being(X)|~absolutelyInfinite(X))|god(X)))),inference(fof_nnf,[status(thm)],[god])).
% 0.42/0.60 fof(c141,plain,((![X]:(~god(X)|(being(X)&absolutelyInfinite(X))))&(![X]:((~being(X)|~absolutelyInfinite(X))|god(X)))),inference(shift_quantors,[status(thm)],[c140])).
% 0.42/0.60 fof(c143,plain,(![X43]:(![X44]:((~god(X43)|(being(X43)&absolutelyInfinite(X43)))&((~being(X44)|~absolutelyInfinite(X44))|god(X44))))),inference(shift_quantors,[status(thm)],[fof(c142,plain,((![X43]:(~god(X43)|(being(X43)&absolutelyInfinite(X43))))&(![X44]:((~being(X44)|~absolutelyInfinite(X44))|god(X44)))),inference(variable_rename,[status(thm)],[c141])).])).
% 0.42/0.60 fof(c144,plain,(![X43]:(![X44]:(((~god(X43)|being(X43))&(~god(X43)|absolutelyInfinite(X43)))&((~being(X44)|~absolutelyInfinite(X44))|god(X44))))),inference(distribute,[status(thm)],[c143])).
% 0.42/0.60 cnf(c147,plain,~being(X145)|~absolutelyInfinite(X145)|god(X145),inference(split_conjunct,[status(thm)],[c144])).
% 0.42/0.60 cnf(c117,plain,~necessary(X143)|isMethodAction(X144)|isMethodExistence(X144),inference(split_conjunct,[status(thm)],[c113])).
% 0.42/0.60 cnf(c6,axiom,X137!=X138|~substance(X137)|substance(X138),theory(equality)).
% 0.42/0.60 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/sandbox2/benchmark/Axioms/PHI002+1.ax', have_nothing_in_common)).
% 0.42/0.60 fof(c64,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.42/0.60 fof(c65,plain,(![X]:(![Y]:(~haveNothingInCommon(X,Y)|(((~canBeUnderstoodInTermsOf(X,Y)&~canBeUnderstoodInTermsOf(Y,X))&~conceptionInvolves(X,Y))&~conceptionInvolves(Y,X))))),inference(fof_nnf,[status(thm)],[c64])).
% 0.42/0.60 fof(c66,plain,(![X7]:(![X8]:(~haveNothingInCommon(X7,X8)|(((~canBeUnderstoodInTermsOf(X7,X8)&~canBeUnderstoodInTermsOf(X8,X7))&~conceptionInvolves(X7,X8))&~conceptionInvolves(X8,X7))))),inference(variable_rename,[status(thm)],[c65])).
% 0.42/0.60 fof(c67,plain,(![X7]:(![X8]:((((~haveNothingInCommon(X7,X8)|~canBeUnderstoodInTermsOf(X7,X8))&(~haveNothingInCommon(X7,X8)|~canBeUnderstoodInTermsOf(X8,X7)))&(~haveNothingInCommon(X7,X8)|~conceptionInvolves(X7,X8)))&(~haveNothingInCommon(X7,X8)|~conceptionInvolves(X8,X7))))),inference(distribute,[status(thm)],[c66])).
% 0.42/0.60 cnf(c71,plain,~haveNothingInCommon(X130,X131)|~conceptionInvolves(X131,X130),inference(split_conjunct,[status(thm)],[c67])).
% 0.42/0.60 cnf(c70,plain,~haveNothingInCommon(X128,X129)|~conceptionInvolves(X128,X129),inference(split_conjunct,[status(thm)],[c67])).
% 0.42/0.60 cnf(c5,axiom,X125!=X127|X126!=X124|~sameKind(X125,X126)|sameKind(X127,X124),theory(equality)).
% 0.42/0.60 cnf(c69,plain,~haveNothingInCommon(X122,X123)|~canBeUnderstoodInTermsOf(X123,X122),inference(split_conjunct,[status(thm)],[c67])).
% 0.42/0.60 cnf(c68,plain,~haveNothingInCommon(X120,X121)|~canBeUnderstoodInTermsOf(X120,X121),inference(split_conjunct,[status(thm)],[c67])).
% 0.42/0.60 cnf(c179,plain,~finiteAfterItsKind(X119)|sameKind(X119,X118),inference(split_conjunct,[status(thm)],[c177])).
% 0.42/0.60 cnf(c178,plain,~finiteAfterItsKind(X117)|canBeLimitedBy(X117,X116),inference(split_conjunct,[status(thm)],[c177])).
% 0.42/0.60 cnf(c116,plain,~necessary(X114)|determinedByDefiniteMethod(X114,X115),inference(split_conjunct,[status(thm)],[c113])).
% 0.42/0.60 cnf(c4,axiom,X111!=X113|X112!=X110|~canBeLimitedBy(X111,X112)|canBeLimitedBy(X113,X110),theory(equality)).
% 0.42/0.60 cnf(c115,plain,~necessary(X108)|determinedByFixedMethod(X108,X109),inference(split_conjunct,[status(thm)],[c113])).
% 0.42/0.60 cnf(c114,plain,~necessary(X106)|externalTo(X107,X106),inference(split_conjunct,[status(thm)],[c113])).
% 0.42/0.60 cnf(c101,plain,~existsIn(X105,X105)|exists(X105),inference(split_conjunct,[status(thm)],[c98])).
% 0.42/0.60 fof(definite_cause,axiom,(![X]:(![Y]:(definiteCause(X)=>(effectNecessarilyFollowsFrom(Y,X)&((~definiteCause(X))=>(~effectNecessarilyFollowsFrom(Y,X))))))),file('/export/starexec/sandbox2/benchmark/Axioms/PHI002+1.ax', definite_cause)).
% 0.42/0.60 fof(c78,plain,(![X]:(![Y]:(definiteCause(X)=>(effectNecessarilyFollowsFrom(Y,X)&(~definiteCause(X)=>~effectNecessarilyFollowsFrom(Y,X)))))),inference(fof_simplification,[status(thm)],[definite_cause])).
% 0.42/0.60 fof(c79,plain,(![X]:(![Y]:(~definiteCause(X)|(effectNecessarilyFollowsFrom(Y,X)&(definiteCause(X)|~effectNecessarilyFollowsFrom(Y,X)))))),inference(fof_nnf,[status(thm)],[c78])).
% 0.42/0.60 fof(c80,plain,(![X]:(~definiteCause(X)|((![Y]:effectNecessarilyFollowsFrom(Y,X))&(definiteCause(X)|(![Y]:~effectNecessarilyFollowsFrom(Y,X)))))),inference(shift_quantors,[status(thm)],[c79])).
% 0.42/0.60 fof(c82,plain,(![X13]:(![X14]:(![X15]:(~definiteCause(X13)|(effectNecessarilyFollowsFrom(X14,X13)&(definiteCause(X13)|~effectNecessarilyFollowsFrom(X15,X13))))))),inference(shift_quantors,[status(thm)],[fof(c81,plain,(![X13]:(~definiteCause(X13)|((![X14]:effectNecessarilyFollowsFrom(X14,X13))&(definiteCause(X13)|(![X15]:~effectNecessarilyFollowsFrom(X15,X13)))))),inference(variable_rename,[status(thm)],[c80])).])).
% 0.42/0.60 fof(c83,plain,(![X13]:(![X14]:(![X15]:((~definiteCause(X13)|effectNecessarilyFollowsFrom(X14,X13))&(~definiteCause(X13)|(definiteCause(X13)|~effectNecessarilyFollowsFrom(X15,X13))))))),inference(distribute,[status(thm)],[c82])).
% 0.42/0.60 cnf(c84,plain,~definiteCause(X103)|effectNecessarilyFollowsFrom(X104,X103),inference(split_conjunct,[status(thm)],[c83])).
% 0.42/0.60 cnf(c3,axiom,X100!=X101|~finiteAfterItsKind(X100)|finiteAfterItsKind(X101),theory(equality)).
% 0.42/0.60 fof(knowledge_of_effect,axiom,(![X]:(![Y]:(knowledgeOfEffect(X,Y)<=>knowledgeOfACause(X)))),file('/export/starexec/sandbox2/benchmark/Axioms/PHI002+1.ax', knowledge_of_effect)).
% 0.42/0.60 fof(c72,plain,(![X]:(![Y]:((~knowledgeOfEffect(X,Y)|knowledgeOfACause(X))&(~knowledgeOfACause(X)|knowledgeOfEffect(X,Y))))),inference(fof_nnf,[status(thm)],[knowledge_of_effect])).
% 0.42/0.60 fof(c73,plain,((![X]:((![Y]:~knowledgeOfEffect(X,Y))|knowledgeOfACause(X)))&(![X]:(~knowledgeOfACause(X)|(![Y]:knowledgeOfEffect(X,Y))))),inference(shift_quantors,[status(thm)],[c72])).
% 0.42/0.60 fof(c75,plain,(![X9]:(![X10]:(![X11]:(![X12]:((~knowledgeOfEffect(X9,X10)|knowledgeOfACause(X9))&(~knowledgeOfACause(X11)|knowledgeOfEffect(X11,X12))))))),inference(shift_quantors,[status(thm)],[fof(c74,plain,((![X9]:((![X10]:~knowledgeOfEffect(X9,X10))|knowledgeOfACause(X9)))&(![X11]:(~knowledgeOfACause(X11)|(![X12]:knowledgeOfEffect(X11,X12))))),inference(variable_rename,[status(thm)],[c73])).])).
% 0.42/0.60 cnf(c77,plain,~knowledgeOfACause(X99)|knowledgeOfEffect(X99,X98),inference(split_conjunct,[status(thm)],[c75])).
% 0.42/0.60 cnf(c76,plain,~knowledgeOfEffect(X97,X96)|knowledgeOfACause(X97),inference(split_conjunct,[status(thm)],[c75])).
% 0.42/0.60 cnf(c62,plain,~trueIdea(X95)|correspondWith(X95,X94),inference(split_conjunct,[status(thm)],[c61])).
% 0.42/0.60 cnf(c2,axiom,X90!=X91|~natureConcOnlyByExistence(X90)|natureConcOnlyByExistence(X91),theory(equality)).
% 0.42/0.60 cnf(c187,plain,~selfCaused(X88)|natureConcOnlyByExistence(X88),inference(split_conjunct,[status(thm)],[c185])).
% 0.42/0.60 cnf(c186,plain,~selfCaused(X87)|essenceInvExistence(X87),inference(split_conjunct,[status(thm)],[c185])).
% 0.42/0.60 cnf(c134,plain,~absolutelyInfinite(X72)|substance(X72),inference(split_conjunct,[status(thm)],[c133])).
% 0.42/0.60 fof(if_god_then_exists,conjecture,(![X]:(god(X)=>exists(X))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', if_god_then_exists)).
% 0.42/0.60 fof(c47,negated_conjecture,(~(![X]:(god(X)=>exists(X)))),inference(assume_negation,[status(cth)],[if_god_then_exists])).
% 0.42/0.60 fof(c48,negated_conjecture,(?[X]:(god(X)&~exists(X))),inference(fof_nnf,[status(thm)],[c47])).
% 0.42/0.60 fof(c49,negated_conjecture,(?[X2]:(god(X2)&~exists(X2))),inference(variable_rename,[status(thm)],[c48])).
% 0.42/0.60 fof(c50,negated_conjecture,(god(skolem0001)&~exists(skolem0001)),inference(skolemize,[status(esa)],[c49])).
% 0.42/0.60 cnf(c51,negated_conjecture,god(skolem0001),inference(split_conjunct,[status(thm)],[c50])).
% 0.42/0.60 cnf(c146,plain,~god(X78)|absolutelyInfinite(X78),inference(split_conjunct,[status(thm)],[c144])).
% 0.42/0.60 cnf(c193,plain,absolutelyInfinite(skolem0001),inference(resolution,[status(thm)],[c146, c51])).
% 0.42/0.60 cnf(c195,plain,substance(skolem0001),inference(resolution,[status(thm)],[c193, c134])).
% 0.42/0.60 cnf(c171,plain,~substance(X86)|conceivedThruItself(X86),inference(split_conjunct,[status(thm)],[c169])).
% 0.42/0.60 cnf(c199,plain,conceivedThruItself(skolem0001),inference(resolution,[status(thm)],[c171, c195])).
% 0.42/0.60 cnf(c1,axiom,X84!=X85|~essenceInvExistence(X84)|essenceInvExistence(X85),theory(equality)).
% 0.42/0.60 cnf(c170,plain,~substance(X83)|inItself(X83),inference(split_conjunct,[status(thm)],[c169])).
% 0.42/0.60 cnf(c197,plain,inItself(skolem0001),inference(resolution,[status(thm)],[c170, c195])).
% 0.42/0.60 fof(attribute,axiom,(![X]:(attribute(X)<=>intPercAsConstEssSub(X))),file('/export/starexec/sandbox2/benchmark/Axioms/PHI002+0.ax', attribute)).
% 0.42/0.60 fof(c159,plain,(![X]:((~attribute(X)|intPercAsConstEssSub(X))&(~intPercAsConstEssSub(X)|attribute(X)))),inference(fof_nnf,[status(thm)],[attribute])).
% 0.42/0.60 fof(c160,plain,((![X]:(~attribute(X)|intPercAsConstEssSub(X)))&(![X]:(~intPercAsConstEssSub(X)|attribute(X)))),inference(shift_quantors,[status(thm)],[c159])).
% 0.42/0.60 fof(c162,plain,(![X53]:(![X54]:((~attribute(X53)|intPercAsConstEssSub(X53))&(~intPercAsConstEssSub(X54)|attribute(X54))))),inference(shift_quantors,[status(thm)],[fof(c161,plain,((![X53]:(~attribute(X53)|intPercAsConstEssSub(X53)))&(![X54]:(~intPercAsConstEssSub(X54)|attribute(X54)))),inference(variable_rename,[status(thm)],[c160])).])).
% 0.42/0.60 cnf(c164,plain,~intPercAsConstEssSub(X82)|attribute(X82),inference(split_conjunct,[status(thm)],[c162])).
% 0.42/0.60 cnf(c163,plain,~attribute(X81)|intPercAsConstEssSub(X81),inference(split_conjunct,[status(thm)],[c162])).
% 0.42/0.60 cnf(c0,axiom,X79!=X80|~selfCaused(X79)|selfCaused(X80),theory(equality)).
% 0.42/0.60 cnf(c135,plain,~absolutelyInfinite(X73)|constInInfAttributes(X73),inference(split_conjunct,[status(thm)],[c133])).
% 0.42/0.60 cnf(c194,plain,constInInfAttributes(skolem0001),inference(resolution,[status(thm)],[c193, c135])).
% 0.42/0.60 cnf(c145,plain,~god(X77)|being(X77),inference(split_conjunct,[status(thm)],[c144])).
% 0.42/0.60 cnf(c192,plain,being(skolem0001),inference(resolution,[status(thm)],[c145, c51])).
% 0.42/0.60 cnf(transitivity,axiom,X74!=X76|X76!=X75|X74=X75,theory(equality)).
% 0.42/0.60 cnf(c125,plain,~free(X71)|existsOnlyByNecessityOfOwnNature(X71),inference(split_conjunct,[status(thm)],[c124])).
% 0.42/0.60 fof(eternity,axiom,(![X]:(eternity(X)<=>existConcFollowFromDefEternal(X))),file('/export/starexec/sandbox2/benchmark/Axioms/PHI002+0.ax', eternity)).
% 0.42/0.60 fof(c103,plain,(![X]:((~eternity(X)|existConcFollowFromDefEternal(X))&(~existConcFollowFromDefEternal(X)|eternity(X)))),inference(fof_nnf,[status(thm)],[eternity])).
% 0.42/0.60 fof(c104,plain,((![X]:(~eternity(X)|existConcFollowFromDefEternal(X)))&(![X]:(~existConcFollowFromDefEternal(X)|eternity(X)))),inference(shift_quantors,[status(thm)],[c103])).
% 0.42/0.60 fof(c106,plain,(![X24]:(![X25]:((~eternity(X24)|existConcFollowFromDefEternal(X24))&(~existConcFollowFromDefEternal(X25)|eternity(X25))))),inference(shift_quantors,[status(thm)],[fof(c105,plain,((![X24]:(~eternity(X24)|existConcFollowFromDefEternal(X24)))&(![X25]:(~existConcFollowFromDefEternal(X25)|eternity(X25)))),inference(variable_rename,[status(thm)],[c104])).])).
% 0.42/0.60 cnf(c108,plain,~existConcFollowFromDefEternal(X70)|eternity(X70),inference(split_conjunct,[status(thm)],[c106])).
% 0.42/0.60 cnf(symmetry,axiom,X67!=X68|X68=X67,theory(equality)).
% 0.42/0.60 cnf(c107,plain,~eternity(X66)|existConcFollowFromDefEternal(X66),inference(split_conjunct,[status(thm)],[c106])).
% 0.42/0.60 fof(can_be_conceived_as_non_existing,axiom,(![X]:(canBeConceivedAsNonExisting(X)=>(~essenceInvExistence(X)))),file('/export/starexec/sandbox2/benchmark/Axioms/PHI002+1.ax', can_be_conceived_as_non_existing)).
% 0.42/0.60 fof(c53,plain,(![X]:(canBeConceivedAsNonExisting(X)=>~essenceInvExistence(X))),inference(fof_simplification,[status(thm)],[can_be_conceived_as_non_existing])).
% 0.42/0.60 fof(c54,plain,(![X]:(~canBeConceivedAsNonExisting(X)|~essenceInvExistence(X))),inference(fof_nnf,[status(thm)],[c53])).
% 0.42/0.60 fof(c55,plain,(![X3]:(~canBeConceivedAsNonExisting(X3)|~essenceInvExistence(X3))),inference(variable_rename,[status(thm)],[c54])).
% 0.42/0.60 cnf(c56,plain,~canBeConceivedAsNonExisting(X65)|~essenceInvExistence(X65),inference(split_conjunct,[status(thm)],[c55])).
% 0.42/0.60 cnf(c52,negated_conjecture,~exists(skolem0001),inference(split_conjunct,[status(thm)],[c50])).
% 0.42/0.60 % SZS output end Saturation
% 0.42/0.60
% 0.42/0.60 % Initial clauses : 107
% 0.42/0.60 % Processed clauses : 116
% 0.42/0.60 % Factors computed : 3
% 0.42/0.60 % Resolvents computed: 44
% 0.42/0.60 % Tautologies deleted: 31
% 0.42/0.60 % Forward subsumed : 7
% 0.42/0.60 % Backward subsumed : 3
% 0.42/0.60 % -------- CPU Time ---------
% 0.42/0.60 % User time : 0.259 s
% 0.42/0.60 % System time : 0.013 s
% 0.42/0.60 % Total time : 0.272 s
%------------------------------------------------------------------------------