%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU150+2 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n010.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:40 EDT 2024
% Result : Theorem 183.54s 183.71s
% Output : Refutation 183.54s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SEU150+2 : TPTP v8.1.2. Released v3.3.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n010.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.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 11:43:23 EDT 2024
% 0.13/0.35 % CPUTime :
% 183.54/183.71 % Version: 1.5
% 183.54/183.71 % SZS status Theorem
% 183.54/183.71 % SZS output start CNFRefutation
% 183.54/183.71 fof(t9_zfmisc_1,conjecture,(![A]:(![B]:(![C]:(singleton(A)=unordered_pair(B,C)=>B=C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t9_zfmisc_1)).
% 183.54/183.71 fof(c11,negated_conjecture,(~(![A]:(![B]:(![C]:(singleton(A)=unordered_pair(B,C)=>B=C))))),inference(assume_negation,[status(cth)],[t9_zfmisc_1])).
% 183.54/183.71 fof(c12,negated_conjecture,(?[A]:(?[B]:(?[C]:(singleton(A)=unordered_pair(B,C)&B!=C)))),inference(fof_nnf,[status(thm)],[c11])).
% 183.54/183.71 fof(c13,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(singleton(X2)=unordered_pair(X3,X4)&X3!=X4)))),inference(variable_rename,[status(thm)],[c12])).
% 183.54/183.71 fof(c14,negated_conjecture,(singleton(skolem0001)=unordered_pair(skolem0002,skolem0003)&skolem0002!=skolem0003),inference(skolemize,[status(esa)],[c13])).
% 183.54/183.71 cnf(c16,negated_conjecture,skolem0002!=skolem0003,inference(split_conjunct,[status(thm)],[c14])).
% 183.54/183.71 cnf(symmetry,axiom,X195!=X196|X196=X195,theory(equality)).
% 183.54/183.71 cnf(transitivity,axiom,X200!=X202|X202!=X201|X200=X201,theory(equality)).
% 183.54/183.71 cnf(c15,negated_conjecture,singleton(skolem0001)=unordered_pair(skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c14])).
% 183.54/183.71 fof(t8_zfmisc_1,plain,(![A]:(![B]:(![C]:(singleton(A)=unordered_pair(B,C)=>A=B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t8_zfmisc_1)).
% 183.54/183.71 fof(c17,plain,(![A]:(![B]:(![C]:(singleton(A)!=unordered_pair(B,C)|A=B)))),inference(fof_nnf,[status(thm)],[t8_zfmisc_1])).
% 183.54/183.71 fof(c18,plain,(![A]:(![B]:((![C]:singleton(A)!=unordered_pair(B,C))|A=B))),inference(shift_quantors,[status(thm)],[c17])).
% 183.54/183.71 fof(c20,plain,(![X5]:(![X6]:(![X7]:(singleton(X5)!=unordered_pair(X6,X7)|X5=X6)))),inference(shift_quantors,[status(thm)],[fof(c19,plain,(![X5]:(![X6]:((![X7]:singleton(X5)!=unordered_pair(X6,X7))|X5=X6))),inference(variable_rename,[status(thm)],[c18])).])).
% 183.54/183.71 cnf(c21,plain,singleton(X310)!=unordered_pair(X309,X311)|X310=X309,inference(split_conjunct,[status(thm)],[c20])).
% 183.54/183.71 cnf(c486,plain,skolem0001=skolem0002,inference(resolution,[status(thm)],[c21, c15])).
% 183.54/183.71 cnf(c491,plain,X1247!=skolem0001|X1247=skolem0002,inference(resolution,[status(thm)],[c486, transitivity])).
% 183.54/183.71 fof(t69_enumset1,plain,(![A]:unordered_pair(A,A)=singleton(A)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t69_enumset1)).
% 183.54/183.71 fof(c45,plain,(![X24]:unordered_pair(X24,X24)=singleton(X24)),inference(variable_rename,[status(thm)],[t69_enumset1])).
% 183.54/183.71 cnf(c46,plain,unordered_pair(X336,X336)=singleton(X336),inference(split_conjunct,[status(thm)],[c45])).
% 183.54/183.71 cnf(c549,plain,singleton(X368)=unordered_pair(X368,X368),inference(resolution,[status(thm)],[c46, symmetry])).
% 183.54/183.71 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)).
% 183.54/183.71 fof(c261,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])).
% 183.54/183.71 fof(c262,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)],[c261])).
% 183.54/183.71 fof(c263,plain,((![X152]:(![X153]:(![X154]:(X154!=unordered_pair(X152,X153)|((![X155]:(~in(X155,X154)|(X155=X152|X155=X153)))&(![X156]:((X156!=X152&X156!=X153)|in(X156,X154))))))))&(![X157]:(![X158]:(![X159]:((?[X160]:((~in(X160,X159)|(X160!=X157&X160!=X158))&(in(X160,X159)|(X160=X157|X160=X158))))|X159=unordered_pair(X157,X158)))))),inference(variable_rename,[status(thm)],[c262])).
% 183.54/183.71 fof(c265,plain,(![X152]:(![X153]:(![X154]:(![X155]:(![X156]:(![X157]:(![X158]:(![X159]:((X154!=unordered_pair(X152,X153)|((~in(X155,X154)|(X155=X152|X155=X153))&((X156!=X152&X156!=X153)|in(X156,X154))))&(((~in(skolem0013(X157,X158,X159),X159)|(skolem0013(X157,X158,X159)!=X157&skolem0013(X157,X158,X159)!=X158))&(in(skolem0013(X157,X158,X159),X159)|(skolem0013(X157,X158,X159)=X157|skolem0013(X157,X158,X159)=X158)))|X159=unordered_pair(X157,X158))))))))))),inference(shift_quantors,[status(thm)],[fof(c264,plain,((![X152]:(![X153]:(![X154]:(X154!=unordered_pair(X152,X153)|((![X155]:(~in(X155,X154)|(X155=X152|X155=X153)))&(![X156]:((X156!=X152&X156!=X153)|in(X156,X154))))))))&(![X157]:(![X158]:(![X159]:(((~in(skolem0013(X157,X158,X159),X159)|(skolem0013(X157,X158,X159)!=X157&skolem0013(X157,X158,X159)!=X158))&(in(skolem0013(X157,X158,X159),X159)|(skolem0013(X157,X158,X159)=X157|skolem0013(X157,X158,X159)=X158)))|X159=unordered_pair(X157,X158)))))),inference(skolemize,[status(esa)],[c263])).])).
% 183.54/183.71 fof(c266,plain,(![X152]:(![X153]:(![X154]:(![X155]:(![X156]:(![X157]:(![X158]:(![X159]:(((X154!=unordered_pair(X152,X153)|(~in(X155,X154)|(X155=X152|X155=X153)))&((X154!=unordered_pair(X152,X153)|(X156!=X152|in(X156,X154)))&(X154!=unordered_pair(X152,X153)|(X156!=X153|in(X156,X154)))))&((((~in(skolem0013(X157,X158,X159),X159)|skolem0013(X157,X158,X159)!=X157)|X159=unordered_pair(X157,X158))&((~in(skolem0013(X157,X158,X159),X159)|skolem0013(X157,X158,X159)!=X158)|X159=unordered_pair(X157,X158)))&((in(skolem0013(X157,X158,X159),X159)|(skolem0013(X157,X158,X159)=X157|skolem0013(X157,X158,X159)=X158))|X159=unordered_pair(X157,X158)))))))))))),inference(distribute,[status(thm)],[c265])).
% 183.54/183.71 cnf(c267,plain,X809!=unordered_pair(X811,X810)|~in(X808,X809)|X808=X811|X808=X810,inference(split_conjunct,[status(thm)],[c266])).
% 183.54/183.71 cnf(c1877,plain,~in(X2044,singleton(X2043))|X2044=X2043,inference(resolution,[status(thm)],[c267, c549])).
% 183.54/183.71 cnf(reflexivity,axiom,X193=X193,theory(equality)).
% 183.54/183.71 cnf(c269,plain,X833!=unordered_pair(X836,X835)|X834!=X835|in(X834,X833),inference(split_conjunct,[status(thm)],[c266])).
% 183.54/183.71 cnf(c1931,plain,X9869!=skolem0003|in(X9869,singleton(skolem0001)),inference(resolution,[status(thm)],[c269, c15])).
% 183.54/183.71 cnf(c179519,plain,in(skolem0003,singleton(skolem0001)),inference(resolution,[status(thm)],[c1931, reflexivity])).
% 183.54/183.71 cnf(c179578,plain,skolem0003=skolem0001,inference(resolution,[status(thm)],[c179519, c1877])).
% 183.54/183.71 cnf(c179706,plain,skolem0003=skolem0002,inference(resolution,[status(thm)],[c179578, c491])).
% 183.54/183.71 cnf(c180549,plain,skolem0002=skolem0003,inference(resolution,[status(thm)],[c179706, symmetry])).
% 183.54/183.71 cnf(c181574,plain,$false,inference(resolution,[status(thm)],[c180549, c16])).
% 183.54/183.71 % SZS output end CNFRefutation
% 183.54/183.71
% 183.54/183.71 % Initial clauses : 132
% 183.54/183.71 % Processed clauses : 2062
% 183.54/183.71 % Factors computed : 144
% 183.54/183.71 % Resolvents computed: 181209
% 183.54/183.71 % Tautologies deleted: 75
% 183.54/183.71 % Forward subsumed : 5192
% 183.54/183.71 % Backward subsumed : 107
% 183.54/183.71 % -------- CPU Time ---------
% 183.54/183.71 % User time : 183.021 s
% 183.54/183.71 % System time : 0.346 s
% 183.54/183.71 % Total time : 183.367 s
%------------------------------------------------------------------------------