%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PHI022+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:17 EDT 2024
% Result : Theorem 0.40s 0.60s
% Output : Refutation 0.40s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : PHI022+1 : TPTP v8.1.2. Released v7.4.0.
% 0.07/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n018.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Wed May 8 22:29:53 EDT 2024
% 0.14/0.36 % CPUTime :
% 0.40/0.60 % Version: 1.5
% 0.40/0.60 % SZS status Theorem
% 0.40/0.60 % SZS output start CNFRefutation
% 0.40/0.60 fof(has_substance_exists,conjecture,(![X]:(substance(X)=>exists(X))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', has_substance_exists)).
% 0.40/0.60 fof(c48,negated_conjecture,(~(![X]:(substance(X)=>exists(X)))),inference(assume_negation,[status(cth)],[has_substance_exists])).
% 0.40/0.60 fof(c49,negated_conjecture,(?[X]:(substance(X)&~exists(X))),inference(fof_nnf,[status(thm)],[c48])).
% 0.40/0.60 fof(c50,negated_conjecture,(?[X2]:(substance(X2)&~exists(X2))),inference(variable_rename,[status(thm)],[c49])).
% 0.40/0.60 fof(c51,negated_conjecture,(substance(skolem0001)&~exists(skolem0001)),inference(skolemize,[status(esa)],[c50])).
% 0.40/0.60 cnf(c53,negated_conjecture,~exists(skolem0001),inference(split_conjunct,[status(thm)],[c51])).
% 0.40/0.60 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.40/0.60 fof(c60,plain,(![X]:(~inItself(X)|selfCaused(X))),inference(fof_nnf,[status(thm)],[is_in_itself_is_self_caused])).
% 0.40/0.60 fof(c61,plain,(![X5]:(~inItself(X5)|selfCaused(X5))),inference(variable_rename,[status(thm)],[c60])).
% 0.40/0.60 cnf(c62,plain,~inItself(X70)|selfCaused(X70),inference(split_conjunct,[status(thm)],[c61])).
% 0.40/0.60 cnf(c52,negated_conjecture,substance(skolem0001),inference(split_conjunct,[status(thm)],[c51])).
% 0.40/0.60 fof(substance,axiom,(![X]:(substance(X)<=>(inItself(X)&conceivedThruItself(X)))),file('/export/starexec/sandbox2/benchmark/Axioms/PHI002+0.ax', substance)).
% 0.40/0.60 fof(c178,plain,(![X]:((~substance(X)|(inItself(X)&conceivedThruItself(X)))&((~inItself(X)|~conceivedThruItself(X))|substance(X)))),inference(fof_nnf,[status(thm)],[substance])).
% 0.40/0.60 fof(c179,plain,((![X]:(~substance(X)|(inItself(X)&conceivedThruItself(X))))&(![X]:((~inItself(X)|~conceivedThruItself(X))|substance(X)))),inference(shift_quantors,[status(thm)],[c178])).
% 0.40/0.60 fof(c181,plain,(![X59]:(![X60]:((~substance(X59)|(inItself(X59)&conceivedThruItself(X59)))&((~inItself(X60)|~conceivedThruItself(X60))|substance(X60))))),inference(shift_quantors,[status(thm)],[fof(c180,plain,((![X59]:(~substance(X59)|(inItself(X59)&conceivedThruItself(X59))))&(![X60]:((~inItself(X60)|~conceivedThruItself(X60))|substance(X60)))),inference(variable_rename,[status(thm)],[c179])).])).
% 0.40/0.60 fof(c182,plain,(![X59]:(![X60]:(((~substance(X59)|inItself(X59))&(~substance(X59)|conceivedThruItself(X59)))&((~inItself(X60)|~conceivedThruItself(X60))|substance(X60))))),inference(distribute,[status(thm)],[c181])).
% 0.40/0.60 cnf(c183,plain,~substance(X90)|inItself(X90),inference(split_conjunct,[status(thm)],[c182])).
% 0.40/0.60 cnf(c208,plain,inItself(skolem0001),inference(resolution,[status(thm)],[c183, c52])).
% 0.40/0.60 cnf(c210,plain,selfCaused(skolem0001),inference(resolution,[status(thm)],[c208, c62])).
% 0.40/0.60 fof(self_caused,axiom,(![X]:(selfCaused(X)<=>(essenceInvExistence(X)&natureConcOnlyByExistence(X)))),file('/export/starexec/sandbox2/benchmark/Axioms/PHI002+0.ax', self_caused)).
% 0.40/0.60 fof(c194,plain,(![X]:((~selfCaused(X)|(essenceInvExistence(X)&natureConcOnlyByExistence(X)))&((~essenceInvExistence(X)|~natureConcOnlyByExistence(X))|selfCaused(X)))),inference(fof_nnf,[status(thm)],[self_caused])).
% 0.40/0.60 fof(c195,plain,((![X]:(~selfCaused(X)|(essenceInvExistence(X)&natureConcOnlyByExistence(X))))&(![X]:((~essenceInvExistence(X)|~natureConcOnlyByExistence(X))|selfCaused(X)))),inference(shift_quantors,[status(thm)],[c194])).
% 0.40/0.60 fof(c197,plain,(![X66]:(![X67]:((~selfCaused(X66)|(essenceInvExistence(X66)&natureConcOnlyByExistence(X66)))&((~essenceInvExistence(X67)|~natureConcOnlyByExistence(X67))|selfCaused(X67))))),inference(shift_quantors,[status(thm)],[fof(c196,plain,((![X66]:(~selfCaused(X66)|(essenceInvExistence(X66)&natureConcOnlyByExistence(X66))))&(![X67]:((~essenceInvExistence(X67)|~natureConcOnlyByExistence(X67))|selfCaused(X67)))),inference(variable_rename,[status(thm)],[c195])).])).
% 0.40/0.60 fof(c198,plain,(![X66]:(![X67]:(((~selfCaused(X66)|essenceInvExistence(X66))&(~selfCaused(X66)|natureConcOnlyByExistence(X66)))&((~essenceInvExistence(X67)|~natureConcOnlyByExistence(X67))|selfCaused(X67))))),inference(distribute,[status(thm)],[c197])).
% 0.40/0.60 cnf(c199,plain,~selfCaused(X94)|essenceInvExistence(X94),inference(split_conjunct,[status(thm)],[c198])).
% 0.40/0.60 cnf(c212,plain,essenceInvExistence(skolem0001),inference(resolution,[status(thm)],[c199, c210])).
% 0.40/0.60 fof(being_has_essense,axiom,(![X]:(being(X)=>hasEssence(X))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', being_has_essense)).
% 0.40/0.60 fof(c57,plain,(![X]:(~being(X)|hasEssence(X))),inference(fof_nnf,[status(thm)],[being_has_essense])).
% 0.40/0.60 fof(c58,plain,(![X4]:(~being(X4)|hasEssence(X4))),inference(variable_rename,[status(thm)],[c57])).
% 0.40/0.60 cnf(c59,plain,~being(X69)|hasEssence(X69),inference(split_conjunct,[status(thm)],[c58])).
% 0.40/0.60 fof(has_substance_being,axiom,(![X]:(substance(X)=>being(X))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', has_substance_being)).
% 0.40/0.60 fof(c63,plain,(![X]:(~substance(X)|being(X))),inference(fof_nnf,[status(thm)],[has_substance_being])).
% 0.40/0.60 fof(c64,plain,(![X6]:(~substance(X6)|being(X6))),inference(variable_rename,[status(thm)],[c63])).
% 0.40/0.60 cnf(c65,plain,~substance(X74)|being(X74),inference(split_conjunct,[status(thm)],[c64])).
% 0.40/0.60 cnf(c203,plain,being(skolem0001),inference(resolution,[status(thm)],[c65, c52])).
% 0.40/0.60 cnf(c204,plain,hasEssence(skolem0001),inference(resolution,[status(thm)],[c203, c59])).
% 0.40/0.60 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.40/0.60 fof(c54,plain,(![X]:((~essenceInvExistence(X)|~hasEssence(X))|exists(X))),inference(fof_nnf,[status(thm)],[essence_involves_existence_exists])).
% 0.40/0.60 fof(c55,plain,(![X3]:((~essenceInvExistence(X3)|~hasEssence(X3))|exists(X3))),inference(variable_rename,[status(thm)],[c54])).
% 0.40/0.60 cnf(c56,plain,~essenceInvExistence(X153)|~hasEssence(X153)|exists(X153),inference(split_conjunct,[status(thm)],[c55])).
% 0.40/0.60 cnf(c220,plain,~essenceInvExistence(skolem0001)|exists(skolem0001),inference(resolution,[status(thm)],[c56, c204])).
% 0.40/0.60 cnf(c222,plain,exists(skolem0001),inference(resolution,[status(thm)],[c220, c212])).
% 0.40/0.60 cnf(c223,plain,$false,inference(resolution,[status(thm)],[c222, c53])).
% 0.40/0.60 % SZS output end CNFRefutation
% 0.40/0.60
% 0.40/0.60 % Initial clauses : 112
% 0.40/0.60 % Processed clauses : 58
% 0.40/0.60 % Factors computed : 2
% 0.40/0.60 % Resolvents computed: 20
% 0.40/0.60 % Tautologies deleted: 9
% 0.40/0.60 % Forward subsumed : 2
% 0.40/0.60 % Backward subsumed : 2
% 0.40/0.60 % -------- CPU Time ---------
% 0.40/0.60 % User time : 0.226 s
% 0.40/0.60 % System time : 0.013 s
% 0.40/0.60 % Total time : 0.239 s
%------------------------------------------------------------------------------