%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET872+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n020.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 8.11s 8.32s
% Output : Refutation 8.11s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : SET872+1 : TPTP v8.1.2. Released v3.2.0.
% 0.04/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n020.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Wed May 8 18:59:23 EDT 2024
% 0.14/0.36 % CPUTime :
% 8.11/8.32 % Version: 1.5
% 8.11/8.32 % SZS status Theorem
% 8.11/8.32 % SZS output start CNFRefutation
% 8.11/8.32 fof(t12_zfmisc_1,conjecture,(![A]:(![B]:subset(singleton(A),unordered_pair(A,B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t12_zfmisc_1)).
% 8.11/8.32 fof(c5,negated_conjecture,(~(![A]:(![B]:subset(singleton(A),unordered_pair(A,B))))),inference(assume_negation,[status(cth)],[t12_zfmisc_1])).
% 8.11/8.32 fof(c6,negated_conjecture,(?[A]:(?[B]:~subset(singleton(A),unordered_pair(A,B)))),inference(fof_nnf,[status(thm)],[c5])).
% 8.11/8.32 fof(c7,negated_conjecture,(?[X2]:(?[X3]:~subset(singleton(X2),unordered_pair(X2,X3)))),inference(variable_rename,[status(thm)],[c6])).
% 8.11/8.32 fof(c8,negated_conjecture,~subset(singleton(skolem0001),unordered_pair(skolem0001,skolem0002)),inference(skolemize,[status(esa)],[c7])).
% 8.11/8.32 cnf(c9,negated_conjecture,~subset(singleton(skolem0001),unordered_pair(skolem0001,skolem0002)),inference(split_conjunct,[status(thm)],[c8])).
% 8.11/8.32 fof(d3_tarski,axiom,(![A]:(![B]:(subset(A,B)<=>(![C]:(in(C,A)=>in(C,B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d3_tarski)).
% 8.11/8.32 fof(c20,plain,(![A]:(![B]:((~subset(A,B)|(![C]:(~in(C,A)|in(C,B))))&((?[C]:(in(C,A)&~in(C,B)))|subset(A,B))))),inference(fof_nnf,[status(thm)],[d3_tarski])).
% 8.11/8.32 fof(c21,plain,((![A]:(![B]:(~subset(A,B)|(![C]:(~in(C,A)|in(C,B))))))&(![A]:(![B]:((?[C]:(in(C,A)&~in(C,B)))|subset(A,B))))),inference(shift_quantors,[status(thm)],[c20])).
% 8.11/8.32 fof(c22,plain,((![X7]:(![X8]:(~subset(X7,X8)|(![X9]:(~in(X9,X7)|in(X9,X8))))))&(![X10]:(![X11]:((?[X12]:(in(X12,X10)&~in(X12,X11)))|subset(X10,X11))))),inference(variable_rename,[status(thm)],[c21])).
% 8.11/8.32 fof(c24,plain,(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:((~subset(X7,X8)|(~in(X9,X7)|in(X9,X8)))&((in(skolem0005(X10,X11),X10)&~in(skolem0005(X10,X11),X11))|subset(X10,X11)))))))),inference(shift_quantors,[status(thm)],[fof(c23,plain,((![X7]:(![X8]:(~subset(X7,X8)|(![X9]:(~in(X9,X7)|in(X9,X8))))))&(![X10]:(![X11]:((in(skolem0005(X10,X11),X10)&~in(skolem0005(X10,X11),X11))|subset(X10,X11))))),inference(skolemize,[status(esa)],[c22])).])).
% 8.11/8.32 fof(c25,plain,(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:((~subset(X7,X8)|(~in(X9,X7)|in(X9,X8)))&((in(skolem0005(X10,X11),X10)|subset(X10,X11))&(~in(skolem0005(X10,X11),X11)|subset(X10,X11))))))))),inference(distribute,[status(thm)],[c24])).
% 8.11/8.32 cnf(c28,plain,~in(skolem0005(X64,X63),X63)|subset(X64,X63),inference(split_conjunct,[status(thm)],[c25])).
% 8.11/8.32 cnf(reflexivity,axiom,X33=X33,theory(equality)).
% 8.11/8.32 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)).
% 8.11/8.32 fof(c29,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])).
% 8.11/8.32 fof(c30,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)],[c29])).
% 8.11/8.32 fof(c31,plain,((![X13]:(![X14]:(![X15]:(X15!=unordered_pair(X13,X14)|((![X16]:(~in(X16,X15)|(X16=X13|X16=X14)))&(![X17]:((X17!=X13&X17!=X14)|in(X17,X15))))))))&(![X18]:(![X19]:(![X20]:((?[X21]:((~in(X21,X20)|(X21!=X18&X21!=X19))&(in(X21,X20)|(X21=X18|X21=X19))))|X20=unordered_pair(X18,X19)))))),inference(variable_rename,[status(thm)],[c30])).
% 8.11/8.32 fof(c33,plain,(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:((X15!=unordered_pair(X13,X14)|((~in(X16,X15)|(X16=X13|X16=X14))&((X17!=X13&X17!=X14)|in(X17,X15))))&(((~in(skolem0006(X18,X19,X20),X20)|(skolem0006(X18,X19,X20)!=X18&skolem0006(X18,X19,X20)!=X19))&(in(skolem0006(X18,X19,X20),X20)|(skolem0006(X18,X19,X20)=X18|skolem0006(X18,X19,X20)=X19)))|X20=unordered_pair(X18,X19))))))))))),inference(shift_quantors,[status(thm)],[fof(c32,plain,((![X13]:(![X14]:(![X15]:(X15!=unordered_pair(X13,X14)|((![X16]:(~in(X16,X15)|(X16=X13|X16=X14)))&(![X17]:((X17!=X13&X17!=X14)|in(X17,X15))))))))&(![X18]:(![X19]:(![X20]:(((~in(skolem0006(X18,X19,X20),X20)|(skolem0006(X18,X19,X20)!=X18&skolem0006(X18,X19,X20)!=X19))&(in(skolem0006(X18,X19,X20),X20)|(skolem0006(X18,X19,X20)=X18|skolem0006(X18,X19,X20)=X19)))|X20=unordered_pair(X18,X19)))))),inference(skolemize,[status(esa)],[c31])).])).
% 8.11/8.32 fof(c34,plain,(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:(((X15!=unordered_pair(X13,X14)|(~in(X16,X15)|(X16=X13|X16=X14)))&((X15!=unordered_pair(X13,X14)|(X17!=X13|in(X17,X15)))&(X15!=unordered_pair(X13,X14)|(X17!=X14|in(X17,X15)))))&((((~in(skolem0006(X18,X19,X20),X20)|skolem0006(X18,X19,X20)!=X18)|X20=unordered_pair(X18,X19))&((~in(skolem0006(X18,X19,X20),X20)|skolem0006(X18,X19,X20)!=X19)|X20=unordered_pair(X18,X19)))&((in(skolem0006(X18,X19,X20),X20)|(skolem0006(X18,X19,X20)=X18|skolem0006(X18,X19,X20)=X19))|X20=unordered_pair(X18,X19)))))))))))),inference(distribute,[status(thm)],[c33])).
% 8.11/8.32 cnf(c36,plain,X112!=unordered_pair(X109,X111)|X110!=X109|in(X110,X112),inference(split_conjunct,[status(thm)],[c34])).
% 8.11/8.32 cnf(c96,plain,X122!=X123|in(X122,unordered_pair(X123,X124)),inference(resolution,[status(thm)],[c36, reflexivity])).
% 8.11/8.32 cnf(c27,plain,in(skolem0005(X59,X58),X59)|subset(X59,X58),inference(split_conjunct,[status(thm)],[c25])).
% 8.11/8.32 fof(d1_tarski,axiom,(![A]:(![B]:(B=singleton(A)<=>(![C]:(in(C,B)<=>C=A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d1_tarski)).
% 8.11/8.32 fof(c41,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])).
% 8.11/8.32 fof(c42,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)],[c41])).
% 8.11/8.32 fof(c43,plain,((![X22]:(![X23]:(X23!=singleton(X22)|((![X24]:(~in(X24,X23)|X24=X22))&(![X25]:(X25!=X22|in(X25,X23)))))))&(![X26]:(![X27]:((?[X28]:((~in(X28,X27)|X28!=X26)&(in(X28,X27)|X28=X26)))|X27=singleton(X26))))),inference(variable_rename,[status(thm)],[c42])).
% 8.11/8.32 fof(c45,plain,(![X22]:(![X23]:(![X24]:(![X25]:(![X26]:(![X27]:((X23!=singleton(X22)|((~in(X24,X23)|X24=X22)&(X25!=X22|in(X25,X23))))&(((~in(skolem0007(X26,X27),X27)|skolem0007(X26,X27)!=X26)&(in(skolem0007(X26,X27),X27)|skolem0007(X26,X27)=X26))|X27=singleton(X26))))))))),inference(shift_quantors,[status(thm)],[fof(c44,plain,((![X22]:(![X23]:(X23!=singleton(X22)|((![X24]:(~in(X24,X23)|X24=X22))&(![X25]:(X25!=X22|in(X25,X23)))))))&(![X26]:(![X27]:(((~in(skolem0007(X26,X27),X27)|skolem0007(X26,X27)!=X26)&(in(skolem0007(X26,X27),X27)|skolem0007(X26,X27)=X26))|X27=singleton(X26))))),inference(skolemize,[status(esa)],[c43])).])).
% 8.11/8.32 fof(c46,plain,(![X22]:(![X23]:(![X24]:(![X25]:(![X26]:(![X27]:(((X23!=singleton(X22)|(~in(X24,X23)|X24=X22))&(X23!=singleton(X22)|(X25!=X22|in(X25,X23))))&(((~in(skolem0007(X26,X27),X27)|skolem0007(X26,X27)!=X26)|X27=singleton(X26))&((in(skolem0007(X26,X27),X27)|skolem0007(X26,X27)=X26)|X27=singleton(X26)))))))))),inference(distribute,[status(thm)],[c45])).
% 8.11/8.32 cnf(c47,plain,X79!=singleton(X77)|~in(X78,X79)|X78=X77,inference(split_conjunct,[status(thm)],[c46])).
% 8.11/8.32 cnf(c75,plain,~in(X81,singleton(X80))|X81=X80,inference(resolution,[status(thm)],[c47, reflexivity])).
% 8.11/8.32 cnf(c76,plain,skolem0005(singleton(X232),X231)=X232|subset(singleton(X232),X231),inference(resolution,[status(thm)],[c75, c27])).
% 8.11/8.32 cnf(c289,plain,subset(singleton(X2229),X2228)|in(skolem0005(singleton(X2229),X2228),unordered_pair(X2229,X2230)),inference(resolution,[status(thm)],[c76, c96])).
% 8.11/8.32 cnf(c23920,plain,subset(singleton(X2232),unordered_pair(X2232,X2231)),inference(resolution,[status(thm)],[c289, c28])).
% 8.11/8.32 cnf(c23927,plain,$false,inference(resolution,[status(thm)],[c23920, c9])).
% 8.11/8.32 % SZS output end CNFRefutation
% 8.11/8.32
% 8.11/8.32 % Initial clauses : 27
% 8.11/8.32 % Processed clauses : 480
% 8.11/8.32 % Factors computed : 36
% 8.11/8.32 % Resolvents computed: 23840
% 8.11/8.32 % Tautologies deleted: 8
% 8.11/8.32 % Forward subsumed : 539
% 8.11/8.32 % Backward subsumed : 2
% 8.11/8.32 % -------- CPU Time ---------
% 8.11/8.32 % User time : 7.869 s
% 8.11/8.32 % System time : 0.082 s
% 8.11/8.32 % Total time : 7.951 s
%------------------------------------------------------------------------------