%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PHI015+1 : TPTP v8.1.2. Released v7.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n027.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.55s 0.75s
% Output : Refutation 0.55s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : PHI015+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 : n027.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:08 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.55/0.75 % Version: 1.5
% 0.55/0.75 % SZS status Theorem
% 0.55/0.75 % SZS output start CNFRefutation
% 0.55/0.75 fof(definition_god,axiom,is_the(god,none_greater),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', definition_god)).
% 0.55/0.75 cnf(c8,plain,is_the(god,none_greater),inference(split_conjunct,[status(thm)],[definition_god])).
% 0.55/0.75 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.55/0.75 fof(c64,plain,(![X]:(![F]:(~is_the(X,F)|(property(F)&object(X))))),inference(fof_nnf,[status(thm)],[description_is_property_and_described_is_object])).
% 0.55/0.75 fof(c65,plain,(![X24]:(![X25]:(~is_the(X24,X25)|(property(X25)&object(X24))))),inference(variable_rename,[status(thm)],[c64])).
% 0.55/0.75 fof(c66,plain,(![X24]:(![X25]:((~is_the(X24,X25)|property(X25))&(~is_the(X24,X25)|object(X24))))),inference(distribute,[status(thm)],[c65])).
% 0.55/0.75 cnf(c68,plain,~is_the(X39,X40)|object(X39),inference(split_conjunct,[status(thm)],[c66])).
% 0.55/0.75 cnf(c83,plain,object(god),inference(resolution,[status(thm)],[c68, c8])).
% 0.55/0.75 cnf(reflexivity,axiom,X29=X29,theory(equality)).
% 0.55/0.75 cnf(c2,axiom,X53!=X56|X54!=X55|~exemplifies_property(X53,X54)|exemplifies_property(X56,X55),theory(equality)).
% 0.55/0.75 cnf(c67,plain,~is_the(X34,X35)|property(X35),inference(split_conjunct,[status(thm)],[c66])).
% 0.55/0.75 cnf(c79,plain,property(none_greater),inference(resolution,[status(thm)],[c67, c8])).
% 0.55/0.75 fof(description_axiom_identity_instance,axiom,(![F]:(![X]:(![W]:(((property(F)&object(X))&object(W))=>((is_the(X,F)&X=W)<=>(?[Y]:(((object(Y)&exemplifies_property(F,Y))&(![Z]:(object(Z)=>(exemplifies_property(F,Z)=>Z=Y))))&Y=W))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', description_axiom_identity_instance)).
% 0.55/0.75 fof(c34,plain,(![F]:(![X]:(![W]:(((~property(F)|~object(X))|~object(W))|(((~is_the(X,F)|X!=W)|(?[Y]:(((object(Y)&exemplifies_property(F,Y))&(![Z]:(~object(Z)|(~exemplifies_property(F,Z)|Z=Y))))&Y=W)))&((![Y]:(((~object(Y)|~exemplifies_property(F,Y))|(?[Z]:(object(Z)&(exemplifies_property(F,Z)&Z!=Y))))|Y!=W))|(is_the(X,F)&X=W))))))),inference(fof_nnf,[status(thm)],[description_axiom_identity_instance])).
% 0.55/0.75 fof(c35,plain,(![X10]:(![X11]:(![X12]:(((~property(X10)|~object(X11))|~object(X12))|(((~is_the(X11,X10)|X11!=X12)|(?[X13]:(((object(X13)&exemplifies_property(X10,X13))&(![X14]:(~object(X14)|(~exemplifies_property(X10,X14)|X14=X13))))&X13=X12)))&((![X15]:(((~object(X15)|~exemplifies_property(X10,X15))|(?[X16]:(object(X16)&(exemplifies_property(X10,X16)&X16!=X15))))|X15!=X12))|(is_the(X11,X10)&X11=X12))))))),inference(variable_rename,[status(thm)],[c34])).
% 0.55/0.75 fof(c37,plain,(![X10]:(![X11]:(![X12]:(![X14]:(![X15]:(((~property(X10)|~object(X11))|~object(X12))|(((~is_the(X11,X10)|X11!=X12)|(((object(skolem0004(X10,X11,X12))&exemplifies_property(X10,skolem0004(X10,X11,X12)))&(~object(X14)|(~exemplifies_property(X10,X14)|X14=skolem0004(X10,X11,X12))))&skolem0004(X10,X11,X12)=X12))&((((~object(X15)|~exemplifies_property(X10,X15))|(object(skolem0005(X10,X11,X12,X15))&(exemplifies_property(X10,skolem0005(X10,X11,X12,X15))&skolem0005(X10,X11,X12,X15)!=X15)))|X15!=X12)|(is_the(X11,X10)&X11=X12))))))))),inference(shift_quantors,[status(thm)],[fof(c36,plain,(![X10]:(![X11]:(![X12]:(((~property(X10)|~object(X11))|~object(X12))|(((~is_the(X11,X10)|X11!=X12)|(((object(skolem0004(X10,X11,X12))&exemplifies_property(X10,skolem0004(X10,X11,X12)))&(![X14]:(~object(X14)|(~exemplifies_property(X10,X14)|X14=skolem0004(X10,X11,X12)))))&skolem0004(X10,X11,X12)=X12))&((![X15]:(((~object(X15)|~exemplifies_property(X10,X15))|(object(skolem0005(X10,X11,X12,X15))&(exemplifies_property(X10,skolem0005(X10,X11,X12,X15))&skolem0005(X10,X11,X12,X15)!=X15)))|X15!=X12))|(is_the(X11,X10)&X11=X12))))))),inference(skolemize,[status(esa)],[c35])).])).
% 0.55/0.75 fof(c38,plain,(![X10]:(![X11]:(![X12]:(![X14]:(![X15]:(((((((~property(X10)|~object(X11))|~object(X12))|((~is_the(X11,X10)|X11!=X12)|object(skolem0004(X10,X11,X12))))&(((~property(X10)|~object(X11))|~object(X12))|((~is_the(X11,X10)|X11!=X12)|exemplifies_property(X10,skolem0004(X10,X11,X12)))))&(((~property(X10)|~object(X11))|~object(X12))|((~is_the(X11,X10)|X11!=X12)|(~object(X14)|(~exemplifies_property(X10,X14)|X14=skolem0004(X10,X11,X12))))))&(((~property(X10)|~object(X11))|~object(X12))|((~is_the(X11,X10)|X11!=X12)|skolem0004(X10,X11,X12)=X12)))&(((((~property(X10)|~object(X11))|~object(X12))|((((~object(X15)|~exemplifies_property(X10,X15))|object(skolem0005(X10,X11,X12,X15)))|X15!=X12)|is_the(X11,X10)))&(((~property(X10)|~object(X11))|~object(X12))|((((~object(X15)|~exemplifies_property(X10,X15))|object(skolem0005(X10,X11,X12,X15)))|X15!=X12)|X11=X12)))&(((((~property(X10)|~object(X11))|~object(X12))|((((~object(X15)|~exemplifies_property(X10,X15))|exemplifies_property(X10,skolem0005(X10,X11,X12,X15)))|X15!=X12)|is_the(X11,X10)))&(((~property(X10)|~object(X11))|~object(X12))|((((~object(X15)|~exemplifies_property(X10,X15))|exemplifies_property(X10,skolem0005(X10,X11,X12,X15)))|X15!=X12)|X11=X12)))&((((~property(X10)|~object(X11))|~object(X12))|((((~object(X15)|~exemplifies_property(X10,X15))|skolem0005(X10,X11,X12,X15)!=X15)|X15!=X12)|is_the(X11,X10)))&(((~property(X10)|~object(X11))|~object(X12))|((((~object(X15)|~exemplifies_property(X10,X15))|skolem0005(X10,X11,X12,X15)!=X15)|X15!=X12)|X11=X12))))))))))),inference(distribute,[status(thm)],[c37])).
% 0.55/0.75 cnf(c40,plain,~property(X102)|~object(X101)|~object(X103)|~is_the(X101,X102)|X101!=X103|exemplifies_property(X102,skolem0004(X102,X101,X103)),inference(split_conjunct,[status(thm)],[c38])).
% 0.55/0.75 cnf(c148,plain,~property(X104)|~object(X105)|~is_the(X105,X104)|exemplifies_property(X104,skolem0004(X104,X105,X105)),inference(resolution,[status(thm)],[c40, reflexivity])).
% 0.55/0.75 cnf(c149,plain,~property(none_greater)|~object(god)|exemplifies_property(none_greater,skolem0004(none_greater,god,god)),inference(resolution,[status(thm)],[c148, c8])).
% 0.55/0.75 cnf(c150,plain,~property(none_greater)|exemplifies_property(none_greater,skolem0004(none_greater,god,god)),inference(resolution,[status(thm)],[c149, c83])).
% 0.55/0.75 cnf(c151,plain,exemplifies_property(none_greater,skolem0004(none_greater,god,god)),inference(resolution,[status(thm)],[c150, c79])).
% 0.55/0.75 cnf(c155,plain,none_greater!=X111|skolem0004(none_greater,god,god)!=X110|exemplifies_property(X111,X110),inference(resolution,[status(thm)],[c151, c2])).
% 0.55/0.75 cnf(c42,plain,~property(X116)|~object(X115)|~object(X117)|~is_the(X115,X116)|X115!=X117|skolem0004(X116,X115,X117)=X117,inference(split_conjunct,[status(thm)],[c38])).
% 0.55/0.75 cnf(c162,plain,~property(X118)|~object(X119)|~is_the(X119,X118)|skolem0004(X118,X119,X119)=X119,inference(resolution,[status(thm)],[c42, reflexivity])).
% 0.55/0.75 cnf(c163,plain,~property(none_greater)|~object(god)|skolem0004(none_greater,god,god)=god,inference(resolution,[status(thm)],[c162, c8])).
% 0.55/0.75 cnf(c164,plain,~property(none_greater)|skolem0004(none_greater,god,god)=god,inference(resolution,[status(thm)],[c163, c83])).
% 0.55/0.75 cnf(c165,plain,skolem0004(none_greater,god,god)=god,inference(resolution,[status(thm)],[c164, c79])).
% 0.55/0.75 cnf(c172,plain,none_greater!=X120|exemplifies_property(X120,god),inference(resolution,[status(thm)],[c165, c155])).
% 0.55/0.75 cnf(c174,plain,exemplifies_property(none_greater,god),inference(resolution,[status(thm)],[c172, reflexivity])).
% 0.55/0.75 fof(god_exists,conjecture,exemplifies_property(existence,god),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', god_exists)).
% 0.55/0.75 fof(c5,negated_conjecture,(~exemplifies_property(existence,god)),inference(assume_negation,[status(cth)],[god_exists])).
% 0.55/0.75 fof(c6,negated_conjecture,~exemplifies_property(existence,god),inference(fof_simplification,[status(thm)],[c5])).
% 0.55/0.75 cnf(c7,negated_conjecture,~exemplifies_property(existence,god),inference(split_conjunct,[status(thm)],[c6])).
% 0.55/0.75 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.55/0.75 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.55/0.75 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.55/0.75 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.55/0.75 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.55/0.75 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.55/0.75 cnf(c14,plain,~object(X78)|~is_the(X78,none_greater)|exemplifies_property(existence,X78)|object(skolem0001(X78)),inference(split_conjunct,[status(thm)],[c13])).
% 0.55/0.75 cnf(c102,plain,~object(god)|exemplifies_property(existence,god)|object(skolem0001(god)),inference(resolution,[status(thm)],[c14, c8])).
% 0.55/0.75 cnf(c103,plain,exemplifies_property(existence,god)|object(skolem0001(god)),inference(resolution,[status(thm)],[c102, c83])).
% 0.55/0.75 cnf(c105,plain,object(skolem0001(god)),inference(resolution,[status(thm)],[c103, c7])).
% 0.55/0.75 cnf(c16,plain,~object(X81)|~is_the(X81,none_greater)|exemplifies_property(existence,X81)|exemplifies_property(conceivable,skolem0001(X81)),inference(split_conjunct,[status(thm)],[c13])).
% 0.55/0.75 cnf(c110,plain,~object(god)|exemplifies_property(existence,god)|exemplifies_property(conceivable,skolem0001(god)),inference(resolution,[status(thm)],[c16, c8])).
% 0.55/0.75 cnf(c111,plain,exemplifies_property(existence,god)|exemplifies_property(conceivable,skolem0001(god)),inference(resolution,[status(thm)],[c110, c83])).
% 0.55/0.75 cnf(c113,plain,exemplifies_property(conceivable,skolem0001(god)),inference(resolution,[status(thm)],[c111, c7])).
% 0.55/0.75 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.55/0.75 fof(c21,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.55/0.75 fof(c22,plain,(![X5]:(~object(X5)|((~exemplifies_property(none_greater,X5)|(exemplifies_property(conceivable,X5)&(![X6]:((~object(X6)|~exemplifies_relation(greater_than,X6,X5))|~exemplifies_property(conceivable,X6)))))&((~exemplifies_property(conceivable,X5)|(?[X7]:((object(X7)&exemplifies_relation(greater_than,X7,X5))&exemplifies_property(conceivable,X7))))|exemplifies_property(none_greater,X5))))),inference(variable_rename,[status(thm)],[c21])).
% 0.55/0.75 fof(c24,plain,(![X5]:(![X6]:(~object(X5)|((~exemplifies_property(none_greater,X5)|(exemplifies_property(conceivable,X5)&((~object(X6)|~exemplifies_relation(greater_than,X6,X5))|~exemplifies_property(conceivable,X6))))&((~exemplifies_property(conceivable,X5)|((object(skolem0003(X5))&exemplifies_relation(greater_than,skolem0003(X5),X5))&exemplifies_property(conceivable,skolem0003(X5))))|exemplifies_property(none_greater,X5)))))),inference(shift_quantors,[status(thm)],[fof(c23,plain,(![X5]:(~object(X5)|((~exemplifies_property(none_greater,X5)|(exemplifies_property(conceivable,X5)&(![X6]:((~object(X6)|~exemplifies_relation(greater_than,X6,X5))|~exemplifies_property(conceivable,X6)))))&((~exemplifies_property(conceivable,X5)|((object(skolem0003(X5))&exemplifies_relation(greater_than,skolem0003(X5),X5))&exemplifies_property(conceivable,skolem0003(X5))))|exemplifies_property(none_greater,X5))))),inference(skolemize,[status(esa)],[c22])).])).
% 0.55/0.75 fof(c25,plain,(![X5]:(![X6]:(((~object(X5)|(~exemplifies_property(none_greater,X5)|exemplifies_property(conceivable,X5)))&(~object(X5)|(~exemplifies_property(none_greater,X5)|((~object(X6)|~exemplifies_relation(greater_than,X6,X5))|~exemplifies_property(conceivable,X6)))))&(((~object(X5)|((~exemplifies_property(conceivable,X5)|object(skolem0003(X5)))|exemplifies_property(none_greater,X5)))&(~object(X5)|((~exemplifies_property(conceivable,X5)|exemplifies_relation(greater_than,skolem0003(X5),X5))|exemplifies_property(none_greater,X5))))&(~object(X5)|((~exemplifies_property(conceivable,X5)|exemplifies_property(conceivable,skolem0003(X5)))|exemplifies_property(none_greater,X5))))))),inference(distribute,[status(thm)],[c24])).
% 0.55/0.75 cnf(c27,plain,~object(X82)|~exemplifies_property(none_greater,X82)|~object(X83)|~exemplifies_relation(greater_than,X83,X82)|~exemplifies_property(conceivable,X83),inference(split_conjunct,[status(thm)],[c25])).
% 0.55/0.75 cnf(c15,plain,~object(X79)|~is_the(X79,none_greater)|exemplifies_property(existence,X79)|exemplifies_relation(greater_than,skolem0001(X79),X79),inference(split_conjunct,[status(thm)],[c13])).
% 0.55/0.75 cnf(c108,plain,~object(god)|exemplifies_property(existence,god)|exemplifies_relation(greater_than,skolem0001(god),god),inference(resolution,[status(thm)],[c15, c8])).
% 0.55/0.75 cnf(c130,plain,exemplifies_property(existence,god)|exemplifies_relation(greater_than,skolem0001(god),god),inference(resolution,[status(thm)],[c108, c83])).
% 0.55/0.75 cnf(c132,plain,exemplifies_relation(greater_than,skolem0001(god),god),inference(resolution,[status(thm)],[c130, c7])).
% 0.55/0.75 cnf(c142,plain,~object(god)|~exemplifies_property(none_greater,god)|~object(skolem0001(god))|~exemplifies_property(conceivable,skolem0001(god)),inference(resolution,[status(thm)],[c132, c27])).
% 0.55/0.75 cnf(c422,plain,~object(god)|~exemplifies_property(none_greater,god)|~object(skolem0001(god)),inference(resolution,[status(thm)],[c142, c113])).
% 0.55/0.75 cnf(c423,plain,~object(god)|~exemplifies_property(none_greater,god),inference(resolution,[status(thm)],[c422, c105])).
% 0.55/0.75 cnf(c424,plain,~object(god),inference(resolution,[status(thm)],[c423, c174])).
% 0.55/0.75 cnf(c425,plain,$false,inference(resolution,[status(thm)],[c424, c83])).
% 0.55/0.75 % SZS output end CNFRefutation
% 0.55/0.75
% 0.55/0.75 % Initial clauses : 46
% 0.55/0.75 % Processed clauses : 122
% 0.55/0.75 % Factors computed : 7
% 0.55/0.75 % Resolvents computed: 341
% 0.55/0.75 % Tautologies deleted: 4
% 0.55/0.75 % Forward subsumed : 69
% 0.55/0.75 % Backward subsumed : 19
% 0.55/0.75 % -------- CPU Time ---------
% 0.55/0.75 % User time : 0.397 s
% 0.55/0.75 % System time : 0.010 s
% 0.55/0.75 % Total time : 0.407 s
%------------------------------------------------------------------------------