%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET893+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n003.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 211.94s 212.11s
% Output : Refutation 211.94s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : SET893+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 : n003.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:26:52 EDT 2024
% 0.15/0.36 % CPUTime :
% 211.94/212.11 % Version: 1.5
% 211.94/212.11 % SZS status Theorem
% 211.94/212.11 % SZS output start CNFRefutation
% 211.94/212.11 cnf(reflexivity,axiom,X31=X31,theory(equality)).
% 211.94/212.11 fof(d1_tarski,axiom,(![A]:(![B]:(B=singleton(A)<=>(![C]:(in(C,B)<=>C=A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', d1_tarski)).
% 211.94/212.11 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])).
% 211.94/212.11 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])).
% 211.94/212.11 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])).
% 211.94/212.11 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])).])).
% 211.94/212.11 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])).
% 211.94/212.11 cnf(c40,plain,X76!=singleton(X75)|~in(X74,X76)|X74=X75,inference(split_conjunct,[status(thm)],[c39])).
% 211.94/212.11 cnf(c66,plain,~in(X82,singleton(X81))|X82=X81,inference(resolution,[status(thm)],[c40, reflexivity])).
% 211.94/212.11 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/sandbox/benchmark/theBenchmark.p', l55_zfmisc_1)).
% 211.94/212.11 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])).
% 211.94/212.11 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])).
% 211.94/212.11 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])).])).
% 211.94/212.11 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])).
% 211.94/212.11 cnf(c26,plain,~in(ordered_pair(X66,X69),cartesian_product2(X68,X67))|in(X66,X68),inference(split_conjunct,[status(thm)],[c25])).
% 211.94/212.11 fof(t34_zfmisc_1,conjecture,(![A]:(![B]:(![C]:(![D]:(in(ordered_pair(A,B),cartesian_product2(singleton(C),singleton(D)))<=>(A=C&B=D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t34_zfmisc_1)).
% 211.94/212.11 fof(c6,negated_conjecture,(~(![A]:(![B]:(![C]:(![D]:(in(ordered_pair(A,B),cartesian_product2(singleton(C),singleton(D)))<=>(A=C&B=D))))))),inference(assume_negation,[status(cth)],[t34_zfmisc_1])).
% 211.94/212.11 fof(c7,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:((~in(ordered_pair(A,B),cartesian_product2(singleton(C),singleton(D)))|(A!=C|B!=D))&(in(ordered_pair(A,B),cartesian_product2(singleton(C),singleton(D)))|(A=C&B=D))))))),inference(fof_nnf,[status(thm)],[c6])).
% 211.94/212.11 fof(c8,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:((~in(ordered_pair(X2,X3),cartesian_product2(singleton(X4),singleton(X5)))|(X2!=X4|X3!=X5))&(in(ordered_pair(X2,X3),cartesian_product2(singleton(X4),singleton(X5)))|(X2=X4&X3=X5))))))),inference(variable_rename,[status(thm)],[c7])).
% 211.94/212.11 fof(c9,negated_conjecture,((~in(ordered_pair(skolem0001,skolem0002),cartesian_product2(singleton(skolem0003),singleton(skolem0004)))|(skolem0001!=skolem0003|skolem0002!=skolem0004))&(in(ordered_pair(skolem0001,skolem0002),cartesian_product2(singleton(skolem0003),singleton(skolem0004)))|(skolem0001=skolem0003&skolem0002=skolem0004))),inference(skolemize,[status(esa)],[c8])).
% 211.94/212.11 fof(c10,negated_conjecture,((~in(ordered_pair(skolem0001,skolem0002),cartesian_product2(singleton(skolem0003),singleton(skolem0004)))|(skolem0001!=skolem0003|skolem0002!=skolem0004))&((in(ordered_pair(skolem0001,skolem0002),cartesian_product2(singleton(skolem0003),singleton(skolem0004)))|skolem0001=skolem0003)&(in(ordered_pair(skolem0001,skolem0002),cartesian_product2(singleton(skolem0003),singleton(skolem0004)))|skolem0002=skolem0004))),inference(distribute,[status(thm)],[c9])).
% 211.94/212.11 cnf(c12,negated_conjecture,in(ordered_pair(skolem0001,skolem0002),cartesian_product2(singleton(skolem0003),singleton(skolem0004)))|skolem0001=skolem0003,inference(split_conjunct,[status(thm)],[c10])).
% 211.94/212.11 cnf(c86,plain,skolem0001=skolem0003|in(skolem0001,singleton(skolem0003)),inference(resolution,[status(thm)],[c12, c26])).
% 211.94/212.11 cnf(c177,plain,skolem0001=skolem0003,inference(resolution,[status(thm)],[c86, c66])).
% 211.94/212.11 cnf(c27,plain,~in(ordered_pair(X70,X73),cartesian_product2(X72,X71))|in(X73,X71),inference(split_conjunct,[status(thm)],[c25])).
% 211.94/212.11 cnf(c13,negated_conjecture,in(ordered_pair(skolem0001,skolem0002),cartesian_product2(singleton(skolem0003),singleton(skolem0004)))|skolem0002=skolem0004,inference(split_conjunct,[status(thm)],[c10])).
% 211.94/212.11 cnf(c124,plain,skolem0002=skolem0004|in(skolem0002,singleton(skolem0004)),inference(resolution,[status(thm)],[c13, c27])).
% 211.94/212.11 cnf(c713,plain,skolem0002=skolem0004,inference(resolution,[status(thm)],[c124, c66])).
% 211.94/212.11 cnf(c11,negated_conjecture,~in(ordered_pair(skolem0001,skolem0002),cartesian_product2(singleton(skolem0003),singleton(skolem0004)))|skolem0001!=skolem0003|skolem0002!=skolem0004,inference(split_conjunct,[status(thm)],[c10])).
% 211.94/212.11 cnf(c41,plain,X85!=singleton(X84)|X83!=X84|in(X83,X85),inference(split_conjunct,[status(thm)],[c39])).
% 211.94/212.11 cnf(c70,plain,X87!=X86|in(X87,singleton(X86)),inference(resolution,[status(thm)],[c41, reflexivity])).
% 211.94/212.11 cnf(c170,plain,in(skolem0001,singleton(skolem0003)),inference(resolution,[status(thm)],[c86, c70])).
% 211.94/212.11 cnf(c28,plain,~in(X135,X134)|~in(X137,X136)|in(ordered_pair(X135,X137),cartesian_product2(X134,X136)),inference(split_conjunct,[status(thm)],[c25])).
% 211.94/212.11 cnf(c708,plain,in(skolem0002,singleton(skolem0004)),inference(resolution,[status(thm)],[c124, c70])).
% 211.94/212.11 cnf(c752,plain,~in(X1987,X1988)|in(ordered_pair(X1987,skolem0002),cartesian_product2(X1988,singleton(skolem0004))),inference(resolution,[status(thm)],[c708, c28])).
% 211.94/212.11 cnf(c47593,plain,in(ordered_pair(skolem0001,skolem0002),cartesian_product2(singleton(skolem0003),singleton(skolem0004))),inference(resolution,[status(thm)],[c752, c170])).
% 211.94/212.11 cnf(c214693,plain,skolem0001!=skolem0003|skolem0002!=skolem0004,inference(resolution,[status(thm)],[c47593, c11])).
% 211.94/212.11 cnf(c214705,plain,skolem0001!=skolem0003,inference(resolution,[status(thm)],[c214693, c713])).
% 211.94/212.11 cnf(c214706,plain,$false,inference(resolution,[status(thm)],[c214705, c177])).
% 211.94/212.11 % SZS output end CNFRefutation
% 211.94/212.11
% 211.94/212.11 % Initial clauses : 25
% 211.94/212.11 % Processed clauses : 2067
% 211.94/212.11 % Factors computed : 18
% 211.94/212.11 % Resolvents computed: 214819
% 211.94/212.11 % Tautologies deleted: 6
% 211.94/212.11 % Forward subsumed : 3501
% 211.94/212.11 % Backward subsumed : 150
% 211.94/212.11 % -------- CPU Time ---------
% 211.94/212.11 % User time : 211.274 s
% 211.94/212.11 % System time : 0.488 s
% 211.94/212.11 % Total time : 211.762 s
%------------------------------------------------------------------------------