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