%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET079+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n008.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:07 EDT 2024
% Result : Theorem 31.99s 32.21s
% Output : Refutation 31.99s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.12 % Problem : SET079+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% 0.05/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n008.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 18:41:23 EDT 2024
% 0.13/0.34 % CPUTime :
% 31.99/32.21 % Version: 1.5
% 31.99/32.21 % SZS status Theorem
% 31.99/32.21 % SZS output start CNFRefutation
% 31.99/32.21 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)).
% 31.99/32.21 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])).
% 31.99/32.21 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])).
% 31.99/32.21 fof(c49,plain,((![X9]:(![X10]:(~disjoint(X9,X10)|(![X11]:(~member(X11,X9)|~member(X11,X10))))))&(![X12]:(![X13]:((?[X14]:(member(X14,X12)&member(X14,X13)))|disjoint(X12,X13))))),inference(variable_rename,[status(thm)],[c48])).
% 31.99/32.21 fof(c51,plain,(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:((~disjoint(X9,X10)|(~member(X11,X9)|~member(X11,X10)))&((member(skolem0004(X12,X13),X12)&member(skolem0004(X12,X13),X13))|disjoint(X12,X13)))))))),inference(shift_quantors,[status(thm)],[fof(c50,plain,((![X9]:(![X10]:(~disjoint(X9,X10)|(![X11]:(~member(X11,X9)|~member(X11,X10))))))&(![X12]:(![X13]:((member(skolem0004(X12,X13),X12)&member(skolem0004(X12,X13),X13))|disjoint(X12,X13))))),inference(skolemize,[status(esa)],[c49])).])).
% 31.99/32.21 fof(c52,plain,(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:((~disjoint(X9,X10)|(~member(X11,X9)|~member(X11,X10)))&((member(skolem0004(X12,X13),X12)|disjoint(X12,X13))&(member(skolem0004(X12,X13),X13)|disjoint(X12,X13))))))))),inference(distribute,[status(thm)],[c51])).
% 31.99/32.21 cnf(c53,plain,~disjoint(X328,X329)|~member(X330,X328)|~member(X330,X329),inference(split_conjunct,[status(thm)],[c52])).
% 31.99/32.21 cnf(c738,plain,~disjoint(X331,X331)|~member(X332,X331),inference(factor,[status(thm)],[c53])).
% 31.99/32.21 fof(corollary_to_set_in_its_singleton,conjecture,(![X]:(member(X,universal_class)=>singleton(X)!=null_class)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', corollary_to_set_in_its_singleton)).
% 31.99/32.21 fof(c26,negated_conjecture,(~(![X]:(member(X,universal_class)=>singleton(X)!=null_class))),inference(assume_negation,[status(cth)],[corollary_to_set_in_its_singleton])).
% 31.99/32.21 fof(c27,negated_conjecture,(?[X]:(member(X,universal_class)&singleton(X)=null_class)),inference(fof_nnf,[status(thm)],[c26])).
% 31.99/32.21 fof(c28,negated_conjecture,(?[X2]:(member(X2,universal_class)&singleton(X2)=null_class)),inference(variable_rename,[status(thm)],[c27])).
% 31.99/32.21 fof(c29,negated_conjecture,(member(skolem0001,universal_class)&singleton(skolem0001)=null_class),inference(skolemize,[status(esa)],[c28])).
% 31.99/32.21 cnf(c30,negated_conjecture,member(skolem0001,universal_class),inference(split_conjunct,[status(thm)],[c29])).
% 31.99/32.21 cnf(reflexivity,axiom,X139=X139,theory(equality)).
% 31.99/32.21 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)).
% 31.99/32.21 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])).
% 31.99/32.21 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])).
% 31.99/32.21 fof(c234,plain,(![X122]:(![X123]:(![X124]:(![X125]:(![X126]:(![X127]:((~member(X122,unordered_pair(X123,X124))|(member(X122,universal_class)&(X122=X123|X122=X124)))&((~member(X125,universal_class)|(X125!=X126&X125!=X127))|member(X125,unordered_pair(X126,X127)))))))))),inference(shift_quantors,[status(thm)],[fof(c233,plain,((![X122]:(![X123]:(![X124]:(~member(X122,unordered_pair(X123,X124))|(member(X122,universal_class)&(X122=X123|X122=X124))))))&(![X125]:(![X126]:(![X127]:((~member(X125,universal_class)|(X125!=X126&X125!=X127))|member(X125,unordered_pair(X126,X127))))))),inference(variable_rename,[status(thm)],[c232])).])).
% 31.99/32.21 fof(c235,plain,(![X122]:(![X123]:(![X124]:(![X125]:(![X126]:(![X127]:(((~member(X122,unordered_pair(X123,X124))|member(X122,universal_class))&(~member(X122,unordered_pair(X123,X124))|(X122=X123|X122=X124)))&(((~member(X125,universal_class)|X125!=X126)|member(X125,unordered_pair(X126,X127)))&((~member(X125,universal_class)|X125!=X127)|member(X125,unordered_pair(X126,X127))))))))))),inference(distribute,[status(thm)],[c234])).
% 31.99/32.21 cnf(c238,plain,~member(X592,universal_class)|X592!=X593|member(X592,unordered_pair(X593,X591)),inference(split_conjunct,[status(thm)],[c235])).
% 31.99/32.21 cnf(c2490,plain,~member(X1062,universal_class)|member(X1062,unordered_pair(X1062,X1063)),inference(resolution,[status(thm)],[c238, reflexivity])).
% 31.99/32.21 cnf(c12382,plain,member(skolem0001,unordered_pair(skolem0001,X1064)),inference(resolution,[status(thm)],[c2490, c30])).
% 31.99/32.21 cnf(c12465,plain,~disjoint(unordered_pair(skolem0001,X2193),unordered_pair(skolem0001,X2193)),inference(resolution,[status(thm)],[c12382, c738])).
% 31.99/32.21 cnf(symmetry,axiom,X143!=X142|X142=X143,theory(equality)).
% 31.99/32.21 fof(singleton_set_defn,axiom,(![X]:singleton(X)=unordered_pair(X,X)),file('/export/starexec/sandbox/benchmark/Axioms/SET005+0.ax', singleton_set_defn)).
% 31.99/32.21 fof(c227,plain,(![X119]:singleton(X119)=unordered_pair(X119,X119)),inference(variable_rename,[status(thm)],[singleton_set_defn])).
% 31.99/32.21 cnf(c228,plain,singleton(X172)=unordered_pair(X172,X172),inference(split_conjunct,[status(thm)],[c227])).
% 31.99/32.21 cnf(c285,plain,unordered_pair(X173,X173)=singleton(X173),inference(resolution,[status(thm)],[c228, symmetry])).
% 31.99/32.21 cnf(c31,negated_conjecture,singleton(skolem0001)=null_class,inference(split_conjunct,[status(thm)],[c29])).
% 31.99/32.21 cnf(transitivity,axiom,X148!=X147|X147!=X146|X148=X146,theory(equality)).
% 31.99/32.21 cnf(c263,plain,X595!=singleton(skolem0001)|X595=null_class,inference(resolution,[status(thm)],[transitivity, c31])).
% 31.99/32.21 cnf(c2505,plain,unordered_pair(skolem0001,skolem0001)=null_class,inference(resolution,[status(thm)],[c263, c285])).
% 31.99/32.21 cnf(c2538,plain,null_class=unordered_pair(skolem0001,skolem0001),inference(resolution,[status(thm)],[c2505, symmetry])).
% 31.99/32.21 fof(null_class_defn,axiom,(![X]:(~member(X,null_class))),file('/export/starexec/sandbox/benchmark/Axioms/SET005+0.ax', null_class_defn)).
% 31.99/32.21 fof(c178,plain,(![X]:~member(X,null_class)),inference(fof_simplification,[status(thm)],[null_class_defn])).
% 31.99/32.21 fof(c179,plain,(![X86]:~member(X86,null_class)),inference(variable_rename,[status(thm)],[c178])).
% 31.99/32.21 cnf(c180,plain,~member(X140,null_class),inference(split_conjunct,[status(thm)],[c179])).
% 31.99/32.21 cnf(c54,plain,member(skolem0004(X222,X221),X222)|disjoint(X222,X221),inference(split_conjunct,[status(thm)],[c52])).
% 31.99/32.21 cnf(c406,plain,disjoint(null_class,X225),inference(resolution,[status(thm)],[c54, c180])).
% 31.99/32.21 cnf(c25,axiom,X350!=X349|X351!=X352|~disjoint(X350,X351)|disjoint(X349,X352),theory(equality)).
% 31.99/32.21 cnf(c826,plain,null_class!=X2889|X2887!=X2888|disjoint(X2889,X2888),inference(resolution,[status(thm)],[c25, c406])).
% 31.99/32.21 cnf(c58335,plain,null_class!=X2892|disjoint(X2892,X2891),inference(resolution,[status(thm)],[c826, reflexivity])).
% 31.99/32.21 cnf(c58486,plain,disjoint(unordered_pair(skolem0001,skolem0001),X2926),inference(resolution,[status(thm)],[c58335, c2538])).
% 31.99/32.21 cnf(c60127,plain,$false,inference(resolution,[status(thm)],[c58486, c12465])).
% 31.99/32.21 % SZS output end CNFRefutation
% 31.99/32.21
% 31.99/32.21 % Initial clauses : 120
% 31.99/32.21 % Processed clauses : 1377
% 31.99/32.21 % Factors computed : 47
% 31.99/32.21 % Resolvents computed: 59843
% 31.99/32.21 % Tautologies deleted: 8
% 31.99/32.21 % Forward subsumed : 1553
% 31.99/32.21 % Backward subsumed : 25
% 31.99/32.21 % -------- CPU Time ---------
% 31.99/32.21 % User time : 31.733 s
% 31.99/32.21 % System time : 0.115 s
% 31.99/32.21 % Total time : 31.848 s
%------------------------------------------------------------------------------