%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU143+2 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n024.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:40:38 EDT 2024
% Result : Theorem 3.52s 3.70s
% Output : Refutation 3.52s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : SEU143+2 : TPTP v8.1.2. Released v3.3.0.
% 0.12/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n024.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 12:11:37 EDT 2024
% 0.14/0.34 % CPUTime :
% 3.52/3.70 % Version: 1.5
% 3.52/3.70 % SZS status Theorem
% 3.52/3.70 % SZS output start CNFRefutation
% 3.52/3.70 fof(fc1_xboole_0,axiom,empty(empty_set),file('/export/starexec/sandbox/benchmark/theBenchmark.p', fc1_xboole_0)).
% 3.52/3.70 cnf(c161,plain,empty(empty_set),inference(split_conjunct,[status(thm)],[fc1_xboole_0])).
% 3.52/3.70 cnf(c9,axiom,X266!=X265|~empty(X266)|empty(X265),theory(equality)).
% 3.52/3.70 cnf(symmetry,axiom,X171!=X170|X170=X171,theory(equality)).
% 3.52/3.70 fof(l1_zfmisc_1,conjecture,(![A]:singleton(A)!=empty_set),file('/export/starexec/sandbox/benchmark/theBenchmark.p', l1_zfmisc_1)).
% 3.52/3.70 fof(c135,negated_conjecture,(~(![A]:singleton(A)!=empty_set)),inference(assume_negation,[status(cth)],[l1_zfmisc_1])).
% 3.52/3.70 fof(c136,negated_conjecture,(?[A]:singleton(A)=empty_set),inference(fof_nnf,[status(thm)],[c135])).
% 3.52/3.70 fof(c137,negated_conjecture,(?[X84]:singleton(X84)=empty_set),inference(variable_rename,[status(thm)],[c136])).
% 3.52/3.70 fof(c138,negated_conjecture,singleton(skolem0006)=empty_set,inference(skolemize,[status(esa)],[c137])).
% 3.52/3.70 cnf(c139,negated_conjecture,singleton(skolem0006)=empty_set,inference(split_conjunct,[status(thm)],[c138])).
% 3.52/3.70 cnf(c333,plain,empty_set=singleton(skolem0006),inference(resolution,[status(thm)],[c139, symmetry])).
% 3.52/3.70 cnf(c433,plain,~empty(empty_set)|empty(singleton(skolem0006)),inference(resolution,[status(thm)],[c333, c9])).
% 3.52/3.70 cnf(c5403,plain,empty(singleton(skolem0006)),inference(resolution,[status(thm)],[c433, c161])).
% 3.52/3.70 fof(t7_boole,axiom,(![A]:(![B]:(~(in(A,B)&empty(B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t7_boole)).
% 3.52/3.70 fof(c24,plain,(![A]:(![B]:(~in(A,B)|~empty(B)))),inference(fof_nnf,[status(thm)],[t7_boole])).
% 3.52/3.70 fof(c25,plain,(![X13]:(![X14]:(~in(X13,X14)|~empty(X14)))),inference(variable_rename,[status(thm)],[c24])).
% 3.52/3.70 cnf(c26,plain,~in(X176,X177)|~empty(X177),inference(split_conjunct,[status(thm)],[c25])).
% 3.52/3.70 cnf(reflexivity,axiom,X167=X167,theory(equality)).
% 3.52/3.70 fof(t69_enumset1,plain,(![A]:unordered_pair(A,A)=singleton(A)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t69_enumset1)).
% 3.52/3.70 fof(c30,plain,(![X16]:unordered_pair(X16,X16)=singleton(X16)),inference(variable_rename,[status(thm)],[t69_enumset1])).
% 3.52/3.70 cnf(c31,plain,unordered_pair(X295,X295)=singleton(X295),inference(split_conjunct,[status(thm)],[c30])).
% 3.52/3.70 cnf(c472,plain,singleton(X334)=unordered_pair(X334,X334),inference(resolution,[status(thm)],[c31, symmetry])).
% 3.52/3.70 fof(d2_tarski,axiom,(![A]:(![B]:(![C]:(C=unordered_pair(A,B)<=>(![D]:(in(D,C)<=>(D=A|D=B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', d2_tarski)).
% 3.52/3.70 fof(c228,plain,(![A]:(![B]:(![C]:((C!=unordered_pair(A,B)|(![D]:((~in(D,C)|(D=A|D=B))&((D!=A&D!=B)|in(D,C)))))&((?[D]:((~in(D,C)|(D!=A&D!=B))&(in(D,C)|(D=A|D=B))))|C=unordered_pair(A,B)))))),inference(fof_nnf,[status(thm)],[d2_tarski])).
% 3.52/3.70 fof(c229,plain,((![A]:(![B]:(![C]:(C!=unordered_pair(A,B)|((![D]:(~in(D,C)|(D=A|D=B)))&(![D]:((D!=A&D!=B)|in(D,C))))))))&(![A]:(![B]:(![C]:((?[D]:((~in(D,C)|(D!=A&D!=B))&(in(D,C)|(D=A|D=B))))|C=unordered_pair(A,B)))))),inference(shift_quantors,[status(thm)],[c228])).
% 3.52/3.70 fof(c230,plain,((![X133]:(![X134]:(![X135]:(X135!=unordered_pair(X133,X134)|((![X136]:(~in(X136,X135)|(X136=X133|X136=X134)))&(![X137]:((X137!=X133&X137!=X134)|in(X137,X135))))))))&(![X138]:(![X139]:(![X140]:((?[X141]:((~in(X141,X140)|(X141!=X138&X141!=X139))&(in(X141,X140)|(X141=X138|X141=X139))))|X140=unordered_pair(X138,X139)))))),inference(variable_rename,[status(thm)],[c229])).
% 3.52/3.70 fof(c232,plain,(![X133]:(![X134]:(![X135]:(![X136]:(![X137]:(![X138]:(![X139]:(![X140]:((X135!=unordered_pair(X133,X134)|((~in(X136,X135)|(X136=X133|X136=X134))&((X137!=X133&X137!=X134)|in(X137,X135))))&(((~in(skolem0011(X138,X139,X140),X140)|(skolem0011(X138,X139,X140)!=X138&skolem0011(X138,X139,X140)!=X139))&(in(skolem0011(X138,X139,X140),X140)|(skolem0011(X138,X139,X140)=X138|skolem0011(X138,X139,X140)=X139)))|X140=unordered_pair(X138,X139))))))))))),inference(shift_quantors,[status(thm)],[fof(c231,plain,((![X133]:(![X134]:(![X135]:(X135!=unordered_pair(X133,X134)|((![X136]:(~in(X136,X135)|(X136=X133|X136=X134)))&(![X137]:((X137!=X133&X137!=X134)|in(X137,X135))))))))&(![X138]:(![X139]:(![X140]:(((~in(skolem0011(X138,X139,X140),X140)|(skolem0011(X138,X139,X140)!=X138&skolem0011(X138,X139,X140)!=X139))&(in(skolem0011(X138,X139,X140),X140)|(skolem0011(X138,X139,X140)=X138|skolem0011(X138,X139,X140)=X139)))|X140=unordered_pair(X138,X139)))))),inference(skolemize,[status(esa)],[c230])).])).
% 3.52/3.70 fof(c233,plain,(![X133]:(![X134]:(![X135]:(![X136]:(![X137]:(![X138]:(![X139]:(![X140]:(((X135!=unordered_pair(X133,X134)|(~in(X136,X135)|(X136=X133|X136=X134)))&((X135!=unordered_pair(X133,X134)|(X137!=X133|in(X137,X135)))&(X135!=unordered_pair(X133,X134)|(X137!=X134|in(X137,X135)))))&((((~in(skolem0011(X138,X139,X140),X140)|skolem0011(X138,X139,X140)!=X138)|X140=unordered_pair(X138,X139))&((~in(skolem0011(X138,X139,X140),X140)|skolem0011(X138,X139,X140)!=X139)|X140=unordered_pair(X138,X139)))&((in(skolem0011(X138,X139,X140),X140)|(skolem0011(X138,X139,X140)=X138|skolem0011(X138,X139,X140)=X139))|X140=unordered_pair(X138,X139)))))))))))),inference(distribute,[status(thm)],[c232])).
% 3.52/3.70 cnf(c235,plain,X722!=unordered_pair(X721,X720)|X719!=X721|in(X719,X722),inference(split_conjunct,[status(thm)],[c233])).
% 3.52/3.70 cnf(c1649,plain,X1927!=X1928|in(X1927,singleton(X1928)),inference(resolution,[status(thm)],[c235, c472])).
% 3.52/3.70 cnf(c12182,plain,in(X1929,singleton(X1929)),inference(resolution,[status(thm)],[c1649, reflexivity])).
% 3.52/3.70 cnf(c12197,plain,~empty(singleton(X1931)),inference(resolution,[status(thm)],[c12182, c26])).
% 3.52/3.70 cnf(c12202,plain,$false,inference(resolution,[status(thm)],[c12197, c5403])).
% 3.52/3.70 % SZS output end CNFRefutation
% 3.52/3.70
% 3.52/3.70 % Initial clauses : 115
% 3.52/3.70 % Processed clauses : 466
% 3.52/3.70 % Factors computed : 32
% 3.52/3.70 % Resolvents computed: 11980
% 3.52/3.70 % Tautologies deleted: 21
% 3.52/3.70 % Forward subsumed : 803
% 3.52/3.70 % Backward subsumed : 14
% 3.52/3.70 % -------- CPU Time ---------
% 3.52/3.70 % User time : 3.318 s
% 3.52/3.70 % System time : 0.030 s
% 3.52/3.70 % Total time : 3.348 s
%------------------------------------------------------------------------------