%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET063+3 : TPTP v8.1.2. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n029.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:03 EDT 2024
% Result : Theorem 0.23s 0.59s
% Output : Refutation 0.23s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : SET063+3 : TPTP v8.1.2. Released v2.2.0.
% 0.08/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n029.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Wed May 8 19:15:08 EDT 2024
% 0.14/0.37 % CPUTime :
% 0.23/0.59 % Version: 1.5
% 0.23/0.59 % SZS status Theorem
% 0.23/0.59 % SZS output start CNFRefutation
% 0.23/0.59 fof(prove_subset_of_empty_set_is_empty_set,conjecture,(![B]:(subset(B,empty_set)=>B=empty_set)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_subset_of_empty_set_is_empty_set)).
% 0.23/0.59 fof(c3,negated_conjecture,(~(![B]:(subset(B,empty_set)=>B=empty_set))),inference(assume_negation,[status(cth)],[prove_subset_of_empty_set_is_empty_set])).
% 0.23/0.59 fof(c4,negated_conjecture,(?[B]:(subset(B,empty_set)&B!=empty_set)),inference(fof_nnf,[status(thm)],[c3])).
% 0.23/0.59 fof(c5,negated_conjecture,(?[X2]:(subset(X2,empty_set)&X2!=empty_set)),inference(variable_rename,[status(thm)],[c4])).
% 0.23/0.59 fof(c6,negated_conjecture,(subset(skolem0001,empty_set)&skolem0001!=empty_set),inference(skolemize,[status(esa)],[c5])).
% 0.23/0.59 cnf(c8,negated_conjecture,skolem0001!=empty_set,inference(split_conjunct,[status(thm)],[c6])).
% 0.23/0.59 cnf(c7,negated_conjecture,subset(skolem0001,empty_set),inference(split_conjunct,[status(thm)],[c6])).
% 0.23/0.59 fof(empty_set_subset,axiom,(![B]:subset(empty_set,B)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', empty_set_subset)).
% 0.23/0.59 fof(c39,plain,(![X19]:subset(empty_set,X19)),inference(variable_rename,[status(thm)],[empty_set_subset])).
% 0.23/0.59 cnf(c40,plain,subset(empty_set,X23),inference(split_conjunct,[status(thm)],[c39])).
% 0.23/0.59 fof(equal_defn,axiom,(![B]:(![C]:(B=C<=>(subset(B,C)&subset(C,B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', equal_defn)).
% 0.23/0.59 fof(c19,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])).
% 0.23/0.59 fof(c20,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)],[c19])).
% 0.23/0.59 fof(c22,plain,(![X8]:(![X9]:(![X10]:(![X11]:((X8!=X9|(subset(X8,X9)&subset(X9,X8)))&((~subset(X10,X11)|~subset(X11,X10))|X10=X11)))))),inference(shift_quantors,[status(thm)],[fof(c21,plain,((![X8]:(![X9]:(X8!=X9|(subset(X8,X9)&subset(X9,X8)))))&(![X10]:(![X11]:((~subset(X10,X11)|~subset(X11,X10))|X10=X11)))),inference(variable_rename,[status(thm)],[c20])).])).
% 0.23/0.59 fof(c23,plain,(![X8]:(![X9]:(![X10]:(![X11]:(((X8!=X9|subset(X8,X9))&(X8!=X9|subset(X9,X8)))&((~subset(X10,X11)|~subset(X11,X10))|X10=X11)))))),inference(distribute,[status(thm)],[c22])).
% 0.23/0.59 cnf(c26,plain,~subset(X63,X64)|~subset(X64,X63)|X63=X64,inference(split_conjunct,[status(thm)],[c23])).
% 0.23/0.59 cnf(c68,plain,~subset(X69,empty_set)|X69=empty_set,inference(resolution,[status(thm)],[c26, c40])).
% 0.23/0.59 cnf(c69,plain,skolem0001=empty_set,inference(resolution,[status(thm)],[c68, c7])).
% 0.23/0.59 cnf(c74,plain,$false,inference(resolution,[status(thm)],[c69, c8])).
% 0.23/0.59 % SZS output end CNFRefutation
% 0.23/0.59
% 0.23/0.59 % Initial clauses : 19
% 0.23/0.59 % Processed clauses : 23
% 0.23/0.59 % Factors computed : 2
% 0.23/0.59 % Resolvents computed: 40
% 0.23/0.59 % Tautologies deleted: 4
% 0.23/0.59 % Forward subsumed : 9
% 0.23/0.59 % Backward subsumed : 0
% 0.23/0.59 % -------- CPU Time ---------
% 0.23/0.59 % User time : 0.197 s
% 0.23/0.59 % System time : 0.025 s
% 0.23/0.59 % Total time : 0.222 s
%------------------------------------------------------------------------------