%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET074+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n009.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:06 EDT 2024
% Result : Theorem 34.56s 34.76s
% Output : Refutation 34.56s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SET074+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n009.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 18:24:08 EDT 2024
% 0.14/0.34 % CPUTime :
% 34.56/34.76 % Version: 1.5
% 34.56/34.76 % SZS status Theorem
% 34.56/34.76 % SZS output start CNFRefutation
% 34.56/34.76 fof(corollary1_2,conjecture,(![X]:(![Y]:(member(Y,universal_class)=>unordered_pair(X,Y)!=null_class))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', corollary1_2)).
% 34.56/34.76 fof(c26,negated_conjecture,(~(![X]:(![Y]:(member(Y,universal_class)=>unordered_pair(X,Y)!=null_class)))),inference(assume_negation,[status(cth)],[corollary1_2])).
% 34.56/34.76 fof(c27,negated_conjecture,(?[X]:(?[Y]:(member(Y,universal_class)&unordered_pair(X,Y)=null_class))),inference(fof_nnf,[status(thm)],[c26])).
% 34.56/34.76 fof(c28,negated_conjecture,(?[X2]:(?[X3]:(member(X3,universal_class)&unordered_pair(X2,X3)=null_class))),inference(variable_rename,[status(thm)],[c27])).
% 34.56/34.76 fof(c29,negated_conjecture,(member(skolem0002,universal_class)&unordered_pair(skolem0001,skolem0002)=null_class),inference(skolemize,[status(esa)],[c28])).
% 34.56/34.76 cnf(c30,negated_conjecture,member(skolem0002,universal_class),inference(split_conjunct,[status(thm)],[c29])).
% 34.56/34.76 fof(disjoint_defn,axiom,(![X]:(![Y]:(disjoint(X,Y)<=>(![U]:(~(member(U,X)&member(U,Y))))))),file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax', disjoint_defn)).
% 34.56/34.76 fof(c47,plain,(![X]:(![Y]:((~disjoint(X,Y)|(![U]:(~member(U,X)|~member(U,Y))))&((?[U]:(member(U,X)&member(U,Y)))|disjoint(X,Y))))),inference(fof_nnf,[status(thm)],[disjoint_defn])).
% 34.56/34.76 fof(c48,plain,((![X]:(![Y]:(~disjoint(X,Y)|(![U]:(~member(U,X)|~member(U,Y))))))&(![X]:(![Y]:((?[U]:(member(U,X)&member(U,Y)))|disjoint(X,Y))))),inference(shift_quantors,[status(thm)],[c47])).
% 34.56/34.76 fof(c49,plain,((![X10]:(![X11]:(~disjoint(X10,X11)|(![X12]:(~member(X12,X10)|~member(X12,X11))))))&(![X13]:(![X14]:((?[X15]:(member(X15,X13)&member(X15,X14)))|disjoint(X13,X14))))),inference(variable_rename,[status(thm)],[c48])).
% 34.56/34.76 fof(c51,plain,(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:((~disjoint(X10,X11)|(~member(X12,X10)|~member(X12,X11)))&((member(skolem0005(X13,X14),X13)&member(skolem0005(X13,X14),X14))|disjoint(X13,X14)))))))),inference(shift_quantors,[status(thm)],[fof(c50,plain,((![X10]:(![X11]:(~disjoint(X10,X11)|(![X12]:(~member(X12,X10)|~member(X12,X11))))))&(![X13]:(![X14]:((member(skolem0005(X13,X14),X13)&member(skolem0005(X13,X14),X14))|disjoint(X13,X14))))),inference(skolemize,[status(esa)],[c49])).])).
% 34.56/34.76 fof(c52,plain,(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:((~disjoint(X10,X11)|(~member(X12,X10)|~member(X12,X11)))&((member(skolem0005(X13,X14),X13)|disjoint(X13,X14))&(member(skolem0005(X13,X14),X14)|disjoint(X13,X14))))))))),inference(distribute,[status(thm)],[c51])).
% 34.56/34.76 cnf(c53,plain,~disjoint(X327,X325)|~member(X326,X327)|~member(X326,X325),inference(split_conjunct,[status(thm)],[c52])).
% 34.56/34.76 cnf(c727,plain,~disjoint(X362,universal_class)|~member(skolem0002,X362),inference(resolution,[status(thm)],[c53, c30])).
% 34.56/34.76 cnf(reflexivity,axiom,X140=X140,theory(equality)).
% 34.56/34.76 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/sandbox2/benchmark/Axioms/SET005+0.ax', unordered_pair_defn)).
% 34.56/34.76 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])).
% 34.56/34.76 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])).
% 34.56/34.76 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])).])).
% 34.56/34.76 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])).
% 34.56/34.76 cnf(c239,plain,~member(X601,universal_class)|X601!=X599|member(X601,unordered_pair(X600,X599)),inference(split_conjunct,[status(thm)],[c235])).
% 34.56/34.76 cnf(c2514,plain,~member(X1036,universal_class)|member(X1036,unordered_pair(X1035,X1036)),inference(resolution,[status(thm)],[c239, reflexivity])).
% 34.56/34.76 cnf(c9377,plain,member(skolem0002,unordered_pair(X1037,skolem0002)),inference(resolution,[status(thm)],[c2514, c30])).
% 34.56/34.76 cnf(c9468,plain,~disjoint(unordered_pair(X1045,skolem0002),universal_class),inference(resolution,[status(thm)],[c9377, c727])).
% 34.56/34.76 cnf(symmetry,axiom,X144!=X143|X143=X144,theory(equality)).
% 34.56/34.76 cnf(c31,negated_conjecture,unordered_pair(skolem0001,skolem0002)=null_class,inference(split_conjunct,[status(thm)],[c29])).
% 34.56/34.76 cnf(c303,plain,null_class=unordered_pair(skolem0001,skolem0002),inference(resolution,[status(thm)],[c31, symmetry])).
% 34.56/34.76 fof(null_class_defn,axiom,(![X]:(~member(X,null_class))),file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax', null_class_defn)).
% 34.56/34.76 fof(c178,plain,(![X]:~member(X,null_class)),inference(fof_simplification,[status(thm)],[null_class_defn])).
% 34.56/34.76 fof(c179,plain,(![X87]:~member(X87,null_class)),inference(variable_rename,[status(thm)],[c178])).
% 34.56/34.76 cnf(c180,plain,~member(X141,null_class),inference(split_conjunct,[status(thm)],[c179])).
% 34.56/34.76 cnf(c54,plain,member(skolem0005(X223,X222),X223)|disjoint(X223,X222),inference(split_conjunct,[status(thm)],[c52])).
% 34.56/34.76 cnf(c408,plain,disjoint(null_class,X224),inference(resolution,[status(thm)],[c54, c180])).
% 34.56/34.76 cnf(c25,axiom,X357!=X355|X358!=X356|~disjoint(X357,X358)|disjoint(X355,X356),theory(equality)).
% 34.56/34.76 cnf(c832,plain,null_class!=X3118|X3117!=X3119|disjoint(X3118,X3119),inference(resolution,[status(thm)],[c25, c408])).
% 34.56/34.76 cnf(c63789,plain,null_class!=X3126|disjoint(X3126,X3127),inference(resolution,[status(thm)],[c832, reflexivity])).
% 34.56/34.76 cnf(c64154,plain,disjoint(unordered_pair(skolem0001,skolem0002),X3142),inference(resolution,[status(thm)],[c63789, c303])).
% 34.56/34.76 cnf(c64510,plain,$false,inference(resolution,[status(thm)],[c64154, c9468])).
% 34.56/34.76 % SZS output end CNFRefutation
% 34.56/34.76
% 34.56/34.76 % Initial clauses : 120
% 34.56/34.76 % Processed clauses : 1408
% 34.56/34.76 % Factors computed : 45
% 34.56/34.76 % Resolvents computed: 64253
% 34.56/34.76 % Tautologies deleted: 8
% 34.56/34.76 % Forward subsumed : 1634
% 34.56/34.76 % Backward subsumed : 22
% 34.56/34.76 % -------- CPU Time ---------
% 34.56/34.76 % User time : 34.255 s
% 34.56/34.76 % System time : 0.143 s
% 34.56/34.76 % Total time : 34.398 s
%------------------------------------------------------------------------------