%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET890+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n008.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:19 EDT 2024
% Result : Theorem 176.15s 176.36s
% Output : Refutation 176.15s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SET890+1 : TPTP v8.1.2. Released v3.2.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n008.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 19:40:08 EDT 2024
% 0.13/0.35 % CPUTime :
% 176.15/176.36 % Version: 1.5
% 176.15/176.36 % SZS status Theorem
% 176.15/176.36 % SZS output start CNFRefutation
% 176.15/176.36 fof(t31_zfmisc_1,conjecture,(![A]:union(singleton(A))=A),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t31_zfmisc_1)).
% 176.15/176.36 fof(c5,negated_conjecture,(~(![A]:union(singleton(A))=A)),inference(assume_negation,[status(cth)],[t31_zfmisc_1])).
% 176.15/176.36 fof(c6,negated_conjecture,(?[A]:union(singleton(A))!=A),inference(fof_nnf,[status(thm)],[c5])).
% 176.15/176.36 fof(c7,negated_conjecture,(?[X2]:union(singleton(X2))!=X2),inference(variable_rename,[status(thm)],[c6])).
% 176.15/176.36 fof(c8,negated_conjecture,union(singleton(skolem0001))!=skolem0001,inference(skolemize,[status(esa)],[c7])).
% 176.15/176.36 cnf(c9,negated_conjecture,union(singleton(skolem0001))!=skolem0001,inference(split_conjunct,[status(thm)],[c8])).
% 176.15/176.36 cnf(symmetry,axiom,X41!=X40|X40=X41,theory(equality)).
% 176.15/176.36 cnf(reflexivity,axiom,X38=X38,theory(equality)).
% 176.15/176.36 fof(d1_tarski,axiom,(![A]:(![B]:(B=singleton(A)<=>(![C]:(in(C,B)<=>C=A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d1_tarski)).
% 176.15/176.36 fof(c44,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])).
% 176.15/176.36 fof(c45,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)],[c44])).
% 176.15/176.36 fof(c46,plain,((![X25]:(![X26]:(X26!=singleton(X25)|((![X27]:(~in(X27,X26)|X27=X25))&(![X28]:(X28!=X25|in(X28,X26)))))))&(![X29]:(![X30]:((?[X31]:((~in(X31,X30)|X31!=X29)&(in(X31,X30)|X31=X29)))|X30=singleton(X29))))),inference(variable_rename,[status(thm)],[c45])).
% 176.15/176.36 fof(c48,plain,(![X25]:(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:((X26!=singleton(X25)|((~in(X27,X26)|X27=X25)&(X28!=X25|in(X28,X26))))&(((~in(skolem0008(X29,X30),X30)|skolem0008(X29,X30)!=X29)&(in(skolem0008(X29,X30),X30)|skolem0008(X29,X30)=X29))|X30=singleton(X29))))))))),inference(shift_quantors,[status(thm)],[fof(c47,plain,((![X25]:(![X26]:(X26!=singleton(X25)|((![X27]:(~in(X27,X26)|X27=X25))&(![X28]:(X28!=X25|in(X28,X26)))))))&(![X29]:(![X30]:(((~in(skolem0008(X29,X30),X30)|skolem0008(X29,X30)!=X29)&(in(skolem0008(X29,X30),X30)|skolem0008(X29,X30)=X29))|X30=singleton(X29))))),inference(skolemize,[status(esa)],[c46])).])).
% 176.15/176.36 fof(c49,plain,(![X25]:(![X26]:(![X27]:(![X28]:(![X29]:(![X30]:(((X26!=singleton(X25)|(~in(X27,X26)|X27=X25))&(X26!=singleton(X25)|(X28!=X25|in(X28,X26))))&(((~in(skolem0008(X29,X30),X30)|skolem0008(X29,X30)!=X29)|X30=singleton(X29))&((in(skolem0008(X29,X30),X30)|skolem0008(X29,X30)=X29)|X30=singleton(X29)))))))))),inference(distribute,[status(thm)],[c48])).
% 176.15/176.36 cnf(c51,plain,X109!=singleton(X108)|X110!=X108|in(X110,X109),inference(split_conjunct,[status(thm)],[c49])).
% 176.15/176.36 cnf(c94,plain,X114!=X115|in(X114,singleton(X115)),inference(resolution,[status(thm)],[c51, reflexivity])).
% 176.15/176.36 cnf(c96,plain,in(X116,singleton(X116)),inference(resolution,[status(thm)],[c94, reflexivity])).
% 176.15/176.36 fof(d4_tarski,axiom,(![A]:(![B]:(B=union(A)<=>(![C]:(in(C,B)<=>(?[D]:(in(C,D)&in(D,A)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d4_tarski)).
% 176.15/176.36 fof(c23,plain,(![A]:(![B]:((B!=union(A)|(![C]:((~in(C,B)|(?[D]:(in(C,D)&in(D,A))))&((![D]:(~in(C,D)|~in(D,A)))|in(C,B)))))&((?[C]:((~in(C,B)|(![D]:(~in(C,D)|~in(D,A))))&(in(C,B)|(?[D]:(in(C,D)&in(D,A))))))|B=union(A))))),inference(fof_nnf,[status(thm)],[d4_tarski])).
% 176.15/176.36 fof(c24,plain,((![A]:(![B]:(B!=union(A)|((![C]:(~in(C,B)|(?[D]:(in(C,D)&in(D,A)))))&(![C]:((![D]:(~in(C,D)|~in(D,A)))|in(C,B)))))))&(![A]:(![B]:((?[C]:((~in(C,B)|(![D]:(~in(C,D)|~in(D,A))))&(in(C,B)|(?[D]:(in(C,D)&in(D,A))))))|B=union(A))))),inference(shift_quantors,[status(thm)],[c23])).
% 176.15/176.36 fof(c25,plain,((![X8]:(![X9]:(X9!=union(X8)|((![X10]:(~in(X10,X9)|(?[X11]:(in(X10,X11)&in(X11,X8)))))&(![X12]:((![X13]:(~in(X12,X13)|~in(X13,X8)))|in(X12,X9)))))))&(![X14]:(![X15]:((?[X16]:((~in(X16,X15)|(![X17]:(~in(X16,X17)|~in(X17,X14))))&(in(X16,X15)|(?[X18]:(in(X16,X18)&in(X18,X14))))))|X15=union(X14))))),inference(variable_rename,[status(thm)],[c24])).
% 176.15/176.36 fof(c27,plain,(![X8]:(![X9]:(![X10]:(![X12]:(![X13]:(![X14]:(![X15]:(![X17]:((X9!=union(X8)|((~in(X10,X9)|(in(X10,skolem0004(X8,X9,X10))&in(skolem0004(X8,X9,X10),X8)))&((~in(X12,X13)|~in(X13,X8))|in(X12,X9))))&(((~in(skolem0005(X14,X15),X15)|(~in(skolem0005(X14,X15),X17)|~in(X17,X14)))&(in(skolem0005(X14,X15),X15)|(in(skolem0005(X14,X15),skolem0006(X14,X15))&in(skolem0006(X14,X15),X14))))|X15=union(X14))))))))))),inference(shift_quantors,[status(thm)],[fof(c26,plain,((![X8]:(![X9]:(X9!=union(X8)|((![X10]:(~in(X10,X9)|(in(X10,skolem0004(X8,X9,X10))&in(skolem0004(X8,X9,X10),X8))))&(![X12]:((![X13]:(~in(X12,X13)|~in(X13,X8)))|in(X12,X9)))))))&(![X14]:(![X15]:(((~in(skolem0005(X14,X15),X15)|(![X17]:(~in(skolem0005(X14,X15),X17)|~in(X17,X14))))&(in(skolem0005(X14,X15),X15)|(in(skolem0005(X14,X15),skolem0006(X14,X15))&in(skolem0006(X14,X15),X14))))|X15=union(X14))))),inference(skolemize,[status(esa)],[c25])).])).
% 176.15/176.36 fof(c28,plain,(![X8]:(![X9]:(![X10]:(![X12]:(![X13]:(![X14]:(![X15]:(![X17]:((((X9!=union(X8)|(~in(X10,X9)|in(X10,skolem0004(X8,X9,X10))))&(X9!=union(X8)|(~in(X10,X9)|in(skolem0004(X8,X9,X10),X8))))&(X9!=union(X8)|((~in(X12,X13)|~in(X13,X8))|in(X12,X9))))&(((~in(skolem0005(X14,X15),X15)|(~in(skolem0005(X14,X15),X17)|~in(X17,X14)))|X15=union(X14))&(((in(skolem0005(X14,X15),X15)|in(skolem0005(X14,X15),skolem0006(X14,X15)))|X15=union(X14))&((in(skolem0005(X14,X15),X15)|in(skolem0006(X14,X15),X14))|X15=union(X14))))))))))))),inference(distribute,[status(thm)],[c27])).
% 176.15/176.36 cnf(c32,plain,~in(skolem0005(X130,X132),X132)|~in(skolem0005(X130,X132),X131)|~in(X131,X130)|X132=union(X130),inference(split_conjunct,[status(thm)],[c28])).
% 176.15/176.36 cnf(c116,plain,~in(skolem0005(X306,X307),X307)|~in(X307,X306)|X307=union(X306),inference(factor,[status(thm)],[c32])).
% 176.15/176.36 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)).
% 176.15/176.36 fof(c35,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])).
% 176.15/176.36 fof(c36,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)],[c35])).
% 176.15/176.36 fof(c37,plain,((![X19]:(![X20]:(~subset(X19,X20)|(![X21]:(~in(X21,X19)|in(X21,X20))))))&(![X22]:(![X23]:((?[X24]:(in(X24,X22)&~in(X24,X23)))|subset(X22,X23))))),inference(variable_rename,[status(thm)],[c36])).
% 176.15/176.36 fof(c39,plain,(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:((~subset(X19,X20)|(~in(X21,X19)|in(X21,X20)))&((in(skolem0007(X22,X23),X22)&~in(skolem0007(X22,X23),X23))|subset(X22,X23)))))))),inference(shift_quantors,[status(thm)],[fof(c38,plain,((![X19]:(![X20]:(~subset(X19,X20)|(![X21]:(~in(X21,X19)|in(X21,X20))))))&(![X22]:(![X23]:((in(skolem0007(X22,X23),X22)&~in(skolem0007(X22,X23),X23))|subset(X22,X23))))),inference(skolemize,[status(esa)],[c37])).])).
% 176.15/176.36 fof(c40,plain,(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:((~subset(X19,X20)|(~in(X21,X19)|in(X21,X20)))&((in(skolem0007(X22,X23),X22)|subset(X22,X23))&(~in(skolem0007(X22,X23),X23)|subset(X22,X23))))))))),inference(distribute,[status(thm)],[c39])).
% 176.15/176.36 cnf(c41,plain,~subset(X81,X80)|~in(X82,X81)|in(X82,X80),inference(split_conjunct,[status(thm)],[c40])).
% 176.15/176.36 cnf(c33,plain,in(skolem0005(X143,X144),X144)|in(skolem0005(X143,X144),skolem0006(X143,X144))|X144=union(X143),inference(split_conjunct,[status(thm)],[c28])).
% 176.15/176.36 cnf(c136,plain,in(skolem0005(X460,X459),X459)|X459=union(X460)|~subset(skolem0006(X460,X459),X461)|in(skolem0005(X460,X459),X461),inference(resolution,[status(thm)],[c33, c41])).
% 176.15/176.36 fof(d10_xboole_0,axiom,(![A]:(![B]:(A=B<=>(subset(A,B)&subset(B,A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d10_xboole_0)).
% 176.15/176.36 fof(c54,plain,(![A]:(![B]:((A!=B|(subset(A,B)&subset(B,A)))&((~subset(A,B)|~subset(B,A))|A=B)))),inference(fof_nnf,[status(thm)],[d10_xboole_0])).
% 176.15/176.36 fof(c55,plain,((![A]:(![B]:(A!=B|(subset(A,B)&subset(B,A)))))&(![A]:(![B]:((~subset(A,B)|~subset(B,A))|A=B)))),inference(shift_quantors,[status(thm)],[c54])).
% 176.15/176.36 fof(c57,plain,(![X32]:(![X33]:(![X34]:(![X35]:((X32!=X33|(subset(X32,X33)&subset(X33,X32)))&((~subset(X34,X35)|~subset(X35,X34))|X34=X35)))))),inference(shift_quantors,[status(thm)],[fof(c56,plain,((![X32]:(![X33]:(X32!=X33|(subset(X32,X33)&subset(X33,X32)))))&(![X34]:(![X35]:((~subset(X34,X35)|~subset(X35,X34))|X34=X35)))),inference(variable_rename,[status(thm)],[c55])).])).
% 176.15/176.36 fof(c58,plain,(![X32]:(![X33]:(![X34]:(![X35]:(((X32!=X33|subset(X32,X33))&(X32!=X33|subset(X33,X32)))&((~subset(X34,X35)|~subset(X35,X34))|X34=X35)))))),inference(distribute,[status(thm)],[c57])).
% 176.15/176.36 cnf(c59,plain,X46!=X47|subset(X46,X47),inference(split_conjunct,[status(thm)],[c58])).
% 176.15/176.36 cnf(c50,plain,X104!=singleton(X103)|~in(X105,X104)|X105=X103,inference(split_conjunct,[status(thm)],[c49])).
% 176.15/176.36 cnf(c92,plain,~in(X107,singleton(X106))|X107=X106,inference(resolution,[status(thm)],[c50, reflexivity])).
% 176.15/176.36 cnf(c34,plain,in(skolem0005(X152,X153),X153)|in(skolem0006(X152,X153),X152)|X153=union(X152),inference(split_conjunct,[status(thm)],[c28])).
% 176.15/176.36 cnf(c890,plain,~in(X1325,X1324)|X1325=union(X1324)|in(skolem0006(X1324,X1325),X1324),inference(resolution,[status(thm)],[c116, c34])).
% 176.15/176.36 cnf(c12440,plain,X6827=union(singleton(X6827))|in(skolem0006(singleton(X6827),X6827),singleton(X6827)),inference(resolution,[status(thm)],[c890, c96])).
% 176.15/176.36 cnf(c224421,plain,X6828=union(singleton(X6828))|skolem0006(singleton(X6828),X6828)=X6828,inference(resolution,[status(thm)],[c12440, c92])).
% 176.15/176.36 cnf(c224863,plain,X6876=union(singleton(X6876))|subset(skolem0006(singleton(X6876),X6876),X6876),inference(resolution,[status(thm)],[c224421, c59])).
% 176.15/176.36 cnf(c231210,plain,X6914=union(singleton(X6914))|in(skolem0005(singleton(X6914),X6914),X6914),inference(resolution,[status(thm)],[c224863, c136])).
% 176.15/176.36 cnf(c234668,plain,X6915=union(singleton(X6915))|~in(X6915,singleton(X6915)),inference(resolution,[status(thm)],[c231210, c116])).
% 176.15/176.36 cnf(c234769,plain,X6916=union(singleton(X6916)),inference(resolution,[status(thm)],[c234668, c96])).
% 176.15/176.36 cnf(c234800,plain,union(singleton(X6917))=X6917,inference(resolution,[status(thm)],[c234769, symmetry])).
% 176.15/176.36 cnf(c235209,plain,$false,inference(resolution,[status(thm)],[c234800, c9])).
% 176.15/176.36 % SZS output end CNFRefutation
% 176.15/176.36
% 176.15/176.36 % Initial clauses : 30
% 176.15/176.36 % Processed clauses : 1688
% 176.15/176.36 % Factors computed : 49
% 176.15/176.36 % Resolvents computed: 235285
% 176.15/176.36 % Tautologies deleted: 6
% 176.15/176.36 % Forward subsumed : 2950
% 176.15/176.36 % Backward subsumed : 24
% 176.15/176.36 % -------- CPU Time ---------
% 176.15/176.36 % User time : 175.420 s
% 176.15/176.36 % System time : 0.576 s
% 176.15/176.36 % Total time : 175.996 s
%------------------------------------------------------------------------------