%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET073+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n013.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:05 EDT 2024
% Result : Theorem 35.82s 35.99s
% Output : Refutation 35.82s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : SET073+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n013.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Wed May 8 19:40:23 EDT 2024
% 0.15/0.36 % CPUTime :
% 35.82/35.99 % Version: 1.5
% 35.82/35.99 % SZS status Theorem
% 35.82/35.99 % SZS output start CNFRefutation
% 35.82/35.99 fof(disjoint_defn,axiom,(![X]:(![Y]:(disjoint(X,Y)<=>(![U]:(~(member(U,X)&member(U,Y))))))),file('/export/starexec/sandbox/benchmark/Axioms/SET005+0.ax', disjoint_defn)).
% 35.82/35.99 fof(c48,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])).
% 35.82/35.99 fof(c49,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)],[c48])).
% 35.82/35.99 fof(c50,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)],[c49])).
% 35.82/35.99 fof(c52,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(c51,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)],[c50])).])).
% 35.82/35.99 fof(c53,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)],[c52])).
% 35.82/35.99 cnf(c54,plain,~disjoint(X325,X327)|~member(X326,X325)|~member(X326,X327),inference(split_conjunct,[status(thm)],[c53])).
% 35.82/35.99 cnf(c724,plain,~disjoint(X333,X333)|~member(X332,X333),inference(factor,[status(thm)],[c54])).
% 35.82/35.99 fof(corollary1_1,conjecture,(![X]:(![Y]:(member(X,universal_class)=>unordered_pair(X,Y)!=null_class))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', corollary1_1)).
% 35.82/35.99 fof(c26,negated_conjecture,(~(![X]:(![Y]:(member(X,universal_class)=>unordered_pair(X,Y)!=null_class)))),inference(assume_negation,[status(cth)],[corollary1_1])).
% 35.82/35.99 fof(c27,negated_conjecture,(?[X]:(?[Y]:(member(X,universal_class)&unordered_pair(X,Y)=null_class))),inference(fof_nnf,[status(thm)],[c26])).
% 35.82/35.99 fof(c28,negated_conjecture,(?[X]:(member(X,universal_class)&(?[Y]:unordered_pair(X,Y)=null_class))),inference(shift_quantors,[status(thm)],[c27])).
% 35.82/35.99 fof(c29,negated_conjecture,(?[X2]:(member(X2,universal_class)&(?[X3]:unordered_pair(X2,X3)=null_class))),inference(variable_rename,[status(thm)],[c28])).
% 35.82/35.99 fof(c30,negated_conjecture,(member(skolem0001,universal_class)&unordered_pair(skolem0001,skolem0002)=null_class),inference(skolemize,[status(esa)],[c29])).
% 35.82/35.99 cnf(c31,negated_conjecture,member(skolem0001,universal_class),inference(split_conjunct,[status(thm)],[c30])).
% 35.82/35.99 cnf(reflexivity,axiom,X140=X140,theory(equality)).
% 35.82/35.99 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)).
% 35.82/35.99 fof(c232,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])).
% 35.82/35.99 fof(c233,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)],[c232])).
% 35.82/35.99 fof(c235,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(c234,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)],[c233])).])).
% 35.82/35.99 fof(c236,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)],[c235])).
% 35.82/35.99 cnf(c239,plain,~member(X595,universal_class)|X595!=X593|member(X595,unordered_pair(X593,X594)),inference(split_conjunct,[status(thm)],[c236])).
% 35.82/35.99 cnf(c2488,plain,~member(X1005,universal_class)|member(X1005,unordered_pair(X1005,X1004)),inference(resolution,[status(thm)],[c239, reflexivity])).
% 35.82/35.99 cnf(c9016,plain,member(skolem0001,unordered_pair(skolem0001,X1006)),inference(resolution,[status(thm)],[c2488, c31])).
% 35.82/35.99 cnf(c9090,plain,~disjoint(unordered_pair(skolem0001,X1990),unordered_pair(skolem0001,X1990)),inference(resolution,[status(thm)],[c9016, c724])).
% 35.82/35.99 cnf(symmetry,axiom,X144!=X143|X143=X144,theory(equality)).
% 35.82/35.99 cnf(c32,negated_conjecture,unordered_pair(skolem0001,skolem0002)=null_class,inference(split_conjunct,[status(thm)],[c30])).
% 35.82/35.99 cnf(c298,plain,null_class=unordered_pair(skolem0001,skolem0002),inference(resolution,[status(thm)],[c32, symmetry])).
% 35.82/35.99 fof(null_class_defn,axiom,(![X]:(~member(X,null_class))),file('/export/starexec/sandbox/benchmark/Axioms/SET005+0.ax', null_class_defn)).
% 35.82/35.99 fof(c179,plain,(![X]:~member(X,null_class)),inference(fof_simplification,[status(thm)],[null_class_defn])).
% 35.82/35.99 fof(c180,plain,(![X87]:~member(X87,null_class)),inference(variable_rename,[status(thm)],[c179])).
% 35.82/35.99 cnf(c181,plain,~member(X141,null_class),inference(split_conjunct,[status(thm)],[c180])).
% 35.82/35.99 cnf(c55,plain,member(skolem0005(X222,X223),X222)|disjoint(X222,X223),inference(split_conjunct,[status(thm)],[c53])).
% 35.82/35.99 cnf(c407,plain,disjoint(null_class,X224),inference(resolution,[status(thm)],[c55, c181])).
% 35.82/35.99 cnf(c25,axiom,X355!=X358|X356!=X357|~disjoint(X355,X356)|disjoint(X358,X357),theory(equality)).
% 35.82/35.99 cnf(c835,plain,null_class!=X3114|X3113!=X3112|disjoint(X3114,X3112),inference(resolution,[status(thm)],[c25, c407])).
% 35.82/35.99 cnf(c63967,plain,null_class!=X3117|disjoint(X3117,X3116),inference(resolution,[status(thm)],[c835, reflexivity])).
% 35.82/35.99 cnf(c64182,plain,disjoint(unordered_pair(skolem0001,skolem0002),X3127),inference(resolution,[status(thm)],[c63967, c298])).
% 35.82/35.99 cnf(c64223,plain,$false,inference(resolution,[status(thm)],[c64182, c9090])).
% 35.82/35.99 % SZS output end CNFRefutation
% 35.82/35.99
% 35.82/35.99 % Initial clauses : 120
% 35.82/35.99 % Processed clauses : 1411
% 35.82/35.99 % Factors computed : 44
% 35.82/35.99 % Resolvents computed: 63953
% 35.82/35.99 % Tautologies deleted: 8
% 35.82/35.99 % Forward subsumed : 1632
% 35.82/35.99 % Backward subsumed : 22
% 35.82/35.99 % -------- CPU Time ---------
% 35.82/35.99 % User time : 35.480 s
% 35.82/35.99 % System time : 0.146 s
% 35.82/35.99 % Total time : 35.626 s
%------------------------------------------------------------------------------