%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU148+2 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n019.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:39 EDT 2024
% Result : Theorem 3.42s 3.61s
% Output : Refutation 3.42s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : SEU148+2 : TPTP v8.1.2. Released v3.3.0.
% 0.13/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n019.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 12:02:37 EDT 2024
% 0.21/0.35 % CPUTime :
% 3.42/3.61 % Version: 1.5
% 3.42/3.61 % SZS status Theorem
% 3.42/3.61 % SZS output start CNFRefutation
% 3.42/3.61 fof(t6_zfmisc_1,conjecture,(![A]:(![B]:(subset(singleton(A),singleton(B))=>A=B))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t6_zfmisc_1)).
% 3.42/3.61 fof(c28,negated_conjecture,(~(![A]:(![B]:(subset(singleton(A),singleton(B))=>A=B)))),inference(assume_negation,[status(cth)],[t6_zfmisc_1])).
% 3.42/3.61 fof(c29,negated_conjecture,(?[A]:(?[B]:(subset(singleton(A),singleton(B))&A!=B))),inference(fof_nnf,[status(thm)],[c28])).
% 3.42/3.61 fof(c30,negated_conjecture,(?[X15]:(?[X16]:(subset(singleton(X15),singleton(X16))&X15!=X16))),inference(variable_rename,[status(thm)],[c29])).
% 3.42/3.61 fof(c31,negated_conjecture,(subset(singleton(skolem0001),singleton(skolem0002))&skolem0001!=skolem0002),inference(skolemize,[status(esa)],[c30])).
% 3.42/3.61 cnf(c33,negated_conjecture,skolem0001!=skolem0002,inference(split_conjunct,[status(thm)],[c31])).
% 3.42/3.61 cnf(c32,negated_conjecture,subset(singleton(skolem0001),singleton(skolem0002)),inference(split_conjunct,[status(thm)],[c31])).
% 3.42/3.61 fof(l2_zfmisc_1,plain,(![A]:(![B]:(subset(singleton(A),B)<=>in(A,B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', l2_zfmisc_1)).
% 3.42/3.61 fof(c156,plain,(![A]:(![B]:((~subset(singleton(A),B)|in(A,B))&(~in(A,B)|subset(singleton(A),B))))),inference(fof_nnf,[status(thm)],[l2_zfmisc_1])).
% 3.42/3.61 fof(c157,plain,((![A]:(![B]:(~subset(singleton(A),B)|in(A,B))))&(![A]:(![B]:(~in(A,B)|subset(singleton(A),B))))),inference(shift_quantors,[status(thm)],[c156])).
% 3.42/3.61 fof(c159,plain,(![X93]:(![X94]:(![X95]:(![X96]:((~subset(singleton(X93),X94)|in(X93,X94))&(~in(X95,X96)|subset(singleton(X95),X96))))))),inference(shift_quantors,[status(thm)],[fof(c158,plain,((![X93]:(![X94]:(~subset(singleton(X93),X94)|in(X93,X94))))&(![X95]:(![X96]:(~in(X95,X96)|subset(singleton(X95),X96))))),inference(variable_rename,[status(thm)],[c157])).])).
% 3.42/3.61 cnf(c160,plain,~subset(singleton(X550),X551)|in(X550,X551),inference(split_conjunct,[status(thm)],[c159])).
% 3.42/3.61 cnf(c1164,plain,in(skolem0001,singleton(skolem0002)),inference(resolution,[status(thm)],[c160, c32])).
% 3.42/3.61 cnf(symmetry,axiom,X190!=X189|X189=X190,theory(equality)).
% 3.42/3.61 fof(t69_enumset1,plain,(![A]:unordered_pair(A,A)=singleton(A)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t69_enumset1)).
% 3.42/3.61 fof(c37,plain,(![X18]:unordered_pair(X18,X18)=singleton(X18)),inference(variable_rename,[status(thm)],[t69_enumset1])).
% 3.42/3.61 cnf(c38,plain,unordered_pair(X324,X324)=singleton(X324),inference(split_conjunct,[status(thm)],[c37])).
% 3.42/3.61 cnf(c497,plain,singleton(X354)=unordered_pair(X354,X354),inference(resolution,[status(thm)],[c38, symmetry])).
% 3.42/3.61 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.42/3.61 fof(c253,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.42/3.61 fof(c254,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)],[c253])).
% 3.42/3.61 fof(c255,plain,((![X146]:(![X147]:(![X148]:(X148!=unordered_pair(X146,X147)|((![X149]:(~in(X149,X148)|(X149=X146|X149=X147)))&(![X150]:((X150!=X146&X150!=X147)|in(X150,X148))))))))&(![X151]:(![X152]:(![X153]:((?[X154]:((~in(X154,X153)|(X154!=X151&X154!=X152))&(in(X154,X153)|(X154=X151|X154=X152))))|X153=unordered_pair(X151,X152)))))),inference(variable_rename,[status(thm)],[c254])).
% 3.42/3.61 fof(c257,plain,(![X146]:(![X147]:(![X148]:(![X149]:(![X150]:(![X151]:(![X152]:(![X153]:((X148!=unordered_pair(X146,X147)|((~in(X149,X148)|(X149=X146|X149=X147))&((X150!=X146&X150!=X147)|in(X150,X148))))&(((~in(skolem0012(X151,X152,X153),X153)|(skolem0012(X151,X152,X153)!=X151&skolem0012(X151,X152,X153)!=X152))&(in(skolem0012(X151,X152,X153),X153)|(skolem0012(X151,X152,X153)=X151|skolem0012(X151,X152,X153)=X152)))|X153=unordered_pair(X151,X152))))))))))),inference(shift_quantors,[status(thm)],[fof(c256,plain,((![X146]:(![X147]:(![X148]:(X148!=unordered_pair(X146,X147)|((![X149]:(~in(X149,X148)|(X149=X146|X149=X147)))&(![X150]:((X150!=X146&X150!=X147)|in(X150,X148))))))))&(![X151]:(![X152]:(![X153]:(((~in(skolem0012(X151,X152,X153),X153)|(skolem0012(X151,X152,X153)!=X151&skolem0012(X151,X152,X153)!=X152))&(in(skolem0012(X151,X152,X153),X153)|(skolem0012(X151,X152,X153)=X151|skolem0012(X151,X152,X153)=X152)))|X153=unordered_pair(X151,X152)))))),inference(skolemize,[status(esa)],[c255])).])).
% 3.42/3.61 fof(c258,plain,(![X146]:(![X147]:(![X148]:(![X149]:(![X150]:(![X151]:(![X152]:(![X153]:(((X148!=unordered_pair(X146,X147)|(~in(X149,X148)|(X149=X146|X149=X147)))&((X148!=unordered_pair(X146,X147)|(X150!=X146|in(X150,X148)))&(X148!=unordered_pair(X146,X147)|(X150!=X147|in(X150,X148)))))&((((~in(skolem0012(X151,X152,X153),X153)|skolem0012(X151,X152,X153)!=X151)|X153=unordered_pair(X151,X152))&((~in(skolem0012(X151,X152,X153),X153)|skolem0012(X151,X152,X153)!=X152)|X153=unordered_pair(X151,X152)))&((in(skolem0012(X151,X152,X153),X153)|(skolem0012(X151,X152,X153)=X151|skolem0012(X151,X152,X153)=X152))|X153=unordered_pair(X151,X152)))))))))))),inference(distribute,[status(thm)],[c257])).
% 3.42/3.61 cnf(c259,plain,X795!=unordered_pair(X796,X794)|~in(X797,X795)|X797=X796|X797=X794,inference(split_conjunct,[status(thm)],[c258])).
% 3.42/3.61 cnf(c1847,plain,~in(X1950,singleton(X1949))|X1950=X1949,inference(resolution,[status(thm)],[c259, c497])).
% 3.42/3.61 cnf(c11678,plain,skolem0001=skolem0002,inference(resolution,[status(thm)],[c1847, c1164])).
% 3.42/3.61 cnf(c11831,plain,$false,inference(resolution,[status(thm)],[c11678, c33])).
% 3.42/3.61 % SZS output end CNFRefutation
% 3.42/3.61
% 3.42/3.61 % Initial clauses : 130
% 3.42/3.61 % Processed clauses : 480
% 3.42/3.61 % Factors computed : 31
% 3.42/3.61 % Resolvents computed: 11531
% 3.42/3.61 % Tautologies deleted: 22
% 3.42/3.61 % Forward subsumed : 777
% 3.42/3.61 % Backward subsumed : 12
% 3.42/3.61 % -------- CPU Time ---------
% 3.42/3.61 % User time : 3.213 s
% 3.42/3.61 % System time : 0.039 s
% 3.42/3.61 % Total time : 3.252 s
%------------------------------------------------------------------------------