%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SEU144+1 : TPTP v8.1.2. Released v3.3.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:39 EDT 2024
% Result : Theorem 0.37s 0.59s
% Output : Refutation 0.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : SEU144+1 : TPTP v8.1.2. Released v3.3.0.
% 0.08/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.35 % Computer : n003.cluster.edu
% 0.12/0.35 % Model : x86_64 x86_64
% 0.12/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.35 % Memory : 8042.1875MB
% 0.12/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.35 % CPULimit : 300
% 0.12/0.35 % WCLimit : 300
% 0.12/0.35 % DateTime : Wed May 8 11:10:08 EDT 2024
% 0.12/0.35 % CPUTime :
% 0.37/0.59 % Version: 1.5
% 0.37/0.59 % SZS status Theorem
% 0.37/0.59 % SZS output start CNFRefutation
% 0.37/0.59 fof(l2_zfmisc_1,conjecture,(![A]:(![B]:(subset(singleton(A),B)<=>in(A,B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l2_zfmisc_1)).
% 0.37/0.59 fof(c6,negated_conjecture,(~(![A]:(![B]:(subset(singleton(A),B)<=>in(A,B))))),inference(assume_negation,[status(cth)],[l2_zfmisc_1])).
% 0.37/0.59 fof(c7,negated_conjecture,(?[A]:(?[B]:((~subset(singleton(A),B)|~in(A,B))&(subset(singleton(A),B)|in(A,B))))),inference(fof_nnf,[status(thm)],[c6])).
% 0.37/0.59 fof(c8,negated_conjecture,(?[X3]:(?[X4]:((~subset(singleton(X3),X4)|~in(X3,X4))&(subset(singleton(X3),X4)|in(X3,X4))))),inference(variable_rename,[status(thm)],[c7])).
% 0.37/0.59 fof(c9,negated_conjecture,((~subset(singleton(skolem0001),skolem0002)|~in(skolem0001,skolem0002))&(subset(singleton(skolem0001),skolem0002)|in(skolem0001,skolem0002))),inference(skolemize,[status(esa)],[c8])).
% 0.37/0.59 cnf(c11,negated_conjecture,subset(singleton(skolem0001),skolem0002)|in(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c9])).
% 0.37/0.59 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)).
% 0.37/0.59 fof(c13,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])).
% 0.37/0.59 fof(c14,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)],[c13])).
% 0.37/0.59 fof(c15,plain,((![X5]:(![X6]:(~subset(X5,X6)|(![X7]:(~in(X7,X5)|in(X7,X6))))))&(![X8]:(![X9]:((?[X10]:(in(X10,X8)&~in(X10,X9)))|subset(X8,X9))))),inference(variable_rename,[status(thm)],[c14])).
% 0.37/0.59 fof(c17,plain,(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:((~subset(X5,X6)|(~in(X7,X5)|in(X7,X6)))&((in(skolem0003(X8,X9),X8)&~in(skolem0003(X8,X9),X9))|subset(X8,X9)))))))),inference(shift_quantors,[status(thm)],[fof(c16,plain,((![X5]:(![X6]:(~subset(X5,X6)|(![X7]:(~in(X7,X5)|in(X7,X6))))))&(![X8]:(![X9]:((in(skolem0003(X8,X9),X8)&~in(skolem0003(X8,X9),X9))|subset(X8,X9))))),inference(skolemize,[status(esa)],[c15])).])).
% 0.37/0.59 fof(c18,plain,(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:((~subset(X5,X6)|(~in(X7,X5)|in(X7,X6)))&((in(skolem0003(X8,X9),X8)|subset(X8,X9))&(~in(skolem0003(X8,X9),X9)|subset(X8,X9))))))))),inference(distribute,[status(thm)],[c17])).
% 0.37/0.59 cnf(c19,plain,~subset(X44,X46)|~in(X45,X44)|in(X45,X46),inference(split_conjunct,[status(thm)],[c18])).
% 0.37/0.59 cnf(reflexivity,axiom,X20=X20,theory(equality)).
% 0.37/0.59 fof(d1_tarski,axiom,(![A]:(![B]:(B=singleton(A)<=>(![C]:(in(C,B)<=>C=A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', d1_tarski)).
% 0.37/0.59 fof(c22,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])).
% 0.37/0.59 fof(c23,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)],[c22])).
% 0.37/0.59 fof(c24,plain,((![X11]:(![X12]:(X12!=singleton(X11)|((![X13]:(~in(X13,X12)|X13=X11))&(![X14]:(X14!=X11|in(X14,X12)))))))&(![X15]:(![X16]:((?[X17]:((~in(X17,X16)|X17!=X15)&(in(X17,X16)|X17=X15)))|X16=singleton(X15))))),inference(variable_rename,[status(thm)],[c23])).
% 0.37/0.59 fof(c26,plain,(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:((X12!=singleton(X11)|((~in(X13,X12)|X13=X11)&(X14!=X11|in(X14,X12))))&(((~in(skolem0004(X15,X16),X16)|skolem0004(X15,X16)!=X15)&(in(skolem0004(X15,X16),X16)|skolem0004(X15,X16)=X15))|X16=singleton(X15))))))))),inference(shift_quantors,[status(thm)],[fof(c25,plain,((![X11]:(![X12]:(X12!=singleton(X11)|((![X13]:(~in(X13,X12)|X13=X11))&(![X14]:(X14!=X11|in(X14,X12)))))))&(![X15]:(![X16]:(((~in(skolem0004(X15,X16),X16)|skolem0004(X15,X16)!=X15)&(in(skolem0004(X15,X16),X16)|skolem0004(X15,X16)=X15))|X16=singleton(X15))))),inference(skolemize,[status(esa)],[c24])).])).
% 0.37/0.59 fof(c27,plain,(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:(((X12!=singleton(X11)|(~in(X13,X12)|X13=X11))&(X12!=singleton(X11)|(X14!=X11|in(X14,X12))))&(((~in(skolem0004(X15,X16),X16)|skolem0004(X15,X16)!=X15)|X16=singleton(X15))&((in(skolem0004(X15,X16),X16)|skolem0004(X15,X16)=X15)|X16=singleton(X15)))))))))),inference(distribute,[status(thm)],[c26])).
% 0.37/0.59 cnf(c29,plain,X68!=singleton(X69)|X70!=X69|in(X70,X68),inference(split_conjunct,[status(thm)],[c27])).
% 0.37/0.59 cnf(c58,plain,X73!=X74|in(X73,singleton(X74)),inference(resolution,[status(thm)],[c29, reflexivity])).
% 0.37/0.59 cnf(c59,plain,in(X75,singleton(X75)),inference(resolution,[status(thm)],[c58, reflexivity])).
% 0.37/0.59 cnf(c61,plain,~subset(singleton(X78),X79)|in(X78,X79),inference(resolution,[status(thm)],[c59, c19])).
% 0.37/0.59 cnf(c66,plain,in(skolem0001,skolem0002),inference(resolution,[status(thm)],[c61, c11])).
% 0.37/0.59 cnf(c10,negated_conjecture,~subset(singleton(skolem0001),skolem0002)|~in(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c9])).
% 0.37/0.59 cnf(c21,plain,~in(skolem0003(X40,X39),X39)|subset(X40,X39),inference(split_conjunct,[status(thm)],[c18])).
% 0.37/0.59 cnf(c1,axiom,X50!=X49|X48!=X47|~in(X50,X48)|in(X49,X47),theory(equality)).
% 0.37/0.59 cnf(c90,plain,skolem0001!=X99|skolem0002!=X100|in(X99,X100),inference(resolution,[status(thm)],[c66, c1])).
% 0.37/0.59 cnf(c104,plain,skolem0001!=X101|in(X101,skolem0002),inference(resolution,[status(thm)],[c90, reflexivity])).
% 0.37/0.59 cnf(symmetry,axiom,X23!=X22|X22=X23,theory(equality)).
% 0.37/0.59 cnf(c28,plain,X52!=singleton(X53)|~in(X51,X52)|X51=X53,inference(split_conjunct,[status(thm)],[c27])).
% 0.37/0.59 cnf(c50,plain,~in(X54,singleton(X55))|X54=X55,inference(resolution,[status(thm)],[c28, reflexivity])).
% 0.37/0.59 cnf(c20,plain,in(skolem0003(X35,X34),X35)|subset(X35,X34),inference(split_conjunct,[status(thm)],[c18])).
% 0.37/0.59 cnf(c45,plain,~in(skolem0001,skolem0002)|in(skolem0003(singleton(skolem0001),skolem0002),singleton(skolem0001)),inference(resolution,[status(thm)],[c10, c20])).
% 0.37/0.59 cnf(c121,plain,in(skolem0003(singleton(skolem0001),skolem0002),singleton(skolem0001)),inference(resolution,[status(thm)],[c45, c66])).
% 0.37/0.59 cnf(c127,plain,skolem0003(singleton(skolem0001),skolem0002)=skolem0001,inference(resolution,[status(thm)],[c121, c50])).
% 0.37/0.59 cnf(c137,plain,skolem0001=skolem0003(singleton(skolem0001),skolem0002),inference(resolution,[status(thm)],[c127, symmetry])).
% 0.37/0.59 cnf(c145,plain,in(skolem0003(singleton(skolem0001),skolem0002),skolem0002),inference(resolution,[status(thm)],[c137, c104])).
% 0.37/0.59 cnf(c151,plain,subset(singleton(skolem0001),skolem0002),inference(resolution,[status(thm)],[c145, c21])).
% 0.37/0.59 cnf(c156,plain,~in(skolem0001,skolem0002),inference(resolution,[status(thm)],[c151, c10])).
% 0.37/0.59 cnf(c160,plain,$false,inference(resolution,[status(thm)],[c156, c66])).
% 0.37/0.59 % SZS output end CNFRefutation
% 0.37/0.59
% 0.37/0.59 % Initial clauses : 18
% 0.37/0.59 % Processed clauses : 52
% 0.37/0.59 % Factors computed : 3
% 0.37/0.59 % Resolvents computed: 135
% 0.37/0.59 % Tautologies deleted: 3
% 0.37/0.59 % Forward subsumed : 17
% 0.37/0.59 % Backward subsumed : 3
% 0.37/0.59 % -------- CPU Time ---------
% 0.37/0.59 % User time : 0.208 s
% 0.37/0.59 % System time : 0.016 s
% 0.37/0.59 % Total time : 0.224 s
%------------------------------------------------------------------------------