%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET906+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n011.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:20 EDT 2024
% Result : Theorem 1.43s 1.66s
% Output : Refutation 1.43s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : SET906+1 : TPTP v8.1.2. Released v3.2.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n011.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Wed May 8 19:16:23 EDT 2024
% 0.15/0.36 % CPUTime :
% 1.43/1.66 % Version: 1.5
% 1.43/1.66 % SZS status Theorem
% 1.43/1.66 % SZS output start CNFRefutation
% 1.43/1.66 fof(t47_zfmisc_1,conjecture,(![A]:(![B]:(![C]:(subset(set_union2(unordered_pair(A,B),C),C)=>in(A,C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t47_zfmisc_1)).
% 1.43/1.66 fof(c5,negated_conjecture,(~(![A]:(![B]:(![C]:(subset(set_union2(unordered_pair(A,B),C),C)=>in(A,C)))))),inference(assume_negation,[status(cth)],[t47_zfmisc_1])).
% 1.43/1.66 fof(c6,negated_conjecture,(?[A]:(?[B]:(?[C]:(subset(set_union2(unordered_pair(A,B),C),C)&~in(A,C))))),inference(fof_nnf,[status(thm)],[c5])).
% 1.43/1.66 fof(c7,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(subset(set_union2(unordered_pair(X2,X3),X4),X4)&~in(X2,X4))))),inference(variable_rename,[status(thm)],[c6])).
% 1.43/1.66 fof(c8,negated_conjecture,(subset(set_union2(unordered_pair(skolem0001,skolem0002),skolem0003),skolem0003)&~in(skolem0001,skolem0003)),inference(skolemize,[status(esa)],[c7])).
% 1.43/1.66 cnf(c10,negated_conjecture,~in(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c8])).
% 1.43/1.66 cnf(c9,negated_conjecture,subset(set_union2(unordered_pair(skolem0001,skolem0002),skolem0003),skolem0003),inference(split_conjunct,[status(thm)],[c8])).
% 1.43/1.66 fof(d3_tarski,axiom,(![A]:(![B]:(subset(A,B)<=>(![C]:(in(C,A)=>in(C,B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', d3_tarski)).
% 1.43/1.66 fof(c36,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])).
% 1.43/1.66 fof(c37,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)],[c36])).
% 1.43/1.66 fof(c38,plain,((![X13]:(![X14]:(~subset(X13,X14)|(![X15]:(~in(X15,X13)|in(X15,X14))))))&(![X16]:(![X17]:((?[X18]:(in(X18,X16)&~in(X18,X17)))|subset(X16,X17))))),inference(variable_rename,[status(thm)],[c37])).
% 1.43/1.66 fof(c40,plain,(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:((~subset(X13,X14)|(~in(X15,X13)|in(X15,X14)))&((in(skolem0006(X16,X17),X16)&~in(skolem0006(X16,X17),X17))|subset(X16,X17)))))))),inference(shift_quantors,[status(thm)],[fof(c39,plain,((![X13]:(![X14]:(~subset(X13,X14)|(![X15]:(~in(X15,X13)|in(X15,X14))))))&(![X16]:(![X17]:((in(skolem0006(X16,X17),X16)&~in(skolem0006(X16,X17),X17))|subset(X16,X17))))),inference(skolemize,[status(esa)],[c38])).])).
% 1.43/1.66 fof(c41,plain,(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:((~subset(X13,X14)|(~in(X15,X13)|in(X15,X14)))&((in(skolem0006(X16,X17),X16)|subset(X16,X17))&(~in(skolem0006(X16,X17),X17)|subset(X16,X17))))))))),inference(distribute,[status(thm)],[c40])).
% 1.43/1.66 cnf(c42,plain,~subset(X111,X110)|~in(X109,X111)|in(X109,X110),inference(split_conjunct,[status(thm)],[c41])).
% 1.43/1.66 cnf(reflexivity,axiom,X43=X43,theory(equality)).
% 1.43/1.66 fof(d2_xboole_0,axiom,(![A]:(![B]:(![C]:(C=set_union2(A,B)<=>(![D]:(in(D,C)<=>(in(D,A)|in(D,B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', d2_xboole_0)).
% 1.43/1.66 fof(c45,plain,(![A]:(![B]:(![C]:((C!=set_union2(A,B)|(![D]:((~in(D,C)|(in(D,A)|in(D,B)))&((~in(D,A)&~in(D,B))|in(D,C)))))&((?[D]:((~in(D,C)|(~in(D,A)&~in(D,B)))&(in(D,C)|(in(D,A)|in(D,B)))))|C=set_union2(A,B)))))),inference(fof_nnf,[status(thm)],[d2_xboole_0])).
% 1.43/1.66 fof(c46,plain,((![A]:(![B]:(![C]:(C!=set_union2(A,B)|((![D]:(~in(D,C)|(in(D,A)|in(D,B))))&(![D]:((~in(D,A)&~in(D,B))|in(D,C))))))))&(![A]:(![B]:(![C]:((?[D]:((~in(D,C)|(~in(D,A)&~in(D,B)))&(in(D,C)|(in(D,A)|in(D,B)))))|C=set_union2(A,B)))))),inference(shift_quantors,[status(thm)],[c45])).
% 1.43/1.66 fof(c47,plain,((![X19]:(![X20]:(![X21]:(X21!=set_union2(X19,X20)|((![X22]:(~in(X22,X21)|(in(X22,X19)|in(X22,X20))))&(![X23]:((~in(X23,X19)&~in(X23,X20))|in(X23,X21))))))))&(![X24]:(![X25]:(![X26]:((?[X27]:((~in(X27,X26)|(~in(X27,X24)&~in(X27,X25)))&(in(X27,X26)|(in(X27,X24)|in(X27,X25)))))|X26=set_union2(X24,X25)))))),inference(variable_rename,[status(thm)],[c46])).
% 1.43/1.66 fof(c49,plain,(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:(![X25]:(![X26]:((X21!=set_union2(X19,X20)|((~in(X22,X21)|(in(X22,X19)|in(X22,X20)))&((~in(X23,X19)&~in(X23,X20))|in(X23,X21))))&(((~in(skolem0007(X24,X25,X26),X26)|(~in(skolem0007(X24,X25,X26),X24)&~in(skolem0007(X24,X25,X26),X25)))&(in(skolem0007(X24,X25,X26),X26)|(in(skolem0007(X24,X25,X26),X24)|in(skolem0007(X24,X25,X26),X25))))|X26=set_union2(X24,X25))))))))))),inference(shift_quantors,[status(thm)],[fof(c48,plain,((![X19]:(![X20]:(![X21]:(X21!=set_union2(X19,X20)|((![X22]:(~in(X22,X21)|(in(X22,X19)|in(X22,X20))))&(![X23]:((~in(X23,X19)&~in(X23,X20))|in(X23,X21))))))))&(![X24]:(![X25]:(![X26]:(((~in(skolem0007(X24,X25,X26),X26)|(~in(skolem0007(X24,X25,X26),X24)&~in(skolem0007(X24,X25,X26),X25)))&(in(skolem0007(X24,X25,X26),X26)|(in(skolem0007(X24,X25,X26),X24)|in(skolem0007(X24,X25,X26),X25))))|X26=set_union2(X24,X25)))))),inference(skolemize,[status(esa)],[c47])).])).
% 1.43/1.66 fof(c50,plain,(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:(![X25]:(![X26]:(((X21!=set_union2(X19,X20)|(~in(X22,X21)|(in(X22,X19)|in(X22,X20))))&((X21!=set_union2(X19,X20)|(~in(X23,X19)|in(X23,X21)))&(X21!=set_union2(X19,X20)|(~in(X23,X20)|in(X23,X21)))))&((((~in(skolem0007(X24,X25,X26),X26)|~in(skolem0007(X24,X25,X26),X24))|X26=set_union2(X24,X25))&((~in(skolem0007(X24,X25,X26),X26)|~in(skolem0007(X24,X25,X26),X25))|X26=set_union2(X24,X25)))&((in(skolem0007(X24,X25,X26),X26)|(in(skolem0007(X24,X25,X26),X24)|in(skolem0007(X24,X25,X26),X25)))|X26=set_union2(X24,X25)))))))))))),inference(distribute,[status(thm)],[c49])).
% 1.43/1.66 cnf(c52,plain,X130!=set_union2(X131,X132)|~in(X129,X131)|in(X129,X130),inference(split_conjunct,[status(thm)],[c50])).
% 1.43/1.66 cnf(c143,plain,~in(X160,X161)|in(X160,set_union2(X161,X162)),inference(resolution,[status(thm)],[c52, reflexivity])).
% 1.43/1.66 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)).
% 1.43/1.66 fof(c57,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])).
% 1.43/1.66 fof(c58,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)],[c57])).
% 1.43/1.66 fof(c59,plain,((![X28]:(![X29]:(![X30]:(X30!=unordered_pair(X28,X29)|((![X31]:(~in(X31,X30)|(X31=X28|X31=X29)))&(![X32]:((X32!=X28&X32!=X29)|in(X32,X30))))))))&(![X33]:(![X34]:(![X35]:((?[X36]:((~in(X36,X35)|(X36!=X33&X36!=X34))&(in(X36,X35)|(X36=X33|X36=X34))))|X35=unordered_pair(X33,X34)))))),inference(variable_rename,[status(thm)],[c58])).
% 1.43/1.66 fof(c61,plain,(![X28]:(![X29]:(![X30]:(![X31]:(![X32]:(![X33]:(![X34]:(![X35]:((X30!=unordered_pair(X28,X29)|((~in(X31,X30)|(X31=X28|X31=X29))&((X32!=X28&X32!=X29)|in(X32,X30))))&(((~in(skolem0008(X33,X34,X35),X35)|(skolem0008(X33,X34,X35)!=X33&skolem0008(X33,X34,X35)!=X34))&(in(skolem0008(X33,X34,X35),X35)|(skolem0008(X33,X34,X35)=X33|skolem0008(X33,X34,X35)=X34)))|X35=unordered_pair(X33,X34))))))))))),inference(shift_quantors,[status(thm)],[fof(c60,plain,((![X28]:(![X29]:(![X30]:(X30!=unordered_pair(X28,X29)|((![X31]:(~in(X31,X30)|(X31=X28|X31=X29)))&(![X32]:((X32!=X28&X32!=X29)|in(X32,X30))))))))&(![X33]:(![X34]:(![X35]:(((~in(skolem0008(X33,X34,X35),X35)|(skolem0008(X33,X34,X35)!=X33&skolem0008(X33,X34,X35)!=X34))&(in(skolem0008(X33,X34,X35),X35)|(skolem0008(X33,X34,X35)=X33|skolem0008(X33,X34,X35)=X34)))|X35=unordered_pair(X33,X34)))))),inference(skolemize,[status(esa)],[c59])).])).
% 1.43/1.66 fof(c62,plain,(![X28]:(![X29]:(![X30]:(![X31]:(![X32]:(![X33]:(![X34]:(![X35]:(((X30!=unordered_pair(X28,X29)|(~in(X31,X30)|(X31=X28|X31=X29)))&((X30!=unordered_pair(X28,X29)|(X32!=X28|in(X32,X30)))&(X30!=unordered_pair(X28,X29)|(X32!=X29|in(X32,X30)))))&((((~in(skolem0008(X33,X34,X35),X35)|skolem0008(X33,X34,X35)!=X33)|X35=unordered_pair(X33,X34))&((~in(skolem0008(X33,X34,X35),X35)|skolem0008(X33,X34,X35)!=X34)|X35=unordered_pair(X33,X34)))&((in(skolem0008(X33,X34,X35),X35)|(skolem0008(X33,X34,X35)=X33|skolem0008(X33,X34,X35)=X34))|X35=unordered_pair(X33,X34)))))))))))),inference(distribute,[status(thm)],[c61])).
% 1.43/1.66 cnf(c64,plain,X197!=unordered_pair(X200,X198)|X199!=X200|in(X199,X197),inference(split_conjunct,[status(thm)],[c62])).
% 1.43/1.66 cnf(c243,plain,X201!=X203|in(X201,unordered_pair(X203,X202)),inference(resolution,[status(thm)],[c64, reflexivity])).
% 1.43/1.66 cnf(c248,plain,in(X204,unordered_pair(X204,X205)),inference(resolution,[status(thm)],[c243, reflexivity])).
% 1.43/1.66 cnf(c259,plain,in(X223,set_union2(unordered_pair(X223,X221),X222)),inference(resolution,[status(thm)],[c248, c143])).
% 1.43/1.66 cnf(c280,plain,~subset(set_union2(unordered_pair(X1244,X1241),X1243),X1242)|in(X1244,X1242),inference(resolution,[status(thm)],[c259, c42])).
% 1.43/1.66 cnf(c3178,plain,in(skolem0001,skolem0003),inference(resolution,[status(thm)],[c280, c9])).
% 1.43/1.66 cnf(c3196,plain,$false,inference(resolution,[status(thm)],[c3178, c10])).
% 1.43/1.66 % SZS output end CNFRefutation
% 1.43/1.66
% 1.43/1.66 % Initial clauses : 34
% 1.43/1.66 % Processed clauses : 259
% 1.43/1.66 % Factors computed : 38
% 1.43/1.66 % Resolvents computed: 3089
% 1.43/1.66 % Tautologies deleted: 14
% 1.43/1.66 % Forward subsumed : 289
% 1.43/1.66 % Backward subsumed : 4
% 1.43/1.66 % -------- CPU Time ---------
% 1.43/1.66 % User time : 1.274 s
% 1.43/1.66 % System time : 0.018 s
% 1.43/1.66 % Total time : 1.292 s
%------------------------------------------------------------------------------