%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET081+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n025.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:39:08 EDT 2024
% Result : Theorem 1.67s 1.89s
% Output : Refutation 1.67s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SET081+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n025.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Wed May 8 19:32:53 EDT 2024
% 0.14/0.34 % CPUTime :
% 1.67/1.89 % Version: 1.5
% 1.67/1.89 % SZS status Theorem
% 1.67/1.89 % SZS output start CNFRefutation
% 1.67/1.89 fof(only_member_in_singleton,conjecture,(![X]:(![Y]:(member(Y,singleton(X))=>Y=X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', only_member_in_singleton)).
% 1.67/1.89 fof(c26,negated_conjecture,(~(![X]:(![Y]:(member(Y,singleton(X))=>Y=X)))),inference(assume_negation,[status(cth)],[only_member_in_singleton])).
% 1.67/1.89 fof(c27,negated_conjecture,(?[X]:(?[Y]:(member(Y,singleton(X))&Y!=X))),inference(fof_nnf,[status(thm)],[c26])).
% 1.67/1.89 fof(c28,negated_conjecture,(?[X2]:(?[X3]:(member(X3,singleton(X2))&X3!=X2))),inference(variable_rename,[status(thm)],[c27])).
% 1.67/1.89 fof(c29,negated_conjecture,(member(skolem0002,singleton(skolem0001))&skolem0002!=skolem0001),inference(skolemize,[status(esa)],[c28])).
% 1.67/1.89 cnf(c31,negated_conjecture,skolem0002!=skolem0001,inference(split_conjunct,[status(thm)],[c29])).
% 1.67/1.89 fof(unordered_pair_defn,axiom,(![U]:(![X]:(![Y]:(member(U,unordered_pair(X,Y))<=>(member(U,universal_class)&(U=X|U=Y)))))),file('/export/starexec/sandbox/benchmark/Axioms/SET005+0.ax', unordered_pair_defn)).
% 1.67/1.89 fof(c231,plain,(![U]:(![X]:(![Y]:((~member(U,unordered_pair(X,Y))|(member(U,universal_class)&(U=X|U=Y)))&((~member(U,universal_class)|(U!=X&U!=Y))|member(U,unordered_pair(X,Y))))))),inference(fof_nnf,[status(thm)],[unordered_pair_defn])).
% 1.67/1.89 fof(c232,plain,((![U]:(![X]:(![Y]:(~member(U,unordered_pair(X,Y))|(member(U,universal_class)&(U=X|U=Y))))))&(![U]:(![X]:(![Y]:((~member(U,universal_class)|(U!=X&U!=Y))|member(U,unordered_pair(X,Y))))))),inference(shift_quantors,[status(thm)],[c231])).
% 1.67/1.89 fof(c234,plain,(![X123]:(![X124]:(![X125]:(![X126]:(![X127]:(![X128]:((~member(X123,unordered_pair(X124,X125))|(member(X123,universal_class)&(X123=X124|X123=X125)))&((~member(X126,universal_class)|(X126!=X127&X126!=X128))|member(X126,unordered_pair(X127,X128)))))))))),inference(shift_quantors,[status(thm)],[fof(c233,plain,((![X123]:(![X124]:(![X125]:(~member(X123,unordered_pair(X124,X125))|(member(X123,universal_class)&(X123=X124|X123=X125))))))&(![X126]:(![X127]:(![X128]:((~member(X126,universal_class)|(X126!=X127&X126!=X128))|member(X126,unordered_pair(X127,X128))))))),inference(variable_rename,[status(thm)],[c232])).])).
% 1.67/1.89 fof(c235,plain,(![X123]:(![X124]:(![X125]:(![X126]:(![X127]:(![X128]:(((~member(X123,unordered_pair(X124,X125))|member(X123,universal_class))&(~member(X123,unordered_pair(X124,X125))|(X123=X124|X123=X125)))&(((~member(X126,universal_class)|X126!=X127)|member(X126,unordered_pair(X127,X128)))&((~member(X126,universal_class)|X126!=X128)|member(X126,unordered_pair(X127,X128))))))))))),inference(distribute,[status(thm)],[c234])).
% 1.67/1.89 cnf(c237,plain,~member(X627,unordered_pair(X625,X626))|X627=X625|X627=X626,inference(split_conjunct,[status(thm)],[c235])).
% 1.67/1.89 fof(extensionality,axiom,(![X]:(![Y]:(X=Y<=>(subclass(X,Y)&subclass(Y,X))))),file('/export/starexec/sandbox/benchmark/Axioms/SET005+0.ax', extensionality)).
% 1.67/1.89 fof(c240,plain,(![X]:(![Y]:((X!=Y|(subclass(X,Y)&subclass(Y,X)))&((~subclass(X,Y)|~subclass(Y,X))|X=Y)))),inference(fof_nnf,[status(thm)],[extensionality])).
% 1.67/1.89 fof(c241,plain,((![X]:(![Y]:(X!=Y|(subclass(X,Y)&subclass(Y,X)))))&(![X]:(![Y]:((~subclass(X,Y)|~subclass(Y,X))|X=Y)))),inference(shift_quantors,[status(thm)],[c240])).
% 1.67/1.89 fof(c243,plain,(![X129]:(![X130]:(![X131]:(![X132]:((X129!=X130|(subclass(X129,X130)&subclass(X130,X129)))&((~subclass(X131,X132)|~subclass(X132,X131))|X131=X132)))))),inference(shift_quantors,[status(thm)],[fof(c242,plain,((![X129]:(![X130]:(X129!=X130|(subclass(X129,X130)&subclass(X130,X129)))))&(![X131]:(![X132]:((~subclass(X131,X132)|~subclass(X132,X131))|X131=X132)))),inference(variable_rename,[status(thm)],[c241])).])).
% 1.67/1.89 fof(c244,plain,(![X129]:(![X130]:(![X131]:(![X132]:(((X129!=X130|subclass(X129,X130))&(X129!=X130|subclass(X130,X129)))&((~subclass(X131,X132)|~subclass(X132,X131))|X131=X132)))))),inference(distribute,[status(thm)],[c243])).
% 1.67/1.89 cnf(c245,plain,X153!=X154|subclass(X153,X154),inference(split_conjunct,[status(thm)],[c244])).
% 1.67/1.89 fof(singleton_set_defn,axiom,(![X]:singleton(X)=unordered_pair(X,X)),file('/export/starexec/sandbox/benchmark/Axioms/SET005+0.ax', singleton_set_defn)).
% 1.67/1.89 fof(c227,plain,(![X120]:singleton(X120)=unordered_pair(X120,X120)),inference(variable_rename,[status(thm)],[singleton_set_defn])).
% 1.67/1.89 cnf(c228,plain,singleton(X169)=unordered_pair(X169,X169),inference(split_conjunct,[status(thm)],[c227])).
% 1.67/1.89 cnf(c271,plain,subclass(singleton(X170),unordered_pair(X170,X170)),inference(resolution,[status(thm)],[c228, c245])).
% 1.67/1.89 cnf(c30,negated_conjecture,member(skolem0002,singleton(skolem0001)),inference(split_conjunct,[status(thm)],[c29])).
% 1.67/1.89 fof(subclass_defn,axiom,(![X]:(![Y]:(subclass(X,Y)<=>(![U]:(member(U,X)=>member(U,Y)))))),file('/export/starexec/sandbox/benchmark/Axioms/SET005+0.ax', subclass_defn)).
% 1.67/1.89 fof(c250,plain,(![X]:(![Y]:((~subclass(X,Y)|(![U]:(~member(U,X)|member(U,Y))))&((?[U]:(member(U,X)&~member(U,Y)))|subclass(X,Y))))),inference(fof_nnf,[status(thm)],[subclass_defn])).
% 1.67/1.89 fof(c251,plain,((![X]:(![Y]:(~subclass(X,Y)|(![U]:(~member(U,X)|member(U,Y))))))&(![X]:(![Y]:((?[U]:(member(U,X)&~member(U,Y)))|subclass(X,Y))))),inference(shift_quantors,[status(thm)],[c250])).
% 1.67/1.89 fof(c252,plain,((![X134]:(![X135]:(~subclass(X134,X135)|(![X136]:(~member(X136,X134)|member(X136,X135))))))&(![X137]:(![X138]:((?[X139]:(member(X139,X137)&~member(X139,X138)))|subclass(X137,X138))))),inference(variable_rename,[status(thm)],[c251])).
% 1.67/1.89 fof(c254,plain,(![X134]:(![X135]:(![X136]:(![X137]:(![X138]:((~subclass(X134,X135)|(~member(X136,X134)|member(X136,X135)))&((member(skolem0009(X137,X138),X137)&~member(skolem0009(X137,X138),X138))|subclass(X137,X138)))))))),inference(shift_quantors,[status(thm)],[fof(c253,plain,((![X134]:(![X135]:(~subclass(X134,X135)|(![X136]:(~member(X136,X134)|member(X136,X135))))))&(![X137]:(![X138]:((member(skolem0009(X137,X138),X137)&~member(skolem0009(X137,X138),X138))|subclass(X137,X138))))),inference(skolemize,[status(esa)],[c252])).])).
% 1.67/1.89 fof(c255,plain,(![X134]:(![X135]:(![X136]:(![X137]:(![X138]:((~subclass(X134,X135)|(~member(X136,X134)|member(X136,X135)))&((member(skolem0009(X137,X138),X137)|subclass(X137,X138))&(~member(skolem0009(X137,X138),X138)|subclass(X137,X138))))))))),inference(distribute,[status(thm)],[c254])).
% 1.67/1.89 cnf(c256,plain,~subclass(X468,X470)|~member(X469,X468)|member(X469,X470),inference(split_conjunct,[status(thm)],[c255])).
% 1.67/1.89 cnf(c1322,plain,~subclass(singleton(skolem0001),X777)|member(skolem0002,X777),inference(resolution,[status(thm)],[c256, c30])).
% 1.67/1.89 cnf(c4196,plain,member(skolem0002,unordered_pair(skolem0001,skolem0001)),inference(resolution,[status(thm)],[c1322, c271])).
% 1.67/1.89 cnf(c4391,plain,skolem0002=skolem0001,inference(resolution,[status(thm)],[c4196, c237])).
% 1.67/1.89 cnf(c4463,plain,$false,inference(resolution,[status(thm)],[c4391, c31])).
% 1.67/1.89 % SZS output end CNFRefutation
% 1.67/1.89
% 1.67/1.89 % Initial clauses : 120
% 1.67/1.89 % Processed clauses : 373
% 1.67/1.89 % Factors computed : 22
% 1.67/1.89 % Resolvents computed: 4210
% 1.67/1.89 % Tautologies deleted: 4
% 1.67/1.89 % Forward subsumed : 279
% 1.67/1.89 % Backward subsumed : 2
% 1.67/1.89 % -------- CPU Time ---------
% 1.67/1.89 % User time : 1.496 s
% 1.67/1.89 % System time : 0.030 s
% 1.67/1.89 % Total time : 1.526 s
%------------------------------------------------------------------------------