%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PHI010+1 : TPTP v8.1.2. Released v7.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n021.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.46s 0.67s
% Output : Refutation 0.46s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : PHI010+1 : TPTP v8.1.2. Released v7.2.0.
% 0.11/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n021.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 22:29:23 EDT 2024
% 0.13/0.36 % CPUTime :
% 0.46/0.67 % Version: 1.5
% 0.46/0.67 % SZS status Theorem
% 0.46/0.67 % SZS output start CNFRefutation
% 0.46/0.67 fof(lemma_1,conjecture,(![X]:(![F]:(![Y]:(((object(X)&property(F))&object(Y))=>((is_the(X,F)&X=Y)=>exemplifies_property(F,Y)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', lemma_1)).
% 0.46/0.67 fof(c4,negated_conjecture,(~(![X]:(![F]:(![Y]:(((object(X)&property(F))&object(Y))=>((is_the(X,F)&X=Y)=>exemplifies_property(F,Y))))))),inference(assume_negation,[status(cth)],[lemma_1])).
% 0.46/0.67 fof(c5,negated_conjecture,(?[X]:(?[F]:(?[Y]:(((object(X)&property(F))&object(Y))&((is_the(X,F)&X=Y)&~exemplifies_property(F,Y)))))),inference(fof_nnf,[status(thm)],[c4])).
% 0.46/0.67 fof(c6,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(((object(X2)&property(X3))&object(X4))&((is_the(X2,X3)&X2=X4)&~exemplifies_property(X3,X4)))))),inference(variable_rename,[status(thm)],[c5])).
% 0.46/0.67 fof(c7,negated_conjecture,(((object(skolem0001)&property(skolem0002))&object(skolem0003))&((is_the(skolem0001,skolem0002)&skolem0001=skolem0003)&~exemplifies_property(skolem0002,skolem0003))),inference(skolemize,[status(esa)],[c6])).
% 0.46/0.67 cnf(c13,negated_conjecture,~exemplifies_property(skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c7])).
% 0.46/0.67 cnf(reflexivity,axiom,X17=X17,theory(equality)).
% 0.46/0.67 cnf(c9,negated_conjecture,property(skolem0002),inference(split_conjunct,[status(thm)],[c7])).
% 0.46/0.67 cnf(c10,negated_conjecture,object(skolem0003),inference(split_conjunct,[status(thm)],[c7])).
% 0.46/0.67 cnf(c12,negated_conjecture,skolem0001=skolem0003,inference(split_conjunct,[status(thm)],[c7])).
% 0.46/0.67 cnf(c11,negated_conjecture,is_the(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c7])).
% 0.46/0.67 cnf(c3,axiom,X50!=X51|X49!=X48|~is_the(X50,X49)|is_the(X51,X48),theory(equality)).
% 0.46/0.67 cnf(c63,plain,skolem0001!=X53|skolem0002!=X52|is_the(X53,X52),inference(resolution,[status(thm)],[c3, c11])).
% 0.46/0.67 cnf(c64,plain,skolem0001!=X54|is_the(X54,skolem0002),inference(resolution,[status(thm)],[c63, reflexivity])).
% 0.46/0.67 cnf(c65,plain,is_the(skolem0003,skolem0002),inference(resolution,[status(thm)],[c64, c12])).
% 0.46/0.67 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/sandbox/benchmark/theBenchmark.p', description_axiom_identity_instance)).
% 0.46/0.67 fof(c14,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.46/0.67 fof(c15,plain,(![X5]:(![X6]:(![X7]:(((~property(X5)|~object(X6))|~object(X7))|(((~is_the(X6,X5)|X6!=X7)|(?[X8]:(((object(X8)&exemplifies_property(X5,X8))&(![X9]:(~object(X9)|(~exemplifies_property(X5,X9)|X9=X8))))&X8=X7)))&((![X10]:(((~object(X10)|~exemplifies_property(X5,X10))|(?[X11]:(object(X11)&(exemplifies_property(X5,X11)&X11!=X10))))|X10!=X7))|(is_the(X6,X5)&X6=X7))))))),inference(variable_rename,[status(thm)],[c14])).
% 0.46/0.67 fof(c17,plain,(![X5]:(![X6]:(![X7]:(![X9]:(![X10]:(((~property(X5)|~object(X6))|~object(X7))|(((~is_the(X6,X5)|X6!=X7)|(((object(skolem0004(X5,X6,X7))&exemplifies_property(X5,skolem0004(X5,X6,X7)))&(~object(X9)|(~exemplifies_property(X5,X9)|X9=skolem0004(X5,X6,X7))))&skolem0004(X5,X6,X7)=X7))&((((~object(X10)|~exemplifies_property(X5,X10))|(object(skolem0005(X5,X6,X7,X10))&(exemplifies_property(X5,skolem0005(X5,X6,X7,X10))&skolem0005(X5,X6,X7,X10)!=X10)))|X10!=X7)|(is_the(X6,X5)&X6=X7))))))))),inference(shift_quantors,[status(thm)],[fof(c16,plain,(![X5]:(![X6]:(![X7]:(((~property(X5)|~object(X6))|~object(X7))|(((~is_the(X6,X5)|X6!=X7)|(((object(skolem0004(X5,X6,X7))&exemplifies_property(X5,skolem0004(X5,X6,X7)))&(![X9]:(~object(X9)|(~exemplifies_property(X5,X9)|X9=skolem0004(X5,X6,X7)))))&skolem0004(X5,X6,X7)=X7))&((![X10]:(((~object(X10)|~exemplifies_property(X5,X10))|(object(skolem0005(X5,X6,X7,X10))&(exemplifies_property(X5,skolem0005(X5,X6,X7,X10))&skolem0005(X5,X6,X7,X10)!=X10)))|X10!=X7))|(is_the(X6,X5)&X6=X7))))))),inference(skolemize,[status(esa)],[c15])).])).
% 0.46/0.67 fof(c18,plain,(![X5]:(![X6]:(![X7]:(![X9]:(![X10]:(((((((~property(X5)|~object(X6))|~object(X7))|((~is_the(X6,X5)|X6!=X7)|object(skolem0004(X5,X6,X7))))&(((~property(X5)|~object(X6))|~object(X7))|((~is_the(X6,X5)|X6!=X7)|exemplifies_property(X5,skolem0004(X5,X6,X7)))))&(((~property(X5)|~object(X6))|~object(X7))|((~is_the(X6,X5)|X6!=X7)|(~object(X9)|(~exemplifies_property(X5,X9)|X9=skolem0004(X5,X6,X7))))))&(((~property(X5)|~object(X6))|~object(X7))|((~is_the(X6,X5)|X6!=X7)|skolem0004(X5,X6,X7)=X7)))&(((((~property(X5)|~object(X6))|~object(X7))|((((~object(X10)|~exemplifies_property(X5,X10))|object(skolem0005(X5,X6,X7,X10)))|X10!=X7)|is_the(X6,X5)))&(((~property(X5)|~object(X6))|~object(X7))|((((~object(X10)|~exemplifies_property(X5,X10))|object(skolem0005(X5,X6,X7,X10)))|X10!=X7)|X6=X7)))&(((((~property(X5)|~object(X6))|~object(X7))|((((~object(X10)|~exemplifies_property(X5,X10))|exemplifies_property(X5,skolem0005(X5,X6,X7,X10)))|X10!=X7)|is_the(X6,X5)))&(((~property(X5)|~object(X6))|~object(X7))|((((~object(X10)|~exemplifies_property(X5,X10))|exemplifies_property(X5,skolem0005(X5,X6,X7,X10)))|X10!=X7)|X6=X7)))&((((~property(X5)|~object(X6))|~object(X7))|((((~object(X10)|~exemplifies_property(X5,X10))|skolem0005(X5,X6,X7,X10)!=X10)|X10!=X7)|is_the(X6,X5)))&(((~property(X5)|~object(X6))|~object(X7))|((((~object(X10)|~exemplifies_property(X5,X10))|skolem0005(X5,X6,X7,X10)!=X10)|X10!=X7)|X6=X7))))))))))),inference(distribute,[status(thm)],[c17])).
% 0.46/0.67 cnf(c22,plain,~property(X74)|~object(X73)|~object(X72)|~is_the(X73,X74)|X73!=X72|skolem0004(X74,X73,X72)=X72,inference(split_conjunct,[status(thm)],[c18])).
% 0.46/0.67 cnf(c88,plain,~property(X76)|~object(X75)|~is_the(X75,X76)|skolem0004(X76,X75,X75)=X75,inference(resolution,[status(thm)],[c22, reflexivity])).
% 0.46/0.67 cnf(c90,plain,~property(skolem0002)|~object(skolem0003)|skolem0004(skolem0002,skolem0003,skolem0003)=skolem0003,inference(resolution,[status(thm)],[c88, c65])).
% 0.46/0.67 cnf(c110,plain,~property(skolem0002)|skolem0004(skolem0002,skolem0003,skolem0003)=skolem0003,inference(resolution,[status(thm)],[c90, c10])).
% 0.46/0.67 cnf(c111,plain,skolem0004(skolem0002,skolem0003,skolem0003)=skolem0003,inference(resolution,[status(thm)],[c110, c9])).
% 0.46/0.67 cnf(c2,axiom,X44!=X45|X43!=X42|~exemplifies_property(X44,X43)|exemplifies_property(X45,X42),theory(equality)).
% 0.46/0.67 cnf(c20,plain,~property(X63)|~object(X62)|~object(X61)|~is_the(X62,X63)|X62!=X61|exemplifies_property(X63,skolem0004(X63,X62,X61)),inference(split_conjunct,[status(thm)],[c18])).
% 0.46/0.67 cnf(c77,plain,~property(X67)|~object(X66)|~is_the(X66,X67)|exemplifies_property(X67,skolem0004(X67,X66,X66)),inference(resolution,[status(thm)],[c20, reflexivity])).
% 0.46/0.67 cnf(c81,plain,~property(skolem0002)|~object(skolem0003)|exemplifies_property(skolem0002,skolem0004(skolem0002,skolem0003,skolem0003)),inference(resolution,[status(thm)],[c77, c65])).
% 0.46/0.67 cnf(c92,plain,~property(skolem0002)|exemplifies_property(skolem0002,skolem0004(skolem0002,skolem0003,skolem0003)),inference(resolution,[status(thm)],[c81, c10])).
% 0.46/0.67 cnf(c93,plain,exemplifies_property(skolem0002,skolem0004(skolem0002,skolem0003,skolem0003)),inference(resolution,[status(thm)],[c92, c9])).
% 0.46/0.67 cnf(c97,plain,skolem0002!=X115|skolem0004(skolem0002,skolem0003,skolem0003)!=X114|exemplifies_property(X115,X114),inference(resolution,[status(thm)],[c93, c2])).
% 0.46/0.67 cnf(c256,plain,skolem0002!=X119|exemplifies_property(X119,skolem0003),inference(resolution,[status(thm)],[c97, c111])).
% 0.46/0.67 cnf(c263,plain,exemplifies_property(skolem0002,skolem0003),inference(resolution,[status(thm)],[c256, reflexivity])).
% 0.46/0.67 cnf(c264,plain,$false,inference(resolution,[status(thm)],[c263, c13])).
% 0.46/0.67 % SZS output end CNFRefutation
% 0.46/0.67
% 0.46/0.67 % Initial clauses : 28
% 0.46/0.67 % Processed clauses : 94
% 0.46/0.67 % Factors computed : 3
% 0.46/0.67 % Resolvents computed: 223
% 0.46/0.67 % Tautologies deleted: 4
% 0.46/0.67 % Forward subsumed : 55
% 0.46/0.67 % Backward subsumed : 12
% 0.46/0.67 % -------- CPU Time ---------
% 0.46/0.67 % User time : 0.283 s
% 0.46/0.67 % System time : 0.011 s
% 0.46/0.67 % Total time : 0.294 s
%------------------------------------------------------------------------------