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