%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU151+3 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n028.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:41 EDT 2024
% Result : Theorem 0.45s 0.67s
% Output : Refutation 0.45s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : SEU151+3 : TPTP v8.1.2. Released v3.2.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n028.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 11:37:53 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.45/0.67 % Version: 1.5
% 0.45/0.67 % SZS status Theorem
% 0.45/0.67 % SZS output start CNFRefutation
% 0.45/0.67 fof(t10_zfmisc_1,conjecture,(![A]:(![B]:(![C]:(![D]:(~((unordered_pair(A,B)=unordered_pair(C,D)&A!=C)&A!=D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t10_zfmisc_1)).
% 0.45/0.67 fof(c3,negated_conjecture,(~(![A]:(![B]:(![C]:(![D]:(~((unordered_pair(A,B)=unordered_pair(C,D)&A!=C)&A!=D))))))),inference(assume_negation,[status(cth)],[t10_zfmisc_1])).
% 0.45/0.67 fof(c4,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:((unordered_pair(A,B)=unordered_pair(C,D)&A!=C)&A!=D))))),inference(fof_nnf,[status(thm)],[c3])).
% 0.45/0.67 fof(c5,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:((unordered_pair(X2,X3)=unordered_pair(X4,X5)&X2!=X4)&X2!=X5))))),inference(variable_rename,[status(thm)],[c4])).
% 0.45/0.67 fof(c6,negated_conjecture,((unordered_pair(skolem0001,skolem0002)=unordered_pair(skolem0003,skolem0004)&skolem0001!=skolem0003)&skolem0001!=skolem0004),inference(skolemize,[status(esa)],[c5])).
% 0.45/0.67 cnf(c9,negated_conjecture,skolem0001!=skolem0004,inference(split_conjunct,[status(thm)],[c6])).
% 0.45/0.67 cnf(c8,negated_conjecture,skolem0001!=skolem0003,inference(split_conjunct,[status(thm)],[c6])).
% 0.45/0.67 cnf(reflexivity,axiom,X21=X21,theory(equality)).
% 0.45/0.67 cnf(symmetry,axiom,X22!=X23|X23=X22,theory(equality)).
% 0.45/0.67 cnf(c7,negated_conjecture,unordered_pair(skolem0001,skolem0002)=unordered_pair(skolem0003,skolem0004),inference(split_conjunct,[status(thm)],[c6])).
% 0.45/0.67 cnf(c49,plain,unordered_pair(skolem0003,skolem0004)=unordered_pair(skolem0001,skolem0002),inference(resolution,[status(thm)],[c7, symmetry])).
% 0.45/0.67 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.45/0.67 fof(c17,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.45/0.67 fof(c18,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)],[c17])).
% 0.45/0.67 fof(c19,plain,((![X8]:(![X9]:(![X10]:(X10!=unordered_pair(X8,X9)|((![X11]:(~in(X11,X10)|(X11=X8|X11=X9)))&(![X12]:((X12!=X8&X12!=X9)|in(X12,X10))))))))&(![X13]:(![X14]:(![X15]:((?[X16]:((~in(X16,X15)|(X16!=X13&X16!=X14))&(in(X16,X15)|(X16=X13|X16=X14))))|X15=unordered_pair(X13,X14)))))),inference(variable_rename,[status(thm)],[c18])).
% 0.45/0.67 fof(c21,plain,(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:((X10!=unordered_pair(X8,X9)|((~in(X11,X10)|(X11=X8|X11=X9))&((X12!=X8&X12!=X9)|in(X12,X10))))&(((~in(skolem0007(X13,X14,X15),X15)|(skolem0007(X13,X14,X15)!=X13&skolem0007(X13,X14,X15)!=X14))&(in(skolem0007(X13,X14,X15),X15)|(skolem0007(X13,X14,X15)=X13|skolem0007(X13,X14,X15)=X14)))|X15=unordered_pair(X13,X14))))))))))),inference(shift_quantors,[status(thm)],[fof(c20,plain,((![X8]:(![X9]:(![X10]:(X10!=unordered_pair(X8,X9)|((![X11]:(~in(X11,X10)|(X11=X8|X11=X9)))&(![X12]:((X12!=X8&X12!=X9)|in(X12,X10))))))))&(![X13]:(![X14]:(![X15]:(((~in(skolem0007(X13,X14,X15),X15)|(skolem0007(X13,X14,X15)!=X13&skolem0007(X13,X14,X15)!=X14))&(in(skolem0007(X13,X14,X15),X15)|(skolem0007(X13,X14,X15)=X13|skolem0007(X13,X14,X15)=X14)))|X15=unordered_pair(X13,X14)))))),inference(skolemize,[status(esa)],[c19])).])).
% 0.45/0.67 fof(c22,plain,(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(((X10!=unordered_pair(X8,X9)|(~in(X11,X10)|(X11=X8|X11=X9)))&((X10!=unordered_pair(X8,X9)|(X12!=X8|in(X12,X10)))&(X10!=unordered_pair(X8,X9)|(X12!=X9|in(X12,X10)))))&((((~in(skolem0007(X13,X14,X15),X15)|skolem0007(X13,X14,X15)!=X13)|X15=unordered_pair(X13,X14))&((~in(skolem0007(X13,X14,X15),X15)|skolem0007(X13,X14,X15)!=X14)|X15=unordered_pair(X13,X14)))&((in(skolem0007(X13,X14,X15),X15)|(skolem0007(X13,X14,X15)=X13|skolem0007(X13,X14,X15)=X14))|X15=unordered_pair(X13,X14)))))))))))),inference(distribute,[status(thm)],[c21])).
% 0.45/0.67 cnf(c24,plain,X71!=unordered_pair(X70,X73)|X72!=X70|in(X72,X71),inference(split_conjunct,[status(thm)],[c22])).
% 0.45/0.67 cnf(c99,plain,X122!=skolem0001|in(X122,unordered_pair(skolem0003,skolem0004)),inference(resolution,[status(thm)],[c24, c49])).
% 0.45/0.67 cnf(c214,plain,in(skolem0001,unordered_pair(skolem0003,skolem0004)),inference(resolution,[status(thm)],[c99, reflexivity])).
% 0.45/0.67 cnf(c23,plain,X67!=unordered_pair(X66,X69)|~in(X68,X67)|X68=X66|X68=X69,inference(split_conjunct,[status(thm)],[c22])).
% 0.45/0.67 cnf(c73,plain,~in(X153,unordered_pair(X152,X151))|X153=X152|X153=X151,inference(resolution,[status(thm)],[c23, reflexivity])).
% 0.45/0.67 cnf(c331,plain,skolem0001=skolem0003|skolem0001=skolem0004,inference(resolution,[status(thm)],[c73, c214])).
% 0.45/0.67 cnf(c407,plain,skolem0001=skolem0004,inference(resolution,[status(thm)],[c331, c8])).
% 0.45/0.67 cnf(c451,plain,$false,inference(resolution,[status(thm)],[c407, c9])).
% 0.45/0.67 % SZS output end CNFRefutation
% 0.45/0.67
% 0.45/0.67 % Initial clauses : 19
% 0.45/0.67 % Processed clauses : 79
% 0.45/0.67 % Factors computed : 4
% 0.45/0.67 % Resolvents computed: 415
% 0.45/0.67 % Tautologies deleted: 3
% 0.45/0.67 % Forward subsumed : 33
% 0.45/0.67 % Backward subsumed : 1
% 0.45/0.67 % -------- CPU Time ---------
% 0.45/0.67 % User time : 0.293 s
% 0.45/0.67 % System time : 0.018 s
% 0.45/0.67 % Total time : 0.311 s
%------------------------------------------------------------------------------