%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET603+3 : TPTP v8.1.2. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n005.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:48 EDT 2024
% Result : Theorem 4.88s 5.03s
% Output : Refutation 4.88s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SET603+3 : TPTP v8.1.2. Released v2.2.0.
% 0.12/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n005.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed May 8 19:00:22 EDT 2024
% 0.14/0.35 % CPUTime :
% 4.88/5.03 % Version: 1.5
% 4.88/5.03 % SZS status Theorem
% 4.88/5.03 % SZS output start CNFRefutation
% 4.88/5.03 fof(prove_th74,conjecture,(![B]:difference(B,empty_set)=B),file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_th74)).
% 4.88/5.03 fof(c4,negated_conjecture,(~(![B]:difference(B,empty_set)=B)),inference(assume_negation,[status(cth)],[prove_th74])).
% 4.88/5.03 fof(c5,negated_conjecture,(?[B]:difference(B,empty_set)!=B),inference(fof_nnf,[status(thm)],[c4])).
% 4.88/5.03 fof(c6,negated_conjecture,(?[X2]:difference(X2,empty_set)!=X2),inference(variable_rename,[status(thm)],[c5])).
% 4.88/5.03 fof(c7,negated_conjecture,difference(skolem0001,empty_set)!=skolem0001,inference(skolemize,[status(esa)],[c6])).
% 4.88/5.03 cnf(c8,negated_conjecture,difference(skolem0001,empty_set)!=skolem0001,inference(split_conjunct,[status(thm)],[c7])).
% 4.88/5.03 cnf(symmetry,axiom,X40!=X41|X41=X40,theory(equality)).
% 4.88/5.03 fof(equal_defn,axiom,(![B]:(![C]:(B=C<=>(subset(B,C)&subset(C,B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', equal_defn)).
% 4.88/5.03 fof(c38,plain,(![B]:(![C]:((B!=C|(subset(B,C)&subset(C,B)))&((~subset(B,C)|~subset(C,B))|B=C)))),inference(fof_nnf,[status(thm)],[equal_defn])).
% 4.88/5.03 fof(c39,plain,((![B]:(![C]:(B!=C|(subset(B,C)&subset(C,B)))))&(![B]:(![C]:((~subset(B,C)|~subset(C,B))|B=C)))),inference(shift_quantors,[status(thm)],[c38])).
% 4.88/5.03 fof(c41,plain,(![X21]:(![X22]:(![X23]:(![X24]:((X21!=X22|(subset(X21,X22)&subset(X22,X21)))&((~subset(X23,X24)|~subset(X24,X23))|X23=X24)))))),inference(shift_quantors,[status(thm)],[fof(c40,plain,((![X21]:(![X22]:(X21!=X22|(subset(X21,X22)&subset(X22,X21)))))&(![X23]:(![X24]:((~subset(X23,X24)|~subset(X24,X23))|X23=X24)))),inference(variable_rename,[status(thm)],[c39])).])).
% 4.88/5.03 fof(c42,plain,(![X21]:(![X22]:(![X23]:(![X24]:(((X21!=X22|subset(X21,X22))&(X21!=X22|subset(X22,X21)))&((~subset(X23,X24)|~subset(X24,X23))|X23=X24)))))),inference(distribute,[status(thm)],[c41])).
% 4.88/5.03 cnf(c45,plain,~subset(X101,X102)|~subset(X102,X101)|X101=X102,inference(split_conjunct,[status(thm)],[c42])).
% 4.88/5.03 fof(subset_defn,axiom,(![B]:(![C]:(subset(B,C)<=>(![D]:(member(D,B)=>member(D,C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', subset_defn)).
% 4.88/5.03 fof(c19,plain,(![B]:(![C]:((~subset(B,C)|(![D]:(~member(D,B)|member(D,C))))&((?[D]:(member(D,B)&~member(D,C)))|subset(B,C))))),inference(fof_nnf,[status(thm)],[subset_defn])).
% 4.88/5.03 fof(c20,plain,((![B]:(![C]:(~subset(B,C)|(![D]:(~member(D,B)|member(D,C))))))&(![B]:(![C]:((?[D]:(member(D,B)&~member(D,C)))|subset(B,C))))),inference(shift_quantors,[status(thm)],[c19])).
% 4.88/5.03 fof(c21,plain,((![X8]:(![X9]:(~subset(X8,X9)|(![X10]:(~member(X10,X8)|member(X10,X9))))))&(![X11]:(![X12]:((?[X13]:(member(X13,X11)&~member(X13,X12)))|subset(X11,X12))))),inference(variable_rename,[status(thm)],[c20])).
% 4.88/5.03 fof(c23,plain,(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:((~subset(X8,X9)|(~member(X10,X8)|member(X10,X9)))&((member(skolem0003(X11,X12),X11)&~member(skolem0003(X11,X12),X12))|subset(X11,X12)))))))),inference(shift_quantors,[status(thm)],[fof(c22,plain,((![X8]:(![X9]:(~subset(X8,X9)|(![X10]:(~member(X10,X8)|member(X10,X9))))))&(![X11]:(![X12]:((member(skolem0003(X11,X12),X11)&~member(skolem0003(X11,X12),X12))|subset(X11,X12))))),inference(skolemize,[status(esa)],[c21])).])).
% 4.88/5.03 fof(c24,plain,(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:((~subset(X8,X9)|(~member(X10,X8)|member(X10,X9)))&((member(skolem0003(X11,X12),X11)|subset(X11,X12))&(~member(skolem0003(X11,X12),X12)|subset(X11,X12))))))))),inference(distribute,[status(thm)],[c23])).
% 4.88/5.03 cnf(c27,plain,~member(skolem0003(X87,X86),X86)|subset(X87,X86),inference(split_conjunct,[status(thm)],[c24])).
% 4.88/5.03 cnf(c26,plain,member(skolem0003(X69,X68),X69)|subset(X69,X68),inference(split_conjunct,[status(thm)],[c24])).
% 4.88/5.03 fof(difference_defn,axiom,(![B]:(![C]:(![D]:(member(D,difference(B,C))<=>(member(D,B)&(~member(D,C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', difference_defn)).
% 4.88/5.03 fof(c49,plain,(![B]:(![C]:(![D]:(member(D,difference(B,C))<=>(member(D,B)&~member(D,C)))))),inference(fof_simplification,[status(thm)],[difference_defn])).
% 4.88/5.03 fof(c50,plain,(![B]:(![C]:(![D]:((~member(D,difference(B,C))|(member(D,B)&~member(D,C)))&((~member(D,B)|member(D,C))|member(D,difference(B,C))))))),inference(fof_nnf,[status(thm)],[c49])).
% 4.88/5.03 fof(c51,plain,((![B]:(![C]:(![D]:(~member(D,difference(B,C))|(member(D,B)&~member(D,C))))))&(![B]:(![C]:(![D]:((~member(D,B)|member(D,C))|member(D,difference(B,C))))))),inference(shift_quantors,[status(thm)],[c50])).
% 4.88/5.03 fof(c53,plain,(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:((~member(X28,difference(X26,X27))|(member(X28,X26)&~member(X28,X27)))&((~member(X31,X29)|member(X31,X30))|member(X31,difference(X29,X30)))))))))),inference(shift_quantors,[status(thm)],[fof(c52,plain,((![X26]:(![X27]:(![X28]:(~member(X28,difference(X26,X27))|(member(X28,X26)&~member(X28,X27))))))&(![X29]:(![X30]:(![X31]:((~member(X31,X29)|member(X31,X30))|member(X31,difference(X29,X30))))))),inference(variable_rename,[status(thm)],[c51])).])).
% 4.88/5.03 fof(c54,plain,(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(![X31]:(((~member(X28,difference(X26,X27))|member(X28,X26))&(~member(X28,difference(X26,X27))|~member(X28,X27)))&((~member(X31,X29)|member(X31,X30))|member(X31,difference(X29,X30)))))))))),inference(distribute,[status(thm)],[c53])).
% 4.88/5.03 cnf(c55,plain,~member(X90,difference(X89,X91))|member(X90,X89),inference(split_conjunct,[status(thm)],[c54])).
% 4.88/5.03 cnf(c92,plain,member(skolem0003(difference(X235,X237),X236),X235)|subset(difference(X235,X237),X236),inference(resolution,[status(thm)],[c55, c26])).
% 4.88/5.03 cnf(c515,plain,subset(difference(X238,X239),X238),inference(resolution,[status(thm)],[c92, c27])).
% 4.88/5.03 cnf(c534,plain,~subset(X895,difference(X895,X896))|X895=difference(X895,X896),inference(resolution,[status(thm)],[c515, c45])).
% 4.88/5.03 fof(empty_set_defn,axiom,(![B]:(~member(B,empty_set))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', empty_set_defn)).
% 4.88/5.03 fof(c46,plain,(![B]:~member(B,empty_set)),inference(fof_simplification,[status(thm)],[empty_set_defn])).
% 4.88/5.03 fof(c47,plain,(![X25]:~member(X25,empty_set)),inference(variable_rename,[status(thm)],[c46])).
% 4.88/5.03 cnf(c48,plain,~member(X37,empty_set),inference(split_conjunct,[status(thm)],[c47])).
% 4.88/5.03 cnf(c57,plain,~member(X117,X118)|member(X117,X116)|member(X117,difference(X118,X116)),inference(split_conjunct,[status(thm)],[c54])).
% 4.88/5.03 cnf(c177,plain,member(skolem0003(X763,X764),X765)|member(skolem0003(X763,X764),difference(X763,X765))|subset(X763,X764),inference(resolution,[status(thm)],[c57, c26])).
% 4.88/5.03 cnf(c2774,plain,member(skolem0003(X2519,X2520),difference(X2519,empty_set))|subset(X2519,X2520),inference(resolution,[status(thm)],[c177, c48])).
% 4.88/5.03 cnf(c13679,plain,subset(X2521,difference(X2521,empty_set)),inference(resolution,[status(thm)],[c2774, c27])).
% 4.88/5.03 cnf(c13739,plain,X2522=difference(X2522,empty_set),inference(resolution,[status(thm)],[c13679, c534])).
% 4.88/5.03 cnf(c13832,plain,difference(X2533,empty_set)=X2533,inference(resolution,[status(thm)],[c13739, symmetry])).
% 4.88/5.03 cnf(c14076,plain,$false,inference(resolution,[status(thm)],[c13832, c8])).
% 4.88/5.03 % SZS output end CNFRefutation
% 4.88/5.03
% 4.88/5.03 % Initial clauses : 27
% 4.88/5.03 % Processed clauses : 416
% 4.88/5.03 % Factors computed : 38
% 4.88/5.03 % Resolvents computed: 13988
% 4.88/5.03 % Tautologies deleted: 19
% 4.88/5.03 % Forward subsumed : 1043
% 4.88/5.03 % Backward subsumed : 16
% 4.88/5.03 % -------- CPU Time ---------
% 4.88/5.03 % User time : 4.649 s
% 4.88/5.03 % System time : 0.035 s
% 4.88/5.03 % Total time : 4.684 s
%------------------------------------------------------------------------------