%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PHI023+1 : TPTP v8.1.2. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:37:18 EDT 2024
% Result : Theorem 0.41s 0.61s
% Output : Refutation 0.41s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : PHI023+1 : TPTP v8.1.2. Released v7.4.0.
% 0.04/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.16/0.36 % Computer : n018.cluster.edu
% 0.16/0.36 % Model : x86_64 x86_64
% 0.16/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.36 % Memory : 8042.1875MB
% 0.16/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.36 % CPULimit : 300
% 0.16/0.36 % WCLimit : 300
% 0.16/0.36 % DateTime : Wed May 8 22:29:08 EDT 2024
% 0.16/0.36 % CPUTime :
% 0.41/0.61 % Version: 1.5
% 0.41/0.61 % SZS status Theorem
% 0.41/0.61 % SZS output start CNFRefutation
% 0.41/0.61 fof(if_god_then_exists,conjecture,(![X]:(god(X)=>exists(X))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', if_god_then_exists)).
% 0.41/0.61 fof(c48,negated_conjecture,(~(![X]:(god(X)=>exists(X)))),inference(assume_negation,[status(cth)],[if_god_then_exists])).
% 0.41/0.61 fof(c49,negated_conjecture,(?[X]:(god(X)&~exists(X))),inference(fof_nnf,[status(thm)],[c48])).
% 0.41/0.61 fof(c50,negated_conjecture,(?[X2]:(god(X2)&~exists(X2))),inference(variable_rename,[status(thm)],[c49])).
% 0.41/0.61 fof(c51,negated_conjecture,(god(skolem0001)&~exists(skolem0001)),inference(skolemize,[status(esa)],[c50])).
% 0.41/0.61 cnf(c53,negated_conjecture,~exists(skolem0001),inference(split_conjunct,[status(thm)],[c51])).
% 0.41/0.61 fof(is_in_itself_is_self_caused,axiom,(![X]:(inItself(X)=>selfCaused(X))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', is_in_itself_is_self_caused)).
% 0.41/0.61 fof(c60,plain,(![X]:(~inItself(X)|selfCaused(X))),inference(fof_nnf,[status(thm)],[is_in_itself_is_self_caused])).
% 0.41/0.61 fof(c61,plain,(![X5]:(~inItself(X5)|selfCaused(X5))),inference(variable_rename,[status(thm)],[c60])).
% 0.41/0.61 cnf(c62,plain,~inItself(X69)|selfCaused(X69),inference(split_conjunct,[status(thm)],[c61])).
% 0.41/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.41/0.61 fof(c139,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.41/0.61 fof(c140,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)],[c139])).
% 0.41/0.61 fof(c142,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(c141,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)],[c140])).])).
% 0.41/0.61 fof(c143,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)],[c142])).
% 0.41/0.61 cnf(c144,plain,~absolutelyInfinite(X80)|substance(X80),inference(split_conjunct,[status(thm)],[c143])).
% 0.41/0.61 cnf(c52,negated_conjecture,god(skolem0001),inference(split_conjunct,[status(thm)],[c51])).
% 0.41/0.61 fof(god,axiom,(![X]:(god(X)<=>(being(X)&absolutelyInfinite(X)))),file('/export/starexec/sandbox2/benchmark/Axioms/PHI002+0.ax', god)).
% 0.41/0.61 fof(c150,plain,(![X]:((~god(X)|(being(X)&absolutelyInfinite(X)))&((~being(X)|~absolutelyInfinite(X))|god(X)))),inference(fof_nnf,[status(thm)],[god])).
% 0.41/0.61 fof(c151,plain,((![X]:(~god(X)|(being(X)&absolutelyInfinite(X))))&(![X]:((~being(X)|~absolutelyInfinite(X))|god(X)))),inference(shift_quantors,[status(thm)],[c150])).
% 0.41/0.61 fof(c153,plain,(![X46]:(![X47]:((~god(X46)|(being(X46)&absolutelyInfinite(X46)))&((~being(X47)|~absolutelyInfinite(X47))|god(X47))))),inference(shift_quantors,[status(thm)],[fof(c152,plain,((![X46]:(~god(X46)|(being(X46)&absolutelyInfinite(X46))))&(![X47]:((~being(X47)|~absolutelyInfinite(X47))|god(X47)))),inference(variable_rename,[status(thm)],[c151])).])).
% 0.41/0.61 fof(c154,plain,(![X46]:(![X47]:(((~god(X46)|being(X46))&(~god(X46)|absolutelyInfinite(X46)))&((~being(X47)|~absolutelyInfinite(X47))|god(X47))))),inference(distribute,[status(thm)],[c153])).
% 0.41/0.61 cnf(c156,plain,~god(X85)|absolutelyInfinite(X85),inference(split_conjunct,[status(thm)],[c154])).
% 0.41/0.61 cnf(c205,plain,absolutelyInfinite(skolem0001),inference(resolution,[status(thm)],[c156, c52])).
% 0.41/0.61 cnf(c206,plain,substance(skolem0001),inference(resolution,[status(thm)],[c205, c144])).
% 0.41/0.61 fof(substance,axiom,(![X]:(substance(X)<=>(inItself(X)&conceivedThruItself(X)))),file('/export/starexec/sandbox2/benchmark/Axioms/PHI002+0.ax', substance)).
% 0.41/0.61 fof(c175,plain,(![X]:((~substance(X)|(inItself(X)&conceivedThruItself(X)))&((~inItself(X)|~conceivedThruItself(X))|substance(X)))),inference(fof_nnf,[status(thm)],[substance])).
% 0.41/0.61 fof(c176,plain,((![X]:(~substance(X)|(inItself(X)&conceivedThruItself(X))))&(![X]:((~inItself(X)|~conceivedThruItself(X))|substance(X)))),inference(shift_quantors,[status(thm)],[c175])).
% 0.41/0.61 fof(c178,plain,(![X58]:(![X59]:((~substance(X58)|(inItself(X58)&conceivedThruItself(X58)))&((~inItself(X59)|~conceivedThruItself(X59))|substance(X59))))),inference(shift_quantors,[status(thm)],[fof(c177,plain,((![X58]:(~substance(X58)|(inItself(X58)&conceivedThruItself(X58))))&(![X59]:((~inItself(X59)|~conceivedThruItself(X59))|substance(X59)))),inference(variable_rename,[status(thm)],[c176])).])).
% 0.41/0.61 fof(c179,plain,(![X58]:(![X59]:(((~substance(X58)|inItself(X58))&(~substance(X58)|conceivedThruItself(X58)))&((~inItself(X59)|~conceivedThruItself(X59))|substance(X59))))),inference(distribute,[status(thm)],[c178])).
% 0.41/0.61 cnf(c180,plain,~substance(X90)|inItself(X90),inference(split_conjunct,[status(thm)],[c179])).
% 0.41/0.61 cnf(c209,plain,inItself(skolem0001),inference(resolution,[status(thm)],[c180, c206])).
% 0.41/0.61 cnf(c210,plain,selfCaused(skolem0001),inference(resolution,[status(thm)],[c209, c62])).
% 0.41/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.41/0.61 fof(c191,plain,(![X]:((~selfCaused(X)|(essenceInvExistence(X)&natureConcOnlyByExistence(X)))&((~essenceInvExistence(X)|~natureConcOnlyByExistence(X))|selfCaused(X)))),inference(fof_nnf,[status(thm)],[self_caused])).
% 0.41/0.61 fof(c192,plain,((![X]:(~selfCaused(X)|(essenceInvExistence(X)&natureConcOnlyByExistence(X))))&(![X]:((~essenceInvExistence(X)|~natureConcOnlyByExistence(X))|selfCaused(X)))),inference(shift_quantors,[status(thm)],[c191])).
% 0.41/0.61 fof(c194,plain,(![X65]:(![X66]:((~selfCaused(X65)|(essenceInvExistence(X65)&natureConcOnlyByExistence(X65)))&((~essenceInvExistence(X66)|~natureConcOnlyByExistence(X66))|selfCaused(X66))))),inference(shift_quantors,[status(thm)],[fof(c193,plain,((![X65]:(~selfCaused(X65)|(essenceInvExistence(X65)&natureConcOnlyByExistence(X65))))&(![X66]:((~essenceInvExistence(X66)|~natureConcOnlyByExistence(X66))|selfCaused(X66)))),inference(variable_rename,[status(thm)],[c192])).])).
% 0.41/0.61 fof(c195,plain,(![X65]:(![X66]:(((~selfCaused(X65)|essenceInvExistence(X65))&(~selfCaused(X65)|natureConcOnlyByExistence(X65)))&((~essenceInvExistence(X66)|~natureConcOnlyByExistence(X66))|selfCaused(X66))))),inference(distribute,[status(thm)],[c194])).
% 0.41/0.61 cnf(c196,plain,~selfCaused(X94)|essenceInvExistence(X94),inference(split_conjunct,[status(thm)],[c195])).
% 0.41/0.61 cnf(c213,plain,essenceInvExistence(skolem0001),inference(resolution,[status(thm)],[c196, c210])).
% 0.41/0.61 fof(being_has_essense,axiom,(![X]:(being(X)=>hasEssence(X))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', being_has_essense)).
% 0.41/0.61 fof(c57,plain,(![X]:(~being(X)|hasEssence(X))),inference(fof_nnf,[status(thm)],[being_has_essense])).
% 0.41/0.61 fof(c58,plain,(![X4]:(~being(X4)|hasEssence(X4))),inference(variable_rename,[status(thm)],[c57])).
% 0.41/0.61 cnf(c59,plain,~being(X68)|hasEssence(X68),inference(split_conjunct,[status(thm)],[c58])).
% 0.41/0.61 cnf(c155,plain,~god(X82)|being(X82),inference(split_conjunct,[status(thm)],[c154])).
% 0.41/0.61 cnf(c202,plain,being(skolem0001),inference(resolution,[status(thm)],[c155, c52])).
% 0.41/0.61 cnf(c203,plain,hasEssence(skolem0001),inference(resolution,[status(thm)],[c202, c59])).
% 0.41/0.61 fof(essence_involves_existence_exists,axiom,(![X]:((essenceInvExistence(X)&hasEssence(X))=>exists(X))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', essence_involves_existence_exists)).
% 0.41/0.61 fof(c54,plain,(![X]:((~essenceInvExistence(X)|~hasEssence(X))|exists(X))),inference(fof_nnf,[status(thm)],[essence_involves_existence_exists])).
% 0.41/0.61 fof(c55,plain,(![X3]:((~essenceInvExistence(X3)|~hasEssence(X3))|exists(X3))),inference(variable_rename,[status(thm)],[c54])).
% 0.41/0.61 cnf(c56,plain,~essenceInvExistence(X154)|~hasEssence(X154)|exists(X154),inference(split_conjunct,[status(thm)],[c55])).
% 0.41/0.61 cnf(c221,plain,~essenceInvExistence(skolem0001)|exists(skolem0001),inference(resolution,[status(thm)],[c56, c203])).
% 0.41/0.61 cnf(c222,plain,exists(skolem0001),inference(resolution,[status(thm)],[c221, c213])).
% 0.41/0.61 cnf(c223,plain,$false,inference(resolution,[status(thm)],[c222, c53])).
% 0.41/0.61 % SZS output end CNFRefutation
% 0.41/0.61
% 0.41/0.61 % Initial clauses : 111
% 0.41/0.61 % Processed clauses : 61
% 0.41/0.61 % Factors computed : 2
% 0.41/0.61 % Resolvents computed: 24
% 0.41/0.61 % Tautologies deleted: 9
% 0.41/0.61 % Forward subsumed : 2
% 0.41/0.61 % Backward subsumed : 2
% 0.41/0.61 % -------- CPU Time ---------
% 0.41/0.61 % User time : 0.231 s
% 0.41/0.61 % System time : 0.012 s
% 0.41/0.61 % Total time : 0.243 s
%------------------------------------------------------------------------------