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