%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PHI013+1 : TPTP v8.1.2. Released v7.2.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:16 EDT 2024
% Result : Theorem 0.83s 1.03s
% Output : Refutation 0.83s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : PHI013+1 : TPTP v8.1.2. Released v7.2.0.
% 0.12/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:23 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.83/1.03 % Version: 1.5
% 0.83/1.03 % SZS status Theorem
% 0.83/1.03 % SZS output start CNFRefutation
% 0.83/1.03 fof(definition_god,axiom,is_the(god,none_greater),file('/export/starexec/sandbox/benchmark/theBenchmark.p', definition_god)).
% 0.83/1.03 cnf(c8,plain,is_the(god,none_greater),inference(split_conjunct,[status(thm)],[definition_god])).
% 0.83/1.03 fof(description_is_property_and_described_is_object,axiom,(![X]:(![F]:(is_the(X,F)=>(property(F)&object(X))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', description_is_property_and_described_is_object)).
% 0.83/1.03 fof(c39,plain,(![X]:(![F]:(~is_the(X,F)|(property(F)&object(X))))),inference(fof_nnf,[status(thm)],[description_is_property_and_described_is_object])).
% 0.83/1.03 fof(c40,plain,(![X11]:(![X12]:(~is_the(X11,X12)|(property(X12)&object(X11))))),inference(variable_rename,[status(thm)],[c39])).
% 0.83/1.03 fof(c41,plain,(![X11]:(![X12]:((~is_the(X11,X12)|property(X12))&(~is_the(X11,X12)|object(X11))))),inference(distribute,[status(thm)],[c40])).
% 0.83/1.03 cnf(c43,plain,~is_the(X27,X26)|object(X27),inference(split_conjunct,[status(thm)],[c41])).
% 0.83/1.03 cnf(c61,plain,object(god),inference(resolution,[status(thm)],[c43, c8])).
% 0.83/1.03 cnf(c42,plain,~is_the(X25,X24)|property(X24),inference(split_conjunct,[status(thm)],[c41])).
% 0.83/1.03 cnf(c60,plain,property(none_greater),inference(resolution,[status(thm)],[c42, c8])).
% 0.83/1.03 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/sandbox/benchmark/theBenchmark.p', description_theorem_2)).
% 0.83/1.03 fof(c44,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.83/1.03 fof(c46,plain,(![X13]:(![X14]:(![X15]:(~property(X13)|((~object(X14)|~is_the(X14,X13))|(~object(X15)|(~is_the(X15,X13)|exemplifies_property(X13,X15)))))))),inference(shift_quantors,[status(thm)],[fof(c45,plain,(![X13]:(~property(X13)|((![X14]:(~object(X14)|~is_the(X14,X13)))|(![X15]:(~object(X15)|(~is_the(X15,X13)|exemplifies_property(X13,X15))))))),inference(variable_rename,[status(thm)],[c44])).])).
% 0.83/1.03 cnf(c47,plain,~property(X91)|~object(X90)|~is_the(X90,X91)|~object(X89)|~is_the(X89,X91)|exemplifies_property(X91,X89),inference(split_conjunct,[status(thm)],[c46])).
% 0.83/1.03 cnf(c134,plain,~property(X92)|~object(X93)|~is_the(X93,X92)|exemplifies_property(X92,X93),inference(factor,[status(thm)],[c47])).
% 0.83/1.03 cnf(c136,plain,~property(none_greater)|~object(god)|exemplifies_property(none_greater,god),inference(resolution,[status(thm)],[c134, c8])).
% 0.83/1.03 cnf(c137,plain,~property(none_greater)|exemplifies_property(none_greater,god),inference(resolution,[status(thm)],[c136, c61])).
% 0.83/1.03 cnf(c138,plain,exemplifies_property(none_greater,god),inference(resolution,[status(thm)],[c137, c60])).
% 0.83/1.03 fof(god_exists,conjecture,exemplifies_property(existence,god),file('/export/starexec/sandbox/benchmark/theBenchmark.p', god_exists)).
% 0.83/1.03 fof(c5,negated_conjecture,(~exemplifies_property(existence,god)),inference(assume_negation,[status(cth)],[god_exists])).
% 0.83/1.03 fof(c6,negated_conjecture,~exemplifies_property(existence,god),inference(fof_simplification,[status(thm)],[c5])).
% 0.83/1.03 cnf(c7,negated_conjecture,~exemplifies_property(existence,god),inference(split_conjunct,[status(thm)],[c6])).
% 0.83/1.03 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/sandbox/benchmark/theBenchmark.p', premise_2)).
% 0.83/1.03 fof(c9,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.83/1.03 fof(c10,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)],[c9])).
% 0.83/1.03 fof(c11,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)],[c10])).
% 0.83/1.03 fof(c12,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)],[c11])).
% 0.83/1.03 fof(c13,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)],[c12])).
% 0.83/1.03 cnf(c14,plain,~object(X60)|~is_the(X60,none_greater)|exemplifies_property(existence,X60)|object(skolem0001(X60)),inference(split_conjunct,[status(thm)],[c13])).
% 0.83/1.03 cnf(c81,plain,~object(god)|exemplifies_property(existence,god)|object(skolem0001(god)),inference(resolution,[status(thm)],[c14, c8])).
% 0.83/1.03 cnf(c92,plain,exemplifies_property(existence,god)|object(skolem0001(god)),inference(resolution,[status(thm)],[c81, c61])).
% 0.83/1.03 cnf(c93,plain,object(skolem0001(god)),inference(resolution,[status(thm)],[c92, c7])).
% 0.83/1.03 cnf(c16,plain,~object(X73)|~is_the(X73,none_greater)|exemplifies_property(existence,X73)|exemplifies_property(conceivable,skolem0001(X73)),inference(split_conjunct,[status(thm)],[c13])).
% 0.83/1.03 cnf(c90,plain,~object(god)|exemplifies_property(existence,god)|exemplifies_property(conceivable,skolem0001(god)),inference(resolution,[status(thm)],[c16, c8])).
% 0.83/1.03 cnf(c123,plain,exemplifies_property(existence,god)|exemplifies_property(conceivable,skolem0001(god)),inference(resolution,[status(thm)],[c90, c61])).
% 0.83/1.03 cnf(c124,plain,exemplifies_property(conceivable,skolem0001(god)),inference(resolution,[status(thm)],[c123, c7])).
% 0.83/1.03 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/sandbox/benchmark/theBenchmark.p', definition_none_greater)).
% 0.83/1.03 fof(c29,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.83/1.03 fof(c30,plain,(![X8]:(~object(X8)|((~exemplifies_property(none_greater,X8)|(exemplifies_property(conceivable,X8)&(![X9]:((~object(X9)|~exemplifies_relation(greater_than,X9,X8))|~exemplifies_property(conceivable,X9)))))&((~exemplifies_property(conceivable,X8)|(?[X10]:((object(X10)&exemplifies_relation(greater_than,X10,X8))&exemplifies_property(conceivable,X10))))|exemplifies_property(none_greater,X8))))),inference(variable_rename,[status(thm)],[c29])).
% 0.83/1.03 fof(c32,plain,(![X8]:(![X9]:(~object(X8)|((~exemplifies_property(none_greater,X8)|(exemplifies_property(conceivable,X8)&((~object(X9)|~exemplifies_relation(greater_than,X9,X8))|~exemplifies_property(conceivable,X9))))&((~exemplifies_property(conceivable,X8)|((object(skolem0004(X8))&exemplifies_relation(greater_than,skolem0004(X8),X8))&exemplifies_property(conceivable,skolem0004(X8))))|exemplifies_property(none_greater,X8)))))),inference(shift_quantors,[status(thm)],[fof(c31,plain,(![X8]:(~object(X8)|((~exemplifies_property(none_greater,X8)|(exemplifies_property(conceivable,X8)&(![X9]:((~object(X9)|~exemplifies_relation(greater_than,X9,X8))|~exemplifies_property(conceivable,X9)))))&((~exemplifies_property(conceivable,X8)|((object(skolem0004(X8))&exemplifies_relation(greater_than,skolem0004(X8),X8))&exemplifies_property(conceivable,skolem0004(X8))))|exemplifies_property(none_greater,X8))))),inference(skolemize,[status(esa)],[c30])).])).
% 0.83/1.03 fof(c33,plain,(![X8]:(![X9]:(((~object(X8)|(~exemplifies_property(none_greater,X8)|exemplifies_property(conceivable,X8)))&(~object(X8)|(~exemplifies_property(none_greater,X8)|((~object(X9)|~exemplifies_relation(greater_than,X9,X8))|~exemplifies_property(conceivable,X9)))))&(((~object(X8)|((~exemplifies_property(conceivable,X8)|object(skolem0004(X8)))|exemplifies_property(none_greater,X8)))&(~object(X8)|((~exemplifies_property(conceivable,X8)|exemplifies_relation(greater_than,skolem0004(X8),X8))|exemplifies_property(none_greater,X8))))&(~object(X8)|((~exemplifies_property(conceivable,X8)|exemplifies_property(conceivable,skolem0004(X8)))|exemplifies_property(none_greater,X8))))))),inference(distribute,[status(thm)],[c32])).
% 0.83/1.03 cnf(c35,plain,~object(X78)|~exemplifies_property(none_greater,X78)|~object(X79)|~exemplifies_relation(greater_than,X79,X78)|~exemplifies_property(conceivable,X79),inference(split_conjunct,[status(thm)],[c33])).
% 0.83/1.03 cnf(c15,plain,~object(X67)|~is_the(X67,none_greater)|exemplifies_property(existence,X67)|exemplifies_relation(greater_than,skolem0001(X67),X67),inference(split_conjunct,[status(thm)],[c13])).
% 0.83/1.03 cnf(c86,plain,~object(god)|exemplifies_property(existence,god)|exemplifies_relation(greater_than,skolem0001(god),god),inference(resolution,[status(thm)],[c15, c8])).
% 0.83/1.03 cnf(c220,plain,exemplifies_property(existence,god)|exemplifies_relation(greater_than,skolem0001(god),god),inference(resolution,[status(thm)],[c86, c61])).
% 0.83/1.03 cnf(c260,plain,exemplifies_relation(greater_than,skolem0001(god),god),inference(resolution,[status(thm)],[c220, c7])).
% 0.83/1.03 cnf(c265,plain,~object(god)|~exemplifies_property(none_greater,god)|~object(skolem0001(god))|~exemplifies_property(conceivable,skolem0001(god)),inference(resolution,[status(thm)],[c260, c35])).
% 0.83/1.03 cnf(c731,plain,~object(god)|~exemplifies_property(none_greater,god)|~object(skolem0001(god)),inference(resolution,[status(thm)],[c265, c124])).
% 0.83/1.03 cnf(c732,plain,~object(god)|~exemplifies_property(none_greater,god),inference(resolution,[status(thm)],[c731, c93])).
% 0.83/1.03 cnf(c733,plain,~object(god),inference(resolution,[status(thm)],[c732, c138])).
% 0.83/1.03 cnf(c734,plain,$false,inference(resolution,[status(thm)],[c733, c61])).
% 0.83/1.03 % SZS output end CNFRefutation
% 0.83/1.03
% 0.83/1.03 % Initial clauses : 32
% 0.83/1.03 % Processed clauses : 261
% 0.83/1.03 % Factors computed : 3
% 0.83/1.03 % Resolvents computed: 673
% 0.83/1.03 % Tautologies deleted: 4
% 0.83/1.03 % Forward subsumed : 191
% 0.83/1.03 % Backward subsumed : 98
% 0.83/1.03 % -------- CPU Time ---------
% 0.83/1.03 % User time : 0.666 s
% 0.83/1.03 % System time : 0.020 s
% 0.83/1.03 % Total time : 0.686 s
%------------------------------------------------------------------------------