%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PHI014+1 : TPTP v8.1.2. Released v7.2.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:16 EDT 2024
% Result : Theorem 0.40s 0.57s
% Output : Refutation 0.40s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : PHI014+1 : TPTP v8.1.2. Released v7.2.0.
% 0.13/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n018.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed May 8 22:29:23 EDT 2024
% 0.14/0.36 % CPUTime :
% 0.40/0.57 % Version: 1.5
% 0.40/0.57 % SZS status Theorem
% 0.40/0.57 % SZS output start CNFRefutation
% 0.40/0.57 fof(god_exists,conjecture,exemplifies_property(existence,god),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', god_exists)).
% 0.40/0.57 fof(c0,negated_conjecture,(~exemplifies_property(existence,god)),inference(assume_negation,[status(cth)],[god_exists])).
% 0.40/0.57 fof(c1,negated_conjecture,~exemplifies_property(existence,god),inference(fof_simplification,[status(thm)],[c0])).
% 0.40/0.57 cnf(c2,negated_conjecture,~exemplifies_property(existence,god),inference(split_conjunct,[status(thm)],[c1])).
% 0.40/0.57 fof(definition_god,axiom,is_the(god,none_greater),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', definition_god)).
% 0.40/0.57 cnf(c3,plain,is_the(god,none_greater),inference(split_conjunct,[status(thm)],[definition_god])).
% 0.40/0.57 fof(description_is_property_and_described_is_object,axiom,(![X]:(![F]:(is_the(X,F)=>(property(F)&object(X))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', description_is_property_and_described_is_object)).
% 0.40/0.57 fof(c22,plain,(![X]:(![F]:(~is_the(X,F)|(property(F)&object(X))))),inference(fof_nnf,[status(thm)],[description_is_property_and_described_is_object])).
% 0.40/0.57 fof(c23,plain,(![X7]:(![X8]:(~is_the(X7,X8)|(property(X8)&object(X7))))),inference(variable_rename,[status(thm)],[c22])).
% 0.40/0.57 fof(c24,plain,(![X7]:(![X8]:((~is_the(X7,X8)|property(X8))&(~is_the(X7,X8)|object(X7))))),inference(distribute,[status(thm)],[c23])).
% 0.40/0.57 cnf(c26,plain,~is_the(X14,X15)|object(X14),inference(split_conjunct,[status(thm)],[c24])).
% 0.40/0.57 cnf(c32,plain,object(god),inference(resolution,[status(thm)],[c26, c3])).
% 0.40/0.57 cnf(c25,plain,~is_the(X12,X13)|property(X13),inference(split_conjunct,[status(thm)],[c24])).
% 0.40/0.57 cnf(c31,plain,property(none_greater),inference(resolution,[status(thm)],[c25, c3])).
% 0.40/0.57 fof(description_theorem_2,axiom,(![F]:(property(F)=>((?[Y]:(object(Y)&is_the(Y,F)))=>(![Z]:(object(Z)=>(is_the(Z,F)=>exemplifies_property(F,Z))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', description_theorem_2)).
% 0.40/0.57 fof(c27,plain,(![F]:(~property(F)|((![Y]:(~object(Y)|~is_the(Y,F)))|(![Z]:(~object(Z)|(~is_the(Z,F)|exemplifies_property(F,Z))))))),inference(fof_nnf,[status(thm)],[description_theorem_2])).
% 0.40/0.57 fof(c29,plain,(![X9]:(![X10]:(![X11]:(~property(X9)|((~object(X10)|~is_the(X10,X9))|(~object(X11)|(~is_the(X11,X9)|exemplifies_property(X9,X11)))))))),inference(shift_quantors,[status(thm)],[fof(c28,plain,(![X9]:(~property(X9)|((![X10]:(~object(X10)|~is_the(X10,X9)))|(![X11]:(~object(X11)|(~is_the(X11,X9)|exemplifies_property(X9,X11))))))),inference(variable_rename,[status(thm)],[c27])).])).
% 0.40/0.57 cnf(c30,plain,~property(X26)|~object(X27)|~is_the(X27,X26)|~object(X25)|~is_the(X25,X26)|exemplifies_property(X26,X25),inference(split_conjunct,[status(thm)],[c29])).
% 0.40/0.57 cnf(c48,plain,~property(X28)|~object(X29)|~is_the(X29,X28)|exemplifies_property(X28,X29),inference(factor,[status(thm)],[c30])).
% 0.40/0.57 cnf(c50,plain,~property(none_greater)|~object(god)|exemplifies_property(none_greater,god),inference(resolution,[status(thm)],[c48, c3])).
% 0.40/0.57 cnf(c51,plain,~property(none_greater)|exemplifies_property(none_greater,god),inference(resolution,[status(thm)],[c50, c32])).
% 0.40/0.57 cnf(c52,plain,exemplifies_property(none_greater,god),inference(resolution,[status(thm)],[c51, c31])).
% 0.40/0.57 fof(premise_2,axiom,(![X]:(object(X)=>((is_the(X,none_greater)&(~exemplifies_property(existence,X)))=>(?[Y]:((object(Y)&exemplifies_relation(greater_than,Y,X))&exemplifies_property(conceivable,Y)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', premise_2)).
% 0.40/0.57 fof(c4,plain,(![X]:(object(X)=>((is_the(X,none_greater)&~exemplifies_property(existence,X))=>(?[Y]:((object(Y)&exemplifies_relation(greater_than,Y,X))&exemplifies_property(conceivable,Y)))))),inference(fof_simplification,[status(thm)],[premise_2])).
% 0.40/0.57 fof(c5,plain,(![X]:(~object(X)|((~is_the(X,none_greater)|exemplifies_property(existence,X))|(?[Y]:((object(Y)&exemplifies_relation(greater_than,Y,X))&exemplifies_property(conceivable,Y)))))),inference(fof_nnf,[status(thm)],[c4])).
% 0.40/0.57 fof(c6,plain,(![X2]:(~object(X2)|((~is_the(X2,none_greater)|exemplifies_property(existence,X2))|(?[X3]:((object(X3)&exemplifies_relation(greater_than,X3,X2))&exemplifies_property(conceivable,X3)))))),inference(variable_rename,[status(thm)],[c5])).
% 0.40/0.57 fof(c7,plain,(![X2]:(~object(X2)|((~is_the(X2,none_greater)|exemplifies_property(existence,X2))|((object(skolem0001(X2))&exemplifies_relation(greater_than,skolem0001(X2),X2))&exemplifies_property(conceivable,skolem0001(X2)))))),inference(skolemize,[status(esa)],[c6])).
% 0.40/0.57 fof(c8,plain,(![X2]:(((~object(X2)|((~is_the(X2,none_greater)|exemplifies_property(existence,X2))|object(skolem0001(X2))))&(~object(X2)|((~is_the(X2,none_greater)|exemplifies_property(existence,X2))|exemplifies_relation(greater_than,skolem0001(X2),X2))))&(~object(X2)|((~is_the(X2,none_greater)|exemplifies_property(existence,X2))|exemplifies_property(conceivable,skolem0001(X2)))))),inference(distribute,[status(thm)],[c7])).
% 0.40/0.57 cnf(c9,plain,~object(X16)|~is_the(X16,none_greater)|exemplifies_property(existence,X16)|object(skolem0001(X16)),inference(split_conjunct,[status(thm)],[c8])).
% 0.40/0.57 cnf(c33,plain,~object(god)|exemplifies_property(existence,god)|object(skolem0001(god)),inference(resolution,[status(thm)],[c9, c3])).
% 0.40/0.57 cnf(c34,plain,exemplifies_property(existence,god)|object(skolem0001(god)),inference(resolution,[status(thm)],[c33, c32])).
% 0.40/0.57 cnf(c35,plain,object(skolem0001(god)),inference(resolution,[status(thm)],[c34, c2])).
% 0.40/0.57 cnf(c11,plain,~object(X20)|~is_the(X20,none_greater)|exemplifies_property(existence,X20)|exemplifies_property(conceivable,skolem0001(X20)),inference(split_conjunct,[status(thm)],[c8])).
% 0.40/0.57 cnf(c37,plain,~object(god)|exemplifies_property(existence,god)|exemplifies_property(conceivable,skolem0001(god)),inference(resolution,[status(thm)],[c11, c3])).
% 0.40/0.57 cnf(c38,plain,exemplifies_property(existence,god)|exemplifies_property(conceivable,skolem0001(god)),inference(resolution,[status(thm)],[c37, c32])).
% 0.40/0.57 cnf(c39,plain,exemplifies_property(conceivable,skolem0001(god)),inference(resolution,[status(thm)],[c38, c2])).
% 0.40/0.57 fof(definition_none_greater,axiom,(![X]:(object(X)=>(exemplifies_property(none_greater,X)<=>(exemplifies_property(conceivable,X)&(~(?[Y]:((object(Y)&exemplifies_relation(greater_than,Y,X))&exemplifies_property(conceivable,Y)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', definition_none_greater)).
% 0.40/0.57 fof(c12,plain,(![X]:(~object(X)|((~exemplifies_property(none_greater,X)|(exemplifies_property(conceivable,X)&(![Y]:((~object(Y)|~exemplifies_relation(greater_than,Y,X))|~exemplifies_property(conceivable,Y)))))&((~exemplifies_property(conceivable,X)|(?[Y]:((object(Y)&exemplifies_relation(greater_than,Y,X))&exemplifies_property(conceivable,Y))))|exemplifies_property(none_greater,X))))),inference(fof_nnf,[status(thm)],[definition_none_greater])).
% 0.40/0.57 fof(c13,plain,(![X4]:(~object(X4)|((~exemplifies_property(none_greater,X4)|(exemplifies_property(conceivable,X4)&(![X5]:((~object(X5)|~exemplifies_relation(greater_than,X5,X4))|~exemplifies_property(conceivable,X5)))))&((~exemplifies_property(conceivable,X4)|(?[X6]:((object(X6)&exemplifies_relation(greater_than,X6,X4))&exemplifies_property(conceivable,X6))))|exemplifies_property(none_greater,X4))))),inference(variable_rename,[status(thm)],[c12])).
% 0.40/0.57 fof(c15,plain,(![X4]:(![X5]:(~object(X4)|((~exemplifies_property(none_greater,X4)|(exemplifies_property(conceivable,X4)&((~object(X5)|~exemplifies_relation(greater_than,X5,X4))|~exemplifies_property(conceivable,X5))))&((~exemplifies_property(conceivable,X4)|((object(skolem0002(X4))&exemplifies_relation(greater_than,skolem0002(X4),X4))&exemplifies_property(conceivable,skolem0002(X4))))|exemplifies_property(none_greater,X4)))))),inference(shift_quantors,[status(thm)],[fof(c14,plain,(![X4]:(~object(X4)|((~exemplifies_property(none_greater,X4)|(exemplifies_property(conceivable,X4)&(![X5]:((~object(X5)|~exemplifies_relation(greater_than,X5,X4))|~exemplifies_property(conceivable,X5)))))&((~exemplifies_property(conceivable,X4)|((object(skolem0002(X4))&exemplifies_relation(greater_than,skolem0002(X4),X4))&exemplifies_property(conceivable,skolem0002(X4))))|exemplifies_property(none_greater,X4))))),inference(skolemize,[status(esa)],[c13])).])).
% 0.40/0.57 fof(c16,plain,(![X4]:(![X5]:(((~object(X4)|(~exemplifies_property(none_greater,X4)|exemplifies_property(conceivable,X4)))&(~object(X4)|(~exemplifies_property(none_greater,X4)|((~object(X5)|~exemplifies_relation(greater_than,X5,X4))|~exemplifies_property(conceivable,X5)))))&(((~object(X4)|((~exemplifies_property(conceivable,X4)|object(skolem0002(X4)))|exemplifies_property(none_greater,X4)))&(~object(X4)|((~exemplifies_property(conceivable,X4)|exemplifies_relation(greater_than,skolem0002(X4),X4))|exemplifies_property(none_greater,X4))))&(~object(X4)|((~exemplifies_property(conceivable,X4)|exemplifies_property(conceivable,skolem0002(X4)))|exemplifies_property(none_greater,X4))))))),inference(distribute,[status(thm)],[c15])).
% 0.40/0.57 cnf(c18,plain,~object(X21)|~exemplifies_property(none_greater,X21)|~object(X22)|~exemplifies_relation(greater_than,X22,X21)|~exemplifies_property(conceivable,X22),inference(split_conjunct,[status(thm)],[c16])).
% 0.40/0.57 cnf(c10,plain,~object(X18)|~is_the(X18,none_greater)|exemplifies_property(existence,X18)|exemplifies_relation(greater_than,skolem0001(X18),X18),inference(split_conjunct,[status(thm)],[c8])).
% 0.40/0.57 cnf(c36,plain,~object(god)|exemplifies_property(existence,god)|exemplifies_relation(greater_than,skolem0001(god),god),inference(resolution,[status(thm)],[c10, c3])).
% 0.40/0.57 cnf(c43,plain,exemplifies_property(existence,god)|exemplifies_relation(greater_than,skolem0001(god),god),inference(resolution,[status(thm)],[c36, c32])).
% 0.40/0.57 cnf(c45,plain,exemplifies_property(existence,god)|~object(god)|~exemplifies_property(none_greater,god)|~object(skolem0001(god))|~exemplifies_property(conceivable,skolem0001(god)),inference(resolution,[status(thm)],[c43, c18])).
% 0.40/0.57 cnf(c66,plain,exemplifies_property(existence,god)|~object(god)|~exemplifies_property(none_greater,god)|~object(skolem0001(god)),inference(resolution,[status(thm)],[c45, c39])).
% 0.40/0.57 cnf(c67,plain,exemplifies_property(existence,god)|~object(god)|~exemplifies_property(none_greater,god),inference(resolution,[status(thm)],[c66, c35])).
% 0.40/0.57 cnf(c68,plain,exemplifies_property(existence,god)|~object(god),inference(resolution,[status(thm)],[c67, c52])).
% 0.40/0.57 cnf(c69,plain,exemplifies_property(existence,god),inference(resolution,[status(thm)],[c68, c32])).
% 0.40/0.57 cnf(c70,plain,$false,inference(resolution,[status(thm)],[c69, c2])).
% 0.40/0.57 % SZS output end CNFRefutation
% 0.40/0.57
% 0.40/0.57 % Initial clauses : 13
% 0.40/0.57 % Processed clauses : 40
% 0.40/0.57 % Factors computed : 1
% 0.40/0.57 % Resolvents computed: 39
% 0.40/0.57 % Tautologies deleted: 0
% 0.40/0.57 % Forward subsumed : 6
% 0.40/0.57 % Backward subsumed : 17
% 0.40/0.57 % -------- CPU Time ---------
% 0.40/0.57 % User time : 0.191 s
% 0.40/0.57 % System time : 0.018 s
% 0.40/0.57 % Total time : 0.209 s
%------------------------------------------------------------------------------