%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU149+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n009.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 0.19s 0.47s
% Output : Refutation 0.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SEU149+1 : TPTP v8.1.2. Released v3.3.0.
% 0.12/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.33 % Computer : n009.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Wed May 8 11:46:37 EDT 2024
% 0.13/0.33 % CPUTime :
% 0.19/0.47 % Version: 1.5
% 0.19/0.47 % SZS status Theorem
% 0.19/0.47 % SZS output start CNFRefutation
% 0.19/0.47 fof(t8_zfmisc_1,conjecture,(![A]:(![B]:(![C]:(singleton(A)=unordered_pair(B,C)=>A=B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t8_zfmisc_1)).
% 0.19/0.47 fof(c3,negated_conjecture,(~(![A]:(![B]:(![C]:(singleton(A)=unordered_pair(B,C)=>A=B))))),inference(assume_negation,[status(cth)],[t8_zfmisc_1])).
% 0.19/0.47 fof(c4,negated_conjecture,(?[A]:(?[B]:(?[C]:(singleton(A)=unordered_pair(B,C)&A!=B)))),inference(fof_nnf,[status(thm)],[c3])).
% 0.19/0.47 fof(c5,negated_conjecture,(?[A]:(?[B]:((?[C]:singleton(A)=unordered_pair(B,C))&A!=B))),inference(shift_quantors,[status(thm)],[c4])).
% 0.19/0.47 fof(c6,negated_conjecture,(?[X2]:(?[X3]:((?[X4]:singleton(X2)=unordered_pair(X3,X4))&X2!=X3))),inference(variable_rename,[status(thm)],[c5])).
% 0.19/0.47 fof(c7,negated_conjecture,(singleton(skolem0001)=unordered_pair(skolem0002,skolem0003)&skolem0001!=skolem0002),inference(skolemize,[status(esa)],[c6])).
% 0.19/0.47 cnf(c9,negated_conjecture,skolem0001!=skolem0002,inference(split_conjunct,[status(thm)],[c7])).
% 0.19/0.47 cnf(symmetry,axiom,X26!=X27|X27=X26,theory(equality)).
% 0.19/0.47 cnf(reflexivity,axiom,X25=X25,theory(equality)).
% 0.19/0.47 fof(d1_tarski,axiom,(![A]:(![B]:(B=singleton(A)<=>(![C]:(in(C,B)<=>C=A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', d1_tarski)).
% 0.19/0.47 fof(c24,plain,(![A]:(![B]:((B!=singleton(A)|(![C]:((~in(C,B)|C=A)&(C!=A|in(C,B)))))&((?[C]:((~in(C,B)|C!=A)&(in(C,B)|C=A)))|B=singleton(A))))),inference(fof_nnf,[status(thm)],[d1_tarski])).
% 0.19/0.47 fof(c25,plain,((![A]:(![B]:(B!=singleton(A)|((![C]:(~in(C,B)|C=A))&(![C]:(C!=A|in(C,B)))))))&(![A]:(![B]:((?[C]:((~in(C,B)|C!=A)&(in(C,B)|C=A)))|B=singleton(A))))),inference(shift_quantors,[status(thm)],[c24])).
% 0.19/0.47 fof(c26,plain,((![X14]:(![X15]:(X15!=singleton(X14)|((![X16]:(~in(X16,X15)|X16=X14))&(![X17]:(X17!=X14|in(X17,X15)))))))&(![X18]:(![X19]:((?[X20]:((~in(X20,X19)|X20!=X18)&(in(X20,X19)|X20=X18)))|X19=singleton(X18))))),inference(variable_rename,[status(thm)],[c25])).
% 0.19/0.47 fof(c28,plain,(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:((X15!=singleton(X14)|((~in(X16,X15)|X16=X14)&(X17!=X14|in(X17,X15))))&(((~in(skolem0005(X18,X19),X19)|skolem0005(X18,X19)!=X18)&(in(skolem0005(X18,X19),X19)|skolem0005(X18,X19)=X18))|X19=singleton(X18))))))))),inference(shift_quantors,[status(thm)],[fof(c27,plain,((![X14]:(![X15]:(X15!=singleton(X14)|((![X16]:(~in(X16,X15)|X16=X14))&(![X17]:(X17!=X14|in(X17,X15)))))))&(![X18]:(![X19]:(((~in(skolem0005(X18,X19),X19)|skolem0005(X18,X19)!=X18)&(in(skolem0005(X18,X19),X19)|skolem0005(X18,X19)=X18))|X19=singleton(X18))))),inference(skolemize,[status(esa)],[c26])).])).
% 0.19/0.47 fof(c29,plain,(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(((X15!=singleton(X14)|(~in(X16,X15)|X16=X14))&(X15!=singleton(X14)|(X17!=X14|in(X17,X15))))&(((~in(skolem0005(X18,X19),X19)|skolem0005(X18,X19)!=X18)|X19=singleton(X18))&((in(skolem0005(X18,X19),X19)|skolem0005(X18,X19)=X18)|X19=singleton(X18)))))))))),inference(distribute,[status(thm)],[c28])).
% 0.19/0.47 cnf(c30,plain,X54!=singleton(X53)|~in(X55,X54)|X55=X53,inference(split_conjunct,[status(thm)],[c29])).
% 0.19/0.47 cnf(c60,plain,~in(X56,singleton(X57))|X56=X57,inference(resolution,[status(thm)],[c30, reflexivity])).
% 0.19/0.47 cnf(c8,negated_conjecture,singleton(skolem0001)=unordered_pair(skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c7])).
% 0.19/0.47 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)).
% 0.19/0.47 fof(c12,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.19/0.47 fof(c13,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)],[c12])).
% 0.19/0.47 fof(c14,plain,((![X5]:(![X6]:(![X7]:(X7!=unordered_pair(X5,X6)|((![X8]:(~in(X8,X7)|(X8=X5|X8=X6)))&(![X9]:((X9!=X5&X9!=X6)|in(X9,X7))))))))&(![X10]:(![X11]:(![X12]:((?[X13]:((~in(X13,X12)|(X13!=X10&X13!=X11))&(in(X13,X12)|(X13=X10|X13=X11))))|X12=unordered_pair(X10,X11)))))),inference(variable_rename,[status(thm)],[c13])).
% 0.19/0.47 fof(c16,plain,(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:((X7!=unordered_pair(X5,X6)|((~in(X8,X7)|(X8=X5|X8=X6))&((X9!=X5&X9!=X6)|in(X9,X7))))&(((~in(skolem0004(X10,X11,X12),X12)|(skolem0004(X10,X11,X12)!=X10&skolem0004(X10,X11,X12)!=X11))&(in(skolem0004(X10,X11,X12),X12)|(skolem0004(X10,X11,X12)=X10|skolem0004(X10,X11,X12)=X11)))|X12=unordered_pair(X10,X11))))))))))),inference(shift_quantors,[status(thm)],[fof(c15,plain,((![X5]:(![X6]:(![X7]:(X7!=unordered_pair(X5,X6)|((![X8]:(~in(X8,X7)|(X8=X5|X8=X6)))&(![X9]:((X9!=X5&X9!=X6)|in(X9,X7))))))))&(![X10]:(![X11]:(![X12]:(((~in(skolem0004(X10,X11,X12),X12)|(skolem0004(X10,X11,X12)!=X10&skolem0004(X10,X11,X12)!=X11))&(in(skolem0004(X10,X11,X12),X12)|(skolem0004(X10,X11,X12)=X10|skolem0004(X10,X11,X12)=X11)))|X12=unordered_pair(X10,X11)))))),inference(skolemize,[status(esa)],[c14])).])).
% 0.19/0.47 fof(c17,plain,(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(((X7!=unordered_pair(X5,X6)|(~in(X8,X7)|(X8=X5|X8=X6)))&((X7!=unordered_pair(X5,X6)|(X9!=X5|in(X9,X7)))&(X7!=unordered_pair(X5,X6)|(X9!=X6|in(X9,X7)))))&((((~in(skolem0004(X10,X11,X12),X12)|skolem0004(X10,X11,X12)!=X10)|X12=unordered_pair(X10,X11))&((~in(skolem0004(X10,X11,X12),X12)|skolem0004(X10,X11,X12)!=X11)|X12=unordered_pair(X10,X11)))&((in(skolem0004(X10,X11,X12),X12)|(skolem0004(X10,X11,X12)=X10|skolem0004(X10,X11,X12)=X11))|X12=unordered_pair(X10,X11)))))))))))),inference(distribute,[status(thm)],[c16])).
% 0.19/0.47 cnf(c19,plain,X74!=unordered_pair(X75,X73)|X72!=X75|in(X72,X74),inference(split_conjunct,[status(thm)],[c17])).
% 0.19/0.47 cnf(c78,plain,X107!=skolem0002|in(X107,singleton(skolem0001)),inference(resolution,[status(thm)],[c19, c8])).
% 0.19/0.47 cnf(c94,plain,in(skolem0002,singleton(skolem0001)),inference(resolution,[status(thm)],[c78, reflexivity])).
% 0.19/0.47 cnf(c97,plain,skolem0002=skolem0001,inference(resolution,[status(thm)],[c94, c60])).
% 0.19/0.47 cnf(c104,plain,skolem0001=skolem0002,inference(resolution,[status(thm)],[c97, symmetry])).
% 0.19/0.47 cnf(c112,plain,$false,inference(resolution,[status(thm)],[c104, c9])).
% 0.19/0.47 % SZS output end CNFRefutation
% 0.19/0.47
% 0.19/0.47 % Initial clauses : 22
% 0.19/0.47 % Processed clauses : 35
% 0.19/0.47 % Factors computed : 3
% 0.19/0.47 % Resolvents computed: 71
% 0.19/0.47 % Tautologies deleted: 2
% 0.19/0.47 % Forward subsumed : 9
% 0.19/0.47 % Backward subsumed : 0
% 0.19/0.47 % -------- CPU Time ---------
% 0.19/0.47 % User time : 0.114 s
% 0.19/0.47 % System time : 0.015 s
% 0.19/0.47 % Total time : 0.129 s
%------------------------------------------------------------------------------