%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET878+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n003.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:17 EDT 2024
% Result : Theorem 0.91s 1.12s
% Output : Refutation 0.91s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SET878+1 : TPTP v8.1.2. Released v3.2.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n003.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 18:29:53 EDT 2024
% 0.14/0.34 % CPUTime :
% 0.91/1.12 % Version: 1.5
% 0.91/1.12 % SZS status Theorem
% 0.91/1.12 % SZS output start CNFRefutation
% 0.91/1.12 fof(t19_zfmisc_1,conjecture,(![A]:(![B]:set_intersection2(singleton(A),unordered_pair(A,B))=singleton(A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t19_zfmisc_1)).
% 0.91/1.12 fof(c5,negated_conjecture,(~(![A]:(![B]:set_intersection2(singleton(A),unordered_pair(A,B))=singleton(A)))),inference(assume_negation,[status(cth)],[t19_zfmisc_1])).
% 0.91/1.12 fof(c6,negated_conjecture,(?[A]:(?[B]:set_intersection2(singleton(A),unordered_pair(A,B))!=singleton(A))),inference(fof_nnf,[status(thm)],[c5])).
% 0.91/1.12 fof(c7,negated_conjecture,(?[X2]:(?[X3]:set_intersection2(singleton(X2),unordered_pair(X2,X3))!=singleton(X2))),inference(variable_rename,[status(thm)],[c6])).
% 0.91/1.12 fof(c8,negated_conjecture,set_intersection2(singleton(skolem0001),unordered_pair(skolem0001,skolem0002))!=singleton(skolem0001),inference(skolemize,[status(esa)],[c7])).
% 0.91/1.12 cnf(c9,negated_conjecture,set_intersection2(singleton(skolem0001),unordered_pair(skolem0001,skolem0002))!=singleton(skolem0001),inference(split_conjunct,[status(thm)],[c8])).
% 0.91/1.12 cnf(symmetry,axiom,X27!=X26|X26=X27,theory(equality)).
% 0.91/1.12 cnf(transitivity,axiom,X30!=X28|X28!=X29|X30=X29,theory(equality)).
% 0.91/1.12 fof(commutativity_k3_xboole_0,axiom,(![A]:(![B]:set_intersection2(A,B)=set_intersection2(B,A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', commutativity_k3_xboole_0)).
% 0.91/1.12 fof(c35,plain,(![X18]:(![X19]:set_intersection2(X18,X19)=set_intersection2(X19,X18))),inference(variable_rename,[status(thm)],[commutativity_k3_xboole_0])).
% 0.91/1.12 cnf(c36,plain,set_intersection2(X54,X53)=set_intersection2(X53,X54),inference(split_conjunct,[status(thm)],[c35])).
% 0.91/1.12 cnf(c69,plain,X263!=set_intersection2(X262,X261)|X263=set_intersection2(X261,X262),inference(resolution,[status(thm)],[c36, transitivity])).
% 0.91/1.12 fof(l32_zfmisc_1,axiom,(![A]:(![B]:(in(A,B)=>set_intersection2(B,singleton(A))=singleton(A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l32_zfmisc_1)).
% 0.91/1.12 fof(c17,plain,(![A]:(![B]:(~in(A,B)|set_intersection2(B,singleton(A))=singleton(A)))),inference(fof_nnf,[status(thm)],[l32_zfmisc_1])).
% 0.91/1.12 fof(c18,plain,(![X6]:(![X7]:(~in(X6,X7)|set_intersection2(X7,singleton(X6))=singleton(X6)))),inference(variable_rename,[status(thm)],[c17])).
% 0.91/1.12 cnf(c19,plain,~in(X84,X83)|set_intersection2(X83,singleton(X84))=singleton(X84),inference(split_conjunct,[status(thm)],[c18])).
% 0.91/1.12 cnf(reflexivity,axiom,X24=X24,theory(equality)).
% 0.91/1.12 fof(d2_tarski,axiom,(![A]:(![B]:(![C]:(C=unordered_pair(A,B)<=>(![D]:(in(D,C)<=>(D=A|D=B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d2_tarski)).
% 0.91/1.12 fof(c23,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])).
% 0.91/1.12 fof(c24,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)],[c23])).
% 0.91/1.12 fof(c25,plain,((![X9]:(![X10]:(![X11]:(X11!=unordered_pair(X9,X10)|((![X12]:(~in(X12,X11)|(X12=X9|X12=X10)))&(![X13]:((X13!=X9&X13!=X10)|in(X13,X11))))))))&(![X14]:(![X15]:(![X16]:((?[X17]:((~in(X17,X16)|(X17!=X14&X17!=X15))&(in(X17,X16)|(X17=X14|X17=X15))))|X16=unordered_pair(X14,X15)))))),inference(variable_rename,[status(thm)],[c24])).
% 0.91/1.12 fof(c27,plain,(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:((X11!=unordered_pair(X9,X10)|((~in(X12,X11)|(X12=X9|X12=X10))&((X13!=X9&X13!=X10)|in(X13,X11))))&(((~in(skolem0005(X14,X15,X16),X16)|(skolem0005(X14,X15,X16)!=X14&skolem0005(X14,X15,X16)!=X15))&(in(skolem0005(X14,X15,X16),X16)|(skolem0005(X14,X15,X16)=X14|skolem0005(X14,X15,X16)=X15)))|X16=unordered_pair(X14,X15))))))))))),inference(shift_quantors,[status(thm)],[fof(c26,plain,((![X9]:(![X10]:(![X11]:(X11!=unordered_pair(X9,X10)|((![X12]:(~in(X12,X11)|(X12=X9|X12=X10)))&(![X13]:((X13!=X9&X13!=X10)|in(X13,X11))))))))&(![X14]:(![X15]:(![X16]:(((~in(skolem0005(X14,X15,X16),X16)|(skolem0005(X14,X15,X16)!=X14&skolem0005(X14,X15,X16)!=X15))&(in(skolem0005(X14,X15,X16),X16)|(skolem0005(X14,X15,X16)=X14|skolem0005(X14,X15,X16)=X15)))|X16=unordered_pair(X14,X15)))))),inference(skolemize,[status(esa)],[c25])).])).
% 0.91/1.12 fof(c28,plain,(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:(((X11!=unordered_pair(X9,X10)|(~in(X12,X11)|(X12=X9|X12=X10)))&((X11!=unordered_pair(X9,X10)|(X13!=X9|in(X13,X11)))&(X11!=unordered_pair(X9,X10)|(X13!=X10|in(X13,X11)))))&((((~in(skolem0005(X14,X15,X16),X16)|skolem0005(X14,X15,X16)!=X14)|X16=unordered_pair(X14,X15))&((~in(skolem0005(X14,X15,X16),X16)|skolem0005(X14,X15,X16)!=X15)|X16=unordered_pair(X14,X15)))&((in(skolem0005(X14,X15,X16),X16)|(skolem0005(X14,X15,X16)=X14|skolem0005(X14,X15,X16)=X15))|X16=unordered_pair(X14,X15)))))))))))),inference(distribute,[status(thm)],[c27])).
% 0.91/1.12 cnf(c30,plain,X101!=unordered_pair(X100,X102)|X103!=X100|in(X103,X101),inference(split_conjunct,[status(thm)],[c28])).
% 0.91/1.12 cnf(c134,plain,X107!=X106|in(X107,unordered_pair(X106,X105)),inference(resolution,[status(thm)],[c30, reflexivity])).
% 0.91/1.12 cnf(c142,plain,in(X108,unordered_pair(X108,X109)),inference(resolution,[status(thm)],[c134, reflexivity])).
% 0.91/1.12 cnf(c148,plain,set_intersection2(unordered_pair(X413,X412),singleton(X413))=singleton(X413),inference(resolution,[status(thm)],[c142, c19])).
% 0.91/1.12 cnf(c1174,plain,singleton(X591)=set_intersection2(unordered_pair(X591,X592),singleton(X591)),inference(resolution,[status(thm)],[c148, symmetry])).
% 0.91/1.12 cnf(c2150,plain,singleton(X634)=set_intersection2(singleton(X634),unordered_pair(X634,X635)),inference(resolution,[status(thm)],[c1174, c69])).
% 0.91/1.12 cnf(c2213,plain,set_intersection2(singleton(X653),unordered_pair(X653,X654))=singleton(X653),inference(resolution,[status(thm)],[c2150, symmetry])).
% 0.91/1.12 cnf(c2326,plain,$false,inference(resolution,[status(thm)],[c2213, c9])).
% 0.91/1.12 % SZS output end CNFRefutation
% 0.91/1.12
% 0.91/1.12 % Initial clauses : 22
% 0.91/1.12 % Processed clauses : 174
% 0.91/1.12 % Factors computed : 5
% 0.91/1.12 % Resolvents computed: 2348
% 0.91/1.12 % Tautologies deleted: 3
% 0.91/1.12 % Forward subsumed : 171
% 0.91/1.12 % Backward subsumed : 0
% 0.91/1.12 % -------- CPU Time ---------
% 0.91/1.12 % User time : 0.741 s
% 0.91/1.12 % System time : 0.017 s
% 0.91/1.12 % Total time : 0.758 s
%------------------------------------------------------------------------------