%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET975+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n027.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:26 EDT 2024
% Result : Theorem 1.58s 1.80s
% Output : Refutation 1.58s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SET975+1 : TPTP v8.1.2. Released v3.2.0.
% 0.11/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n027.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Wed May 8 18:56:08 EDT 2024
% 0.14/0.34 % CPUTime :
% 1.58/1.80 % Version: 1.5
% 1.58/1.80 % SZS status Theorem
% 1.58/1.80 % SZS output start CNFRefutation
% 1.58/1.80 cnf(reflexivity,axiom,X31=X31,theory(equality)).
% 1.58/1.80 fof(d1_tarski,axiom,(![A]:(![B]:(B=singleton(A)<=>(![C]:(in(C,B)<=>C=A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d1_tarski)).
% 1.58/1.80 fof(c34,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])).
% 1.58/1.80 fof(c35,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)],[c34])).
% 1.58/1.80 fof(c36,plain,((![X20]:(![X21]:(X21!=singleton(X20)|((![X22]:(~in(X22,X21)|X22=X20))&(![X23]:(X23!=X20|in(X23,X21)))))))&(![X24]:(![X25]:((?[X26]:((~in(X26,X25)|X26!=X24)&(in(X26,X25)|X26=X24)))|X25=singleton(X24))))),inference(variable_rename,[status(thm)],[c35])).
% 1.58/1.80 fof(c38,plain,(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:(![X25]:((X21!=singleton(X20)|((~in(X22,X21)|X22=X20)&(X23!=X20|in(X23,X21))))&(((~in(skolem0007(X24,X25),X25)|skolem0007(X24,X25)!=X24)&(in(skolem0007(X24,X25),X25)|skolem0007(X24,X25)=X24))|X25=singleton(X24))))))))),inference(shift_quantors,[status(thm)],[fof(c37,plain,((![X20]:(![X21]:(X21!=singleton(X20)|((![X22]:(~in(X22,X21)|X22=X20))&(![X23]:(X23!=X20|in(X23,X21)))))))&(![X24]:(![X25]:(((~in(skolem0007(X24,X25),X25)|skolem0007(X24,X25)!=X24)&(in(skolem0007(X24,X25),X25)|skolem0007(X24,X25)=X24))|X25=singleton(X24))))),inference(skolemize,[status(esa)],[c36])).])).
% 1.58/1.80 fof(c39,plain,(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:(![X25]:(((X21!=singleton(X20)|(~in(X22,X21)|X22=X20))&(X21!=singleton(X20)|(X23!=X20|in(X23,X21))))&(((~in(skolem0007(X24,X25),X25)|skolem0007(X24,X25)!=X24)|X25=singleton(X24))&((in(skolem0007(X24,X25),X25)|skolem0007(X24,X25)=X24)|X25=singleton(X24)))))))))),inference(distribute,[status(thm)],[c38])).
% 1.58/1.80 cnf(c40,plain,X76!=singleton(X74)|~in(X75,X76)|X75=X74,inference(split_conjunct,[status(thm)],[c39])).
% 1.58/1.80 cnf(c66,plain,~in(X82,singleton(X81))|X82=X81,inference(resolution,[status(thm)],[c40, reflexivity])).
% 1.58/1.80 fof(l55_zfmisc_1,axiom,(![A]:(![B]:(![C]:(![D]:(in(ordered_pair(A,B),cartesian_product2(C,D))<=>(in(A,C)&in(B,D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l55_zfmisc_1)).
% 1.58/1.80 fof(c21,plain,(![A]:(![B]:(![C]:(![D]:((~in(ordered_pair(A,B),cartesian_product2(C,D))|(in(A,C)&in(B,D)))&((~in(A,C)|~in(B,D))|in(ordered_pair(A,B),cartesian_product2(C,D)))))))),inference(fof_nnf,[status(thm)],[l55_zfmisc_1])).
% 1.58/1.80 fof(c22,plain,((![A]:(![B]:(![C]:(![D]:(~in(ordered_pair(A,B),cartesian_product2(C,D))|(in(A,C)&in(B,D)))))))&(![A]:(![B]:(![C]:(![D]:((~in(A,C)|~in(B,D))|in(ordered_pair(A,B),cartesian_product2(C,D)))))))),inference(shift_quantors,[status(thm)],[c21])).
% 1.58/1.80 fof(c24,plain,(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:((~in(ordered_pair(X8,X9),cartesian_product2(X10,X11))|(in(X8,X10)&in(X9,X11)))&((~in(X12,X14)|~in(X13,X15))|in(ordered_pair(X12,X13),cartesian_product2(X14,X15)))))))))))),inference(shift_quantors,[status(thm)],[fof(c23,plain,((![X8]:(![X9]:(![X10]:(![X11]:(~in(ordered_pair(X8,X9),cartesian_product2(X10,X11))|(in(X8,X10)&in(X9,X11)))))))&(![X12]:(![X13]:(![X14]:(![X15]:((~in(X12,X14)|~in(X13,X15))|in(ordered_pair(X12,X13),cartesian_product2(X14,X15)))))))),inference(variable_rename,[status(thm)],[c22])).])).
% 1.58/1.80 fof(c25,plain,(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(((~in(ordered_pair(X8,X9),cartesian_product2(X10,X11))|in(X8,X10))&(~in(ordered_pair(X8,X9),cartesian_product2(X10,X11))|in(X9,X11)))&((~in(X12,X14)|~in(X13,X15))|in(ordered_pair(X12,X13),cartesian_product2(X14,X15)))))))))))),inference(distribute,[status(thm)],[c24])).
% 1.58/1.80 cnf(c26,plain,~in(ordered_pair(X66,X68),cartesian_product2(X67,X69))|in(X66,X67),inference(split_conjunct,[status(thm)],[c25])).
% 1.58/1.80 fof(t128_zfmisc_1,conjecture,(![A]:(![B]:(![C]:(![D]:(in(ordered_pair(A,B),cartesian_product2(singleton(C),D))<=>(A=C&in(B,D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', t128_zfmisc_1)).
% 1.58/1.80 fof(c6,negated_conjecture,(~(![A]:(![B]:(![C]:(![D]:(in(ordered_pair(A,B),cartesian_product2(singleton(C),D))<=>(A=C&in(B,D)))))))),inference(assume_negation,[status(cth)],[t128_zfmisc_1])).
% 1.58/1.80 fof(c7,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:((~in(ordered_pair(A,B),cartesian_product2(singleton(C),D))|(A!=C|~in(B,D)))&(in(ordered_pair(A,B),cartesian_product2(singleton(C),D))|(A=C&in(B,D)))))))),inference(fof_nnf,[status(thm)],[c6])).
% 1.58/1.80 fof(c8,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:((~in(ordered_pair(X2,X3),cartesian_product2(singleton(X4),X5))|(X2!=X4|~in(X3,X5)))&(in(ordered_pair(X2,X3),cartesian_product2(singleton(X4),X5))|(X2=X4&in(X3,X5)))))))),inference(variable_rename,[status(thm)],[c7])).
% 1.58/1.80 fof(c9,negated_conjecture,((~in(ordered_pair(skolem0001,skolem0002),cartesian_product2(singleton(skolem0003),skolem0004))|(skolem0001!=skolem0003|~in(skolem0002,skolem0004)))&(in(ordered_pair(skolem0001,skolem0002),cartesian_product2(singleton(skolem0003),skolem0004))|(skolem0001=skolem0003&in(skolem0002,skolem0004)))),inference(skolemize,[status(esa)],[c8])).
% 1.58/1.80 fof(c10,negated_conjecture,((~in(ordered_pair(skolem0001,skolem0002),cartesian_product2(singleton(skolem0003),skolem0004))|(skolem0001!=skolem0003|~in(skolem0002,skolem0004)))&((in(ordered_pair(skolem0001,skolem0002),cartesian_product2(singleton(skolem0003),skolem0004))|skolem0001=skolem0003)&(in(ordered_pair(skolem0001,skolem0002),cartesian_product2(singleton(skolem0003),skolem0004))|in(skolem0002,skolem0004)))),inference(distribute,[status(thm)],[c9])).
% 1.58/1.80 cnf(c12,negated_conjecture,in(ordered_pair(skolem0001,skolem0002),cartesian_product2(singleton(skolem0003),skolem0004))|skolem0001=skolem0003,inference(split_conjunct,[status(thm)],[c10])).
% 1.58/1.80 cnf(c86,plain,skolem0001=skolem0003|in(skolem0001,singleton(skolem0003)),inference(resolution,[status(thm)],[c12, c26])).
% 1.58/1.80 cnf(c206,plain,skolem0001=skolem0003,inference(resolution,[status(thm)],[c86, c66])).
% 1.58/1.80 cnf(c27,plain,~in(ordered_pair(X70,X72),cartesian_product2(X71,X73))|in(X72,X73),inference(split_conjunct,[status(thm)],[c25])).
% 1.58/1.80 cnf(c13,negated_conjecture,in(ordered_pair(skolem0001,skolem0002),cartesian_product2(singleton(skolem0003),skolem0004))|in(skolem0002,skolem0004),inference(split_conjunct,[status(thm)],[c10])).
% 1.58/1.80 cnf(c128,plain,in(skolem0002,skolem0004),inference(resolution,[status(thm)],[c13, c27])).
% 1.58/1.80 cnf(c11,negated_conjecture,~in(ordered_pair(skolem0001,skolem0002),cartesian_product2(singleton(skolem0003),skolem0004))|skolem0001!=skolem0003|~in(skolem0002,skolem0004),inference(split_conjunct,[status(thm)],[c10])).
% 1.58/1.80 cnf(c41,plain,X85!=singleton(X83)|X84!=X83|in(X84,X85),inference(split_conjunct,[status(thm)],[c39])).
% 1.58/1.80 cnf(c70,plain,X86!=X87|in(X86,singleton(X87)),inference(resolution,[status(thm)],[c41, reflexivity])).
% 1.58/1.80 cnf(c199,plain,in(skolem0001,singleton(skolem0003)),inference(resolution,[status(thm)],[c86, c70])).
% 1.58/1.80 cnf(c28,plain,~in(X122,X120)|~in(X121,X123)|in(ordered_pair(X122,X121),cartesian_product2(X120,X123)),inference(split_conjunct,[status(thm)],[c25])).
% 1.58/1.80 cnf(c152,plain,~in(X383,X384)|in(ordered_pair(X383,skolem0002),cartesian_product2(X384,skolem0004)),inference(resolution,[status(thm)],[c28, c128])).
% 1.58/1.80 cnf(c1235,plain,in(ordered_pair(skolem0001,skolem0002),cartesian_product2(singleton(skolem0003),skolem0004)),inference(resolution,[status(thm)],[c152, c199])).
% 1.58/1.80 cnf(c4402,plain,skolem0001!=skolem0003|~in(skolem0002,skolem0004),inference(resolution,[status(thm)],[c1235, c11])).
% 1.58/1.80 cnf(c4509,plain,skolem0001!=skolem0003,inference(resolution,[status(thm)],[c4402, c128])).
% 1.58/1.80 cnf(c4510,plain,$false,inference(resolution,[status(thm)],[c4509, c206])).
% 1.58/1.80 % SZS output end CNFRefutation
% 1.58/1.80
% 1.58/1.80 % Initial clauses : 25
% 1.58/1.80 % Processed clauses : 291
% 1.58/1.80 % Factors computed : 7
% 1.58/1.80 % Resolvents computed: 4454
% 1.58/1.80 % Tautologies deleted: 5
% 1.58/1.80 % Forward subsumed : 380
% 1.58/1.80 % Backward subsumed : 15
% 1.58/1.80 % -------- CPU Time ---------
% 1.58/1.80 % User time : 1.438 s
% 1.58/1.80 % System time : 0.015 s
% 1.58/1.80 % Total time : 1.453 s
%------------------------------------------------------------------------------