%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET056+1 : TPTP v8.1.2. Bugfixed v5.4.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:39:00 EDT 2024
% Result : Theorem 9.93s 10.18s
% Output : Refutation 9.93s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : SET056+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% 0.08/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 19:17:08 EDT 2024
% 0.13/0.34 % CPUTime :
% 9.93/10.18 % Version: 1.5
% 9.93/10.18 % SZS status Theorem
% 9.93/10.18 % SZS output start CNFRefutation
% 9.93/10.18 fof(equality1,conjecture,(![X]:(![Y]:((X=Y|(?[U]:(member(U,X)&(~member(U,Y)))))|(?[W]:(member(W,Y)&(~member(W,X))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', equality1)).
% 9.93/10.18 fof(c26,negated_conjecture,(~(![X]:(![Y]:((X=Y|(?[U]:(member(U,X)&(~member(U,Y)))))|(?[W]:(member(W,Y)&(~member(W,X)))))))),inference(assume_negation,[status(cth)],[equality1])).
% 9.93/10.18 fof(c27,negated_conjecture,(~(![X]:(![Y]:((X=Y|(?[U]:(member(U,X)&~member(U,Y))))|(?[W]:(member(W,Y)&~member(W,X))))))),inference(fof_simplification,[status(thm)],[c26])).
% 9.93/10.18 fof(c28,negated_conjecture,(?[X]:(?[Y]:((X!=Y&(![U]:(~member(U,X)|member(U,Y))))&(![W]:(~member(W,Y)|member(W,X)))))),inference(fof_nnf,[status(thm)],[c27])).
% 9.93/10.18 fof(c29,negated_conjecture,(?[X2]:(?[X3]:((X2!=X3&(![X4]:(~member(X4,X2)|member(X4,X3))))&(![X5]:(~member(X5,X3)|member(X5,X2)))))),inference(variable_rename,[status(thm)],[c28])).
% 9.93/10.18 fof(c31,negated_conjecture,(![X4]:(![X5]:((skolem0001!=skolem0002&(~member(X4,skolem0001)|member(X4,skolem0002)))&(~member(X5,skolem0002)|member(X5,skolem0001))))),inference(shift_quantors,[status(thm)],[fof(c30,negated_conjecture,((skolem0001!=skolem0002&(![X4]:(~member(X4,skolem0001)|member(X4,skolem0002))))&(![X5]:(~member(X5,skolem0002)|member(X5,skolem0001)))),inference(skolemize,[status(esa)],[c29])).])).
% 9.93/10.18 cnf(c32,negated_conjecture,skolem0001!=skolem0002,inference(split_conjunct,[status(thm)],[c31])).
% 9.93/10.18 cnf(symmetry,axiom,X146!=X145|X145=X146,theory(equality)).
% 9.93/10.18 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)).
% 9.93/10.18 fof(c253,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])).
% 9.93/10.18 fof(c254,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)],[c253])).
% 9.93/10.18 fof(c255,plain,((![X136]:(![X137]:(~subclass(X136,X137)|(![X138]:(~member(X138,X136)|member(X138,X137))))))&(![X139]:(![X140]:((?[X141]:(member(X141,X139)&~member(X141,X140)))|subclass(X139,X140))))),inference(variable_rename,[status(thm)],[c254])).
% 9.93/10.18 fof(c257,plain,(![X136]:(![X137]:(![X138]:(![X139]:(![X140]:((~subclass(X136,X137)|(~member(X138,X136)|member(X138,X137)))&((member(skolem0009(X139,X140),X139)&~member(skolem0009(X139,X140),X140))|subclass(X139,X140)))))))),inference(shift_quantors,[status(thm)],[fof(c256,plain,((![X136]:(![X137]:(~subclass(X136,X137)|(![X138]:(~member(X138,X136)|member(X138,X137))))))&(![X139]:(![X140]:((member(skolem0009(X139,X140),X139)&~member(skolem0009(X139,X140),X140))|subclass(X139,X140))))),inference(skolemize,[status(esa)],[c255])).])).
% 9.93/10.18 fof(c258,plain,(![X136]:(![X137]:(![X138]:(![X139]:(![X140]:((~subclass(X136,X137)|(~member(X138,X136)|member(X138,X137)))&((member(skolem0009(X139,X140),X139)|subclass(X139,X140))&(~member(skolem0009(X139,X140),X140)|subclass(X139,X140))))))))),inference(distribute,[status(thm)],[c257])).
% 9.93/10.18 cnf(c261,plain,~member(skolem0009(X268,X269),X269)|subclass(X268,X269),inference(split_conjunct,[status(thm)],[c258])).
% 9.93/10.18 cnf(c34,negated_conjecture,~member(X193,skolem0002)|member(X193,skolem0001),inference(split_conjunct,[status(thm)],[c31])).
% 9.93/10.18 cnf(c260,plain,member(skolem0009(X265,X266),X265)|subclass(X265,X266),inference(split_conjunct,[status(thm)],[c258])).
% 9.93/10.18 cnf(c476,plain,subclass(skolem0002,X1336)|member(skolem0009(skolem0002,X1336),skolem0001),inference(resolution,[status(thm)],[c260, c34])).
% 9.93/10.18 cnf(c15332,plain,subclass(skolem0002,skolem0001),inference(resolution,[status(thm)],[c476, c261])).
% 9.93/10.18 fof(extensionality,axiom,(![X]:(![Y]:(X=Y<=>(subclass(X,Y)&subclass(Y,X))))),file('/export/starexec/sandbox/benchmark/Axioms/SET005+0.ax', extensionality)).
% 9.93/10.18 fof(c243,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])).
% 9.93/10.18 fof(c244,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)],[c243])).
% 9.93/10.18 fof(c246,plain,(![X131]:(![X132]:(![X133]:(![X134]:((X131!=X132|(subclass(X131,X132)&subclass(X132,X131)))&((~subclass(X133,X134)|~subclass(X134,X133))|X133=X134)))))),inference(shift_quantors,[status(thm)],[fof(c245,plain,((![X131]:(![X132]:(X131!=X132|(subclass(X131,X132)&subclass(X132,X131)))))&(![X133]:(![X134]:((~subclass(X133,X134)|~subclass(X134,X133))|X133=X134)))),inference(variable_rename,[status(thm)],[c244])).])).
% 9.93/10.18 fof(c247,plain,(![X131]:(![X132]:(![X133]:(![X134]:(((X131!=X132|subclass(X131,X132))&(X131!=X132|subclass(X132,X131)))&((~subclass(X133,X134)|~subclass(X134,X133))|X133=X134)))))),inference(distribute,[status(thm)],[c246])).
% 9.93/10.18 cnf(c250,plain,~subclass(X456,X455)|~subclass(X455,X456)|X456=X455,inference(split_conjunct,[status(thm)],[c247])).
% 9.93/10.18 cnf(c33,negated_conjecture,~member(X192,skolem0001)|member(X192,skolem0002),inference(split_conjunct,[status(thm)],[c31])).
% 9.93/10.18 cnf(c475,plain,subclass(skolem0001,X1334)|member(skolem0009(skolem0001,X1334),skolem0002),inference(resolution,[status(thm)],[c260, c33])).
% 9.93/10.18 cnf(c15311,plain,subclass(skolem0001,skolem0002),inference(resolution,[status(thm)],[c475, c261])).
% 9.93/10.18 cnf(c15317,plain,~subclass(skolem0002,skolem0001)|skolem0002=skolem0001,inference(resolution,[status(thm)],[c15311, c250])).
% 9.93/10.18 cnf(c24677,plain,skolem0002=skolem0001,inference(resolution,[status(thm)],[c15317, c15332])).
% 9.93/10.18 cnf(c24693,plain,skolem0001=skolem0002,inference(resolution,[status(thm)],[c24677, symmetry])).
% 9.93/10.18 cnf(c24785,plain,$false,inference(resolution,[status(thm)],[c24693, c32])).
% 9.93/10.18 % SZS output end CNFRefutation
% 9.93/10.18
% 9.93/10.18 % Initial clauses : 121
% 9.93/10.18 % Processed clauses : 912
% 9.93/10.18 % Factors computed : 34
% 9.93/10.18 % Resolvents computed: 24585
% 9.93/10.18 % Tautologies deleted: 6
% 9.93/10.18 % Forward subsumed : 934
% 9.93/10.18 % Backward subsumed : 10
% 9.93/10.18 % -------- CPU Time ---------
% 9.93/10.18 % User time : 9.781 s
% 9.93/10.18 % System time : 0.048 s
% 9.93/10.18 % Total time : 9.829 s
%------------------------------------------------------------------------------