%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PHI030+1 : TPTP v8.1.2. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n026.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.44s 0.68s
% Output : Saturation 0.44s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : PHI030+1 : TPTP v8.1.2. Released v7.4.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n026.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:38 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.44/0.68 % Version: 1.5
% 0.44/0.68 % SZS status CounterSatisfiable
% 0.44/0.68 % SZS output start Saturation
% 0.44/0.68 cnf(reflexivity,axiom,X67=X67,theory(equality)).
% 0.44/0.68 cnf(c40,axiom,X317!=X316|X315!=X318|~conceptionInvolves(X317,X315)|conceptionInvolves(X316,X318),theory(equality)).
% 0.44/0.68 fof(have_nothing_in_common,conjecture,(![X]:(![Y]:(haveNothingInCommon(X,Y)=>((((~canBeUnderstoodInTermsOf(X,Y))&(~canBeUnderstoodInTermsOf(Y,X)))&(~conceptionInvolves(X,Y)))&(~conceptionInvolves(Y,X)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', have_nothing_in_common)).
% 0.44/0.68 fof(c71,negated_conjecture,(~(![X]:(![Y]:(haveNothingInCommon(X,Y)=>((((~canBeUnderstoodInTermsOf(X,Y))&(~canBeUnderstoodInTermsOf(Y,X)))&(~conceptionInvolves(X,Y)))&(~conceptionInvolves(Y,X))))))),inference(assume_negation,[status(cth)],[have_nothing_in_common])).
% 0.44/0.68 fof(c72,negated_conjecture,(~(![X]:(![Y]:(haveNothingInCommon(X,Y)=>(((~canBeUnderstoodInTermsOf(X,Y)&~canBeUnderstoodInTermsOf(Y,X))&~conceptionInvolves(X,Y))&~conceptionInvolves(Y,X)))))),inference(fof_simplification,[status(thm)],[c71])).
% 0.44/0.68 fof(c73,negated_conjecture,(?[X]:(?[Y]:(haveNothingInCommon(X,Y)&(((canBeUnderstoodInTermsOf(X,Y)|canBeUnderstoodInTermsOf(Y,X))|conceptionInvolves(X,Y))|conceptionInvolves(Y,X))))),inference(fof_nnf,[status(thm)],[c72])).
% 0.44/0.68 fof(c74,negated_conjecture,(?[X10]:(?[X11]:(haveNothingInCommon(X10,X11)&(((canBeUnderstoodInTermsOf(X10,X11)|canBeUnderstoodInTermsOf(X11,X10))|conceptionInvolves(X10,X11))|conceptionInvolves(X11,X10))))),inference(variable_rename,[status(thm)],[c73])).
% 0.44/0.68 fof(c75,negated_conjecture,(haveNothingInCommon(skolem0001,skolem0002)&(((canBeUnderstoodInTermsOf(skolem0001,skolem0002)|canBeUnderstoodInTermsOf(skolem0002,skolem0001))|conceptionInvolves(skolem0001,skolem0002))|conceptionInvolves(skolem0002,skolem0001))),inference(skolemize,[status(esa)],[c74])).
% 0.44/0.68 cnf(c77,negated_conjecture,canBeUnderstoodInTermsOf(skolem0001,skolem0002)|canBeUnderstoodInTermsOf(skolem0002,skolem0001)|conceptionInvolves(skolem0001,skolem0002)|conceptionInvolves(skolem0002,skolem0001),inference(split_conjunct,[status(thm)],[c75])).
% 0.44/0.68 cnf(c240,plain,canBeUnderstoodInTermsOf(skolem0001,skolem0002)|canBeUnderstoodInTermsOf(skolem0002,skolem0001)|conceptionInvolves(skolem0001,skolem0002)|skolem0002!=X356|skolem0001!=X355|conceptionInvolves(X356,X355),inference(resolution,[status(thm)],[c77, c40])).
% 0.44/0.68 cnf(c247,plain,canBeUnderstoodInTermsOf(skolem0001,skolem0002)|canBeUnderstoodInTermsOf(skolem0002,skolem0001)|conceptionInvolves(skolem0001,skolem0002)|skolem0002!=X357|conceptionInvolves(X357,skolem0001),inference(resolution,[status(thm)],[c240, reflexivity])).
% 0.44/0.68 cnf(c239,plain,canBeUnderstoodInTermsOf(skolem0001,skolem0002)|canBeUnderstoodInTermsOf(skolem0002,skolem0001)|conceptionInvolves(skolem0002,skolem0001)|skolem0001!=X353|skolem0002!=X352|conceptionInvolves(X353,X352),inference(resolution,[status(thm)],[c77, c40])).
% 0.44/0.68 cnf(c245,plain,canBeUnderstoodInTermsOf(skolem0001,skolem0002)|canBeUnderstoodInTermsOf(skolem0002,skolem0001)|conceptionInvolves(skolem0002,skolem0001)|skolem0001!=X354|conceptionInvolves(X354,skolem0002),inference(resolution,[status(thm)],[c239, reflexivity])).
% 0.44/0.68 cnf(c41,axiom,X328!=X327|X326!=X329|~canBeUnderstoodInTermsOf(X328,X326)|canBeUnderstoodInTermsOf(X327,X329),theory(equality)).
% 0.44/0.68 cnf(c238,plain,canBeUnderstoodInTermsOf(skolem0001,skolem0002)|conceptionInvolves(skolem0001,skolem0002)|conceptionInvolves(skolem0002,skolem0001)|skolem0002!=X350|skolem0001!=X349|canBeUnderstoodInTermsOf(X350,X349),inference(resolution,[status(thm)],[c77, c41])).
% 0.44/0.68 cnf(c243,plain,canBeUnderstoodInTermsOf(skolem0001,skolem0002)|conceptionInvolves(skolem0001,skolem0002)|conceptionInvolves(skolem0002,skolem0001)|skolem0002!=X351|canBeUnderstoodInTermsOf(X351,skolem0001),inference(resolution,[status(thm)],[c238, reflexivity])).
% 0.44/0.68 cnf(c237,plain,canBeUnderstoodInTermsOf(skolem0002,skolem0001)|conceptionInvolves(skolem0001,skolem0002)|conceptionInvolves(skolem0002,skolem0001)|skolem0001!=X347|skolem0002!=X346|canBeUnderstoodInTermsOf(X347,X346),inference(resolution,[status(thm)],[c77, c41])).
% 0.44/0.68 cnf(c241,plain,canBeUnderstoodInTermsOf(skolem0002,skolem0001)|conceptionInvolves(skolem0001,skolem0002)|conceptionInvolves(skolem0002,skolem0001)|skolem0001!=X348|canBeUnderstoodInTermsOf(X348,skolem0002),inference(resolution,[status(thm)],[c237, reflexivity])).
% 0.44/0.68 fof(necessary,axiom,(![X]:(![Y]:(necessary(X)<=>(((externalTo(Y,X)&determinedByFixedMethod(X,Y))&determinedByDefiniteMethod(X,Y))&(isMethodAction(Y)|isMethodExistence(Y)))))),file('/export/starexec/sandbox/benchmark/Axioms/PHI002+0.ax', necessary)).
% 0.44/0.68 fof(c115,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.44/0.68 fof(c116,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)],[c115])).
% 0.44/0.68 fof(c118,plain,(![X29]:(![X30]:(![X31]:(![X32]:(![X33]:(![X34]:(![X35]:((~necessary(X29)|(((externalTo(X30,X29)&determinedByFixedMethod(X29,X31))&determinedByDefiniteMethod(X29,X32))&(isMethodAction(X33)|isMethodExistence(X33))))&((((~externalTo(X35,X34)|~determinedByFixedMethod(X34,X35))|~determinedByDefiniteMethod(X34,X35))|(~isMethodAction(X35)&~isMethodExistence(X35)))|necessary(X34)))))))))),inference(shift_quantors,[status(thm)],[fof(c117,plain,((![X29]:(~necessary(X29)|((((![X30]:externalTo(X30,X29))&(![X31]:determinedByFixedMethod(X29,X31)))&(![X32]:determinedByDefiniteMethod(X29,X32)))&(![X33]:(isMethodAction(X33)|isMethodExistence(X33))))))&(![X34]:((![X35]:(((~externalTo(X35,X34)|~determinedByFixedMethod(X34,X35))|~determinedByDefiniteMethod(X34,X35))|(~isMethodAction(X35)&~isMethodExistence(X35))))|necessary(X34)))),inference(variable_rename,[status(thm)],[c116])).])).
% 0.44/0.68 fof(c119,plain,(![X29]:(![X30]:(![X31]:(![X32]:(![X33]:(![X34]:(![X35]:(((((~necessary(X29)|externalTo(X30,X29))&(~necessary(X29)|determinedByFixedMethod(X29,X31)))&(~necessary(X29)|determinedByDefiniteMethod(X29,X32)))&(~necessary(X29)|(isMethodAction(X33)|isMethodExistence(X33))))&(((((~externalTo(X35,X34)|~determinedByFixedMethod(X34,X35))|~determinedByDefiniteMethod(X34,X35))|~isMethodAction(X35))|necessary(X34))&((((~externalTo(X35,X34)|~determinedByFixedMethod(X34,X35))|~determinedByDefiniteMethod(X34,X35))|~isMethodExistence(X35))|necessary(X34))))))))))),inference(distribute,[status(thm)],[c118])).
% 0.44/0.68 cnf(c125,plain,~externalTo(X345,X344)|~determinedByFixedMethod(X344,X345)|~determinedByDefiniteMethod(X344,X345)|~isMethodExistence(X345)|necessary(X344),inference(split_conjunct,[status(thm)],[c119])).
% 0.44/0.68 cnf(c124,plain,~externalTo(X343,X342)|~determinedByFixedMethod(X342,X343)|~determinedByDefiniteMethod(X342,X343)|~isMethodAction(X343)|necessary(X342),inference(split_conjunct,[status(thm)],[c119])).
% 0.44/0.68 cnf(c45,axiom,X340!=X339|X338!=X341|~objectOf(X340,X338)|objectOf(X339,X341),theory(equality)).
% 0.44/0.68 cnf(c44,axiom,X336!=X335|X334!=X337|~ideateOf(X336,X334)|ideateOf(X335,X337),theory(equality)).
% 0.44/0.68 cnf(c43,axiom,X332!=X331|X330!=X333|~correspondWith(X332,X330)|correspondWith(X331,X333),theory(equality)).
% 0.44/0.68 fof(absolutely_infinite,axiom,(![X]:(![Y]:(absolutelyInfinite(X)<=>((substance(X)&constInInfAttributes(X))&(attributeOf(Y,X)=>(expressesEternalEssentiality(Y)&expressesInfiniteEssentiality(Y))))))),file('/export/starexec/sandbox/benchmark/Axioms/PHI002+0.ax', absolutely_infinite)).
% 0.44/0.68 fof(c135,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.44/0.69 fof(c136,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)],[c135])).
% 0.44/0.69 fof(c138,plain,(![X41]:(![X42]:(![X43]:(![X44]:(![X45]:((~absolutelyInfinite(X41)|((substance(X41)&constInInfAttributes(X41))&(~attributeOf(X42,X41)|(expressesEternalEssentiality(X42)&expressesInfiniteEssentiality(X42)))))&(((~substance(X43)|~constInInfAttributes(X43))|(attributeOf(X44,X43)&(~expressesEternalEssentiality(X45)|~expressesInfiniteEssentiality(X45))))|absolutelyInfinite(X43)))))))),inference(shift_quantors,[status(thm)],[fof(c137,plain,((![X41]:(~absolutelyInfinite(X41)|((substance(X41)&constInInfAttributes(X41))&(![X42]:(~attributeOf(X42,X41)|(expressesEternalEssentiality(X42)&expressesInfiniteEssentiality(X42)))))))&(![X43]:(((~substance(X43)|~constInInfAttributes(X43))|((![X44]:attributeOf(X44,X43))&(![X45]:(~expressesEternalEssentiality(X45)|~expressesInfiniteEssentiality(X45)))))|absolutelyInfinite(X43)))),inference(variable_rename,[status(thm)],[c136])).])).
% 0.44/0.69 fof(c139,plain,(![X41]:(![X42]:(![X43]:(![X44]:(![X45]:((((~absolutelyInfinite(X41)|substance(X41))&(~absolutelyInfinite(X41)|constInInfAttributes(X41)))&((~absolutelyInfinite(X41)|(~attributeOf(X42,X41)|expressesEternalEssentiality(X42)))&(~absolutelyInfinite(X41)|(~attributeOf(X42,X41)|expressesInfiniteEssentiality(X42)))))&((((~substance(X43)|~constInInfAttributes(X43))|attributeOf(X44,X43))|absolutelyInfinite(X43))&(((~substance(X43)|~constInInfAttributes(X43))|(~expressesEternalEssentiality(X45)|~expressesInfiniteEssentiality(X45)))|absolutelyInfinite(X43))))))))),inference(distribute,[status(thm)],[c138])).
% 0.44/0.69 cnf(c145,plain,~substance(X324)|~constInInfAttributes(X324)|~expressesEternalEssentiality(X325)|~expressesInfiniteEssentiality(X325)|absolutelyInfinite(X324),inference(split_conjunct,[status(thm)],[c139])).
% 0.44/0.69 cnf(c76,negated_conjecture,haveNothingInCommon(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c75])).
% 0.44/0.69 cnf(c39,axiom,X303!=X302|X301!=X304|~haveNothingInCommon(X303,X301)|haveNothingInCommon(X302,X304),theory(equality)).
% 0.44/0.69 cnf(c231,plain,skolem0001!=X321|skolem0002!=X322|haveNothingInCommon(X321,X322),inference(resolution,[status(thm)],[c39, c76])).
% 0.44/0.69 cnf(c235,plain,skolem0001!=X323|haveNothingInCommon(X323,skolem0002),inference(resolution,[status(thm)],[c231, reflexivity])).
% 0.44/0.69 cnf(c144,plain,~substance(X319)|~constInInfAttributes(X319)|attributeOf(X320,X319)|absolutelyInfinite(X319),inference(split_conjunct,[status(thm)],[c139])).
% 0.44/0.69 fof(conceived_through,axiom,(![X]:(![Y]:((~conceivedThru(X,X))=>(conceivedThru(X,Y)&X!=Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', conceived_through)).
% 0.44/0.69 fof(c92,plain,(![X]:(![Y]:(~conceivedThru(X,X)=>(conceivedThru(X,Y)&X!=Y)))),inference(fof_simplification,[status(thm)],[conceived_through])).
% 0.44/0.69 fof(c93,plain,(![X]:(![Y]:(conceivedThru(X,X)|(conceivedThru(X,Y)&X!=Y)))),inference(fof_nnf,[status(thm)],[c92])).
% 0.44/0.69 fof(c94,plain,(![X]:(conceivedThru(X,X)|((![Y]:conceivedThru(X,Y))&(![Y]:X!=Y)))),inference(shift_quantors,[status(thm)],[c93])).
% 0.44/0.69 fof(c96,plain,(![X19]:(![X20]:(![X21]:(conceivedThru(X19,X19)|(conceivedThru(X19,X20)&X19!=X21))))),inference(shift_quantors,[status(thm)],[fof(c95,plain,(![X19]:(conceivedThru(X19,X19)|((![X20]:conceivedThru(X19,X20))&(![X21]:X19!=X21)))),inference(variable_rename,[status(thm)],[c94])).])).
% 0.44/0.69 fof(c97,plain,(![X19]:(![X20]:(![X21]:((conceivedThru(X19,X19)|conceivedThru(X19,X20))&(conceivedThru(X19,X19)|X19!=X21))))),inference(distribute,[status(thm)],[c96])).
% 0.44/0.69 cnf(c98,plain,conceivedThru(X122,X122)|conceivedThru(X122,X123),inference(split_conjunct,[status(thm)],[c97])).
% 0.44/0.69 cnf(c202,plain,conceivedThru(X128,X128),inference(factor,[status(thm)],[c98])).
% 0.44/0.69 cnf(c14,axiom,X189!=X188|X187!=X190|~conceivedThru(X189,X187)|conceivedThru(X188,X190),theory(equality)).
% 0.44/0.69 cnf(c215,plain,X309!=X307|X309!=X308|conceivedThru(X307,X308),inference(resolution,[status(thm)],[c14, c202])).
% 0.44/0.69 cnf(c233,plain,X313!=X312|conceivedThru(X312,X313),inference(resolution,[status(thm)],[c215, reflexivity])).
% 0.44/0.69 fof(finite_after_its_kind,axiom,(![X]:(![Y]:(finiteAfterItsKind(X)<=>(canBeLimitedBy(X,Y)&sameKind(X,Y))))),file('/export/starexec/sandbox/benchmark/Axioms/PHI002+0.ax', finite_after_its_kind)).
% 0.44/0.69 fof(c179,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.44/0.69 fof(c180,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)],[c179])).
% 0.44/0.69 fof(c182,plain,(![X60]:(![X61]:(![X62]:(![X63]:(![X64]:((~finiteAfterItsKind(X60)|(canBeLimitedBy(X60,X61)&sameKind(X60,X62)))&((~canBeLimitedBy(X63,X64)|~sameKind(X63,X64))|finiteAfterItsKind(X63)))))))),inference(shift_quantors,[status(thm)],[fof(c181,plain,((![X60]:(~finiteAfterItsKind(X60)|((![X61]:canBeLimitedBy(X60,X61))&(![X62]:sameKind(X60,X62)))))&(![X63]:((![X64]:(~canBeLimitedBy(X63,X64)|~sameKind(X63,X64)))|finiteAfterItsKind(X63)))),inference(variable_rename,[status(thm)],[c180])).])).
% 0.44/0.69 fof(c183,plain,(![X60]:(![X61]:(![X62]:(![X63]:(![X64]:(((~finiteAfterItsKind(X60)|canBeLimitedBy(X60,X61))&(~finiteAfterItsKind(X60)|sameKind(X60,X62)))&((~canBeLimitedBy(X63,X64)|~sameKind(X63,X64))|finiteAfterItsKind(X63)))))))),inference(distribute,[status(thm)],[c182])).
% 0.44/0.69 cnf(c186,plain,~canBeLimitedBy(X306,X305)|~sameKind(X306,X305)|finiteAfterItsKind(X306),inference(split_conjunct,[status(thm)],[c183])).
% 0.44/0.69 fof(mode,axiom,(![X]:(![Y]:(![Z]:(mode(X)<=>((modification(X,Y)&substance(Y))|(existsIn(X,Z)&conceivedThru(X,Z))))))),file('/export/starexec/sandbox/benchmark/Axioms/PHI002+0.ax', mode)).
% 0.44/0.69 fof(c154,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.44/0.69 fof(c155,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)],[c154])).
% 0.44/0.69 fof(c157,plain,(![X48]:(![X49]:(![X50]:(![X51]:(![X52]:(![X53]:(![X54]:(![X55]:((~mode(X48)|((modification(X48,X49)&substance(X50))|(existsIn(X48,X51)&conceivedThru(X48,X52))))&(((~modification(X53,X54)|~substance(X54))&(~existsIn(X53,X55)|~conceivedThru(X53,X55)))|mode(X53))))))))))),inference(shift_quantors,[status(thm)],[fof(c156,plain,((![X48]:(~mode(X48)|(((![X49]:modification(X48,X49))&(![X50]:substance(X50)))|((![X51]:existsIn(X48,X51))&(![X52]:conceivedThru(X48,X52))))))&(![X53]:(((![X54]:(~modification(X53,X54)|~substance(X54)))&(![X55]:(~existsIn(X53,X55)|~conceivedThru(X53,X55))))|mode(X53)))),inference(variable_rename,[status(thm)],[c155])).])).
% 0.44/0.69 fof(c158,plain,(![X48]:(![X49]:(![X50]:(![X51]:(![X52]:(![X53]:(![X54]:(![X55]:((((~mode(X48)|(modification(X48,X49)|existsIn(X48,X51)))&(~mode(X48)|(modification(X48,X49)|conceivedThru(X48,X52))))&((~mode(X48)|(substance(X50)|existsIn(X48,X51)))&(~mode(X48)|(substance(X50)|conceivedThru(X48,X52)))))&(((~modification(X53,X54)|~substance(X54))|mode(X53))&((~existsIn(X53,X55)|~conceivedThru(X53,X55))|mode(X53)))))))))))),inference(distribute,[status(thm)],[c157])).
% 0.44/0.69 cnf(c164,plain,~existsIn(X298,X299)|~conceivedThru(X298,X299)|mode(X298),inference(split_conjunct,[status(thm)],[c158])).
% 0.44/0.69 cnf(c230,plain,~existsIn(X300,X300)|mode(X300),inference(resolution,[status(thm)],[c164, c202])).
% 0.44/0.69 cnf(c160,plain,~mode(X296)|modification(X296,X295)|conceivedThru(X296,X297),inference(split_conjunct,[status(thm)],[c158])).
% 0.44/0.69 cnf(c159,plain,~mode(X293)|modification(X293,X292)|existsIn(X293,X294),inference(split_conjunct,[status(thm)],[c158])).
% 0.44/0.69 fof(free,axiom,(![X]:(![Y]:(free(X)<=>(existsOnlyByNecessityOfOwnNature(X)&(actionOf(Y,X)=>determinedByItselfAlone(Y,X)))))),file('/export/starexec/sandbox/benchmark/Axioms/PHI002+0.ax', free)).
% 0.44/0.69 fof(c126,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.44/0.69 fof(c127,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)],[c126])).
% 0.44/0.69 fof(c129,plain,(![X36]:(![X37]:(![X38]:(![X39]:(![X40]:((~free(X36)|(existsOnlyByNecessityOfOwnNature(X36)&(~actionOf(X37,X36)|determinedByItselfAlone(X37,X36))))&((~existsOnlyByNecessityOfOwnNature(X38)|(actionOf(X39,X38)&~determinedByItselfAlone(X40,X38)))|free(X38)))))))),inference(shift_quantors,[status(thm)],[fof(c128,plain,((![X36]:(~free(X36)|(existsOnlyByNecessityOfOwnNature(X36)&(![X37]:(~actionOf(X37,X36)|determinedByItselfAlone(X37,X36))))))&(![X38]:((~existsOnlyByNecessityOfOwnNature(X38)|((![X39]:actionOf(X39,X38))&(![X40]:~determinedByItselfAlone(X40,X38))))|free(X38)))),inference(variable_rename,[status(thm)],[c127])).])).
% 0.44/0.69 fof(c130,plain,(![X36]:(![X37]:(![X38]:(![X39]:(![X40]:(((~free(X36)|existsOnlyByNecessityOfOwnNature(X36))&(~free(X36)|(~actionOf(X37,X36)|determinedByItselfAlone(X37,X36))))&(((~existsOnlyByNecessityOfOwnNature(X38)|actionOf(X39,X38))|free(X38))&((~existsOnlyByNecessityOfOwnNature(X38)|~determinedByItselfAlone(X40,X38))|free(X38))))))))),inference(distribute,[status(thm)],[c129])).
% 0.44/0.69 cnf(c132,plain,~free(X291)|~actionOf(X290,X291)|determinedByItselfAlone(X290,X291),inference(split_conjunct,[status(thm)],[c130])).
% 0.44/0.69 cnf(c37,axiom,X288!=X287|X286!=X289|~knowledgeOfEffect(X288,X286)|knowledgeOfEffect(X287,X289),theory(equality)).
% 0.44/0.69 fof(exists,axiom,(![X]:(![Y]:(exists(X)<=>(existsIn(X,X)|(existsIn(X,Y)&X!=Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', exists)).
% 0.44/0.69 fof(c100,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.44/0.69 fof(c101,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)],[c100])).
% 0.44/0.69 fof(c103,plain,(![X22]:(![X23]:(![X24]:(![X25]:(![X26]:((~exists(X22)|(existsIn(X22,X22)|(existsIn(X22,X23)&X22!=X24)))&((~existsIn(X25,X25)&(~existsIn(X25,X26)|X25=X26))|exists(X25)))))))),inference(shift_quantors,[status(thm)],[fof(c102,plain,((![X22]:(~exists(X22)|(existsIn(X22,X22)|((![X23]:existsIn(X22,X23))&(![X24]:X22!=X24)))))&(![X25]:((~existsIn(X25,X25)&(![X26]:(~existsIn(X25,X26)|X25=X26)))|exists(X25)))),inference(variable_rename,[status(thm)],[c101])).])).
% 0.44/0.69 fof(c104,plain,(![X22]:(![X23]:(![X24]:(![X25]:(![X26]:(((~exists(X22)|(existsIn(X22,X22)|existsIn(X22,X23)))&(~exists(X22)|(existsIn(X22,X22)|X22!=X24)))&((~existsIn(X25,X25)|exists(X25))&((~existsIn(X25,X26)|X25=X26)|exists(X25))))))))),inference(distribute,[status(thm)],[c103])).
% 0.44/0.69 cnf(c108,plain,~existsIn(X284,X285)|X284=X285|exists(X284),inference(split_conjunct,[status(thm)],[c104])).
% 0.44/0.69 cnf(c106,plain,~exists(X282)|existsIn(X282,X282)|X282!=X281,inference(split_conjunct,[status(thm)],[c104])).
% 0.44/0.69 cnf(c229,plain,~exists(X283)|existsIn(X283,X283),inference(resolution,[status(thm)],[c106, reflexivity])).
% 0.44/0.69 fof(true_idea,axiom,(![X]:(![Y]:(trueIdea(X)=>(correspondWith(X,Y)&(ideateOf(Y,X)|objectOf(Y,X)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', true_idea)).
% 0.44/0.69 fof(c64,plain,(![X]:(![Y]:(~trueIdea(X)|(correspondWith(X,Y)&(ideateOf(Y,X)|objectOf(Y,X)))))),inference(fof_nnf,[status(thm)],[true_idea])).
% 0.44/0.69 fof(c65,plain,(![X]:(~trueIdea(X)|((![Y]:correspondWith(X,Y))&(![Y]:(ideateOf(Y,X)|objectOf(Y,X)))))),inference(shift_quantors,[status(thm)],[c64])).
% 0.44/0.69 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.44/0.69 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.44/0.69 cnf(c70,plain,~trueIdea(X277)|ideateOf(X278,X277)|objectOf(X278,X277),inference(split_conjunct,[status(thm)],[c68])).
% 0.44/0.69 cnf(c36,axiom,X275!=X274|X273!=X276|~effectNecessarilyFollowsFrom(X275,X273)|effectNecessarilyFollowsFrom(X274,X276),theory(equality)).
% 0.44/0.69 cnf(c163,plain,~modification(X271,X272)|~substance(X272)|mode(X271),inference(split_conjunct,[status(thm)],[c158])).
% 0.44/0.69 cnf(c162,plain,~mode(X268)|substance(X270)|conceivedThru(X268,X269),inference(split_conjunct,[status(thm)],[c158])).
% 0.44/0.69 cnf(c161,plain,~mode(X265)|substance(X266)|existsIn(X265,X267),inference(split_conjunct,[status(thm)],[c158])).
% 0.44/0.69 cnf(c143,plain,~absolutelyInfinite(X263)|~attributeOf(X264,X263)|expressesInfiniteEssentiality(X264),inference(split_conjunct,[status(thm)],[c139])).
% 0.44/0.69 cnf(c142,plain,~absolutelyInfinite(X261)|~attributeOf(X262,X261)|expressesEternalEssentiality(X262),inference(split_conjunct,[status(thm)],[c139])).
% 0.44/0.69 cnf(c31,axiom,X259!=X258|X257!=X260|~determinedByFixedMethod(X259,X257)|determinedByFixedMethod(X258,X260),theory(equality)).
% 0.44/0.69 cnf(c134,plain,~existsOnlyByNecessityOfOwnNature(X255)|~determinedByItselfAlone(X256,X255)|free(X255),inference(split_conjunct,[status(thm)],[c130])).
% 0.44/0.69 cnf(c133,plain,~existsOnlyByNecessityOfOwnNature(X253)|actionOf(X254,X253)|free(X253),inference(split_conjunct,[status(thm)],[c130])).
% 0.44/0.69 cnf(c47,axiom,X249!=X248|~hasEssence(X249)|hasEssence(X248),theory(equality)).
% 0.44/0.69 cnf(c30,axiom,X246!=X245|X244!=X247|~externalTo(X246,X244)|externalTo(X245,X247),theory(equality)).
% 0.44/0.69 cnf(c46,axiom,X242!=X241|~canBeConceivedAsNonExisting(X242)|canBeConceivedAsNonExisting(X241),theory(equality)).
% 0.44/0.69 cnf(c42,axiom,X239!=X238|~trueIdea(X239)|trueIdea(X238),theory(equality)).
% 0.44/0.69 cnf(c27,axiom,X235!=X234|X233!=X236|~determinedByDefiniteMethod(X235,X233)|determinedByDefiniteMethod(X234,X236),theory(equality)).
% 0.44/0.69 cnf(c38,axiom,X232!=X231|~knowledgeOfACause(X232)|knowledgeOfACause(X231),theory(equality)).
% 0.44/0.69 cnf(c35,axiom,X229!=X228|~definiteCause(X229)|definiteCause(X228),theory(equality)).
% 0.44/0.69 cnf(c34,axiom,X226!=X225|~exists(X226)|exists(X225),theory(equality)).
% 0.44/0.69 cnf(c25,axiom,X223!=X222|X221!=X224|~determinedByItselfAlone(X223,X221)|determinedByItselfAlone(X222,X224),theory(equality)).
% 0.44/0.69 cnf(c33,axiom,X219!=X218|~existConcFollowFromDefEternal(X219)|existConcFollowFromDefEternal(X218),theory(equality)).
% 0.44/0.69 cnf(c32,axiom,X216!=X215|~eternity(X216)|eternity(X215),theory(equality)).
% 0.44/0.69 cnf(c24,axiom,X212!=X211|X210!=X213|~actionOf(X212,X210)|actionOf(X211,X213),theory(equality)).
% 0.44/0.69 cnf(c29,axiom,X209!=X208|~isMethodExistence(X209)|isMethodExistence(X208),theory(equality)).
% 0.44/0.69 cnf(c28,axiom,X206!=X205|~isMethodAction(X206)|isMethodAction(X205),theory(equality)).
% 0.44/0.69 cnf(c26,axiom,X203!=X202|~necessary(X203)|necessary(X202),theory(equality)).
% 0.44/0.69 cnf(c19,axiom,X200!=X199|X198!=X201|~attributeOf(X200,X198)|attributeOf(X199,X201),theory(equality)).
% 0.44/0.69 cnf(c23,axiom,X196!=X195|~existsOnlyByNecessityOfOwnNature(X196)|existsOnlyByNecessityOfOwnNature(X195),theory(equality)).
% 0.44/0.69 cnf(c22,axiom,X193!=X192|~free(X193)|free(X192),theory(equality)).
% 0.44/0.69 cnf(c21,axiom,X186!=X185|~expressesInfiniteEssentiality(X186)|expressesInfiniteEssentiality(X185),theory(equality)).
% 0.44/0.69 cnf(c20,axiom,X183!=X182|~expressesEternalEssentiality(X183)|expressesEternalEssentiality(X182),theory(equality)).
% 0.44/0.69 cnf(c18,axiom,X180!=X179|~constInInfAttributes(X180)|constInInfAttributes(X179),theory(equality)).
% 0.44/0.69 cnf(c13,axiom,X177!=X176|X175!=X178|~existsIn(X177,X175)|existsIn(X176,X178),theory(equality)).
% 0.44/0.69 cnf(c17,axiom,X173!=X172|~absolutelyInfinite(X173)|absolutelyInfinite(X172),theory(equality)).
% 0.44/0.69 cnf(c16,axiom,X170!=X169|~being(X170)|being(X169),theory(equality)).
% 0.44/0.69 cnf(c12,axiom,X166!=X165|X164!=X167|~modification(X166,X164)|modification(X165,X167),theory(equality)).
% 0.44/0.69 cnf(c15,axiom,X163!=X162|~god(X163)|god(X162),theory(equality)).
% 0.44/0.69 cnf(c11,axiom,X160!=X159|~mode(X160)|mode(X159),theory(equality)).
% 0.44/0.69 cnf(c10,axiom,X156!=X155|~intPercAsConstEssSub(X156)|intPercAsConstEssSub(X155),theory(equality)).
% 0.44/0.69 cnf(c9,axiom,X154!=X153|~attribute(X154)|attribute(X153),theory(equality)).
% 0.44/0.69 cnf(c8,axiom,X151!=X150|~conceivedThruItself(X151)|conceivedThruItself(X150),theory(equality)).
% 0.44/0.69 cnf(c7,axiom,X147!=X146|~inItself(X147)|inItself(X146),theory(equality)).
% 0.44/0.69 cnf(c6,axiom,X145!=X144|~substance(X145)|substance(X144),theory(equality)).
% 0.44/0.69 fof(self_caused,axiom,(![X]:(selfCaused(X)<=>(essenceInvExistence(X)&natureConcOnlyByExistence(X)))),file('/export/starexec/sandbox/benchmark/Axioms/PHI002+0.ax', self_caused)).
% 0.44/0.69 fof(c187,plain,(![X]:((~selfCaused(X)|(essenceInvExistence(X)&natureConcOnlyByExistence(X)))&((~essenceInvExistence(X)|~natureConcOnlyByExistence(X))|selfCaused(X)))),inference(fof_nnf,[status(thm)],[self_caused])).
% 0.44/0.69 fof(c188,plain,((![X]:(~selfCaused(X)|(essenceInvExistence(X)&natureConcOnlyByExistence(X))))&(![X]:((~essenceInvExistence(X)|~natureConcOnlyByExistence(X))|selfCaused(X)))),inference(shift_quantors,[status(thm)],[c187])).
% 0.44/0.69 fof(c190,plain,(![X65]:(![X66]:((~selfCaused(X65)|(essenceInvExistence(X65)&natureConcOnlyByExistence(X65)))&((~essenceInvExistence(X66)|~natureConcOnlyByExistence(X66))|selfCaused(X66))))),inference(shift_quantors,[status(thm)],[fof(c189,plain,((![X65]:(~selfCaused(X65)|(essenceInvExistence(X65)&natureConcOnlyByExistence(X65))))&(![X66]:((~essenceInvExistence(X66)|~natureConcOnlyByExistence(X66))|selfCaused(X66)))),inference(variable_rename,[status(thm)],[c188])).])).
% 0.44/0.69 fof(c191,plain,(![X65]:(![X66]:(((~selfCaused(X65)|essenceInvExistence(X65))&(~selfCaused(X65)|natureConcOnlyByExistence(X65)))&((~essenceInvExistence(X66)|~natureConcOnlyByExistence(X66))|selfCaused(X66))))),inference(distribute,[status(thm)],[c190])).
% 0.44/0.69 cnf(c194,plain,~essenceInvExistence(X143)|~natureConcOnlyByExistence(X143)|selfCaused(X143),inference(split_conjunct,[status(thm)],[c191])).
% 0.44/0.69 fof(substance,axiom,(![X]:(substance(X)<=>(inItself(X)&conceivedThruItself(X)))),file('/export/starexec/sandbox/benchmark/Axioms/PHI002+0.ax', substance)).
% 0.44/0.69 fof(c171,plain,(![X]:((~substance(X)|(inItself(X)&conceivedThruItself(X)))&((~inItself(X)|~conceivedThruItself(X))|substance(X)))),inference(fof_nnf,[status(thm)],[substance])).
% 0.44/0.69 fof(c172,plain,((![X]:(~substance(X)|(inItself(X)&conceivedThruItself(X))))&(![X]:((~inItself(X)|~conceivedThruItself(X))|substance(X)))),inference(shift_quantors,[status(thm)],[c171])).
% 0.44/0.69 fof(c174,plain,(![X58]:(![X59]:((~substance(X58)|(inItself(X58)&conceivedThruItself(X58)))&((~inItself(X59)|~conceivedThruItself(X59))|substance(X59))))),inference(shift_quantors,[status(thm)],[fof(c173,plain,((![X58]:(~substance(X58)|(inItself(X58)&conceivedThruItself(X58))))&(![X59]:((~inItself(X59)|~conceivedThruItself(X59))|substance(X59)))),inference(variable_rename,[status(thm)],[c172])).])).
% 0.44/0.69 fof(c175,plain,(![X58]:(![X59]:(((~substance(X58)|inItself(X58))&(~substance(X58)|conceivedThruItself(X58)))&((~inItself(X59)|~conceivedThruItself(X59))|substance(X59))))),inference(distribute,[status(thm)],[c174])).
% 0.44/0.69 cnf(c178,plain,~inItself(X142)|~conceivedThruItself(X142)|substance(X142),inference(split_conjunct,[status(thm)],[c175])).
% 0.44/0.69 fof(god,axiom,(![X]:(god(X)<=>(being(X)&absolutelyInfinite(X)))),file('/export/starexec/sandbox/benchmark/Axioms/PHI002+0.ax', god)).
% 0.44/0.69 fof(c146,plain,(![X]:((~god(X)|(being(X)&absolutelyInfinite(X)))&((~being(X)|~absolutelyInfinite(X))|god(X)))),inference(fof_nnf,[status(thm)],[god])).
% 0.44/0.69 fof(c147,plain,((![X]:(~god(X)|(being(X)&absolutelyInfinite(X))))&(![X]:((~being(X)|~absolutelyInfinite(X))|god(X)))),inference(shift_quantors,[status(thm)],[c146])).
% 0.44/0.69 fof(c149,plain,(![X46]:(![X47]:((~god(X46)|(being(X46)&absolutelyInfinite(X46)))&((~being(X47)|~absolutelyInfinite(X47))|god(X47))))),inference(shift_quantors,[status(thm)],[fof(c148,plain,((![X46]:(~god(X46)|(being(X46)&absolutelyInfinite(X46))))&(![X47]:((~being(X47)|~absolutelyInfinite(X47))|god(X47)))),inference(variable_rename,[status(thm)],[c147])).])).
% 0.44/0.69 fof(c150,plain,(![X46]:(![X47]:(((~god(X46)|being(X46))&(~god(X46)|absolutelyInfinite(X46)))&((~being(X47)|~absolutelyInfinite(X47))|god(X47))))),inference(distribute,[status(thm)],[c149])).
% 0.44/0.69 cnf(c153,plain,~being(X141)|~absolutelyInfinite(X141)|god(X141),inference(split_conjunct,[status(thm)],[c150])).
% 0.44/0.69 cnf(c123,plain,~necessary(X139)|isMethodAction(X140)|isMethodExistence(X140),inference(split_conjunct,[status(thm)],[c119])).
% 0.44/0.69 cnf(c5,axiom,X137!=X136|X135!=X138|~sameKind(X137,X135)|sameKind(X136,X138),theory(equality)).
% 0.44/0.69 fof(essence_involves_existence_exists,axiom,(![X]:((essenceInvExistence(X)&hasEssence(X))=>exists(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', essence_involves_existence_exists)).
% 0.44/0.69 fof(c48,plain,(![X]:((~essenceInvExistence(X)|~hasEssence(X))|exists(X))),inference(fof_nnf,[status(thm)],[essence_involves_existence_exists])).
% 0.44/0.69 fof(c49,plain,(![X2]:((~essenceInvExistence(X2)|~hasEssence(X2))|exists(X2))),inference(variable_rename,[status(thm)],[c48])).
% 0.44/0.69 cnf(c50,plain,~essenceInvExistence(X134)|~hasEssence(X134)|exists(X134),inference(split_conjunct,[status(thm)],[c49])).
% 0.44/0.69 cnf(c4,axiom,X126!=X125|X124!=X127|~canBeLimitedBy(X126,X124)|canBeLimitedBy(X125,X127),theory(equality)).
% 0.44/0.69 cnf(c185,plain,~finiteAfterItsKind(X121)|sameKind(X121,X120),inference(split_conjunct,[status(thm)],[c183])).
% 0.44/0.69 cnf(c184,plain,~finiteAfterItsKind(X118)|canBeLimitedBy(X118,X119),inference(split_conjunct,[status(thm)],[c183])).
% 0.44/0.69 cnf(c122,plain,~necessary(X116)|determinedByDefiniteMethod(X116,X117),inference(split_conjunct,[status(thm)],[c119])).
% 0.44/0.69 cnf(c3,axiom,X114!=X113|~finiteAfterItsKind(X114)|finiteAfterItsKind(X113),theory(equality)).
% 0.44/0.69 cnf(c121,plain,~necessary(X111)|determinedByFixedMethod(X111,X112),inference(split_conjunct,[status(thm)],[c119])).
% 0.44/0.69 cnf(c120,plain,~necessary(X109)|externalTo(X110,X109),inference(split_conjunct,[status(thm)],[c119])).
% 0.44/0.69 cnf(c107,plain,~existsIn(X108,X108)|exists(X108),inference(split_conjunct,[status(thm)],[c104])).
% 0.44/0.69 fof(definite_cause,axiom,(![X]:(![Y]:(definiteCause(X)=>(effectNecessarilyFollowsFrom(Y,X)&((~definiteCause(X))=>(~effectNecessarilyFollowsFrom(Y,X))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', definite_cause)).
% 0.44/0.69 fof(c84,plain,(![X]:(![Y]:(definiteCause(X)=>(effectNecessarilyFollowsFrom(Y,X)&(~definiteCause(X)=>~effectNecessarilyFollowsFrom(Y,X)))))),inference(fof_simplification,[status(thm)],[definite_cause])).
% 0.44/0.69 fof(c85,plain,(![X]:(![Y]:(~definiteCause(X)|(effectNecessarilyFollowsFrom(Y,X)&(definiteCause(X)|~effectNecessarilyFollowsFrom(Y,X)))))),inference(fof_nnf,[status(thm)],[c84])).
% 0.44/0.69 fof(c86,plain,(![X]:(~definiteCause(X)|((![Y]:effectNecessarilyFollowsFrom(Y,X))&(definiteCause(X)|(![Y]:~effectNecessarilyFollowsFrom(Y,X)))))),inference(shift_quantors,[status(thm)],[c85])).
% 0.44/0.69 fof(c88,plain,(![X16]:(![X17]:(![X18]:(~definiteCause(X16)|(effectNecessarilyFollowsFrom(X17,X16)&(definiteCause(X16)|~effectNecessarilyFollowsFrom(X18,X16))))))),inference(shift_quantors,[status(thm)],[fof(c87,plain,(![X16]:(~definiteCause(X16)|((![X17]:effectNecessarilyFollowsFrom(X17,X16))&(definiteCause(X16)|(![X18]:~effectNecessarilyFollowsFrom(X18,X16)))))),inference(variable_rename,[status(thm)],[c86])).])).
% 0.44/0.69 fof(c89,plain,(![X16]:(![X17]:(![X18]:((~definiteCause(X16)|effectNecessarilyFollowsFrom(X17,X16))&(~definiteCause(X16)|(definiteCause(X16)|~effectNecessarilyFollowsFrom(X18,X16))))))),inference(distribute,[status(thm)],[c88])).
% 0.44/0.69 cnf(c90,plain,~definiteCause(X106)|effectNecessarilyFollowsFrom(X107,X106),inference(split_conjunct,[status(thm)],[c89])).
% 0.44/0.69 cnf(c2,axiom,X104!=X103|~natureConcOnlyByExistence(X104)|natureConcOnlyByExistence(X103),theory(equality)).
% 0.44/0.69 fof(knowledge_of_effect,axiom,(![X]:(![Y]:(knowledgeOfEffect(X,Y)<=>knowledgeOfACause(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', knowledge_of_effect)).
% 0.44/0.69 fof(c78,plain,(![X]:(![Y]:((~knowledgeOfEffect(X,Y)|knowledgeOfACause(X))&(~knowledgeOfACause(X)|knowledgeOfEffect(X,Y))))),inference(fof_nnf,[status(thm)],[knowledge_of_effect])).
% 0.44/0.69 fof(c79,plain,((![X]:((![Y]:~knowledgeOfEffect(X,Y))|knowledgeOfACause(X)))&(![X]:(~knowledgeOfACause(X)|(![Y]:knowledgeOfEffect(X,Y))))),inference(shift_quantors,[status(thm)],[c78])).
% 0.44/0.69 fof(c81,plain,(![X12]:(![X13]:(![X14]:(![X15]:((~knowledgeOfEffect(X12,X13)|knowledgeOfACause(X12))&(~knowledgeOfACause(X14)|knowledgeOfEffect(X14,X15))))))),inference(shift_quantors,[status(thm)],[fof(c80,plain,((![X12]:((![X13]:~knowledgeOfEffect(X12,X13))|knowledgeOfACause(X12)))&(![X14]:(~knowledgeOfACause(X14)|(![X15]:knowledgeOfEffect(X14,X15))))),inference(variable_rename,[status(thm)],[c79])).])).
% 0.44/0.69 cnf(c83,plain,~knowledgeOfACause(X102)|knowledgeOfEffect(X102,X101),inference(split_conjunct,[status(thm)],[c81])).
% 0.44/0.69 cnf(c82,plain,~knowledgeOfEffect(X100,X99)|knowledgeOfACause(X100),inference(split_conjunct,[status(thm)],[c81])).
% 0.44/0.69 cnf(c69,plain,~trueIdea(X97)|correspondWith(X97,X98),inference(split_conjunct,[status(thm)],[c68])).
% 0.44/0.69 cnf(c1,axiom,X94!=X93|~essenceInvExistence(X94)|essenceInvExistence(X93),theory(equality)).
% 0.44/0.69 cnf(c193,plain,~selfCaused(X92)|natureConcOnlyByExistence(X92),inference(split_conjunct,[status(thm)],[c191])).
% 0.44/0.69 cnf(c192,plain,~selfCaused(X91)|essenceInvExistence(X91),inference(split_conjunct,[status(thm)],[c191])).
% 0.44/0.69 cnf(c177,plain,~substance(X90)|conceivedThruItself(X90),inference(split_conjunct,[status(thm)],[c175])).
% 0.44/0.69 cnf(c176,plain,~substance(X89)|inItself(X89),inference(split_conjunct,[status(thm)],[c175])).
% 0.44/0.69 fof(attribute,axiom,(![X]:(attribute(X)<=>intPercAsConstEssSub(X))),file('/export/starexec/sandbox/benchmark/Axioms/PHI002+0.ax', attribute)).
% 0.44/0.69 fof(c165,plain,(![X]:((~attribute(X)|intPercAsConstEssSub(X))&(~intPercAsConstEssSub(X)|attribute(X)))),inference(fof_nnf,[status(thm)],[attribute])).
% 0.44/0.69 fof(c166,plain,((![X]:(~attribute(X)|intPercAsConstEssSub(X)))&(![X]:(~intPercAsConstEssSub(X)|attribute(X)))),inference(shift_quantors,[status(thm)],[c165])).
% 0.44/0.69 fof(c168,plain,(![X56]:(![X57]:((~attribute(X56)|intPercAsConstEssSub(X56))&(~intPercAsConstEssSub(X57)|attribute(X57))))),inference(shift_quantors,[status(thm)],[fof(c167,plain,((![X56]:(~attribute(X56)|intPercAsConstEssSub(X56)))&(![X57]:(~intPercAsConstEssSub(X57)|attribute(X57)))),inference(variable_rename,[status(thm)],[c166])).])).
% 0.44/0.69 cnf(c170,plain,~intPercAsConstEssSub(X88)|attribute(X88),inference(split_conjunct,[status(thm)],[c168])).
% 0.44/0.69 cnf(c0,axiom,X87!=X86|~selfCaused(X87)|selfCaused(X86),theory(equality)).
% 0.44/0.69 cnf(c169,plain,~attribute(X85)|intPercAsConstEssSub(X85),inference(split_conjunct,[status(thm)],[c168])).
% 0.44/0.69 cnf(c152,plain,~god(X84)|absolutelyInfinite(X84),inference(split_conjunct,[status(thm)],[c150])).
% 0.44/0.69 cnf(c151,plain,~god(X83)|being(X83),inference(split_conjunct,[status(thm)],[c150])).
% 0.44/0.69 cnf(c141,plain,~absolutelyInfinite(X82)|constInInfAttributes(X82),inference(split_conjunct,[status(thm)],[c139])).
% 0.44/0.69 cnf(c140,plain,~absolutelyInfinite(X81)|substance(X81),inference(split_conjunct,[status(thm)],[c139])).
% 0.44/0.69 cnf(transitivity,axiom,X80!=X78|X78!=X79|X80=X79,theory(equality)).
% 0.44/0.69 cnf(c131,plain,~free(X77)|existsOnlyByNecessityOfOwnNature(X77),inference(split_conjunct,[status(thm)],[c130])).
% 0.44/0.69 fof(eternity,axiom,(![X]:(eternity(X)<=>existConcFollowFromDefEternal(X))),file('/export/starexec/sandbox/benchmark/Axioms/PHI002+0.ax', eternity)).
% 0.44/0.69 fof(c109,plain,(![X]:((~eternity(X)|existConcFollowFromDefEternal(X))&(~existConcFollowFromDefEternal(X)|eternity(X)))),inference(fof_nnf,[status(thm)],[eternity])).
% 0.44/0.69 fof(c110,plain,((![X]:(~eternity(X)|existConcFollowFromDefEternal(X)))&(![X]:(~existConcFollowFromDefEternal(X)|eternity(X)))),inference(shift_quantors,[status(thm)],[c109])).
% 0.44/0.69 fof(c112,plain,(![X27]:(![X28]:((~eternity(X27)|existConcFollowFromDefEternal(X27))&(~existConcFollowFromDefEternal(X28)|eternity(X28))))),inference(shift_quantors,[status(thm)],[fof(c111,plain,((![X27]:(~eternity(X27)|existConcFollowFromDefEternal(X27)))&(![X28]:(~existConcFollowFromDefEternal(X28)|eternity(X28)))),inference(variable_rename,[status(thm)],[c110])).])).
% 0.44/0.69 cnf(c114,plain,~existConcFollowFromDefEternal(X76)|eternity(X76),inference(split_conjunct,[status(thm)],[c112])).
% 0.44/0.69 cnf(c113,plain,~eternity(X75)|existConcFollowFromDefEternal(X75),inference(split_conjunct,[status(thm)],[c112])).
% 0.44/0.69 cnf(symmetry,axiom,X73!=X72|X72=X73,theory(equality)).
% 0.44/0.69 fof(can_be_conceived_as_non_existing,axiom,(![X]:(canBeConceivedAsNonExisting(X)=>(~essenceInvExistence(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', can_be_conceived_as_non_existing)).
% 0.44/0.69 fof(c60,plain,(![X]:(canBeConceivedAsNonExisting(X)=>~essenceInvExistence(X))),inference(fof_simplification,[status(thm)],[can_be_conceived_as_non_existing])).
% 0.44/0.69 fof(c61,plain,(![X]:(~canBeConceivedAsNonExisting(X)|~essenceInvExistence(X))),inference(fof_nnf,[status(thm)],[c60])).
% 0.44/0.69 fof(c62,plain,(![X6]:(~canBeConceivedAsNonExisting(X6)|~essenceInvExistence(X6))),inference(variable_rename,[status(thm)],[c61])).
% 0.44/0.69 cnf(c63,plain,~canBeConceivedAsNonExisting(X71)|~essenceInvExistence(X71),inference(split_conjunct,[status(thm)],[c62])).
% 0.44/0.69 fof(has_substance_being,axiom,(![X]:(substance(X)=>being(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', has_substance_being)).
% 0.44/0.69 fof(c57,plain,(![X]:(~substance(X)|being(X))),inference(fof_nnf,[status(thm)],[has_substance_being])).
% 0.44/0.69 fof(c58,plain,(![X5]:(~substance(X5)|being(X5))),inference(variable_rename,[status(thm)],[c57])).
% 0.44/0.69 cnf(c59,plain,~substance(X70)|being(X70),inference(split_conjunct,[status(thm)],[c58])).
% 0.44/0.69 fof(is_in_itself_is_self_caused,axiom,(![X]:(inItself(X)=>selfCaused(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', is_in_itself_is_self_caused)).
% 0.44/0.69 fof(c54,plain,(![X]:(~inItself(X)|selfCaused(X))),inference(fof_nnf,[status(thm)],[is_in_itself_is_self_caused])).
% 0.44/0.69 fof(c55,plain,(![X4]:(~inItself(X4)|selfCaused(X4))),inference(variable_rename,[status(thm)],[c54])).
% 0.44/0.69 cnf(c56,plain,~inItself(X69)|selfCaused(X69),inference(split_conjunct,[status(thm)],[c55])).
% 0.44/0.69 fof(being_has_essense,axiom,(![X]:(being(X)=>hasEssence(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', being_has_essense)).
% 0.44/0.69 fof(c51,plain,(![X]:(~being(X)|hasEssence(X))),inference(fof_nnf,[status(thm)],[being_has_essense])).
% 0.44/0.69 fof(c52,plain,(![X3]:(~being(X3)|hasEssence(X3))),inference(variable_rename,[status(thm)],[c51])).
% 0.44/0.69 cnf(c53,plain,~being(X68)|hasEssence(X68),inference(split_conjunct,[status(thm)],[c52])).
% 0.44/0.69 % SZS output end Saturation
% 0.44/0.69
% 0.44/0.69 % Initial clauses : 108
% 0.44/0.69 % Processed clauses : 121
% 0.44/0.69 % Factors computed : 3
% 0.44/0.69 % Resolvents computed: 51
% 0.44/0.69 % Tautologies deleted: 32
% 0.44/0.69 % Forward subsumed : 9
% 0.44/0.69 % Backward subsumed : 3
% 0.44/0.69 % -------- CPU Time ---------
% 0.44/0.69 % User time : 0.315 s
% 0.44/0.69 % System time : 0.020 s
% 0.44/0.69 % Total time : 0.335 s
%------------------------------------------------------------------------------