%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET976+1 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n013.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 2.84s 3.00s
% Output : Refutation 2.84s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SET976+1 : TPTP v8.1.2. Released v3.2.0.
% 0.07/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n013.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 19:40:08 EDT 2024
% 0.13/0.35 % CPUTime :
% 2.84/3.00 % Version: 1.5
% 2.84/3.00 % SZS status Theorem
% 2.84/3.00 % SZS output start CNFRefutation
% 2.84/3.00 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)).
% 2.84/3.00 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])).
% 2.84/3.00 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])).
% 2.84/3.00 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])).])).
% 2.84/3.00 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])).
% 2.84/3.00 cnf(c26,plain,~in(ordered_pair(X67,X68),cartesian_product2(X66,X69))|in(X67,X66),inference(split_conjunct,[status(thm)],[c25])).
% 2.84/3.00 fof(t129_zfmisc_1,conjecture,(![A]:(![B]:(![C]:(![D]:(in(ordered_pair(A,B),cartesian_product2(C,singleton(D)))<=>(in(A,C)&B=D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', t129_zfmisc_1)).
% 2.84/3.00 fof(c6,negated_conjecture,(~(![A]:(![B]:(![C]:(![D]:(in(ordered_pair(A,B),cartesian_product2(C,singleton(D)))<=>(in(A,C)&B=D))))))),inference(assume_negation,[status(cth)],[t129_zfmisc_1])).
% 2.84/3.00 fof(c7,negated_conjecture,(?[A]:(?[B]:(?[C]:(?[D]:((~in(ordered_pair(A,B),cartesian_product2(C,singleton(D)))|(~in(A,C)|B!=D))&(in(ordered_pair(A,B),cartesian_product2(C,singleton(D)))|(in(A,C)&B=D))))))),inference(fof_nnf,[status(thm)],[c6])).
% 2.84/3.00 fof(c8,negated_conjecture,(?[X2]:(?[X3]:(?[X4]:(?[X5]:((~in(ordered_pair(X2,X3),cartesian_product2(X4,singleton(X5)))|(~in(X2,X4)|X3!=X5))&(in(ordered_pair(X2,X3),cartesian_product2(X4,singleton(X5)))|(in(X2,X4)&X3=X5))))))),inference(variable_rename,[status(thm)],[c7])).
% 2.84/3.00 fof(c9,negated_conjecture,((~in(ordered_pair(skolem0001,skolem0002),cartesian_product2(skolem0003,singleton(skolem0004)))|(~in(skolem0001,skolem0003)|skolem0002!=skolem0004))&(in(ordered_pair(skolem0001,skolem0002),cartesian_product2(skolem0003,singleton(skolem0004)))|(in(skolem0001,skolem0003)&skolem0002=skolem0004))),inference(skolemize,[status(esa)],[c8])).
% 2.84/3.00 fof(c10,negated_conjecture,((~in(ordered_pair(skolem0001,skolem0002),cartesian_product2(skolem0003,singleton(skolem0004)))|(~in(skolem0001,skolem0003)|skolem0002!=skolem0004))&((in(ordered_pair(skolem0001,skolem0002),cartesian_product2(skolem0003,singleton(skolem0004)))|in(skolem0001,skolem0003))&(in(ordered_pair(skolem0001,skolem0002),cartesian_product2(skolem0003,singleton(skolem0004)))|skolem0002=skolem0004))),inference(distribute,[status(thm)],[c9])).
% 2.84/3.00 cnf(c12,negated_conjecture,in(ordered_pair(skolem0001,skolem0002),cartesian_product2(skolem0003,singleton(skolem0004)))|in(skolem0001,skolem0003),inference(split_conjunct,[status(thm)],[c10])).
% 2.84/3.00 cnf(c89,plain,in(skolem0001,skolem0003),inference(resolution,[status(thm)],[c12, c26])).
% 2.84/3.00 cnf(reflexivity,axiom,X31=X31,theory(equality)).
% 2.84/3.00 fof(d1_tarski,axiom,(![A]:(![B]:(B=singleton(A)<=>(![C]:(in(C,B)<=>C=A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', d1_tarski)).
% 2.84/3.00 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])).
% 2.84/3.00 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])).
% 2.84/3.00 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])).
% 2.84/3.00 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])).])).
% 2.84/3.00 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])).
% 2.84/3.00 cnf(c40,plain,X75!=singleton(X76)|~in(X74,X75)|X74=X76,inference(split_conjunct,[status(thm)],[c39])).
% 2.84/3.00 cnf(c66,plain,~in(X81,singleton(X82))|X81=X82,inference(resolution,[status(thm)],[c40, reflexivity])).
% 2.84/3.00 cnf(c27,plain,~in(ordered_pair(X71,X72),cartesian_product2(X70,X73))|in(X72,X73),inference(split_conjunct,[status(thm)],[c25])).
% 2.84/3.00 cnf(c13,negated_conjecture,in(ordered_pair(skolem0001,skolem0002),cartesian_product2(skolem0003,singleton(skolem0004)))|skolem0002=skolem0004,inference(split_conjunct,[status(thm)],[c10])).
% 2.84/3.00 cnf(c109,plain,skolem0002=skolem0004|in(skolem0002,singleton(skolem0004)),inference(resolution,[status(thm)],[c13, c27])).
% 2.84/3.00 cnf(c183,plain,skolem0002=skolem0004,inference(resolution,[status(thm)],[c109, c66])).
% 2.84/3.00 cnf(c11,negated_conjecture,~in(ordered_pair(skolem0001,skolem0002),cartesian_product2(skolem0003,singleton(skolem0004)))|~in(skolem0001,skolem0003)|skolem0002!=skolem0004,inference(split_conjunct,[status(thm)],[c10])).
% 2.84/3.00 cnf(c28,plain,~in(X130,X131)|~in(X129,X128)|in(ordered_pair(X130,X129),cartesian_product2(X131,X128)),inference(split_conjunct,[status(thm)],[c25])).
% 2.84/3.00 cnf(c41,plain,X83!=singleton(X84)|X85!=X84|in(X85,X83),inference(split_conjunct,[status(thm)],[c39])).
% 2.84/3.00 cnf(c70,plain,X87!=X86|in(X87,singleton(X86)),inference(resolution,[status(thm)],[c41, reflexivity])).
% 2.84/3.00 cnf(c175,plain,in(skolem0002,singleton(skolem0004)),inference(resolution,[status(thm)],[c109, c70])).
% 2.84/3.00 cnf(c259,plain,~in(X860,X859)|in(ordered_pair(X860,skolem0002),cartesian_product2(X859,singleton(skolem0004))),inference(resolution,[status(thm)],[c175, c28])).
% 2.84/3.00 cnf(c8025,plain,in(ordered_pair(skolem0001,skolem0002),cartesian_product2(skolem0003,singleton(skolem0004))),inference(resolution,[status(thm)],[c259, c89])).
% 2.84/3.00 cnf(c8334,plain,~in(skolem0001,skolem0003)|skolem0002!=skolem0004,inference(resolution,[status(thm)],[c8025, c11])).
% 2.84/3.00 cnf(c8340,plain,~in(skolem0001,skolem0003),inference(resolution,[status(thm)],[c8334, c183])).
% 2.84/3.00 cnf(c8468,plain,$false,inference(resolution,[status(thm)],[c8340, c89])).
% 2.84/3.00 % SZS output end CNFRefutation
% 2.84/3.00
% 2.84/3.00 % Initial clauses : 25
% 2.84/3.00 % Processed clauses : 370
% 2.84/3.00 % Factors computed : 8
% 2.84/3.00 % Resolvents computed: 8411
% 2.84/3.00 % Tautologies deleted: 6
% 2.84/3.00 % Forward subsumed : 447
% 2.84/3.00 % Backward subsumed : 10
% 2.84/3.00 % -------- CPU Time ---------
% 2.84/3.00 % User time : 2.613 s
% 2.84/3.00 % System time : 0.031 s
% 2.84/3.00 % Total time : 2.644 s
%------------------------------------------------------------------------------